Module cofactor 

The cofactor-DAG lens: symmetry above the instance.

§4 of work/PAPER.md measures symmetry in the instance — automorphisms of the cover (Bₙ, AGL, shears). The residue (census::residue_map) is rigid to all of them; that rigidity is the wall. This module lifts the lens one level up, onto the formula’s Shannon cofactor DAG: the DAG whose nodes are the distinct residual sub-formulas F|ρ under partial assignments ρ, with edges the Shannon expansion F = x·F|_{x=1} + x̄·F|_{x=0}.

A hard core has exponentially many distinct cofactors — that is exactly what “no small variable-order decision DAG / exponential resolution width” means, and it is the finite, per-n incompressibility pole (crate::ait::incompressible_string_exists) one level up. The hypothesis this module makes executable: those exponentially-many cofactors may fall into polynomially many equivalence classes under a congruence ~ that is not induced by any automorphism of the instance. Quotient the DAG by ~ and the exponential object becomes a polynomial one; when the certificate is ~-invariant the quotient DAG is the refutation, with class-sharing playing the role of extension variables (the Resolution → ER/SR jump).

The collapse measure, and the certificate — kept deliberately separate:

• distinct_width / cofactor_set — the strict distinct-cofactor set under the fixed order 0..n (the OBDD width): the honest exponential floor for the residue.
• quotient_class_count — the number of ~-classes among that same fixed set. Because it only quotients a fixed set, quotient_class_count(Raw) = distinct_width and coarser congruences give monotonically fewer classes: iso ≤ rename ≤ raw = distinct are theorems (not artifacts of a branching order), so they hold on every formula, the residue included. This is the clean measure of “do exponentially-many cofactors fall into polynomially-many classes?”
• quotient_dag — the certificate realization: the cofactor DAG quotiented by ~, every edge carrying the explicit Twist (literal renaming) verified locally by check_quotient_dag (zero trust). It is a sound, poly-time-checkable refutation; its node count is a certificate size, reported but never conflated with the collapse measure (the two constructions are size-incomparable — renaming can re-order the branch variable).

The congruence ladder, finest → coarsest: Raw (strict equality) ⊂ Rename (first-appearance renaming) ⊂ GroupInduced (an instance symmetry group’s orbits — Bₙ, AGL) ⊂ CofactorIso (full CNF-isomorphism: any variable relabeling and polarity flip, not tied to an instance automorphism — the strongest decidable rung, the one that sees symmetry above the instance). Whether a poly-index congruence exists for the residue past this rung — an SR-definable one — is 3-SAT ∈ coNP.

Structs

CofactorIso

Merge cofactors that are CNF-isomorphic (any relabeling + polarity flip) — the strongest decidable rung, the symmetry that need not live in the instance. cap bounds the brute force.

GroupInduced

Merge cofactors lying in the same orbit under an instance-symmetry group (Bₙ, AGL, …).

QuotientDag

The cofactor DAG quotiented by a Congruence: root node index, nodes (one per class), and visits (the memoized recursion’s work — output-sensitive: linear in the collapse found).

Raw

Strict equality — no canonicalization at all (the identity twist). The finest rung: it merges nothing, so quotient_class_count(Raw) == distinct_width exactly.

ReduceIso

Apply the full sound reduction (reduce: unit-prop + pure-literal + subsumption to fixpoint), then canonicalize up to CNF-isomorphism — one rung coarser than UnitPropIso. A collapse-measure congruence (the reduction is structural, RUP/reduction-certified, not a relabeling), for quotient_class_count. The ladder: reduce-iso ≤ unitprop-iso ≤ iso ≤ rename ≤ raw = distinct.

Rename

First-appearance renaming (trivial group). One rung coarser than Raw: it merges cofactors that coincide after relabeling variables by order of first appearance.

StructuredDag

