pub fn recover_at_most_one(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Vec<PbConstraint>Expand description
Recover the at-most-one cardinality substructure from arbitrary clauses — the substructure twin of
[discover_covering], which requires the WHOLE formula to be a covering (so a single XOR gadget makes it
decline). Binary all-negative clauses ¬a ∨ ¬b are at-most-one edges; this returns an at_most(group, 1)
PB constraint per maximal exclusion clique of size ≥ 2, IGNORING every other clause. Each emitted group is
a verified FULL clique (every pair has its exclusion clause present), so its ≤ 1 is implied by clauses
in the formula — sound to feed a solver alongside a recovered parity system (the par32 fusion).