Formulierung · Zufalls-3-SAT an der Schwelle

SAT ohne UND und ODER

Eine Klausel sagt nicht „eines von dreien gilt“. Wörtlich sagt sie: dieses eine Eckenmuster ist verboten. Rollt man UND und ODER ganz auf, bleibt eine Liste verbotener Blöcke im Würfel — und drei Messungen, die sich in der üblichen Schreibweise gar nicht formulieren lassen.

Stand: 3. September 2026

1 UND und ODER sind keine Axiome

Erklärt man (a ODER b ODER c) einem Fünfjährigen, sagt man: schau sie der Reihe nach an; sobald eine stimmt, bist du fertig. Das ist kein Grundbegriff, sondern ein Durchlauf mit einem Abbruchwert. UND ist derselbe Satz mit vertauschtem Abbruchwert. Beide lassen sich also ausprogrammieren statt voraussetzen.

Sieben Ebenen, jede ausführbar, alle sieben gegeneinander geprüft auf 72 320 Belegungen ohne einen einzigen Unterschied:

Ebene	Was sie sagt	Was sie benutzt
0	die Abstraktion	`all(any(…))`
1	Quantoren	ES GIBT / FÜR ALLE
2	Durchlauf mit Abbruch	Schleife, Vergleich, Abbruch
3	eine Faltung	UND und ODER trennen genau drei Zahlen
4	Zählen	wieviele Literale stimmen
5	Arithmetik	ein Produkt je Klausel, eine Summe darüber
6	Bitmaske	`(p & fest) == wert`

Zwei Dinge fallen dabei heraus, die die Abstraktion versteckt hatte. Ebene 4 erzeugt die Höhe d — die Zahl der verletzten Klauseln, die UND/ODER gar nicht kennen können, weil sie nur erfüllt von nicht erfüllt unterscheiden. Und Ebene 6 ist das Blockbild: es wurde nie als andere Sicht gewählt, es ist schlicht der Rest.

Code & Daten ansehen — die sieben Ebenen und ihre Uebereinstimmung

aufgerollt.py

def ebene0(klauseln, v):                 # die Abstraktion
    return all(any(literal_wert(l, v) for l in c) for c in klauseln)

def falte(werte, start, verknuepfen, abbruch):
    """Der gemeinsame Kern.  ODER und UND sind DERSELBE Code.

    ODER = falte(werte, start=0, verknuepfen=groesser, abbruch=1)
    UND  = falte(werte, start=1, verknuepfen=kleiner,  abbruch=0)
    """
    e = start
    for w in werte:
        e = verknuepfen(e, w)
        if e == abbruch:
            break
    return e

def ebene6(bloecke, p):                  # eine Bitmaske, sonst nichts
    for fest, wert in bloecke:
        if (p & fest) == wert:
            return False
    return True

Ausgabe

$ python3 aufgerollt.py

Eine Klausel, sieben Mal dasselbe.   Klausel [-1, 2, -3]   Belegung [1, 0, 1]

  Ebene 0  Abstraktion    any(literal_wert(l, v) for l in c)      -> False
  Ebene 1  Quantor        ES GIBT ein Literal, das stimmt         -> False
  Ebene 2  Durchlauf      lauf durch, brich ab sobald eines stimmt-> False
  Ebene 3  Faltung        falte(werte, 0, groesser, abbruch=1)    -> 0
  Ebene 4  Zaehlen        Trefferzahl > 0 ?                       -> 0 Treffer
  Ebene 5  Arithmetik     Produkt der (1 - wert) == 0 ?           -> Produkt = 1
  Ebene 6  Bitmaske       fest=111 wert=101 p=101                 -> True

Sieben Ebenen, 200 Instanzen, 72320 Belegungen: einig
Vier Halbringe, 40 Instanzen, gegen unabhaengige Rechnung: einig

Und derselbe Auswerter mit vier Halbringen, an einem Beispiel:
    Boolesch  -> loesbar?                                    = 1
    Zaehlen   -> wieviele Loesungen                          = 13
    min-plus  -> Hoehe d (kleinste Zahl verletzter Klauseln) = 0
    max-plus  -> MaxSAT (groesste Zahl erfuellter Klauseln)  = 40

