# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1906.11718