Module lyapunov 

Lyapunov-function synthesis — don’t search for the proof, discover the measure that collapses the problem, and let the proof fall out as a corollary.

This is the thesis of the whole certified-symmetry campaign made into one procedure. A symmetry-breaking refutation is a Lyapunov function for the search dynamics: a scalar potential (“active items remaining”) that strictly descends to the goal. Once you have that potential, the refutation, its correctness, and its O(n²) complexity certificate are all just readings of it (crate::complexity). So the engine here inverts the usual game:

1. Synthesize — search a bounded, polynomial class of candidate potentials. The class is “covering layouts”: a factorization of the variables into items × bins under which swapping two items is a symmetry of the formula. Testing a candidate is cheap (one automorphism check), so the whole search is polynomial — categorically unlike the exponential graph-automorphism detection it replaces.
2. Collapse — if a potential is found, drive the steered Heule descent with the discovered item-swap symmetry (covering_collapse); every step is PR-self-checked, fail-closed.
3. Fall out — the result is a RankedRefutation that certifies both correctness and its own polynomial size.

When no potential in the class works, the answer is an honest, bounded impossibility: “this formula has no covering-symmetry collapse” — None, never a wrong answer.

Structs

CardinalitySeams

The cardinality / parity symmetry seams. Each recovered cardinality group is fully symmetric — its members are interchangeable (S_m preserves “at most k of them true”). In a COUPLED instance only some of those swaps survive as MODEL-SET symmetries; the parity coupling blocks the rest. This partitions the candidate interchangeable pairs into joint (a transposition that preserves the model set — a free symmetry to break) and seams (a transposition the parity genuinely tears). The check is SEMANTIC (parity SPAN + non-parity clauses via [SemanticSymmetry]), so it recognizes the affine parity symmetry a clause-automorphism test misses. The joint swaps generate the model-preserving symmetry at the seam.

CollapsingMeasure

A discovered collapsing potential: the formula’s variables read as an items × bins grid (var(i, b) = i*bins + b) under which item-permutations are symmetries — so the formula is a covering / pigeonhole problem and items > bins makes it unsatisfiable.

CoveringMeasure

A covering Lyapunov measure: items into bins (var(i,b) = i*bins + b) with item-swap witnesses. ONE measure type that instantiates the theorem for every covering family — PHP (items = n, bins = n-1), clique-coloring (items = n, bins = k), and any other generalized pigeonhole. The “lift”: the family is data, the measure is uniform.

LyapunovCertificate

A machine-checked certificate that a refutation’s trajectory carries a valid Lyapunov function, with the four dynamical-systems axioms verified explicitly and the resulting complexity bound.

PartialCoveringMeasure

A covering measure restricted to the absolute rounds [lo, hi] — it breaks only those covering levels, leaving a residual for a later stage. The tool that makes COMPOSITION non-trivial: a stage that genuinely hands a smaller problem to the next.

SymmetryTheory

A live symmetry theory for crate::cdcl::Solver::solve_with — DYNAMIC lex-leader propagation over the whole symmetry group. Each element is an AFFINE map α (a model-set automorphism) given as a per-output spec α(x)[i] = ⊕_{s∈xset_i} x_s ⊕ b_i; permutations are the special case where every xset is a single variable. During search it enforces x ≤_lex α(x): walking positions while the prefix stays equal, computing α(x)[i] from the trail (an XOR of the support), then at the frontier forcing x_i = 0 when α(x)[i] = 0, forcing the last free support bit to make α(x)[i] = 1 when x_i = 1, or conflicting — AUX-FREE, on the shared trail, fused alongside the parity and cardinality theories. Sound: the orbit’s global lex-minimum satisfies x ≤_lex α(x) for EVERY α, so the whole group’s predicate keeps exactly one representative per orbit (equisatisfiable), and every reason clause (prefix + support witnesses) is implied by it.

Enums

AutoCollapse

The result of the unified engine: which physics collapsed the formula, with its checkable artifact.

Constants

MAX_RECOVERED_CARDINALITY

The widest core a fused solve recovers automatically: at-most-k groups up to this k. Beyond it, call recover_at_most_k directly — but the C(group, k) scan cost (budget-bounded) and the diminishing yield of ever-wider exclusion cliques make 4 (5-ary clauses) the default ceiling.

Traits

LyapunovMeasure

The hypothesis of the ⟸ theorem: a Lyapunov measure that generates certified descent steps for a formula, independent of any particular family.

Functions

affine_parity_symmetries

