pub fn prove_unsat_certified_cnf(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<Vec<ProofStep>>Expand description
prove_unsat_certified for a CNF the caller has ALREADY built — the seam for a producer
that clausifies something other than a ProofExpr tree (a bit-blaster asserting a shared gate
DAG, whose tree form is exponentially larger than the circuit). Same refutation, same steps:
the certificate is a function of the clause set, never of how it was spelled.