Word Equations in Synergy with Regular Constraints

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F23%3APU149383" target="_blank" >RIV/00216305:26230/23:PU149383 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-031-27481-7_23" target="_blank" >http://dx.doi.org/10.1007/978-3-031-27481-7_23</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-27481-7_23" target="_blank" >10.1007/978-3-031-27481-7_23</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Word Equations in Synergy with Regular Constraints

Popis výsledku v původním jazyce

We argue that in string solving, word equations and regular constraints are better mixed together than approached separately as in most current string solvers. We propose a fast algorithm, complete for the fragment of chain-free constraints, in which word equations and regular constraints are tightly integrated and exchange information, efficiently pruning the cases generated by each other and limiting possible combinatorial explosion. The algorithm is based on a novel language-based characterisation of satisfiability of word equations with regular constraints. We experimentally show that  our prototype implementation is competitive with the best string solvers and even superior in that it is the fastest on difficult examples and has the least number of timeouts.

Název v anglickém jazyce

Word Equations in Synergy with Regular Constraints

Popis výsledku anglicky

We argue that in string solving, word equations and regular constraints are better mixed together than approached separately as in most current string solvers. We propose a fast algorithm, complete for the fragment of chain-free constraints, in which word equations and regular constraints are tightly integrated and exchange information, efficiently pruning the cases generated by each other and limiting possible combinatorial explosion. The algorithm is based on a novel language-based characterisation of satisfiability of word equations with regular constraints. We experimentally show that  our prototype implementation is competitive with the best string solvers and even superior in that it is the fastest on difficult examples and has the least number of timeouts.

Druh

D - Stať ve sborníku

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)

Rok uplatnění

2023

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 statě ve sborníku

Proceedings of FM'23

ISBN

—

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

21

Strana od-do

403-423

Název nakladatele

Springer Verlag

Místo vydání

Lübeck

Místo konání akce

Lübeck

Datum konání akce

6. 3. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000999132100023