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.

翻译：本文提出一种基于图神经网络引导的词语方程求解算法，其核心建立在经典的尼尔森变换分割方程方法之上。该算法通过迭代重写方程两侧的首项，构建出树状搜索空间。在树的每个分割点处选择不同路径会显著影响求解时间，这促使我们采用图神经网络（GNN）来实现高效的分割决策。我们将分割决策编码为多分类任务，并针对词语方程的结构信息提出了五种图表示方法以供GNN处理。该算法被实现为名为DragonLi的求解器。我们在人工构造和真实场景的基准测试上进行了实验验证。该算法在可满足性问题上的表现尤为突出。对于单词语方程，DragonLi能够求解的问题数量显著超过成熟的字符串求解器。对于多词语方程的合取问题，DragonLi与当前最先进的字符串求解器相比具有竞争力。