RP2019.pdf (423.58 kB)
Download file

On solving word equations using SAT

Download (423.58 kB)
conference contribution
posted on 21.07.2021, 13:08 by Joel DayJoel Day, Thorsten Ehlers, Mitja Kulczynski, Florin Manea, Dirk Nowotka, Danny Bøgsted Poulsen
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.

Funding

DFG grant MA 5725/2-1

BMBF through the ARAMiS2 (01IS160253) project

History

School

  • Science

Department

  • Computer Science

Published in

Reachability Problems

Pages

93 - 106

Source

International Conference on Reachability Problems (RP 2019)

Publisher

Springer

Version

AM (Accepted Manuscript)

Rights holder

© Springer Nature Switzerland AG

Publisher statement

The final authenticated version is available online at https://doi.org/10.1007/978-3-030-30806-3_8.

Publication date

2019-09-06

Copyright date

2019

ISBN

9783030308056; 9783030308063

ISSN

0302-9743

eISSN

1611-3349

Book series

Lecture Notes in Computer Science; 11674

Language

en

Editor(s)

Emmanuel Filiot; Raphaël Jungers; Igor Potapov

Location

Brussels, Belgium

Event dates

11th September 2019 - 13th September 2019

Depositor

Dr Joel Day. Deposit date: 21 July 2021

Usage metrics

Read the paper on the publisher website

Categories

Exports