The Judo Throw

The move is not new — and that is the good news

Reversal has won in several fields. Ramsey theory: “complete disorder is impossible”[1] — push a coloring toward randomness and structure emerges regardless. Szemerédi's regularity lemma: every graph decomposes into a bounded number of pieces that look random. Erdős's probabilistic method: construct objects by showing that a random one will do. Concentration of measure: in high dimension randomness turns rigid again.

But the case that matters here happened on exactly this subject. Mézard, Parisi and Zecchina did not search for structure in the formula — they asked what the disorder looks like[2]. Answer: the solution space shatters at α_d ≈ 3.86 into exponentially many clusters[3], long before the threshold at α_s ≈ 4.267[4]. This anti-structure was the structure, and Survey Propagation used it to solve random 3-SAT with a million variables near the threshold, when nothing else could.

So the judo throw is permitted — but it inherits a known half-blindness. That is no reason not to make it. It is the reason to give it a stopping criterion beforehand instead of a hope.

Why the disorder moves into the instrument, not the instance

All the examples above put the randomness in the instance. Here it moves into the measuring instrument instead — and the instrument was already standing ready: SAT in phase space measures exactly this flow, its fractal basin boundaries, and the relation α = κ/λ. There it was understood on one instance; here the question is whether it knows something about hardness across many instances. A process is run on the formula, and what is measured is how disorderly it behaves. That follows a pattern this project has already measured twice on its own:

The same thing happened twice in this repo: the blunt coordinate — the formula as its own location — died; the front of the current-counting, a process quantity, lives. These are not two independent findings but one pattern confirming itself.

The instrument panel

Six probes, sharing the decisive property: none of them calls a solver. That is a condition, not a coincidence — in the handbook, every good method separates SAT from UNSAT only because it asks satisfiability questions, and is thereby circular.

The interim finding: don't hold a parameter fixed

The first version of probe F set one variable and measured the avalanche of unit propagation. Result: always exactly 1, with no spread at all. That was not a bug in the code but a finding — at α = 4.267, random 3-SAT sits far below the percolation threshold of unit propagation. Starting from one variable, nothing runs.

Instead of holding the parameter fixed, it was swept. And then something appears:

How to keep the search from fooling itself

This is the actual substance of the run. Measure 76,501 candidates and report the best one, and you are reporting the maximum of a sample — and that is clearly nonzero even when every single candidate was pure noise.

Three barriers against confounders

What is measured is the partial rank correlation against log₂(conflicts), with {n, σ_deg², sat} regressed out. Degree spread carries 42 % of the hardness spread in this project; regressing out sat is the sharpest barrier, because that UNSAT is more expensive is already known — rediscovering only that is finding nothing.

The permutation null over the whole chain

The same search was run eight times, complete, on shuffled labels. The threshold for a finding is the maximum of those, not zero.

def korr(v, H, zr):
    """|Rank correlation| of v with the already residualized target zr."""
    r = B.rang(v)
    r = r - H @ r
    s = r.std()
    if s < 1e-12:
        return 0.0
    return abs(float(np.dot(r, zr) / (len(r) * s * zr.std())))


# ------------------------------------------------------------ Search space

def paare(Q, hoechstens=None, rng=None):
    ij = [(i, j) for i in range(Q) for j in range(i + 1, Q)]
    if hoechstens and len(ij) > hoechstens:
        rng = rng or np.random.default_rng(0)
        pick = rng.choice(len(ij), hoechstens, replace=False)
        ij = [ij[t] for t in pick]
    return ij


def verbinde(X, i, j, art):
    a, b = X[:, i], X[:, j]
    if art == "quot":
        n = np.abs(b)
        return a / np.where(n < 1e-9, 1e-9, np.where(b < 0, -n, n))
    if art == "prod":
        return a * b
    if art == "diff":                     # standardized difference
        za = (a - a.mean()) / (a.std() + 1e-12)
        zb = (b - b.mean()) / (b.std() + 1e-12)
        return za - zb
    raise ValueError(art)


ARTEN = ("quot", "prod", "diff")


