Why aggregates over the assignment space can't distinguish SAT from UNSAT — and what follows from that.
Eight independent approaches over the solution set — backbone, repair set |R|, survey propagation, cavity, residual geometry, backbone trajectory, and now also the exact moments μ₁…μ₃ — have no predictive power for refutation cost (AUC ≈ 0.5, correlation r ≤ 0.15). The one exception is the order d(50%), which measures derivative behavior (r ≈ 0.56, replicated three times).
Consider the energy distribution of a 3-CNF formula:
N(k) = |{x ∈ {0,1}n : c(x) = k}| where c(x) = number of clauses violated by x
Let F be a uniform random 3-CNF at the threshold. For a fixed assignment x, each clause is falsified by exactly 1/8 of all assignments. Two clauses sharing no variable are independent. The fraction of pairs with shared variables is O(1/n). Consequently:
Any finite set of clause correlations (pairs, triples, …) produces deviations of O(1), which vanish as n → ∞ against the mass of N(k≥1) ∼ O(2n). The only non-removable deviation is N(0): a satisfying assignment by definition violates no clause, so N(0) > 0 for SAT and = 0 for UNSAT.
This difference, however, is exponentially small: the expected value of N(0) for a random formula is 2n·(7/8)m = (2·(7/8)α)n. At α = 4.267, the base is 2·(7/8)4.267 ≈ 2·0.545 = 1.090. The relative share N(0)/2n falls like 0.545n — exponentially. At n = 200 it is ≈10-53.
For n = 16 (m = 68, α = 4.25), 300 instances, brute force over all 216 = 65536 assignments:
| 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 |
The original instances behind this table can no longer be reconstructed (no saved script, no fixed seed). The evidence below reproduces the same measurement freshly, with a persisted script and fixed seed — same order of magnitude, same pattern, its own (not identical) numbers.
"""The energy distribution N(k) for SAT and UNSAT, exact -- the evidence
behind zwei-achsen-trennung.html.
c(x) = number of clauses violated by assignment x. F is unsatisfiable
exactly when c has no minimum of 0. N(k)/2^n is the distribution of c
over all 2^n assignments, exact (no sampling) for small n.
Usage: python3 energieverteilung.py [n=16] [alpha=4.25] [anzahl=300] [seed=42]
Writes 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) for all 2^n assignments as an 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)
# One value N(k)/2^n per instance -- that is the sampling unit for
# Cohen's d, not the individual assignment (those are not independent
# within an instance).
sat_dichten = [] # list of (m+1,)-arrays, one per instance
unsat_dichten = []
sat_mu1 = [] # first moment per instance, for the moments table
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)
# Binomial reference 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 over the INSTANCES: one N(k)/2^n value per instance,
# pooled standard deviation over the two samples.
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 of {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("\nsaved -> 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 of 300 instances, seed 42. μ₁ = 8.5000 (SAT) / 8.5000 (UNSAT) exactly equal — 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
}
]
}The only visible difference is at k=0 (UNSAT curve exactly zero) — exactly the N(0) gap from the theorem above. From k=1 on, the difference vanishes into the noise of the O(1) deviations from the binomial distribution.
The first three moments confirm the structural identity. The small variance difference (7.65 vs. 6.80) is the last trace of the N(0) gap — and it vanishes into the noise as n grows.
| μ₁ | μ₂ | Variance | |
|---|---|---|---|
| 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 |
The two-axis separation explains why no statistic over the assignment space predicts hardness. But it does not explain how d(50%) works — and it delivers no new algorithm.
The order d(50%) is the only quantity that operates on axis B (propagation depth in clause space) and correlates with hardness. Why does it correlate? Can its information be translated into a procedure that speeds up the search for c(x) = 0? So far every translation has cost more than the gain it brings.
That is the door still open.