Module affine 

The affine group AGL(n,2) — the symmetry a permutation break cannot see.

The clause-level symmetry breakers (symmetry_detect, sym_certify) quotient by the hyperoctahedral group Bₙ of signed variable permutations. Bₙ is exactly the subgroup of AGL(n,2) (affine bijections x ↦ A x ⊕ b of the cube GF(2)ⁿ) whose linear part A is a permutation matrix. The census proved the clause breakers are complete for Bₙ — yet AGL(n,2) ⊋ Bₙ, and the gap is the shears xᵢ ↦ xᵢ ⊕ xⱼ. A shear maps an axis-aligned subcube (a clause) to a non-subcube, so no amount of clause permutation can reach it. That gap is precisely why parity / Tseitin formulas — affine invariant, Bₙ-rigid — defeat clause symmetry breaking and need a linear-algebra engine instead.

This module is that engine, at the symmetry level: the AGL(n,2) group itself, an exhaustive ground-truth detector of a formula’s affine symmetries (so AGL ⊋ Bₙ is measured, not asserted), and the affine break — recover the formula’s GF(2)-linear substructure, Gauss-eliminate it, and either refute an inconsistent linear core or inject the forced units / equivalences (the linear consequences no single clause states) that collapse the residual search.

Structs

Affine

An affine map of the Boolean cube GF(2)ⁿ: x ↦ A x ⊕ b. matrix[i] is row i of A as a coefficient bitmask over the low n bits; translation is b. It is a bijection iff A ∈ GL(n,2).

AffineCanonical

The result of the canonical affine reduction: an equisatisfiable formula over the free generators (the linearly-determined variables eliminated), plus the map to lift a reduced model back to the full space. This is the affine analogue of breaking a permutation orbit down to one representative — here the RREF canonicalizes the affine structure and the determined coordinates fall away.

Enums

AffineCanon

The outcome of the canonical RREF break.

AffineOutcome

The outcome of the affine break.

Functions

affine_canonicalize

The affine SBP — the canonical RREF break. Recover the formula’s GF(2)-linear substructure and take its reduced row-echelon form (via gf2::solve_gf2, whose kernel basis is the affine translation symmetry). The RREF partitions variables into free generators and determined coordinates: every variable the kernel never moves is forced to a constant, and every set the kernel moves in lockstep is an equivalence class collapsing to one representative. Substituting those determined coordinates out yields an equisatisfiable formula over the free generators alone — the affine symmetry quotiented to a canonical representative, exactly as a permutation lex-leader collapses an orbit. An inconsistent core instead AffineCanon::Refuteds (certified). Sound: the eliminated relations are GF(2)-entailed by the formula, so AffineCanonical::lift turns any reduced model into a full one.

affine_reduce

The affine GF(2) break. Recover the formula’s linear substructure and Gauss-eliminate it (gf2::solve_gf2): an inconsistent core AffineOutcome::Refuteds outright; otherwise the elimination’s gf2::SolutionSpace exposes which variables are forced (the kernel never moves them ⇒ a unit) and which are locked together (the kernel moves them in lockstep ⇒ an equivalence), and we return those consequences as new clauses (AffineOutcome::Forced) — the linear inferences the permutation breaker structurally cannot make.

affine_refutation_drat

The clausal DRAT certificate for an affine refutation, or None if the formula’s linear core is not inconsistent (or num_vars exceeds the u64 mask, or the resolution expansion overruns its budget). Recovers the XOR system, finds the GF(2) linear dependency that sums to 0 = 1 (crate::xorsat::solve), and compiles it to RUP resolvent lemmas through the crate::xor_drat bridge — the same path Route::Parity uses, so it is drat-trim-checkable against the original CNF.

affine_subspace_agl_order

The affine automorphism group order of a k-dimensional affine subspace of GF(2)ⁿ — i.e. the number of affine maps x ↦ Ax ⊕ b fixing the model set of an XOR-defined family whose solution space has dimension k. In closed form, computable at every n without enumerating AGL(n,2): |GL(k,2)| · |GL(n−k,2)| · 2^{k(n−k)} · 2^k — the block-upper-triangular invertible linear parts (GL(k) on the subspace, GL(n−k) on the quotient, 2^{k(n−k)} shears between them) times the 2^k in-subspace translations. The scalable affine-symmetry detector for the whole class of linear families: Bₙ sees a vanishing fraction of it (see the tests).

affine_symmetries

The affine symmetry group of a formula, computed exhaustively: every φ ∈ AGL(n,2) that maps the model set onto itself (φ a bijection, so φ(models) = models iff φ maps each model to a model). This is the AGL(n,2) analogue of symmetry_detect::find_generators (which finds only the Bₙ part), and it is exact for n ≤ 4 — the instrument that measures AGL ⊋ Bₙ.

agl_order

|AGL(n,2)| = 2ⁿ · |GL(n,2)| — the 2ⁿ translations times the invertible linear parts.

all_affine_bijections

Every affine bijection of GF(2)ⁿ (each invertible matrix × each translation). Exhaustive — for ground-truth symmetry computation only — so it is capped at n ≤ 4 (|AGL(4,2)| = 322 560).

models_of

The satisfying assignments of a CNF, each packed into the low num_vars bits of a u64. Brute force over 2^{num_vars} — small n only (the census / symmetry-measurement regime).

recover_linear_system

Recover the GF(2)-linear substructure of a CNF: the XOR equations its clauses encode (units, binary equivalences, and complete wrong-parity bundles), as (coefficient-mask, rhs) rows over the low num_vars bits. None when there is no linear structure or num_vars exceeds the u64 mask.