Skip to main content

affine_transvection_generators

Function affine_transvection_generators 

Source
pub fn affine_transvection_generators(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Vec<(u32, u32)>
Expand description

A scalable, ∀n affine-symmetry finder — the transvection generators, in polynomial time. Exhaustive AGL(n,2) enumeration is stuck at n ≤ 4; this finds every transvection x_i ↦ x_i ⊕ x_j that is an affine automorphism of the clause set, in O(n² · |clauses|) time via [transvection_image_clause] — no 2ⁿ anywhere, so it runs at any n. Sound: every returned pair is a genuine automorphism (the produced clause set is checked equal to the original). Incomplete by design: an affine symmetry realized only by a composite of transvections (e.g. parity’s shears, products of two transvections) is not a single generator and is not returned — completeness for general formulas is a hard affine-equivalence problem, and the closed form (crate::affine::affine_subspace_agl_order) is the route for structured families.