Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)
This work addresses the problem of efficient word equation solving for automated reasoning and verification, presenting an incremental improvement by integrating GNNs into an existing transformation-based method.
The paper tackles the problem of solving word equations by proposing a Graph Neural Network-guided algorithm that iteratively rewrites terms and uses GNNs for split decisions, implemented as the solver DragonLi. It shows that DragonLi solves significantly more satisfiable single-word equation problems than established solvers and is competitive with state-of-the-art solvers for conjunctions of multiple equations.
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.