k-SAT · Kartographie · 25. August 2026

Karte des Instanzraums

Nicht der Lösungsraum, sondern der Raum aller Instanzen. Erfüllbarkeit ist darauf eine monotone Funktion — der Raum hat also einen Rand, eine Höhe und eine lokale Geometrie. Alle drei sind exakt vermessen. Und trotzdem lässt sich die Zugehörigkeit nicht ausrechnen; auch dafür gibt es einen gemessenen Grund.

Exakt über den vollständigen Würfel, n = 10 … 22 · instanzraum.py · randnaehe.py

6 528

Dimensionen bei n = 18

monoton

Klausel dazu kippt nur SAT→UNSAT

95 %

liegen 1 Klausel von der Gegenmenge

C(b,3)

tötende Einzelklauseln, exakt

1 · Der Raum ist ein Verband, kein Nebel

Bei n Variablen gibt es 8·C(n,3) mögliche Klauseln — Tripel mal Vorzeichenmuster. Eine Instanz ist eine Teilmenge davon, der Instanzraum also der Würfel {0,1}^8·C(n,3). Bei n = 18 sind das 6 528 Dimensionen.

Ein einziger Satz ordnet das Ganze: eine Klausel hinzufügen kann nur SAT → UNSAT kippen, nie zurück.

Die UNSAT-Menge ist nach oben abgeschlossen — ein Filter.
Die SAT-Menge ist nach unten abgeschlossen — ein Ideal.
Der Rand ist die Antikette der minimal unerfüllbaren Formeln.
Der Übergang bei α = 4,267 ist ein scharfer Schwellenwert einer monotonen Eigenschaft — die Lage, für die Friedguts Satz gilt.

2 · Ein Schnitt durch den Raum

6 528 Dimensionen lassen sich nicht zeichnen — ein zweidimensionaler Schnitt schon. Zwei unabhängige Klauselströme A und B; das Feld an der Stelle (i, j) ist die Instanz aus den ersten i Klauseln von A und den ersten j von B. Nach rechts und nach oben werden also Klauseln hinzugefügt.

Weil Erfüllbarkeit monoton ist, muss das lösbare Gebiet unten links zusammenhängen und der Rand eine Treppe sein, die nie zurückläuft. Genau das ist zu sehen — und die Treppe ist ausgefranst, nicht glatt.

n = 18 · Gitter 81 × 81 · 6 561 Instanzen einzeln exakt gelöst

Klauseln aus Strom B →

Klauseln aus Strom A →

Zeiger über die Karte bewegen.

Die gestrichelte Diagonale ist i + j = 77, also α = 4,26 — die Schwelle. Sie schneidet die Treppe ungefähr dort, wo sie verläuft, aber nicht entlang: gleiche Klauselzahl heisst nicht gleiche Antwort.

Kontrolle: d wächst entlang beider Achsen nirgends rückwärts — auf allen 6 561 Feldern geprüft. Die Monotonie ist damit nicht behauptet, sondern nachgerechnet.

3 · Warum sich die Koordinate nicht ausrechnen lässt

Wenn der Raum so sauber geordnet ist — warum kann man dann nicht die Koordinaten einer Eingabeinstanz ausrechnen und nachsehen, ob sie im Gebiet liegt? Weil es genau zwei Sorten Koordinaten gibt und dazwischen nichts.

Billige Koordinaten

α, Gradverteilung, Unwucht, Frontbreite, Baumweite. In Polynomzeit ausrechenbar — aber der Rand ist keine Niveaumenge davon. Zwei Instanzen können in jeder dieser Zahlen übereinstimmen und verschieden antworten.

Exakte Koordinaten

d, Rückgrat, Lösungszahl. Sie bestimmen die Zugehörigkeit — aber sie auszurechnen ist mindestens so schwer wie das Problem selbst. d = 0 zu prüfen ist SAT.

Dazwischen ist nichts, und das ist kein Mangel an Fleiss: eine billige Koordinate, deren Niveaumenge der Rand wäre, wäre ein Polynomzeitverfahren für SAT. Die Frage „warum rechnet man die Koordinate nicht einfach aus" ist die P-gegen-NP-Frage in Koordinatenform.

