Measurement log August 20, 2026 random 3-SAT, α = 4.267 around 21,000 solver runs

Scaffold and
Sign

What determines how hard a single unsatisfiable instance is at the threshold — and what does not.

41.7 %of hardness variance already sits in the sign-free scaffold

Σ deg²carries it — a single pass over the clause list

16×harder is regular 3-SAT at n = 200

49 %remain unexplained on the sign axis

§ 1

The question

Not whether the information is there

The subject is random 3-SAT at the satisfiability threshold α = m/n ≈ 4.267. There, about half of the instances are unsatisfiable, and there they are hardest.

That the information "solvable or unsolvable" is contained in the formula is not in question: unsatisfiability is a well-defined property of the clause set, invariant under renaming and permutation. Resolution is complete, nothing is missing from the vocabulary. What is missing is brevity — for random 3-CNF every resolution proof has size 2^Ω(n) (Chvátal/Szemerédi 1988).

This investigation does not answer that question. It answers a smaller one, upstream of it:

Two unsatisfiable instances with the same n and the same α differ in refutation cost by orders of magnitude. What does that depend on?

The answer splits into two axes, and they come out very differently.

§ 2

The design

Scaffold, signature, null perturbation

A 3-CNF splits into two independent parts. The scaffold is the m variable triples without sign — the clause-variable hypergraph. The signature is a sign assignment on top of it. Both can be drawn independently, and that is exactly the lever.

Scaffold g      m variable triples, without sign            60 pieces
  └ Signature s independent fair signs on it                16 per scaffold
      └ Run r   clauses and literals permuted                3 per signature

The third rank is a null perturbation: the same clause set in a different order. The answer has to be the same; the conflict count is not. What varies there is the solver's own noise and must not be attributed to the signs. Checked: in 0 of 960 cells did the answer diverge.

Why this is a bound, not a measurement

Every structural predictor this project has ever considered — expansion ∂S, double triples, pairs-2, treewidth, spectral gap, degree distribution — is a function of the scaffold alone. It is sign-blind. The best possible sign-blind predictor is the conditional expectation E[hardness | scaffold]. So for every one of them, without exception

r²(P, hardness)  ≤  σ²_A / (σ²_A + σ²_B + σ²_ε)

A single measurement thereby caps the entire class. The design does not answer "is this predictor any good," but "how much is there to gain on this axis at all."

§ 3

The decomposition

Two-fifths are fixed before the first sign

Nested analysis of variance on y = log₂(conflicts), unsatisfiable instances only, fixed n and α. Not a single run hit the conflict budget.

The share replicates on a second seed range and grows with n: 32 % at n = 150, 42–45 % at n = 200. Cross-checked distribution-free by permuting the signature → scaffold assignment, 20,000 draws: observed spread of the scaffold means 0.183 against a null median of 0.046, p < 5·10⁻⁵ in all three runs. The same permutation doubles as the negative control — without a real scaffold effect, the same computation yields zero.

The positive control

A finding without a positive control is not one. So scaffold g is deliberately injected with (g mod 4) · 15 double triples — the configuration with border ∂S = 0, the spark of width-bounded resolution. n, m, and α stay the same; only the scaffold structure changes, in a direction theory says must lower the hardness.

The design finds the planted effect (scaffold share 41.7 % → 60.4 %, F 6.8 → 14.3) and attributes it to the right feature: dopp explains r² = 0.67 of the between-scaffold variance there, against 0.006 on the natural scaffold. And exactly this contrast is the real takeaway — on the natural scaffold, the known local features explain almost nothing of the true 42 %.

§ 4

The carrier

It is the second moment of the degree sequence

Nineteen scaffold features, all computable in polynomial time from the sign-free hypergraph, against the scaffold mean of log₂(conflicts).

Two things stand out in this picture.

First: it is all the same quantity

grad_var and kk_gewicht yield correlations identical down to the last digit, because Σ_i≠j|C_i ∩ C_j| = Σ_v deg(v)(deg(v)−1). Measured: r(degree variance, Σdeg²) = +1.00000, because Σ_v deg(v) = 3m is fixed. The carrier is

Σ_v deg(v)²         a single pass over the clause list, O(m)

Second: it is not expansion

