Extending a tableau-based SAT procedure with techniques from CNF-based SAT

Abstract

Das propositionale Erfüllbarkeitsproblem ist ein klassisches Entscheidungsproblem der theoretischen Informatik. Es war das erste Entscheidungsproblem für das NP-Vollständigkeit bewiesen wurde. In den letzten fünfzehn Jahren hat sich die Effizienz von Lösungsalgorithmen für Instanzen in konjunktiver Normalform enorm verbessert. Programme, die das Erfüllbarkeitsproblem lösen (sogenannte SAT Solver), finden heute vielfältige Anwendung in Industrie und Forschung, etwa in Soft- und Hardwareverifikation und in Logik-basierter Planung. Bei der Übersetzung von strukturierten Formeln oder Schaltkreisinstanzen in konjunktive Normalform (KNF) geht die ursprüngliche Strukturinformation der Formel verloren. Durch deren Verlust wird der Einsatz strukturbasierter Heuristiken zum Beschleunigen des Lösungsprozesses unmöglich.<br />In dieser Arbeit wird eine Erweiterung des BC Tableaukalküls zur Feststellung der Erfüllbarkeit von beschränkten kombinatorischen Schaltkreisen präsentiert. Eine kurze Einführung in propositionale Logik und das Erfüllbarkeitsproblem (SAT) wird gegeben, und es wird der klassische Davis-Logemann-Loveland (DLL) Algorithmus zur Lösung von SAT Instanzen in konjunktiver Normalform präsentiert. Es wird aufgezeigt, wie moderne KNF-Solver das grundlegende DLL Schema um nicht-chronologisches Backtracking und Lernen erweitern. Moderne Techniken werden beschrieben mithilfe derer SAT-Solver in der Lage sind praktisch relevante Probleme in Industrie und Forschung zu lösen, und es werden Ansätze präsentiert um das Lösen des SAT Problems in Schaltkreisinstanzen zu beschleunigen.<br />Es wird gezeigt, dass eine Implementierung des BC Tableaus als generalisierte DLL Prozedur gesehen werden kann und es wird dargestellt, wie sich Techniken aus dem Bereich des KNF-basierten SAT Solving in das BC Tableau integrieren lassen. Ein Prototyp einer solchen erweiterten Tableauprozedur wurde entwickelt und seine Effektivität im Vergleich zu bestehenden SAT Solvern evaluiert. Es zeigt sich, dass die Erweiterung des BC Tableaus die durchschnittliche Geschwindigkeit in Benchmarks wesentlich verbessert, und dass das erweiterte BC Tableau als Grundlage für Schaltkreis-basierte SAT Solver durchaus mit modernen CNF-basierten Implementierungen Schritt halten kann.<br />

The propositional satisfiability problem (SAT) is one of the central decision problems in theoretical computer science. It was the first decision problem that was proven to be NP complete. In the last 15 years, the efficacy of CNF-based SAT algorithms, i.e., algorithms for instances of propositional formulas in conjunctive normal form (CNF), has increased significantly. Today, SAT solvers are employed in a number of applications in industry and science such as software and hardware verification or logic-based planning. Using a CNF-based SAT solver requires a translation step from the original formula to CNF. The result lacks the structural information of the original instance, which could have been used heuristically to speed up the solving process.<br />In this thesis, we present an extension of the BC tableau calculus for determining satisfiability of constrained Boolean circuits. A short introduction to propositional logic and the SAT problem is given.<br />Classical algorithms for solving SAT such as the Davis-Putnam (DP) procedure and the Davis-Logemann-Loveland (DLL) procedure are presented.<br />Modern extensions to the basic DLL framework, such as non-chronological backtracking and clause learning, are discussed, which reduce solving time on industrial instances considerably. We also present some approaches for solving the SAT problem in circuits.<br />We show that a BC-tableau-based SAT algorithm can be seen as a generalization of the basic DLL procedure. We show how techniques from CNF-based SAT can be integrated into such a tableau procedure and present a prototype that implements these ideas. We use a set of benchmark instances to show that the extensions increase the efficiency of the basic BC tableau considerably, and that our circuit-based SAT solver can compete with state-of-the-art CNF-based solving procedures.