Der geometrische Grund dahinter ist messbar. An der Schwelle hat keine der beiden Mengen ein Inneres:

Abstand zur Gegenmenge in Klauseln · n = 18 · je 150 Instanzen
α	Art	Anteil	Abstand 1	Abstand 2+	mittlerer Abstand
3,50	SAT	98 %	52 %	48 %	1,48
4,00	SAT	85 %	91 %	9 %	1,09
4,26	SAT	67 %	95 %	5 %	1,05
4,26	UNSAT	33 %	96 %	4 %	1,04
5,00	UNSAT	67 %	85 %	15 %	1,15
6,00	UNSAT	95 %	33 %	67 %	1,80

Bei α = 4,26 liegen 95 % der lösbaren Instanzen eine einzige Klausel von der unlösbaren Menge entfernt — und 96 % der unlösbaren eine einzige Klausel von der lösbaren. Es gibt an der Schwelle kein Inneres, in dem man liegen könnte. Der Rand ist überall.

lösbar unlösbar

500 Instanzen bei n = 18, α = 4,26, aufgetragen über den zwei stärksten billigen Strukturgrössen dieses Projekts. Die Gradstreuung liegt bei 10,873 (lösbar) gegen 10,889 (unlösbar) — die Wolken liegen ineinander.

4 · Der Rand, und wie er mit n schärfer wird

n = 10 n = 14 n = 18 n = 22 α = 4,267

Der Abstand α_c(n) − 4,267 fällt 0,719 → 0,524 → 0,447 → 0,276, die Breite von 1,879 auf 1,599. Beides passt zu n^−1/ν mit 1/ν ≈ 0,8.

Anteil lösbarer Instanzen · exakt · 600 / 600 / 400 / 150 Instanzen je Zelle
n	3,00	3,50	4,00	4,26	4,50	5,00	5,50	6,00	α_c(n)	Breite
10	1,00	0,96	0,85	0,75	0,67	0,49	0,32	0,22	4,986	—
14	1,00	0,97	0,85	0,73	0,66	0,39	0,23	0,11	4,791	—
18	1,00	0,97	0,84	0,73	0,61	0,35	0,13	0,04	4,714	1,879
22	1,00	0,98	0,83	0,64	0,53	0,22	0,05	0,02	4,543	1,599

5 · Die Höhe über dem Rand

d(F) = min über alle Belegungen der Zahl verletzter Klauseln

d = 0 heisst lösbar. Und d ist zugleich die kleinste Zahl von Klauseln, die man streichen muss, damit F lösbar wird — der Abstand zum Rand in der Streichmetrik. Eine echte Höhenfunktion: monoton beim Hinzufügen, null genau auf dem Ideal.

n = 10 n = 14 n = 18 n = 22

d/n ist intensiv: bei α = 12 messen wir 0,515 / 0,514 / 0,498 / 0,503 — über eine Verdopplung von n hinweg dieselbe Zahl.

6 · Die lokale Geometrie: wie spitz ist der Rand?

Von der SAT-Seite nach oben

Eine hinzugefügte Klausel macht F genau dann unerfüllbar, wenn alle Lösungen sie verletzen — also wenn alle Lösungen auf ihren drei Variablen dasselbe Muster tragen. Das sind exakt die Tripel aus dem Rückgrat, je Tripel ein Vorzeichenmuster.

tötende Klauseln = C(b, 3)

Von der UNSAT-Seite nach unten

Die kritischen Klauseln: Streichen macht lösbar. Genau die Klauseln, die als einzige einen Punkt des Würfels verletzen — der Ausgang aus dem Filter, eine Kante tief.

Ausgänge = #{c : ∃x, c ist einziger Verletzer}

Kontrolle der Formel · alle 960 Klauseln bei n = 10 einzeln angehängt und geprüft
α	Lösungen	Rückgrat b	C(b,3)	roh gezählt	gleich
3,00	27	0	0	0	ja
4,00	8	3	1	1	ja
4,26	7	3	1	1	ja
4,60	3	4	4	4	ja

