Messprotokoll 20. August 2026 zufälliges 3-SAT, α = 4,267 rund 21 000 Solverläufe

Gerüst und
Vorzeichen

Wovon es abhängt, wie schwer eine einzelne unerfüllbare Instanz an der Schwelle ist — und wovon nicht.

41,7 %der Härtestreuung liegen schon im vorzeichenlosen Gerüst

Σ grad²trägt sie — ein Durchlauf über die Klauselliste

16×schwerer ist reguläres 3-SAT bei n = 200

49 %bleiben auf der Vorzeichenachse unerklärt

§ 1

Die Frage

Nicht ob die Information da ist

Gegenstand ist zufälliges 3-SAT an der Erfüllbarkeitsschwelle α = m/n ≈ 4,267. Dort ist etwa die Hälfte der Instanzen unerfüllbar, und dort sind sie am schwersten.

Dass die Information „lösbar oder unlösbar" in der Formel steckt, ist keine Frage: Unerfüllbarkeit ist eine wohldefinierte Eigenschaft der Klauselmenge, invariant unter Umbenennung und Permutation. Resolution ist vollständig, es fehlt nichts im Wortschatz. Was fehlt, ist Kürze — für zufälliges 3-CNF hat jeder Resolutionsbeweis Grösse 2^Ω(n) (Chvátal/Szemerédi 1988).

Diese Untersuchung beantwortet diese Frage nicht. Sie beantwortet eine kleinere, die ihr vorgelagert ist:

Zwei unerfüllbare Instanzen mit demselben n und demselben α unterscheiden sich in den Widerlegungskosten um Grössenordnungen. Wovon hängt das ab?

Die Antwort zerfällt in zwei Achsen, und sie fallen sehr verschieden aus.

§ 2

Der Aufbau

Gerüst, Signatur, Nullstörung

Eine 3-CNF zerfällt in zwei unabhängige Teile. Das Gerüst sind die m Variablentripel ohne Vorzeichen — der Klausel-Variablen-Hypergraph. Die Signatur ist eine Vorzeichenbelegung darauf. Beides lässt sich getrennt würfeln, und genau das ist der Hebel.

Gerüst g        m Variablentripel, ohne Vorzeichen          60 Stück
  └ Signatur s  unabhängige faire Vorzeichen darauf         16 je Gerüst
      └ Lauf r  Klauseln und Literale permutiert             3 je Signatur

Der dritte Rang ist eine Nullstörung: dieselbe Klauselmenge in anderer Reihenfolge. Die Antwort muss dieselbe sein, die Konfliktzahl ist es nicht. Was dort schwankt, ist Eigenrauschen des Solvers und darf den Vorzeichen nicht zugeschlagen werden. Geprüft: in 0 von 960 Zellen wich die Antwort ab.

Warum das eine Schranke ist und keine Messung

Jeder strukturelle Prädiktor, den dieses Projekt je betrachtet hat — Expansion ∂S, Doppeltripel, Paare2, Baumweite, Spektrallücke, Gradverteilung — ist eine Funktion allein des Gerüsts. Er ist vorzeichenblind. Der bestmögliche vorzeichenblinde Prädiktor ist der bedingte Erwartungswert E[Härte | Gerüst]. Also gilt für jeden von ihnen ohne Ausnahme

r²(P, Härte)  ≤  σ²_A / (σ²_A + σ²_B + σ²_ε)

Eine Messung deckelt damit die ganze Klasse. Der Aufbau beantwortet nicht „taugt dieser Prädiktor", sondern „wieviel ist auf dieser Achse überhaupt zu holen".

§ 3

Die Zerlegung

Zwei Fünftel stehen vor dem ersten Vorzeichen fest

Geschachtelte Varianzanalyse auf y = log₂(Konflikte), nur unerfüllbare Instanzen, festes n und α. Kein einziger Lauf ist ins Konfliktbudget gelaufen.

