pub fn recover_cardinality_substructure(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Vec<PbConstraint>Expand description
Recover the cardinality substructure a fused solve consumes: every at-most-k group over arbitrary
literals, k = 1 … MAX_RECOVERED_CARDINALITY — pairwise, ternary, quaternary, … exclusion cliques of
any polarity, so at-most-k, at-least-k (the negated cliques), and mixed counting cores all flow into
the fused theory. Each recover_at_most_k returns immediately when the formula has no width-(k+1)
clause of the right shape, so widening is free on instances that lack those cores.