Von einer Sonde, die nicht löst, zum ersten Eingriff in diesem Bestand — und warum beide kausalen Gerüstgrössen nur über Löser wirken, die auf Struktur reagieren.
Die Zahl der kritischen Klauseln einer unerfüllbaren Instanz — Klauseln, deren Entfernen sie erfüllbar macht — korreliert mit der Härte. Sie auf dem naheliegenden Weg zu messen heisst, die Instanz je Klausel einmal zu lösen, und das ist zirkulär. Gefragt war, ob eine billige Antwort auf eine kleine Störung dasselbe Signal trägt.
Sie tut es, über ein Zertifikat. Lokale Suche mit festem Budget besucht Belegungen, die genau eine Klausel verletzen; diese Klausel ist dann beweisbar kritisch, und entschieden wurde nichts. Auf 600 unerfüllbaren Instanzen ist die so gefundene Menge bei 72–99 % der Instanzen exakt die kritische Menge, enthält nie eine Klausel zu viel und korreliert so stark mit der Härte wie die teure Fassung.
| n | r(|K|, log Härte) | |K| = kritische Menge | Kosten gegen einen Löserlauf |
|---|---|---|---|
| 70 | +0,42 | 98,5 % | 319× |
| 100 | +0,32 | 90,5 % | 72× |
| 130 | +0,38 | 72,5 % | 31× |
Die Sonde wächst wie n^1,15, der Löser exponentiell; die beiden kreuzen sich bei n ≈ 120–200. Bei den gemessenen Grössen ist die Sonde noch die teurere — eine Aussage über den Vorsprung des Lösers, nicht über die Sonde.
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 ←Vier billige Grössen korrelierten immer wieder mit der Härte und untereinander: die Bethe-Entropie, wie viele Klauseln eine Instanz bis zum Kippen verträgt, der Punkt, an dem Belief Propagation nicht mehr konvergiert, und die kritische Menge. Sie erweisen sich als vier Schätzungen einer einzigen Distanz — wie weit die Instanz von ihrer eigenen Erfüllbarkeitsschwelle entfernt ist. Die Grundwahrheit, der erste unerfüllbare Präfix einer Klauselfolge, ist per Bisektion exakt, weil Erfüllbarkeit entlang der Folge monoton ist; Belief Propagation stimmt damit nach Reliabilitätskorrektur zu 0,79–0,81 überein.
Neben dieser Achse, fast orthogonal dazu, liegt die Streuung der Variablengrade (Σ grad²). Wäre sie über die Schwelle vermittelt, betrüge ihre Korrelation mit der Härte r(Σ grad², Schwelle)·r(Schwelle, Härte) ≈ −0,03; gemessen sind −0,45 bis −0,52. Auf der unerfüllbaren Seite ist sie die grössere der beiden Achsen: die Schwelle allein erklärt kreuzvalidiert R² = 0,12–0,16, zusammen mit der Gradstreuung 0,35–0,43.
Was das Spektrum über Σ grad² hinaus trägt, ist eine zweite Gradgrösse: ob hochgradige Variablen gemeinsam in Klauseln stehen — die Gradkorrelation C.
Eine Korrelation kann einen Hebel nicht von einem Stellvertreter unterscheiden. Also wurden die Instanzen umverdrahtet: zwei Slots tauschen ihre Variablen, die Vorzeichen bleiben am Slot, die Gradfolge bleibt exakt erhalten, die Erfüllbarkeit wird alle zehn Tausche geprüft, die Schwelle geht als Kovariate ein. Vier Arme je Instanz — C um 2,5 natürliche Standardabweichungen hoch, C tief, ein neutraler Arm mit gleich vielen Tauschen und festem C, und eine Positivkontrolle, die Σ grad² hebt. Vorhersage, erwartete Grösse und Entscheidungsregel standen vor dem Lauf im Quelltext.
| unerfüllbar, C hoch − C tief | n = 100 | n = 130 |
|---|---|---|
| DPLL (Jeroslow–Wang), primär | −0,77 [−0,82, −0,71] | −0,94 [−1,01, −0,87] |
| erwartet aus der Korrelation | −0,73 | −0,72 |
| CaDiCaL | −0,42 [−0,46, −0,37] | −0,45 [−0,50, −0,40] |
| Σ grad² +2,5 SD (bereinigt) | −0,48 | −0,56 |
| neutraler Arm | +0,04 (mit 0) | +0,01 (mit 0) |
Richtung und Existenz halten, unter zwei Lösern, repliziert. Die Grösse hält nicht: bei n = 130 liegt die vorab festgehaltene Erwartung ausserhalb des Intervalls — die Korrelation unterschätzt den kausalen Effekt. Beide Gradgrössen sind kausal. Keine wirkt über die kritische Menge: vermittelt werden 0–1 %.
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.0032Unter CaDiCaL war der Effekt halb so gross wie unter DPLL. Um herauszufinden, welcher Baustein eines Lösers reagiert, bekam der Haus-CDCL-Löser Schalter, die je einen Baustein herausnehmen, und lief auf denselben umverdrahteten Instanzen.
| unerfüllbar, n = 100, Anteil q am vollen Effekt | Gradkorrelation C | Gradstreuung Σ grad² |
|---|---|---|
| voll (VSIDS, 1UIP-Lernen, Neustarts, Phasenspeicher) | 1 | 1 |
| ohne 1UIP-Lernen (VSIDS weiter aus Konflikten gespeist) | 0,97 | 1,26 |
| statische Zufallsordnung statt VSIDS (lernt weiter) | 0,48 | 0,85 |
| statische Ordnung und kein Lernen | −0,07 | 0,12 |
Beide kausalen Grössen verschwinden im blinden, lernfreien Löser — relativ zu seinen Kosten, die 64-mal höher sind; absolut bleibt diese Zelle unentschieden. Die beiden unterscheiden sich im Weg: die Gradkorrelation hängt daran, wohin der Löser verzweigt, die Gradstreuung kaum — ihr genügt, dass der Löser aus Konflikten lernt.
Zwei naheliegende Lesarten wurden geprüft und verworfen. Eine feste absolute Ersparnis, die teure Löser nur verdünnen, ist ausgeschlossen: der volle Löser und der ohne Lernen unterscheiden sich vierfach in den Grundkosten und nicht im Effekt. Und dass der Effekt mit der Härte der Instanz wachse, ist ein Artefakt — ein neutraler Arm ohne Effekt erzeugt dieselbe Steigung, weil jede Umverdrahtung einer harten Instanz im Mittel eine weniger harte ist.
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 | Das ist enger, als es klingt. Die Schwellenachse ist nie ablatiert worden und steht auf Korrelation. Über Beweislängen, die keine Verzweigungsheuristik kennen, sagt nichts hiervon etwas. Der Beitrag ist ebenso methodisch wie inhaltlich: Eingriffe entlang einer Strukturgrösse bei festgehaltenen übrigen, ein neutraler Arm, Vorregistrierung, und ein Löser, Baustein für Baustein zerlegt.