pub fn counting_certificate(e: &ProofExpr) -> Option<CountingCert>Expand description
Expose the O(1) counting certificate for any matching-shaped cover, not just literal pigeonhole:
recover the bipartite (items → slots) structure and certify UNSAT by the full-set Hall bound
items > slots. Fires for pigeonhole and clique-coloring (n vertices, k < n colors) — the
same crush, derived structurally. None when there is no such bipartite structure or the full set
does not overflow the slots (a subset-Hall failure is still caught by decide_pigeonhole_unsat).