当图神经网络遇见单词方程求解器：学习排序方程（扩展技术报告）
人工智能
2025-07-01 v1 机器学习
摘要
Nielsen变换是求解单词方程的标准方法：通过反复拆分方程并应用简化步骤，对方程进行重写，直到达到解。当通过这种方式求解一组单词方程的 conjunction 时，求解器的性能将在方程被处理的顺序上有很大影响。在本工作中，探索了使用图神经网络（GNN）在求解过程中对单词方程进行排序的问题。为此，提出了一种用于单词方程的新型图基表示，保留跨conjuncts的全局信息，使GNN在排序时拥有整体视图。为了处理conjuncts的可变数量，提出了三种方法来适应多分类任务以解决方程排序问题。GNN的训练借助单词方程的最小不可满足子集（MUSes）完成。实验结果表明，与当前最先进的字符串求解器相比，新框架在基准测试中解决了更多问题，其中每个变量在每个方程中最多出现一次。
引用
@article{arxiv.2506.23784,
title = {When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)},
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Julie Cailler and Chencheng Liang and Philipp Rümmer},
journal= {arXiv preprint arXiv:2506.23784},
year = {2025}
}