On Solving Word Equations Using SAT

TL;DR

This paper introduces Woorpje, a SAT-based solver for bounded word equations that reformulates the problem as an automata reachability and SAT problem, enabling efficient solving and detection of solver faults.

Contribution

Woorpje is a novel string solver that encodes bounded word equations as SAT problems, allowing for linear constraints and improved reliability.

Findings

Woorpje achieves reliable and competitive results.

It detects cases where other solvers fail.

It effectively incorporates additional linear length constraints.

Abstract

We present Woorpje, a string solver for bounded word equations (i.e., equations where the length of each variable is upper bounded by a given integer). Our algorithm works by reformulating the satisfiability of bounded word equations as a reachability problem for nondeterministic finite automata, and then carefully encoding this as a propositional satisfiability problem, which we then solve using the well-known Glucose SAT-solver. This approach has the advantage of allowing for the natural inclusion of additional linear length constraints. Our solver obtains reliable and competitive results and, remarkably, discovered several cases where state-of-the-art solvers exhibit a faulty behaviour.