Hasso-Plattner-Institut25 Jahre HPI
Hasso-Plattner-Institut25 Jahre HPI
Login
 

Ralf Rothenberger

Satisfiability Thresholds for Non-Uniform Random k-SAT

Das Boolesche Erfüllbarkeitsproblem (SAT) ist eines der zentralsten Probleme der theoretischen Informatik. Es war das erste Problem, dessen NP-Vollständigkeit nachgewiesen wurde, von Cook und Levin unabhängig voneinander. Heutzutage wird vermutet, dass SAT nicht in subexponentialler Zeit gelöst werden kann. Darum wird allgemein angenommen, dass SAT und seine eingeschränkte Version k-SAT nicht effizient zu lösen sind. Trotzdem können moderne SAT solver sogar riesige Echtweltinstanzen dieser Probleme in angemessener Zeit lösen.

Warum ist SAT theoretisch schwer, aber einfach in der Praxis? Ein Ansatz um diese Frage zu beantworten ist die Untersuchung der durchschnittlichen Laufzeit von SAT. Um diese durchschnittliche oder typische Laufzeit analysieren zu können, wurde zufälliges k-SAT eingeführt. Dieses Modell erzeugt all k-SAT-Instanzen mit n Variablen und m Klauseln mit gleicher Wahrscheinlichkeit. Die Untersuchung des Zufallsmodells für k-SAT führte zu einer Vielzahl von Erkenntnissen und Techniken zur Untersuchung zufälliger Strukturen im Allgemeinen. Eine der größten Entdeckungen in diesem Zusammenhang war das Auftreten des sogenannten Erfüllbarkeitsschwellwerts: Ein Phasenübergang in der Anzahl der Klauseln, an dem die generierten Formeln von asymptotisch sicher erfüllbar zu asymptotisch sicher unerfüllbar wechseln. Zusätzlich scheinen Instanzen, die um diesen Übergang herum erzeugt werden, besonders schwer zu lösen zu sein.

In dieser Arbeit analysieren wir ein allgemeineres Zufallsmodell für k-SAT, das wir nichtuniformes zufälliges k-SAT nennen. Im Gegensatz zum klassischen Modell, hat jede Boolesche Variable jetzt eine bestimmte Wahrscheinlichkeit gezogen zu werden. Für jede der m Klauseln ziehen wir k Variablen entsprechend ihrer Wahrscheinlichkeitsverteilung und wählen ihre Vorzeichen uniform zufällig. Nichtuniformes zufälliges k-SAT gibt uns mehr Kontrolle über die Verteilung Boolescher Variablen in den resultierenden Formeln. Das erlaubt uns diese Verteilungen auf die in der Praxis beobachteten zuzuschneiden. Insbesondere enthält nichtuniformes zufälliges k-SAT die zuvor vorgestellten Modelle zufälliges k-SAT, skalenfreies zufälliges k-SAT und geometrisches zufälliges k-SAT als Spezialfälle.

Wir analysieren den Erfüllbarkeitsschwellwert in nichtuniformem zufälligen k-SAT abhängig von den Wahrscheinlichkeitsverteilungen für Variablen. Unser Ziel ist es, Bedingungen an diese Verteilungen abzuleiten, unter denen ein Äquivalent der Erfüllbarkeitsschwellwertsvermutung für zufälliges k-SAT gilt. Wir fangen mit dem wahrscheinlich einfacheren Modell nichtuniformem zufälligen 2-SAT an. Für dieses Modell zeigen wir, unter welchen Bedingungen ein Schwellwert existiert, ob er steil oder flach ansteigt und was die führende Konstante der Schwellwertfunktion ist. Das sind genau die Zutaten, die man benötigt um die Erfüllbarkeitsschwellwertsvermutung zu bestätigen oder zu widerlegen. Für nichtuniformes zufälliges k-SAT mit k≥3 zeigen wir nur hinreichende Bedingungen, unter denen ein Schwellwert existiert. Wir zeigen außerdem einige Eigenschaften der Variablenwahrscheinlichkeiten, die dazu führen, dass der Schwellwert steil ansteigt. Dies sind unseres Wissens nach die ersten allgemeinen Resultate zum Schwellwertverhalten von nichtuniformem zufälligen k-SAT.