Function recover_cardinality_constraints 

pub fn recover_cardinality_constraints(
    num_vars: usize,
    formula: &[Vec<Lit>],
) -> Option<Vec<PbConstraint>>

The third physics, made automatic: cardinality / cutting-planes collapse of a discovered covering. When the formula is a bipartite covering with more items than bins, summing the “item ≥ 1” rows against the “bin ≤ 1” columns telescopes to 0 ≥ (items − bins) > 0 — the Cook–Coullard–Turán refutation, in the cutting-planes proof system. Sound: every summed constraint is implied by clauses present in the formula (full-clique-checked), so a contradiction proves UNSAT. Returns (trajectory, reached_goal, constraints) — the GF(2)-analogue Lyapunov descent (constraints remaining to combine). Crucially this needs no symmetry, so it collapses asymmetric coverings the geometric route cannot. Recover the cardinality structure of an opaque CNF as PB constraints — a ≥ 1 clause per at-least-one row and a ≤ 1 per at-most-one clique (the cardinality the pairwise encoding loses). The clause-level recognizer (the extract_xor analogue for counting) that feeds BOTH the static cardinality_collapse cut and the live crate::pseudo_boolean::CardinalityTheory. None when the formula is not a clean covering, so callers fall through. Each returned constraint is implied by clauses present in the formula (the columns are full-clique-checked by [discover_covering]), so feeding them to a solver is sound.