用图神经网络排序单词方程，提升求解效率
When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)
- 构建图结构表示保留方程全局信息，支持整体排序
- 基于最小不可满足子集训练，使排序更贴近求解需求
- 在变量不重复的测试中，比现有求解器解决更多问题
Nielsen变换是求解单词方程的标准方法：通过反复拆分方程并应用简化步骤，将方程重写直至获得解。在求解一组连贯的单词方程时，求解器性能高度依赖于方程的处理顺序。本文探索使用图神经网络（GNN）对单词方程进行排序，以优化求解过程。为此，提出一种新的基于图的单词方程表示方法，能够保持各连贯方程间的全局信息，使GNN在排序时具备整体视角。为应对连贯方程数量可变的问题，提出三种将多分类任务适配至方程排序的方法。GNN的训练借助单词方程的最小不可满足子集（MUSes）完成。实验结果表明，在每个变量在每条方程中最多出现一次的基准测试中，该新框架相比现有顶尖字符串求解器，能解决更多问题。
原文摘要 · Abstract (English)
Nielsen transformation is a standard approach for solving word equations: by repeatedly splitting equations and applying simplification steps, equations are rewritten until a solution is reached. When solving a conjunction of word equations in this way, the performance of the solver will depend considerably on the order in which equations are processed. In this work, the use of Graph Neural Networks (GNNs) for ranking word equations before and during the solving process is explored. For this, a novel graph-based representation for word equations is presented, preserving global information across conjuncts, enabling the GNN to have a holistic view during ranking. To handle the variable number of conjuncts, three approaches to adapt a multi-classification task to the problem of ranking equations are proposed. The training of the GNN is done with the help of minimum unsatisfiable subsets (MUSes) of word equations. The experimental results show that, compared to state-of-the-art string solvers, the new framework solves more problems in benchmarks where each variable appears at most once in each equation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。