Exakte Algorithmen für Erfüllbarkeitsprobleme

Abstract

Die Erfüllbarkeitsprobleme SAT und CSP dürfen mit Fug als die "natürlichsten" aller NP-vollständigen Probleme bezeichnet werden. Die vorliegende Arbeit befasst sich mit deren algorithmischen Behandlung. Sie besteht aus zwei Teilen. Der erste Teil befasst sich mit Erfüllbarkeitsproblemen, deren Lösbarkeit aus dem bekannten Lovász Local Lemma folgt. Während seit dessen Entdeckung im Jahre 1975 durch Paul Erdős und Lászlo ́ Lovász feststeht, dass Erfüllbarkeitsprobleme mit einer nirgends zu dichten Konzentration an Klauseln immer eine erfüllende Belegung zulassen, war ein algorithmisches Verfahren zur tatsächlichen Bestimmung dieser Lösung lange nicht bekannt. Wir verfeinern frühere Ansätze, das Local Lemma algorithmisch zu machen und präsentieren schliesslich einen Polynomialzeitalgorithmus, der für beinahe alle bisher bekannten Anwendungen des Local Lemma einen konstruktiven Beweis liefert. Im zweiten Teil verlassen wir die Klasse der in polynomieller Zeit lösbaren Probleme und betrachten stattdessen den von Uwe Schöning im Jahre 1999 vorgeschlagenen und analysierten randomisierten Exponentialzeitalgorithmus für allgemeine Klauselerfüllungsprobleme. Als Hauptbeitrag neben weiteren Aspekten verfeinern wir frühere Ansätze, diesen Algorithmus zu derandomisieren und präsentieren schliesslich die erste deterministische Variante, welche gegenüber dem Zufallsalgorithmus nicht an Effizienz einbüsst.