Deciding the truth of a Quantified Boolean Formula (QBF) is a canonical PSPACE-complete problem. It provides a powerful framework for encoding problems that lie in PSPACE. These include many problems in automatic verification, and problems with discrete uncertainty or non-determinism. Two person adversarial games are another type of problem that are naturally encoded in QBF. It is standard practice to use Conjunctive Normal Form (CNF) when representing QBFs. Any propositional formula can be efficiently translated to CNF via the addition of new variables, and solvers can be implemented more efficiently due to the structural simplicity of CNF. However, the translation to CNF involves a loss of some structural information. This thesis shows that this structural information is important for efficient QBF solving, and shows how this structural information can be utilized to improve state-of-the-art QBF solving. First, a non-CNF circuit-based solver is presented. It makes use of information not present in CNF to improve its performance. We present techniques that allow it to exploit the duality between solutions and conflicts that is lost when working with CNF. This duality can also be utilized in the production of certificates, allowing both true and false formulas to have easy-to-verify certificates of the same form. Then, it is shown that most modern CNF-based solvers can benefit from the additional information derived from duality using only minor modifications. Furthermore, even partial duality information can be helpful. We show that for standard methods for conversion to CNF, some of the required information can be reconstructed from the CNF and greatly benefit the solver.

Deciding the truth of a Quantified Boolean Formula (QBF) is a canonical PSPACE-complete problem. It provides a powerful framework for encoding problems that lie in PSPACE. These include many problems in automatic verification, and problems with discrete uncertainty or non-determinism. Two person adversarial games are another type of problem that are naturally encoded in QBF. It is standard practice to use Conjunctive Normal Form (CNF) when representing QBFs. Any propositional formula can be efficiently translated to CNF via the addition of new variables, and solvers can be implemented more efficiently due to the structural simplicity of CNF. However, the translation to CNF involves a loss of some structural information. This thesis shows that this structural information is important for efficient QBF solving, and shows how this structural information can be utilized to improve state-of-the-art QBF solving. First, a non-CNF circuit-based solver is presented. It makes use of information not present in CNF to improve its performance. We present techniques that allow it to exploit the duality between solutions and conflicts that is lost when working with CNF. This duality can also be utilized in the production of certificates, allowing both true and false formulas to have easy-to-verify certificates of the same form. Then, it is shown that most modern CNF-based solvers can benefit from the additional information derived from duality using only minor modifications. Furthermore, even partial duality information can be helpful. We show that for standard methods for conversion to CNF, some of the required information can be reconstructed from the CNF and greatly benefit the solver.

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.