Erfüllbarkeit und Suchaufwand · Verständlich erklärt

Der Phasenübergang bei SAT verständlich erklärt

Ein Buffet soll alle Gäste zufriedenstellen, doch jeder Gast stellt Bedingungen. Je mehr Bedingungen, desto mühsamer die Planung? Die Messung hinter dieser Seite zeigt: Am mühsamsten wird es in der Mitte. Bei sehr vielen Bedingungen merkt man früher, dass es nicht geht. Erst für Einsteiger, dann für Fachleute.

Zuletzt aktualisiert:

Teil 1 · Für Einsteiger

Ein Wort unbekannt? Das Begriffsverzeichnis erklärt es in wenigen Sätzen.

Ein Buffet für alle Gäste

Stellen Sie sich vor, Sie planen ein Buffet. Für jede Speise entscheiden Sie nur mit Ja oder Nein, ob sie aufgetischt wird: Salat ja oder nein, Suppe ja oder nein, Kuchen ja oder nein.

Jeder Gast hat einen Wunsch aus drei Teilen, zum Beispiel: „Es gibt Salat, oder es gibt keine Suppe, oder es gibt Kuchen.“ Der Gast ist zufrieden, wenn mindestens ein Teil seines Wunsches zutrifft. Alle Wünsche zusammen heißen hier Wunschzettel.

Die Frage lautet: Gibt es eine Auswahl von Ja und Nein, die alle Gäste zufriedenstellt? Fachleute nennen diese Aufgabe SAT, nach dem englischen Wort für „erfüllbar“. Ein Wunschzettel ist erfüllbar, wenn es so eine Auswahl gibt.

Die Aufgabe gilt als Musterbeispiel einer schweren Aufgabe, in der Fachsprache NP-vollständig. Gemeint ist der schlimmste Fall, ein gezielt böse gebauter Wunschzettel. Ein Verfahren, das dafür bei wachsender Speisenzahl sicher schnell bleibt, kennt niemand.

Diese Seite fragt etwas anderes: Wie schwer sind zufällig gewürfelte Wunschzettel? In einem vereinfachten Rechenbild sucht dafür ein einfaches Rechenprogramm die Auswahl.

Wie das Rechenprogramm plant

Das Programm geht vor wie Sie am Küchentisch. Es legt eine Speise fest, etwa „Salat ja“, und prüft alle Wünsche neu. Ist bei einem Wunsch nur noch ein Teil offen, weil die anderen beiden nicht mehr zutreffen können, ist dieser Teil erzwungen. Das ist eine Zwangsfolge.

Trifft bei einem Wunsch gar nichts mehr zu, ist das eine Sackgasse. Dann geht das Programm zurück und probiert bei der letzten freien Entscheidung das Gegenteil. Sind alle Gäste zufrieden, ist es fertig. Sind alle Möglichkeiten erfolglos probiert, gibt es kein passendes Buffet.

Den Aufwand messen wir in Suchschritten: Wie viele Zwischenstände betrachtet das Programm? Sekunden zählen wir nicht, denn die Dauer eines Schritts hängt von der Größe des Wunschzettels ab.

Das Überraschende: Am schwersten ist es in der Mitte

Entscheidend ist, wie viele Wünsche auf eine Speise kommen. Dazu teilen wir die Zahl der Wünsche durch die Zahl der Speisen. Beispiel: 20 Speisen und 90 Wünsche ergeben im Durchschnitt viereinhalb Wünsche je Speise. Gemessen wurde an zufälligen Wunschzetteln mit 20 bis 40 Speisen, je 40 Wunschzettel gleicher Größe. Als typischer Aufwand gilt der mittlere Wert: Man ordnet alle nach ihren Suchschritten und nimmt den in der Mitte. Er ist weniger anfällig für einzelne Ausreißer als ein Durchschnitt.

