Expand description
The affine group AGL(n,p) over GF(p) — the mod-p generalization of the affine break.
crate::affine handles the GF(2) cube: the shears xᵢ↦xᵢ⊕xⱼ no permutation can see, and the
linear obstruction (parity) that decides them. Over a prime p the same picture lifts: the cube
becomes GF(p)ⁿ, signed permutations become the monomial group (one nonzero scalar per row/column —
the Bₙ analog over GF(p)), and AGL(n,p) = { x ↦ A x + b : A ∈ GL(n,p), b ∈ GF(p)ⁿ } is strictly
larger — its GF(p) shears are what mod-p counting (the Count_p / mod-p Tseitin families) is
invariant under and the monomial breakers are blind to. This module is the GF(p) affine layer:
the group itself, an exhaustive ground-truth detector of a GF(p)-system’s affine symmetries (so
AGL(n,p) ⊋ monomial is measured), and the certified GF(p) affine refutation via the mod-p
Gaussian engine and the emit_modp_drat bridge. It reuses crate::modp’s GF(p) arithmetic
throughout (gl_order_p, is_invertible_modp, recover_from_cnf, solve).
Structs§
- AffineP
- An affine map of
GF(p)ⁿ:x ↦ A x + b.matrix[i][j]isA’s entry,translationisb; both reduced modp. A bijection iffA ∈ GL(n,p). - AffineP
Canonical - The reduced one-hot formula over the surviving groups, plus the lift map.
Enums§
- AffineP
Canon - The outcome of the
GF(p)canonical elimination. - AffineP
Forced - The outcome of the
GF(p)SAT-side break.
Functions§
- affine_
m_ canonicalize - The composite-ring canonical elimination. The
ℤ/manalogue ofaffine_p_canonicalizeand the eliminate twin of [prime_power_forced]: over a non-prime modulus, recover the mod-msystem, take its [composite_break_structure], and physically eliminate the determined one-hot structure rather than merely injecting it. A forced group (x_gpinned to a single value) becomes constants; a partially forced group (x_gconfined to a cosetv ≡ res (mod modu),1 < modu < m) keeps only its on-coset bits, the rest pinned false; a linked group’s bits alias its representative’s, value-permuted (b(g,v) = b(rep, σ(v)),σ(v) = (v−d)·c⁻¹ mod m). The result is equisatisfiable over the surviving bits, withAffinePCanonical::liftto recover the rest. An inconsistent componentAffinePCanon::Refuteds; a prime modulus is left toaffine_p_canonicalize. - affine_
m_ forced - The composite
ℤ/mSAT-side break (squarefreem), the full mod-manalogue ofaffine_p_forcedvia CRT (ℤ/m ≅ ∏ GF(pᵢ)). Solve the system over each prime field, then for each variable combine the per-prime structure: - affine_
p_ canonicalize - The
GF(p)canonical RREF break (elimination). The one-hot analogue ofcrate::affine::affine_canonicalize: recover the mod-psystem and solve its space, then physically eliminate the determined one-hot groups rather than merely injecting their consequences. A forced group’s bits become constants; a linked group’s bits alias to its representative’s, value-permuted (b(g,v) = b(rep, σ(v))withσ(v) = (v−d)·c⁻¹). The result is an equisatisfiable formula over the surviving (free/representative) groups, withAffinePCanonical::liftto recover the eliminated bits. An inconsistent coreAffinePCanon::Refuteds; a composite modulus is left toaffine_m_forced. - affine_
p_ forced - The
GF(p)SAT-side break. Recover the one-hot mod-psystem (crate::modp::recover_from_cnf) and solve its solution space (crate::modp::solve_space), whose kernel is the affine translation symmetry. Two structures fall out, the mod-panalogues ofcrate::affine::affine_reduce’s forced units and equivalence classes: - affine_
p_ refutation_ drat - The clausal DRAT certificate for a
GF(p)affine refutation, orNoneif the formula’s mod-pcore is not inconsistent (or the resolution expansion overruns its budget). Recovers the one-hotGF(p)system, finds theΣ multiplierᵢ·equationᵢdependency whose left side cancels while the right does not (crate::modp::solve), and compiles it to RUP resolvent lemmas over the Boolean one-hot encoding through thecrate::xor_dratbridge —drat-trim-checkable against the original CNF, the mod-pgeneralization ofcrate::affine::affine_refutation_drat. - affine_
p_ symmetries - The affine symmetry group of a
GF(p)model set, computed exhaustively: everyφ ∈ AGL(n,p)that maps the model set onto itself. TheAGL(n,p)analogue ofcrate::affine::affine_symmetries— the instrument that measuresAGL(n,p) ⊋ monomial. - agl_
m_ order |AGL(n, ℤ/m)|for squarefreem: by CRT (ℤ/m ≅ ∏ GF(pᵢ)) the affine group factors as∏ AGL(n, pᵢ), so the order is the product of the prime orders.Noneifmis not squarefree.- agl_
p_ order |AGL(n,p)| = pⁿ · |GL(n,p)|.- all_
affine_ p_ bijections - Every affine bijection of
GF(p)ⁿ(each invertible matrix × each translation). Exhaustive — for ground-truth symmetry computation only — bounded sop^{n²} ≤ 200_000. - models_
p - The
GF(p)-valued solutions of a mod-plinear system (Σ coeffs·x ≡ rhs (mod p)for each equation), brute force overpⁿ— smallnonly.