Feasibility Certificate Check¶

Checking method — instantiates Generate-and-Verify Separation

Accepts or prunes a candidate branch by checking a supplied certificate — a witness that a solution exists, or a compact rationale that none can — instead of re-searching it.

A search process can be enormously expensive while the evidence it produces is trivial to check. Feasibility Certificate Check exploits exactly that gap: it never searches or re-derives anything, it consumes a certificate the generator emits and verifies it. A feasibility certificate is a concrete witness — an assignment, a point, a schedule — that demonstrably satisfies every mandatory constraint; an infeasibility certificate is a compact rationale (say, a contradictory subset of the constraints) proving that an entire branch can hold no solution at all. The one idea that makes it this mechanism and not its siblings is that acceptance rides on a generator-supplied witness of feasibility only — not optimality, not quality, not a predicate the checker holds itself. Confirm the witness and accept; confirm the infeasibility rationale and discard the whole subtree unexplored.

Example¶

An airline is solving a crew-pairing problem as a large integer program, branching over which crews fly which sequences. Deep in the branch-and-bound tree, one node's relaxed subproblem has no feasible assignment — but proving that by re-solving the node from scratch would be costly, and there are millions of nodes. Instead the solver emits an infeasibility certificate: a nonnegative combination of the node's own constraints that sums to a plain contradiction (the classic Farkas-style witness, 0 ≤ −1). The checker's entire job is to multiply the constraints by the supplied weights and confirm the contradiction — arithmetic, not search. Once confirmed, the node and everything beneath it are pruned. When a leaf finally yields a full crew schedule, the same mechanism runs the other polarity: it walks the proposed schedule against every rule (rest minima, qualifications, base coverage) and certifies it as a genuine feasible witness. Producing either certificate was hard; checking each is cheap and independent of the solver's internals.

How it works¶

What sets it apart from the other checkers is that it is certificate-driven and two-polarity:

Consume, don't compute. The input is a certificate, not the raw problem; the mechanism verifies the certificate's internal validity rather than re-running the search.
Two polarities, one contract. A feasibility witness is checked by substitution ("does this point satisfy all constraints?"); an infeasibility certificate is checked by confirming its rationale ("do these weights really force a contradiction?").
Bind before believing. Each certificate is verified to belong to the exact subproblem it claims, so a certificate valid for one branch cannot be replayed against a different one.

Tuning parameters¶

Certificate format & strength — what counts as an admissible certificate (a full witness point, a dual/Farkas vector, an unsat core). Stronger formats are harder for the generator to produce but cheaper and more certain to check.
Polarity coverage — whether the mechanism only certifies feasibility (accept witnesses), only prunes (check infeasibility), or both. Pruning is where most of the search savings live.
Binding strictness — how tightly the certificate is tied to the precise subproblem hash/version; loose binding is fast but admits stale or mismatched certificates.
Numerical tolerance — how much constraint slack still counts as "satisfied." Too loose and a near-violation is certified; too tight and rounding noise rejects valid witnesses.
Model-trust stance — whether to re-check the constraint set the certificate refers to, or trust the generator's rendering of it.

When it helps, and when it misleads¶

Its strength is leverage: a one-line certificate can retire an astronomically large region of a search space, and because the check is self-contained, an entirely untrusted solver can participate — its certificates stand or fall on their own. The advantage is real precisely because producing feasibility is hard and checking it is easy.

The failure mode is that a certificate proves feasibility only with respect to the modeled constraints. If the real problem has a constraint the model omits, a perfectly valid "feasible" witness certifies something worthless — the archetype's core warning, a narrow technical property silently standing in for real-world validity. The classic misuse is accepting a certificate's polarity without checking its binding, so a certificate minted for another node quietly prunes a branch that actually contained the answer, and the lost solution never surfaces. The discipline that guards against both is to validate the constraint model against reality and to verify binding on every certificate, treating an unsound infeasibility certificate as the most dangerous kind of pass.^[1]

How it implements the components¶

Feasibility Certificate Check fills only the witness-handling components — the parts a certificate consumer can own:

witness_or_certificate_contract — it defines and consumes the certificate format itself: what a feasibility witness or an infeasibility rationale must contain to be checkable.
candidate_evidence_binding — it verifies each certificate is bound to the exact subproblem it claims, so valid evidence cannot be replayed against a different candidate.

It does not evaluate a standing acceptance predicate or declare a soundness/completeness boundary — that is the Constraint and Invariant Checker — and it does not gate any release on the result, which is the Verification Hold Point.

Instantiates: Generate-and-Verify Separation — it supplies the cheap acceptance/pruning step that lets an untrusted, expensive search be trusted through its output.
Sibling mechanisms: Constraint and Invariant Checker · Proof Checking · Proof-Carrying Artifact Gate · Untrusted Solver with Trusted Checker · Succinct Cryptographic Proof Verifier

Notes¶

The mechanism certifies feasibility, and nothing more — a certified schedule may be legal yet far from the cheapest one. Optimality, ranking, and comparison are separate concerns; conflating "feasible" with "good" is the most common way a certificate check is over-read.

References¶

[1] Farkas' lemma is the formal basis for linear-programming infeasibility certificates: a system has no feasible point exactly when a nonnegative combination of its constraints yields a contradiction, so the certificate is a finite object a checker can validate directly. Used correctly it makes pruning sound; the caution above is that it is only sound relative to the constraints actually written down. ↩