Die Messung zeigt drei Bereiche. Die Begründungen sind Deutungen, gemessen sind nur Anteile und Suchschritte.

  • Drei Wünsche je Speise: Alle gemessenen Wunschzettel waren erfüllbar, und das Programm fand die Auswahl mit wenigen Suchschritten. Warum: Es bleibt viel Spielraum, deshalb endet eine Wahl selten in einer Sackgasse.
  • Viereinhalb bis fünf Wünsche je Speise: Hier kippt der Anteil erfüllbarer Wunschzettel von überwiegend erfüllbar zu überwiegend unerfüllbar, und das Programm braucht typisch die meisten Suchschritte. Warum: Es gibt nur noch wenige passende Auswahlen, aber noch keinen offensichtlichen Widerspruch. Das Programm läuft lange in Zweige, die erst spät enden.
  • Sechs Wünsche je Speise: Höchstens 2 von 40 Wunschzetteln waren noch erfüllbar. Bei den größeren Wunschzetteln der Messung brauchte das Programm weniger Suchschritte als in der Mitte, aber mehr als bei drei Wünschen je Speise. Warum: Jede Festlegung berührt viele Wünsche, deshalb zeigt sich ein Widerspruch früh.

Das Kippen heißt in der Fachsprache Phasenübergang, nach der Physik, wo Stoffe ihren Zustand wechseln. Wo genau die schwerste Stelle liegt, hing von den gewürfelten Wunschzetteln ab: Sie lag zwischen viereinhalb und gut fünf Wünschen je Speise.

Wächst der Aufwand trotzdem mit der Größe?

An der schwierigen Stelle ja. Bei viereinhalb Wünschen je Speise haben wir von 20 auf 70 Speisen vergrößert, je 20 Wunschzettel. Der typische Aufwand stieg auf das 23-Fache, bei nur dreieinhalbmal so vielen Speisen. Ob das so weitergeht, ist nicht bewiesen, es sind nur sechs Größen. Unsere Deutung: Mit jeder weiteren Speise kommen zu jeder bisherigen Auswahl zwei neue, mit Ja und mit Nein.

Was dem Programm hilft

Erstens: Zwangsfolgen nutzen oder nicht. Ohne sie probiert das Programm auch dort herum, wo nichts zu probieren ist. Zweitens: die Reihenfolge der Speisen. Das Programm kann sie stur nach der Liste festlegen, oder zuerst die Speise, die in den meisten Wünschen vorkommt, oder nach einer dritten Regel, die Wünschen mit nur noch wenigen offenen Teilen mehr Gewicht gibt.

Gemessen wurde an 20 Wunschzetteln mittlerer Größe, mit festem Höchstmaß an Suchschritten. Ohne Zwangsfolgen brauchte das Programm je nach Regel mindestens 20-mal so viele Suchschritte. Nach der Liste brach es bei 18 von 20 ab; dort ist der Faktor nur eine Untergrenze.

Mit Zwangsfolgen blieb ein Unterschied: Die schlechteste Regel brauchte typisch mehr als das Fünffache der Suchschritte der besten, nämlich der dritten.

Schwer durch den Aufbau, nicht durch den Zufall

Manche Aufgaben sind schwer, weil sie so gebaut sind. Stellen Sie sich eine Tischordnung vor: sechs Einzeltische, sieben Gäste, jeder Gast braucht einen Tisch. Das geht nicht, das sehen Sie durch Zählen. Das Programm zählt aber nicht, es probiert Tisch für Tisch durch. Als Wunschzettel geschrieben: Jeder Gast wünscht sich einen Tisch, und je zwei Gäste wünschen sich, nicht am selben Tisch zu sitzen.

In der Messung brauchte es dafür 1.439 Suchschritte. Zum Vergleich: Ein zufällig gewürfelter Wunschzettel mit ähnlich vielen Wünschen brauchte typisch 26.

Dann wurde bei 1 % der Wunschteile zufällig getauscht: Aus „Anna sitzt an Tisch drei“ wird „Anna sitzt nicht an Tisch drei“, oder umgekehrt. Alle gestörten Fassungen der Messung ließen sich nun erfüllen, typisch mit wenigen Suchschritten.

Häufige Missverständnisse

  • „NP-vollständig heißt: für das Programm nicht lösbar.“ Nein. Die zufälligen Wunschzettel der Messung entschied das einfache Programm mit Zwangsfolgen auch bei den größten Größen. Schwer wird es im schlimmsten Fall, nicht bei jedem Wunschzettel.
  • „Wenn ein kleiner Eingriff eine schwere Aufgabe leicht macht, war sie nie wirklich schwer.“ Nein. Durch das Tauschen hat sich die Antwort geändert. Gelöst wurde eine andere Aufgabe. Unlösbar blieben in einer Nachprüfung fast nur Fassungen, bei denen zufällig nichts getauscht wurde: Sie sind das Original.

