Original title:
Řešení řetězcových omezení pomocí Parikhových obrazů
Translated title:
String Constraint Solving Through Parikh Images
Authors:
Bartoš, Petr ; Havlena, Vojtěch (referee) ; Holík, Lukáš (advisor) Document type: Bachelor's theses
Year:
2024
Language:
eng Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[eng][cze]
Tato bakalářská práce si klade za cíl implementovat alternativní způsob řešení řetězcových omezení pomocí takzvaného flattening algoritmu, který pomocí Parikhových obrazů a parametrických plochých automatů transformuje řetězcová omezení na lineární vzorce. Takto vyjádřené omezení je možné řešit pomocí výkonných SMT solverů a předchází problémům spjatým s tradičně používanými metodami založených na automatech, jako je například exploze stavového prostoru. Práce popisuje teoretické znalosti potřebné k pochopení algoritmu pro řešení a představuje další state of the art způsoby řešení. Výsledky implementace jsou poté porovnány s ostatnímy solvery na klasických soutěžních benchmarcích. Provedené experimenty ukazují smíšené výsledky – ač navržené řešení nedosahuje podobné rychlosti jako state-of-the-art solvery, přesnost podaproximačního přístupu je relativně příznivá.
This bachelor thesis aims to implement an alternative way of solving string constraints using the so-called flattening algorithm. The algorithm makes use of Parikh images and parametric flat automata to effectively convert string constraints to linear arithmetic, which allows for leveraging powerful SMT solvers. Solving constraints as an algebraic problem is supposed to be more efficient than standardly used automata-based techniques, as it avoids common pitfalls, such as state-space exposion. The thesis covers the theoretical knowledge required to understand the flattening algorithm and introduces alternative modern solution strategies. The implementation results are then compared to other solvers using conventional competition benchmarks. The conducted experiments show that while the speed of the implementation compared to other state-of-the-art solvers is worse, the effectiveness of the underapproximation itself is fairly promising, thus yielding mixed results.
Keywords:
lineární vzorce; parametrický automat; Parikhův obraz; plochý automat; SMT výpočty; řetězce; řetězcová omezení; řešení řetězcových omezení; flat automaton; linear formulae; parametric automaton; Parikh image; SMT solving; string constraints; string solving; strings
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: https://hdl.handle.net/11012/246956