Model Counting for SAT via Clause Expansion

Abstract

Beim Modellzählen wird die Anzahl der erfüllenden Variablenzuweisungen einer Booleschen Formel ermittelt. Es handelt sich dabei um eine rechnerisch aufwendige Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Während moderne exakte Modellzähler überwiegend auf Backtracking-basierten Techniken und verwandten Methoden beruhen, bietet das Zählen mittels Inklusions-Exklusions-Prinzip einen alternativen Ansatz, der bislang vergleichsweise wenig Beachtung gefunden hat. Diese Arbeit untersuchtdas Modellzählen für CNF-Formeln unter Verwendung eines auf Klauselerweiterung basierenden Inklusions-Exklusions-Rahmens. Zunächst liefert die Arbeit einen beweistheoretischen Hintergrund, indem sie den etablierten formalen Rahmen der Klauselerweiterung mit dem Resolutions-Beweissystem in Verbindung bringt. Anstatt die leere Menge aus einer Menge unerfüllbarer Klauseln abzuleiten, besteht die Idee darin, die Anzahl der subsumierten Maxterme mithilfe des Inklusions-Exklusions-Prinzips zu zählen. Aufbauend auf diesem Rahmen werden verschiedene Techniken evaluiert, um den Rechenaufwand der Inklusions-Exklusions-Zählung zu reduzieren. Dazu gehören die Subsumption, die Verwendung von Konfliktgraphen und deren unabhängigen Mengen zur Gewinnung von Informationen über die integralen Eigenschaften sowie das Sieben von Inklusions-Exklusions-Termen durch die Propagierung von Konflikten. Ein zentraler Beitrag ist ein neuartiges Vorverarbeitungsverfahren, das auf einer modifizierten Form der inversen Resolution basiert. Das Verfahren fügt Klauseln widersprüchliche Literale hinzu und beseitigt so Überschneidungen bei gemeinsamen Maxtermen, was wiederum die Anzahl der Inklusions-Exklusions-Terme zur Berechnung der exakten Modellanzahl erheblich reduziert. Diese Methode ist in der Lage, geeignete Formeln auf „Hitting-Formeln“ zu reduzieren, für die die Modellanzahl in linearer Zeit berechnet werden kann. Die Leistungsfähigkeit der inversen Resolution wird analysiert, indem eine Verbindung zu strukturellen Eigenschaften von Instanzen hergestellt wird, die sich aus den zugrunde liegenden Graphstrukturen ergeben. Schließlich werden die entwickelten Techniken zu einem vollständigen Algorithmus zur Modellanzahlberechnung kombiniert und an ausgewählten Klassen von Instanzen analysiert, darunter k-CNF, Pigeonhole-Formeln sowie graphbasierte Formeln. Die Ergebnisse zeigen, dass das Inklusions-Exklusions-Verfahren etablierte State-of-the-Art-Zähler im allgemeinen Fall wahrscheinlich nicht ersetzen wird, jedoch eine vielversprechende Alternative für strukturell günstige Instanzen bieten kann, da im Durchschnittsfall für k-CNFs mit k ≫ √n die Zählung in polynomieller Zeit möglich ist. Die Arbeit liefert somit eine theoretische Grundlage für die weitere Erforschung der auf dem Inklusions-Exklusions-Prinzip basierenden Modellzählung, wobei der Schwerpunkt insbesondere auf der Charakterisierung von Instanzen, verbesserten Vorverarbeitungsstrategien und praktischen Implementierungen liegt.

Model counting asks for the number of satisfying assignments of a Boolean formula and is a computationally demanding generalization of the Boolean satisfiability problem. While modern exact model counters predominantly rely on backtracking-based techniques and related methods, counting via inclusion exclusion provides an alternative approach that has received comparatively little attention. This thesis investigates model counting for CNF formulas using an inclusion-exclusion framework based on clause expansion. Initially, the work provides a proof-theoretic background by relating the established formal clause expansion framework to the resolution proof system. Instead of deriving the empty set from a set of unsatisfiable clauses, the idea is to count the number of subsumed maxterms with the inclusion-exclusion principle. Building on this framework, several techniques are evaluated to reduce the computational cost of inclusion-exclusion counting. These include subsumption, using conflict graphs and their independent sets to obtain information about the integral properties, and sieving of inclusion-exclusion terms by propagating conflicts. A central contribution is a novel preprocessing procedure based on a modified form of inverse resolution. The procedure introduces conflicting literals to clauses and thus removes overlaps among shared maxterms, which in turn significantly reduces the amount of inclusion-exclusion terms to compute the exact model count. This method is able to reduce suitable formulas into “hitting formulas”, for which model counting can be performed in linear time. The power of inverse resolution is analyzed by bridging the gap to structural properties of instances that emerge from underlying graph structures. Finally, the developed techniques are combined into a complete model counting algorithm and analyzed on selected classes of instances, including k-CNF, pigeonhole formulas, as well as graph-based formulas. The results demonstrate that inclusion-exclusion is unlikely to replace established state-of-the-art counters in the general case, but can offer a promising alternative for structurally favorable instances, as in the average case for k-CNFs with k ≫ √n, counting is possible in polynomial time. The thesis therefore provides a theoretical foundation for further investigation of inclusion-exclusion-based model counting, with particular emphasis on instance characterization, improved preprocessing strategies, and practical implementations.