Module pigeonhole 

Pigeonhole / bipartite-matching detection for the general solver — the cardinality reasoning that lets prove_unsat win on pigeonhole-shaped formulas in POLYNOMIAL time.

A conjunction of “each item is in at least one slot” (positive disjunctions) and “each slot holds at most one item” (pairwise mutual-exclusion clauses) is a bipartite-matching feasibility question. Encoded as boolean SAT it needs exponentially long resolution refutations — the classic wall for CDCL (ours and Z3’s). But the underlying matching is decided in polynomial time with a certified Hall witness (crate::matching).

This module recognizes that structure SOUNDLY — a faithful, fully-verified decomposition or it bails to None — and routes the UNSAT case to the matching reasoner. Soundness: a satisfying assignment of (at-least-one rows ∧ fully-encoded at-most-one columns) is exactly a perfect matching of items to slots (each item ≥1 true variable, each slot ≤1), so “no perfect matching” (a re-verified Hall witness) ⟺ UNSAT. A true from decide_pigeonhole_unsat is therefore always a genuine, witnessed refutation; everything else falls back to CDCL.

Structs

CountingCert

The pigeonhole counting certificate — the symmetry break taken to its absolute limit. For the complete bipartite instance PHP(pigeons → holes) (every pigeon may use every hole, each hole ≤ 1 pigeon), the full pigeon set has neighborhood = all holes slots, so Hall’s condition fails the instant pigeons > holes. That single inequality IS the refutation — sound, O(1), and scale-free.

Functions

certify_pigeonhole_unsat

Certify PHP(pigeons → holes) UNSAT by pure counting, in O(1). Some iff pigeons > holes (Hall violated by the full pigeon set); None otherwise (feasible — a perfect matching can exist).

check_counting_cert

Re-check a counting certificate from scratch: it witnesses UNSAT iff pigeons > holes. O(1), zero trust in how it was produced — the whole refutation is one inequality.

counting_certificate

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).

decide_pigeonhole_unsat

Decide whether e is a clean pigeonhole structure that is UNSAT. Returns true ONLY when the formula decomposes faithfully into at-least-one rows + fully-encoded (clique) at-most-one columns AND the bipartite matching is infeasible with a RE-VERIFIED Hall witness. false otherwise — for a non-pigeonhole formula, or a feasible one (the caller falls back to CDCL). Never a false true.

hall_refutation

The full Hall certificate — the matching symmetry invariant in its complete form. A bipartite cover is infeasible the moment some subset S of items reaches fewer than |S| slots, even when the totals balance and the crude items > slots bound sees nothing. Returns the violating subset (re-checked by is_hall_witness), strictly stronger than counting_certificate. This is the witness behind decide_pigeonhole_unsat’s verdict, surfaced.