Module cardinality 

Cardinality constraints over boolean ProofExpr atoms — the missing primitive that lets the certified solver answer “at most / at least / exactly k of these are true”. Encoded with Sinz’s sequential counter (linear in n·k, fresh auxiliary atoms under a caller-chosen prefix), so the result is an ordinary boolean obligation the existing CNF/CDCL/RUP pipeline discharges. This is the building block for SAT-based optimization (crate::optimize).

Correctness is pinned exhaustively against a brute-force oracle (every assignment, small n).

Functions

at_least

“At least k of vars are true” — i.e. at most n−k are false.

at_most

“At most k of vars are true.” Auxiliary atoms are named {aux}_{i}_{j}, so distinct constraints in one formula must use distinct aux prefixes.

exactly

“Exactly k of vars are true.”