von SAT nach oben (Anteil aller 6 528 Klauseln) von UNSAT nach unten (Anteil der eigenen Klauseln)

n = 18, je 120 Instanzen. Von unten wird der Rand immer spitzer, von oben immer dicker. Treiber ist das Rückgrat: 0,05·n bei α = 3, 0,84·n bei α = 5.

7 · Was die Karte sagt

Der Instanzraum ist geordnet, nicht diffus. Monotonie gibt ihm Filter, Ideal und eine Randantikette — und macht die Schwellenphänomene zu Sätzen statt zu Beobachtungen.
Es gibt eine natürliche Höhe. d ist zugleich Streichabstand zum Rand und MAXSAT-Defizit, und d/n ist intensiv.
Aber es gibt kein Inneres. An der Schwelle liegen 95 % der Instanzen eine Klausel von der Gegenmenge. Ein Gebiet ohne Inneres lässt sich nicht durch Koordinaten eingrenzen.
Und die Härte steht ohnehin nicht auf dieser Karte. d, Rückgrat, Randabstand — alles Eigenschaften der Instanz, alle sauber geordnet, und keine sagt, wie lange ein Solver braucht.

instanzraum.py · randnaehe.py · INSTANZRAUM.md

Code & Daten ansehen — Rand P(lösbar) und Höhe d über α und n

instanzraum.py — Rand und Höhe über dem vollständigen Würfel

"""Der INSTANZRAUM statt des Loesungsraums.

Eine Instanz ist eine Teilmenge der 8*C(n,3) moeglichen Klauseln. Der Raum ist
also der Wuerfel {0,1}^(8*C(n,3)) -- und Erfuellbarkeit ist darauf eine
MONOTONE Funktion: Klausel hinzufuegen kann nur SAT->UNSAT kippen, nie zurueck.

Damit ist:
  * die UNSAT-Menge nach oben abgeschlossen (ein Filter),
  * die SAT-Menge nach unten abgeschlossen (ein Ideal),
  * der Rand die Antikette der minimal unerfuellbaren Formeln,
  * und es gibt eine natuerliche HOEHE ueber dem Rand:

      d(F) = min ueber alle Belegungen der Zahl verletzter Klauseln

  d = 0 genau dann, wenn F loesbar ist. d ist zugleich die kleinste Zahl von
  Klauseln, die man streichen muss, um F loesbar zu machen -- also der exakte
  Abstand zum Rand in der Streichmetrik. (MAXSAT-Defizit.)

A  Der Rand: P(loesbar) ueber alpha, und wie scharf er mit n wird.
B  Die Hoehe: d und d/n ueber alpha und n.
C  Die Entartung: wieviele Belegungen erreichen das Minimum.
"""
import sys
import numpy as np
from streichliste import bits, rand_cnf, maske, K

def hoehe(n, B, vs, sg):
    """(d, Entartung) -- d = min Zahl verletzter Klauseln.
    Der verletzende Bereich einer Klausel ist ein Teilwuerfel: als (2,)*n
    umgeformtes Feld ist das ein Schnitt, also O(2^(n-k)) statt O(2^n)."""
    kc = np.zeros((2,) * n, dtype=np.int16)
    leer = [slice(None)] * n
    for c in range(len(vs)):
        idx = list(leer)
        for j in range(K):
            idx[int(vs[c, j])] = 0 if sg[c, j] else 1
        kc[tuple(idx)] += 1
    d = int(kc.min())
    return d, int((kc == d).sum())

