A Uniform Framework for Handling Position Constraints in String Solving

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0197690" target="_blank" >RIV/00216305:26230/26:0197690 - isvavai.cz</a>

Result on the web

<a href="https://dl.acm.org/doi/10.1145/3729273" target="_blank" >https://dl.acm.org/doi/10.1145/3729273</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3729273" target="_blank" >10.1145/3729273</a>

Result language

angličtina

Original language name

A Uniform Framework for Handling Position Constraints in String Solving

Original language description

We introduce a novel decision procedure for solving the class of position string constraints, which includes string disequalities, prefixof, suffixof, str.at, and str.at. These constraints are generated frequently in almost any application of string constraint solving. Our procedure avoids expensive encoding of the constraints to word equations and, instead, reduces the problem to checking conflicts on positions satisfying an integerconstraint obtained from the Parikh image of a polynomial-sized finite automaton with a special structure. By the reduction to counting, solving position constraints becomes NP-complete and for some cases even falls into PTime. This is much cheaper than the previously used techniques, which either used reductions generating word equations and length constraints (for which modern string solvers use exponential-space algorithms) or incomplete techniques. Our method is relevant especially for automata-based string solvers, which have recently achieved the best results in terms of practical efficiency, generality, and completeness guarantees. This work allows them to excel also on position constraints, which used to be their weakness. Besides the efficiency gains, we show that our framework may be extended to solve a large fragment of contains (in NExpTime), for which decidability has been long open, and gives a hope to solve the general problem. Our implementation of the technique within the Z3-Noodler solver significantly improves its performance on position constraints.

Czech name

—

Czech description

—

Type

J_imp - 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)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2025

Confidentiality

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

Name of the periodical

Proceedings of the ACM on Programming Languages-PACMPL

ISSN

—

e-ISSN

2475-1421

Volume of the periodical

9

Issue of the periodical within the volume

PLDI

Country of publishing house

US - UNITED STATES

Number of pages

26

Pages from-to

550-575

UT code for WoS article

001532151900022

EID of the result in the Scopus database

2-s2.0-105008277250