The spectral gap of the normalized Laplacian — the quantity that, via Cheeger, precisely bounds expansion, and that under this project's prior reading was the currency of the whole affair — says nothing about hardness within the family: r = +0.10 / +0.03 / +0.22, in three runs with the wrong sign. That was the prediction this measurement began with. It is refuted.

Tested against the order d(50 %)

d(50 %) — the number of random assumptions at which unit propagation runs into a contradiction in half the cases — was so far the only quantity with predictive power for hardness at fixed n. On the instance level, both on the same footing:

Quantity	n = 200 a	n = 200 b	out-of-sample	sign-blind	cost
sv1 (largest singular value)	−0.646	−0.651	—	yes	one SVD
Σ deg²	−0.598	−0.595	R² = 0.352	yes	O(m)
order d(50 %)	+0.387	+0.412	R² = 0.158	no	2,800 propagations

At the scaffold level, Σdeg² absorbs the order almost completely: r(d50, hardness | Σdeg²) = +0.137, whereas conversely r(Σdeg², hardness | d50) = −0.736 remains. At the instance level, d(50 %) retains a partial +0.23 — precisely what a scaffold-blind measure cannot see: the signs.

The ceiling is nearly reached

The decomposition says: no sign-blind predictor gets above r² = 0.417 [0.314–0.495] or 0.446 [0.333–0.532]. Σdeg² reaches out-of-sample 0.352. Roughly 79 % of all sign-blind information about hardness sits in this one number, and the rest of the axis is r² ≈ 0.09.

§ 5

The counter-checks

Three explanations it is not

Trivial explanation	tested as	result	remains partial
effective size	iteratively remove degree ≤ 1	n_eff = 199…200 of 200	does not apply
effective density	densest sub-hypergraph	range 4.2650…4.2879	−0.832 / −0.819
collider bias	d(50 %), unconditionally measurable	all −0.360 · UNSAT −0.358 · SAT −0.344	no conditioning acts

The third is the most important. Evaluation happens only on unsatisfiable instances, and UNSAT is a joint effect of scaffold and sign — conditioning on it can create spurious correlation. But d(50 %) needs neither solver nor satisfiability status and is therefore measurable unconditionally. Conditioning changes nothing there.

Does it measure the formula or the solver?

Conflicts are a search trace, and VSIDS favors high-degree variables — the finding could be a property of the heuristic. So the same instances are measured again, with instruments that do not search. Both programs share the generator, so demonstrably the same formulas are measured.

Instrument	branches	learns	heuristic	r against Σ deg²
CDCL conflicts	yes	yes	VSIDS	−0.945
width-3 closure	no	no	none	+0.700
order rate d(50 %)	no	no	none	−0.921

The signs fit together: more degree spread means a larger closure (more derivable narrow resolvents) and a lower d(50 %) (propagation runs into the contradiction earlier), and both mean fewer conflicts. Limit of this check: all three instruments are this project's own code; the counter-check against third-party code is still pending.

§ 6

The lever

The law outside its band

Up to this point everything is correlation over the generator's natural fluctuation: at n = 200 the degrees are Poisson(12.8), and the sample variance only ranges between 9.3 and 15.5. A law fitted on such a narrow band deserves to be tested outside it. So the degree spread is imposed rather than observed — every variable gets a target frequency with mean 3m/n and a desired spread, while n, m, and α stay the same.

Monotone across the whole span, in both seed ranges and at both n. The factor between regular and overdispersed is 38 at n = 150 and 114 at n = 200 — the gap grows with n. Two n-points don't establish an exponent; the direction is unambiguous.

§ 7

The sharpest counter-check

Not merely the shifted threshold

The strongest objection: degree spread lowers the satisfiability threshold α_c. At a fixed nominal α, an overdispersed formula therefore sits deeper in the unsatisfiable phase, and deep inside is easy to refute. The UNSAT share visibly does move along, from 24 % to 84 %. Then everything would just be the known density effect in disguise.

Measured, the threshold really does move: α_c from 4.409 (regular) to 4.062 (overdispersed). So every family is measured anew at its own α_c plus a fixed distance.

The comparable UNSAT shares confirm that the matching succeeded — the families really do sit at the same spot of the phase diagram. The effect nonetheless remains almost entirely intact: across all three distances together, r(Σdeg², hardness | distance) = −0.914 at N = 1384. And it is strongest near the threshold — exactly where this project operates.

§ 8

The width wall

The same ladder, on a second family

