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.
@article{arxiv.1906.11718,
title = {On Solving Word Equations Using SAT},
author = {Joel D. Day and Thorsten Ehlers and Mitja Kulczynski and Florin Manea and Dirk Nowotka and Danny Bøgsted Poulsen},
journal= {arXiv preprint arXiv:1906.11718},
year = {2019}
}