Ein Satz sagt, die Beweisbreite wachse linear mit der Zahl der Variablen. Die Messung sagt, sie sei 3. Beide haben recht — und der Grund dafür ist eine Zahl, die bisher niemand ausgerechnet hat.
Eine Formel in konjunktiver Normalform ist eine Liste von
Klauseln — Oder-Verknüpfungen von Variablen und ihren Negationen.
(x₁ ∨ ¬x₂ ∨ x₃) ist eine solche Klausel der Breite 3. Ist die
Formel unerfüllbar, so lässt sich das durch Resolution beweisen:
aus zwei Klauseln, die ein Literal in beiden Vorzeichen enthalten, folgt
ihre Verschmelzung ohne dieses Literal.
Der Beweis endet, wenn die leere Klausel abgeleitet ist — ein Widerspruch. Die Breite w* eines solchen Beweises ist die Grösse seiner breitesten Zwischenklausel, und w*(F) ist die kleinste Breite, mit der F überhaupt widerlegbar ist.
Diese Grösse ist exakt bestimmbar, nicht nur schätzbar. Der Abschluss unter Resolution mit Breitenschranke w enthält genau die Klauseln, die ein Beweis der Breite ≤ w ableiten kann. Also:
Man zählt w von 3 an hoch, bis die Sättigung widerlegt. Kein Schätzer, kein Verfahren mit Restzweifel — der Wert fällt exakt.
Ben-Sasson und Wigderson haben 1999 gezeigt: für zufälliges 3-SAT an der Schwelle wächst die Beweisbreite linear mit der Zahl der Variablen, w* = Ω(n). Daraus folgt, über den Zusammenhang zwischen Breite und Länge, dass jeder Resolutionsbeweis exponentiell gross sein muss.
Gemessen wird etwas anderes:
| n | gemessenes w* | Ω(n) sagt |
|---|---|---|
| 25 | 3 | wächst linear |
| 45 | 3 | wächst linear |
| 55 | 3 – 4 | wächst linear |
| 110 | 4 | wächst linear |
w* = 3 ist der kleinstmögliche Wert für eine 3-KNF. Über einen Faktor vier in n bewegt sich die Grösse um genau einen Schritt. Die daraus gefittete Gerade „w* ≈ 0,018·n + 2" ist eine Gerade durch zwei ganzzahlige Sprünge — kein Beleg für ein lineares Regime.
Erstens der Aufwand. Der Abschluss wächst quadratisch mit seiner eigenen Grösse. Neu implementiert, mit jeder Klausel in ein einziges 64-Bit-Wort gepackt:
| Breite | n | Abschluss | Aufwand je Instanz |
|---|---|---|---|
| 3 | 30 | 33 000 | ≈ 1 s |
| 3 | 62 | 500 | Sekunden — verhungert |
| 4 | 90 | Millionen | > 400 s |
| 5 | ≈ 160 | — | unbezahlbar |
Zweitens die Form des Übergangs. Man könnte hoffen, die Grösse des Abschlusses divergiere beim Übergang und liesse sich von der billigen Seite extrapolieren. Sie tut es nicht. Der Abschluss ist bimodal:
Der entscheidende Punkt: Ben-Sasson/Wigderson misst w* gar nicht. Der Satz leitet die Schranke aus einer anderen Eigenschaft her — der Expansion — und deren Konstante ist ausrechenbar. Man muss den Satz also nicht asymptotisch zitieren; man kann ihn bei dem n auswerten, bei dem tatsächlich gemessen wird.
Der Rand ∂S einer Klauselmenge S ist die Zahl der Variablen, die in genau einer Klausel von S vorkommen. Eine Variable am Rand ist frei wählbar — sie kann die eine Klausel erfüllen, ohne irgendwo sonst zu stören. Viel Rand heisst: die Menge ist leicht zu erfüllen und trägt keinen Widerspruch.
Der Satz lautet dann:
Und wo das Fenster endet — wo also die erste Menge mit zu kleinem Rand auftaucht —, ist eine reine Abzählfrage. Eine Menge aus s Klauseln, die V Variablen berührt, hat Rand ≥ 2V − 3s; Rand ≤ ε·s verlangt also V ≤ (3+ε)·s/2. Die erwartete Zahl solcher Mengen ist ausrechenbar:
Wo dieser Erwartungswert 1 überschreitet, hört die nachweisbare Expansion auf. Das ist dieselbe Rechnung, mit der die Konstante im Ω(n) überhaupt bestimmt wird — hier nur nicht im Grenzwert, sondern bei endlichem n.
| n | Schranke für w* | ε | Fenster s | s / n |
|---|---|---|---|---|
| 10² | 0,99 | 0,99 | 2 | 2,0·10⁻² |
| 10³ | 0,99 | 0,99 | 2 | 2,0·10⁻³ |
| 10⁴ | 0,99 | 0,99 | 2 | 2,0·10⁻⁴ |
| 10⁵ | 1,49 | 0,99 | 3 | 3,0·10⁻⁵ |
| 10⁶ | 3,00 | 0,097 | 62 | 6,2·10⁻⁵ |
| 10⁷ | 19,0 | 0,092 | 414 | 4,1·10⁻⁵ |
| 10⁹ | 1 736 | 0,079 | 43 744 | 4,4·10⁻⁵ |
| 10¹¹ | 173 331 | 0,079 | 4 367 685 | 4,4·10⁻⁵ |
Das Fenster stabilisiert sich bei δ = s/n ≈ 4,4·10⁻⁵, die Schranke wird linear mit der Steigung 1,73·10⁻⁶ je Variable. Daraus:
Die Messung w* = 3 bei n = 55 widerspricht Ω(n) also nicht. Der Satz hat dort überhaupt keinen Inhalt. Er bekommt erst bei rund 1,7 Millionen Variablen genug Inhalt, um w* = 3 auszuschliessen — beim 31 000-fachen des n, bei dem gemessen wird.
Und die Schwelle ist dabei der günstigste Fall. Mit wachsender Klauseldichte wandert der Einsetzpunkt nach oben:
| α | Steigung je Variable | n₀ (Schranke > 3) | δ |
|---|---|---|---|
| 4,267 | 1,73·10⁻⁶ | 1,7·10⁶ | 4,4·10⁻⁵ |
| 6 | 8,28·10⁻⁷ | 3,6·10⁶ | 2,2·10⁻⁵ |
| 10 | 2,75·10⁻⁷ | 1,1·10⁷ | 8,0·10⁻⁶ |
| 20 | 6,22·10⁻⁸ | 4,8·10⁷ | 2,0·10⁻⁶ |
Gemessen 0,018·n, bewiesen 1,73·10⁻⁶·n: ein Faktor 10⁴. Das ist kein Widerspruch — BW ist eine untere Schranke, das wahre w* darf beliebig steiler sein. Aber es heisst, dass die gefittete Steigung keine Messung der Konstante im Ω(n) ist. Die beiden Geraden beschreiben verschiedene Dinge.
Wer bei n ≈ 100 misst und das Ergebnis gegen Chvátal/Szemerédi hält, vergleicht mit einem Satz, der dort noch nicht angesprungen ist. Gemessen wird ein anderes Objekt.
Die endliche Grössenskalierung der Schwelle ist gut untersucht. Die der Beweisbreite und Beweisgrösse ist es nicht. Zwischen n ≈ 10² — wo gemessen wird, hier wie in der Literatur — und n ≈ 10⁶, wo die Sätze greifen, liegen vier Grössenordnungen, für die es keine Theorie gibt.
"""
Wo faengt Asymptopia an? Die BW-Schranke, exakt bei endlichem n ausgewertet.
PROGRAMM.md §2.1 nennt es "the most important single fact in the corpus":
gemessen wird w* = 3 bei n = 55 und w* = 4 bei n ~ 110, waehrend
Ben-Sasson/Wigderson w* = Omega(n) sagt. Die Gerade w* = 0,018n + 2 ist ein
Fit durch ZWEI ganzzahlige Spruenge.
w* direkt weiterzumessen ist unbezahlbar (Breite-4-Abschluss bei n = 90
schon > 400 s je Instanz). Aber BW MISST w* nicht -- die Schranke folgt aus
der EXPANSION, und deren Fenster ist ausrechenbar:
gilt dS >= eps*|S| fuer alle S mit |S| <= s, so ist w* >= eps*s/2
Das Fenster endet, wo es die erste Klauselmenge mit zu kleinem Rand gibt.
Deren Existenz ist eine Abzaehlfrage, kein Suchproblem:
Eine Menge von s Klauseln, die V verschiedene Variablen beruehrt, hat
Rand b >= 2V - 3s. Rand <= eps*s heisst also V <= (3+eps)s/2. Und
E[#Mengen mit s Klauseln auf hoechstens V Variablen]
= C(m,s) * C(n,V) * (C(V,3)/C(n,3))^s
Wo dieser Erwartungswert 1 ueberschreitet, hoert die Expansion auf. Das
ist die uebliche erste-Moment-Rechnung, mit der die Konstante in
Omega(n) ueberhaupt bestimmt wird -- hier nur nicht asymptotisch, sondern
bei dem n, bei dem dieses Projekt misst.
Die Pointe, auf die es ankommt: liefert die Schranke bei n = 100 einen Wert
UNTER 3, so ERLAUBT der Satz dort w* = 3. Die Messung widerspricht ihm dann
nicht -- sie liegt vor seinem Einsetzpunkt.
"""
from math import comb, log, exp
import numpy as np
def lc(a, b):
"""log C(a,b), auch fuer grosse a."""
if b < 0 or b > a:
return -1e18
from math import lgamma
return lgamma(a + 1) - lgamma(b + 1) - lgamma(a - b + 1)
def erwartung(n, m, s, V):
"""log E[#Mengen aus s Klauseln, die hoechstens V Variablen beruehren]."""
if V < 3 or s < 1:
return -1e18
return lc(m, s) + lc(n, V) + s * (lc(V, 3) - lc(n, 3))
def fenster(n, alpha, eps):
"""Groesstes s, fuer das noch KEINE Menge mit Rand <= eps*s zu erwarten
ist. Das ist die Grenze des Expansionsfensters."""
m = round(alpha * n)
letzte = 0
for s in range(2, m + 1):
V = int((3.0 + eps) * s / 2.0) # Rand <= eps*s => V <= ...
if erwartung(n, m, s, V) > 0.0:
return letzte
letzte = s
return letzte
def schranke(n, alpha, feins=200):
"""max ueber eps von eps*s(eps)/2 -- die beste Schranke, die BW bei
diesem n hergibt."""
best, be, bs = 0.0, 0.0, 0
for eps in np.linspace(0.02, 2.0, feins):
s = fenster(n, alpha, eps)
w = eps * s / 2.0
if w > best:
best, be, bs = w, eps, s
return best, be, bs
if __name__ == "__main__":
print(" Die BW-Schranke fuer w*, bei endlichem n ausgewertet")
print(" (alpha = 4,267; 'Fenster' = groesste Menge, bis zu der die")
print(" Expansion nachweislich haelt)\n")
print(f" {'n':>7s} {'m':>8s} {'Schranke':>9s} {'eps':>6s} {'Fenster s':>10s} "
f"{'erlaubt w*=3?':>14s}")
for n in (50, 100, 200, 400, 800, 1600, 3200, 6400,
12800, 25600, 51200, 102400, 204800, 409600):
b, e, s = schranke(n, 4.267)
print(f" {n:7d} {round(4.267*n):8d} {b:9.2f} {e:6.2f} {s:10d} "
f"{'JA' if b < 3 else 'nein':>14s}")
# ---------------------------------------------------------------- Der Kern
def fenster_schnell(n, alpha, eps):
"""Wie `fenster`, aber mit Verdopplungssuche statt linearem Hochzaehlen --
das Fenster liegt bei delta*n mit delta ~ 1e-4, lineares Suchen waere
bei n = 10^8 hoffnungslos."""
m = round(alpha * n)
def kippt(s):
V = int((3.0 + eps) * s / 2.0)
return erwartung(n, m, s, V) > 0.0
if kippt(2):
return 0
lo, hi = 2, 4
while hi < m and not kippt(hi):
lo, hi = hi, hi * 2
hi = min(hi, m)
while lo + 1 < hi:
mid = (lo + hi) // 2
if kippt(mid): hi = mid
else: lo = mid
return lo
def beste_schranke(n, alpha=4.267):
best, be, bs = 0.0, 0.0, 0
for eps in np.concatenate([np.linspace(0.005, 0.3, 120),
np.linspace(0.3, 1.5, 60)]):
s = fenster_schnell(n, alpha, eps)
w = eps * s / 2.0
if w > best:
best, be, bs = w, eps, s
return best, be, bs
Wo faengt Asymptopia an? BW-Schranke fuer w*, endliches n, alpha=4,267
Gemessen im Korpus: w* = 3 bei n = 55, w* = 4 bei n ~ 110.
n BW-Schranke eps Fenster s s/n
100 0.992 0.992 2 2.00e-02
1000 0.992 0.992 2 2.00e-03
10000 0.992 0.992 2 2.00e-04
100000 1.487 0.992 3 3.00e-05
300000 1.994 0.166 24 8.00e-05
1000000 2.998 0.097 62 6.20e-05
3000000 6.050 0.102 119 3.97e-05
10000000 18.995 0.092 414 4.14e-05
30000000 53.018 0.074 1425 4.75e-05
100000000 174.993 0.082 4276 4.28e-05
300000000 521.949 0.082 12754 4.25e-05
1000000000 1735.975 0.079 43744 4.37e-05
10000000000 17342.012 0.079 436993 4.37e-05
100000000000 173331.029 0.079 4367685 4.37e-05
Wo ueberschreitet die Schranke die gemessenen w*-Werte?
Steigung der Schranke: 1.733e-06 je Variable
Schranke > 3 ab n ~ 1.73e+06 (w*=3, gemessen bei n=55)
Schranke > 4 ab n ~ 2.31e+06 (w*=4, gemessen bei n~110)
Schranke > 5 ab n ~ 2.88e+06 (w*=5)"""Der Einsetzpunkt n0 bei wachsender Klauseldichte -- dieselbe BW-Schranke
wie in asymptopia.py, nur mehrfach bei alpha = 4,267 / 6 / 10 / 20 ausgewertet.
Aufruf: python3 vielfache_dichten.py
Schreibt daten_dichten.json.
"""
import json
import sys, os
import numpy as np
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from asymptopia import beste_schranke
def einsetzpunkt(alpha, ziel=3.0):
ns = np.array([1e5, 3e5, 1e6, 3e6, 1e7, 3e7, 1e8, 3e8, 1e9, 1e10, 1e11], float)
bs, ds = [], []
for n in ns:
b, e, s = beste_schranke(int(n), alpha)
bs.append(b); ds.append(s / n)
bs = np.array(bs)
k = np.polyfit(ns[-4:], bs[-4:], 1)[0]
n0 = ziel / k
return float(k), float(n0), float(ds[-1])
def lauf():
aus = {}
for alpha in (4.267, 6, 10, 20):
k, n0, delta = einsetzpunkt(alpha)
aus[str(alpha)] = {"alpha": alpha, "steigung": k, "n0": n0, "delta": delta}
print(f" alpha={alpha:6.3f} Steigung {k:.3e} n0(w*>3) {n0:.3e} delta {delta:.3e}")
with open("../daten_dichten.json", "w") as f:
json.dump(aus, f, indent=1)
print("\ngespeichert -> daten_dichten.json")
if __name__ == "__main__":
lauf()
| α | Steigung je Variable | n₀ (Schranke > 3) | δ |
|---|---|---|---|
| 4.267 | 1.733e-06 | 1.731e+06 | 4.368e-05 |
| 6.000 | 8.277e-07 | 3.625e+06 | 2.225e-05 |
| 10.000 | 2.750e-07 | 1.091e+07 | 7.921e-06 |
| 20.000 | 6.226e-08 | 4.818e+07 | 1.931e-06 |
Erste-Moment-Rechnung, deterministisch (kein Sampling) — bei fester Bedingung V ≤ (3+ε)s/2 reproduzierbar exakt dieselben Werte wie im Text.
{
"4.267": {
"alpha": 4.267,
"steigung": 1.7332697195401431e-06,
"n0": 1730832.7527904517,
"delta": 4.367685e-05
},
"6": {
"alpha": 6,
"steigung": 8.276615622323391e-07,
"n0": 3624669.9579819893,
"delta": 2.224621e-05
},
"10": {
"alpha": 10,
"steigung": 2.750410766301191e-07,
"n0": 10907461.666296711,
"delta": 7.92067e-06
},
"20": {
"alpha": 20,
"steigung": 6.226491512175137e-08,
"n0": 48181226.84554969,
"delta": 1.93128e-06
}
}