Word equations in synergy with regular constraints (extended version)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0197939" target="_blank" >RIV/00216305:26230/26:0197939 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/article/10.1007/s10601-025-09379-w" target="_blank" >https://link.springer.com/article/10.1007/s10601-025-09379-w</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10601-025-09379-w" target="_blank" >10.1007/s10601-025-09379-w</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Word equations in synergy with regular constraints (extended version)

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Word equations in synergy with regular constraints (extended version)

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2025

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Constraints

ISSN

1383-7133

e-ISSN

1572-9354

Svazek periodika

30

Číslo periodika v rámci svazku

May

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

34

Strana od-do

1-34

Kód UT WoS článku

001492135600001

EID výsledku v databázi Scopus

2-s2.0-105005597927