The true resolution width w* is exactly measurable: the width-w closure contains the empty clause if and only if w*(F) ≤ w. For the standard model, two anchor points are available — w* = 3 dies at n₅₀ = 52.9, w* = 4 about 55 later — giving w*(n) ≈ 0.018·n. That is the constant with which the bound of Ben-Sasson/Wigderson runs empty in the measurable range, and the reason the width road is considered closed.

A third anchor point would need width 5 and is computationally unreachable. So instead of raising the width, the family is switched.

The transition moves monotonically with degree spread, r = +0.99. And the calibration holds: my standard family gives n₅₀ = 53.1 against the project's 52.9, and at width 4 then 111.0 against 108.2. That measures the ladder for both families.

The result, and what it's worth

The constant in Ben-Sasson/Wigderson is family-dependent — 0.0214·n regular against 0.0173·n standard, factor 1.24. Real, measured, calibrated. And far too weak: the exponent (w*−3)²/n rises from 0.00032·n to 0.00046·n. The width road stays empty, now on two families instead of one. A cleanly closed road is a result — this one is, for the first time, backed by the positive control of a "harder family."

§ 9

The other axis

On the sign side there is almost nothing to find

42 % sit on the scaffold axis, and it is nearly exhausted. 54 % sit on the sign axis, and there, until now, only d(50 %) told us anything. The direct counterpart to Σdeg² is the imbalance Σ_v(pos(v) − neg(v))² — at a fixed scaffold, deg(v) is fixed, so everything about it is pure sign information.

The imbalance predicts d(50 %) with r ≈ +0.51, unconditionally and equally on both satisfiability sides. Against hardness, however, it switches sign: +0.25 on UNSAT, −0.23 on SAT. That is the signature of a threshold-distance quantity — more imbalance means more satisfiable; among those that are unsatisfiable anyway, one then sits closer to the threshold, and among the satisfiable ones, deeper in the SAT phase.

So the same test as for degree spread: draw signs with a bias, measure α_c(imbalance), compare at equal distance. Result: factor 1.24 / 1.09 / 1.03, against 15.0 / 11.1 / 6.6 for degree spread.

Imbalance acts only through the threshold. Degree spread does not. The two axes thus separate in mechanism, not just in magnitude.

A side finding belongs here too: at this density there are practically no pure literals — 0 to 3 at n = 200, r ≈ 0. The obvious mechanism simply doesn't exist.

§ 10

The balance sheet

Where the hardness actually sits

The scaffold axis is measured and largely closed: 42 % found, of which roughly four-fifths is in Σdeg². What comes after that only shows itself once the degree sequence is held fixed — on regular scaffolds, where Σdeg² cannot vary by construction, the scaffold share collapses from 27.4 % to 10.0 %, and a second quantity emerges there that was previously invisible: paare2, the clause pairs with ∂S = 2, jumps from r = −0.04 to −0.588. Once the degree sequence is fixed, the local overlap structure takes over.

Roughly half of all hardness variance sits on the sign axis and is touched by no structural quantity measured so far.

§ 11

Limits

What this does not say

It is not a refutation procedure. Σdeg² predicts which instances are hard, not how to refute a hard one. A path from here to a procedure is not in sight.

It says nothing about P versus NP. Random 3-SAT is neither necessary nor sufficient for that: P vs NP is a statement about the worst case. If random instances were easy, P = NP would not follow; if they are hard, P ≠ NP does not follow either.

The direction points away from the door. The hardest is the most uniform scaffold. The less expressive the structure, the more expensive the proof — the old diagnosis, now fitted with a lever and a dose-response curve.

What it is good for

For two things, and both are immediately actionable.

First: regress out Σ_v deg(v)² before every test of a new hardness predictor. One line, and the noise floor drops by 42 %. Every measurement in this project sits "at the threshold α = 4.267" — but α_c depends on the realized degree sequence. Instances at nominal 4.267 are therefore not all sitting at the threshold, but distributed over a range of distances. That is a plausible contributing cause for why earlier approaches came out at r ≈ 0: the single largest share of variance was a structural confounder nobody controlled for.

Second: regular 3-SAT at its own α_c ≈ 4.41 as a test family. At n = 200 it is sixteen times harder, the gap grows with n, and the degree spread is zero by construction — the dominant confounder is not controlled there, but absent. In hardness, n = 200 regular corresponds to roughly n ≈ 250 in the standard model; because everything runs exponentially in n, that is the difference between "still feasible" and "no longer feasible."