Detect affine (shear) symmetries of a fused instance that preserve the model set — the affine parity symmetries a variable-permutation break structurally cannot express (an image bit becomes an XOR of two variables). For a variable i that appears in NO non-parity (cardinality / residual) clause and any j ≠ i, the shear x_i ↦ x_i ⊕ x_j moves only position i, so it leaves the cardinality/residual intact; it is a model-set symmetry iff it maps the parity SOLUTION SPACE to itself (checked on the space’s affine spanning set — particular ⊕ each kernel basis vector). Each valid shear is returned as an SBP affine-map spec (identity except output i = ⊕{i,j}) for crate::sym_break::affine_lex_leader_sbp. Gated to num_vars ≤ 64.

all_transposition_symmetries

Every single-transposition model-set symmetry — every variable swap that preserves the model set ([SemanticSymmetry]): parity-variable permutations, cardinality permutations, and residual-clause permutations alike. Broadens the wreath-tower (cardinality-only) symmetry to the FULL permutation symmetry of the whole instance — in particular the permutations of parity-only variables neither the cardinality detector nor the affine shear detector finds. Budget-bounded (n ≤ 64, C(n,2) checks).

auto_collapse

The unified, structure-recognizing engine. Given only opaque clauses, decide WHICH collapse physics applies — covering symmetry or parity — and produce the corresponding Lyapunov-certified artifact. One engine; the structure selects the mechanism. Sound and fail-closed on both paths.

cardinality_collapse

cardinality_parity_seams

Compute the CardinalitySeams of a fused instance: for every pair of variables interchangeable in some recovered cardinality group, test whether swapping them is a model-set symmetry ([SemanticSymmetry]) — joint if so, a seam if not. Pair-budget-bounded (a partial joint set still yields sound symmetry breaks).

cardinality_symmetry_break

Break the joint cardinality/parity symmetry: union the joint swaps into interchangeable components (a component is fully symmetric — the group generated by its transpositions is S, every element an automorphism), then order each component’s variables into a descending chain with vᵢ ≥ vᵢ₊₁ clauses (vᵢ ∨ ¬vᵢ₊₁). A lex-leader: equisatisfiable (every orbit keeps its ordered representative), so it shrinks the fused search without changing the verdict. Returns the extra clauses (empty if no joint symmetry).

cardinality_symmetry_generators

The generators of the joint parity/cardinality symmetry, UP THE WREATH CHAIN. Two levels:

compose_collapses

Compose collapses — the Poly wiring diagram on certified descents. Each stage’s descent runs on the residual database of the previous; the potentials are banded (earlier stages occupy the higher rank band) so the composite strictly descends across every stage boundary; the whole closes by resolution. The result is ONE refutation carrying ONE combined Lyapunov certificate — two (or more) collapses wired into a single descent. Fail-closed: each step is PR-self-checked.

covering_collapse

Drive the steered Heule descent over a discovered items × bins covering layout: bins + 1 items are a tight pigeonhole, so force them out of the bins one at a time, each ¬var(i, bin) certified by “swap item i with the last active item.” Returns the ranked refutation; every step is PR-self-checked, so a layout that is not really a covering problem simply fails to refute.

cutting_planes_lyapunov

The Lyapunov function for the cardinality / cutting-planes collapse — the THIRD physics. The Cook–Coullard–Turán refutation of PHP sums 2n-1 pseudo-Boolean constraints; each addition cancels a literal against its negation and tightens the accumulated constraint toward the infeasible 0 ≥ 1. The potential is the number of constraints still to combine, descending to 0 exactly as the contradiction is exposed.

extract_xor

Recover the XOR (parity) constraints latent in a CNF: a constraint x₁⊕…⊕x_k = b is encoded by exactly the 2^(k-1) clauses over {x₁,…,x_k} whose negated-literal count has one fixed parity. We group clauses by their variable set and emit an XorEquation for each group that is exactly such a gadget. Sound: every emitted equation is logically equivalent to a clause group present in the formula, so a refutation of the extracted (sub)system implies the formula is UNSAT.

fused_parity_cardinality_decide

The fused parity + cardinality decision. When a formula carries BOTH a GF(2) linear substructure (recovered XOR equations via extract_xor) AND an at-most-one cardinality substructure (via recover_at_most_one), decide it with the two live theories reasoning TOGETHER on one trail — Gaussian elimination for the parity, cardinality propagation for the counting — the structural attack on minimal-disagreement parity that neither alone cracks. Returns Some(is_sat), or None when either substructure is absent (so a caller falls through to other routes). Sound: the original clauses are solved (Boolean-complete), the theories return only formula-entailed clauses, and a SAT model is re-checked against the clauses (fail-closed). Uses the stateless crate::xor_engine::XorEngine (not IncXor, whose value-blind trail-sync is unsafe without a backing clausal XOR encoding).

