Das Brett, wie es steht: was bewiesen zu ist, was gemessen zu ist, was offen bleibt — und eine Prüfliste, die untaugliche Ideen in einer halben Minute erledigt, damit die Zeit für die tauglichen bleibt.
Drei Fragen werden leicht verwechselt, und die Verwechslung kostet Wochen.
| Frage | Was zu zeigen wäre | Unser Bezug |
|---|---|---|
| P vs NP | ein polynomialer Algorithmus, oder dass keiner existiert | nicht direkt |
| NP vs coNP | ein Beweissystem mit polynomialen Beweisen für alle Tautologien (Cook/Reckhow) | das ist unser Programm |
| Zufalls-3-SAT | dass diese eine Familie leicht oder schwer ist | unser Messobjekt |
Zwei Konsequenzen, die man sich merken sollte. Erstens: Zufalls-3-SAT ist weder notwendig noch hinreichend für P vs NP. P vs NP ist eine Aussage über den schlimmsten Fall — wären Zufallsinstanzen leicht, folgte P = NP nicht; sind sie schwer, folgt P ≠ NP nicht. Zweitens: sie sind trotzdem die Standard-Prüffamilie des Cook/Reckhow-Programms, und der Weg zu NP ≠ coNP führt über untere Schranken für immer stärkere Systeme.
Wer den grossen Preis will, muss zeigen, dass irgendein System keine kurzen Beweise hat — und die Familie darf man sich aussuchen. Wir haben zufälliges 3-SAT gewählt, weil dort am meisten bekannt ist.
| System | Ergebnis für Zufalls-3-CNF | Quelle |
|---|---|---|
| Resolution | Grösse 2^Ω(n) | Chvátal/Szemerédi 1988 |
| Res(k), k klein | 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 bei x = ½ | Verletzung 0 | hier, erschöpfend gerechnet |
Fünf Abschlussräume, alle leer: Literale · Binärklauseln · Linearformen über GF(2) · LP-Ungleichungen · Klauseln der Breite ≤ w. Dazu keine Symmetrie (Bahnkompression exakt 1,00 bis n = 400) und kein Signal des Wiederkehr-Detektors (~1 % gegen 49–73 % bei Tseitin).
| System | Was fehlt |
|---|---|
| Schnittebenen bei k = 3 | Fleming u.a. 2017 deckt nur k = log n |
| Frege beschränkter Tiefe | nur Ω(n^(1+ε)) Schritte bekannt (2024) |
| Frege, erweitertes Frege | für keine Familie ist eine superpolynomiale Schranke bekannt |
Der letzte Punkt ist keine Lücke unserer Arbeit, sondern die offene Frage der Beweiskomplexität seit vierzig Jahren.
Expansion ist eine GLOBALE Eigenschaft.
Jedes unserer Werkzeuge ist LOKAL:
Variable festlegen → berührt 12,8 Klauseln
Klausel hinzufügen → berührt 1
Resolutionsschritt → berührt 2
Ω(n) lokale Züge für eine globale Eigenschaft — daher sind alle Kosten linear im Exponenten. Nicht-lokale Werkzeuge kennt die Beweiskomplexität drei: Symmetrie (gemessen abwesend), lineare Algebra (bewiesen wirkungslos), Extension (offen).
Für jede neue Idee der Reihe nach durchgehen. Ein Nein heisst nicht „falsch" — es heisst: hier liegt die Beweislast.
Der einzige nicht-lokale Weg, der offensteht. Führe eine frische Variable y ein, mit definierenden Klauseln:
y ↔ (a ∨ b) → (¬y ∨ a ∨ b) , (y ∨ ¬a) , (y ∨ ¬b)
Das ist erfüllbarkeitserhaltend — y ist definiert, nicht eingeschränkt. Man darf beliebig viele solcher Definitionen stapeln.
Extension macht Breitenschranken bedeutungslos — per Konstruktion.
Unser ganzes Härtebild hängt an der Breite: Beweise brauchen breite Klauseln, breite Klauseln kosten. Extension erlaubt, eine breite Tatsache zu benennen und danach mit Breite O(1) weiterzurechnen. Deshalb ist es nicht bloss die letzte Tür — es ist die Tür, die unser eigenes Argument prinzipiell nicht schliessen kann.
Cooks Beweis des Taubenschlags in erweiterter Resolution ist polynomial, wo gewöhnliche Resolution 2^Ω(n) braucht. Das Muster: die Extension kodiert eine Selbstreduktion — man benennt die Instanz des kleineren Problems und führt Induktion.
Finde polynomial viele Definitionen y₁…y_p, so dass die erweiterte Formel kleine geschlossene Klauselmengen hat — also niedrige Expansion im erweiterten Variablenraum.
Denn geschlossene Mengen (∂S = 0) sind genau das, was zufälligen Instanzen fehlt, und ihre Zahl sagt nachweislich die Zündung vorher (p ~ 2·10⁻¹³).
Und jetzt die Falle. Rechne den Rand des Extensionsgadgets selbst aus:
S = { (¬y ∨ a ∨ b) , (y ∨ ¬a) , (y ∨ ¬b) }
Variablen: y (3×), a (2×), b (2×) → ∂S = 0
Das Gadget ist selbst eine geschlossene Menge. Niedrige Expansion lässt sich also beliebig fälschen, ohne dass irgendetwas gewonnen wäre — die Definitionsklauseln sind erfüllbar, aus ihnen folgt nie ein Widerspruch. Zwei Binärklauseln bekommt man gratis dazu, aber sie sind definitorisch, nicht einschränkend.
Geschlossenheit ist notwendig, nicht hinreichend. Fälschen kann man alles ausser dem Widerspruch.
Wer eine Extension vorschlägt, muss also sagen, warum die entstehende Geschlossenheit tragend ist und nicht bloss definitorisch. Das ist die schärfste Prüfung, die sich formulieren lässt — sie hat hier schon eine Idee zerlegt.
| Idee | Bewertung |
|---|---|
| Die Schnittstelle einer Teilformel benennen. Resolviert man in S alles weg, bleibt eine Klausel über ∂S. Benenne sie. | Kosten 2^|∂S| = 2^εk. Für k ~ log n sind die Gadgets polynomial. Nah an dem, was CDCL-Lernen ohnehin tut. Testbar. |
| Eine Vergröberung benennen. Variablen in Blöcke, je Block eine Variable für den Blockzustand. | Vermutlich nein — Zufälligkeit ist nicht selbstähnlich. Aber in einer Stunde testbar, und das Nein wäre selbst informativ. |
| Gelernte Klauseln benennen. Jede Lernklausel der Breite w durch eine Variable ersetzen. | Ist im Kern „extended learning"; bringt empirisch nichts auf Zufallsinstanzen. Aber warum wurde nie gemessen — mit dem Expansionsprofil geht das jetzt. Neue Messung. |
| Zählen jenseits von x = ½. Schneidet ein Verfahren anderswo, wandert das Optimum. | Die einzige der drei offenen Türen, an die man empirisch herankommt. Es fehlt ein Mass für Straffheit an beliebiger Polytopecke. Werkzeugproblem, lösbar. |
| Die Asymmetrie SAT/UNSAT ausnutzen. WalkSAT löst jede erfüllbare Schwellinstanz. | Starker Hinweis, dass es um das Zertifikat geht, nicht um die Suche. Passt genau zum Cook/Reckhow-Rahmen. |
| Untere Schranke statt Algorithmus. Frege beschränkter Tiefe auf Zufalls-3-CNF. | Offen, wohldefiniert, publikationswürdig — und die Expansionsdaten sind genau das Werkzeug, mit dem solche Schranken geführt werden. Der realistischste Beitrag. |
Für jede Idee steht das Instrumentarium bereit.
| Frage | Werkzeug | Dauer |
|---|---|---|
| Senkt eine Erweiterung die Expansion echt? | expansionsprofil | Minuten |
| Zündet eine geimpfte oder erweiterte Formel? | wechselkurs, umweg | Minuten |
| Wieviele Umwege braucht sie wirklich? | existenz (Beweis-DAG) | Stunden |
| Reicht ein Verfahren weiter als n₅₀ = 52,9? | pvier, schnellp4 | Minuten |
| Hat eine Familie einen kleinen Abschlussraum? | Wiederkehr-Detektor | Minuten |
| Hat sie Symmetrie? | bahnen (1-WL) | Sekunden |
| Wieviele Binärklauseln entstehen? | zweier | Sekunden |
Und die Regel, die uns dreimal gerettet hat: ein negativer Befund ohne funktionierende positive Kontrolle ist kein Befund.
Für jede Idee erst eine Familie suchen, bei der sie funktionieren muss (Taubenschlag, Tseitin, 2-SAT), und prüfen, dass das Instrument dort anschlägt. Ein Schnittebenentest meldete hier einmal „nichts gefunden" — und die Kontrolle verriet, dass der Taubenschlag schon aufgehört hatte zu feuern.