GQBF and proof complexity

Abstract

Das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln - das ist, zu entscheiden ob alle existentiell quantifizierten Variablen einer geschlossenen quantifizierten boolschen Formel in einer Form belegt werden können, so dass die Formel damit wahr wird - ist von besonderem beweistheoretischen und komplexitätstheoretischen Interesse. Es generalisiert das aussagenlogische Erfüllbarkeitsproblem und bietet für jede Stufe der polynomiellen Hierarchie prototypische Probleme.<br />Weiters lassen sich viele Probleme der künstlichen Intelligenz und der Spieltheorie als Erfüllbarkeitsproblem für quantifizierte boolesche Formeln kodieren.<br />Derzeit existieren mehrere Beweiser für dieses Problem, basierend auf einer Vielzahl unterschiedlicher Lösungsansätze. Ein kürzlich vorgestellter Beweiser konstruiert Beweise mit Hilfe eines Sequenzkalküls.<br />In diesem Papier untersuchen wir die Fähigkeiten dieses Kalküls kurze Beweise erzeugen zu können und vergleichen verschiedene Konstruktionsmerkmale des Kalküls diesbezüglich. Wir vergleichen diesen Kalkül weiters mit einem weit verbreiteten Resolutionskalkül und untersuchen die Auswirkungen von Pränexierung auf die Länge von Beweisen.<br />Wir zeigen, dass eine strenge Ordnung von Sequenzkalkülen existiert was ihre Fähigkeit betrifft, kurze Beweise erzeugen zu können.<br />Manipulationen im Inneren von Formeln - zusätzlich zu Manipulationen die streng der Struktur von Formeln folgen - können Beweise exponentiell verkürzen. Beweise in Form eines gerichteten, azyklischen Graphen können expontiell kürzer sein als Beweise in Baumform. Weiters zeigen wir obere und untere Schranken für Fähigkeiten, die ein Sequenzkalkül besitzen muss, um ebenso kurze Beweise erzeugen zu können wie Resolutionskalküle. Das Papier beweist auch, dass eine gute Pränexierungsstrategie essentiell ist, um kurze Beweise erzeugen zu können.<br />

The evaluation problem for quantified boolean formulas - deciding if a truth value can be assigned to each existentially quantified variable of a dedicated quantified boolean formula in a way that the formula evaluates to true - is especially interesting from a proof theoretical and complexity theoretical viewpoint. It generalizes the propositional satisfiability problem and provides natural problems for any level of the polynomial hierarchy. From a more practical perspective, many problems from the field of artificial intelligence and game theory can be encoded as evaluation problems for quantified boolean formulas.<br />Currently there exists a wide range of solvers for the evaluation problem for quantified boolean formulas, using a variety of different evaluation strategies.<br />A solver presented recently uses a sequent-style calculus to construct proofs for quantified boolean formulas. We research the capabilities of this sequent-style calculus and compare different features of the calculus amongst each other with respect to their power to generate short proofs. We also compare sequent-style calculi to a widely used version of a resolution-like calculus and examine the impact of prenexing on proof size.<br />In this thesis we establish a strict hierarchy of sequent-style calculi that orders them with respect to their power of creating short proofs. It is proven that adding rules that operate within sub-formulas instead of operating on the outermost connective, respectively quantifier, can exponentially shorten proofs.<br />So can allowing proofs to form directed acyclic graphs rather than trees. We establish an upper and an lower bound of features that are needed for a sequent calculus to generate proofs as short as resolution can. It is also shown that a good choice of prenexing strategy is essential to construct short proofs.<br />