# When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 43 references that are in the map.
- First posted on arXiv 30 Jun 2025.

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

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Graph Attention Networks](https://mlsanity.com/paper/1710.10903/) (2017)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [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)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [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)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations](https://mlsanity.com/paper/1811.03167/) (2018)
- [Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)](https://mlsanity.com/paper/2411.15194/) (2024)

## Abstract (arXiv)

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.