correctness: free columns come back at the 1e20 INF sentinel, so an infeasible point is reported optimal (issue-2388.lp)

[jkitchin]

Summary

On ref/HiGHS/check/instances/issue-2388.lp the MILP driver returns
status = optimal, obj = 0.0, bound = 0.0 after 1 node — and the incumbent it
hands back is infeasible. Eight of the 42 structural entries come back
holding the INF sentinel 1e20.

The reported objective happens to equal the true optimum (HiGHS: 0.0), so
nothing downstream notices: the objective is right because those eight columns
all have zero cost, not because the point is feasible.

This is the INF-sentinel class the repo CLAUDE.md already warns about
("INF in the Rust LP layer is the sentinel 1e20, not f64::INFINITY"), but
in the solution readback rather than in FBBT.

Reproduction

import numpy as np, mloader
from discopt import _rust
from discopt.solvers.milp_simplex import _marshal_std_form

p = "ref/HiGHS/check/instances/issue-2388.lp"
d = mloader.read_arrays(p)
A_ub, b_ub, A_eq, b_eq, bounds = mloader.to_ub_eq(d)
std = _marshal_std_form(d["c"], A_ub, b_ub, A_eq, b_eq, bounds, d["integrality"])
n = len(d["c"])
st, x, obj, bd, nodes, iters = _rust.solve_milp_csc_py(
    std.c, std.m, n + std.m, std.col_ptr, std.row_idx, std.vals,
    std.b, std.lb, std.ub, std.int_cols, n, 0.0, 1_000_000, 1e-4, 1e-9,
    root_cuts=16, cut_rounds=1, cut_select=False,
    sb_max_cands=6, sb_node_budget=48, time_limit_s=15.0)
# -> optimal, obj 0.0, nodes 1, iters 12

What comes back

columns at the 1e20 sentinel: 8 of 42   (free columns in the model: 14)
  x5    x[ 6] = 1e+20   clo=-inf  chi=inf   std.lb=-1e+20 std.ub=1e+20
  x27   x[ 8] = 1e+20   ...
  x17   x[ 9] = 1e+20
  x37   x[11] = 1e+20
  x6    x[15] = 1e+20
  x28   x[17] = 1e+20
  x18   x[21] = 1e+20
  x38   x[23] = 1e+20

All eight are free columns (lb = -1e20, ub = +1e20 in standard form),
returned nonbasic at the sentinel upper bound. The other six free columns
(x31 x32 x41 x42 x43 x44) come back at sensible near-zero values, so this is
not "the whole model is unbounded" — it is specific columns parked on the
sentinel.

Why it slips the internal feasibility check

The sentinels cancel pairwise and exactly in the rows that pair them:

c1:  x5  + x11 - x27 = 0     ->  1e20 + 0 - 1e20  = 0   exactly
c41: -a x5 + a x37 + b x43 = 0  ->  same magnitude, cancels

so the residual on those rows is genuinely 0 and the point looks feasible.

The row that catches it does not pair them:

c43:  x17 - x37 >= 10.2      ->  1e20 - 1e20 = 0  <  10.2

Violated by exactly 10.2. HiGHS on the same arrays returns a point with
max |A_eq x - b_eq| = 6.6e-17 and max (A_ub x - b_ub) = 0.

Note on the reported violation magnitude

A verifier built on scipy.sparse matvec reports viol = 173.82 on row c41
for this point. That number is an artifact of the checker, not of the
solver: scipy's CSR matvec contracts to FMA, so evaluating
-a*1e20 + a*1e20 accumulates the exact second product against the
rounded first one and returns the first product's rounding residual instead
of 0. The dense dot of the identical row and vector gives exactly 0:

A_eq row 9 coefs:  x5 -0x1.dfb29f4d88341p-3,  x37 +0x1.dfb29f4d88341p-3  (exact negatives)
sparse  A_eq @ x  ->  -173.8205348
dense   row @ x   ->   0

The c43 violation of 10.2 is FMA-independent and is the real one. Any
feasibility verifier in this repo that may see sentinel-valued entries should
avoid the sparse-matvec path for the same reason.

Scope

• Found by the 46-instance MILP differential panel run for #2122 (PR fix(correctness): FBBT read a 3.2e-9 rounding residual as a proof of infeasibility #1228).
• Reproduces identically on origin/main and on the #2122 branch — it is
  pre-existing and unrelated to that fix.
• Only issue-2388 in that 46-instance panel exhibits it, but the mechanism is
  not instance-specific: any model with free columns that the simplex leaves
  nonbasic at the sentinel bound can produce the same readback.

What "done" looks like

A free column must never be returned at ±1e20. Either the simplex must not
leave a free column nonbasic at a sentinel bound, or the readback must detect
it and refuse (loudly) rather than reporting optimal — per CLAUDE.md §3, a
refusal is preferable to a silently wrong certificate. A regression test should
assert that the returned incumbent for this instance satisfies every original
row within 1e-6, checked densely (see the FMA note above).

🤖 Generated with Claude Code

https://claude.ai/code/session_0115eE146uMqL5w3mDqKgYSD