Publication Details

Word equations in synergy with regular constraints (extended version)

HAVLENA, V.; CHOCHOLATÝ, D.; LENGÁL, O.; HOLÍK, L.; SÍČ, J.; BLAHOUDEK, F.; CHEN, Y. Word equations in synergy with regular constraints (extended version). Constraints, 2025. ISSN: 1572-9354.
Czech title
Rovnice nad slovy v součinnosti s regulárními omezeními (rozšírena verze)
Type
journal article
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS)
Chocholatý David, Ing. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Síč Juraj, Mgr. (DITS)
Blahoudek František, RNDr., Ph.D.
Chen Yu-Fang
Keywords

Word equations, regular constraints, string solving, finite automata

Abstract

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.

Published
2025 (in print)
Pages
34
Journal
Constraints, ISSN 1572-9354
DOI
10.1007/s10601-025-09379-w
BibTeX 
@article{BUT197939,
  author="Vojtěch {Havlena} and David {Chocholatý} and Ondřej {Lengál} and Lukáš {Holík} and Juraj {Síč} and František {Blahoudek} and Yu-Fang {Chen}",
  title="Word equations in synergy with regular constraints (extended version)",
  journal="Constraints",
  year="2025",
  pages="34",
  doi="10.1007/s10601-025-09379-w",
  issn="1572-9354"
}
Back to top