pub fn counting_certificate(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<CountingCert>Expand description
Recover a Count_q(n) core from clauses and refute it by the q ∤ n counting argument, or None
if there is no such core. Conservative / fail-closed — see the module docs.