English

Die Ordnung eines Widerspruchs

Was genau unterscheidet aussagenlogische Formeln, die sich in Polynomialzeit entscheiden lassen, von zufälligem 3-SAT an der Schwelle? Sechzehn Berichte aus einem laufenden Projekt.

Stand 16. September 2026

Vier Familien unerfüllbarer Formeln lassen sich in Polynomialzeit widerlegen: Horn, 2-SAT, Tseitin und der Taubenschlag. Zufälliges 3-SAT bei α ≈ 4,267 nicht. Alles hier dreht sich um die Frage, woran dieser Unterschied liegt — und die Berichte sind so geschrieben, dass die Nullbefunde genauso festgehalten sind wie die Funde. Es sind mehr Nullbefunde.

Jede gemessene Zahl führt zu einem „Code & Daten ansehen“-Feld: der Quelltext, der sie erzeugt hat, und die tatsächliche Ausgabe — beides sicht- und kopierbar, nicht behauptet.

Der Stand

Wo das Projekt steht, und woran man weiterarbeiten kann.

  1. Die Ordnung eines Widerspruchs Der vollständige Arbeitsstand: was gemessen, was hergeleitet und was offen ist.
  2. Wo man ansetzen könnte Das Brett, wie es steht — und eine Prüfliste, die untaugliche Ideen in einer halben Minute erledigt, damit die Zeit für die tauglichen bleibt.
  3. Die Sätze an einer einzigen Formel Sieben Variablen, dreißig Klauseln, unerfüllbar. Jeder Satz des Projekts als Markierung auf derselben Matrix.

Zum Lernen

Erklärungen für alle, die die Werkzeuge selbst verstehen wollen.

  1. Wie CDCL funktioniert — und wie man misst, ohne sich zu täuschenneu Was moderne SAT-Löser tatsächlich tun, ein echter Lauf Schritt für Schritt, was jeder Baustein auf gemessenen Instanzen einbringt, und die Nullmessungen, die einen Algorithmen-Programmierer ehrlich halten — mit Code für den Alltag. Beispiel gegen Brute Force geprüft · für Programmierer

Die Achsen der Härte

Wovon es abhängt, wie schwer eine einzelne Instanz ist — und wovon nicht.

  1. Gerüst und Vorzeichen Die Zerlegung der Härtestreuung in ihre beiden Anteile. Ausgangspunkt für alles Weitere.
  2. Die Vorzeichenachse Die Hälfte der Streuung sitzt in den Vorzeichen. Vollständig vermessen bis Fourier-Grad 12 — und dort sind es genau zwei Richtungen.
  3. Der Vorzeichenkörper Erst der stumpfste Versuch — die Formel selbst als Koordinate —, der beweisbar scheitert. Dann der Vorschlag, der ihn ersetzt.
  4. Zwei-Achsen-Trennung Warum Aggregate über den Belegungsraum SAT nicht von UNSAT trennen können. Gemessen und bewiesen — und die Schranke, an der sich seither jeder Zugang misst.
  5. Eingriff am Gerüstneu Eine Sonde, die kritische Klauseln findet, ohne zu lösen, zwei Achsen der Härte, die keine Expansion sind, und der erste Eingriff im Bestand: Instanzen bei fester Gradfolge umzuverdrahten verändert die Härte wie vorhergesagt — aber nur für Löser, die auf Struktur reagieren. kausal · vorregistriert · 250 800 Ablationsläufe · n = 100 und 130

Härte vorhersagen

Der schmale Grat: Größen, die tatsächlich etwas über die Kosten wissen.

  1. d(50 %)-Analyse Die einzige Größe, die Härte bei festem n vorhersagt — warum, und was daraus folgt. r = 0,56 · braucht einen Löser
  2. r(d)-Kurvenform Die Form der Ordnungsrate-Kurve trägt mehr Härteinformation als d(50 %) allein.
  3. Der Judo-Wurfneu Statt nach Struktur zu suchen, die Unordnung eines Prozesses als Sonde nehmen. Sechs löserfreie Sonden, 80 000 Kandidaten, geeicht gegen Vertauschung — und ein Fund, der knapp über allem bisher Löserfreien liegt — auf frischen Instanzen wiederholt. streng r = 0,27 · ohne Löser · auf 900 frischen Instanzen bestätigt

Räume und Karten

Nicht einzelne Formeln, sondern die Räume, in denen sie liegen.

  1. Karte des Instanzraums Nicht der Lösungsraum, sondern der Raum aller Instanzen. Erfüllbarkeit ist darauf monoton — der Raum hat einen Rand, eine Höhe und eine lokale Geometrie.
  2. Der Zulässigkeitsraumneu Fünf Kandidaten für ein Strukturmass, vier davon durch eigene Kontrollen gekippt. Was bleibt: ein Redundanzmass ohne Clustering und ein exakt verifizierter gleichverteilter Sampler über den vollständigen Lösungsraum, mit drehbarer 3D-Ansicht der echten Cluster.
  3. SAT im Phasenraum Ersetzt man die Wahrheitswerte durch reelle Zahlen, wird aus Erfüllbarkeit ein deterministischer Fluss. Er findet jede Lösung — aber der Weg dorthin ist ein chaotischer Transient mit fraktalen Einzugsrändern. 1,8 Mio. Trajektorien · Vorläufer des Judo-Wurfs
  4. Bahnen Fünf Tafeln aus 692 MB Rohdaten: bis zu 20 006 Sortierungen je Instanz, jede Klausel ein Messpunkt.

Grenzen

Wo die Verfahren kippen, und ab wann die Sätze überhaupt gelten.

  1. Welcher Hebel wirklich bewegtneu Drei Stellen, an denen dieser Bestand gegen sich selbst steht — darunter sein grösster Hebel, verbucht als wirkungslos. Und eine Regel, um Extensionsvariablen zu erfinden: bei identischer Klausel- und Variablenzahl retten gezielte Definitionen 13 von 20 Instanzen, wo zufällige 0 von 23 retten. Dann schliesst die Skalierung sie wieder. n₅₀ 52,9 → 90,9 · Soundness 438/438 · und er stirbt trotzdem
  2. SAT ohne UND und ODER Rollt man UND und ODER ganz auf, wird eine Klausel zu genau einem verbotenen Muster. Sieben ausführbare Ebenen, die auf 72.320 Belegungen übereinstimmen, ein Auswerter mit vier Halbringen — und zwei Messungen, die sich in der üblichen Schreibweise nicht formulieren lassen: die Saat ist vor dem Lauf ablesbar, und die Konfliktgraph-Route ist dominiert. Korrektur: die dritte, „die Zünddichte ist breiteninvariant“, ist widerlegt — siehe die Hebel-Seite. AUC 0,91 · löserfrei · mit Werkbank
  3. Zwei Attraktoren Breitenbeschränkte Resolution bricht nicht ein, sie kippt: entweder eine Lawine von zwanzigtausend Klauseln oder Verhungern bei fünfhundert — dazwischen praktisch nichts.
  4. Wo Asymptopia anfängt Ein Satz sagt, die Beweisbreite wachse linear mit n. Die Messung sagt, sie sei 3. Beide haben recht — und der Grund ist eine Zahl, die bisher niemand ausgerechnet hat.