用图神经网络指导单词方程求解，提升求解效率。
Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)
- 将分裂决策建模为多分类任务，用图神经网络选择最优路径。
- 在可满足问题上表现优异，单个单词方程求解率显著更高。
- 适合需要高效求解单词方程的自动化验证与形式化方法研究者。
本文提出一种基于图神经网络（GNN）的单词方程求解算法，利用经典的尼尔森变换进行方程拆分。算法通过迭代重写等式两侧首项，生成树状搜索空间，而每个分裂点的选择对求解时间影响显著，因此引入GNN进行高效决策。分裂决策被建模为多分类任务，并设计了五种单词方程的图表示以编码其结构信息。该算法实现为名为DragonLi的求解器。在人工和真实世界基准上进行实验，结果表明，在可满足问题上表现突出：对于单个单词方程，DragonLi比现有主流字符串求解器解决更多问题；对于多个单词方程的合取，性能与最先进求解器相当。
原文摘要 · Abstract (English)
This paper proposes a Graph Neural Network-guided algorithm for solving word equations, based on the well-known Nielsen transformation for splitting equations. The algorithm iteratively rewrites the first terms of each side of an equation, giving rise to a tree-like search space. The choice of path at each split point of the tree significantly impacts solving time, motivating the use of Graph Neural Networks (GNNs) for efficient split decision-making. Split decisions are encoded as multi-classification tasks, and five graph representations of word equations are introduced to encode their structural information for GNNs. The algorithm is implemented as a solver named DragonLi. Experiments are conducted on artificial and real-world benchmarks. The algorithm performs particularly well on satisfiable problems. For single word \mbox{equations}, DragonLi can solve significantly more problems than well-established string solvers. For the conjunction of multiple word equations, DragonLi is competitive with state-of-the-art string solvers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。