QPar : a multithreaded distributed solver for quantified Boolean formulas

Abstract

Viele wichtige Probleme aus den Gebieten der künstlichen Intelligenz, wie zum Beispiel Verfikation, Planen und Wissensrepräsentation, befinden sich in der Komplexitätsklasse PSPACE.<br />Quantifizierte Boolsche Formeln (QBFs) erweitern die Aussagenlogik um Quantoren über aussagenlogische Variablen, und sind das prototypische Problem für PSPACE.<br />Durch eine Polynomialzeitreduktion ist es möglich ein Problem auf eine Darstellung in QBF zu reduzieren. Durch die Lösung dieser QBF kann eine Lösung des Originalproblems hergeleitet werden. Im Allgemeinen unterliegen solche Formeln keinen strukturellen Einschränkungen. Unglücklicherweise akzeptieren viele Solver nur Formeln in der konjunktiven Pränex-Normalform (PCNF). Die Überführung von QBFs in diese Form verlangt das Pränexieren der Formel und der Transformation in die konjunktive Normalform.<br />Die Pränexierung schiebt alle Quantifikatoren aus der Formel heraus, sodass diese einen durchgehenden Quantifikatorenblock am Beginn der Formel bilden. Das Pränexieren selbst ist nicht deterministisch, und es wurde gezeigt, dass die Wahl der Pränexierungsstrategie einen grossen Einfluss auf das Verhalten des Solvers hat. Zusätzlich muss die Formel in konjunktive Normalform konvertiert werden, was zu einem Verlust von struktureller Information über die Formel führt und potentiell die Formelgrösse erhöht. Durch die Verarbeitung von Formeln in Negationsnormalform (NNF) wird das Pränexieren überflüssig und die Formelstruktur bleibt erhalten.<br />In dieser Diplomarbeit stellen wir QPar vor. QPar ist ein Solver für QBFs in NNF. QPar teilt eine Formel in Unterprobleme und verteilt diese an mehrere Slave Rechner zur parellelen Verarbeitung. Die Methode zur Teilung der Formel, eine Variante des DPLL Algorithmus, erlaubt die Verwendung verschiedener Teilungsheuristiken. Durch Multi-threading auf den Slave Rechnern kann eine maximale Ausnutzung der modernen Multi-Core- bzw.<br />Multi-Prozessor- Architekturen erreicht werden. Die einzelnen Unterprobleme werden zur Berechnung an singlethreaded Solver weitergereicht. Aus den Resultaten der Unterprobleme kann eine Lösung des Gesamtproblems konstruiert werden.<br />QPar zeichnet sich durch eine modulare Architektur aus, welche die Integration von neuen single-threaded Solvern als Back-end erleichtert, und QPar zu einem generischen Parallelisierungsframework macht. Im Zuge dieser Arbeit stellen wir auch neue Heuristiken für Formeln in negations normal Form vor, welche bis jetzt noch nicht in der Literatur diskutiert wurden.<br />Wir vergleichen die Performance der parallelen Berechnung mit QPar mit serieller Verarbeitung und präsentieren eine Evaluation der implementierten Teilungsheuristiken.<br />

Many important problems in the fields of artificial intelligence like verification, planning and knowledge representation are located in the complexity class PSPACE. The decision problem of quantified Boolean formulas (QBFs), which extend classical propositional logic with quantifications over propositional variables, is the prototypical problem for PSPACE.<br />By polynomial-time computable reductions of problems into an adequate representation as QBFs, solutions to the original problems can be found by solving the respective QBF and translating back the solution. Most state-of-the-art QBF solvers only accept formulas in prenex conjunctive normal form (PCNF) as input which requires additional preprocessing steps. Prenexing shifts all quantifiers to the leftmost position, forming a single block of quantifiers at the start of the formula. Prenexing is not deterministic and it has been empirically shown that the selection of a prenexing strategy strongly influences the behaviour of a solver.<br />In addition to prenexing, the formula must be converted into conjunctive normal form, which results in a loss of structural information about the formula and a potential increase in formula size.<br />By allowing input formulas to be in negation normal form (NNF), prenexing is not necessary and the formula structure can be preserved.<br />In this thesis we present QPar, a solver for QBFs in NNF. QPar works by semantically splitting a formula into sub-problems and distributing them to multiple slave hosts for parallel computation.<br />The splitting method, a variant of the DPLL algorithm, allows for the use of different branching heuristics. Multi-threading on the slave components allow for maximum utilisation of modern multi-core/multi-processor systems. The individual sub-problems are passed to a single-threaded solver for computation. The results of the sub-problems are combined to yield a result for the original formula.<br />QPar features a modular architecture, making the implementation of new back ends easy and allowing it to be used as a general parallelization framework for single-threaded solvers. QPar also introduces new branching heuristics for formulas in NNF which have not been discussed in present literature yet.<br />We show the performance of QPar in comparison to single-threaded solving, and present results of the evaluation of the realised branching heuristics.