fix(correctness): LP presolve fabricated bounds from the INF sentinel

[jkitchin]

The defect

crates/discopt-core/src/lp/simplex/presolve.rs decides whether a column's contribution to a row is unbounded by testing the product a_ij * x_j against the sentinel INF = 1e20:

let (cmin, cmax) = if aij > 0.0 { (aij*lo[j], aij*hi[j]) } else { (aij*hi[j], aij*lo[j]) };
if cmin <= -INF { n_min_inf += 1; } else { sum_min_finite += cmin; }

INF is a sentinel, not a true infinity. For |a_ij| < 1 an unbounded column contributes an ordinary finite number — -0.5 * 1e20 = -5e19 — which fails the <= -INF test and is booked as a finite activity. Two things then go wrong at once:

1. the row's activity range is no longer recognised as unbounded, so the pass derives bounds it has no right to derive; and
2. the huge magnitude annihilates every smaller term in the running sum (ulp(5e19) = 8192), so the residual sum_min_finite - ck_min evaluates to exactly 0.0 instead of its true value.

The result is an invalid tightening. Presolve is dimension-preserving with no postsolve, so the mutilated box goes straight to the B&B tree and the node LPs, and the search reports OPTIMAL on a box the optimum has been removed from — a false dual bound. The module's own docstring promises the pass "never cuts a feasible (let alone optimal) solution"; it did.

Minimal reproducer

min 4096·x0    s.t.  -0.5·x0 - 1.9073486328125·x1 <= -17.612222262299806
                     x0 in [0, inf),  x1 in [2.56, 1600.0]

x1 = 1600 satisfies the row on its own (activity −3051 ≤ −17.6), so x0 = 0 is feasible and optimal at objective 0. HiGHS agrees. Pre-fix, presolve fabricates x0 >= 35.2244 and the solver returns OPTIMAL at 144279.32 — and 4096 × 35.2244 = 144279.32 exactly.

The threshold is precisely the sentinel: x0 upper bound of 1e19 is correct, while 1e20, 1e21, 1e25 and inf are all wrong.

How it was found, and how the layer was identified