200 Zufallsinstanzen, n ∈ {6,8,10}, α ∈ {2,0; 4,26; 6,0}; jede Ebene auf jeder der 2^n Belegungen ausgewertet.

2 Ein Programm, vier Bedeutungen

Wenn UND und ODER sich nur in drei Zahlen unterscheiden, rechnet dasselbe Programm etwas anderes aus, sobald man diese Zahlen durch zwei andere Operationen ersetzt. Ein Paar (plus, mal) mit neutralen Elementen heisst Halbring. Vier davon, ein Auswerter, jeder gegen eine unabhängige Rechnung geprüft:

Halbring	Z = ⊕_Belegungen ⊗_Klauseln	Beispiel
(max, min)	gibt es eine Lösung?	1
(+, ×)	wieviele Lösungen	13
(min, +)	Höhe d — wenigste verletzte Klauseln	0
(max, +)	MaxSAT — meiste erfüllte Klauseln	40

Die Schleife weiss davon nichts.

Code & Daten ansehen — ein Auswerter, vier Halbringe

aufgerollt.py

HALBRINGE = {                    # (plus, mal, null, eins, wert_einer_klausel)
    "Boolesch -> loesbar?":     (groesser, kleiner, 0, 1, lambda e: 1 if e else 0),
    "Zaehlen  -> #Loesungen":   (add,      mul,     0, 1, lambda e: 1 if e else 0),
    "min-plus -> Hoehe d":      (kleiner,  add,   inf, 0, lambda e: 0 if e else 1),
    "max-plus -> MaxSAT":       (groesser, add,  -inf, 0, lambda e: 1 if e else 0),
}

def auswerten(n, klauseln, halbring):
    """EIN Programm.  Die Bedeutung steckt allein im Halbring."""
    plus, mal, null, eins, klauselwert = halbring
    z = null
    for p in range(1 << n):                       # alle Belegungen
        v = [(p >> i) & 1 for i in range(n)]
        t = eins
        for c in klauseln:                        # alle Klauseln
            t = mal(t, klauselwert(erfuellt(c, v)))
        z = plus(z, t)
    return z

Ausgabe

$ python3 aufgerollt.py

Eine Klausel, sieben Mal dasselbe.   Klausel [-1, 2, -3]   Belegung [1, 0, 1]

  Ebene 0  Abstraktion    any(literal_wert(l, v) for l in c)      -> False
  Ebene 1  Quantor        ES GIBT ein Literal, das stimmt         -> False
  Ebene 2  Durchlauf      lauf durch, brich ab sobald eines stimmt-> False
  Ebene 3  Faltung        falte(werte, 0, groesser, abbruch=1)    -> 0
  Ebene 4  Zaehlen        Trefferzahl > 0 ?                       -> 0 Treffer
  Ebene 5  Arithmetik     Produkt der (1 - wert) == 0 ?           -> Produkt = 1
  Ebene 6  Bitmaske       fest=111 wert=101 p=101                 -> True

Sieben Ebenen, 200 Instanzen, 72320 Belegungen: einig
Vier Halbringe, 40 Instanzen, gegen unabhaengige Rechnung: einig

Und derselbe Auswerter mit vier Halbringen, an einem Beispiel:
    Boolesch  -> loesbar?                                    = 1
    Zaehlen   -> wieviele Loesungen                          = 13
    min-plus  -> Hoehe d (kleinste Zahl verletzter Klauseln) = 0
    max-plus  -> MaxSAT (groesste Zahl erfuellter Klauseln)  = 40

40 Instanzen; jeder Halbring gegen eine unabhängige Aufzählung derselben Größe geprüft. Keine Abweichung.

3 Die Zünddichte ist breiteninvariant

Zwei Attraktoren zeigt, dass die breitenbeschränkte Sättigung kippt statt abzufallen, und Wo Asymptopia anfängt, dass Breite 3 bis n ≈ 55 trägt. Das Blockbild liefert die Buchhaltung dazu, warum eine breitere Ebene nicht hilft.

