pub fn recover_at_most_k(
num_vars: usize,
clauses: &[Vec<Lit>],
k: usize,
) -> Vec<PbConstraint>Expand description
Recover the at-most-k cardinality substructure over arbitrary LITERALS — the generalisation of
recover_at_most_one to WIDER and MIXED-POLARITY counting cores (the ternary at-most-two cores of
parity-learning instances, and — via negation — at-least-k). Work in literal codes (2·var + sign,
negation flips the low bit). A width-(k+1) clause ℓ₀ ∨ … ∨ ℓ_k is violated only when all of
{¬ℓ₀,…,¬ℓ_k} are true, so it FORBIDS that literal set; a set S of literals (distinct variables) is an
at-most-k group iff EVERY (k+1)-subset of S is some clause’s forbidden set. Greedy maximal extension
from each forbidden seed — a literal joins S only when every k-subset of S together with it is
forbidden, so the invariant keeps every (k+1)-subset forbidden and at_most(S, k) genuinely implied by
clauses present (sound to fuse). A clause [¬a,¬b,¬c] ⇒ at-most-2 of {a,b,c}; the three clauses
[a,b],[a,c],[b,c] ⇒ at-most-1 of {¬a,¬b,¬c} = at-least-2 of {a,b,c}. k = 1 over all-negative
binary clauses reproduces recover_at_most_one.