Struct SymmetryTheory 

pub struct SymmetryTheory { /* private fields */ }

A live symmetry theory for crate::cdcl::Solver::solve_with — DYNAMIC lex-leader propagation over the whole symmetry group. Each element is an AFFINE map α (a model-set automorphism) given as a per-output spec α(x)[i] = ⊕_{s∈xset_i} x_s ⊕ b_i; permutations are the special case where every xset is a single variable. During search it enforces x ≤_lex α(x): walking positions while the prefix stays equal, computing α(x)[i] from the trail (an XOR of the support), then at the frontier forcing x_i = 0 when α(x)[i] = 0, forcing the last free support bit to make α(x)[i] = 1 when x_i = 1, or conflicting — AUX-FREE, on the shared trail, fused alongside the parity and cardinality theories. Sound: the orbit’s global lex-minimum satisfies x ≤_lex α(x) for EVERY α, so the whole group’s predicate keeps exactly one representative per orbit (equisatisfiable), and every reason clause (prefix + support witnesses) is implied by it.

Implementations

impl SymmetryTheory

pub fn new(num_vars: usize, maps: Vec<Vec<(Vec<usize>, bool)>>) -> Self

pub fn from_perms(num_vars: usize, perms: Vec<Vec<usize>>) -> Self

Convenience: build from variable permutations (each σ[i] the image variable of output i).

Trait Implementations

impl Theory for SymmetryTheory

fn propagate(&mut self, trail: &[Lit]) -> Vec<Vec<Lit>>

Given the solver’s current trail (assigned literals in assignment order), return a clause that is theory-entailed and currently unit or falsified (so the core will propagate or conflict on it), or None at a theory fixpoint. The trail is passed in order — and shrinks on backtrack — so an incremental theory can sync forward/undo against it (LIFO). The returned clauses MUST each be a sound consequence of the theory. Returning the whole batch of forced clauses at once (rather than one per call) lets an incremental theory amortise its work over one pass instead of rescanning per implication. An empty vec means “theory fixpoint”.