pith. sign in

arxiv: 1906.11718 · v1 · pith:UB4LIIPCnew · submitted 2019-06-27 · 💻 cs.FL

On Solving Word Equations Using SAT

Joel D. Day , Thorsten Ehlers , Mitja Kulczynski , Florin Manea , Dirk Nowotka , Danny B{\o}gsted Poulsen This is my paper

Pith reviewed 2026-05-25 13:46 UTC · model grok-4.3

classification 💻 cs.FL
keywords word equationsSAT solverstring solverNFA reachabilitybounded satisfiabilitylength constraints
0
0 comments X

The pith

Reducing bounded word equations to SAT via NFA reachability yields a competitive solver that exposes errors in other tools.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a solver called Woorpje for bounded word equations, where each variable has an explicit upper bound on its length. It reformulates the satisfiability question as a reachability problem over a nondeterministic finite automaton and then encodes that problem as a propositional SAT instance solved by Glucose. The encoding naturally accommodates additional linear length constraints on the variables. Testing shows the approach produces reliable results on benchmarks while also revealing incorrect answers from several existing state-of-the-art solvers.

Core claim

The satisfiability of bounded word equations can be decided by first building an NFA whose paths correspond to solutions and then reducing reachability in that automaton to a SAT instance; the same encoding admits linear length constraints and, when run on standard test suites, identifies cases in which leading solvers return wrong answers.

What carries the argument

The reduction from bounded word equation satisfiability to NFA reachability followed by a direct propositional encoding solved with a SAT solver.

If this is right

  • Linear length constraints on variables can be incorporated directly into the SAT encoding without separate handling.
  • The resulting solver returns reliable answers on existing benchmark suites for bounded word equations.
  • Execution of the solver on standard instances can surface faulty outputs produced by other string solvers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same reduction technique might serve as a verification oracle to cross-check results from other string solvers on bounded instances.
  • Because the encoding is modular, it could be combined with other decision procedures when length bounds are relaxed or removed.
  • The discovery of bugs in competing tools suggests that NFA-to-SAT reductions could be used systematically for regression testing of string solvers.

Load-bearing premise

The transformation from a bounded word equation into an NFA reachability question and then into a SAT formula is both sound and complete.

What would settle it

A concrete bounded word equation together with explicit length bounds for which the SAT encoding reports satisfiable yet no string assignment of those lengths satisfies the original equation, or reports unsatisfiable when such an assignment exists.

Figures

Figures reproduced from arXiv: 1906.11718 by Danny B{\o}gsted Poulsen, Dirk Nowotka, Florin Manea, Joel D. Day, Mitja Kulczynski, Thorsten Ehlers.

