Module infeasibility_refutation 

Refuting an infeasibility verdict with a point that is actually feasible.

Why this exists

Infeasible_Problem_Detected (AMPL solve_result_num 200, Pyomo TerminationCondition.infeasible) is the most consequential thing POUNCE can say: a caller told a feasible model is infeasible has no signal that anything went wrong. It fails silently and confidently, which is worse than an error.

The numerical paths that produce that verdict — the restoration gates, the outer cycle detector, the SQP infeasible-subproblem exit, the ℓ₁ wrapper’s uncollapsed-slack certificate — all reason from a local argument: the feasibility sub-problem stopped making progress at a point whose violation is bounded away from zero. That is evidence, not proof, and gh #379 is what it looks like when the evidence is wrong. On seed 294 of the feasible-by-construction property sweep (pyomo-pounce/tests/test_infeasibility_no_false_positives.py) the solver starts at a point that satisfies every row exactly, walks away from it (the model carries ±1e30 row coefficients, so the barrier’s slack initialization moves the scaled slack far from what x can follow), burns the restoration budget, and reports the model infeasible.

A concrete feasible point settles the question outright. If some x inside the variable box satisfies every constraint, the feasible set is not empty, whatever a local argument concluded. So: before any numerical path is allowed to say “infeasible”, try to refute it.

Which point

The model’s own starting point, clamped into the variable box. Deliberately only that one, unlike the presolve-side refutation (pounce_presolve::witness_refutes_infeasibility), which also samples the box midpoint and corners.

The two are answering different questions. Presolve claims a proof over the whole box from interval arithmetic, so probing the box is exactly the right counter-evidence. Here the claim is numerical and the refutation runs on every solve that ends in the infeasible band; widening it to sampled points would change verdicts on models this change cannot be validated against (the benchmark corpus is not in the tree). The starting point needs no such justification: a modeller who hands the solver a feasible point and is told the model is infeasible has been given a wrong answer under any reading.

Direction

One-directional, like its presolve twin: this can only ever withdraw a verdict, never create one. A model with no feasible point cannot produce a witness, so a genuinely infeasible model is untouched — and any failure to evaluate (eval_g returning false, a non-finite value, a missing starting point) simply declines to refute.

Structs

FeasibleWitness

A point that satisfies every constraint and bound, disproving a candidate infeasibility verdict.

Functions

starting_point_refutes_infeasibility

Try to refute a candidate infeasibility verdict using the model’s starting point.