Algorithms for the satisfiability problem

Abstract

Diese Arbeit befasst sich mit Worst-Case-Algorithmen für das Erfüllbarkeitsproblem boolescher Ausdrücke in konjunktiver Normalform. Im Wesentlichen betrachten wir Laufzeitschranken drei verschiedener Algorithmen, zwei für 3-SAT und einen für Unique-k-SAT. Wir entwickeln einen randomisierten Algorithmus, der eine Lösung eines erfüllbaren 3-KNF-Ausdrucks G mit n Variablen mit einer erwarteten Laufzeit von O(1.32793^n) findet. Der Algorithmus basiert auf der Analyse sogenannter Strings, welche Sequenzen von Klauseln der Länge drei sind. Dabei dürfen einerseits nicht aufeinanderfolgende Klauseln keine Variablen und andererseits aufeinanderfolgende Klauseln ein oder zwei Variablen gemeinsam haben. Gibt es wenige Strings, so treffen wir wahrscheinlich bereits während der String-Suche auf eine Lösung von G. 1999 entwarf Schöning einen Algorithmus mit einer Schranke von O(1.3334^n) für 3-SAT. Viele Strings erlauben es, die Laufzeit dieses Algorithmusses zu verbessern. Weiterhin werden wir den PPSZ-Algorithmus für Unique-k-SAT derandomisieren. Der 1998 von Paturi, Pudlak, Saks und Zane vorgestellte PPSZ-Algorithmus hat die besondere Eigenschaft, dass die Lösung eines eindeutig erfüllbaren 3-KNF-Ausdrucks in höchstens O(1.3071^n) erwarteter Laufzeit gefunden wird. Die derandomisierte Variante des Algorithmusses für Unique-k-SAT hat im Wesentlichen die gleiche Laufzeitschranke. Wir erreichen damit die momentan beste deterministische Worst-Case-Schranke für Unique-k-SAT. Zur Derandomisierung wenden wir die "Methode der kleinen Zufallsräume" an. Schließlich verbessern wir die Schranke für den Algorithmus von Iwama und Tamaki. 2003 kombinierten Iwama und Tamaki den PPSZ-Algorithmus mit Schönigs Algorithmus und konnten eine Schranke von O(1.3238^n) bewiesen. Um seinen Beitrag zum kombinierten Algorithmus zu steigern, justieren wir die Schranke des PPSZ-Algorithmusses. Damit erhalten wir die momentan beste randomisierte Worst-Case-Schranke für das 3-SAT-Problem von O(1.32216^n).

This work deals with worst-case algorithms for the satisfiability problem regarding boolean formulas in conjunctive normal form. The main part of this work consists of the analysis of the running time of three different algorithms, two for 3-SAT and one for Unique-k-SAT. We establish a randomized algorithm that finds a satisfying assignment for a satisfiable 3-CNF formula G on n variables in O(1.32793^n) expected running time. The algorithm is based on the analysis of so-called strings, which are sequences of clauses of size three, whereby non-succeeding clauses do not share a variable, and succeeding clauses share one or two variables. If there are not many strings, it is likely that we already encounter a solution of G while searching for strings. In 1999, Schöning proved a bound of O(1.3334^n) for 3-SAT. If there are many strings, we use them to improve the running time of Schöning''s algorithm. Furthermore, we derandomize the PPSZ algorithm for Unique-k-SAT. The PPSZ algorithm presented by Paturi, Pudlak, Saks, and Zane in 1998 has the feature that the solution of a uniquely satisfiable 3-CNF formula can be found in expected running time at most O(1.3071^n). In general, we will obtain a derandomized version of the algorithm for Unique-k-SAT that has essentially the same bound as the randomized version. This settles the currently best known deterministic worst-case bound for the Unique-k-SAT problem. We apply the `Method of Small Sample Spaces'' in order to derandomize the algorithm. Finally, we improve the bound for the algorithm of Iwama and Tamaki to get the currently best known randomized worst-case bound for the 3-SAT problem of O(1.32216^n). In 2003 Iwama and Tamaki combined Schöning''s and the PPSZ algorithm to yield an O(1.3238^n) bound. We tweak the bound for the PPSZ algorithm to get a slightly better contribution to the combined algorithm.