Skip to main content

incompressibility_gate

Function incompressibility_gate 

Source
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.