Erst der stumpfste Versuch: die Formel selbst als Koordinate. Er scheitert, und zwar beweisbar. Dann der Vorschlag, der ihn ersetzt — das Gerüst festhalten und nur die Vorzeichen aufspannen. Der entstehende Körper ist wirklich ein Körper. Sein Koordinatensystem steht aber schon fest, bevor man ihn betritt.
n = 14, m = 60 (α = 4,29) · alles exakt über den vollständigen Belegungswürfel · koordinate.py · vorzeichenkoerper.py
Die Koordinaten der Karte des Instanzraums — Unwucht, Gradstreuung, Höhe d — sind ausgerechnete Grössen. Der naheliegende Gegenvorschlag: nimm die Formel selbst. Klauseln sortiert, je Literal Variablenindex und Vorzeichen. Idiomatischer geht es nicht, und billiger auch nicht — die Koordinate ist die Eingabe.
Kanonische Form: in jeder Klausel die drei Literale nach (Variable, Vorzeichen) sortiert, dann die Klauseln lexikographisch. Das ergibt 180 Literalplätze, jeder mit einem Paar aus 2n = 28 Möglichkeiten. Sie trägt die volle Information — verlustfrei, denn sie ist die Formel.
Und sie klassifiziert nicht. Nächster-Nachbar auf dieser Liste, 120 exakt gelöste Instanzen, leave-one-out:
| Grösse | Wert | Bemerkung |
|---|
Der Gewinn gegenüber „immer SAT sagen“ ist negativ. Der nächste Nachbar liegt im Median 129 von 180 Plätzen entfernt — er ist eine beliebige andere Instanz, sein Label ein Münzwurf.
Der Grund steht in einem einzigen Bild. Drei Abstandsverteilungen liegen übereinander: der Abstand zum nächsten Nachbarn in der Stichprobe, der Abstand zur eigenen umbenannten Kopie (gleiche Antwort, garantiert) und der Abstand zu einer fremden Zufallsinstanz. Und ganz links, bei 1, sitzt der Massstab, auf dem die Antwort tatsächlich kippt.
Zwei Zufallsformeln haben im Median 59 ihrer 60 Klauseln nicht gemeinsam. Das ist Abzählung, nicht Pech:
Alle 180 Ein-Literal-Nachbarn jeder Instanz, exakt geprüft. Unten die Kippkarte einer einzelnen Instanz: 60 Klauseln zu je 3 Literalplätzen, markiert sind die Plätze, an denen ein umgelegtes Vorzeichen die Antwort umwirft.
| Klasse | Instanzen | mit ≥ 1 kippendem Nachbarn | kippende Nachbarn im Mittel |
|---|
Abstand klein ⇏ Label gleich. 82 % aller Instanzen haben einen direkten Nachbarn mit dem anderen Label — ein einziges umgelegtes Vorzeichen in einer einzigen Klausel.
Abstand gross ⇏ Label verschieden. Der Abstand einer Formel zu ihrer eigenen umbenannten Kopie ist 149; zu einem völlig Fremden 150. Die Antwort ist im ersten Fall garantiert dieselbe — nachgeprüft, 120 von 120.
Der Abstand in dieser Koordinate ist also zu beiden Seiten vom Label unabhängig. Kein Verfahren, das auf Nachbarschaft beruht — 1-NN, Kernel, Einbettung, Interpolation — kann darauf etwas ausrichten. Nicht weil die Information fehlte: sie ist vollständig da. Sondern weil die Metrik nichts mit ihr zu tun hat.
Damit steht auch, was eine brauchbare Koordinate mitbringen muss: sie muss die Symmetrien der Antwort teilen. Die stumpfe Liste teilt keine einzige — weder die Umbenennung der Variablen (n! = 1010,9 Varianten je Formel) noch die Umeichung der Vorzeichen.
Der nächste Schritt geht deshalb nicht über die ganze Formel, sondern über den Teil, der eine Symmetriegruppe mitbringt.
Der Vorschlag: das Gerüst festhalten — welche Variablen in welcher Klausel stehen — und nur die Vorzeichen als Koordinaten nehmen. Ursprung ist die Formel ohne Vorzeichen, alle Literale positiv. Jedes einzelne Vorzeichen ist eine eigene Richtung, und der Körper baut sich auf, bis alle Vorzeichen gesetzt sind.
Das ist ein sauber definiertes Objekt: der Würfel {+,−}180. Der Ursprung ist immer lösbar — alles wahr setzen. Und dann kommt sofort die Symmetrie, die alles Weitere bestimmt.
Alle Vorkommen einer Variablen umzudrehen heisst, die Variable umzubenennen. x ↦ ¬x. Die Antwort bleibt. Das ist eine Gruppe von 2n = 16 384 Eichungen, die frei auf dem Würfel wirkt — nachgeprüft an 1 000 von 1 000 Umeichungen.
Insbesondere für g = −1: „alle Literale negativ“ ist derselbe Punkt wie „alle Literale positiv“. Beide sind trivial lösbar. Der Weg „bis alle Vorzeichen gesetzt sind“ endet also dort, wo er begann — er ist ein geschlossener Ring, kein Durchmesser.
Die erste Frage an einen Körper ist seine Form von aussen: wie lösbar ist eine Schale mit r negativen Literalen? Sechs Gerüste, 60 Proben je Schale, jede Instanz exakt gelöst.
Jetzt der Aufbau selbst, Schritt für Schritt: vom Ursprung ein Vorzeichen nach dem anderen umlegen, bis alle 180 gesetzt sind. Beide Enden sind derselbe, lösbare Punkt — die Zahl der Kreuzungen muss also gerade sein. Gemessen: in 100 % der 120 Wege. Das ist die Eichprobe.
Ein Ball hätte genau zwei Kreuzungen und ein zusammenhängendes Loch.
180 Dimensionen lassen sich nicht zeichnen, 16 schon. Sechzehn Vorzeichenplätze freigegeben, die anderen 164 festgehalten, alle 65 536 Punkte einzeln exakt gelöst. Die Fläche unten ist dieser Teilwürfel im Gray-Code: benachbarte Bildpunkte sind immer Nachbarn im Würfel, unterscheiden sich also in genau einem Vorzeichen.
| Grösse | gemessen | Zufallsfunktion gleicher Bilanz |
|---|
Dieselben 65 536 Werte, Fourier-transformiert. Das Gewicht Wk sagt, wieviel der Antwort auf Wechselwirkungen von genau k Vorzeichen entfällt. Eine Zufallsfunktion legt ihr Gewicht in die Mitte, auf Grad 8.
Mittlerer Grad 1,33 von 16, gegen 8,0 bei Rauschen; die lösbare Menge hat genau eine Zusammenhangskomponente. Die Intuition des Vorschlags ist damit bestätigt — es ist wirklich ein Körper, kein Staub.
Jetzt die Eichung aus §4 auf das Spektrum angewandt. Ein Charakter χS(x) = ∏i∈S xi überlebt die Umeichung einer Variablen v genau dann, wenn S gerade viele Plätze von v enthält — sonst wechselt er das Vorzeichen, während die Antwort sich nicht rührt, und sein Koeffizient ist exakt null.
Überleben also genau die Mengen, die jede Variable gerade oft treffen: die Kreise des Inzidenzgraphen. Das ist eine Vorhersage mit scharfen Nullstellen, und sie lässt sich gegen den eigenen Rauschboden prüfen — 3 Gerüste × 6 000 exakt gelöste Punkte:
| Charakterklasse | Gerüst 1 | Gerüst 2 | Gerüst 3 | Vorhersage |
|---|
Von den C(180,2) = 16 110 Paaren überleben 1 118 (6,9 %) — genau die auf derselben Variablen. Und ihre ungewichtete Summe ist eine alte Bekannte dieses Projekts:
| Koordinate | Grad | AUC | Korrelation | Urteil |
|---|
Der naive Radius ist beweisbar blind. „Wieviele Vorzeichen habe ich gesetzt“ ist eine Grad-1-Grösse, also exakt null. Korrelation mit der Antwort: −0,006 / −0,005 / −0,002 über drei Gerüste, AUC 0,508. Das ist kein schwaches Messergebnis, sondern ein Satz — und genau deshalb ist auch das Radialprofil aus §5 exakt spiegelsymmetrisch.
Der Vorzeichenkörper ist keine neue Tür. Er ist etwas Selteneres: die Herleitung der Tür, die dieses Projekt vorher nur empirisch gefunden hatte. Der Suchraum auf der Vorzeichenachse ist damit nicht vermutet, sondern bewiesen geschlossen — wer dort etwas sucht, sucht eine Funktion der Kreise, denn es gibt nichts anderes.
| Grad | Charaktere | Name | Stand |
|---|
Und der Befund sagt zusätzlich, wo die restlichen 85 % der Vorzeichenachse nicht sitzen können: in keiner Grösse, die nicht eichinvariant ist. Jede Kandidatengrösse, die sich unter dem Umbenennen einer Variablen ändert, ist vor der ersten Messung erledigt.
Der naheliegende erste Griff — „(a ∨ b ∨ c) und (¬a ∨ ¬b ∨ ¬c) sagen dasselbe" — stimmt global und nicht einzeln. Alle Klauseln zugleich zu komplementieren ist die Eichung g = −1 aus §4: die Lösung wird mitkomplementiert, nachgeprüft an 400 von 400 Instanzen. Eine Klausel zu komplementieren kippt die Antwort — auf Zufallsinstanzen an der Schwelle in der Fälle.
Und es gibt ein Gegenbeispiel mit vier Variablen, das man von Hand nachrechnet:
Die sieben Klauseln über {a, b, c} schliessen jede Belegung ausser a = b = c = 1 aus; danach sind (a ∨ b ∨ d) und (a ∨ b ∨ ¬d) durch a = 1 erfüllt. Nach dem Tausch bleibt statt 111 nur 000 übrig, also a = b = 0 — und dann verlangen die beiden d-Klauseln d = 1 und d = 0 zugleich.
Das passt zum bekannten Extremfall: bei Tseitin-Formeln über einem 3-regulären Graphen ist die Gerüst-Statistik von den Ladungen unabhängig, und allein das Vorzeichenmuster entscheidet über die Erfüllbarkeit. Vorzeichen sind nicht wegzukürzen — nur ihre Bahn ist es.
Was bleibt, sind zwei Sorten Redundanz: die der Notation (Reihenfolgen, Doppelungen) und die der Gruppe (Umbenennen, Umeichen). Beide vollständig, mit exaktem Faktor:
| Stufe | Balken | Rest | Faktor | Preis |
|---|
Von 10255 auf 10111. Davon trägt die Notation 10129 und die Gruppe 1015. Mehr Gruppenredundanz gibt es nicht: Sn ⋉ {±1}n ist die volle Automorphismengruppe des Literalraums.
Blockierte Klauseln (BCE) sind die stärkste in Polynomzeit erkennbare Streichregel; reine Literale sind ihr Sonderfall. Bei α = 2 nimmt sie fast die halbe Formel weg. An der Schwelle bleibt weniger als 1 %.
Sortieren erledigt die Notation. Für die Gruppe braucht es eine Regel, die aus jeder Bahn genau einen Vertreter wählt. Sie steht in redundanz.py:
| Prüfung | Ergebnis | Bedeutung |
|---|
Diskret heisst zugleich: der Stabilisator ist trivial. Die Bahn hat also volle Grösse 2n·n!, und der Quotient in §12 ist exakt, keine obere Schranke. Der teure Fall — Verfeinerung diskretisiert nicht, dann wäre Individualisieren nötig und im schlimmsten Fall Graphisomorphie — tritt bei Zufallsinstanzen an der Schwelle nie ein.
§3 hatte zwei Krankheiten diagnostiziert. Dieselben 120 Instanzen, jetzt kanonisiert:
| Grösse | roh sortiert | kanonisiert |
|---|
Krankheit 1 ist geheilt. „Abstand gross ⇏ Label verschieden" gilt nicht mehr — die eigene umbenannte Kopie liegt jetzt auf Abstand null, ausnahmslos.
Krankheit 2 ist unberührt. „Abstand klein ⇏ Label gleich": 82 % der Instanzen haben weiterhin einen Nachbarn auf Abstand 1 mit dem anderen Label. Das ist eine Eigenschaft der Antwort, nicht der Darstellung, und keine Kanonisierung kann daran etwas ändern.
Der Ertrag in einem Satz: Kanonisierung entfernt Redundanz, sie erzeugt keine Struktur. Der Raum wird um 144 Zehnerpotenzen kleiner und bleibt genauso ungeordnet.
Einundzwanzig Vorzeichenplätze freigegeben, in drei Gruppen zu sieben. Jede Gruppe ist eine Achse, im Gray-Code auf 128 Stufen: benachbarte Zellen unterscheiden sich in genau einem Vorzeichen, in allen drei Richtungen. Alle 2 097 152 Zellen einzeln exakt gelöst, bei n = 20 Variablen und α = 4,25.
Möglich wird das durch einen inkrementellen Löser: auf einem Schlangenpfad durch das Gitter ändert sich je Schritt genau ein Vorzeichen, also genau eine Klausel — statt neu zu lösen werden zwei Schnitte im Verletzungsfeld umgebucht und die Zahl der Lösungen mitgeführt. 43 µs je Zelle auf 24 Kernen, Zelle für Zelle gegen den Referenzlöser geprüft.
| Grösse | gemessen | Zufallsfunktion gleicher Dichte |
|---|
Dasselbe Bild wie in §6, jetzt räumlich — und die Zufallskontrolle macht es erst scharf. Das Lösbare hängt zusammen, wo eine Zufallsmenge gleicher Dichte in Zehntausende Stücke zerfiele; das Unlösbare zerreisst, wo Zufall einen einzigen Klumpen hätte. Die Abweichung geht in beide Richtungen.
Und die letzte Zeile der Tafel ist die schärfste Strukturzahl der ganzen Seite: verschmilzt man die Oberfläche zu möglichst grossen Rechtecken, schrumpft sie um mehr als das Zwanzigfache — bei einer Zufallsfunktion um das Anderthalbfache. Die Oberfläche besteht fast nur aus grossen ebenen Platten. Warum, steht in §16.
Der Würfel ist offensichtlich strukturiert — Platten, Balken, Säulen, Treppen, alles achsenparallel. Dafür gibt es zwei mögliche Ursachen, und sie lassen sich trennen: die Funktion (wenige Vorzeichen tragen fast alles) und die Anordnung (der Gray-Code legt gleiche Bitwerte in zusammenhängende Streifen). Die Gegenprobe ist einfach: dieselbe Menge mit zufällig durchgewürfelten Achsenpositionen, und eine Zufallsfunktion gleicher Dichte im selben Raster.
| Fall | Oberfläche (Flächen, mit Rand) | verschmolzene Rechtecke | Lauflänge x · y · z |
|---|
Beides trägt bei, aber nicht gleich viel — und die Netzspalte trennt es am schärfsten. Der echte Körper braucht 56 839 Rechtecke. Dieselbe Menge mit durchgewürfelten Achsenpositionen braucht 5,6-mal so viele, eine Zufallsfunktion im selben Raster 36-mal so viele. Die Formen sind also überwiegend echt — der Gray-Code macht sie sichtbar, er erfindet sie nicht.
Der eigentliche Grund steht in den Einflüssen: wie oft kippt die Antwort, wenn man genau dieses eine Vorzeichen umlegt und alle anderen stehen lässt? Bei einer Zufallsfunktion wären alle 21 Werte gleich.
Das ist der Mechanismus hinter den Stufen: ein Vorzeichen, das die Antwort nur in eine Richtung kippt, schneidet einen Halbraum aus dem Körper. Mehrere davon geben Platten, Balken und Treppen — nie zerstreute Flecken.
Damit lässt sich jede sichtbare Form einem Vorzeichen zuordnen. Der Gray-Code legt fest, welche Streifenbreite dabei herauskommt: das höchste Bit teilt die Achse ein einziges Mal, das niedrigste in 32 schmale Bänder.
| Rang | Achse · Bit | Form im Bild | Einfluss | einseitig |
|---|
Die dritte Ursache gilt nur für diesen Würfel, und das ist selbst ein Befund: die drei Achsen sind hier ungleich stark besetzt — Einfluss , Spanne . Die schwächste Achse hat eine mittlere Lauflänge von Zellen gegen . Das sind die langen Säulen im Bild. Auf welche Achse es fällt, ist reine Willkür der Zuteilung: im Vergleichswürfel bei n = 22 sind die drei Achsen fast gleich stark (Spanne 1,2×), und dort gibt es die Säulen in dieser Form nicht.
Alle drei Befunde zeigen dorthin, wo schon das Spektrum aus §8 hinzeigte: Gesamteinfluss von 21 gegen bei Rauschen, mittlerer Fourier-Grad . Die Formen sind die niedrige Ordnung, sichtbar gemacht.
Bleibt die Frage, ob das alles an diesem Würfel hängt — am kleinen n, an der Auflösung, an der Zahl freigegebener Vorzeichen. Also zwei weitere Läufe: derselbe Aufbau bei n = 22 (α = 4,27, wieder 2 097 152 Zellen, 597 s statt 89), und ein achtmal feinerer Würfel — 256 × 256 × 256 = 16 777 216 Zellen mit 24 freien Vorzeichen, 1 631 Sekunden.
Der Kern hält über alle drei. Der Gesamteinfluss liegt bei 1,99 / 1,93 / 1,53 — immer bei einem Sechstel bis einem Achtel dessen, was Rauschen ergäbe. Eine Näherung aus zwölf Vorzeichen trifft 97,8 / 99,0 / 97,5 %, und die Netzverdichtung liegt bei 22,5 / 11,2 / 47,8× gegen 1,3–1,5× bei Zufall. Auch die beiden Kontrollfaktoren bleiben stabil.
Zwei Aussagen sind dagegen würfelspezifisch und dürfen nicht verallgemeinert werden. Die Achsen-Asymmetrie schwankt (5,3× / 1,2× / 2,2×) — die langen Säulen im Bild sind eine Eigenschaft der Zuteilung, nicht des Körpers. Und der Zusammenhang zwischen Einfluss und Einseitigkeit wechselt sogar das Vorzeichen: +0,312 / −0,048 / −0,747. Einseitig sind die Vorzeichen überall — welche es besonders sind, ist Zufall des Würfels.
Und eine Einschränkung, die der grosse Würfel erzwingt. Bei 50 % und 60 % Lösbarkeit hing die lösbare Menge weitgehend zusammen und die unlösbare zerfiel; bei 19,3 % ist es umgekehrt — die grösste lösbare Komponente hält nur noch 5,9 %. Das ist kein Unterschied zwischen SAT und UNSAT, sondern Perkolation: unterhalb der Schwelle des Würfelgitters (rund 31 %) zerfällt jede Menge dieser Dichte.
Der Vergleich mit dem Zufall überlebt das aber mühelos und ist die eigentliche Aussage: bei 19,3 % Dichte zerfällt eine Zufallsmenge in 1 442 302 Stücke mit grösstem Anteil 0,0 % — die gemessene lösbare Menge in 94. Das ist ein Faktor 15 000 weniger Zerfall bei gleicher Dichte.
Konzentration und Einseitigkeit sind bisher an einem Würfel gemessen. Die Gegenprobe: 30 frisch gezogene Würfel bei n = 18, je 32 768 Zellen exakt gelöst — 450 Vorzeichenplätze.
| Grösse | Mittel ± Streuung | was daraus folgt |
|---|
Und damit die Frage, die entscheidet, ob das ein Werkzeug ist: lässt sich vorher sagen, welche Vorzeichen die einflussreichen sind — aus billigen örtlichen Grössen des Platzes? Mitgeprüft sind zwei teure Merkmale (liegt die Variable im Rückgrat, stimmt das Literal mit ihrem Rückgratwert überein) und eine Nullkontrolle, die leer sein muss: die Gray-Bitstelle, reine Anordnung.
| Merkmal | Art | r | in σ |
|---|
Und damit ist es kein Verfahren. Welche Vorzeichen einflussreich sind, hängt an der Instanz — und den Einfluss eines Vorzeichens auszurechnen heisst, die Formel auf beiden Seiten davon zu lösen. Die Struktur ist da, sichtbar und messbar; der Weg zu ihr führt durch die Antwort, die man sucht.
Der Würfel wirkt auffällig symmetrisch. Das hat zwei Gründe, und nur einer davon steht im Körper.
Der gespiegelte Gray-Code erfüllt eine Identität, die man nachrechnen kann:
Eine Achse zu spiegeln heisst also genau ein Vorzeichen umzulegen — das auf dem obersten Bit dieser Achse. Daraus folgt eine scharfe Vorhersage: die Übereinstimmung des Bildes mit seinem Spiegelbild muss gleich 1 − Einfluss(oberstes Bit) sein.
| Würfel · Achse | Spiegel-Übereinstimmung | 1 − Einfluss(oberstes Bit) | Abweichung |
|---|
Abweichung exakt null, auf jeder Achse jedes Würfels. Die Spiegelsymmetrie ist das oberste Bit — ein Befund über die Karte, nicht über den Körper. Legt man dieselben Daten neu auf, mit den stärksten Vorzeichen auf den obersten Bits, fällt die Übereinstimmung auf — die Symmetrie verschwindet, ohne dass sich am Körper irgendetwas geändert hätte.
Manche der freigegebenen Vorzeichen ändern die Antwort in keiner einzigen Zelle. Nicht selten, nicht fast nie: exakt nie. Jedes solche Vorzeichen verdoppelt das Bild, ohne etwas hinzuzufügen.
| Würfel | freigegeben | wirksam | wirkungslos | verlustfreie Reduktion |
|---|
| Erklärung | Treffer | Bewertung |
|---|
Und was das für den Instanzraum heisst: nichts. Diese Vorzeichen sind wirkungslos in diesem Ausschnitt — ihre Klausel ist durch den festgehaltenen Rest schon erfüllt. Es ist keine Symmetrie der Formel, sondern eine Eigenschaft des Kontexts, und sie zu erkennen verlangt das Rückgrat, also die Lösung. Die Bilanz aus §12 bleibt daher stehen: 10111, und der Raum wird davon nicht kleiner.
Was kleiner wird, ist das Bild: der 256³-Würfel ist in Wahrheit ein 14-dimensionales Objekt, 1024-fach im Gitter wiederholt.
Vollständigkeit heisst auch, zu sagen, was es nicht gibt.
| Vorschlag | Status | Grund |
|---|