Function decide_laddered 

pub fn decide_laddered(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> (bool, LadderStats)

Ladder up the hypercube: crush what we can, brute-force the rest. Branch-and-cut over {0,1}ⁿ, one variable at a time — exactly DPLL with our certified cuts as the theory:

1. base — a residual empty clause means this subcube is fully covered (UNSAT branch); no residual clauses means a corner escapes here (SAT).
2. unit propagation — a residual unit clause forces its variable (free dimension reduction).
3. cut — try the certified shadows (counting / parity / cutting-planes) on the residual; if one fires, the whole subcube is crushed without descending — the learned invariant doing its work.
4. branch — otherwise split on a residual variable and ladder down.

Structured families (pigeonhole, Tseitin, clique) are crushed by a cut at or near the root in a handful of nodes at any n, because the cut is scale-free; the genuinely unstructured residual is brute-forced by the branching. Works on raw clauses, so it ladders past the cube’s 63-variable geometric ceiling.