Result 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, vol. 30, no. May, p. 1-34.
Type
journal article
Language
English
Authors
Blahoudek František, RNDr., Ph.D.
Chen Yu-Fang
Chocholatý David, Ing., DITS (FIT)
Havlena Vojtěch, Ing., Ph.D., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Síč Juraj, Mgr., DITS (FIT)
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.

Keywords

Word equations, regular constraints, string solving, finite automata

URL
Published
2025
Pages
1–34
Journal
Constraints, vol. 30, no. May, ISSN
Publisher
Springer Nature
DOI
10.1007/s10601-025-09379-w
UT WoS
001492135600001
EID Scopus
2-s2.0-105005597927
BibTeX 
@article{BUT197939,
  author="František {Blahoudek} and Yu-Fang {Chen} and David {Chocholatý} and Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Juraj {Síč}",
  title="Word equations in synergy with regular constraints (extended version)",
  journal="Constraints",
  year="2025",
  volume="30",
  number="May",
  pages="1--34",
  doi="10.1007/s10601-025-09379-w",
  issn="1383-7133",
  url="https://link.springer.com/article/10.1007/s10601-025-09379-w"
}
Files
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, completed
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, completed
Representing Boolean Functions by a Self-Adaptable Data Structure, GACR, Standardní projekty, GA23-07565S, start: 2023-01-01, end: 2025-12-31, completed
Departments
Department of Intelligent Systems (DITS)
Back to top