Detail publikačního 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.

Originální název

Word equations in synergy with regular constraints (extended version)

Anglický název

Word equations in synergy with regular constraints (extended version)

Druh

Článek WoS

Originální 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.

Anglický 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

Klíčová slova v angličtině

Word equations, regular constraints, string solving, finite automata

Autoři

HAVLENA, V.; CHOCHOLATÝ, D.; LENGÁL, O.; HOLÍK, L.; SÍČ, J.; BLAHOUDEK, F.; CHEN, Y.

Rok RIV

2026

Vydáno

21.05.2025

Nakladatel

Springer Nature

Periodikum

Constraints

Svazek

30

Číslo

May

Stát

Nizozemsko

Strany od

1

Strany do

34

Strany počet

34

URL

https://link.springer.com/article/10.1007/s10601-025-09379-w

Plný text v Digitální knihovně

http://hdl.handle.net/11012/256369

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"
}