Detail výsledku

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, iss. May, p. 1-34.
Typ
článek v časopise
Jazyk
angličtina
Autoři
Blahoudek František, RNDr., Ph.D.
Chen Yu-Fang
Chocholatý David, Ing., UITS (FIT)
Havlena Vojtěch, Ing., Ph.D., UITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Síč Juraj, Mgr., UITS (FIT)
Abstrakt

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.

Klíčová slova

Word equations, regular constraints, string solving, finite automata

URL
Rok
2025
Strany
1–34
Časopis
Constraints, roč. 30, č. May, ISSN
Vydavatel
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"
}
Soubory
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, ukončen
Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury, GAČR, Standardní projekty, GA23-07565S, zahájení: 2023-01-01, ukončení: 2025-12-31, ukončen
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru