RP2019.pdf (423.58 kB)
Download fileOn solving word equations using SAT
conference contribution
posted on 2021-07-21, 13:08 authored by Joel DayJoel Day, Thorsten Ehlers, Mitja Kulczynski, Florin Manea, Dirk Nowotka, Danny Bøgsted PoulsenWe 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.
Funding
DFG grant MA 5725/2-1
BMBF through the ARAMiS2 (01IS160253) project
History
School
- Science
Department
- Computer Science
Published in
Reachability ProblemsPages
93 - 106Source
International Conference on Reachability Problems (RP 2019)Publisher
SpringerVersion
- AM (Accepted Manuscript)
Rights holder
© Springer Nature Switzerland AGPublisher statement
The final authenticated version is available online at https://doi.org/10.1007/978-3-030-30806-3_8.Publication date
2019-09-06Copyright date
2019ISBN
9783030308056; 9783030308063ISSN
0302-9743eISSN
1611-3349Publisher version
Book series
Lecture Notes in Computer Science; 11674Language
- en