摘要
本文提出了一种基于著名的 Nielsen 变换分解方程的图神经网络引导算法来求解单词方程。该算法迭代地重写方程每一侧的第一个项,从而产生一个树状搜索空间。在树的每个分裂点处路径的选择会显著影响求解时间,这促使我们使用图神经网络 (GNN) 来进行高效的分裂决策。分裂决策被编码为多分类任务,并且引入了五种单词方程的图表示来为 GNN 编码其结构信息。该算法被实现为名为 DragonLi 的求解器。实验在人工和真实世界的基准上进行。该算法在可满足性问题上表现尤其出色。对于单个单词方程,DragonLi 可以求解比已建立的字符串求解器多得多的问题。对于多个单词方程的合取,DragonLi 与最先进的字符串求解器具有竞争力。