All numbers come from the raw data under mess_geruest/ and mess_zuendbreite/, around 21,000 solver runs. Tools: geruest_signum.rs, gradstreuung.rs, gradstreuung_beweis.rs, unwucht.rs, zuendbreite.rs; analysis geruest_analyse.py, geruest_merkmale.py, schwelle_gradstreuung.py, zuendbreite_analyse.py, unwucht_analyse.py. Chart data is generated by webdaten.py directly from the measurement series — no number on this page was entered by hand.

View code & data — Σdeg² and the 42 % of the scaffold axis

solver/src/bin/gradstreuung.rs — the measurement behind Σdeg²

//! # Degree spread as a lever — the prediction from the scaffold decomposition
//!
//! The decomposition (`geruest_signum`) finds: roughly 42 % of hardness
//! variance at fixed n sits in the sign-free scaffold, and the carrier is
//! the **second moment of the degree sequence** Σ_v deg(v)². Higher degree
//! spread means easier (r ≈ −0.83 over the scaffold means, replicated twice).
//!
//! So far this is a correlation over the generator's **natural spread**:
//! at n = 200, α = 4.267 the degrees are Poisson(12.8), and the sample
//! variance only ranges between 9.3 and 15.5. A law fitted on this narrow
//! band must be tested outside it.
//!
//! Here the degree spread is therefore **imposed** rather than observed.
//! Every variable v gets a target frequency c_v with mean 3m/n and a given
//! spread; the pool of c_v copies is shuffled and cut into triples. That
//! makes deg(v) = c_v exact.
//!
//! ```text
//!   sigma = 0.0   regular, every variable exactly equally often (spread 0)
//!   sigma = 3.58  corresponds to the standard model              (spread 12.8)
//!   sigma = 5.5   clearly overdispersed                          (spread 30)
//! ```
//!
//! n, m, α and the sign distribution stay the same in all cases.
//! **Prediction: hardness falls monotonically with degree spread, and
//! regular is the maximum.** This is a threefold extrapolation beyond the
//! fitted band, in both directions.
//!
//! Call: gradstreuung <n> [count=120] [seed] [alpha=4.267] [budget]
//! Output: n,alpha,sigma_ziel,instanz,gradvar,sat,unsat,konflikte
use ordnungssolver::cdcl;
use ordnungssolver::erzeuger::Zufall;
use ordnungssolver::formel::{Formel, Urteil};

fn main() {
    let a: Vec<String> = std::env::args().collect();
    let n: usize = a.get(1).and_then(|s| s.parse().ok()).expect("n fehlt");
    let anzahl: usize = a.get(2).and_then(|s| s.parse().ok()).unwrap_or(120);
    let saat: u64 = a.get(3).and_then(|s| s.parse().ok()).unwrap_or(20260820);
    let alpha: f64 = a.get(4).and_then(|s| s.parse().ok()).unwrap_or(4.267);
    let budget: u64 = a.get(5).and_then(|s| s.parse().ok()).unwrap_or(2_000_000);
    // Measure only one spread (negative = all). Allows measuring each
    // family at its OWN alpha — needed for the comparison at
    // equal distance to the threshold.
    let nur: f64 = a.get(6).and_then(|s| s.parse().ok()).unwrap_or(-1.0);

    let m = (alpha * n as f64).round() as usize;
    let sigmas = [0.0f64, 1.5, 2.5, 3.58, 4.5, 5.5];
    let mut rng = Zufall::neu(saat);

    println!("n,alpha,sigma_ziel,instanz,gradvar,sat,unsat,konflikte");
    for &sig in &sigmas {
        if nur >= 0.0 && (sig - nur).abs() > 1e-9 { continue; }
        let mut i = 0usize;
        let mut versuche = 0usize;
        while i < anzahl && versuche < anzahl * 20 {
            versuche += 1;
            let Some((f, gv)) = baue(n, m, sig, &mut rng) else { continue };
            let (urteil, konflikte) = cdcl::stufe3(&f, budget);
            let sat = matches!(urteil, Urteil::Erfuellbar(_));
            let unsat = urteil == Urteil::Unerfuellbar;
            if !sat && !unsat { continue; }
            println!("{n},{alpha},{sig},{i},{gv:.4},{},{},{konflikte}",
                     sat as u8, unsat as u8);
            i += 1;
        }
        eprintln!("sigma {sig}: {i} Instanzen ({versuche} Versuche)");
    }
}