def teilA(ns, alphas, proben, seed=151):
    if not isinstance(proben, dict):
        proben = {n: proben for n in ns}
    print("== A  Der Rand: P(loesbar) ueber alpha")
    print(f"{'n':>4} " + " ".join(f"{a:>7.2f}" for a in alphas)
          + f" {'a_c(n)':>8} {'Breite':>8}")
    tab = {}
    for n in ns:
        rng = np.random.default_rng(seed + n)
        B = bits(n)
        ps = []
        pn = proben[n]
        for a in alphas:
            m = round(a * n)
            s = 0
            for _ in range(pn):
                vs, sg = rand_cnf(n, m, rng)
                d, _ = hoehe(n, B, vs, sg)
                s += (d == 0)
            ps.append(s / pn)
        tab[n] = ps
        p = np.array(ps); aa = np.array(alphas)
        def kreuz(ziel):
            for i in range(len(p) - 1):
                if p[i] >= ziel >= p[i + 1]:
                    t = (p[i] - ziel) / max(p[i] - p[i + 1], 1e-9)
                    return aa[i] + t * (aa[i + 1] - aa[i])
            return float('nan')
        ac, hi, lo = kreuz(0.5), kreuz(0.9), kreuz(0.1)
        print(f"{n:>4} " + " ".join(f"{v:>7.2f}" for v in ps)
              + f" {ac:>8.3f} {lo-hi:>8.3f}")
    return tab

def teilBC(ns, alphas, proben, seed=163):
    if not isinstance(proben, dict):
        proben = {n: proben for n in ns}
    print("\n== B/C  Die Hoehe ueber dem Rand: d = min verletzte Klauseln")
    print(f"{'n':>4} {'alpha':>6} {'m':>5} {'P(d=0)':>8} {'d Mittel':>9} "
          f"{'d/n':>8} {'d Median':>9} {'Entartung bei d':>16}")
    for n in ns:
        rng = np.random.default_rng(seed + n)
        B = bits(n)
        for a in alphas:
            m = round(a * n)
            ds, gs = [], []
            for _ in range(proben[n]):
                vs, sg = rand_cnf(n, m, rng)
                d, g = hoehe(n, B, vs, sg)
                ds.append(d); gs.append(g)
            ds = np.array(ds)
            print(f"{n:>4} {a:>6.2f} {m:>5} {(ds==0).mean():>8.2f} "
                  f"{ds.mean():>9.2f} {ds.mean()/n:>8.4f} {np.median(ds):>9.0f} "
                  f"{np.mean(gs):>16.1f}")

# ---------------------------------------------------------------- D
def lokale_geometrie(n, vs, sg):
    """Wieviele EINZELNE Klauselaenderungen kippen die Antwort?

    Von der SAT-Seite nach oben: eine hinzugefuegte Klausel macht F genau dann
    unerfuellbar, wenn ALLE Loesungen sie verletzen -- also wenn alle Loesungen
    auf ihren drei Variablen dasselbe Muster tragen. Das sind exakt die Tripel
    aus dem RUECKGRAT (Variablen, auf denen alle Loesungen uebereinstimmen),
    und je Tripel genau ein Vorzeichenmuster:

        Zahl der toetenden Klauseln  =  C(b, 3)     mit b = Rueckgratgroesse.

    Von der UNSAT-Seite nach unten: die kritischen Klauseln (Streichen macht
    loesbar) -- die Punkte, die nur von dieser einen Klausel verletzt werden.
    """
    from math import comb
    kc = np.zeros((2,) * n, dtype=np.int16)
    ks = np.zeros((2,) * n, dtype=np.int32)
    leer = [slice(None)] * n
    for c in range(len(vs)):
        idx = list(leer)
        for j in range(K):
            idx[int(vs[c, j])] = 0 if sg[c, j] else 1
        kc[tuple(idx)] += 1
        ks[tuple(idx)] += c + 1
    kcf = kc.ravel(); ksf = ks.ravel()
    N = 1 << n
    if (kcf == 0).any():                                   # loesbar
        loes = np.flatnonzero(kcf == 0)
        b = 0
        for v in range(n):
            bit = (loes >> v) & 1
            if bit.min() == bit.max():
                b += 1
        return "SAT", len(loes), b, comb(b, 3), 8 * comb(n, 3)
    einzig = ksf[kcf == 1]
    krit = int((np.bincount(einzig, minlength=len(vs) + 1)[1:] > 0).sum())
    return "UNSAT", 0, 0, krit, len(vs)