def stufe1(X, H, zr, ij, arten=ARTEN, mitsingles=True):
    """Rank all candidates on `lern`. Returns list (score, description)."""
    aus = []
    if mitsingles:
        for i in range(X.shape[1]):
            aus.append((korr(X[:, i], H, zr), ("einzeln", i, -1)))
    for (i, j) in ij:
        for art in arten:
            aus.append((korr(verbinde(X, i, j, art), H, zr), (art, i, j)))
    return aus


def baue(X, bez):
    art, i, j = bez
    return X[:, i] if art == "einzeln" else verbinde(X, i, j, art)


# ------------------------------------------------------------------ Run

def sammle_bank(substrate):
    with Pool(min(22, os.cpu_count() or 4)) as p:
        reihen = p.map(BK.bank, substrate, chunksize=16)
    namen = sorted(set().union(*[set(r) for r in reihen]))
    X = np.array([[r.get(k, 0.0) for k in namen] for r in reihen], np.float64)
    X[~np.isfinite(X)] = 0.0
    return namen, X


def z(v):
    s = v.std()
    return (v - v.mean()) / s if s > 1e-12 else np.zeros_like(v)


def gierig(Xl, Hl, zrl, Xp, Hp, zrp, bezuege, tiefe=4):
    """Forward selection: standardized sums of several expressions.

    Rank correlation is blind to monotone transformations, so a single
    expression can no longer be improved -- gains only come from FURTHER
    terms. A term is taken only if it raises min(lern,pruef): a term that
    only helps on lern is overfitting and is not taken.
    """
    if not bezuege:
        return []
    vl = {b: z(baue(Xl, b)) for b in bezuege}
    vp = {b: z(baue(Xp, b)) for b in bezuege}
    start = bezuege[0]
    kette, sl, sp = [start], vl[start].copy(), vp[start].copy()
    bestwert = min(korr(sl, Hl, zrl), korr(sp, Hp, zrp))
    zeichen = [1.0]
    spur = [(bestwert, tuple(kette), tuple(zeichen))]
    for _ in range(tiefe - 1):
        bester, bwert, bvz = None, bestwert, 1.0
        for b in bezuege:
            if b in kette:
                continue
            for vz in (1.0, -1.0):
                w = min(korr(sl + vz * vl[b], Hl, zrl),
                        korr(sp + vz * vp[b], Hp, zrp))
                if w > bwert + 1e-4:
                    bester, bwert, bvz = b, w, vz
        if bester is None:
            break
        kette.append(bester)
        zeichen.append(bvz)
        sl += bvz * vl[bester]
        sp += bvz * vp[bester]
        bestwert = bwert
        spur.append((bestwert, tuple(kette), tuple(zeichen)))
    return spur

{
 "schwelle": 0.1301589930874898,
 "s1schwelle": 0.11654299343656545,
 "nullwerte": [
  0.07307985475037881,
  0.09803691914137302,
  0.12620280753198415,
  0.10369664996358074,
  0.1301589930874898,
  0.09224358597393721,
  0.09736080529329685,
  0.09094165030533212
 ],
 "kandidaten": 76501,
 "bank": 226
}

The strict test

The pooled value overestimates: n has four levels and sat two, and what rank-linear regression removes leaves a nonlinear dependency standing. So every candidate is additionally recomputed within each fixed (n, sat) cell, where neither one can reach through. Also reported is in how many of the eight cells the sign is the same — a real feature points the same direction everywhere, an artifact flips.

Checked that the apparatus works

On synthetic data with a planted signal, before the actual run:

The second row is the more important one: on pure noise the search reaches 0.126 — and the threshold catches it.

The finding

Thirty candidates lay above the threshold. The strict test leaves one of them standing as the best:

The product carries more than its parts. The entropy alone is worthless and flips sign in half the cells; the participation ratio alone sits at 0.192. The information does not sit in either coordinate but in their combination — exactly what a search over ratios and products is built for.

What turned out to be an artifact

The larger part of the thirty was confounder recombination, and the strict test found it:

More terms buy nothing real

The greedy stage combines several expressions into a signed sum. The result is the most instructive part of the run:

