Was genau unterscheidet aussagenlogische Formeln, die sich in Polynomialzeit entscheiden lassen, von zufälligem 3-SAT? Dieser Text fasst zusammen, was dazu gemessen, was hergeleitet und was offen ist — vollständig genug, um ohne Vorgeschichte gelesen zu werden.
Vier Familien unerfüllbarer Formeln lassen sich in Polynomialzeit widerlegen: Horn, 2-SAT, Tseitin (Paritätsgleichungen über GF(2)) und der Taubenschlag. Zufälliges 3-SAT an der Schwelle α ≈ 4,27 nicht. Was fehlt ihm?
Neun Kandidatenkriterien wurden geprüft und alle verworfen — Kerngrösse, Rissordnung, Zirkularität, Lokalität, Verzweigungsgrad, Klauselbreite, Komprimierbarkeit, Horn-Nähe, Backdoors. Sie scheitern alle an demselben Gegenbeispielpaar, und der Grund dafür ist strukturell: die massgebliche Grösse ist stetig, und die Kosten hängen exponentiell von ihr ab. Ein Ja/Nein-Kriterium kann das nicht darstellen.
Ordnung d\*. Die Anzahl Literale, die festgehalten werden muss, bevor Einheitspropagation ohne weitere Entscheidung in einen Widerspruch läuft.
2-Klauseln und Horn-Klauseln erzwingen; eine allgemeine 3-Klausel lässt eine Wahl und erzwingt nichts. Die Ordnung misst, wie weit man raten muss, bis die Propagation wieder greift.
| Familie | Ordnung d_zert | entspricht |
|---|---|---|
| Horn-3-SAT | 0 | Propagation allein genügt |
| 2-SAT | 1 | genau dem Kriterium von Aspvall/Plass/Tarjan |
| zufälliges 3-SAT | 0,13·n + 3 | — gemessen · Code & Daten |
| Taubenschlag | 0,909·n − 7,2 | r = 1,000 |
Satz. Gibt es eine Variablenmenge V mit |V| = d, so dass alle 2^d Belegungen von V unter Einheitspropagation in den Widerspruch laufen, so ist F unerfüllbar; und umgekehrt existiert ein solches V für jede unerfüllbare Formel. bewiesen Damit ist die Ordnung ein korrektes und vollständiges Zertifikat, prüfbar mit 2^d Propagationsläufen — ohne dem Solver etwas glauben zu müssen. Und es liefert einen ausführbaren Resolutionsbeweis: die Konfliktanalyse jeder Belegung, rückwärts durch die Begründungen resolviert, ergibt eine Klausel nur über V.
Alle vier lösen nicht durch Suche, sondern durch Sättigung: eine Schlussregel anwenden bis zum Fixpunkt, Ergebnis ablesen. Das läuft in P, weil der Abschluss in einem Raum polynomialer Grösse lebt.
| Familie | Abschlussraum | Grösse | für Zufalls-3-SAT |
|---|---|---|---|
| Horn | Literale | ≤ 2n | leer |
| 2-SAT | Binärklauseln | ≤ 4n² | leer |
| Tseitin | Linearformen über GF(2) | Rang ≤ n | Grad Ω(n) bewiesen |
| Taubenschlag | Ungleichungen (LP) | polynomial | identisch mit Propagation |
| — | k-DNFs, Res(k) | n^O(k) | exponentiell bewiesen (Alekhnovich 2005) |
| — | Klauseln der Breite ≤ w | O(n^w) | trägt bis n ≈ 53 (w=3) bzw. 108 (w=4) |
Zwei 3-Klauseln resolvieren zu einer 4-Klausel — die Klasse ist unter ihrer eigenen Regel nicht abgeschlossen. Erzwingt man den Abschluss durch eine Breitenschranke w, so ist das für festes w ein echtes Polynomialzeitverfahren, denn es gibt nur O(n^w) Klauseln der Breite ≤ w. Genau dieses Verfahren ist das Messobjekt der folgenden Abschnitte.
Dies war eine Korrektur an einem früheren Befund: die Zahl 0,2125·n + 4,09, die als „Beweisbreite" gemeldet worden war, misst w_zert. Der wahre Wert w* ist 3, der kleinstmögliche für eine 3-CNF. Eine unabhängige Neuimplementierung in Rust bestätigt w* exakt (2-SAT → 2, Taubenschlag → 2/3/4), reproduziert aber d_zert und w_zert nicht — die eine Grösse ist eine Eigenschaft der Formel, die anderen sind Eigenschaften der Konstruktion.
Die beiden Halbwertspunkte sind zwei Stützpunkte der Umkehrfunktion von w*(n):
w*(n) ≈ 3 + (n − 52,9) / 54,6 ≈ 0,0183 · n gemessen
Ben-Sasson und Wigderson haben bewiesen, dass w* für zufälliges 3-SAT linear in n wachsen muss; die Konstante steckt bei ihnen im Ω-Zeichen. Dies ist ihr gemessener Wert. Und daraus folgt zugleich, warum das polynomiale Verfahren nicht zu retten ist: n^O(w*) mit w* = 0,018·n ist n^(0,018n), also exponentiell.
Die p₄-Kurve wurde mit einer Abkürzung gemessen: weil der Abschluss bimodal ist (Abschnitt 06), muss man ihn nicht zu Ende rechnen, sondern nur feststellen, auf welcher Seite der Separatrix eine Instanz startet — 480-mal billiger. Dieser Schätzer wurde nicht an p₄ angepasst, sondern aus der Rückkopplung hergeleitet, und sagte n₅₀(4) = 108,2 vorher. Die parallel weiterlaufende Vollrechnung ist inzwischen an allen elf Stützpunkten konvergiert und ergibt 107,5 ± 1,1.
Das ist die schärfste Bestätigung des Mechanismus in diesem Text: eine aus ihm hergeleitete Vorhersage, unabhängig nachgerechnet.
Der Übergang wandert ausserdem mit der Dichte, n₅₀ = 16,5·α − 18,0 (r = 0,9976 über vier Dichten). Mehr Klauseln verlängern also die Gültigkeit des polynomialen Verfahrens — dichtere Instanzen sind leichter, und hier heisst leichter, dass die Zündung länger trägt.
Der Grund ist eine Rückkopplung. Ein Resolvent der Breite ≤ 3 entsteht nur, wenn zwei Klauseln ausser dem Drehliteral noch ein Literal teilen — je voller der Abschluss, desto mehr Partner findet jede neue Klausel. Die Reproduktionszahl R hängt also vom bereits Angesammelten ab, und das System ist autokatalytisch.
Rohstoff E[P2] = C(m,2)·3(n−3)/C(n,3) = 164 konstant in n Ertrag was eine Instanz ansammelt ≈ 500 konstant in n Bedarf |A|*(n) = 23,3·n − 649 linear in n
Der Rohstoff sind die Klauselpaare mit genau zwei gemeinsamen Variablen — daraus entstehen die Resolventen der Breite 3. Ihre Erwartungszahl ist geschlossen ausrechenbar und hängt nicht von n ab: die Vorhersage 164 trifft die Messung auf allen sechs Punkten (161–168). Der Ertrag, also was eine verhungernde Instanz tatsächlich zusammenbringt, ist ebenfalls konstant (382–592 über n = 40…90, ohne Trend). Nur der Bedarf wächst.
Was die Formel von selbst zusammenbringt, bleibt gleich. Was sie zum Zünden braucht, wächst. Der Übergang ist die Kreuzung.
Nachtrag, und er korrigiert diesen Abschnitt. Der Impfversuch in Abschnitt 08 hat geprüft, ob eine Instanz zündet, sobald ihr Abschluss |A| *(n) erreicht — und die Antwort ist nein. Mit zufälligen Umwegen lässt sich der Abschluss auf 2466 Klauseln treiben, weit über |A| *(60) = 749, ohne dass irgendetwas zündet. Die Kreuzung beschreibt richtig, warum der Übergang bei n ≈ 50 liegt; sie ist aber keine Schwelle, die man durch Auffüllen überschreitet. Was zählt, steht im nächsten Abschnitt.
Sie liegt bei n = 49,2 — und damit zeigen drei unabhängige Messungen auf denselben Punkt: der Anteil gezündeter Instanzen (52,9), der Nulldurchgang von R bei |A| = 500 (49,6), und diese Kreuzung (49,2).
Es hiess: „Der Suchraum ist nicht zu gross zum Durchsuchen. Er ist zu klein, um den Beweis zu enthalten." Der zweite Satz stimmt so nicht. Das Maximum von R bleibt bis n ≈ 87 über 1 — der selbsttragende Bereich existiert weiter, nur führt kein Weg vom Anfang dorthin. Bei n = 80 fehlen einer Instanz rund 700 Klauseln, und das ist eine lineare Zahl. Bemerkenswert: eine ganz andere Messung dieses Arbeitsstands kam auf dieselbe Gestalt — 0,8 Binärklauseln je Variable lassen die Härte kollabieren.
Bis hierher ist alles Beobachtung. Dieser Abschnitt ist der erste Versuch, der eine Zahl vorher festlegt und sie danebenliegen lässt, wenn sie falsch ist: eine verhungernde Instanz mit k zusätzlichen Klauseln impfen und das kleinste zündende k suchen.
Die heikle Stelle ist, woher die Impfklauseln kommen dürfen. Die Instanz ist unerfüllbar, also ist jede Klausel logisch impliziert — die leere eingeschlossen. „Gültig" wäre damit ein leeres Kriterium, und man könnte den Versuch mit k = 1 gewinnen, indem man ⊥ einsetzt. Das brauchbare Kriterium ist Ableitbarkeit: die Impfklauseln müssen echte Resolutionsschritte sein. Quelle ist der Breite-4-Abschluss, eingeschränkt auf Breite ≤ 3 und abzüglich dessen, was Breite 3 selbst erreicht — genau das, was der stärkere Beweiser hat und der schwächere aufschreiben könnte.
Die Separatrix wuchs klar linear (r = 0,911), aber mit Steigung 16,2 ± 2,0 statt 23,3 — 3,6 σ zu flach. Der Grund ist ein Störfaktor, dessen Richtung vor der Messung feststand: Impfen erhöht die Dichte, dichtere Instanzen sind leichter, und bei grossem n muss mehr geimpft werden. Gemessen steigt α von 4,27 auf 5,24 bei n = 70.
Rechnet man ihn heraus — n_eff = n − 16,5·(α_eff − 4,27) —, fällt etwas heraus,
wonach nicht gesucht wurde:
Gezündet wird nicht, wenn genug Klauseln beisammen sind, sondern wenn die Instanz auf die kritische Linie zurückgeschoben ist. gemessen
n_eff im Zündaugenblick, abgeleitete Klauseln, n ≥ 58: 54,0 ± 1,5
n_eff im Zündaugenblick, gewürfelte Klauseln, n = 60…120: 52,8 ± 0,9
gegen n₅₀(3) = 52,9
Daraus folgt ein Gesetz für den Preis, das keine neue Grösse enthält: 52,9 stammt aus der p₃-Kurve, 16,5 aus der Dichtereihe, beide vorher und für andere Zwecke gemessen.
Und ein Nebenergebnis, das für die Deutung schwerer wiegt als der Test selbst: bei n = 70 brauchte die Impfung mit abgeleiteten Klauseln k* = 68, die mit gewürfelten 63,3. Ableitbares Material ist nicht mehr wert als frisch gewürfeltes. Was fehlt, ist keine bestimmte Information — es ist Dichte.
Die naheliegendste Idee, wenn der Raum ungünstig entsteht: ihn anders aufbauen, die konfliktreichsten Klauseln zuerst. Ein Teil der Antwort lässt sich hier ausnahmsweise beweisen statt messen.
Breitenbeschränkte Sättigung ist ein monotoner Abschlussoperator. Ihr Fixpunkt ist eindeutig. Sortieren ändert, wann eine Klausel auftaucht, nicht ob. bewiesen
Das verschärft den Hauptbefund: die fehlende Information bei Breite 3 ist wirklich fehlend, nicht bloss schlecht terminiert. Für die Suche gilt das Umgekehrte — aber es ist ausgeschöpft: VSIDS im CDCL ist „konfliktreichste zuerst", und daher kommt der Faktor 1,9 im Exponenten. Reihenfolge kann keinen Beweis kürzen, der lang sein muss.
Die Eindeutigkeit gilt nur bei fester Breite. Mischt man — Breite 3 plus ein Budget von B Zwischenklauseln der Breite 4 —, ist das Verfahren nicht konfluent, und welche B Umwege man nimmt, entscheidet alles. Der entstehende Beweis bleibt gewöhnliche Resolution, in der alle bis auf B Klauseln die Breite 3 haben; der Raum bleibt O(n³) + B.
| Auswahlmass | was es zählt | Budget bis zur Zündung |
|---|---|---|
| zufall | — | > 150, ausnahmslos |
| ertrag | freigesetzte Klauseln der Breite ≤ 3 | > 150, ausnahmslos |
| frisch | davon nur die noch nicht vorhandenen | 1 … 35 bei n ≤ 55 |
Konfliktreich heisst nicht viel Ertrag, sondern viel neuer Ertrag.
Roher Ertrag verhält sich exakt wie Zufall — die reichsten Klauseln leiten überwiegend
Vorhandenes noch einmal ab. Ein tiefer Lauf über 2000 Runden zeigt drei verschiedene
Misserfolge: Zufall lässt den Abschluss stetig auf 2466 wachsen und zündet nie; ertrag
friert bei 496 ein und bleibt 2000 Runden dort; frisch kommt auf 719 und friert
dann auch.
Es trägt nicht weit: zwischen n = 55 und n = 60 hört es auf. Die Wand verschiebt sich, sie verschwindet nicht. Was bleibt, ist die beste Frage aus diesem Zweig — das benötigte Material ist winzig (1 bis 35 Umwege aus 5 000 bis 29 000 Kandidaten). Es ist da. Nur findet es niemand zuverlässig.
Eine 3-CNF zerfällt in das Gerüst (welche Variablen zusammenstehen) und die Vorzeichen. Für die Erfüllbarkeit ist die Aufteilung bekannt: das Gerüst bestimmt, wie teuer eine Widerlegung ist, die Vorzeichen bestimmen, ob es überhaupt eine gibt. Für die Zündung wurde sie gemessen — ein Gerüst, sechzig Vorzeichenwürfe, 144 Gerüste, 3 456 unerfüllbare Instanzen:
logit p₃ = +5,515 − 0,2772·n + 0,2205·Doppeltripel + 0,05545·Paare2
(9,6σ) (29,7σ) (5,2σ) (15,8σ)
Beides trägt bei, und man kann es trennen. Die Zündrate streut zwischen Gerüsten 2,8- bis 7,3-mal stärker, als die Vorzeichen allein erklären könnten — das Gerüst trägt also. Innerhalb eines festen Gerüsts ist die Rate aber nie 0 und nie 1 — die Vorzeichen tragen auch. In Variablen umgerechnet: ein Doppeltripel wiegt 0,80 Variablen, ein Paar2 wiegt 0,20. Da die Paare2 um ±13 streuen, ist ihr Beitrag der grössere.
Der n-Koeffizient −0,277 dieser Anpassung reproduziert die unabhängig gemessene p₃-Steigung −0,2387 — zwei völlig verschiedene Experimente, dieselbe Grösse.
| System | zufälliges 3-CNF | Quelle |
|---|---|---|
| Resolution | Grösse 2^Ω(n) | Chvátal/Szemerédi 1988 |
| Res(k), k ≤ √(log n/log log n) | exponentiell | Alekhnovich 2005 |
| Polynomkalkül, jeder Körper | Grad Ω(n) | Ben-Sasson/Impagliazzo 1999 |
| Summen von Quadraten | Grad Ω(n) | Grigoriev 2001, Schoenebeck 2008 |
| Rang-1-Schnitte an x = ½ | Verletzung 0 | hier, erschöpfend gerechnet |
| Schnittebenen, k = 3 | offen | Fleming u.a. 2017 nur für k = log n |
| Frege beschränkter Tiefe | offen | nur Ω(n^(1+ε)) Schritte, 2024 |
| Frege, erweitertes Frege | offen | — |
Ein Ergebnis dieser Zusammenstellung hat uns überrascht: zufälliges 3-CNF ist schon bei beschränkter Tiefe offen — dort, wo Taubenschlag und Tseitin seit Jahren erledigt sind. Die beiden Familien, die dieses Projekt als negative Kontrollen führt, sind für die Frege-Hierarchie die verstandenen Fälle.
Am Punkt x = ½ hat eine Klausel der Breite w den Schlupf w/2 − 1. Daraus folgt unmittelbar:
Straffheit bei x = ½ ist dasselbe wie Klauselbreite 2, Verletzung dasselbe wie Breite ≤ 1. bewiesen
Für {0,½}-Multiplikatoren lässt sich der Schlupf eines Chvátal-Gomory-Schnitts geschlossen ausrechnen, und er ist für eine 3-CNF stets ≥ ½ — ausser wenn zwei Klauseln auf demselben Variablentripel liegen. Das ist genau der Zündfunke. Der Schnittebenenweg bei x = ½ ist kein anderer Weg als der Resolutionsweg. Nebenbei fällt daraus die Erwartungszahl der Zündfunken, C(m,2)/C(n,3)·3/8 ≈ 20,5/n — ein Gesetz, das vorher nur angepasst war.
Offen bleibt: das Argument hängt an einem Punkt. Schneidet ein Verfahren anderswo, wandert das Optimum, und über die dortige Straffheitsstruktur wissen wir nichts.
Die Konfliktfolge von CDCL lässt sich als eigenes Messobjekt lesen. Zwei Grössen: die Wiederkehr (kehrt der Solver zu denselben Variablenträgern zurück?) und die Reichweite (wie weit greift ein Konflikt zurück?).
| Familie | kleiner Raum | Symmetrie | Wiederkehr | Zufallslinie |
|---|---|---|---|---|
| Taubenschlag | nein (für Resolution) | ja, maximal | 0,2–0,6 % | 0,00 % |
| Tseitin, Gitter | ja, GF(2) | ja | 49–73 % | 0,07 % |
| Tseitin, 3-regulär | ja, GF(2) | nein | 51–60 % | 0,01 % |
| zufälliges 3-SAT | nein | nein | ~1 % | 0,00 % |
Die dritte Zeile ist der Trennungstest: eine Familie mit kleinem Abschlussraum und ohne Symmetrie. Der Detektor schlägt dort genauso an wie beim symmetrischen Gitter. Er sieht also den Raum, nicht die Symmetrie — und ist damit ein Kandidat für die Aufgabe, einen unbekannten Abschlussraum zu erkennen, bevor man weiss, welcher es ist. Bei Tseitin hat er es getan. Für zufälliges 3-SAT schweigt er.
Ehrliche Grenze: beide positiven Kontrollen sind GF(2)-Familien, und der Taubenschlag mit seinem Zähl-Raum löst nichts aus. „Kein Signal" heisst also nicht „kein Raum", sondern „kein Raum von der Art, die dieses Mass sieht".
Es gibt genau zwei Eigenschaften, von denen wir wissen, dass sie kurze Beweise tragen: ein kleiner Abschlussraum, oder Symmetrie, über die man einen Fall auf alle hebt (so funktioniert Buss' polynomialer Frege-Beweis des Taubenschlags).
| Familie | kleiner Abschlussraum | nichttriviale Bahnen | kurzer Beweis bekannt |
|---|---|---|---|
| Horn, 2-SAT | ja | nein | ja, durch Sättigung |
| Taubenschlag, Tseitin | nein (für Resolution) | ja | ja, Frege bzw. Gauss |
| zufälliges 3-SAT | nein | nein | keiner |
Die Bahnkompression (Farbverfeinerung auf dem Inzidenzgraphen) ist für zufälliges 3-SAT exakt 1,00 bis n = 400 — die Automorphismengruppe ist beweisbar trivial. Für den Taubenschlag liegen alle Variablen in einer Bahn.
Das ist keine untere Schranke: Symmetrie ist nicht notwendig, Horn und 2-SAT haben keine. Es ist die präziseste Beschreibung der Lage, die aus Messungen zu haben ist. Was auffällt: ein kurzer Beweis, der weder einen kleinen Abschlussraum sättigt noch über eine Symmetrie hebt, wurde für keine Familie je konstruiert.
Ausdrücklich nicht belegt, aber aus dem Gemessenen naheliegend:
Drei Regeln, alle aus Fehlern entstanden:
Dazu: ein vollständiger gestufter SAT-Solver in Rust, dessen vier Stufen die vier Verfahren dieses Arbeitsstands sind, mit Testsuite — über 700 Instanzen gegen rohe Gewalt, und die Einstufung der Messinstanzen gegen einen fremden Solver geprüft (170 Instanzen, null Abweichungen).