Original title:
Řešení problémů booleovské splnitelnosti
Translated title:
Solving Boolean satisfiability problems
Authors:
Balyo, Tomáš ; Surynek, Pavel (advisor) ; Barták, Roman (referee) Document type: Master’s theses
Year:
2010
Language:
slo Abstract:
[eng][cze] In this thesis we study the possibilities of decomposing Boolean formulae into connected components. For this reason, we introduce a new concept - component trees. We describe some of their properties and suggest some applications. We designed a class of decision heuristics for SAT solvers based on component trees and experimentally examined their performance on benchmark problems. For this purpose we implemented our own solver, which uses the state-of-theart SAT solving algorithms and techniques.V této práci studujeme možnosti rozkladu booleovských formulí do komponent souvislosti. Z tohoto důodu zavádíme nový pojem - komponentový strom. Popisujeme některé vlastnosti komponentových stromů a možnosti jejich aplikace. Navrhli jsme třídu rozhodovacích heuristik pro SAT řešič na základě komponentových stromů a experimentálně zkoumali jejich výkon na testovacích SAT problémech. Pro tento účel jsme implementovali vlastní řešič, který využívá nejmodernější algoritmy a techniky pro řešení booleovské splnitelnosti.
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/31123