A theorem says proof width grows linearly with the number of variables. The measurement says it's 3. Both are right — and the reason is a number nobody had computed before.
A formula in conjunctive normal form is a list of
clauses — disjunctions of variables and their negations.
(x₁ ∨ ¬x₂ ∨ x₃) is such a clause, of width 3. If the
formula is unsatisfiable, that can be proved by resolution:
from two clauses that contain one literal in both signs, their
merge follows, without that literal.
The proof ends when the empty clause has been derived — a contradiction. The width w* of such a proof is the size of its widest intermediate clause, and w*(F) is the smallest width with which F can be refuted at all.
This quantity is exactly determinable, not merely estimable. The closure under resolution with width bound w contains exactly the clauses that a proof of width ≤ w can derive. So:
One counts w upward from 3 until saturation refutes it. No estimator, no procedure with residual doubt — the value falls out exactly.
Ben-Sasson and Wigderson showed in 1999: for random 3-SAT at the threshold, proof width grows linearly with the number of variables, w* = Ω(n). From this it follows, via the relationship between width and length, that every resolution proof must be exponentially large.
What is measured is something else:
| n | measured w* | Ω(n) says |
|---|---|---|
| 25 | 3 | grows linearly |
| 45 | 3 | grows linearly |
| 55 | 3 – 4 | grows linearly |
| 110 | 4 | grows linearly |
w* = 3 is the smallest possible value for a 3-CNF. Across a factor of four in n, the quantity moves by exactly one step. The line fitted to this, "w* ≈ 0.018·n + 2", is a line through two integer jumps — no evidence of a linear regime.
First, the cost. The closure grows quadratically with its own size. Freshly implemented, with every clause packed into a single 64-bit word:
| width | n | closure | cost per instance |
|---|---|---|---|
| 3 | 30 | 33,000 | ≈ 1 s |
| 3 | 62 | 500 | seconds — starved |
| 4 | 90 | millions | > 400 s |
| 5 | ≈ 160 | — | unaffordable |
Second, the shape of the transition. One might hope that the size of the closure diverges at the transition and could be extrapolated from the cheap side. It doesn't. The closure is bimodal:
The crucial point: Ben-Sasson/Wigderson doesn't measure w* at all. The theorem derives the bound from a different property — expansion — and that property's constant is computable. So one doesn't need to cite the theorem asymptotically; one can evaluate it at the n where measurement actually takes place.
The boundary ∂S of a set of clauses S is the number of variables that occur in exactly one clause of S. A variable on the boundary is freely choosable — it can satisfy that one clause without disturbing anything else. A large boundary means: the set is easy to satisfy and carries no contradiction.
The theorem then reads:
And where the window ends — that is, where the first set with too small a boundary appears — is a pure counting question. A set of s clauses touching V variables has boundary ≥ 2V − 3s; boundary ≤ ε·s thus requires V ≤ (3+ε)·s/2. The expected number of such sets is computable:
Where this expectation exceeds 1, provable expansion ends. This is the same calculation used to determine the constant in Ω(n) in the first place — here just not in the limit, but at finite n.
| n | bound for w* | ε | window 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⁻⁵ |
The window stabilizes at δ = s/n ≈ 4.4·10⁻⁵, and the bound becomes linear with slope 1.73·10⁻⁶ per variable. From this:
The measurement w* = 3 at n = 55 does not contradict Ω(n) after all. The theorem has no content there whatsoever. It only gains enough content to rule out w* = 3 at around 1.7 million variables — at 31,000 times the n at which measurement takes place.
And the threshold density is, in this respect, the most favorable case. As clause density grows, the onset point moves further out:
| α | slope per variable | n₀ (bound > 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⁻⁶ |
Measured 0.018·n, proven 1.73·10⁻⁶·n: a factor of 10⁴. That is no contradiction — BW is a lower bound, the true w* is allowed to be arbitrarily steeper. But it means that the fitted slope is not a measurement of the constant in Ω(n). The two lines describe different things.
Whoever measures at n ≈ 100 and holds the result against Chvátal/Szemerédi is comparing against a theorem that hasn't yet kicked in there. What is measured is a different object.
The finite-size scaling of the threshold is well studied. That of proof width and proof size is not. Between n ≈ 10² — where measurement takes place, both here and in the literature — and n ≈ 10⁶, where the theorems take hold, lie four orders of magnitude for which there is no theory.
"""
Where does Asymptopia begin? The BW bound, evaluated exactly at finite n.
PROGRAMM.md sec2.1 calls it "the most important single fact in the corpus":
measured is w* = 3 at n = 55 and w* = 4 at n ~ 110, while
Ben-Sasson/Wigderson says w* = Omega(n). The line w* = 0.018n + 2 is a
fit through TWO integer jumps.
Measuring w* further directly is unaffordable (the width-4 closure at
n = 90 already takes > 400 s per instance). But BW does NOT measure w* --
the bound follows from EXPANSION, and its window is computable:
if dS >= eps*|S| for all S with |S| <= s, then w* >= eps*s/2
The window ends where the first set of clauses with too small a boundary
appears. Its existence is a counting question, not a search problem:
A set of s clauses touching V distinct variables has boundary
b >= 2V - 3s. Boundary <= eps*s thus means V <= (3+eps)s/2. And
E[#sets with s clauses on at most V variables]
= C(m,s) * C(n,V) * (C(V,3)/C(n,3))^s
Where this expectation exceeds 1, expansion ends. This is the usual
first-moment calculation used to determine the constant in
Omega(n) in the first place -- here just not asymptotically, but
at the n at which this project actually measures.
The point that matters: if the bound at n = 100 yields a value
BELOW 3, the theorem then ALLOWS w* = 3 there. The measurement does not
contradict it -- it simply lies before its onset point.
"""
from math import comb, log, exp
import numpy as np
def lc(a, b):
"""log C(a,b), also for large 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[#sets of s clauses touching at most V variables]."""
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):
"""Largest s for which NO set with boundary <= eps*s is yet expected.
This is the edge of the expansion window."""
m = round(alpha * n)
letzte = 0
for s in range(2, m + 1):
V = int((3.0 + eps) * s / 2.0) # boundary <= eps*s => V <= ...
if erwartung(n, m, s, V) > 0.0:
return letzte
letzte = s
return letzte
def schranke(n, alpha, feins=200):
"""max over eps of eps*s(eps)/2 -- the best bound that BW yields
at this n."""
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(" The BW bound for w*, evaluated at finite n")
print(" (alpha = 4.267; 'window' = largest set up to which")
print(" expansion provably holds)\n")
print(f" {'n':>7s} {'m':>8s} {'bound':>9s} {'eps':>6s} {'window s':>10s} "
f"{'allows 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"{'YES' if b < 3 else 'no':>14s}")
# ---------------------------------------------------------------- The core
def fenster_schnell(n, alpha, eps):
"""Like `fenster`, but with doubling search instead of a linear
count-up -- the window sits at delta*n with delta ~ 1e-4, a linear
search would be hopeless at n = 10^8."""
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
Where does Asymptopia begin? BW bound for w*, finite n, alpha=4.267
Measured in the corpus: w* = 3 at n = 55, w* = 4 at n ~ 110.
n BW bound eps window 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
Where does the bound cross the measured w* values?
slope of the bound: 1.733e-06 per variable
bound > 3 from n ~ 1.73e+06 (w*=3, measured at n=55)
bound > 4 from n ~ 2.31e+06 (w*=4, measured at n~110)
bound > 5 from n ~ 2.88e+06 (w*=5)"""The onset point n0 as clause density grows -- the same BW bound
as in asymptopia.py, just evaluated repeatedly at alpha = 4.267 / 6 / 10 / 20.
Usage: python3 vielfache_dichten.py
Writes 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} slope {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("\nsaved -> daten_dichten.json")
if __name__ == "__main__":
lauf()
| α | slope per variable | n₀ (bound > 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 |
First-moment calculation, deterministic (no sampling) — under the fixed condition V ≤ (3+ε)s/2 it reproducibly yields exactly the same values as in the 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
}
}