Struct CardinalityTheory 

pub struct CardinalityTheory { /* private fields */ }

A live cardinality theory for the CDCL engine (crate::cdcl::Theory) — the trail-driven twin of the static cutting-plane refuter refute_clausal. It propagates and conflicts on unit-coefficient cardinality constraints (Σ ℓ ≥ k, covering clauses, at-least-k, and at-most-k) directly on the solver’s trail (stateless: it rebuilds the partial assignment each call, so it can never desync), so it FUSES with a GF(2) parity theory (crate::xor_engine::XorEngine) under one crate::cdcl::Solver::solve_with: parity and counting reason together on the shared trail. That is exactly the structure that defeats either alone — e.g. minimal-disagreement parity, a parity core plus a residual cardinality core, where Gaussian elimination handles the parity and cardinality propagation handles the counting, but neither is a refutation by itself.

Pair it with the stateless crate::xor_engine::XorEngine, not the incremental crate::xor_engine::IncXor: IncXor’s trail-sync matches by variable but not value, so a backtrack-then-flip leaves its matrix stale — correct whenever a clausal XOR encoding backs it (the dispatcher’s case), but unsound in a pure-theory fusion with no Boolean clauses to mask it.

Soundness rests on the cardinality reason clause: for Σ ℓ ≥ k over n literals, ANY n − k + 1 of them form a clause entailed by the constraint (at most n − k of the literals can be false, so any n − k + 1 contain a true one). Hence when more than n − k are false, n − k + 1 false literals are an all-false entailed clause — a conflict; when exactly n − k are false, every unassigned literal is forced true with reason {the false literals} ∨ ℓ (size n − k + 1, entailed, currently unit). Every returned clause is a logical consequence of the constraint, so Solver::solve_with may carry it into the learned database soundly.

Implementations

impl CardinalityTheory

pub fn new(num_vars: usize, constraints: &[PbConstraint]) -> Self

Build from normalized PbConstraints. Every input MUST be unit-coefficient (a cardinality constraint); a weighted term is rejected (panic) rather than risk an unsound weighted reason — general weighted PB belongs to the static cutting-plane engine (refute_clausal), not this live clausal-reason theory.

Trait Implementations

impl Theory for CardinalityTheory

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