Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer

TL;DR

A Graph Neural Network-guided algorithm for solving word equations, based on the well-known Nielsen transformation for splitting equations, which iteratively rewrites the first terms of each side of an equation, giving rise to a tree-like search space.

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.

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

TL;DR

A Graph Neural Network-guided algorithm for solving word equations, based on the well-known Nielsen transformation for splitting equations, which iteratively rewrites the first terms of each side of an equation, giving rise to a tree-like search space.

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.

Paper Structure

This paper contains 26 sections, 2 theorems, 8 equations, 8 figures, 3 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Word Equations.
  4. Graph Neural Networks.
  5. Search Procedure and Split Algorithm
  6. Split Rules
  7. Proof Trees
  8. GNN-Guided Split Algorithm
  9. Guiding the Split Algorithm
  10. Representing Word Equations by Graphs
  11. Training of Graph Neural Networks
  12. Forward Propagation.
  13. Propagation on Graphs.
  14. Backward Propagation.
  15. Training Data Collection
  16. ...and 11 more sections

Key Result

lemma 1

The proof rules in Figure fig:split_rules are sound and locally complete.

Figures (8)

  • Figure 1: The workflow diagram for the training and prediction stage
  • Figure 2: Simplification rules
  • Figure 3: Letter-letter rules
  • Figure 4: Variable-letter rules
  • Figure 5: Variable-variable rules
  • ...and 3 more figures

Theorems & Definitions (4)

  • definition 1: Satisfiability of word equations
  • lemma 1
  • lemma 2: Soundness of Algorithm \ref{['algorithm:SolveEqs']}
  • proof