Der Anteil repliziert an einem zweiten Startwertbereich und wächst mit n: 32 % bei n = 150, 42–45 % bei n = 200. Verteilungsfrei gegengeprüft durch Permutation der Zuordnung Signatur → Gerüst, 20 000 Ziehungen: beobachtete Streuung der Gerüstmittel 0,183 gegen Null-Median 0,046, p < 5·10⁻⁵ in allen drei Läufen. Dieselbe Permutation ist zugleich die Negativkontrolle — ohne echten Gerüsteffekt liefert derselbe Rechenweg null.

Die Positivkontrolle

Ein Befund ohne Positivkontrolle ist keiner. Also bekommt Gerüst g gezielt (g mod 4) · 15 doppelte Tripel eingespritzt — die Konfiguration mit Rand ∂S = 0, der Zündfunke der breitenbeschränkten Resolution. n, m und α bleiben gleich; nur die Gerüststruktur ändert sich, in einer Richtung, von der die Theorie sagt, dass sie die Härte senken muss.

Der Aufbau findet den gepflanzten Effekt (Gerüstanteil 41,7 % → 60,4 %, F 6,8 → 14,3) und schreibt ihn dem richtigen Merkmal zu: dopp erklärt dort r² = 0,67 der Zwischen-Gerüst-Streuung, gegen 0,006 am natürlichen Gerüst. Und genau dieser Kontrast ist die eigentliche Auskunft — am natürlichen Gerüst erklären die bekannten lokalen Merkmale von den echten 42 % fast nichts.

§ 4

Der Träger

Es ist das zweite Moment der Gradfolge

Neunzehn Gerüstmerkmale, alle in polynomialer Zeit aus dem vorzeichenlosen Hypergraphen, gegen das Gerüstmittel von log₂(Konflikte).

Zwei Dinge stehen in diesem Bild.

Erstens: es ist alles dieselbe Grösse

grad_var und kk_gewicht liefern bis auf die letzte Stelle identische Korrelationen, weil Σ_i≠j|C_i ∩ C_j| = Σ_v grad(v)(grad(v)−1) ist. Gemessen ist r(Gradvarianz, Σgrad²) = +1,00000, weil Σ_v grad(v) = 3m fest liegt. Der Träger ist

Σ_v grad(v)²        ein Durchlauf über die Klauselliste, O(m)

Zweitens: die Expansion ist es nicht

Die Spektrallücke des normierten Laplace-Operators — die Grösse, die über Cheeger genau die Expansion beschränkt und die nach der bisherigen Lesart des Projekts die Währung der ganzen Sache ist — sagt über die Härte innerhalb der Familie nichts: r = +0,10 / +0,03 / +0,22, in drei Läufen mit dem falschen Vorzeichen. Das war die Vorhersage, mit der diese Messung begonnen wurde. Sie ist widerlegt.

Gegen die Ordnung d(50 %) gestellt

d(50 %) — die Zahl zufälliger Annahmen, bei der Einheitspropagation in der Hälfte der Fälle in den Widerspruch läuft — war bisher die einzige Grösse mit Vorhersagekraft für die Härte bei festem n. Auf Instanzebene, beide auf derselben Ebene:

Grösse	n = 200 a	n = 200 b	out-of-sample	vorzeichenblind	Kosten
sv1 (grösster Singulärwert)	−0,646	−0,651	—	ja	eine SVD
Σ grad²	−0,598	−0,595	R² = 0,352	ja	O(m)
Ordnung d(50 %)	+0,387	+0,412	R² = 0,158	nein	2 800 Propagationen

Auf Gerüstebene saugt Σgrad² die Ordnung fast vollständig auf: r(d50, Härte | Σgrad²) = +0,137, während umgekehrt r(Σgrad², Härte | d50) = −0,736 bleibt. Auf Instanzebene behält d(50 %) partiell +0,23 — und zwar genau das, was ein gerüstblindes Mass nicht sehen kann: die Vorzeichen.

Der Deckel ist fast erreicht

