# Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)

arXiv: https://arxiv.org/abs/2411.15194 · HTML: https://mlsanity.com/paper/2411.15194/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 49 references that are in the map.
- First posted on arXiv 19 Nov 2024.

## Builds on (most cited first, 13 of 13)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Relational inductive biases, deep learning, and graph networks](https://mlsanity.com/paper/1806.01261/) (2018)
- [Graph Neural Networks for Social Recommendation](https://mlsanity.com/paper/1902.07243/) (2019)
- [Learning to Represent Programs with Graphs](https://mlsanity.com/paper/1711.00740/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?](https://mlsanity.com/paper/1909.11830/) (2019)
- [Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations](https://mlsanity.com/paper/1811.03167/) (2018)
- [Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)](https://mlsanity.com/paper/2206.06986/) (2022)

## Built on by (most cited first, 1 of 1)

- [When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)](https://mlsanity.com/paper/2506.23784/) (2025)

## Abstract (arXiv)

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 mboxequations, 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.