"""The strict (cell-wise) metric for every stage of the greedy combination,
persisted -- previously computed only in a throwaway script, never
saved anywhere. That contradicts the project's own rule: every measured
claim on the page must lead to a file that can be viewed and rechecked.

Reads sieb.json (field "gierig", the identifiers of the individual terms)
and the bank afresh, rebuilds every stage as a signed sum, and computes
at every stage the control from HANDBUCH.md/JUDO.md: partial rank
correlation *within* each fixed (n, sat) cell, averaged, with a count of
the cells that point in the same sign.
"""
import json, pickle, sys, os
import numpy as np
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import bewerten as B
import sieb as SB

HIER = os.path.dirname(os.path.abspath(__file__))
DATEN = os.path.join(HIER, "daten")


def streng(v, nn, sat, gv, y, mindest=60):
    ws, ns = [], []
    for x in sorted(set(nn)):
        for s_ in (0.0, 1.0):
            m = (nn == x) & (sat == s_)
            if m.sum() < mindest:
                continue
            ws.append(B.partiell(v[m], y[m], [gv[m]]))
            ns.append(int(m.sum()))
    if not ws:
        return 0.0, 0, 0
    ws, ns = np.array(ws), np.array(ns)
    mit = float(np.average(ws, weights=ns))
    return mit, int((np.sign(ws) == np.sign(mit)).sum()), len(ws)


import lauf as L

_TEIL_CACHE = {}
def _bauen(X, R, menge):
    if not _TEIL_CACHE:
        substrate = pickle.load(open(os.path.join(DATEN, "substrat.pkl"), "rb"))
        satz, subs, idx = L.teile(R, substrate)
        P = B.Pruefstand(satz)
        for k in ("lern", "pruef", "test"):
            Xk = X[idx[k]]
            H = SB.hut(P.stoer[k], len(Xk))
            zr0 = B.rang(P.ziel[k])
            _TEIL_CACHE[k] = (Xk, H, zr0 - H @ zr0)
    return _TEIL_CACHE[menge]


def lauf():
    d = np.load(os.path.join(DATEN, "bank.npz"), allow_pickle=True)
    X, namen = d["X"], list(d["namen"])
    ni = {n: i for i, n in enumerate(namen)}
    R = pickle.load(open(os.path.join(DATEN, "korpus.pkl"), "rb"))
    sb = json.load(open(os.path.join(DATEN, "sieb.json")))

    nn = np.array([r["n"] for r in R], float)
    sat = np.array([r["sat"] for r in R], float)
    gv = np.array([r["gradvar"] for r in R], float)
    y = np.log2(np.maximum([r["konflikte"] for r in R], 1)).astype(float)    # IMPORTANT: sieb.json stores "gierig" only with tiefe=4 and the pool of
    # the best 40 stage-2 candidates (internal call in sieb.py::eine_suche).
    # But the table on judo.html has 5 stages from a wider pool --
    # all 30 candidates from sb["ergebnis"] instead of just the best 40 from
    # stage 2 -- and tiefe=5. To reproduce the exact numbers shown, the same
    # (wider) pool and the same depth must be used here.
    bezuege = [(e["art"], ni[e["a"]], ni[e["b"]]) for e in sb["ergebnis"]]
    Xl_, Hl_, zrl_ = _bauen(X, R, "lern")
    Xp_, Hp_, zrp_ = _bauen(X, R, "pruef")
    Xt_, Ht_, zrt_ = _bauen(X, R, "test")
    spur = SB.gierig(Xl_, Hl_, zrl_, Xp_, Hp_, zrp_, bezuege, tiefe=5)

    aus = []
    for wert, kette, zeichen in spur:
        sl = sum(v * SB.z(SB.baue(Xl_, b)) for v, b in zip(zeichen, kette))
        sp = sum(v * SB.z(SB.baue(Xp_, b)) for v, b in zip(zeichen, kette))
        st = sum(v * SB.z(SB.baue(Xt_, b)) for v, b in zip(zeichen, kette))
        rl, rp, rt = SB.korr(sl, Hl_, zrl_), SB.korr(sp, Hp_, zrp_), SB.korr(st, Ht_, zrt_)
        ganz = sum(v * SB.z(SB.baue(X, b)) for v, b in zip(zeichen, kette))
        sg, gl, zz = streng(ganz, nn, sat, gv, y)
        txt = " ".join(("+" if v > 0 else "-") +
                       (namen[i] if a == "einzeln" else f"({namen[i]} {a} {namen[j]})")
                       for v, (a, i, j) in zip(zeichen, kette))
        aus.append({"terme": len(kette), "lern": rl, "pruef": rp, "test": rt,
                    "streng": sg, "zellen_gleich": gl, "zellen": zz, "ausdruck": txt})    print(f"  {len(kette)} terms: lern {rl:.3f} pruef {rp:.3f} test {rt:.3f}  "
              f"streng {sg:+.3f} {gl}/{zz}")

    with open(os.path.join(DATEN, "streng_je_term.json"), "w") as f:
        json.dump(aus, f, indent=1)    print(f"\\nsaved -> {os.path.join(DATEN, 'streng_je_term.json')}")