Woran Sie das im Alltag erkennen

  • Sie stopfen eine Lücke im Plan, und dafür reißt an anderer Stelle eine neue auf, mehrmals hintereinander. Vermutlich haben Sie viele, aber noch nicht zu viele Auflagen.
  • Jemand nennt eine Aufgabe „schwer“, Sie lösen Ihre in Minuten. Gemeint ist vermutlich die schlimmste Fassung.

Wie ernst ist das Rechenbild zu nehmen?

Gemessen wurde nur an zufälligen Wunschzetteln mit bis zu 70 Speisen und an einem einfachen Suchverfahren. Moderne Programme lernen aus Sackgassen und lösen Aufgaben aus der Praxis mit Millionen Entscheidungen; dazu sagt diese Seite nichts.

Was Sie mitnehmen

  • Fragen Sie beim Wort „schwer“ zuerst: Gilt es für den schlimmsten Fall oder für meine Aufgabe?
  • Suchen Sie in einer Planung zuerst, was erzwungen ist, bevor Sie Möglichkeiten durchprobieren.
  • Wird eine Planung zäh, fragen Sie, ob Sie zwischen Spielraum und Überbestimmung stehen.

Zu dieser Seite gehört ein Programm zum Ausprobieren im Browser, die Demo. Dort würfeln Sie Wunschzettel und sehen die Suchschritte. Zum Verstehen brauchen Sie sie nicht. Der erste Knopf unten öffnet die Demo, der zweite führt zum zweiten Teil für Fachleute.

Hinweis: Alle Demos rechnen mit synthetischen oder frei verfügbaren Beispieldaten und laufen auf einem externen Anbieter (Datenschutz). Bitte geben Sie darin keine vertraulichen oder personenbezogenen Daten ein. Die Ergebnisse gelten für die jeweilige Demo-Instanz und lassen sich nicht ungeprüft auf reale Fälle übertragen; für darauf gestützte Entscheidungen übernehme ich keine Gewähr.

Teil 2 · Für Fachleute

Modell und Annahmen