/// Scaffold with imposed degree spread, then fair signs.
/// Also returns the actually achieved degree variance.
fn baue(n: usize, m: usize, sigma: f64, r: &mut Zufall) -> Option<(Formel, f64)> {
    let mu = 3.0 * m as f64 / n as f64;
    // --- Draw target frequencies c_v, bring the sum exactly to 3m ---
    let mut c: Vec<i64> = (0..n)
        .map(|_| {
            let z = if sigma > 0.0 { normal(r) } else { 0.0 };
            (mu + sigma * z).round().max(3.0) as i64
        })
        .collect();
    let ziel = 3 * m as i64;
    loop {
        let s: i64 = c.iter().sum();
        if s == ziel { break; }
        let i = r.unter(n as u64) as usize;
        if s < ziel { c[i] += 1; } else if c[i] > 3 { c[i] -= 1; }
    }
    let mittel = ziel as f64 / n as f64;
    let gv = c.iter().map(|&x| (x as f64 - mittel).powi(2)).sum::<f64>() / n as f64;

    // --- Shuffle the pool and cut it into triples ---
    let mut topf: Vec<usize> = Vec::with_capacity(ziel as usize);
    for (v, &k) in c.iter().enumerate() {
        for _ in 0..k { topf.push(v + 1); }
    }
    for i in (1..topf.len()).rev() {
        let j = r.unter((i + 1) as u64) as usize;
        topf.swap(i, j);
    }
    // Locally repair triples with repetition: swap the duplicate
    // occurrence with a random other pool slot. This preserves the
    // degree sequence c_v exactly — unlike discarding, which would
    // bias the spread.
    for _ in 0..200 {
        let mut schlecht = false;
        for k in 0..m {
            let (i, j, l) = (3 * k, 3 * k + 1, 3 * k + 2);
            for (x, y) in [(i, j), (i, l), (j, l)] {
                if topf[x] == topf[y] {
                    schlecht = true;
                    let z = r.unter(topf.len() as u64) as usize;
                    topf.swap(y, z);
                }
            }
        }
        if !schlecht { break; }
    }
    let mut kl: Vec<Vec<i32>> = Vec::with_capacity(m);
    for ch in topf.chunks(3) {
        if ch[0] == ch[1] || ch[0] == ch[2] || ch[1] == ch[2] { return None; }
        kl.push(ch.iter()
            .map(|&v| if r.bit() { v as i32 } else { -(v as i32) })
            .collect());
    }
    Some((Formel::mit(n, kl), gv))
}

/// Box-Muller from the built-in uniform generator.
fn normal(r: &mut Zufall) -> f64 {
    let u1 = (r.naechste() >> 11) as f64 / (1u64 << 53) as f64;
    let u2 = (r.naechste() >> 11) as f64 / (1u64 << 53) as f64;
    let u1 = u1.max(1e-12);
    (-2.0 * u1.ln()).sqrt() * (std::f64::consts::TAU * u2).cos()
}

geruest_analyse.py — analysis, produces the numbers on this page

"""
Scaffold versus sign — nested variance decomposition of hardness.

MODEL    y_gsr = μ + A_g + B_g(s) + ε_gsr        y = log2(conflicts), UNSAT only

  A_g     scaffold        (the sign-free clause-variable hypergraph)
  B_g(s)  sign            (signature s on the same scaffold)
  ε_gsr   own noise       (null perturbation: clauses/literals permuted,
                           same formula, same answer)

THE BOUND.  Every sign-blind predictor P — expansion ∂S,
double triples, pairs-2, treewidth, spectral gap, degree distribution — is a
function of the scaffold alone. The best possible such predictor is
E[y | scaffold]. So for every one of them

    r²(P, y)  ≤  σ²_A / (σ²_A + σ²_B + σ²_ε)          (against the measured value)
    r²(P, y)  ≤  σ²_A / (σ²_A + σ²_B)                 (against the noise-removed value)

This is not a measurement of one predictor, but a ceiling over the
entire class.
"""
import sys, math
import numpy as np