if __name__ == "__main__":
    lauf()

[
 {
  "terme": 1,
  "lern": 0.3121949716325861,
  "pruef": 0.30971683757420543,
  "test": 0.3324133787235236,
  "streng": 0.25930672858491144,
  "zellen_gleich": 8,
  "zellen": 8,
  "ausdruck": "+(cSchuld.entropie prod cTeil.teilnahme)"
 },
 {
  "terme": 2,
  "lern": 0.3446945783258858,
  "pruef": 0.3547529368331009,
  "test": 0.3919760659956465,
  "streng": 0.24807174490592482,
  "zellen_gleich": 7,
  "zellen": 8,
  "ausdruck": "+(cSchuld.entropie prod cTeil.teilnahme) -(cBogen.median diff cSchuldStreu.median)"
 },
 {
  "terme": 3,
  "lern": 0.35832565991185183,
  "pruef": 0.37746030194027413,
  "test": 0.38782528426719703,
  "streng": 0.26004803841288204,
  "zellen_gleich": 7,
  "zellen": 8,
  "ausdruck": "+(cSchuld.entropie prod cTeil.teilnahme) -(cBogen.median diff cSchuldStreu.median) -(cTeil.streu diff sL.teilnahme)"
 },
 {
  "terme": 4,
  "lern": 0.3776439765673545,
  "pruef": 0.389714897199669,
  "test": 0.407362902209816,
  "streng": 0.23569579486940836,
  "zellen_gleich": 6,
  "zellen": 8,
  "ausdruck": "+(cSchuld.entropie prod cTeil.teilnahme) -(cBogen.median diff cSchuldStreu.median) -(cTeil.streu diff sL.teilnahme) +(cK.teilnahme quot kUeberhang)"
 },
 {
  "terme": 5,
  "lern": 0.3794966148490839,
  "pruef": 0.39318464523725827,
  "test": 0.404828812015732,
  "streng": 0.24841559524734894,
  "zellen_gleich": 6,
  "zellen": 8,
  "ausdruck": "+(cSchuld.entropie prod cTeil.teilnahme) -(cBogen.median diff cSchuldStreu.median) -(cTeil.streu diff sL.teilnahme) +(cK.teilnahme quot kUeberhang) -(cSchuld.streu quot cSpurEnde.teilnahme)"
 }
]

Anyone who had optimized for the pooled number here would have reported a four-term expression at 0.41 that knows less than the one-term expression at 0.33. Pooled and strict measures diverge under greedy search, and only the strict one is reliable.

The injection on the iGPU

The original plan was to run a local language model as a mutation operator. Measured: the Radeon 890M has 512 MiB of its own memory, everything beyond that runs over GTT and thus over the same DDR5 bus as the CPU. No bandwidth advantage, 12 to 15 characters per second — independent of model size, a 4B model was as slow as a 35B one.

So it was rebuilt: the breadth comes from the sieve (all pairs, exhaustively), the model gets the part that suits it — one line per suggestion instead of a code block, and only combinations of three or more names, whose space is too large to enumerate. In three hours: 3,551 candidates, 3,514 of them after deduplication.

The injection's own permutation null — the same 3,514 expressions against a label shuffled within the cells — sits at 0.067, with zero false hits across four runs. The strict statistic with cell consistency is a markedly sharper instrument than the pooled one.

Putting it in context, without rounding up

The fresh test

One question remained open, and it was the most uncomfortable one. The injection was steered over 497 rounds by a leaderboard ranked by exactly the quantity it is ultimately evaluated on — and that quantity ran over all instances. So there was no held-out set that would have broken the feedback loop.