gear4 returned status=optimal objective=bound=184279.32477 gap_certified=True against a true optimum of 1.643428474 (this repo's own test_gear4_false_infeasible.py, and minlplib.solu).

The layer was pinned by a box-monotonicity check that needs no oracle: a valid relaxation bound is antitone in the box, so capping an infinite endpoint (which shrinks the box) cannot lower the bound. On gear4 the raw box gave 184279.32 and a box capped at 1e6 — a strict subset — gave 0.0. Enlarging the box raised the minimum, which is impossible.

That pointed at the relaxation, but the relaxation was exonerated: A, b, c, obj_offset and the objective floor are byte-identical between the two builds; only two column bounds differ. Handing the identical LP to scipy/HiGHS returned 0.0 while the in-house path returned 184279.32. Equilibration was also exonerated (scipy returns 0.0 on both the scaled and unscaled systems). Shrinking the equilibrated LP greedily while the discrepancy persisted reduced 44×16 to the 1×2 case above.

Fix

Infinity is now decided on the bounds (lo <= -INF / hi >= INF) in a shared contrib() helper used by both the activity-sum loop and the per-column loop.

Additionally, each derived bound is widened by an explicit rounding-error budget 8 * eps * max_abs_term, so that a legitimately large but finite bound swamping the smaller terms cannot reproduce the same false tightening by cancellation. For terms of order 1e3 that is ~2e-13 — no practical loss of propagation.

This is a general defect, not a gear4 quirk

In the differential fuzz added here, 11 of 174 random LPs with unbounded columns (6.3%) returned a claimed-OPTIMAL objective above the true minimum before this change; 0 of 174 after.

Box monotonicity over the in-repo corpus went from 1 violation in 17 comparisons to 0 in 18.

Corpus differential (79 instances, time_limit=20, oracle = minlplib.solu)

Both arms were run with the extension rebuilt and a marker assertion proving which build was loaded (144279.32 for unfixed, 0.0 for fixed) before either panel started.

	main	this PR
oracle crossings	0	0
gap_certified	62	62 — 0 regressions, 0 newly certified
objective drifts	—	0
bound drifts	—	0
status changes	—	0
node-count changes	—	11 (both directions: nvs14 223→129, ex1263 7455→10005)
total wall	356.4 s	350.7 s (−1.6%, noise)

Exactly the expected shape for a soundness fix: identical answers, a slightly different search once the invalid tightenings stop firing.

Honest blast radius. gear4 through the default solve() path is byte-identical on both arms (1.6434284641, 3 nodes, certified) and no in-repo instance crossed its oracle on either arm. Surfacing this required either the relaxation-level entry (build_milp_relaxation(...).solve()) or the mixed-scope LP engine. It also explains why the finite-root-box guard in lp_spatial_bb was load-bearing rather than conservative: it was masking this defect for the pure-integer engine, which is why removing it in #874 produced a certified optimal at 184279.32.

Tests

python/tests/test_lp_presolve_infinite_bound.py:

• the shrunk LP across a bound ladder — inf, 1e20, 1e21, 1e25, plus sub-sentinel 1e19/1e15/1e8 as over-correction guards;
• a HiGHS differential fuzz over LPs with sentinel/infinite bounds, with a comparison counter (assert compared >= 50) so a vacuous run fails instead of passing green.

Fails-before / passes-after verified by rebuilding the extension with the fix reverted: 5 failed / 3 passed before, 8 passed after.

Verification

check	result
cargo test -p discopt-core	537 passed, 0 failed (+ 4 presolve-determinism, 1 doc-test)
pytest python/tests/ -m smoke	832 passed, 1 skipped, 2 xpassed
pytest -m slow test_adversarial_recent_fixes.py	10 passed
ruff check / ruff format --check	clean
cargo fmt --check / cargo clippy	clean

Contributes to #874's blocker (that PR's false certificate on gear4 is this bug, surfaced by widening the engine's scope).

[jkitchin]

Correction to this PR's corpus-differential table — the panel was partly vacuous

Two numbers in the merged description were wrong. The fix itself, the minimal reproducer, the fuzz result and the box-monotonicity result are unaffected; this is a correction to the panel evidence, and it is the exact failure mode the companion PR #876 added a rule against, committed hours earlier.

What went wrong. The panel harness read the dual bound as result.best_bound. SolveResult has no such attribute — it is result.bound. The read was getattr(r, k, None), so every row recorded bound=None, and the derived bound_crosses_oracle check was therefore False everywhere by construction. Consequently:

• "oracle crossings: 0 / 0" was vacuous — it compared nothing;
• "bound drifts: 0" was vacuous for the same reason, and is also wrong — there are 4.

Both arms have been re-run on the corrected harness, which now prints and asserts a fired-check counter (n_checked, exiting non-zero below 20) so a run that compares nothing fails instead of passing green. Each arm asserted its build via the minimal-LP probe first (144279.32477276 for pre-#877, 0.0 for this PR).

Corrected table (79 instances, time_limit=20, oracle minlplib.solu)

	pre-#877 (7e78ec64)	this PR
bound checks that fired	76	76
oracle crossings	0	0
gap_certified	62	62 — 0 regressions, 0 new
objective drifts	—	0
bound drifts	—	4 (was reported as 0)
status changes	—	0
node-count changes	—	11

The 4 bound drifts, all sound

instance	oracle	bound pre → post	certified	objective
ex1233	155010.6713	121555.490 → 120818.798	False → False	unchanged
nvs05	5.470934108	3.805337 → 4.099238	False → False	unchanged
nvs18	−778.4	−779.398 → −780.173	False → False	unchanged
nvs20	230.9221652	227.518 → 226.097	False → False	unchanged

All MINIMIZE; every bound on both arms is verified <= oracle. Three loosen marginally and nvs05 tightens — the expected signature of no longer applying invalid presolve tightenings. All four are already-uncertified instances, objectives are identical, and no instance changes certification state. So the conclusion — cert-clean, no certification regression — stands; the change is not bound-neutral, which the original table wrongly implied.

The independent evidence for the fix is untouched and was never routed through this harness: the 1-row/2-column reproducer where presolve fabricates x0 >= 35.2244 on a column whose optimum is 0; the HiGHS differential fuzz at 11/174 → 0/174; box monotonicity 1 violation in 17 → 0 in 18; cargo test 537, smoke 832, adversarial 10; and fails-before/passes-after confirmed by rebuilding with the fix reverted.

Follow-on verification requested in review, now done

Rebasing #874 onto this fix (10 commits, clean) and re-running gear4 with solve(lp_spatial=True), with both markers asserted (the issue #860 widening present and the presolve probe returning 0.0):

	gear4 under #874
before this fix	optimal, obj = bound = 184279.32, gap_certified=True — false certificate
after this fix	time_limit, obj 17.514, bound None, gap_certified=False, 2673 nodes — sound

The false certificate is gone, confirming the diagnosis. Note for #874 separately: gear4 is still a quality regression there — main's default path certifies 1.6434284641 in 3 nodes, while the widened engine spends the full 25 s over 2673 nodes and returns an incumbent ~10x worse, uncertified. Soundness is restored; net-positive on that instance is not established.