Název: Heuristiky ve string solvingu
Překlad názvu: Heuristics in String Solving
Autoři: Řezáč, Michal ; Havlena, Vojtěch (oponent) ; Síč, Juraj (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2024
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
Tato práce se zaměřuje na identifikaci heuristik a strategií použitých v moderních string solverech a na vyhodnocení jejich dopadu na efektivitu řešení. Zkoumány jsou především dva solvery – cvc5 a Z3. Práce popisuje techniky používané SMT solverech a strategie, které implementují string solvery. Vyhodnocení efektivity heuristik bylo prováděno jejich vypínáním přímo v kódu uvedených nástrojů a následným vyhodnocením dopadu na řešení standardních sad benchmarků. Výsledkem této práce je soupis sady konkrétních heuristik a popis struktury nástrojů cvc5 a Z3. Měřením se nepodařilo prokázat, jak velký skutečný dopad identifikované a popsané heuristiky mají. This work aims on identifying heuristics and strategies used in modern string solvers and evaluating their impact on the effectiveness of the solving. In particular, two solvers -- cvc5 and Z3 -- are examined. The thesis describes the techniques used by SMT solvers and the strategies implemented by string solvers. The evaluation of the effectiveness of the heuristics was performed by disabling them directly in the code of the tools mentioned and then evaluating the impact on solving the sets of standard benchmarks. The result of this work is summary of a set of specific heuristics and a description of the structure of the tools cvc5 and Z3. The measurements failed to demonstrate the actual impact of the heuristics identified and described.
Klíčová slova: cvc4; cvc5; heuristics; SMT; string constraints; string solving; z3; cvc4; cvc5; heuristiky; SMT; string solving; z3; řetězcová omezení

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: https://hdl.handle.net/11012/248989

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-620055


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce