Module matching 

Certified bipartite-matching infeasibility — the polynomial reasoner for pigeonhole-shaped problems that are exponential for resolution (and therefore for any CDCL SAT solver, ours included).

Many infeasibility claims are really “n items must each take a distinct slot, but they only reach m < n slots” — graph colouring of a clique (n mutually-adjacent movements need n phases), the pigeonhole principle, exam scheduling, register allocation. Encoded as boolean SAT these are pigeonhole instances, which need exponentially long resolution refutations. But the underlying question — does a system of “each slot holds at most one item” constraints admit an assignment of every item? — is just bipartite maximum matching, decided in polynomial time.

assign_or_hall returns either a feasible assignment (a checkable witness of feasibility) or a Hall witness: a set S of items whose combined reachable slots T satisfy |T| < |S|, so the items cannot be placed (a checkable witness of infeasibility, à la a clique or an odd cycle). Both outcomes are independently re-verifiable — is_hall_witness and a feasibility check — so this is a certified decision, never a trusted solver verdict.

Structs

CapHallWitness

A capacitated Hall certificate: the items in S can only reach the slots in slots, whose total capacity is strictly less than |S| — so they cannot all be placed. Re-checkable via is_cap_hall_witness.

HallWitness

A Hall-theorem certificate of infeasibility: items (the set S) can collectively reach only the slots in slots (a superset of N(S)), and slots.len() < items.len() — so by pigeonhole the items cannot be placed one-per-slot. Independently checkable via is_hall_witness.

Enums

CapMatchOutcome

The outcome of a capacitated assignment: each slot s holds at most capacities[s] items.

MatchOutcome

The outcome of a bipartite “each slot holds at most one item” feasibility check.

Functions

assign_or_hall

Decide whether every item can be assigned a distinct slot, where adj[i] lists the slots item i may use and slots range over 0..num_slots. Returns a perfect assignment or a certified Hall witness. Finds a maximum matching with Hopcroft–Karp (O(E·√V) — many shortest vertex-disjoint augmenting paths per phase, far faster than Kuhn’s O(V·E) as instances grow), then — on failure — the König alternating-reachability construction extracts the deficient set.

assign_or_hall_capacitated

Decide whether every item can be assigned a slot when slot s holds at most capacities[s] items (a b-matching / resource-allocation feasibility — e.g. traffic movements sharing capacity-limited green windows). Reduces to plain matching by splitting each slot into that many interchangeable copies, then maps the result (and any Hall witness) back to original slots.

is_cap_hall_witness

Re-check a capacitated Hall witness: every item in S reaches only slots in T, and the total capacity of T is below |S|.

is_hall_witness

Independently re-check a Hall witness: every item in S reaches only slots in T, and |T| < |S|. This is the certificate verifier — a trusted, solver-free check that the claimed infeasibility is genuine.

is_valid_assignment

Re-check a feasible assignment: one distinct slot per item, each within that item’s allowed set.