Publication Details
A symbolic algorithm for the case-split rule in solving word constraints with extensions
string constraints, satisfiability modulo theories, regular model
checking, Nielsen transformation, finite automata, monadic second-order logic
over strings
Case split is a core proof rule in current decision procedures for the theory of
string constraints. Its use is the primary cause of the state space explosion
in string constraint solving, since it is the only rule that creates branches in
the proof tree. Moreover, explicit handling of the case split rule may cause
recomputation of the same tasks in multiple branches of the proof tree. In
this paper, we propose a symbolic algorithm that significantly reduces such
a redundancy. In particular, we encode a string constraint as a regular language
and proof rules as rational transducers. This allows us to perform similar steps in
the proof tree only once, alleviating the state space explosion. We also extend
the encoding to handle arbitrary Boolean combinations of string constraints,
length constraints, and regular constraints. In our experimental results, we
validate that our technique works in many practical cases where other state-of-the-art solvers fail to provide an answer; our Python prototype implementation
solved over 50% of string constraints that could not be solved by the other tools.
@article{BUT185153,
author="HAVLENA, V. and LENGÁL, O. and CHEN, Y. and TURRINI, A.",
title="A symbolic algorithm for the case-split rule in solving word constraints with extensions",
journal="JOURNAL OF SYSTEMS AND SOFTWARE",
year="2023",
volume="201",
number="201",
pages="111673--111693",
doi="10.1016/j.jss.2023.111673",
issn="0164-1212",
url="http://dx.doi.org/10.1016/j.jss.2023.111673"
}