Drei Stellen, an denen der Bestand gegen sich selbst steht — und ein Hebel, der weiter trägt als jeder andere und trotzdem stirbt.
Die polynomiale Schicht dieses Projekts ist die breitenbeschränkte Resolution: man leitet alles ab, was sich ableiten lässt, wirft aber jede Klausel weg, die breiter als w ist. Für festes w gibt es nur O(n^w) davon, das Verfahren ist also polynomial. Die Frage ist immer dieselbe — wie weit trägt es?
Zwei Dokumente des Bestands antworten verschieden, und der Widerspruch hat eine strategische Folge.
Das andere misst dieselbe Frage direkt, an 330 Instanzen über elf Werte von n, auf zwei methodisch unabhängigen Wegen, die übereinstimmen:
| Ebene | n₅₀ | Übergangsbreite |
|---|---|---|
| Breite 3 | 52,9 | 18,4 in n |
| Breite 4 | 108,2 | 12,3 in n |
Breite 4 trägt gut doppelt so weit. Das ist keine kleine Verschiebung, sondern der grösste im ganzen Bestand gemessene Hebel — mehr als die erweiterte Resolution mit Faktor 1,35.
Warum das Dichteargument scheitert, steht in demselben Dokument, das es aufstellt: die naheliegende Verfeinerung, der Verzweigungsfaktor λ als Schwelle, wird dort geprüft und verworfen — eine Instanz mit λ > 1 stirbt, eine mit λ < 1 zündet. Ist der Rundenfaktor keine Schwelle, ist die statische Dichte erst recht keine.
Aus denselben beiden Zahlen zieht der Bestand eine Gerade, w*(n) ≈ 0,018·n. Dieselben zwei Punkte tragen aber auch ein geometrisches Gesetz, und das Verhältnis 108,2 / 52,9 = 2,05 ist auffällig nahe an 2.
| Gesetz | sagt n₅₀(5) | und über w* |
|---|---|---|
| linear | 163 | w* = Θ(n) schon im Messfenster |
| geometrisch | 222 | w* = Θ(log n) im Messfenster |
Die beiden liegen 36 % auseinander und sind mit einem Messpunkt zu trennen. Der Unterschied ist nicht kosmetisch: geometrisch hiesse, dass im ganzen messbaren Bereich Beweise der Grösse n^O(log n) genügen — quasipolynomial statt exponentiell. Asymptotisch muss w* linear werden; wo der Übergang liegt, ist nie gefragt worden.
Der Bestand hält Breite 5 für unerreichbar, weil ihr Raum bei n = 55 schon 10⁸ Klauseln hat. Das ist der Vorrat, nicht der Abschluss. Derselbe Text misst an anderer Stelle, dass der widerlegende Breite-4-Abschluss kubisch bleibt, während sein Raum quartisch wächst.
Hier ist dieselbe Messung noch einmal, mit Hilfsstellen und über fünf Stützpunkte:
Ein früherer Bericht schliesst, zufälliges 3-SAT habe keine der beiden Ressourcen, die kurze Beweise tragen: keinen kleinen Abschlussraum und keine Symmetrie. Die Automorphismengruppe ist bis n = 400 beweisbar trivial.
Der naheliegende Einwand ist, dass ein Beweis auch über eine Näherungssymmetrie heben könnte und nur die Naht bezahlt. Der Bestand nimmt ihn ernst, baut das Mass dafür, prüft es an einer Positivkontrolle — und stellt die Frage, ob die Grösse Θ(1) oder Θ(n) ist. Dann steht dort: läuft.
Der Lauf ist durchgelaufen. Seine Ausgabe lag neun Tage unausgewertet auf der Platte.
| n | 100 | 150 | 200 | 300 | 400 |
|---|---|---|---|---|---|
| nutzen | 60 | 77 | 101 | 138 | 177 |
| nutzen / n | 0,600 | 0,513 | 0,505 | 0,460 | 0,442 |
Θ(1) ist ausgeschlossen. Es verlangte, dass nutzen/n von n = 100 auf 400 um Faktor 4 fällt; gemessen ist Faktor 1,36. Und der Ausschluss trägt trotz dünner Datenlage, weil alle Werte untere Schranken sind: eine untere Schranke, die schneller als jede Konstante wächst, schliesst Θ(1) aus, gleichgültig wie schlecht die Suche war.
Erweiterte Resolution darf eine neue Variable erfinden. Eine Definition
schränkt die alten Variablen um nichts ein — z ist bestimmt, nicht eingeschränkt — und alle drei Klauseln passen in die Ebene 3. Das ist die einzige Richtung, die die Variablenmenge verlässt, und deshalb die einzige, die das eigene Abzählargument des Projekts nicht erreichen kann. Für sie ist für keine Formelfamilie eine untere Schranke bekannt.
Die stehende Auskunft lautet trotzdem: es gibt kein Verfahren, nützliche Extensionsvariablen zu finden. Das etablierte Verfahren dafür sucht wiederkehrende Struktur zum Herausfaktorisieren und findet auf Zufallsinstanzen genau null — was kein Wunder ist, denn dort steht nichts mehrfach da.
Die Definition liefert zwei Zweierklauseln. Eine davon verschmilzt mit jeder Klausel C, die ¬la enthält, zu einer Klausel der Breite 3 über z. Zwei solche Nachkommen verschmelzen wieder in die Ebene, wenn ihre Reste sich eine Stelle teilen. Das sind die neuen Zündpunkte, und sie sind vor jeder Rechnung abzählbar:
Gemessen an genau den Instanzen, bei denen die Ebene 3 ohne Hilfsstellen versagt — und zwar bewiesen versagt, denn die Kappe liegt über dem Vorrat. Bei identischer Klausel- und Variablenzahl unterscheidet die Läufe nichts als die Wahl der Paare.
| Vergleich, k = n Definitionen | gezielt | Vergleich |
|---|---|---|
| gegen zufällige Variablenpaare, n = 88 | 13/20 | 0/23 |
| gegen zufällige Literalpaare, n = 88 | 5/9 | 0/9 |
| gegen verteilte statt konzentrierte Wahl, n = 80 | 6/6 | 0/6 |
| gegen Anti-Auswahl, n = 64 (k = n/2) | 13/14 | 0/14 |
Die dritte Zeile war eine Verfeinerung, die besser sein sollte und fällt — sie schärft den Mechanismus: die Definitionen müssen einen Knoten bauen, kein Netz. Die vierte ist die zweite Seite der Kontrolle: die Anti-Regel ist schlechter als der Zufall, nicht nur besser als nichts.
Als Kurve über n, mit k = n Definitionen:
Je Kosteneinheit ist das der beste Hebel des Bestands. Die Breite kostet einen Faktor n/2 und bringt 2,05; die gezielten Definitionen kosten einen festen Faktor 8 und bringen 1,72.
Ob das mehr ist als ein weiterer Hebel, entscheidet die Zahl der Definitionen, die bei Grösse n nötig ist. Die Kosten sind O((n+k)³) — für jedes polynomiale k* bliebe das Verfahren polynomial. Gemessen wird das als Budgetantwort, über zwei vollständige Kurven.
Damit steht der Befund vollständig, und er ist zweiseitig. Die Auswahl der Definitionen ist ein echter, grosser, mechanistisch verstandener und in beide Richtungen kontrollierter Effekt. Und sie ist trotzdem kein Ausweg: der Preis wächst exponentiell, wie bei jedem anderen Hebel.
Die unwahrscheinliche Lesart wäre bemerkenswert gewesen, denn für erweiterte Resolution verbietet kein Satz eine polynomiale Widerlegung zufälliger 3-CNF. Sie ist jetzt gemessen und trifft nicht zu — jedenfalls nicht für diese Auswahlregel in diesem Fenster.