pub fn incompressibility_gate(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<LinearStructureCert>Expand description
The SAT-dispatcher gate: Some(cert) iff F’s parity structure is fully exposed AND F is provably
rigid (|Aut| = 1), so the symmetry arsenal is provably useless and the solver may go straight to
CDCL with an honest “no shortcut of this class” verdict. The exact rigidity check
(symmetry_entropy_bits == 0) is size-gated — past [GATE_SYMMETRY_MAX_VARS] the gate declines rather
than run the superpolynomial automorphism search (there is no cheap sound global-asymmetry test; it is
graph-isomorphism-hard). Fail-closed throughout: any doubt returns None and the arsenal runs as usual.