Publication Details

A symbolic algorithm for the case-split rule in solving word constraints with extensions

HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software, vol. 201, no. 201, 2023, pp. 111673-111693. ISSN 0164-1212. Available from: http://dx.doi.org/10.1016/j.jss.2023.111673
Czech title
Symbolický algoritmus pro případové pravidlo v řešení omezení nad slovy s rozšířeními
Type
journal article
Language
english
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Turrini Andrea (Chinese Academy of Sciences)
URL
Keywords

string constraints, satisfiability modulo theories, regular model checking, Nielsen transformation, finite automata, monadic second-order logic over strings

Abstract

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.

Published
2023
Pages
111673-111693
Journal
Journal of Systems and Software, vol. 201, no. 201, ISSN 0164-1212
Publisher
Elsevier Science
DOI
UT WoS
000965770000001
EID Scopus
BibTeX
@ARTICLE{FITPUB12977,
   author = "Vojt\v{e}ch Havlena and Yu-Fang Chen and Ond\v{r}ej Leng\'{a}l and Andrea Turrini",
   title = "A symbolic algorithm for the case-split rule in solving word constraints with extensions",
   pages = "111673--111693",
   journal = "Journal of Systems and Software",
   volume = 201,
   number = 201,
   year = 2023,
   ISSN = "0164-1212",
   doi = "10.1016/j.jss.2023.111673",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12977"
}
Back to top