The permutation test does not answer this. It shuffles the label and recomputes a fixed set of candidates; it thereby prices “is the value of this expression real”, not “did the steering drive it up”. The latter can only be answered with instances that did not exist during the search.

So: 900 fresh instances, different seeds, the same substrate, the same expressions — and no more tuning. Three sizes n instead of four, hence six cells instead of eight.

Three things are established by this.

Notable in passing: cSchuldStreu.schiefe, the building block present in eight of the ten best injection expressions, is alone weak and inconsistent (−0.123 at 4/6). The same pattern as with the sieve — the information sits in the combination, not the building block.

The final result

"""The final test: a corpus that nothing has ever seen.

WHY IT IS NEEDED. The injection was steered over 497 rounds by a
leaderboard ranked by exactly the quantity it is ultimately evaluated
on -- and that quantity ran over ALL instances. So there was no held-out
set that would have broken the feedback loop.

The permutation test does not answer this. It shuffles the label and
recomputes a FIXED set of candidates; it thereby prices "is the value of
this expression real", not "did the steering drive it up". The latter can
only be answered with instances that did not exist during the search.

So: fresh instances, a different seed, the same substrate, the same
expressions -- and no more tuning.
"""
import glob, json, os, pickle, sys, time
from multiprocessing import Pool
import numpy as np
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import bank as BK, bewerten as B, einspritzung as E, substrat as S

HIER = os.path.dirname(os.path.abspath(__file__))

def eine(a):
    i, r = a
    return i, BK.bank(S.alles(r["klauseln"], r["n"], saat=7000 + i))

def lauf():
    R = []
    for f in sorted(glob.glob(os.path.join(HIER, "frisch", "korpus_n*.jsonl"))):
        for z in open(f):
            z = z.strip()
            if z:
                try: R.append(json.loads(z))
                except json.JSONDecodeError: pass
    for r in R:
        c = np.zeros(r["n"], np.int64)
        for k in r["klauseln"]:
            for l in k: c[abs(l) - 1] += 1
        r["gradvar"] = float(c.var())
    print(f"# {len(R)} frische Instanzen, SAT-Anteil {np.mean([r['sat'] for r in R]):.3f}",
          flush=True)

    t0 = time.time()
    aus = [None] * len(R)
    with Pool(min(22, os.cpu_count() or 4)) as p:
        for i, b in p.imap_unordered(eine, list(enumerate(R)), chunksize=4):
            aus[i] = b
    print(f"# Substrat+Bank in {(time.time()-t0)/60:.1f} min", flush=True)

    alt = np.load(os.path.join(HIER, "daten", "bank.npz"), allow_pickle=True)
    namen = list(alt["namen"])
    X = np.array([[b.get(k, 0.0) for k in namen] for b in aus], np.float64)
    X[~np.isfinite(X)] = 0.0
    ni = {n: i for i, n in enumerate(namen)}

    nn = np.array([r["n"] for r in R], float)
    sat = np.array([r["sat"] for r in R], float)
    gv = np.array([r["gradvar"] for r in R], float)
    y = np.log2(np.maximum([r["konflikte"] for r in R], 1)).astype(float)
    zellen = [m for m in ((nn == x) & (sat == s)
                          for x in sorted(set(nn)) for s in (0.0, 1.0))
              if m.sum() >= 40]
    gr = np.array([m.sum() for m in zellen], float)

    def streng(v):
        w = np.array([B.partiell(v[m], y[m], [gv[m]]) for m in zellen])
        mit = float((w * gr).sum() / gr.sum())
        return mit, int((np.sign(w) == np.sign(mit)).sum()), len(w)

    KAND = [
      ("Sieb, bester Paarausdruck",
       "cSchuld.entropie * cTeil.teilnahme", 0.259),
      ("Einspritzung, bester",
       "cSchuldStreu.schiefe * wE.rate_frueh * sLAbst.median / cTeil.streu", 0.283),
      ("Einspritzung, zweitbester",
       "cSchuldStreu.schiefe * wE.rate_frueh / cTeil.streu", 0.273),
      ("Einspritzung, dritter",
       "cSchuldStreu.schiefe * wE.rate_frueh * sLAbst.median / cTeil.vk", 0.272),
      ("nur der Hauptbaustein", "cSchuldStreu.schiefe", None),
      ("nur cTeil.teilnahme", "cTeil.teilnahme", 0.192),
      ("Artefakt zur Kontrolle (n-Stellvertreter)", "kGeruest", 0.013),
      ("Artefakt zur Kontrolle (sat-Stellvertreter)", "cSaettigung", -0.040),
    ]
    print(f"\n  {'':44s} {'frisch':>8s} {'Zellen':>7s}   {'alt':>7s}")
    for nam, ausdr, alt_ in KAND:
        try:
            v = E.werte_aus(ausdr, X, ni)
        except Exception as ex:
            print(f"  {nam:44s}  -- {ex}"); continue
        m, g, z = streng(v)
        av = f"{alt_:+.3f}" if alt_ is not None else "   -  "
        print(f"  {nam:44s} {m:+8.3f}  {g}/{z:<4d}  {av}")
    print(f"\n  (Zellen = wieviele der {len(zellen)} (n,sat)-Zellen dasselbe "
          f"Vorzeichen zeigen)")

