Quantified Boolean formulas (QBFs) play an important role in theoretical computer science. QBF extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated.
In this dissertation we present our ZQSAT, which is an algorithm for evaluating quantified Boolean formulas. ZQSAT is based on ZBDD: Zero-Suppressed Binary Decision Diagram / which is a variant of BDD, and an adopted version of the DPLL algorithm. It has been implemented in C using the CUDD: Colorado University Decision Diagram package.
<br><br>
The capability of ZBDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and let us to embed the notion of memoization to the DPLL algorithm. These points led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with a little overheads. ZQSAT can solve some sets of standard QBF benchmark problems (known to be hard for DPLL based algorithms) faster than the best existing solvers. In addition to prenex-CNF, ZQSAT accepts prenex-NNF formulas. We show and prove how this capability can be exponentially beneficial.
<br><br> / In der Dissertation stellen wir einen neuen Algorithmus vor, welcher Formeln
der quantifizierten Aussagenlogik (engl. Quantified Boolean formula, kurz QBF)
löst. QBFs sind eine Erweiterung der klassischen Aussagenlogik um die Quantifizierung über aussagenlogische Variablen. Die quantifizierte Aussagenlogik ist dabei eine konservative Erweiterung der Aussagenlogik, d.h. es können nicht mehr Theoreme nachgewiesen werden als in der gewöhnlichen Aussagenlogik. Der Vorteil der Verwendung von QBFs ergibt sich durch die Möglichkeit, Sachverhalte kompakter zu repräsentieren.
<br><br>
SAT (die Frage nach der Erfüllbarkeit einer Formel der Aussagenlogik) und
QSAT (die Frage nach der Erfüllbarkeit einer QBF) sind zentrale Probleme
in der Informatik mit einer Fülle von Anwendungen, wie zum Beispiel in der
Graphentheorie, bei Planungsproblemen, nichtmonotonen Logiken oder bei der
Verifikation. Insbesondere die Verifikation von Hard- und Software ist ein sehr
aktuelles und wichtiges Forschungsgebiet in der Informatik.
<br><br>
Unser Algorithmus zur Lösung von QBFs basiert auf sogenannten ZBDDs
(engl. Zero-suppressed Binary decision Diagrams), welche eine Variante der
BDDs (engl. Binary decision Diagrams) sind. BDDs sind eine kompakte Repräsentation von Formeln der Aussagenlogik. Der Algorithmus kombiniert nun
bekannte Techniken zum Lösen von QBFs mit der ZBDD-Darstellung unter
Verwendung geeigneter Heuristiken und Memoization. Memoization ermöglicht
dabei das einfache Wiederverwenden bereits gelöster Teilprobleme.
<br><br>
Der Algorithmus wurde unter Verwendung des CUDD-Paketes (Colorado
University Decision Diagram) implementiert und unter dem Namen ZQSAT
veröffentlicht. In Tests konnten wir nachweisen, dass ZQSAT konkurrenzfähig
zu existierenden QBF-Beweisern ist, in einigen Fällen sogar bessere Resultate
liefern kann.
| Identifer | oai:union.ndltd.org:Potsdam/oai:kobv.de-opus-ubp:637 |
| Date | January 2005 |
| Creators | Ghasemzadeh, Mohammad |
| Publisher | Universität Potsdam, Mathematisch-Naturwissenschaftliche Fakultät. Institut für Informatik |
| Source Sets | Potsdam University |
| Language | English |
| Detected Language | English |
| Type | Text.Thesis.Doctoral |
| Format | application/pdf |
| Rights | http://opus.kobv.de/ubp/doku/urheberrecht.php |
Page generated in 0.0016 seconds