Dieser Teil ist eigenständig lesbar. Es geht um Zufallsformeln von 3-SAT und darum, wie viele Knoten eine einfache vollständige Suche braucht, um sie zu entscheiden.

  • Formel: Eine 3-KNF-Formel \(F\) über den Variablen \(x_1, \dots, x_n\) hat \(m\) Klauseln. Jede Klausel ist die Oder-Verknüpfung dreier Literale (eine Variable oder ihre Verneinung) über drei verschiedene Variablen mit zufälligem Vorzeichen. Das Verhältnis \(\alpha = m/n\) steuert die Schwierigkeit. \(F\) ist erfüllbar, wenn eine Belegung jede Klausel wahr macht. Die Formeln kommen aus einem eigenen Zufallsgenerator (SplitMix64) und sind deshalb auf jeder Plattform dieselben. Bei gleichem Zufallsstrom und wachsendem \(m\) kommen Klauseln hinzu, die früheren bleiben. Eine erfüllbare Formel kann dadurch unerfüllbar werden, nie umgekehrt: Der Anteil erfüllbarer Formeln einer festen Menge ist in \(m\) nicht steigend.
  • Suche (DPLL): Die Suche vereinfacht die Formel unter der bisherigen Teilbelegung: Erfüllte Klauseln fallen weg, falsche Literale werden gestrichen. Eine Klausel mit nur noch einem offenen Literal erzwingt es (Einheitspropagation, abschaltbar). Eine leere Klausel ist ein Widerspruch (Sackgasse), keine Klausel mehr heißt gelöst. Sonst verzweigt die Suche auf einer Variablen und probiert zuerst wahr, dann falsch. Drei Verzweigungsregeln: die erste Variable (kleinste Nummer unter den noch offenen), die häufigste Variable (meiste Vorkommen in den offenen Klauseln) und Jeroslow–Wang (siehe Formeln; zuerst das schwerere Vorzeichen). Bei Gleichstand entscheidet die kleinere Variablennummer, die Suche ist deterministisch.
  • Aufwand: Gezählt wird der Knoten, ein Aufruf der Suche. Einheitsschritte, Verzweigungen und Sackgassen werden einzeln ausgewiesen. Ein Knotenbudget bricht die Suche ab; abgebrochene Läufe zählen mit dem Budget und sind damit untere Schranken. Die Knotenzahl misst die Größe des Suchbaums, nicht die Laufzeit: Ein Knoten kostet je nach Formelgröße verschieden viel.
  • Messreihen: Eine Zelle ist eine Kombination aus Größe \(n\) und Verhältnis \(\alpha\); je Zelle gibt es feste Formeln, dieselben über alle Verhältnisse. Jede Messreihe hat ihre eigene Formelmenge, Zahlen verschiedener Tabellen sind daher nicht direkt vergleichbar (etwa Median 31 bei \(n = 30\), \(\alpha = 4,5\) im Wachstum gegen 29 bei der Umbenennung). Phasenübergang: \(n\) = 20, 30, 40, \(\alpha\) von 3,00 bis 6,00 (Schrittweite ein Viertel), je 40 Formeln, Einheitspropagation an, häufigste Variable. Wachstum: \(\alpha = 4,5\), \(n\) = 20 bis 70, je 20 Formeln, dieselbe Suche. Löser-Vergleich: \(n = 30\), \(m = 128\) (\(\alpha \approx 4,27\)), 20 Formeln, Budget 10.000, alle sechs Varianten (Einheitspropagation an oder aus, drei Regeln). Störung: 10 feste Störungen je Wert.
  • Struktur und Störung: Die Schubfach-Formel hat \(h+1\) Tauben und \(h\) Fächer. Jede Taube sitzt in einem Fach (Klausel der Länge \(h\)), kein Fach trägt zwei Tauben (Klauseln der Länge 2). Sie ist unerfüllbar und keine 3-KNF. Störung: Jedes Literal wird unabhängig mit Wahrscheinlichkeit \(p\) umgedreht, \(\ell \mapsto \neg\ell\). Das ändert die Formel und oft ihre Antwort, es ist keine Glättung desselben Problems. Eine zufällige Umbenennung der Variablen ändert die Antwort nie; bei der gemessenen Regel „häufigste Variable“ ändert sie die Knotenzahl nur über die Auflösung von Gleichständen.

Die Formeln

Suche. \(F[x \mapsto b]\) ist \(F\) mit \(x\) auf \(b\) gesetzt und vereinfacht. Die Einheitspropagation steckt in der Vereinfachung:

\[\operatorname{DPLL}(F) = \begin{cases} \text{falsch} & \text{wenn } F \text{ eine leere Klausel enthält} \\ \text{wahr} & \text{wenn } F \text{ keine Klausel enthält} \\ \operatorname{DPLL}(F[x \mapsto 1]) \vee \operatorname{DPLL}(F[x \mapsto 0]) & \text{sonst (Verzweigung auf } x\text{)} \end{cases}\]

Jeroslow–Wang. \(C \ni \ell\) heißt: \(\ell\) kommt in der (offenen, vereinfachten) Klausel \(C\) der Länge \(|C|\) vor. Jedes Vorkommen zählt \(2^{-|C|}\), kurze Klauseln zählen also mehr. Gewählt wird die Variable mit dem größten Gesamtgewicht beider Vorzeichen, zuerst mit dem schwereren Vorzeichen:

\[J(\ell) = \sum_{C \ni \ell} 2^{-|C|}, \qquad x^\ast = \arg\max_x \big( J(x) + J(\neg x) \big)\]

Das Verhältnis \(\alpha = m/n\) und die Störung \(\ell \mapsto \neg\ell\) mit Wahrscheinlichkeit \(p\) je Literal stehen oben im Modell.

Herleitung Schritt für Schritt