if __name__ == "__main__":
    lauf()

# 900 frische Instanzen, SAT-Anteil 0.509
# Substrat+Bank in 14.9 min

                                                 frisch  Zellen       alt
  Sieb, bester Paarausdruck                      +0.266  6/6     +0.259
  Einspritzung, bester                           +0.238  6/6     +0.283
  Einspritzung, zweitbester                      +0.222  6/6     +0.273
  Einspritzung, dritter                          +0.225  6/6     +0.272
  nur der Hauptbaustein                          -0.123  4/6        -  
  nur cTeil.teilnahme                            +0.211  6/6     +0.192
  Artefakt zur Kontrolle (n-Stellvertreter)      +0.009  3/6     +0.013
  Artefakt zur Kontrolle (sat-Stellvertreter)    -0.037  3/6     -0.040

  (Zellen = wieviele der 6 (n,sat)-Zellen dasselbe Vorzeichen zeigen)

Sources

1. The phrase “complete disorder is impossible” traces back to Theodore S. Motzkin and is cited as a maxim of Ramsey theory, among others in Graham, Rothschild & Spencer, Ramsey Theory, Wiley, 2nd ed. 1990. Biography (MacTutor)
2. M. Mézard, G. Parisi, R. Zecchina: Analytic and Algorithmic Solution of Random Satisfiability Problems. Science 297, 812–815 (2002). doi:10.1126/science.1073287 · companion paper with the algorithm: M. Mézard, R. Zecchina, The random K-satisfiability problem: from an analytic solution to an efficient algorithm, Phys. Rev. E 66, 056126 (2002), arXiv:cond-mat/0207194
3. F. Krzakała, A. Montanari, F. Ricci-Tersenghi, G. Semerjian, L. Zdeborová: Gibbs states and the set of solutions of random constraint satisfaction problems. PNAS 104, 10318–10323 (2007). doi:10.1073/pnas.0703685104 · arXiv:cond-mat/0612365
4. S. Mertens, M. Mézard, R. Zecchina: Threshold values of random K-SAT from the cavity method. Random Structures & Algorithms 28, 340–373 (2006). arXiv:cs/0309020
5. M. Ercsey-Ravasz, Z. Toroczkai: Optimization hardness as transient chaos in an analog approach to constraint satisfaction. Nature Physics 7, 966–970 (2011). doi:10.1038/nphys2105
6. V. Oganesyan, D. A. Huse: Localization of interacting fermions at high temperature. Phys. Rev. B 75, 155111 (2007) — introduces the spacing ratio. doi:10.1103/PhysRevB.75.155111 · arXiv:cond-mat/0610854
7. Y. Y. Atas, E. Bogomolny, O. Giraud, G. Roux: Distribution of the Ratio of Consecutive Level Spacings in Random Matrix Ensembles. Phys. Rev. Lett. 110, 084101 (2013) — hence the values 0.3863 (Poisson) and 0.5307 (GOE). doi:10.1103/PhysRevLett.110.084101 · arXiv:1212.5611

The measurements on this page come from judo/ in the project archive: substrat.py (probes), bank.py (feature bank), sieb.py (search and permutation null), bewerten.py (confounders), frischprobe.py (the fresh instances). The full text is included as JUDO.md.