Struct StructuredReduceIso 

pub struct StructuredReduceIso {
    pub cap: usize,
}

The reduction rung fused with the non-resolution crushers as terminals: reduce to fixpoint, then if a non-resolution specialist (parity/GF(2), mod-p, exact-cover, algebraic collapse) refutes the reduced cofactor, collapse it to one “crushed” class; otherwise canonicalize up to iso. Coarser than ReduceIso (all non-resolution-crushable reduced cofactors merge into one), so struct-reduce-iso ≤ reduce-iso. This is the rung that can beat the Chvátal–Szemerédi resolution cap — GF(2)/mod-p are polynomial exactly where resolution is exponential — measured via quotient_class_count (specialist verdicts certified by their routes; reduce by RUP).

Fields

cap: usize

Trait Implementations

impl Congruence for StructuredReduceIso

fn name(&self) -> &str

A short label for reporting ("identity", "Bn", "AGL", "cofactor-iso").

fn canonicalize(&self, clauses: &CanonClauses) -> (CanonClauses, Twist)

The canonical representative of clauses’s class, and the twist mapping clauses onto it (i.e. apply_twist(clauses, twist) == representative).