Figure 1
Figure 1. Figure 1: Automaton for the word equation aZXb ˙=aXaY , with the states grouped according to their locations. Only reachable states are shown. for w ∈ { uξ, vξ } and each position i of w and letter a ∈ Σλ we introduce a variable which is true if and only if w[i] will correspond to an a in the solution of the word equation. More precisely, we make a distinction between constant letters and variable positions and defi… view at source ↗
Figure 2
Figure 2. Figure 2: Solver computation on XaXbY bZ ˙= aXY - Y bZZbaa is true iff the given word equation is satisfiable w.r.t. the given length bounds. Lemma 1. Let u ˙=v be a word equation, B be the function giving the bounds for the word equation variable, and ϕ the corresponding formula consist￾ing of the conjunction (1) - (10) and the earlier defined constraints in this section, then ϕ ∧ S0,0 ∧ S|uξ|,|vξ| has a satisfying… view at source ↗
Figure 3
Figure 3. Figure 3: The MDD for aX1aX2 ˙= aX3X1b and adding it to the previous partial sum s. Whenever there is only one successor to a node (Ii , j) within our MDD, we directly force its corresponding one hot encoding to be true by adding Mi−1,j → OHi(j). This reduces the amount of guesses on variables. Example 3. Consider the equation u ˙= v for u = aX1aX2, v = aX3X1b ∈ Ξ∗ , where Σ = { a, b } and Γ = { X1, X2, X3 }. The co… view at source ↗
Figure 4
Figure 4. Figure 4: Architecture of Woorpje equations are immediately reported. After the preprocessing step, Woorpje it￾eratively encodes the word equation into a propositional logic formula and solves it with Glucose [3] for increasing maximal variable lengths (i 2 , where i is the current iteration). If a solution is found, it is reported. The maximal value of i is user definable, and by default set to 2n where n is the le… view at source ↗
Figure 5
Figure 5. Figure 5: Cactus plots for all Tracks [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 1 minor

Summary. The paper presents Woorpje, a solver for bounded word equations that reformulates satisfiability as an NFA reachability problem, encodes the reachability query (including linear length constraints) as a SAT instance, and solves it with Glucose. It claims the method yields reliable, competitive performance and has identified faulty behavior in other state-of-the-art string solvers.

Significance. If the core reduction is shown to be sound and complete, the work supplies a practical, extensible SAT-based decision procedure for bounded string constraints that naturally incorporates length bounds; this could serve as a reliable baseline or oracle in verification tool-chains. The reported discovery of bugs in competing solvers would then constitute a useful empirical contribution, provided the experimental evidence is fully documented.

major comments (3)
  1. [algorithm description (Sections 3–4)] The manuscript describes the reduction from bounded word equations to NFA reachability and then to a SAT encoding, yet supplies no explicit formal argument (lemma, theorem, or proof sketch) establishing that the encoding is sound and complete—i.e., that every satisfying assignment to the generated SAT formula corresponds to a solution of the original bounded equation and vice versa. This absence is load-bearing for the central claims of reliability and bug discovery.
  2. [encoding of length constraints] The additional linear length constraints are stated to be included “naturally,” but the precise translation of these constraints into propositional clauses is not accompanied by a separate correctness argument; without it, the claim that the encoding preserves the bounded-length semantics cannot be verified from the text.
  3. [experimental evaluation] The experimental claims that Woorpje discovered faulty behavior in other solvers presuppose that Woorpje itself is correct on the reported instances; because no soundness argument is provided, these findings rest on an unverified assumption and require either a proof or an independent validation procedure.
minor comments (1)
  1. [abstract] The abstract and introduction would benefit from an explicit statement of the precise bound on variable lengths that the solver handles and any restrictions on the alphabet or equation form.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive comments. We address each major point below and will revise the manuscript to strengthen the formal foundations of the encoding.

read point-by-point responses

  1. Referee: [algorithm description (Sections 3–4)] The manuscript describes the reduction from bounded word equations to NFA reachability and then to a SAT encoding, yet supplies no explicit formal argument (lemma, theorem, or proof sketch) establishing that the encoding is sound and complete—i.e., that every satisfying assignment to the generated SAT formula corresponds to a solution of the original bounded equation and vice versa. This absence is load-bearing for the central claims of reliability and bug discovery.

    Authors: We agree that an explicit formal argument is needed to support the central claims. In the revised manuscript we will insert a lemma (in Section 3 or 4) together with a short proof sketch establishing the soundness and completeness of the two-stage reduction: every solution of a bounded word equation corresponds to an accepting path in the constructed NFA, and every satisfying assignment to the generated SAT formula corresponds to such a path (and vice versa). revision: yes

  2. Referee: [encoding of length constraints] The additional linear length constraints are stated to be included “naturally,” but the precise translation of these constraints into propositional clauses is not accompanied by a separate correctness argument; without it, the claim that the encoding preserves the bounded-length semantics cannot be verified from the text.

    Authors: We will add an explicit subsection describing the clause-level encoding of the linear length constraints and supply a short correctness argument showing that any satisfying assignment respects the original length bounds. revision: yes

  3. Referee: [experimental evaluation] The experimental claims that Woorpje discovered faulty behavior in other solvers presuppose that Woorpje itself is correct on the reported instances; because no soundness argument is provided, these findings rest on an unverified assumption and require either a proof or an independent validation procedure.

    Authors: The addition of the soundness and completeness arguments described above will place the bug-discovery claims on a firmer footing. We will also state in the revised experimental section that the implementation and benchmark instances are publicly available for independent validation. revision: partial

Circularity Check

0 steps flagged

No circularity; reduction to independent external SAT solver

full rationale

The paper describes a reduction of bounded word equations to NFA reachability followed by an encoding into SAT clauses solved by the external Glucose solver. No derivation step is shown to be self-definitional, a fitted input renamed as prediction, or dependent on a load-bearing self-citation chain. The central claim of discovering faults in other solvers rests on the soundness of the presented reduction, but the absence of an explicit proof is a verification gap rather than circularity. The method is self-contained against external benchmarks (the SAT solver and the reported instances), yielding a normal non-finding of circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard automata theory and the correctness of the Glucose SAT solver; no free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (2)
  • domain assumption Nondeterministic finite automata correctly model concatenation and length-bounded string assignments for word equations.
    Invoked by the reformulation step described in the abstract.
  • standard math The Glucose SAT solver returns correct answers for the generated propositional formulas.
    Relied upon for the final decision procedure.

pith-pipeline@v0.9.0 · 5647 in / 1308 out tokens · 20204 ms · 2026-05-25T13:46:02.947216+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    In: Kroe ning, D., P˘ as˘ areanu, C.S

    Abdulla, P.A., Atig, M.F., Chen, Y.F., Hol ´ ık, L., Rezine, A., R¨ ummer, P ., Stenman, J.: Norn: An SMT solver for string constraints. In: Kroe ning, D., P˘ as˘ areanu, C.S. (eds.) Computer Aided Verification. pp. 462–469. Springer International Publishing, Cham (2015)

    work page 2015

  2. [2]

    In: Interna- tional Conference on Principles and Practice of Constraint Progra mming

    Ab ´ ıo, I., Stuckey, P.J.: Encoding linear constraints into SAT. In: Interna- tional Conference on Principles and Practice of Constraint Progra mming. pp. 75–91. Springer (2014)

    work page 2014

  3. [3]

    Internationa l Journal on Artificial Intelligence Tools 27(01), 1840001 (2018)

    Audemard, G., Simon, L.: On the glucose SAT solver. Internationa l Journal on Artificial Intelligence Tools 27(01), 1840001 (2018)

    work page 2018

  4. [4]

    In: International Conference on Com puter Aided Verification

    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi´c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: International Conference on Com puter Aided Verification. pp. 171–177. Springer (2011)

    work page 2011

  5. [5]

    In: 2017 Formal Methods in Computer Aided Desig n (FMCAD)

    Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A string solver with th eory- aware heuristics. In: 2017 Formal Methods in Computer Aided Desig n (FMCAD). pp. 55–59 (Oct 2017)

    work page 2017

  6. [6]

    In: International Conference on Tools an d Algo- rithms for the Construction and Analysis of Systems

    Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string- manipulating programs. In: International Conference on Tools an d Algo- rithms for the Construction and Analysis of Systems. pp. 307–321 . Springer (2009)

    work page 2009

  7. [7]

    In: Draves, R., van Renesse, R

    Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automa tic generation of high-coverage tests for complex systems program s. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Syst ems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. pp. 209–224. USENIX Association (2 008), ...

    work page 2008

  8. [8]

    Proceedings of the ACM on Programming Languages 3(POPL) , 49 (2019)

    Chen, T., Hague, M., Lin, A.W., R¨ ummer, P., Wu, Z.: Decision procedu res for path feasibility of string-manipulating programs with complex ope ra- tions. Proceedings of the ACM on Programming Languages 3(POPL) , 49 (2019)

    work page 2019

  9. [9]

    In: C hockler, H., Weissenbacher, G

    Cordeiro, L.C., Kesseli, P., Kroening, D., Schrammel, P., Trt ´ ık, M.: J BMC: A bounded model checking tool for verifying java bytecode. In: C hockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th Int erna- tional Conference, CA V 2018, Held as Part of the Federated Logic Confer- ence, FloC 2018, Oxford, UK, July 14-17, 2018, Proceeding...

    work page doi:10.1007/978-3-319-96145-3_10 2018

  10. [10]

    In: Proc

    Day, J.D., Manea, F., Nowotka, D.: The hardness of solving simple w ord equations. In: Proc. MFCS 2017. LIPIcs, vol. 83, pp. 18:1–18:14 ( 2017)

    work page 2017

  11. [11]

    Proceeding s of the ACM on Programming Languages 2(POPL), 4 (2017)

    Hol ´ ık, L., Jank, P., Lin, A.W., R¨ ummer, P., Vojnar, T.: String con straints with concatenation and transducers solved efficiently. Proceeding s of the ACM on Programming Languages 2(POPL), 4 (2017)

    work page 2017

  12. [12]

    In: 30th International Symposium on Theoretical Aspects of Com puter Sci- ence, STACS 2013, February 27 - March 2, 2013, Kiel, Germany

    Je˙ z, A.: Recompression: a simple and powerful technique for w ord equations. In: 30th International Symposium on Theoretical Aspects of Com puter Sci- ence, STACS 2013, February 27 - March 2, 2013, Kiel, Germany. pp. 233–244 (2013), https://doi.org/10.4230/LIPIcs.STACS.2013.233

    work page doi:10.4230/lipics.stacs.2013.233 2013

  13. [13]

    In: Pr oc

    Je˙ z, A.: Word equations in nondeterministic linear space. In: Pr oc. ICALP

    work page

  14. [14]

    LIPIcs, vol. 80, pp. 95:1–95:13. Schloss Dagstuhl - Leibniz- Zentrum fuer Informatik (2017)

    work page 2017

  15. [15]

    Journal of the ACM (JACM) 47(3) , 483– 505 (2000)

    Karhum¨ aki, J., Mignosi, F., Plandowski, W.: The expressibility of languages and relations by word equations. Journal of the ACM (JACM) 47(3) , 483– 505 (2000)

    work page 2000

  16. [16]

    In: Proceedings of the eighteenth international symposium on Software testing and analysis

    Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: Hamp i: a solver for string constraints. In: Proceedings of the eighteenth international symposium on Software testing and analysis. pp. 105–116. ACM (20 09)

    work page

  17. [17]

    Sbornik: Mathematics 32(2), 129–198 (1977)

    Makanin, G.S.: The problem of solvability of equations in a free semig roup. Sbornik: Mathematics 32(2), 129–198 (1977)

    work page 1977

  18. [18]

    In: Proc

    Plandowski, W., Rytter, W.: Application of Lempel-Ziv encodings to the solution of words equations. In: Proc. 25th International Colloqu ium on Automata, Languages and Programming, ICALP’98. Lecture Note s in Com- puter Science, vol. 1443, pp. 731–742. Springer (1998)

    work page 1998

  19. [19]

    In: Foundations of Computer Science, 1999

    Plandowski, W.: Satisfiability of word equations with constants is in pspace. In: Foundations of Computer Science, 1999. 40th Annual Sympos ium on. pp. 495–500. IEEE (1999)

    work page 1999

  20. [20]

    In: 2010 IEEE Symp osium on Security and Privacy

    Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript. In: 2010 IEEE Symp osium on Security and Privacy. pp. 513–528. IEEE (2010)

    work page 2010

  21. [21]

    In: Chaudhuri, S., Farzan, A

    Trinh, M.T., Chu, D.H., Jaffar, J.: Progressive reasoning over rec ursively- defined strings. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aid ed Veri- fication. pp. 218–240. Springer International Publishing, Cham (2 016) A Artifacts for this paper You can download our artifacts at http://informatik.uni-kiel.de/ ~mku/woorpje/rp19.tar.gz. This package contains:

    work page

  22. [22]

    A README.txt including a guide to use our artifacts

    work page

  23. [23]

    Download script for all used tools

    work page

  24. [24]

    Woorpje source code B Preprocessing algorithms B.1 Prefix reducer For a word w ∈ Ξ ∗ we define the prefix of length i ∈ [|w|] by w[i :] = w[1] . . . w[i]. This algorithm is used analogously for suffices. 1 Input : u ˙ =v # input word equation Output : u′ ˙ =v′ # reduced word equation 2 commonPref ix I nd e x = 0 3 for i ∈ min { | v|, |u| } 4 if v[i] ̸= u[i] 5 ...

    work page 2089