Die Zerlegung sagt: kein vorzeichenblinder Prädiktor kommt über r² = 0,417 [0,314–0,495] bzw. 0,446 [0,333–0,532]. Σgrad² erreicht out-of-sample 0,352. Rund 79 % der gesamten vorzeichenblinden Information über die Härte stecken in dieser einen Zahl, und der Rest der Achse ist r² ≈ 0,09.

§ 5

Die Gegenproben

Drei Erklärungen, die es nicht sind

Trivialerklärung	geprüft als	Ergebnis	partiell bleibt
effektive Grösse	Grad ≤ 1 iteriert entfernen	n_eff = 199…200 von 200	greift nicht
effektive Dichte	dichtester Teil-Hypergraph	Spanne 4,2650…4,2879	−0,832 / −0,819
Kollider-Verzerrung	d(50 %), unbedingt messbar	alle −0,360 · UNSAT −0,358 · SAT −0,344	keine Bedingung wirkt

Die dritte ist die wichtigste. Ausgewertet wird nur auf unerfüllbaren Instanzen, und UNSAT ist eine gemeinsame Wirkung von Gerüst und Vorzeichen — darauf zu bedingen kann Scheinkorrelation erzeugen. d(50 %) braucht aber weder Solver noch Erfüllbarkeitsstatus und ist deshalb unbedingt messbar. Die Bedingung ändert dort nichts.

Misst es die Formel oder den Solver?

Konflikte sind eine Suchspur, und VSIDS bevorzugt hochgradige Variablen — der Befund könnte eine Eigenschaft der Heuristik sein. Also dieselben Instanzen noch einmal, mit Instrumenten, die nicht suchen. Beide Programme teilen sich den Erzeuger, damit nachweislich dieselben Formeln gemessen werden.

Instrument	verzweigt	lernt	Heuristik	r gegen Σ grad²
CDCL-Konflikte	ja	ja	VSIDS	−0,945
Abschluss der Breite 3	nein	nein	keine	+0,700
Ordnungsrate d(50 %)	nein	nein	keine	−0,921

Die Vorzeichen passen zusammen: mehr Gradstreuung heisst grösserer Abschluss (mehr ableitbare schmale Resolventen) und niedrigeres d(50 %) (Propagation läuft früher in den Widerspruch), und beides heisst weniger Konflikte. Grenze dieser Kontrolle: alle drei Instrumente sind Eigenbau dieses Projekts; die Gegenprobe an fremdem Code steht aus.

§ 6

Die Stellschraube

Das Gesetz ausserhalb seines Bandes

Bis hierher ist alles Korrelation über die natürliche Schwankung des Erzeugers: bei n = 200 sind die Grade Poisson(12,8), die Stichprobenvarianz schwankt nur zwischen 9,3 und 15,5. Ein Gesetz auf so schmalem Band gehört ausserhalb geprüft. Also wird die Gradstreuung vorgegeben statt beobachtet — jede Variable bekommt eine Zielhäufigkeit mit Mittel 3m/n und gewünschter Streuung, n, m und α bleiben gleich.

Monoton über die ganze Spanne, in beiden Startwertbereichen und bei beiden n. Der Faktor zwischen regulär und überstreut beträgt 38 bei n = 150 und 114 bei n = 200 — der Abstand wächst mit n. Zwei n-Punkte begründen keinen Exponenten; die Richtung ist eindeutig.

§ 7

Die schärfste Gegenprobe

Nicht bloss die verschobene Schwelle

Der stärkste Einwand: die Gradstreuung senkt die Erfüllbarkeitsschwelle α_c. Bei festem nominellem α sitzt eine überstreute Formel deshalb tiefer in der unerfüllbaren Phase, und tief drin ist leicht zu widerlegen. Der UNSAT-Anteil wandert ja sichtbar von 24 % auf 84 % mit. Dann wäre alles nur der bekannte Dichteeffekt in Verkleidung.

Gemessen wandert die Schwelle wirklich: α_c von 4,409 (regulär) auf 4,062 (überstreut). Also wird jede Familie bei ihrem eigenen α_c plus festem Abstand neu gemessen.

