Struct Reduction 

pub struct Reduction {
    pub image: Vec<Lit>,
    pub target_num_vars: usize,
}

A reduction ρ: F' → F — a sign-respecting variable→literal map. It acts on clauses, on substitution witnesses (by conjugation ρσρ⁻¹), and hence on whole refutations. When ρ(F') ⊆ F (the source embeds into the target), ρ carries any refutation of F' to one of F. This is the morphism along which the transfer functor moves collapses between problems.

Fields

image: Vec<Lit>

image[v] = ρ(+v), a literal over the target’s variables.

target_num_vars: usize

Implementations

impl Reduction

pub fn apply_lit(&self, l: Lit) -> Lit

ρ applied to a literal (sign-respecting).

pub fn apply_clause(&self, c: &[Lit]) -> Vec<Lit>

ρ applied to a clause.

pub fn apply_step(&self, step: &ProofStep) -> ProofStep

ρ applied to a proof step (clause + witness).

impl Reduction

pub fn is_bijective(&self) -> bool

Is ρ an isomorphism (a bijective, sign-respecting variable renaming)? Such reductions are the invertible 1-morphisms — they make problems-and-reductions a groupoid.

pub fn inverse(&self) -> Option<Reduction>

The inverse isomorphism ρ⁻¹ (if ρ is bijective).

pub fn compose(&self, other: &Reduction) -> Reduction

Composition self ∘ other (apply other then self).

pub fn is_identity(&self) -> bool

Is ρ the identity reduction?

pub fn is_loop_at(&self, formula: &[Vec<Lit>]) -> bool

Is ρ a loop at F — an isomorphism F → F carrying the clause set onto itself? A loop is exactly an automorphism of F. The loops at F are π₁(F) of the groupoid, and they form the symmetry group of F.