The cofactor DAG cut off at structured leaves: the whole dispatcher, organized as a decision DAG. Its size is the number of cofactors that must be branched before a specialist (or ⊥) fires — 1 exactly when the root itself is crushed, growing only where no specialist ever fires (the wall). Reported structured/trivial leaf counts show which crushers carried the refutation.

StructuredReduceIso

The reduction rung fused with the non-resolution crushers as terminals: reduce to fixpoint, then if a non-resolution specialist (parity/GF(2), mod-p, exact-cover, algebraic collapse) refutes the reduced cofactor, collapse it to one “crushed” class; otherwise canonicalize up to iso. Coarser than ReduceIso (all non-resolution-crushable reduced cofactors merge into one), so struct-reduce-iso ≤ reduce-iso. This is the rung that can beat the Chvátal–Szemerédi resolution cap — GF(2)/mod-p are polynomial exactly where resolution is exponential — measured via quotient_class_count (specialist verdicts certified by their routes; reduce by RUP).

UnitPropIso

Unit-propagate to fixpoint, then canonicalize up to CNF-isomorphism — strictly coarser than CofactorIso (cofactors that reduce to isomorphic residuals after propagation merge, and all unit-refutable cofactors collapse into one). A collapse-measure congruence only: unit propagation is a structural reduction, not a relabeling, so the returned twist is the iso-twist of the reduced form — valid for quotient_class_count (which uses only the canonical key), not for the twist-certificate quotient_dag (a propagation merge is certified by RUP instead).

Enums

Node

A node of the strict distinct-cofactor DAG.

QNode

A node of the quotient DAG. Edges carry the Twist that maps the recomputed cofactor onto the stored child representative.

SNode

A node of the structured-leaf cofactor DAG.

Traits

Congruence

An equivalence relation on cofactors, given by a canonical representative of each class plus the Twist realizing the merge. To be a sound certificate substrate it must be a congruence: its twists are literal renamings (bijection + polarity flips), which preserve (un)satisfiability, so isomorphism-invariance of UNSAT makes the local check sound. Two cofactors are ~-equivalent iff canonicalize returns the same representative.

Functions

apply_twist

Apply a Twist to a clause set; None if a live variable is unmapped.

canon

Canonicalize a CNF given as packed Lits.

canon_raw

Canonicalize a CNF given in raw (var, polarity) form.

check_distinct_dag

Zero-trust local checker for the strict DAG: leaves carry ⊥; every internal node’s two children are exactly its recomputed cofactors. A pass certifies the root UNSAT by structural induction, in time linear in the DAG.

check_quotient_dag

Zero-trust checker with twist verification: leaves carry ⊥; each internal node’s recomputed cofactor, pushed through the stored twist, must equal the child EXACTLY. A pass certifies the root UNSAT by structural induction (unsatisfiability is isomorphism-invariant and each twist is a literal renaming), in time linear in the quotient DAG.

check_structured_dag

The checker: ⊥ leaves carry the empty clause; structured leaves re-fire their specialist (the dispatcher’s route re-checks internally — an idempotent re-verification); internal nodes’ children are exactly their recomputed Shannon cofactors. The internal skeleton is fully zero-trust; the structured leaves are dispatcher-certified (extracting each route’s own witness for end-to-end zero trust is the next hardening).

cofactor

The Shannon cofactor F|_{x=b}: drop clauses satisfied by x=b, delete the x literal from the rest, recanonicalize. An empty clause survives as ⊥ (the branch is UNSAT on the spot).

cofactor_set

The strict distinct-cofactor set: every (depth, cofactor) pair reachable by prefix-restricting the fixed order 0..n. Its cardinality is distinct_width; quotienting it by a congruence can only merge pairs, so every quotient_class_count is ≤ distinct_width and coarser congruences give monotonically fewer classes — both are theorems about quotients of this one fixed set, and therefore hold on every formula.

distinct_cofactor_dag