Die vergleichbaren UNSAT-Anteile belegen, dass die Anpassung gelungen ist — die Familien sitzen wirklich an derselben Stelle des Phasendiagramms. Der Effekt bleibt trotzdem fast vollständig: über alle drei Abstände zusammen r(Σgrad², Härte | Abstand) = −0,914 bei N = 1384. Und er ist nahe der Schwelle am stärksten, also genau dort, wo dieses Projekt arbeitet.

§ 8

Die Breitenwand

Dieselbe Leiter, an einer zweiten Familie

Die wahre Resolutionsbreite w* ist exakt messbar: der Abschluss der Breite w enthält die leere Klausel genau dann, wenn w*(F) ≤ w. Für das Standardmodell liegen zwei Stützpunkte vor — w* = 3 stirbt bei n₅₀ = 52,9, w* = 4 rund 55 später — und daraus w*(n) ≈ 0,018·n. Das ist die Konstante, mit der die Schranke von Ben-Sasson/Wigderson im messbaren Bereich leer läuft, und der Grund, warum der Breitenweg als geschlossen gilt.

Ein dritter Stützpunkt bräuchte Breite 5 und ist rechnerisch unerreichbar. Also wird nicht die Breite erhöht, sondern die Familie gewechselt.

Der Übergang wandert monoton mit der Gradstreuung, r = +0,99. Und die Eichung sitzt: meine Standardfamilie liefert n₅₀ = 53,1 gegen die 52,9 des Projekts, bei Breite 4 dann 111,0 gegen 108,2. Damit ist die Leiter für beide Familien vermessen.

Das Ergebnis, und was es wert ist

Die Konstante in Ben-Sasson/Wigderson ist familienabhängig — 0,0214·n regulär gegen 0,0173·n Standard, Faktor 1,24. Real, gemessen, kalibriert. Und viel zu schwach: der Exponent (w*−3)²/n steigt von 0,00032·n auf 0,00046·n. Der Breitenweg bleibt leer, jetzt an zwei Familien statt einer. Ein sauber geschlossener Weg ist ein Ergebnis — dieser ist erstmals gegen die Positivkontrolle „härtere Familie" abgesichert.

§ 9

Die andere Achse

Auf der Vorzeichenseite ist fast nichts zu finden

Auf der Gerüstachse liegen 42 %, und sie sind fast ausgeschöpft. Auf der Vorzeichenachse liegen 54 %, und dort wusste bisher nur d(50 %) etwas. Das direkte Gegenstück zu Σgrad² ist die Unwucht Σ_v(pos(v) − neg(v))² — bei festem Gerüst ist grad(v) fix, also ist alles daran reine Vorzeicheninformation.

Die Unwucht sagt d(50 %) mit r ≈ +0,51 vorher, unbedingt und auf beiden Erfüllbarkeitsseiten gleich. Gegen die Härte aber wechselt sie das Vorzeichen: +0,25 auf UNSAT, −0,23 auf SAT. Das ist die Signatur einer Schwellenabstands-Grösse — mehr Unwucht heisst erfüllbarer; unter den trotzdem unerfüllbaren sitzt man dann näher an der Schwelle, unter den erfüllbaren tiefer in der SAT-Phase.

Also dieselbe Prüfung wie bei der Gradstreuung: Vorzeichen mit Bias ziehen, α_c(Unwucht) messen, bei gleichem Abstand vergleichen. Ergebnis: Faktor 1,24 / 1,09 / 1,03, gegen 15,0 / 11,1 / 6,6 bei der Gradstreuung.

Die Unwucht wirkt nur über die Schwelle. Die Gradstreuung nicht. Damit trennen sich die beiden Achsen im Mechanismus, nicht nur im Betrag.

Ein Nebenbefund gehört dazu: reine Literale gibt es bei dieser Dichte praktisch nicht — 0 bis 3 Stück bei n = 200, r ≈ 0. Der naheliegende Mechanismus existiert schlicht nicht.

