Enum Route 

pub enum Route {
    TwoSat,
    Horn,
    Lll,
    Pigeonhole,
    CuttingPlanes,
    Parity,
    ExactCover,
    ModP,
    ModM,
    Collapse,
    HybridXor,
    Sos,
    Nullstellensatz,
    SymmetryBreak,
    NestedSymmetry,
    Sel,
    LocalSymmetry,
    OrbitalBranch,
    SymmetricProbe,
    SymmetricBinary,
    OrbitWeightQuotient,
    SymmetryPropagate,
    SymmetricComponent,
    SymmetrySimplify,
    SemanticSymmetry,
    AlmostSymmetry,
    DeclaredSymmetry,
    RecursiveBreak,
    Incompressible,
    Component,
    BoundedVarElim,
    EquivLit,
    TreeWidth,
    Cdcl,
}

Which engine decided the instance.

Variants

TwoSat

Horn

Lll

Pigeonhole

CuttingPlanes

Parity

ExactCover

Exactly-one groups harvested from the raw clauses (all-positive clause + full pairwise at-most-one) yield Σ_{v∈g} x_v = 1 over every modulus; Gaussian elimination over small fields finds the counting obstruction — the parity sum, the signed bipartite combination — with the refutation re-checked fail-closed. The covering-encoded counting crusher.

ModP

ModM

Collapse

HybridXor

Sos

Nullstellensatz

SymmetryBreak

NestedSymmetry

Sel

LocalSymmetry

OrbitalBranch

SymmetricProbe

SymmetricBinary

OrbitWeightQuotient

SymmetryPropagate

SymmetricComponent

SymmetrySimplify

SemanticSymmetry

AlmostSymmetry

DeclaredSymmetry

RecursiveBreak

Incompressible

The formula is certified to carry no linear/parity symmetry shortcut and is provably rigid, so the symmetry arsenal is useless — decided by CDCL with that honest “no shortcut” verdict on record.

Component

The formula split into independent components with no symmetry relating them; each was solved apart through the full arsenal and the verdicts combined (the plain-decomposition analogue of separability).

BoundedVarElim

Certified bounded variable elimination (Davis–Putnam, non-growing) reduced the formula to ⊥. The missing preprocessing crusher: it refutes bounded-treewidth cores the symmetry/algebra chain declared Incompressible. Its RUP resolvents + clause deletions are the independently checkable proof.

EquivLit

The binary-implication graph’s SCCs forced x ≡ ¬x — the 2-clauses alone refute the formula. Catches general (non-pure-2SAT) formulas whose binary sub-part is contradictory, which the pure-TwoSat route misses. Certified by a short RUP chain ((x), (¬x), ⊥), re-checkable by propagation.

TreeWidth

Davis–Putnam bucket elimination refuted the formula with every resolvent width ≤ a cap — a bounded- treewidth resolution certificate (2^w·n). Covers the medium-treewidth families that BVE’s non-growing rule misses; declines (leaving Incompressible) on the high-treewidth residue where width would blow up.

Cdcl

Trait Implementations

impl Clone for Route

fn clone(&self) -> Route

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Route

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for Route

fn eq(&self, other: &Route) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for Route

impl Eq for Route

impl StructuralPartialEq for Route