def lade(datei):
    kopf = open(datei).readline().strip().split(",")
    dat = np.loadtxt(datei, delimiter=",", skiprows=1)
    if dat.ndim == 1:
        dat = dat.reshape(1, -1)
    S = {k: i for i, k in enumerate(kopf)}
    return {k: dat[:, i] for k, i in S.items()}, dat.shape[0]


def pruefe_nullstoerung(d):
    """The permutation must not change the answer. Otherwise it isn't one."""
    schluessel = {}
    for i in range(len(d["geruest"])):
        k = (d["geruest"][i], d["signatur"][i])
        schluessel.setdefault(k, []).append((d["sat"][i], d["unsat"][i]))
    verletzt = sum(1 for v in schluessel.values() if len(set(v)) > 1)
    return verletzt, len(schluessel)


def zerlegung(d):
    """Unbalanced nested ANOVA, UNSAT formulas only."""
    ok = d["unsat"] == 1
    if ok.sum() == 0:
        return None
    g = d["geruest"][ok].astype(int)
    s = d["signatur"][ok].astype(int)
    y = np.log2(np.maximum(d["konflikte"][ok], 1.0))

    # cells = (scaffold, signature); R runs per cell
    zellen = {}
    for i in range(len(y)):
        zellen.setdefault((g[i], s[i]), []).append(y[i])
    geruste = {}
    for (gg, ss), w in zellen.items():
        geruste.setdefault(gg, []).append(np.array(w))

    N = sum(len(w) for w in zellen.values())
    gesamt = np.concatenate([w for w in zellen.values()])
    ybar = gesamt.mean()

    SS_e = df_e = 0.0
    SS_B = df_B = 0.0
    SS_A = 0.0
    gewichte = []
    for gg, zl in geruste.items():
        ng = sum(len(w) for w in zl)
        gbar = np.concatenate(zl).mean()
        gewichte.append(ng)
        SS_A += ng * (gbar - ybar) ** 2
        for w in zl:
            SS_e += ((w - w.mean()) ** 2).sum()
            df_e += len(w) - 1
            SS_B += len(w) * (w.mean() - gbar) ** 2
        df_B += len(zl) - 1
    G = len(geruste)
    df_A = G - 1
    if df_A < 1 or df_B < 1:
        return None

    MS_A = SS_A / df_A
    MS_B = SS_B / df_B if df_B > 0 else 0.0
    MS_e = SS_e / df_e if df_e > 0 else 0.0

    # mean cell occupancy (runs per signature) and ANOVA coefficient c
    R_quer = N / len(zellen)
    gewichte = np.array(gewichte, float)
    c = (N - (gewichte ** 2).sum() / N) / df_A

    var_e = MS_e
    var_B = max((MS_B - MS_e) / R_quer, 0.0)
    var_A = max((MS_A - MS_B) / c, 0.0)
    ges = var_A + var_B + var_e
    return dict(G=G, N=int(N), zellen=len(zellen), R=R_quer,
                var_A=var_A, var_B=var_B, var_e=var_e, gesamt=ges,
                anteil_A=var_A / ges if ges > 0 else 0.0,
                anteil_A_entrauscht=var_A / (var_A + var_B) if var_A + var_B > 0 else 0.0,
                sd_gesamt=math.sqrt(ges),
                MS_A=MS_A, MS_B=MS_B, MS_e=MS_e, df_A=df_A, df_B=df_B, df_e=df_e,
                F=MS_A / MS_B if MS_B > 0 else float("inf"))


def bootstrap(d, B=2000, saat=7):
    """Confidence band for the scaffold share: resample scaffolds with replacement."""
    rng = np.random.default_rng(saat)
    gs = np.unique(d["geruest"]).astype(int)
    werte, werte_e = [], []
    for _ in range(B):
        zug = rng.choice(gs, size=len(gs), replace=True)
        teile = {k: [] for k in d}
        neu_id = []
        for j, gg in enumerate(zug):
            msk = d["geruest"] == gg
            for k in d:
                teile[k].append(d[k][msk])
            neu_id.append(np.full(msk.sum(), j))
        dd = {k: np.concatenate(v) for k, v in teile.items()}
        dd["geruest"] = np.concatenate(neu_id).astype(float)
        z = zerlegung(dd)
        if z:
            werte.append(z["anteil_A"])
            werte_e.append(z["anteil_A_entrauscht"])
    if not werte:
        return None
    return (np.percentile(werte, [2.5, 97.5]),
            np.percentile(werte_e, [2.5, 97.5]))