§ 10

Die Bilanz

Wo die Härte wirklich sitzt

Die Gerüstachse ist vermessen und weitgehend zu: 42 % gefunden, davon rund vier Fünftel in Σgrad². Was dahinter noch kommt, zeigt sich erst, wenn man die Gradfolge festhält — auf regulären Gerüsten, wo Σgrad² konstruktionsbedingt nicht variieren kann, bricht der Gerüstanteil von 27,4 % auf 10,0 % ein, und dort tritt eine zweite Grösse hervor, die vorher unsichtbar war: paare2, die Klauselpaare mit ∂S = 2, springt von r = −0,04 auf −0,588. Sobald die Gradfolge festliegt, übernimmt die lokale Überlappungsstruktur.

Rund die Hälfte der gesamten Härtestreuung sitzt auf der Vorzeichenachse und wird von keiner bisher gemessenen Strukturgrösse berührt.

§ 11

Grenzen

Was das nicht sagt

Es ist kein Widerlegungsverfahren. Σgrad² sagt vorher, welche Instanzen schwer sind, nicht wie man eine schwere widerlegt. Ein Weg von hier zu einem Verfahren ist nicht in Sicht.

Es sagt nichts über P gegen NP. Zufalls-3-SAT ist weder notwendig noch hinreichend dafür: P vs NP ist eine Aussage über den schlimmsten Fall. Wären Zufallsinstanzen leicht, folgte P = NP nicht; sind sie schwer, folgt P ≠ NP nicht.

Die Richtung zeigt von der Tür weg. Am schwersten ist das gleichmässigste Gerüst. Je ausdrucksloser die Struktur, desto teurer der Beweis — die alte Diagnose, jetzt mit einer Stellschraube und einer Dosis-Wirkungs-Kurve versehen.

Wofür es taugt

Für zwei Dinge, und beide sind sofort umsetzbar.

Erstens: Σ_v grad(v)² vor jedem Test eines neuen Härteprädiktors herausregressieren. Eine Zeile, und der Rauschboden fällt um 42 %. Jede Messung dieses Projekts sitzt „an der Schwelle α = 4,267" — aber α_c hängt von der realisierten Gradfolge ab. Instanzen bei nominell 4,267 sitzen deshalb nicht alle an der Schwelle, sondern über einen Bereich von Abständen verteilt. Das ist eine plausible Mitursache dafür, warum frühere Zugänge auf r ≈ 0 kamen: der grösste einzelne Varianzanteil war ein struktureller Störfaktor, gegen den niemand kontrolliert hat.

Zweitens: reguläres 3-SAT bei seinem eigenen α_c ≈ 4,41 als Prüffamilie. Es ist bei n = 200 sechzehnmal schwerer, der Abstand wächst mit n, und die Gradstreuung ist konstruktionsbedingt null — der dominante Störfaktor ist dort nicht kontrolliert, sondern abwesend. In der Härte entspricht n = 200 regulär etwa n ≈ 250 im Standardmodell; weil alles exponentiell in n läuft, ist das der Unterschied zwischen „geht noch" und „geht nicht mehr".

Alle Zahlen aus den Rohdaten unter mess_geruest/ und mess_zuendbreite/, rund 21 000 Solverläufe. Werkzeuge: geruest_signum.rs, gradstreuung.rs, gradstreuung_beweis.rs, unwucht.rs, zuendbreite.rs; Auswertung geruest_analyse.py, geruest_merkmale.py, schwelle_gradstreuung.py, zuendbreite_analyse.py, unwucht_analyse.py. Diagrammdaten erzeugt webdaten.py direkt aus den Messreihen — keine Zahl auf dieser Seite ist von Hand eingetragen.

Code & Daten ansehen — Σgrad² und die 42 % der Gerüstachse

solver/src/bin/gradstreuung.rs — die Messung hinter Σgrad²

