Original title: Hledání minimálních splňujících ohodnocení Booleovských formulí
Translated title: Finding Minimum Satisfying Assignments of Boolean Formulas
Authors: Švancara, Jiří ; Balyo, Tomáš (advisor) ; Trunda, Otakar (referee)
Document type: Bachelor's theses
Year: 2014
Language: cze
Abstract: [cze] [eng]
V této práci zkoumáme algoritmy a techniky pro řešení Booleovské splnitelnosti. Dále se zabýváme možnostmi jejich použití při řešení weighted short SAT, což je zobecnění problému splnitelnosti. Toto zobecnění požaduje nalézt splňující ohodnocení za použití minimálního součtu vah proměnných. K řešení tohoto problému zavádíme tři pravdivostní ohodnocení proměnných - True, False a Unassign. Ukážeme, že ne všechny algoritmy a techniky používané v moderních SAT solverech můžeme aplikovat v našem programu. Ty, které můžeme, převedeme tak, aby používali námi nadefinované pravdivostní ohodnocení. Různou kombinací takto převedených technik dostaneme několik verzí solveru, které mezi sebou na závěr porovnáme. Powered by TCPDF (www.tcpdf.org) In this thesis we examine algorithms and techniques used for solving Boolean satisfiability (SAT). Then we inspect the possibility to use them in solving the weighted short SAT problem, which is a generalization of the satisfiability problem. Given that each variable has a weight, this generalization is the problem of finding a satisfying truth assignment while using the smallest sum of weights. To solve this problem, we introduce three truth assignments of variables - True, False and Unassign. We show that not all algorithms and techniques used in modern SAT solvers can be used in our program. Those that can be converted, will be implemented using our three truth assignments. This will yield several versions of our new solver, which will be compared. Powered by TCPDF (www.tcpdf.org)
Keywords: DPLL algorithm; resolution; SAT; weighted short SAT; DPLL algoritmus; rezoluce; SAT; weighted short SAT

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

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


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Bachelor's theses