Sieben Variablen, dreissig Klauseln, unerfüllbar. Jeder Satz dieses Projekts wird als Markierung auf derselben Matrix gezeigt — Zeilen sind Variablen, Spalten sind Klauseln, grün = positives, rot = negatives Literal.
Die Formel
Dreissig Klauseln über sieben Variablen. Jede Spalte hat genau drei gefüllte Zellen — das ist die 3-CNF-Bedingung. Alles, was folgt, ist eine Markierung auf genau diesem Bild.
C3 · Der Abstand ist die Grundzustandsenergie
d(F) = minx c(x) — die kleinste Zahl Vorzeichenkippe, die F erfüllbar macht, ist gleich der kleinsten Zahl gleichzeitig verletzter Klauseln.
Bei sieben Variablen lassen sich alle 128 Belegungen zeigen:
Jedes Kästchen ist eine Belegung. Keine erreicht null — die Formel ist unerfüllbar. Aber elf erreichen Energie 1: sie verletzen genau eine Klausel. Also ist d(F) = 1, und ein einziger Vorzeichenkipp genügt.
Einer dieser elf Grundzustände, in die Matrix eingetragen — die Belegung steht als Spalte links, die einzige verletzte Klausel ist markiert:
Belegung x = 0000010 (grüne Zeile = wahr, rote = falsch). Unter dieser Belegung ist nur C10 verletzt: alle drei seiner Literale sind falsch. Genau das ist Energie 1.
C1 und C2 · Schuldig ⟺ reparabel ⟺ unentbehrlich
Für unerfüllbares F sind äquivalent: (a) es gibt x mit c(x) = 1 und C als einziger verletzter Klausel · (b) ein Vorzeichenkipp in C macht F erfüllbar · (c) F∖{C} ist erfüllbar · (d) C liegt in jedem minimalen unerfüllbaren Teilsystem.
Sammelt man über alle elf Grundzustände ein, welche Klausel dort jeweils verletzt ist, kommen genau sechs heraus:
Die sechs markierten Spalten sind die im Grundzustand verletzten Klauseln — und zugleich exakt die unentbehrlichen. Der Satz ist hier nicht behauptet, sondern abgezählt: beide Mengen sind {C4, C9, C10, C25, C27, C29}.
Zum Nachvollziehen. Nimm C10. Kippe eines seiner drei Vorzeichen — die Formel wird erfüllbar, und zwar mit genau der Belegung von oben. Entfernst du C10 stattdessen ganz, ist sie ebenfalls erfüllbar. Beides sagt derselbe Satz.
A1 · Das Ordnungszertifikat
Gibt es eine Variablenmenge V mit |V| = d, so dass alle 2d Belegungen von V unter Einheitspropagation in den Widerspruch laufen, so ist F unerfüllbar.
Für diese Formel genügt d = 2. Hält man x1 und x2 fest, erledigt Propagation den Rest — in allen vier Fällen:
Vier Blätter, vier Widersprüche. Jeder Pfeil ist ein Propagationsschritt, den die Formel erzwingt; unten steht die Klausel, an der es bricht. Mehr braucht der Unerfüllbarkeitsbeweis nicht.
Dieselben vier Konfliktklauseln in der Matrix, dazu die beiden Zertifikatsvariablen als Zeilen:
Blaue Zeilen: die zwei festgehaltenen Variablen. Rote Spalten: die vier Klauseln, an denen die Propagation jeweils bricht. Zwei von 7 Variablen und vier von 30 Klauseln tragen den ganzen Beweis.
B1 · Der Schlupf
Kodiert man eine Klausel der Breite w als Ungleichung, so hat sie am Punkt x = ½ den Schlupf ½w − 1 — unabhängig von den Vorzeichen.
In dieser Formel hat jede Spalte drei Zellen, also Breite 3, also Schlupf ½·3 − 1 = +0,5. Keine einzige ist straff. Straff hiesse Breite 2 — und dazu müsste erst ein Literal falsifiziert werden:
Unter jeder Spalte steht ihr Schlupf bei x = ½. Alle gleich, alle locker. Genau daran scheitert der Schnittebenenweg (Satz B3): es gibt keine straffe Stelle, an der eine Rundung greifen könnte.
C4 und C5 · Der Backbone als Handhabe
Sei F erfüllbar. Dann ist F ∧ C genau dann unerfüllbar, wenn alle drei Negationen der Literale von C Backbone-Literale sind. Folglich |A| = C(b, 3).
Entfernt man C4, wird die Formel erfüllbar — und zwar so knapp, dass alle sieben Variablen eingefroren sind. Sie hat dann genau eine Lösung:
Graue Spalte: C4 ist weg. Blaue Zeilen: alle sieben Variablen sind Backbone, ihr Wert steht in jeder Lösung fest. Nach C4 gibt es damit C(7,3) = 35 verschiedene 3-Klauseln, die diese Formel wieder unerfüllbar machen — C4 ist nur eine davon.
Resolution · warum die Sättigung verhungert
Zwei Klauseln lassen sich resolvieren, wenn sie ein Literal in entgegengesetztem Vorzeichen teilen. Das Ergebnis ist meist breiter als die Eltern. Nur wenn sie ausserdem ein Literal gleichsinnig teilen, wird es schmaler:
Jeder Bogen verbindet zwei Klauseln, deren Resolvent Breite ≤ 2 hat. Bei n = 7 gibt es davon 7 — reichlich. Bei n = 200 sind es im Mittel 0,2, und ab n = 200 kein einziger mehr. Das ist der Zündertrag 39,3/n aus ZUENDUNG.md, hier noch im sichtbaren Bereich.
Was diese Formel nicht zeigen kann. Sie ist zu klein für die Grössengesetze: d_zert = 0,130·n, Beweisbreite 0,254·n, der Zündertrag 39,3/n, die Lawinenverteilung. Die brauchen n in den Hunderten. Was sie zeigt, sind die Sätze — und die gelten für jede Grösse.