Skip to main content

Module affine_gfp

Module affine_gfp 

Source
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] is A’s entry, translation is b; both reduced mod p. A bijection iff A ∈ GL(n,p).
AffinePCanonical
The reduced one-hot formula over the surviving groups, plus the lift map.

Enums§

AffinePCanon
The outcome of the GF(p) canonical elimination.
AffinePForced
The outcome of the GF(p) SAT-side break.

Functions§

affine_m_canonicalize
The composite-ring canonical elimination. The ℤ/m analogue of affine_p_canonicalize and the eliminate twin of [prime_power_forced]: over a non-prime modulus, recover the mod-m system, take its [composite_break_structure], and physically eliminate the determined one-hot structure rather than merely injecting it. A forced group (x_g pinned to a single value) becomes constants; a partially forced group (x_g confined to a coset v ≡ 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, with AffinePCanonical::lift to recover the rest. An inconsistent component AffinePCanon::Refuteds; a prime modulus is left to affine_p_canonicalize.
affine_m_forced
The composite ℤ/m SAT-side break (squarefree m), the full mod-m analogue of affine_p_forced via 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 of crate::affine::affine_canonicalize: recover the mod-p system 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, with AffinePCanonical::lift to recover the eliminated bits. An inconsistent core AffinePCanon::Refuteds; a composite modulus is left to affine_m_forced.
affine_p_forced
The GF(p) SAT-side break. Recover the one-hot mod-p system (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-p analogues of crate::affine::affine_reduce’s forced units and equivalence classes:
affine_p_refutation_drat
The clausal DRAT certificate for a GF(p) affine refutation, or None if the formula’s mod-p core is not inconsistent (or the resolution expansion overruns its budget). Recovers the one-hot GF(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 the crate::xor_drat bridge — drat-trim-checkable against the original CNF, the mod-p generalization of crate::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. The AGL(n,p) analogue of crate::affine::affine_symmetries — the instrument that measures AGL(n,p) ⊋ monomial.
agl_m_order
|AGL(n, ℤ/m)| for squarefree m: by CRT (ℤ/m ≅ ∏ GF(pᵢ)) the affine group factors as ∏ AGL(n, pᵢ), so the order is the product of the prime orders. None if m is 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 so p^{n²} ≤ 200_000.
models_p
The GF(p)-valued solutions of a mod-p linear system (Σ coeffs·x ≡ rhs (mod p) for each equation), brute force over pⁿ — small n only.