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.

Seit langem ist die Intelligenz des Menschen für viele Forscher und Philosophen ein faszinierendes Forschungsobjekt. Mit dem Aufkommen der Computertechnik erscheint nun zum ersten mal der Traum, einige dieser typisch menschlichen Fähigkeiten nicht nur zu verstehen, sondern nachbauen oder in Teilgebieten gar übertreffen zu können, als realistisch. Ein wichtiger Teil dieses mit &amp;quot;Künstliche Intelligenz&amp;quot; überschriebenen Forschungsgebietes ist das Schließen über Aktionen und Veränderung. Hier wird versucht, die menschliche Fähigkeit, die Effekte seiner Aktionen vorauszusehen und Pläne zum Erreichen von Zielen zu schmieden, nachzubilden. Ein aktives Forschungsgebiet in diesem Rahmen ist der Fluentkalkül, ein Formalismus zur Modellierung von Aktionen und Veränderung. Er stellt Mittel bereit, in der ein automatischer Agent seine Umgebung und die Effekte seiner Aktionen im Rahmen der mathematischen Logik darstellen kann, um mit Hilfe von logischem Schließen sein Verhalten zu planen. Obwohl zum Fluentkalkül viele Arbeiten existieren, die dessen Anwendungsbereiche und Semantik erweitern, gibt es doch noch relativ wenige Arbeiten zum effizienten Schlussfolgern. Dies ist ein Hauptaugenmerk der vorliegenden Arbeit. Es wird ein Algorithmus geschaffen, der Erkenntnisse aus effizienten Verfahren zum Modelchecking mit Binären Entscheidungsdiagrammen (BDDs) sinngemäß überträgt und für ein Fragment des Fluentkalkül erweitert. Damit können nun auch Planungsprobleme von Fluentkalkül-Planern gelöst werden, die der realisierten symbolischen Breitensuche besser zugänglich sind, als der bisher aussschliesslich verwendeten heuristischen Tiefensuche. Um eine leichtere Vergleichbarkeit Fluentkalkül-basierter Planungsverfahren mit anderen Planungsalgorithmen zu ermöglichen, wurde eine Übersetzung des ADL-Fragments der Planungsdomänenbeschreibungssprache PDDL in den Fluentkalkül geschaffen. Damit können zahlreiche Planungsprobleme aus der Literatur und Planungsdomänenbibliotheken auch mit Fluentkalkül-Planern bearbeitet werden. Die Übersetzung kann zugleich als formale Semantik des nur informal spezifizierten PDDL dienen.