Publication Details
Word equations in synergy with regular constraints (extended version)
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Chocholatý David, Ing. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
Word equations, regular constraints, string solving, finite automata
We propose a new automata-based algorithm for solving string constraints that tightly integrates reasoning about equations and regular constraints. Exchanging information between the two allows an efficient pruning of generated combinatorial cases. The algorithm is based on a novel language-based characterization of satisfiability of word equations with regular constraints. Namely, satisfiability of an equation is implied by its stability: the concatenation of the regular languages constraining variables on the left-hand side equals the concatenation of the languages on the right-hand side. It is complete for the chain-free string constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior on difficult examples.
@ARTICLE{FITPUB13513,
author = "Franti\v{s}ek Blahoudek and Vojt\v{e}ch Havlena and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and David Chocholat\'{y} and Ond\v{r}ej Leng\'{a}l and Juraj S\'{i}\v{c}",
title = "Word equations in synergy with regular constraints (extended version)",
pages = 34,
journal = "Constraints",
year = 2025,
ISSN = "1572-9354",
doi = "10.1007/s10601-025-09379-w",
language = "english",
url = "https://www.fit.vut.cz/research/publication/13513"
}