From a probe that does not solve to the first intervention in this corpus — and why both causal structural quantities act only through solvers that react to structure.
The number of critical clauses in an unsatisfiable instance — clauses whose removal makes it satisfiable — correlates with hardness. Measuring it the obvious way means solving the instance once per clause, which is circular. The question was whether some cheap response to a small perturbation carries the same signal.
It does, through a certificate. Local search with a fixed budget visits assignments that violate exactly one clause; that clause is then provably critical, and nothing has been decided. On 600 unsatisfiable instances the set found this way equals the true critical set on 72–99 % of instances, never contains a clause too many, and correlates with hardness as strongly as the expensive version.
| n | r(|K|, log hardness) | |K| = critical set | cost vs. one solver run |
|---|---|---|---|
| 70 | +0.42 | 98.5 % | 319× |
| 100 | +0.32 | 90.5 % | 72× |
| 130 | +0.38 | 72.5 % | 31× |
The probe grows like n^1.15, the solver exponentially; the two cross near n ≈ 120–200. At the sizes measured here the probe is still the more expensive of the two — a statement about the solver's head start, not about the probe.
void sonde_walk(const F& f, uint64_t saat, J& j, int neustarts = 200, int fluege_pro_n = 20) {
auto t0 = Clk::now();
Walk w(f, saat);
vector<char> inK(f.c.size(), 0);
int k = 0, emin = INT_MAX, loesung = 0;
long long e1_besuche = 0, flips = 0, letzter_flip = 0;
int letzter_neustart = 0;
vector<int> kurve;
for (int s = 1; s <= neustarts; s++) {
w.neu();
for (int t = 0; t < fluege_pro_n * f.n; t++) {
int e = w.offen.size();
emin = min(emin, e);
if (e == 0) { loesung = 1; break; }
if (e == 1) { e1_besuche++; int c = w.offen[0]; if (!inK[c]) { inK[c] = 1; k++; letzter_neustart = s; letzter_flip = flips; } }
w.schritt(0.5);
flips++;
}
if (s == 25 || s == 50 || s == 100 || s == 200 || s == 400) kurve.push_back(k);
}
j.i("walk_K", k).a("walk_K_kurve", kurve).i("walk_letzter_neustart", letzter_neustart).i("walk_letzter_flip", letzter_flip).i("walk_flips", flips).i("walk_emin", emin).i("walk_e1", e1_besuche).i("walk_loesung", loesung).z("zeit_walk", sek(t0));
}2.3-S Walk-Menge K gegen kritische Klauseln (UNSAT, N 200): K == krit auf 90.5%, Summe K / Summe krit = 0.9894, K > krit (darf nie sein): 0
nach Neustarts 25: 0.794 (r +0.976), 50: 0.887 (r +0.990), 100: 0.945 (r +0.997), 200: 0.977 (r +0.998), 400: 0.989 (r +0.999)
Median Neustart des letzten Fundes 44, P90 216, max 392; krit Median 10 [0–69], krit = 0 auf 10.5%
*walk_K 2.3-S UNSAT 200 +0.316 [+0.185, +0.436] +0.339 +0.285 +0.372 +0.290 +1.000 0.141 ←Four cheap quantities kept correlating with hardness and with each other: the Bethe entropy, how many clauses an instance tolerates before tipping, the point where belief propagation stops converging, and the critical set. They turn out to be four estimates of one distance — how far the instance sits from its own satisfiability threshold. The ground truth, the first unsatisfiable prefix of a clause sequence, is exact by bisection because satisfiability is monotone along the sequence; against it, belief propagation agrees to 0.79–0.81 after reliability correction.
Next to this axis, almost orthogonal to it, sits the spread of variable degrees (Σ grad²). Were it mediated by the threshold, its correlation with hardness would be r(Σ grad², threshold)·r(threshold, hardness) ≈ −0.03; measured is −0.45 to −0.52. On the unsatisfiable side it is the larger of the two axes: the threshold alone explains cross-validated R² = 0.12–0.16, together with degree spread 0.35–0.43.
What the spectrum does carry beyond Σ grad² is a second degree quantity: whether high-degree variables sit together in clauses — the degree correlation C.
A correlation cannot tell a lever from a proxy. So the instances were rewired: two slots swap their variables, signs stay with the slot, the degree sequence is preserved exactly, satisfiability is checked every ten swaps, the threshold enters as a covariate. Four arms per instance — C up by 2.5 natural standard deviations, C down, a neutral arm with as many swaps and C held fixed, and a positive control raising Σ grad². Prediction, expected size and decision rule were written into the source before the run.
| unsatisfiable, C high − C low | n = 100 | n = 130 |
|---|---|---|
| DPLL (Jeroslow–Wang), primary | −0.77 [−0.82, −0.71] | −0.94 [−1.01, −0.87] |
| expected from the correlation | −0.73 | −0.72 |
| CaDiCaL | −0.42 [−0.46, −0.37] | −0.45 [−0.50, −0.40] |
| Σ grad² +2.5 SD (adjusted) | −0.48 | −0.56 |
| neutral arm | +0.04 (includes 0) | +0.01 (includes 0) |
Direction and existence hold, under two solvers, replicated. The size does not: at n = 130 the pre-registered expectation lies outside the interval — the correlation underestimates the causal effect. Both degree quantities are causal. Neither acts through the critical set: 0–1 % of either effect is mediated by it.
Umverdrahtung umverdrahten(const F& basis, int modus, double ziel, double band, int ziel_tausche, int status0, mt19937_64& r) {
Umverdrahtung u; u.f = basis;
F& f = u.f;
int m = f.c.size();
vector<int> d = grade(f);
long long C = grad_korrelation(f, d);
long long sg2 = sigma_grad2(f);
auto andere = [&](const Cl& cl, int p, const vector<int>& dd) { long long s = 0; for (int q = 0; q < 3; q++) if (q != p) s += dd[var_(cl[q])]; return s; };
auto erreicht = [&]() {
if (modus == 1) return C >= ziel;
if (modus == -1) return C <= ziel;
if (modus == 0) return u.tausche >= ziel_tausche;
return (double)sg2 >= ziel;
};
F sicherung = f; vector<int> d_sich = d; long long C_sich = C, sg2_sich = sg2; int block = 0, t_sich = 0;
const int MAXVERSUCHE = 4000000;
while (!erreicht() && u.versuche < MAXVERSUCHE) {
u.versuche++;
int i = r() % m, j = r() % m, p = r() % 3, q = r() % 3;
if (modus == 2) {
// Slot (i,p) von Variable a auf Variable b umhaengen, grad(b) >= grad(a)
int a = var_(f.c[i][p]), b = r() % f.n;
if (b == a || d[b] < d[a]) continue;
if (var_(f.c[i][(p + 1) % 3]) == b || var_(f.c[i][(p + 2) % 3]) == b) continue;
if (d[a] <= 1) continue;
long long dsg = (long long)(d[b] + 1) * (d[b] + 1) - (long long)d[b] * d[b] + (long long)(d[a] - 1) * (d[a] - 1) - (long long)d[a] * d[a];
if (dsg <= 0) continue;
int sg = f.c[i][p] > 0 ? 1 : -1;
f.c[i][p] = sg * (b + 1); d[a]--; d[b]++; sg2 += dsg;
C = grad_korrelation(f, d);
} else {
if (i == j) continue;
int a = var_(f.c[i][p]), b = var_(f.c[j][q]);
if (a == b) continue;
if (var_(f.c[i][(p + 1) % 3]) == b || var_(f.c[i][(p + 2) % 3]) == b) continue;
if (var_(f.c[j][(q + 1) % 3]) == a || var_(f.c[j][(q + 2) % 3]) == a) continue;
long long dC = (long long)(d[b] - d[a]) * (andere(f.c[i], p, d) - andere(f.c[j], q, d));
if (modus == 1 && dC <= 0) continue;
if (modus == -1 && dC >= 0) continue;
if (modus == 0 && fabs((double)(C + dC) - (ziel)) > band) continue;
int si = f.c[i][p] > 0 ? 1 : -1, sj = f.c[j][q] > 0 ? 1 : -1;
f.c[i][p] = si * (b + 1); f.c[j][q] = sj * (a + 1); // Vorzeichen bleiben am Slot
C += dC;
}
u.tausche++;
if (++block == 10 || erreicht()) {
block = 0;
if (status_von(f) != status0) {
f = sicherung; d = d_sich; C = C_sich; sg2 = sg2_sich; u.tausche = t_sich; u.verworfen++;
if (u.verworfen > 400) break;
} else {
sicherung = f; d_sich = d; C_sich = C; sg2_sich = sg2; t_sich = u.tausche;
}
}
}
u.fertig = erreicht() && status_von(f) == status0;
return u;
} --- UNSAT: 150 Basisinstanzen, alle Arme fertig und Status erhalten: 150; Gradfolge in den Tausch-Armen exakt erhalten: True
hoch Tausche Median 46, verworfen Median 1, ΔC/SD Median +2.54, Δ log2H -0.376 [-0.423, -0.329], Δ kipp -0.0188
tief Tausche Median 45, verworfen Median 1, ΔC/SD Median -2.53, Δ log2H +0.405 [+0.348, +0.461], Δ kipp -0.0079
neutral Tausche Median 45, verworfen Median 1, ΔC/SD Median -0.04, Δ log2H +0.044 [-0.016, +0.105], Δ kipp -0.0013
gradhoch Tausche Median 48, verworfen Median 0, ΔC/SD Median +28.53, Δ log2H -0.512 [-0.564, -0.460], Δ kipp -0.0402
PRIMÄRSTATISTIK d = log2H(hoch) - log2H(tief), N = 150
roh: -0.781 [-0.842, -0.720]
Δ kipp(hoch - tief): -0.0109, Steigung von d auf Δ kipp +1.488
bei gleicher Schwelle (Achsenabschnitt): -0.765 [-0.823, -0.707] erwartet -0.729
Positivkontrolle gradhoch - basis: -0.512 [-0.564, -0.460] -> bestanden
neutral - basis (allgemeiner Umverdrahtungseffekt): +0.044 [-0.016, +0.105]
URTEIL nach Regel: VORHERSAGE ERFÜLLT
sekundär hoch - neutral: -0.421 [-0.491, -0.351]
sekundär tief - neutral: +0.360 [+0.294, +0.427]
--- SAT: 150 Basisinstanzen, alle Arme fertig und Status erhalten: 150; Gradfolge in den Tausch-Armen exakt erhalten: True
hoch Tausche Median 46, verworfen Median 1, ΔC/SD Median +2.53, Δ log2H -0.225 [-0.502, +0.052], Δ kipp +0.0032The effect was a factor of two smaller under CaDiCaL than under DPLL. To find out which component of a solver responds, the in-house CDCL solver got switches, each removing one component, and ran on the same rewired instances.
| unsatisfiable, n = 100, share q of the full effect | degree correlation C | degree spread Σ grad² |
|---|---|---|
| full (VSIDS, 1UIP learning, restarts, phase saving) | 1 | 1 |
| without 1UIP learning (VSIDS still fed by conflicts) | 0.97 | 1.26 |
| static random order instead of VSIDS (still learns) | 0.48 | 0.85 |
| static order and no learning | −0.07 | 0.12 |
Both causal quantities vanish in the blind, non-learning solver — relative to its cost, which is 64 times higher; in absolute terms that cell stays undecided. The two differ in the route: the degree correlation depends on where the solver branches, the degree spread hardly — it is enough that the solver learns from conflicts.
Two tempting readings were checked and dropped. A fixed absolute saving that expensive solvers merely dilute is ruled out: the full solver and the one without learning differ fourfold in base cost and not in effect. And the apparent growth of the effect with instance hardness is an artefact — a neutral arm with no effect produces the same slope, because every rewiring of a hard instance is, on average, a less hard instance.
fn schalter(konfig: &str, n: usize, saat: u64) -> Schalter {
let mut s = Schalter::default();
match konfig {
"voll" => {}
"R" => s.neustarts = false,
"P" => s.phasenspeicher = false,
"L" => { s.lernen = false; s.neustarts = false; s.vergessen = false; }
"S" => s.ordnung = Some(permutation(n, saat)),
"SL" => { s.ordnung = Some(permutation(n, saat)); s.lernen = false; s.neustarts = false; s.vergessen = false; }
_ => panic!("unbekannte Konfiguration {konfig}"),
}
s
}Gradkorrelation C (hoch − tief):
--- UNSAT, N = 150 ---
voll a = -0.442 [-0.493, -0.392] (Faktor 1.36) Zuverlässigkeit d +0.95 Median log2 Konflikte (tief) 9.1
R a = -0.430 [-0.483, -0.377] (Faktor 1.35) Zuverlässigkeit d +0.97 Median log2 Konflikte (tief) 9.2
P a = -0.454 [-0.503, -0.405] (Faktor 1.37) Zuverlässigkeit d +0.96 Median log2 Konflikte (tief) 9.1
L a = -0.427 [-0.480, -0.375] (Faktor 1.34) Zuverlässigkeit d +0.95 Median log2 Konflikte (tief) 11.1
S a = -0.214 [-0.259, -0.168] (Faktor 1.16) Zuverlässigkeit d +0.75 Median log2 Konflikte (tief) 11.2
SL a = +0.031 [-0.014, +0.076] (Faktor 0.98) Zuverlässigkeit d +0.40 Median log2 Konflikte (tief) 15.4
q_R = +0.97 [+0.92, +1.02]
q_P = +1.03 [+0.99, +1.07]
q_L = +0.97 [+0.88, +1.06]
q_S = +0.48 [+0.39, +0.57]
q_SL = -0.07 [-0.18, +0.03]
Gradstreuung Σ grad² (gradhoch − basis):
--- UNSAT, N = 150 ---
voll a = -0.344 [-0.393, -0.295] Zuverlässigkeit +0.92 Median log2 B 8.8
L a = -0.433 [-0.484, -0.381] Zuverlässigkeit +0.91 Median log2 B 10.9
S a = -0.291 [-0.333, -0.249] Zuverlässigkeit +0.68 Median log2 B 11.1
SL a = -0.041 [-0.087, +0.004] Zuverlässigkeit +0.31 Median log2 B 15.4
q_L = +1.26 [+1.15, +1.39]
q_S = +0.85 [+0.73, +0.99]
q_SL = +0.12 [-0.00, +0.24]
VERDÜNNUNGSKONTRAST in SL: a_SL(Σgrad²) -0.041 gegen a_SL(C) +0.031, Differenz -0.072 [-0.139, -0.008]
REGELN: 0 True | I bleibt im blinden Löser False | II verschwindet wie C True | That is narrower than it sounds. The threshold axis has never been ablated and rests on correlation. Nothing here bears on proof length, which knows no branching heuristic. The contribution is methodological as much as substantive: interventions along one structural quantity with the others held fixed, a neutral arm, pre-registration, and a solver taken apart component by component.