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

TL;DR

This paper introduces DragonLi, a GNN-guided algorithm for solving word equations that improves efficiency by making informed split decisions, especially excelling on satisfiable problems and outperforming existing solvers on single equations.

Contribution

The paper presents a novel GNN-based approach for guiding word equation solving, including new graph representations and an implementation that outperforms existing methods.

Findings

DragonLi solves more single equations than existing solvers.

The GNN-guided approach is effective on satisfiable problems.

DragonLi is competitive with state-of-the-art solvers on multiple equations.

Abstract

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.