Zwei Überlegungen erklären Größen der Messung. Beide sind Rechnung dieser Seite, keine Messung der Demo.

  • Schritt 1, warum viele Klauseln unerfüllbar machen: Eine feste Belegung verletzt eine zufällige Klausel mit Wahrscheinlichkeit \(1/8\): Von den acht Vorzeichenmustern auf den drei Variablen ist genau eins falsch. Die Klauseln sind unabhängig gezogen, also erfüllt eine feste Belegung alle \(m\) mit Wahrscheinlichkeit \((7/8)^m\).
  • Schritt 2, erwartete Zahl erfüllender Belegungen: Es gibt \(2^n\) Belegungen, also im Mittel \(E = 2^n (7/8)^m = \big(2\,(7/8)^{\alpha}\big)^n\) erfüllende. Die Wahrscheinlichkeit, erfüllbar zu sein, ist höchstens \(E\). Es gilt \(E < 1\) genau für \(\alpha > \ln 2/\ln(8/7)\), also etwas über fünf. Darüber fällt die Obergrenze für den Anteil erfüllbarer Formeln mit \(n\) exponentiell.
  • Schritt 3, Einordnung: Das ist nur eine Obergrenze. Sie liegt über allen gemessenen 50-%-Schnitten und über der Vorhersage 4,27. Bei \(n = 20\) und \(\alpha = 6\) beträgt sie gut ein Zehntel, der gemessene Anteil ist kleiner. Die Rechnung erklärt also das Verschwinden erfüllbarer Formeln bei großem \(\alpha\), nicht die Lage des Übergangs.
  • Schritt 4, Bilanz der Knoten: Jeder Knoten ist eine Verzweigung, eine Sackgasse, ein gelöster Knoten oder der Knoten, an dem das Budget überschritten wird. Eine unerfüllbare Formel wird vollständig durchsucht: Jede Verzweigung ruft zwei Kinder auf, jede Sackgasse ist ein Blatt. Also gilt Sackgassen = Verzweigungen + 1 und Knoten = 2 · Verzweigungen + 1. Bei einer erfüllbaren Formel kommt der gelöste Knoten hinzu, bei einem Abbruch der Abbruchknoten: Knoten = Verzweigungen + Sackgassen + 1.
  • Schritt 5, mittlerer Wachstumsfaktor: Von \(n = 20\) bis \(n = 70\) steigt der Median von 14 auf 317 Knoten. Der Faktor je zehn zusätzliche Variablen ist \((317/14)^{10/50}\), etwa 1,9.

Durchgerechnet: eine einzelne Formel

Die Voreinstellung der Demo ist eine Einzelinstanz: \(n = 20\), \(m = 90\) (\(\alpha = 4,5\)), Einheitspropagation an, häufigste Variable. Sie ist erfüllbar und braucht 14 Knoten: 66 Einheitsschritte, 7 Verzweigungen, 6 Sackgassen. Die Bilanz aus Schritt 4 geht auf: \(7 + 6 + 1 = 14\) (Rechnung dieser Seite). Sie geht auch bei den übrigen Einzelinstanzen der Demo auf, einschließlich der unerfüllbaren; deren Zerlegungen sind hier nicht wiedergegeben. Eine Einzelinstanz ist kein Mittel und sagt nichts über die Streuung.

Befunde

Alle Zahlen sind Messungen der Demo und gelten nur für die genannte Voraussetzung. Die Formelmengen sind fest und stammen aus dem eigenen Generator. „Nachprüfung“ bezeichnet eine unabhängige Wiederholung der Entwicklung mit anderen Formelmengen; sie gehört nicht zu den automatischen Prüfungen der Demo. „Median“ heißt Median über die Formeln der Zelle, erfüllbare und unerfüllbare gemischt; der Aufwand ist in Knoten gemessen. Ein großer Prüflauf der Entwicklung verglich alle sechs Suchvarianten mit dem Durchprobieren aller Belegungen (420 Formeln, 2.520 Läufe, erfüllbare und unerfüllbare Formeln) und fand 0 Abweichungen.

Wo kippt die Erfüllbarkeit, wo ist die Suche am teuersten? Je Zelle 40 Formeln, Einheitspropagation an, häufigste Variable. Der Anteil erfüllbarer Formeln fällt von 100 % bei \(\alpha = 3,00\) auf die Werte der Tabelle bei 6,00; bei \(n = 20\) sind schon ab 3,25 höchstens 39 von 40 erfüllbar. Der 50-%-Schnitt ist das \(\alpha\), bei dem der Anteil erfüllbarer Formeln durch 50 % fällt, linear zwischen den Messpunkten interpoliert.