Zwei Breite-3-Blöcke verschmelzen nur dann wieder auf Breite ≤ 3, wenn sie mindestens zwei Stellen teilen. Das sind die Zündpunkte. Ebene w hat O(n^w2^w) Plätze. Zünddichte × n³, Median über 10 Instanzen:

n	w = 3	w = 4	w = 5	w = 6
32	62,8	64,4	5,6	0,6
48	61,1	62,5	3,5	0,2
64	65,2	63,3	2,6	0,1
96	60,9	63,2	1,7	0,1
128	62,6	62,3	1,3	0,0

Ebene 4 hat bei n = 32 fünfzehnmal so viel Saat wie Ebene 3 (1 214 gegen 80) und einen fünfzehnmal größeren Vorrat. Das kürzt sich weg, auf zwei Stellen genau, über den ganzen gemessenen Bereich. Und ab Ebene 5 wird es schlechter: die Saat sättigt — zwei Breite-3-Blöcke mit einer Streitstelle teilen mindestens diese Stelle, also landet jede mögliche Verschmelzung ohnehin auf Ebene 4 — während der Vorrat weiter mit n^w wächst. Breiter werden fügt keinen Zündpunkt hinzu, nur Platz.

4 Die Saat ist vor dem Lauf ablesbar

Zwei Attraktoren misst den Verzweigungsfaktor während der Sättigung. Dieselbe Größe steht vorher zur Verfügung, allein aus der Klauselliste, in O(m²) — ohne jeden Abschluss.

20 unlösbare Instanzen bei n = 56; billige Kennzahlen (0 s) gegen die teure Frage, ob der Abschluss zündet (bis 1 217 s):

Kennzahl	AUC	Median zuendend	Median sterbend
Saat	0,91	95	79
λ₁	0,91	0,38	0,33
λ₂	0,86	0,90	0,65
λ₃	0,85	1,06	0,68
Gradstreuung	0,83	13,0	10,5
groesster Grad	0,58	22	21

Neun zünden, elf sterben. Von zwei Instanzen gleicher Größe zündet in neun von zehn Fällen die mit mehr Zündpunkten — der Mechanismus ist also kein Ensemble-Artefakt. Praktisch: in O(m²) entscheiden, ob sich das polynomiale Verfahren überhaupt lohnt.

Und ein Teil-Nein: λ = 1 taugt in dieser rundenweisen Fassung nicht als parameterfreies Kriterium. Instanz #19 hat λ₃ = 1,05 und stirbt, #18 hat 1,31 und zündet. Die zustandsabhängige Fassung aus Zwei Attraktoren — R als Funktion des angesammelten Abschlusses — ist die richtige.

Code & Daten ansehen — die Saat und was sie voraussagt

werkbank.py

def saat(bloecke, w=3):
    """Zuendpunkte: Paare, deren Verschmelzung wieder Breite <= w hat.

    Nur diese koennen die Lawine anstossen.  O(m^2), kein Abschluss noetig.
    """
    v = 0
    for i in range(len(bloecke)):
        for j in range(i + 1, len(bloecke)):
            r = verschmelzen(bloecke[i], bloecke[j])
            if r is not None and breite(r) <= w:
                v += 1
    return v

Ausgabe — instanzweise.py 56 20

  # 2  Saat   91  lam [0.38, 0.91, 0.86]  ->  ZUENDET bei |228033| nach 32 Runden  (331s)
  # 3  Saat   81  lam [0.34, 0.53, 0.67]  ->  stirbt  bei |446|    nach 11 Runden  (0s)
  # 5  Saat  110  lam [0.46, 1.21, 0.91]  ->  ZUENDET bei |228033| nach 24 Runden  (1217s)
  # 8  Saat   64  lam [0.27, 0.34, 0.36]  ->  stirbt  bei |338|    nach  5 Runden  (0s)
  #18  Saat   76  lam [0.32, 0.68, 1.31]  ->  ZUENDET bei |221982| nach 39 Runden  (242s)
  #19  Saat   92  lam [0.38, 1.01, 1.05]  ->  stirbt  bei |913|    nach 18 Runden  (0s)

  9 zuenden, 11 sterben.
    Saat             AUC 0.91   Median zuendend 95.00  sterbend 79.00
    lambda_1         AUC 0.91
    lambda_2         AUC 0.86
    lambda_3         AUC 0.85
    Gradstreuung     AUC 0.83
    groesster Grad   AUC 0.58