fused_permutation_generators

The permutation generators for the DYNAMIC symmetry theory: the wreath-tower cardinality permutations plus every transposition symmetry of the whole instance.

fused_symmetry_group

gaussian_lyapunov

The Lyapunov function for the algebraic collapse — Gaussian elimination over GF(2). The potential is the number of pivots still to be found in the unsolved linear system; each elimination step strictly reduces it, and the trajectory reaches the goal exactly when an inconsistent row 0 = 1 is exposed. Returns the descending potential and whether the goal (contradiction) was reached.

lyapunov_of_symmetry

Extract and verify the Lyapunov certificate of a symmetry refutation: its rank annotation is the potential (“active items remaining”), and the refutation closing is the goal-reaching axiom.

proof_from_measure

The constructive proof of the ⟸ theorem. Drive the measure’s descent from L down to 0, self-checking every step (fail-closed), then close with unit propagation. Returns a ranked refutation whose descent has ≤ L·w steps — read its certificate with crate::complexity::RankedRefutation::certify.

proof_induced_measure

The ⟹ direction of the characterization: any checkable refutation of n_steps steps induces a Lyapunov measure — rank the steps in descending order. The induced trajectory is a valid Lyapunov function of size n_steps, so the minimum measure cost μ*(F) ≤ (min proof size).

recover_at_most_k

Recover the at-most-k cardinality substructure over arbitrary LITERALS — the generalisation of recover_at_most_one to WIDER and MIXED-POLARITY counting cores (the ternary at-most-two cores of parity-learning instances, and — via negation — at-least-k). Work in literal codes (2·var + sign, negation flips the low bit). A width-(k+1) clause ℓ₀ ∨ … ∨ ℓ_k is violated only when all of {¬ℓ₀,…,¬ℓ_k} are true, so it FORBIDS that literal set; a set S of literals (distinct variables) is an at-most-k group iff EVERY (k+1)-subset of S is some clause’s forbidden set. Greedy maximal extension from each forbidden seed — a literal joins S only when every k-subset of S together with it is forbidden, so the invariant keeps every (k+1)-subset forbidden and at_most(S, k) genuinely implied by clauses present (sound to fuse). A clause [¬a,¬b,¬c] ⇒ at-most-2 of {a,b,c}; the three clauses [a,b],[a,c],[b,c] ⇒ at-most-1 of {¬a,¬b,¬c} = at-least-2 of {a,b,c}. k = 1 over all-negative binary clauses reproduces recover_at_most_one.

recover_at_most_one

Recover the at-most-one cardinality substructure from arbitrary clauses — the substructure twin of [discover_covering], which requires the WHOLE formula to be a covering (so a single XOR gadget makes it decline). Binary all-negative clauses ¬a ∨ ¬b are at-most-one edges; this returns an at_most(group, 1) PB constraint per maximal exclusion clique of size ≥ 2, IGNORING every other clause. Each emitted group is a verified FULL clique (every pair has its exclusion clause present), so its ≤ 1 is implied by clauses in the formula — sound to feed a solver alongside a recovered parity system (the par32 fusion).

recover_cardinality_constraints

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.

recover_cardinality_substructure

Recover the cardinality substructure a fused solve consumes: every at-most-k group over arbitrary literals, k = 1 … MAX_RECOVERED_CARDINALITY — pairwise, ternary, quaternary, … exclusion cliques of any polarity, so at-most-k, at-least-k (the negated cliques), and mixed counting cores all flow into the fused theory. Each recover_at_most_k returns immediately when the formula has no width-(k+1) clause of the right shape, so widening is free on instances that lack those cores.

solve_by_measure_synthesis

The whole inversion: discover the Lyapunov function, then let the proof fall out. Search the covering-layout class; for each candidate whose item-swap is a symmetry, run the steered collapse; return the first that yields a checking refutation, paired with the measure that drove it. None is a bounded impossibility — no covering-symmetry collapse exists for this formula.

synthesize_measure

Search the bounded class of covering layouts for one whose item-swap is a genuine symmetry — a cheap pre-filter (one automorphism check per candidate factorization). Returns the first such measure in the items > bins (unsatisfiable) direction, or None.

verify_lyapunov

Verify the four Lyapunov axioms over a potential trajectory and return the certificate, or None if any axiom fails. (1) bounded below — u64 is ≥ 0 by type; (2) monotone non-increasing; (3) strict descent across the level set; (4) reaches the minimum at the goal. A trajectory that stalls (a level recurs) or never closes is not a Lyapunov function and certifies nothing.