def teilD(ns, alphas, proben, seed=181):
    from math import comb
    print("\n== D  Lokale Geometrie des Randes: kippende Einzelaenderungen")
    print(f"{'n':>4} {'alpha':>6} {'Art':>6} {'Anteil':>7} {'Rueckgrat b':>12} "
          f"{'b/n':>7} {'kippende Richtungen':>20} {'von':>9} {'Anteil':>9}")
    for n in ns:
        rng = np.random.default_rng(seed + n)
        for a in alphas:
            m = round(a * n)
            S, U = [], []
            for _ in range(proben):
                vs, sg = rand_cnf(n, m, rng)
                art, nl, b, kipp, ges = lokale_geometrie(n, vs, sg)
                (S if art == "SAT" else U).append((b, kipp, ges))
            for art, L in (("SAT", S), ("UNSAT", U)):
                if not L:
                    continue
                b = np.mean([x[0] for x in L]); kp = np.mean([x[1] for x in L])
                ge = np.mean([x[2] for x in L])
                print(f"{n:>4} {a:>6.2f} {art:>6} {len(L)/proben:>7.0%} "
                      f"{b:>12.1f} {b/n:>7.3f} {kp:>20.1f} {ge:>9.0f} "
                      f"{kp/max(ge,1):>9.2%}")

if __name__ == "__main__":
    w = sys.argv[1] if len(sys.argv) > 1 else "alle"
    A = [3.0, 3.5, 4.0, 4.26, 4.5, 5.0, 5.5, 6.0]
    if w in ("alle", "A"): teilA([10, 14, 18, 22, 26], A,
                                 {10: 600, 14: 600, 18: 400, 22: 150, 26: 40})
    if w in ("alle", "B"): teilBC([10, 14, 18, 22], [3.0, 4.26, 5.0, 6.0, 8.0, 12.0],
                                  {10: 300, 14: 300, 18: 200, 22: 80})
    if w in ("alle", "D"): teilD([14, 18], [3.0, 4.0, 4.26, 4.6, 5.0], 120)

python3 instanzraum.py B — Live-Ausgabe, exakt über 2ⁿ (n bis 22)


== B/C  Die Hoehe ueber dem Rand: d = min verletzte Klauseln
   n  alpha     m   P(d=0)  d Mittel      d/n  d Median  Entartung bei d
  10   3.00    30     0.99      0.01   0.0010         0             18.5
  10   4.26    43     0.74      0.26   0.0260         0              6.7
  10   5.00    50     0.54      0.49   0.0493         0              4.8
  10   6.00    60     0.19      1.07   0.1067         1              3.7
  10   8.00    80     0.03      2.25   0.2250         2              3.0
  10  12.00   120     0.00      5.15   0.5150         5              2.2
  14   3.00    42     1.00      0.00   0.0002         0             56.3
  14   4.26    60     0.73      0.27   0.0195         0             10.4
  14   5.00    70     0.42      0.65   0.0462         1              7.7
  14   6.00    84     0.12      1.40   0.0998         1              5.7
  14   8.00   112     0.01      3.12   0.2226         3              3.7
  14  12.00   168     0.00      7.19   0.5136         7              2.7
  18   3.00    54     1.00      0.00   0.0000         0            188.5
  18   4.26    77     0.70      0.30   0.0169         0             19.1
  18   5.00    90     0.39      0.77   0.0425         1             11.3
  18   6.00   108     0.09      1.62   0.0903         2              6.6
  18   8.00   144     0.00      3.78   0.2100         4              4.6
  18  12.00   216     0.00      8.96   0.4978         9              2.8
  22   3.00    66     1.00      0.00   0.0000         0            647.6
  22   4.26    94     0.64      0.36   0.0165         0             38.1
  22   5.00   110     0.23      0.94   0.0426         1             13.9
  22   6.00   132     0.04      1.90   0.0864         2              9.1
  22   8.00   176     0.00      4.76   0.2165         5              6.9
  22  12.00   264     0.00     11.06   0.5028        11              4.2

exakt über den vollständigen Würfel 25. August 2026