6 von 20 Zeilen gezeigt. n = 56, α = 4,26, nur unlösbare. Die Saat kostet 0 s, der Abschluss bis zu 1 217 s.

5 Der Konfliktgraph: eine strukturelle Route, und sie ist dominiert

Blöcke sind gemeinsam verträglich genau dann, wenn sie es paarweise sind — für Unterwürfel lassen sich die Teilbelegungen einfach vereinigen (3 000 Proben, 0 Abweichungen). Damit sind die verträglichen Familien exakt die unabhängigen Mengen des Konfliktgraphen der Klauseln, und die ganze Ein-/Ausschluss-Reihe ist dessen volumengewichtetes Unabhängigkeitspolynom. Der Graph hat 4,26n Knoten bei mittlerem Grad 19,0, konstant von n = 16 bis 256.

Das legt Leichtigkeit über die Struktur nahe statt über die Operation: kleine Baumweite des Konfliktgraphen machte die Lösungszahl polynomial. Gemessen (min-fill-Schranke, Konflikt / primal):

Familie	n=32	n=64	n=96	lösbar
zufällig p=0,5	75 / 22	149 / 44	227 / 65	gemischt
schief p=0,15	35 / 22	73 / 44	108 / 66	1,00
lokal W=8	46 / 13	52 / 13	49 / 13	0,00
lokal W=16	70 / 21	99 / 26	104 / 26	0,00
lokal+schief	21 / 12	21 / 13	20 / 13	1,00

Der gesuchte Bereich — Konfliktgraph schmal, primaler breit — ist leer, und er kann nicht anders sein: 4,26n Knoten bei gleicher Dichte gegen n Knoten. Wo der Konfliktgraph schmal ist, ist der primale schmaler, bei n = 96 um Faktor 2³⁶. Die Umformulierung bleibt korrekt und erklärend — sie liefert die dritte unabhängige Herleitung der 2^1,57n Reihenkosten — als Verfahren ist sie dominiert.

6 Was daran neu ist, und was nicht

Dieser Bericht entstand, indem die Blockdarstellung von Grund auf neu gebaut wurde, ohne den vorhandenen Korpus vorher zu lesen. Mehrere Befunde erwiesen sich als Wiederherleitung, und sie stehen dort, wo sie hingehören:

Befund	stand schon in
der Zündfunke: Paare mit zwei gemeinsamen Stellen	Warum das Sättigungsrezept verhungert (ZUENDUNG)
die Kante bei n ≈ 48	Zwei Attraktoren — dort n = 49,2, ausgerechnet statt gemessen
Bistabilität des Abschlusses	Zwei Attraktoren
der Verzweigungsfaktor	Zwei Attraktoren, und dort besser gefasst
Breite 3 trägt bis n ≈ 55	Wo Asymptopia anfängt

Neu ist, was in den Abschnitten 1 bis 5 steht: das durchgehaltene Blockvokabular, die sieben Ebenen und der Halbring, die Breiteninvarianz der Zünddichte, die Saat als a-priori-Kennzahl und der Konfliktgraph. Dass dieselbe Struktur zu denselben Befunden führt, spricht für die Befunde und gegen das Vorgehen.

Eine Werkbank gehört dazu. werkbank.py hält eine Instanz als Liste von Verbotsblöcken und macht beide Griffe einzeln greifbar, dazu Saat, Vorrat, Zünddichte, Abschluss, Entscheidung, schrittweises Sammeln und den Polymorphismus-Test:

from werkbank import Instanz
I = Instanz.zufall(n=20, alpha=4.26, saat=1)   # oder .aus_dimacs("x.cnf")
print(I.bericht())