//! # Gradstreuung als Stellschraube — die Vorhersage aus der Gerüstzerlegung
//!
//! Die Zerlegung (`geruest_signum`) findet: rund 42 % der Härtestreuung bei
//! festem n liegen im vorzeichenlosen Gerüst, und der Träger ist das
//! **zweite Moment der Gradfolge** Σ_v grad(v)². Höhere Gradstreuung heisst
//! leichter (r ≈ −0,83 über die Gerüstmittel, zweimal repliziert).
//!
//! Das ist bisher eine Korrelation über die **natürliche Streuung** des
//! Erzeugers: bei n = 200, α = 4,267 sind die Grade Poisson(12,8), und die
//! Stichprobenvarianz schwankt nur zwischen 9,3 und 15,5. Ein Gesetz, das
//! auf diesem schmalen Band gefittet ist, muss ausserhalb geprüft werden.
//!
//! Hier wird die Gradstreuung deshalb **vorgegeben** statt beobachtet. Jede
//! Variable v bekommt eine Zielhäufigkeit c_v mit Mittel 3m/n und
//! vorgegebener Streuung; der Topf aus c_v Kopien wird gemischt und in
//! Tripel geschnitten. Damit ist grad(v) = c_v exakt.
//!
//! ```text
//!   sigma = 0.0   regulär, jede Variable exakt gleich oft  (Streuung 0)
//!   sigma = 3.58  entspricht dem Standardmodell             (Streuung 12,8)
//!   sigma = 5.5   deutlich überstreut                       (Streuung 30)
//! ```
//!
//! n, m, α und die Vorzeichenverteilung bleiben in allen Fällen gleich.
//! **Vorhersage: die Härte fällt monoton mit der Gradstreuung, und regulär
//! ist das Maximum.** Das ist eine Extrapolation um den Faktor drei über
//! das gefittete Band hinaus, in beide Richtungen.
//!
//! Aufruf: gradstreuung <n> [anzahl=120] [saat] [alpha=4.267] [budget]
//! Ausgabe: 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);
    // Nur eine Streuung messen (negativ = alle). Erlaubt, jede Familie
    // bei ihrem EIGENEN alpha zu messen — nötig für den Vergleich bei
    // gleichem Abstand zur Schwelle.
    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)");
    }
}

/// Gerüst mit vorgegebener Gradstreuung, dann faire Vorzeichen.
/// Gibt zusätzlich die tatsächlich erreichte Gradvarianz zurück.
fn baue(n: usize, m: usize, sigma: f64, r: &mut Zufall) -> Option<(Formel, f64)> {
    let mu = 3.0 * m as f64 / n as f64;
    // --- Zielhäufigkeiten c_v ziehen, Summe exakt auf 3m bringen ---
    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;

    // --- Topf mischen und in Tripel schneiden ---
    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);
    }
    // Tripel mit Wiederholung lokal reparieren: das doppelte Vorkommen
    // mit einer zufälligen anderen Topfstelle tauschen. Das erhält die
    // Gradfolge c_v exakt — anders als Verwerfen, das die Streuung
    // verzerren würde.
    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 aus dem eingebauten Gleichverteiler.
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 — Auswertung, erzeugt die Zahlen dieser Seite

