Název: Řešení problémů booleovské splnitelnosti
Překlad názvu: Solving Boolean satisfiability problems
Autoři: Balyo, Tomáš
Typ dokumentu: Rigorózní práce
Rok: 2013
Jazyk: eng
Abstrakt: [eng] [cze]
In this thesis we study the possibilities of decomposing Boolean formulae into connected components. or 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-the-art SAT solving algorithms and techniques. V této práci studujeme možnosti rozkladu booleovských formulí do komponent souvislosti. Z tohoto důvodu 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.
Klíčová slova: komponentový strom; rozhodovací heuristiky; Splnitelnost; component tree; decision heuristics; Satisfiability

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/59202

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


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Rigorózní práce