def geruest_praediktor(d, name):
    """How much of the between-scaffold variance do the known
    scaffold features (double triples, pairs-2) actually capture?"""
    ok = d["unsat"] == 1
    if ok.sum() < 10:
        return
    g = d["geruest"][ok].astype(int)
    y = np.log2(np.maximum(d["konflikte"][ok], 1.0))
    gs = np.unique(g)
    mittel = np.array([y[g == gg].mean() for gg in gs])
    for merkmal in ("dopp", "paare2"):
        if merkmal not in d:
            continue
        x = np.array([d[merkmal][ok][g == gg][0] for gg in gs])
        if x.std() < 1e-12:
            print(f"    {merkmal:8s}  constant, no spread")
            continue
        r = np.corrcoef(x, mittel)[0, 1]
        print(f"    {merkmal:8s}  range {x.min():.0f}..{x.max():.0f}   "
              f"r(feature, scaffold mean) = {r:+.3f}   r² = {r*r:.3f}")


def bericht(datei, mit_bootstrap=True):
    d, zeilen = lade(datei)
    verletzt, zellen = pruefe_nullstoerung(d)
    n = int(np.median(d["n"]))
    alpha = float(np.median(d["alpha"]))
    unsat = int((d["unsat"] == 1).sum())
    offen = int(((d["sat"] == 0) & (d["unsat"] == 0)).sum())

    print(f"\n{'='*74}")
    print(f"  {datei}")
    print(f"  n = {n}   α = {alpha}   rows = {zeilen}   of which UNSAT runs = {unsat}"
          f"   budget hit = {offen}")
    print(f"  null-perturbation check: {verletzt} of {zellen} cells with "
          f"inconsistent answer  {'← ERROR' if verletzt else '(clean)'}")
    print(f"{'='*74}")

    z = zerlegung(d)
    if not z:
        print("  too little data")
        return None
    print(f"  scaffolds {z['G']}   UNSAT signatures {z['zellen']}   "
          f"runs per signature {z['R']:.2f}")
    print()
    print(f"  spread of log2(conflicts), UNSAT, fixed n:  "
          f"σ_total = {z['sd_gesamt']:.4f}")
    print(f"  {'source':<28} {'variance':>10}  {'share':>8}   {'σ':>8}")
    print(f"  {'-'*28} {'-'*10}  {'-'*8}   {'-'*8}")
    for lab, v in (("A  scaffold (sign-blind)", z["var_A"]),
                   ("B  sign | scaffold", z["var_B"]),
                   ("ε  solver's own noise", z["var_e"])):
        print(f"  {lab:<28} {v:10.5f}  {v/z['gesamt']:7.1%}   {math.sqrt(v):8.4f}")
    print(f"  {'-'*28} {'-'*10}  {'-'*8}")
    print(f"  {'total':<28} {z['gesamt']:10.5f}  {1.0:7.1%}")
    print()
    print(f"  F(scaffold against sign) = {z['F']:.3f}   "
          f"df = {z['df_A']}, {z['df_B']}")
    print()
    print(f"  ► CEILING for every sign-blind predictor:")
    print(f"      r² ≤ {z['anteil_A']:.4f}   (against measured hardness)"
          f"     |r| ≤ {math.sqrt(z['anteil_A']):.3f}")
    print(f"      r² ≤ {z['anteil_A_entrauscht']:.4f}   (noise-removed)"
          f"          |r| ≤ {math.sqrt(z['anteil_A_entrauscht']):.3f}")
    if mit_bootstrap:
        bs = bootstrap(d)
        if bs:
            (lo, hi), (loe, hie) = bs
            print(f"      95% bootstrap over scaffolds: "
                  f"[{lo:.4f}, {hi:.4f}] and [{loe:.4f}, {hie:.4f}]")
    print()
    print(f"  scaffold features against scaffold mean:")
    geruest_praediktor(d, datei)
    return z


if __name__ == "__main__":
    for datei in sys.argv[1:]:
        bericht(datei)

script#daten — the same raw data that draw the charts on this page

Not a single run hit the conflict budget. The cap on width-bounded saturation stood on the full space bound and could not trigger; every reported w* is a verdict, not a timeout.