"""
Gerüst gegen Vorzeichen — geschachtelte Varianzzerlegung der Härte.

MODELL   y_gsr = μ + A_g + B_g(s) + ε_gsr        y = log2(Konflikte), nur UNSAT

  A_g     Gerüst          (der vorzeichenlose Klausel-Variablen-Hypergraph)
  B_g(s)  Vorzeichen      (Signatur s auf demselben Gerüst)
  ε_gsr   Eigenrauschen   (Nullstörung: Klauseln/Literale permutiert,
                           dieselbe Formel, dieselbe Antwort)

DIE SCHRANKE.  Jeder vorzeichenblinde Prädiktor P — Expansion ∂S,
Doppeltripel, Paare2, Baumweite, Spektrallücke, Gradverteilung — ist eine
Funktion allein des Gerüsts. Der bestmögliche solche Prädiktor ist
E[y | Gerüst]. Also gilt für jeden von ihnen

    r²(P, y)  ≤  σ²_A / (σ²_A + σ²_B + σ²_ε)          (gegen Gemessenes)
    r²(P, y)  ≤  σ²_A / (σ²_A + σ²_B)                 (gegen Rauschbereinigtes)

Das ist keine Messung eines Prädiktors, sondern ein Deckel über die
ganze Klasse.
"""
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):
    """Die Permutation darf die Antwort nicht ändern. Sonst ist sie keine."""
    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):
    """Unbalancierte geschachtelte ANOVA, nur UNSAT-Formeln."""
    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))

    # Zellen = (Gerüst, Signatur); R Läufe je Zelle
    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

    # mittlere Zellbesetzung (Läufe je Signatur) und ANOVA-Koeffizient 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):
    """Vertrauensband für den Gerüstanteil: Gerüste mit Zurücklegen ziehen."""
    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):
    """Wieviel der Zwischen-Gerüst-Streuung fangen die bekannten
    Gerüstmerkmale (Doppeltripel, Paare2) tatsächlich ein?"""
    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}  konstant, keine Streuung")
            continue
        r = np.corrcoef(x, mittel)[0, 1]
        print(f"    {merkmal:8s}  Spanne {x.min():.0f}..{x.max():.0f}   "
              f"r(Merkmal, Gerüstmittel) = {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}   Zeilen = {zeilen}   davon UNSAT-Läufe = {unsat}"
          f"   Budget gerissen = {offen}")
    print(f"  Nullstörungs-Prüfung: {verletzt} von {zellen} Zellen mit "
          f"uneinheitlicher Antwort  {'← FEHLER' if verletzt else '(sauber)'}")
    print(f"{'='*74}")

    z = zerlegung(d)
    if not z:
        print("  zu wenig Daten")
        return None
    print(f"  Gerüste {z['G']}   UNSAT-Signaturen {z['zellen']}   "
          f"Läufe je Signatur {z['R']:.2f}")
    print()
    print(f"  Streuung von log2(Konflikte), UNSAT, festes n:  "
          f"σ_gesamt = {z['sd_gesamt']:.4f}")
    print(f"  {'Quelle':<28} {'Varianz':>10}  {'Anteil':>8}   {'σ':>8}")
    print(f"  {'-'*28} {'-'*10}  {'-'*8}   {'-'*8}")
    for lab, v in (("A  Gerüst (vorzeichenblind)", z["var_A"]),
                   ("B  Vorzeichen | Gerüst", z["var_B"]),
                   ("ε  Eigenrauschen Solver", 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"  {'gesamt':<28} {z['gesamt']:10.5f}  {1.0:7.1%}")
    print()
    print(f"  F(Gerüst gegen Vorzeichen) = {z['F']:.3f}   "
          f"df = {z['df_A']}, {z['df_B']}")
    print()
    print(f"  ► DECKEL für jeden vorzeichenblinden Prädiktor:")
    print(f"      r² ≤ {z['anteil_A']:.4f}   (gegen gemessene Härte)"
          f"     |r| ≤ {math.sqrt(z['anteil_A']):.3f}")
    print(f"      r² ≤ {z['anteil_A_entrauscht']:.4f}   (rauschbereinigt)"
          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 über Gerüste: "
                  f"[{lo:.4f}, {hi:.4f}] bzw. [{loe:.4f}, {hie:.4f}]")
    print()
    print(f"  Gerüstmerkmale gegen Gerüstmittel:")
    geruest_praediktor(d, datei)
    return z


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

script#daten — dieselben Rohdaten, die die Grafiken auf dieser Seite zeichnen

Kein Lauf ist ins Konfliktbudget gelaufen. Die Kappe der breitenbeschränkten Sättigung stand auf der vollen Raumschranke und konnte nicht feuern; jedes gemeldete w* ist ein Urteil, keine Zeitüberschreitung.