Function clause_agl_symmetries 

pub fn clause_agl_symmetries(num_vars: usize, clauses: &[Vec<Lit>]) -> usize

The clause-level AGL symmetry detector — the affine analog of the Bₙ stabilizer, and the one symmetry lens that works on UNSAT formulas (the model-based detector is vacuous — no models). An affine map φ : x ↦ Ax ⊕ b (φ ∈ AGL(n,2)) is a clause-set automorphism iff, acting on 𝔽₂ⁿ, it permutes the falsifying-point sets of the clauses. Since Bₙ ⊆ AGL(n,2), |Aut_AGL| ≥ |Bₙ-stabilizer|; a Bₙ-rigid core with |Aut_AGL| > 1 has hidden affine symmetry (breakable by an affine SBP); |Aut_AGL| = 1 means it is affine-rigid — structure-minimal at the affine level too. Brute over AGL(n,2), feasible n ≤ 4.