Warum Aggregate ueber den Belegungsraum nicht zwischen SAT und UNSAT unterscheiden koennen — und was daraus folgt.
Acht unabhaengige Zugaenge ueber die Loesungsmenge — Backbone, Reparaturmenge |R|, Survey Propagation, Kavitaet, Restgeometrie, Backbone-Bahn, und jetzt auch die exakten Momente μ₁…μ₃ — haben keinerlei Vorhersagekraft fuer die Widerlegungskosten (AUC ≈ 0,5, Korrelation r ≤ 0,15). Die einzige Ausnahme ist die Ordnung d(50%), die das Ableitungsverhalten misst (r ≈ 0,56, dreimal repliziert).
Betrachte die Energieverteilung einer 3-CNF-Formel:
N(k) = |{x ∈ {0,1}n : c(x) = k}| mit c(x) = Zahl der von x verletzten Klauseln
Sei F eine uniforme Zufalls-3-CNF an der Schwelle. Fuer eine feste Belegung x, jede Klausel wird von genau 1/8 aller Belegungen falsifiziert. Zwei Klauseln, die keine Variable teilen, sind unabhaengig. Der Anteil der Paare mit gemeinsamen Variablen ist O(1/n). Folglich:
Jede endliche Menge von Klausel-Korrelationen (Paare, Tripel, …) erzeugt Abweichungen von O(1), die fuer n → ∞ unter der Masse von N(k≥1) ∼ O(2n) verschwinden. Die einzige nicht-hebbare Abweichung ist N(0): eine erfuellende Belegung verletzt per Definition keine Klausel, also ist N(0) > 0 fuer SAT und = 0 fuer UNSAT.
Dieser Unterschied ist jedoch exponentiell klein: der Erwartungswert von N(0) einer Zufallsformel ist 2n·(7/8)m = (2·(7/8)α)n. Bei α = 4,267 ist die Basis 2·(7/8)4,267 ≈ 2·0,545 = 1,090. Der relative Anteil N(0)/2n faellt wie 0,545n — exponentiell. Bei n = 200 liegt er bei ≈10-53.
Fuer n = 16 (m = 68, α = 4,25), 300 Instanzen, brute force ueber alle 216 = 65536 Belegungen:
| k | N(k) SAT | N(k) UNSAT | Δ | Cohen’s d | B(68, 1/8) |
|---|---|---|---|---|---|
| 0 | 1,51·10-4 | 0 | -1,51·10-4 | -1,09 | 1,14·10-4 |
| 1 | 1,32·10-3 | 4,66·10-4 | -8,58·10-4 | -1,14 | 1,11·10-3 |
| 2 | 5,97·10-3 | 3,49·10-3 | -2,47·10-3 | -1,08 | 5,30·10-3 |
| 3 | 1,78·10-2 | 1,33·10-2 | -4,49·10-3 | -1,00 | 1,66·10-2 |
| 4 | 4,01·10-2 | 3,48·10-2 | -5,22·10-3 | -0,81 | 3,86·10-2 |
| 5 | 7,15·10-2 | 6,87·10-2 | -2,82·10-3 | -0,46 | 7,06·10-2 |
| 6 | 1,05·10-1 | 1,08·10-1 | +2,37·10-3 | +0,52 | 1,06·10-1 |
| 7 | 1,32·10-1 | 1,39·10-1 | +6,96·10-3 | +1,06 | 1,34·10-1 |
| 8 | 1,44·10-1 | 1,52·10-1 | +8,05·10-3 | +0,78 | 1,46·10-1 |
| 9 | 1,37·10-1 | 1,44·10-1 | +6,66·10-3 | +0,60 | 1,39·10-1 |
| 10 | 1,16·10-1 | 1,20·10-1 | +3,91·10-3 | +0,45 | 1,17·10-1 |
Die Originalinstanzen dieser Tabelle sind nicht mehr rekonstruierbar (kein gespeichertes Skript, keine feste Saat). Der folgende Beleg reproduziert dieselbe Messung frisch, mit persistiertem Skript und fester Saat — dieselbe Grössenordnung, dasselbe Muster, eigene (nicht identische) Zahlen.
"""Die Energieverteilung N(k) fuer SAT und UNSAT, exakt -- der Beleg hinter
zwei-achsen-trennung.html.
c(x) = Zahl der von Belegung x verletzten Klauseln. F unerfuellbar genau
dann, wenn c hat kein Minimum 0. N(k)/2^n ist die Verteilung von c ueber
alle 2^n Belegungen, exakt (kein Sampling) fuer kleine n.
Aufruf: python3 energieverteilung.py [n=16] [alpha=4.25] [anzahl=300] [seed=42]
Schreibt daten_energieverteilung.json.
"""
import json
import sys
import numpy as np
from streichliste import K, bits, maske, rand_cnf
def c_verteilung(n, vs, sg, B):
"""c(x) fuer alle 2^n Belegungen als int-Array."""
c = np.zeros(1 << n, dtype=np.int32)
for i in range(len(vs)):
c += maske(B, vs[i], sg[i])
return c
def lauf(n=16, alpha=4.25, anzahl=300, seed=42):
m = round(alpha * n)
B = bits(n)
rng = np.random.default_rng(seed)
# Je Instanz EIN Wert N(k)/2^n -- das ist die Stichprobeneinheit fuer
# Cohen's d, nicht die einzelne Belegung (die sind innerhalb einer
# Instanz nicht unabhaengig).
sat_dichten = [] # Liste von (m+1,)-Arrays, je Instanz
unsat_dichten = []
sat_mu1 = [] # erstes Moment je Instanz, fuer die Momente-Tabelle
unsat_mu1 = []
sat_mu2 = []
unsat_mu2 = []
n_sat = n_unsat = 0
while n_sat + n_unsat < anzahl:
vs, sg = rand_cnf(n, m, rng)
c = c_verteilung(n, vs, sg, B)
hist = np.bincount(c, minlength=m + 1).astype(np.float64) / (1 << n)
cf = c.astype(np.float64)
if c.min() == 0:
sat_dichten.append(hist); sat_mu1.append(cf.mean()); sat_mu2.append((cf**2).mean())
n_sat += 1
else:
unsat_dichten.append(hist); unsat_mu1.append(cf.mean()); unsat_mu2.append((cf**2).mean())
n_unsat += 1
sat_dichten = np.array(sat_dichten) # (n_sat, m+1)
unsat_dichten = np.array(unsat_dichten)
sat_dicht = sat_dichten.mean(axis=0)
unsat_dicht = unsat_dichten.mean(axis=0)
mu1_sat, var_sat = float(np.mean(sat_mu1)), float(np.mean(sat_mu2) - np.mean(sat_mu1)**2)
mu1_unsat, var_unsat = float(np.mean(unsat_mu1)), float(np.mean(unsat_mu2) - np.mean(unsat_mu1)**2)
# Binomialreferenz B(m, 1/8)
from math import comb
p = 1.0 / (2 ** K)
binom = np.array([comb(m, k) * p ** k * (1 - p) ** (m - k) for k in range(m + 1)])
zeilen = []
for k in range(11):
s, u, b = sat_dicht[k], unsat_dicht[k], binom[k]
delta = u - s
# Cohen's d ueber die INSTANZEN: je Instanz ein N(k)/2^n-Wert,
# gepoolte Standardabweichung ueber die beiden Stichproben.
var_s = float(sat_dichten[:, k].var(ddof=1)) if n_sat > 1 else 0.0
var_u = float(unsat_dichten[:, k].var(ddof=1)) if n_unsat > 1 else 0.0
sd = np.sqrt(((n_sat - 1) * var_s + (n_unsat - 1) * var_u) / max(n_sat + n_unsat - 2, 1))
d = delta / sd if sd > 1e-15 else 0.0
zeilen.append({"k": k, "sat": float(s), "unsat": float(u),
"delta": float(delta), "cohens_d": float(d), "binom": float(b)})
aus = {"n": n, "m": m, "alpha": alpha, "anzahl": anzahl, "seed": seed,
"n_sat": n_sat, "n_unsat": n_unsat,
"mu1_sat": mu1_sat, "mu2_sat": var_sat + mu1_sat ** 2, "var_sat": var_sat,
"mu1_unsat": mu1_unsat, "mu2_unsat": var_unsat + mu1_unsat ** 2, "var_unsat": var_unsat,
"mu1_binom": m * p, "mu2_binom": m * p * (1 - p) + (m * p) ** 2, "var_binom": m * p * (1 - p),
"zeilen": zeilen}
print(f"n={n} m={m} alpha={alpha} {n_sat} SAT / {n_unsat} UNSAT von {anzahl}")
print(f"{'k':>3} {'N(k) SAT':>12} {'N(k) UNSAT':>12} {'Delta':>12} {'Cohens d':>9} {'B(m,1/8)':>12}")
for z in zeilen:
print(f"{z['k']:3d} {z['sat']:12.3e} {z['unsat']:12.3e} {z['delta']:+12.3e} "
f"{z['cohens_d']:+9.2f} {z['binom']:12.3e}")
print(f"\n mu1 SAT {mu1_sat:.6f} UNSAT {mu1_unsat:.6f} Binomial {aus['mu1_binom']:.6f}")
print(f" var SAT {var_sat:.3f} UNSAT {var_unsat:.3f} Binomial {aus['var_binom']:.3f}")
with open("daten_energieverteilung.json", "w") as f:
json.dump(aus, f, indent=1)
print("\ngespeichert -> daten_energieverteilung.json")
if __name__ == "__main__":
a = sys.argv[1:]
lauf(
n=int(a[0]) if len(a) > 0 else 16,
alpha=float(a[1]) if len(a) > 1 else 4.25,
anzahl=int(a[2]) if len(a) > 2 else 300,
seed=int(a[3]) if len(a) > 3 else 42,
)
| k | N(k) SAT | N(k) UNSAT | Δ | Cohen's d | B(68, 1/8) |
|---|---|---|---|---|---|
| 0 | 1.537e-04 | 0.000e+00 | -1.537e-04 | -0.84 | 1.139e-04 |
| 1 | 1.366e-03 | 3.578e-04 | -1.008e-03 | -1.22 | 1.107e-03 |
| 2 | 6.148e-03 | 3.089e-03 | -3.059e-03 | -1.27 | 5.295e-03 |
| 3 | 1.828e-02 | 1.292e-02 | -5.359e-03 | -1.14 | 1.664e-02 |
| 4 | 4.070e-02 | 3.464e-02 | -6.064e-03 | -0.93 | 3.864e-02 |
| 5 | 7.204e-02 | 6.843e-02 | -3.605e-03 | -0.58 | 7.065e-02 |
| 6 | 1.055e-01 | 1.075e-01 | +2.029e-03 | +0.43 | 1.060e-01 |
| 7 | 1.315e-01 | 1.396e-01 | +8.136e-03 | +1.17 | 1.341e-01 |
| 8 | 1.426e-01 | 1.531e-01 | +1.051e-02 | +1.00 | 1.461e-01 |
| 9 | 1.359e-01 | 1.452e-01 | +9.338e-03 | +0.82 | 1.391e-01 |
| 10 | 1.156e-01 | 1.203e-01 | +4.709e-03 | +0.54 | 1.172e-01 |
n=16, m=68, α=4.25, 209 SAT / 91 UNSAT von 300 Instanzen, Saat 42. μ₁ = 8.5000 (SAT) / 8.5000 (UNSAT) exakt gleich — Var 7.750 vs 6.738 vs Binomial 7.438.
{
"n": 16,
"m": 68,
"alpha": 4.25,
"anzahl": 300,
"seed": 42,
"n_sat": 209,
"n_unsat": 91,
"mu1_sat": 8.5,
"mu2_sat": 79.9995514354067,
"var_sat": 7.749551435406701,
"mu1_unsat": 8.5,
"mu2_unsat": 78.98832417582418,
"var_unsat": 6.738324175824175,
"mu1_binom": 8.5,
"mu2_binom": 79.6875,
"var_binom": 7.4375,
"zeilen": [
{
"k": 0,
"sat": 0.00015368301902661484,
"unsat": 0.0,
"delta": -0.00015368301902661484,
"cohens_d": -0.8428776819657726,
"binom": 0.00011390626342427423
},
{
"k": 1,
"sat": 0.0013656251168136962,
"unsat": 0.0003578269874656593,
"delta": -0.001007798129348037,
"cohens_d": -1.218662506835455,
"binom": 0.0011065179875500925
},
{
"k": 2,
"sat": 0.006148269872345993,
"unsat": 0.003089317908653846,
"delta": -0.0030589519636921468,
"cohens_d": -1.2660746936872362,
"binom": 0.005295478940418301
},
{
"k": 3,
"sat": 0.018277400988711126,
"unsat": 0.012918325570913462,
"delta": -0.005359075417797664,
"cohens_d": -1.14002595541737,
"binom": 0.01664293381274323
},
{
"k": 4,
"sat": 0.040703951456900415,
"unsat": 0.03463963099888393,
"delta": -0.006064320458016484,
"cohens_d": -0.9328236708114455,
"binom": 0.038635382065296785
},
{
"k": 5,
"sat": 0.07203688918118271,
"unsat": 0.06843164464929602,
"delta": -0.003605244531886695,
"cohens_d": -0.581205845340745,
"binom": 0.07064755577654268
},
{
"k": 6,
"sat": 0.10549700431276167,
"unsat": 0.10752633901742789,
"delta": 0.002029334704666222,
"cohens_d": 0.4266047622969223,
"binom": 0.10597133366481402
},
{
"k": 7,
"sat": 0.1314697265625,
"unsat": 0.13960618239182693,
"delta": 0.008136455829326927,
"cohens_d": 1.1661909376261517,
"binom": 0.13408617729017286
},
{
"k": 8,
"sat": 0.14255308306388306,
"unsat": 0.15306359594994848,
"delta": 0.010510512886065415,
"cohens_d": 0.9968310563644459,
"binom": 0.14605815740536685
},
{
"k": 9,
"sat": 0.13587068256578946,
"unsat": 0.14520850548377404,
"delta": 0.009337822917984573,
"cohens_d": 0.819348875198814,
"binom": 0.13910300705273035
},
{
"k": 10,
"sat": 0.11562307257401316,
"unsat": 0.1203319842998798,
"delta": 0.004708911725866641,
"cohens_d": 0.5390461340779255,
"binom": 0.11724396308730128
}
]
}Der einzige sichtbare Unterschied liegt bei k=0 (UNSAT-Kurve exakt null) — genau die N(0)-Lücke aus dem Satz oben. Ab k=1 verschwindet der Unterschied im Rauschen der O(1)-Abweichungen von der Binomialverteilung.
Die ersten drei Momente bestaetigen die strukturelle Identitaet. Die kleine Varianzdifferenz (7,65 vs. 6,80) ist die letzte Spur der N(0)-Luecke — und sie verschwindet mit wachsendem n im Rauschen.
| μ₁ | μ₂ | Varianz | |
|---|---|---|---|
| SAT (n=16) | 8,500000 | 79,904 | 7,654 |
| UNSAT (n=16) | 8,500000 | 79,053 | 6,803 |
| Binomial | 8,500000 | 79,688 | 7,438 |
Die Zwei-Achsen-Trennung erklaert, warum keine Statistik ueber den Belegungsraum die Haerte vorhersagt. Aber sie erklaert nicht, wie d(50%) funktioniert — und sie liefert keinen neuen Algorithmus.
Die Ordnung d(50%) ist die einzige Groesse, die auf Achse B operiert (Propagationstiefe im Klauselraum) und Haerte korreliert. Warum korreliert sie? Kann man ihre Information in ein Verfahren uebersetzen, das die Suche nach c(x) = 0 beschleunigt? Bisher kostet jede Uebersetzung mehr, als der Gewinn bringt.
Das ist die noch offene Tuer.