\(n\)erfüllbar bei \(\alpha = 3,00\)erfüllbar bei \(\alpha = 6,00\)50-%-Schnitt bei \(\alpha\)teuerste Suche bei \(\alpha\) (Median, Knoten)Median bei 3,00Median bei 6,00
2040 von 405 %4,675,00 (15)815
3040 von 400 %4,504,75 (30)1221
4040 von 402,5 %4,524,75 (52,5)1334

Die Spitze des Medians ist flach und breit: Mit anderen Formelmengen lag sie bei diesen \(n\) zwischen \(\alpha = 4,5\) und 5,25 (Nachprüfung). Bei \(n = 40\) ist die Suche bei 6,00 um etwa ein Drittel billiger als an der Spitze, aber nicht so billig wie bei 3,00. Bei \(n = 20\) ist der Median bei 6,00 so hoch wie an der Spitze (Rechnung dieser Seite aus der Tabelle). Der Schnitt hängt von der Formelmenge ab: Eine Vormessung mit anderen Formeln ergab 4,39 bis 4,50, die festen Formeln dieser Messung 4,50 bis 4,67. Er streut bei 40 Formeln um etwa ±0,1 bis ±0,15 (bei \(n = 20\) am stärksten) und ist eine Messung, kein Wert. Alle drei Schnitte liegen über der Vorhersage 4,27 (aus der Literatur für sehr große \(n\), bei \(k = 3\) nicht bewiesen); ein Trend zu ihr ist bei diesen kleinen \(n\) nicht erkennbar.

Wie wächst die Suche? \(\alpha = 4,5\), je 20 Formeln, Einheitspropagation an, häufigste Variable. Spalte „erfüllbar“: Zahl erfüllbarer Formeln von 20.

\(n\)Median (Knoten)Maximumerfüllbar
20143314
3031556
40488210
50842016
601433299
703176073

Das ist das 23-Fache des Medians für das 3,5-Fache an Variablen, im Mittel ×1,9 je zehn zusätzliche Variablen. Mit anderen Formelmengen waren es etwa das 17- bis 23-Fache und ×1,8 bis ×1,9 (Nachprüfung). Der Median mischt erfüllbare und unerfüllbare Formeln, deren Anteil mit \(n\) sinkt. Das ist ein exponentieller Trend über sechs Größen, kein Beweis; die Maxima streuen stark (bei \(n = 50\) Maximum 201 bei Median 84).

Was leistet ein Löser? \(n = 30\), \(m = 128\), 20 Formeln, Budget 10.000. Median der Knoten, in Klammern die Zahl der Abbrüche von 20:

Einheitspropagationerste Variablehäufigste VariableJeroslow–Wang
an66 (0)19,5 (0)13 (0)
aus10.001 (18)2.859 (1)291 (0)

Der Faktor der Einheitspropagation ist bei der Regel „erste Variable“ über 150 (untere Schranke, denn 18 von 20 Läufen erreichen das Budget) und bei Jeroslow–Wang 22; als Größenordnung mindestens 20 bis 150, je nach Regel. Einzelne Mediane weichen mit anderen Formelmengen bis etwa um den Faktor 2 ab (Nachprüfung). Mit Einheitspropagation wirkt die Verzweigungsregel mit Faktor 5,1 (66 gegen 13), ohne sie mindestens mit Faktor 34 (10.001 gegen 291).

Struktur gegen Zufall. Schubfach-Formeln sind unerfüllbar; je \(h\) gibt es eine Formel, angegeben ist ihre Knotenzahl. Bei der Zufallsformel (\(n = 30\), \(m = 150\)) ist es der Median über 10 feste Formeln; sie hat etwa so viele Klauseln wie die Schubfach-Formel mit \(h = 6\), aber weniger Variablen.

FormelKnoten
Schubfach \(h = 3\)11
Schubfach \(h = 4\)47
Schubfach \(h = 5\)239
Schubfach \(h = 6\)1.439
Zufallsformel mittlerer Größe26

Der Faktor je zusätzliches Fach wächst von gut vier über gut fünf auf sechs (Rechnung dieser Seite aus der Tabelle). Das ist nur die Knotenzahl dieser Suche; eine Aussage über andere Verfahren folgt daraus nicht.

Hilft die Störung? Ja, aber sie ändert die Antwort. Median der Knoten (in Klammern: erfüllbare von 10 gestörten Formeln) bei Anteil \(p\) umgedrehter Literale, 10 feste Störungen je Wert:

\(p\)\(h = 5\)\(h = 6\)
0 % (ungestört)239 (unerfüllbar)1.439 (unerfüllbar)
0,5 %200 (5)198 (10)
1 %16,5 (10)7 (10)
2 %5 (10)6,5 (10)
5 %5 (10)8 (10)
10 %8 (10)14 (10)
20 %8,5 (5)11 (0)
50 %3 (0)3 (0)

Die Zeile 0,5 % ist ein Sonderfall der kleinen Stichprobe: Bei \(h = 5\) war in 5 der 10 festen Störungen kein Literal umgedreht, diese Formeln sind das unerfüllbare Original; die anderen 5 waren erfüllbar. Der Median 200 liegt deshalb zwischen einer erfüllbaren Formel und dem Original. Die Wahrscheinlichkeit, dass bei Anteil \(p\) und \(L\) Literalen keines umgedreht wird, ist \((1-p)^L\); bei 0,5 % ist sie bei \(h = 5\) gut zwei Fünftel, bei \(h = 6\) knapp ein Viertel (Rechnung dieser Seite). Bei \(h = 6\) hatte jede der 10 Störungen mindestens eine Umdrehung, und der Median fiel dort von 1.439 auf 198. Schon bei 1 % sind in dieser Messung alle gestörten Formeln erfüllbar und im Median in 16,5 (\(h = 5\)) bzw. 7 (\(h = 6\)) Knoten gelöst. Bei anderen Störungen bleibt ein Teil (\(h = 5\): etwa 17 von 100, Nachprüfung) unerfüllbar. Das sind im Wesentlichen die Störungen, bei denen zufällig kein Literal umgedreht wurde, also das unveränderte Original: Bei 1 % ist diese Wahrscheinlichkeit für \(h = 5\) etwa ein Sechstel (Rechnung dieser Seite). In einer eigenen Stichprobe von mehreren hundert Störungen war jede mit mindestens einer Umdrehung bis auf einen Fall erfüllbar (Rechnung dieser Seite, Voraussetzung \(h = 5\), 1 % und 0,5 %). Bei hohem Anteil wird die Formel wieder unerfüllbar, aber zufallsähnlich und leicht. Eine zufällige Umbenennung der Variablen änderte die Antwort nie (0 Abweichungen), die Knotenzahl aber bei 7 von 10 Formeln (\(n = 30\), \(\alpha = 4,5\), 10 Formeln, Regel häufigste Variable); der Median blieb 29.

Einzelinstanzen (je eine feste Formel, kein Mittel; Einheitspropagation an, häufigste Variable, sofern nicht anders genannt):

InstanzErgebnisKnoten
\(n = 6\), \(m = 14\)erfüllbar3
\(n = 20\), \(m = 90\)erfüllbar14
\(n = 30\), \(m = 90\) (\(\alpha = 3\))erfüllbar8
\(n = 40\), \(m = 180\)erfüllbar42
\(n = 40\), \(m = 240\) (\(\alpha = 6\))unerfüllbar25
\(n = 30\), \(m = 128\), ohne Einheitspropagation, erste VariableAbbruch10.001