Build the memoized strict distinct-cofactor DAG over the fixed order 0..n. Identical cofactors at the same depth SHARE a node. Returns None iff the formula is satisfiable (some fully unfolded branch carries no ⊥). The node count is the number of distinct cofactors — the OBDD width — and is the honest exponential floor on the residue (no order keeps it small).

distinct_width

The distinct-cofactor count — the OBDD width under the fixed order 0..n. Equal to Σ (level widths) and to |cofactor_set|.

group_canon

The group-canonical form of a clause set: the minimum, over every group element g, of the name-normalized image — plus the twist realizing it. Two cofactors in the same G-orbit canonicalize identically, whatever corner of the orbit they sit in.

is_leaf

A leaf: the clause set contains the empty clause ⊥.

iso_canon

The full CNF-isomorphism canonical form: the lex-least image over all relabelings of the live variables and all polarity flips — not tied to any instance automorphism. Above cap live variables it degrades gracefully to first-appearance normalization (the boundary is reported by callers, never silently exceeded).

level_widths

The per-level widths of the strict decision DAG: w[i] = number of distinct residual clause-sets reachable after branching on variables 0..i. The distinct-cofactor count is Σ w[i].

normalize

Deterministic name-normalization: rename variables by first appearance over the sorted clause list, iterated to a fixpoint of (rename, sort). Returns the normalized set and the renaming.

quotient_class_count

The collapse measure. The number of ~-classes among the strict distinct-cofactor set: canonicalize every (depth, cofactor) under ~ and count distinct. Because it is a quotient of the fixed set cofactor_set, it satisfies — as theorems, for every formula — quotient_class_count(Raw) = distinct_width and monotonicity under congruence coarsening (iso ≤ rename ≤ raw). This is the clean instrument for “do exponentially-many cofactors fall into polynomially-many classes?”, with no dependence on any branching order.

quotient_dag

Build the cofactor DAG quotiented by cong: memoize on the canonical form, branch on the first live variable of the (canonicalized) subproblem, and merge ~-equivalent cofactors, recording the realizing twist on each edge. Returns None iff the formula is satisfiable.

quotient_width

The quotient width W(F, ~) — None iff satisfiable.

reduce

A sound poly reduction to fixpoint: unit propagation, then pure-literal elimination, then subsumption, iterated. Each step preserves (un)satisfiability and commutes with relabeling, so reduce(π(F)) = π(reduce(F)) — which makes ReduceIso a legitimate coarsening of UnitPropIso.

structured_leaf

A cofactor is a structured leaf if a decidable specialist refutes it — the full dispatcher (crate::solve::solve_structured) returns UNSAT via a route that is not raw CDCL or the certified-no-shortcut Incompressible verdict. So GF(2)/parity (Tseitin), mod-p (mod-p Tseitin), counting (pigeonhole/exact-cover), 2-SAT, Horn — every nut the paper already cracks — is a leaf here, certified internally by the route it fired. Returns that route, or None if no specialist crushes the cofactor (it must be branched, or it is ⊥/satisfiable).

structured_leaf_dag

Build the structured-leaf cofactor DAG over the fixed order 0..n: a node is a leaf when it is ⊥ or when a specialist crushes it (structured_leaf); otherwise it branches. Identical cofactors at the same depth share a node. None iff the formula is satisfiable.

unit_propagate

Unit-propagate a clause set to fixpoint: repeatedly assign a unit clause’s literal (drop satisfied clauses, delete the falsified literal), stopping at a derived ⊥ or when no unit remains. A sound structural reduction (RUP-certified), monotone under relabeling.

Type Aliases

CanonClauses

A canonicalized CNF: clauses of (var, polarity) literals, each clause sorted+deduped, the clause list sorted+deduped. The node currency of every cofactor DAG here.

Twist

An explicit literal renaming var → (var′, flip), stored on a quotient-DAG edge and verified by the checker: it witnesses that a recomputed cofactor is ~-equivalent to its stored child.