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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F23%3APU149380" target="_blank" >RIV/00216305:26230/23:PU149380 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1016/j.jss.2023.111673" target="_blank" >http://dx.doi.org/10.1016/j.jss.2023.111673</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.jss.2023.111673" target="_blank" >10.1016/j.jss.2023.111673</a>

Result language
angličtina
Original language name
A symbolic algorithm for the case-split rule in solving word constraints with extensions
Original language description
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.
Czech name
—
Czech description
—

Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2023
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)