Grenzen: was die Messung zeigt und was nicht

  • Instanzfamilie und Größe: Die Aussagen zu Phasenübergang und Wachstum gelten für diese Zufallsformeln, diese einfache Suche und \(n\) bis 70. Sie sagen nichts über Industrieformeln und nichts über \(n \to \infty\).
  • Die Vorhersage 4,27: Für \(k = 3\) ist sie nicht bewiesen. Für \(k \ge 3\) ist die Erfüllbarkeitsschwelle von Zufalls-\(k\)-SAT nur für große \(k\) bewiesen. Die Demo misst endliches \(n\) und nennt 4,27 nur zur Einordnung; die gemessenen 50-%-Schnitte liegen bei diesen \(n\) darüber.
  • Der exponentielle Trend: Er ist kein Beweis und gilt nur für \(n\) bis 70. Es sind sechs Größen mit je 20 Formeln, die Maxima streuen stark; eine asymptotische Rate bestimmt die Messung nicht.
  • Der Median mischt: Er enthält erfüllbare und unerfüllbare Formeln und sagt über eine der beiden Gruppen allein nichts. Bei \(n = 20\) fällt der Median bei 6,00 nicht unter die Spitze (siehe Tabelle).
  • Der Löser-Vergleich: Sie läuft mit Budget 10.000 an einer Größe und an 20 Formeln. Abgebrochene Läufe zählen mit dem Budget, die Faktoren der Einheitspropagation sind daher untere Schranken. Eine Vormessung mit Budget 200.000 und 30 Formeln ergab Faktoren von rund 26 bis 1.000.
  • Die Störung ist keine Glättung: Das Umdrehen von Vorzeichen ändert die Formel und oft ihre Antwort. Glättung (geglättete Analyse) heißt: Man betrachtet den Aufwand für leicht zufällig gestörte Eingaben statt für die schlimmste. Beim Simplex-Verfahren ändert die Störung der Daten die Zahl der Pivotschritte, nicht die Antwort; hier ändert sie die Erfüllbarkeit. Die Messung zeigt, dass kleine Störungen eine strukturell harte Formel leicht machen, nicht dass dieselbe Instanz „im Mittel leicht“ wäre.
  • Ein einfaches DPLL steht nicht für „den Löser“: Moderne SAT-Löser lernen aus Widersprüchen (Klausellernen). Eine Probe mit einem solchen Löser (OR-Tools CP-SAT) zeigte, dass auch er auf Zufallsformeln am Übergang mit \(n\) mehr Konflikte braucht; die Zahlen sind plattform- und versionsabhängig und stehen deshalb hier nicht.
  • Schubfach-Formeln: Gemessen sind nur die Knotenzahlen dieser Suche. Dass die Formeln für Verfahren, die auf Resolution beruhen, exponentiell schwer sind (Haken 1985), wurde nicht nachgeschlagen und ist keine Aussage dieser Seite.

Erweiterungen und Verweise

Nicht gebaut sind Klausellernen (CDCL) und Industrieformeln, die lokale Suche für SAT (etwa WalkSAT, ein anderes Verfahren mit anderen Stärken), eine Glättung, die die Antwort erhält (die Umbenennung der Variablen erhält sie, ändert bei der gemessenen Regel aber nur die Auflösung von Gleichständen), und Größen über \(n = 70\). Verweise (Angaben nach der Beschreibung der jeweiligen Demo):

  • Störung bei Simplex: Die klee-minty-demo zeigt, dass bei Simplex Rauschen in den Daten die Pivotzahl ändert (Median über 20 Störungen) und wie das von der Art der Störung abhängt.
  • Von der Formel zum Graphen: Die reduktionskette-demo übersetzt Formeln in Graphprobleme. Dort wird die Formel selbst in wenigen DPLL-Knoten entschieden, während Graphlöser am Budget scheitern; diese Demo fragt nach dem Grund.

Quellen

  • Davis, M., Logemann, G., & Loveland, D. (1962): A machine program for theorem-proving. Communications of the ACM 5, 394–397.
  • Cheeseman, P., Kanefsky, B., & Taylor, W. M. (1991): Where the really hard problems are. IJCAI 1991.
  • Mitchell, D., Selman, B., & Levesque, H. (1992): Hard and easy distributions of SAT problems. AAAI 1992, 459–465.
  • Jeroslow, R. G., & Wang, J. (1990): Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1, 167–187.
  • Ding, J., Sly, A., & Sun, N. (2022): Proof of the satisfiability conjecture for large k. Annals of Mathematics 196.
  • Spielman, D. A., & Teng, S.-H. (2001): geglättete Analyse des Simplex-Verfahrens, STOC 2001; Englert, M., Röglin, H., & Vöcking, B. (2016): geglättete Analyse von 2-opt, ACM Transactions on Algorithms.
  • Quelltext, Messreihen und Tests der Demo: github.com/sebastian-hanisch/sat-phasenuebergang-demo.

Die Angaben zu den ersten fünf Quellen stammen aus der Quellenliste der Demo, dort anhand der Quellen geprüft; bei Cheeseman et al. fehlen die Seiten, weil sie in den Quellen uneinheitlich sind. Bei Jeroslow und Wang beruht die Angabe nur auf einer Bibliographie, der Inhalt wurde nicht eingesehen. Die beiden Arbeiten zur geglätteten Analyse sind nur mit Autoren, Jahr und Gegenstand genannt, nicht nachgeschlagen.