Theorembeweisen für QBF und die Anwendung zum Planen

Theorembeweisen für QBF und die Anwendung zum Planen

Quantifizierte Boolesche Formeln (QBF) sind deshalb interessant, weil das Evaluierungsproblem f"ur QBF mit unterschiedlichen Quantifizierungen die Klassen der polynomiellen Hierarchie absteckt, wie SAT, das Erfüllbarkeitsproblem für unquantifizierte Boolesche Formeln, die Komplexitätsklasse NP absteckt. Quantifizierte Boolesche Formeln der Form EA... repräsentieren die Komplexitätsklassen Sigma_k^p, QBF der Form AE... die Klassen Pi_k^p. QBF können deshalb als Repräsentation für alle Probleme in der polynomiellen Hierarchie dienen. In dieser Arbeit wird mit Qsat ein Algorithmus vorgestellt, der die Evaluierbarkeit von QBF testet und auf dem Davis-Putnam-Algorithmus für SAT basiert. Als eine Anwendung wird das bedingte Planen (Conditional Planning) herangezogen und zwei Methoden für das Übersetzen bedingter Planungsprobleme von STRIPS-Notation nach QBF vorgestellt. Mit Hilfe der Qsat-Implementierung wurden die Untersuchungen über den Crossover-Point von SAT-Problemen auf QBF-Probleme ausgedehnt und eine Abhängigkeit des Crossover-Points vom Anteil der universellen Variablen festgestellt. Diese Abhängigkeit kann mit einer Crossover-Funktion beschrieben werden.

QBF and Conditional Planning

The interest in Quantified Boolean Formulae (QBF) rises from the fact that the problems of evaluating QBF with the different quantifications characterize the complexity levels of the polynomial hierarchy, like SAT, the satisfiability problem for unquantified Boolean Formulae characterizes the complexity class NP. The evaluation problem for Quantified Boolean Formulae of the Form EA... is a complete problem for the classes Sigma_k^p, the Evaluation problem for QBF of the Form AE... is complete for the complexity classes Pi_k^p. QBF can therefore be used as a representation for all problems in the polynomial hierarchy. In this work Qsat, an algorithm for evaluating QBF is presented, based on the Davis-Putnam-Procedure for SAT problems. An application is presented by showing two translation strategies for STRIPS-encoded Conditional Planning problems to QBF. Using the Qsat implementation we extended the tests concerning the Crossover-Point for SAT-problems to QBF. We examined the influence of universally quantified variables on this point and describe it with a Crossover-Function.

Die Diplomarbeit - the diploma thesis - gziped postscript file in German

Ein Dateiformat für QBF - a file format for QBF - gziped postscript file in German

@MastersThesis{Bos98,
  author = "Rainer Bosch",
  title =  "{Theorembeweisen f{\"u}r QBF und die Anwendung zum Planen}", 
  school = "Universit{\"a}t Ulm",
  year =   1998}