Original title: Heuristiky ve string solvingu
Translated title: Heuristics in String Solving
Authors: Řezáč, Michal ; Havlena, Vojtěch (referee) ; Síč, Juraj (advisor)
Document type: Master’s theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [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.
Keywords: cvc4; cvc5; heuristiky; SMT; string solving; z3; řetězcová omezení; cvc4; cvc5; heuristics; SMT; string constraints; string solving; z3

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/248989

Permalink: http://www.nusl.cz/ntk/nusl-620055


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses