Publication Details

A Uniform Framework for Handling Position Constraints in String Solving

CHEN Yu-Fang, HAVLENA Vojtěch, HEČKO Michal, HOLÍK Lukáš and LENGÁL Ondřej. A Uniform Framework for Handling Position Constraints in String Solving. Proceedings of the ACM on Programming Languages, vol. 9, no. 169, 2025, pp. 550-575. ISSN 2475-1421.
Czech title
Uniformní rámec pro řešení pozičních omezení nad řetězci
Type
journal article
Language
english
Authors
Chen Yu-Fang (ASIN)
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Hečko Michal, Ing. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Keywords

string constraints,SMT,automata,position constraints,disequalities,not contains,regular languages

Abstract

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.

Published
2025
Pages
550-575
Journal
Proceedings of the ACM on Programming Languages, vol. 9, no. 169, ISSN 2475-1421
Book
Proceedings of PLDI'25
Publisher
Association for Computing Machinery
DOI
BibTeX
@ARTICLE{FITPUB13500,
   author = "Yu-Fang Chen and Vojt\v{e}ch Havlena and Michal He\v{c}ko and Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l",
   title = "A Uniform Framework for Handling Position Constraints in String Solving",
   pages = "550--575",
   booktitle = "Proceedings of PLDI'25",
   journal = "Proceedings of the ACM on Programming Languages",
   volume = 9,
   number = 169,
   year = 2025,
   ISSN = "2475-1421",
   doi = "10.1145/3729273",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13500"
}
Back to top