Skip to content

fix(relaxation): #861 admit even-power monomials on a root box spanning zero - #873

Merged
jkitchin merged 4 commits into
mainfrom
claude/discopt-issue-861-oot05s
Jul 26, 2026
Merged

fix(relaxation): #861 admit even-power monomials on a root box spanning zero#873
jkitchin merged 4 commits into
mainfrom
claude/discopt-issue-861-oot05s

Conversation

@jkitchin

@jkitchin jkitchin commented Jul 26, 2026

Copy link
Copy Markdown
Owner

Summary

IncrementalMcCormickLP declined every monomial x_i**p whose root box straddled zero. A sign-mixed integer QCQP (the ball_mk2_30 class: 30 integers over [-1,1], one "thin shell" row) therefore lost the incremental structure — and with it the cuts, the feasibility pump and, under require_incremental (#858), the whole LP-per-node solve.

The issue's premise needed reframing, and the entry experiment is what did it. The issue reports that "the relaxation cannot be built" and suggests splitting the monomial's box at zero. Measuring first showed the cold build already builds a perfectly good envelope for x**2 on a straddling box; the decline lived entirely in the incremental gate. Re-probing the cold build under the flags that structure actually compares against (skip_separable_floor=True, skip_convex_lift=True):

power spanning [-2,3] positive [1,3] negative [-3,-1]
4 rows 4 4
x⁴ 4 rows 4 4
2 rows 4 4

The 2026-07-02 T1.2 probe that produced the wide gate ran without those flags; the sign-dependence it saw for /x⁴ was the extra separable-floor row s ≥ 0, which the incremental path never regenerates and never sees. Even p has f'' = p(p-1)x^(p-2) ≥ 0 on all of ℝ — one convexity, hence one envelope shape in every regime. Only an odd power is S-shaped across zero, where the cold build swaps to _emit_odd_power_hull's 2 facets: a facet-count change a fixed sparsity pattern genuinely cannot express. So the gate becomes root_sign == 0 and p odd, not root_sign == 0.

Two prerequisites had to be generalized first, both latent before this:

  • _monomial_aux_bounds assumed monotonicity (endpoint min/max). On a straddling box that floors at min(l²,u²) > 0 and cuts off the true point x=0 — unsound, unreachable only because of the gate. It now reproduces Interval.__pow__, which is where the cold build takes its aux bound. Matching rather than tightening is the point: a tighter aux bound is a different relaxation, which is precisely what this path may not be.
  • _validate's literal row-set equality could not validate a pinned box (lb==ub, reached whenever integer branching fixes a variable): the cold build emits no envelope rows at zero width while the fixed pattern must fill its four reserved rows with the tangents/secant collapsed at the pinned point. Those rows are exactly tight, so _rowset now drops rows whose maximum over the column box already satisfies them.

The falsification of the T1.2 record, the measurements, and the residuals are written up in docs/dev/certification-gap-plan.md (T1.2 section) per the house style.

Contributes to #861 — this closes the relaxation-coverage half. It does not close the issue: see Residual.

Review round 2 (@jkitchin's review of bbaf33ca)

Both blocking findings reproduced and fixed; force-pushed as 90d10e6 + 064b917d432294. 90d10e6 is bbaf33ca with only the commit message corrected (tree byte-identical, verified); 064b917 is the review response, so the delta is reviewable on its own.

Finding 2 (NaN on half-infinite boxes) — fixed. Reproduced exactly as reported: _monomial_aux_bounds(-inf, 0, 4) returned (nan, nan) on bbaf33ca, giving 2 NaNs in bounds on the sign-definite [-inf,0]/x**4 model (0 on main). The enclosure now delegates to Interval.__pow__ when an endpoint is non-finite — it can't be reproduced in closed form there, exactly as you implied: Interval outward-rounds per step, so [0,inf]**2 has lower end -5e-324, which at the next multiply gives -inf rather than a NaN-to-zero corner. Hence [0,inf]**3 = [-inf,inf], and reporting the tighter [0,inf] would have made the patched aux tighter than the cold build — the second half of your finding. Delegation costs ~65 µs vs ~2 µs, so it is confined to the non-finite case; the finite fast path measures unchanged at 1.17 µs.

Fixing only the enclosure left 4 NaNs in A.data/b from _monomial_rows (inf - inf in the tangent intercept) — you flagged that as pre-existing, and my first patch would have left a half-fix behind a test that only checked bounds. _monomial_rows now emits four vacuous rows on a non-finite box, which is exactly the cold build's polytope there (_emit_1d bails under _finite and emits nothing), so the patch now agrees with the cold build on a box where it previously disagreed. Parity with Interval.__pow__ holds on all 196 (box, p) pairs over {-inf,-3,-1,0,1,2.5,+inf}² × p ∈ 2..8: 0 mismatches, 0 NaNs.

I did not extend this to _bilinear_rows / _affine_square_rows, which have the same shape of divergence (_emit_mccormick skips a row on a non-finite endpoint). That's pre-existing and unrelated to the monomial regression — flagging rather than silently widening scope.

Finding 1 (Closes overstates it) — accepted, keyword downgraded, real instance now tested. You're right, and the reconstruction reproduces your numbers. min -Σxᵢ s.t. Σ(xᵢ² − 0.995825xᵢ) ≤ 0, xᵢ ∈ {−1,0,1}: structure admitted (ok=True, 30 monomials), bound sound, objective=None — 791 nodes / bound −27.88 at 20 s, 12236 nodes / −26.89 at 60 s, both budgets honoured. So the issue's own premise ("the primal is not the problem; admitting the model is") is falsified, and I've recorded that as a falsification in the plan doc rather than just a caveat. ClosesContributes to in the PR body and in both commit messages (a commit-message keyword would have auto-closed the issue regardless of the body).

The new tests are test_real_ball_mk2_30_relaxation_is_admitted (fails before, passes after), test_real_ball_mk2_30_bound_is_sound_and_no_false_certificate (written to keep holding if a primal fix lands), and test_real_ball_mk2_30_still_finds_no_incumbent, which pins the residual and fails loudly the day it stops being true rather than quietly locking in the bad behaviour.

Your secondary consequence — ball_mk2_30 previously declined in 0.5 s and now spends the whole fallback reserve for no primal — I've recorded rather than acted on. require_incremental's predicate ("the structure builds") is a proxy for "this path can produce a primal", and widening admission widened the gap between them; closing it is primal work (#844), not a predicate change. The core.py / lp_spatial_bb.py comments now say exactly that instead of implying the instance is fixed. Happy to take it further in this PR if you'd rather.

Finding 3 — the measured 7.1e-15 worst drop-excess is now recorded at the slack, with a note on where the relative form would first matter (a large-coefficient lift).

Nits — both if ... continue tests now assert an executed-assertion count (648 row assertions / 4 brute-forced boxes); the parity test covers half-infinite and doubly-infinite boxes and p up to 8.

Finding 4 (corpus-wide sweep) — still missing, and I can't close it here. ~/Dropbox/projects/discopt-minlp-benchmark/ is not present in this environment, so the admission blast radius beyond the 66-file in-repo corpus (where the changed class has sample size 1) remains unmeasured. Stating that plainly rather than substituting a weaker panel and calling it done.

Correctness

The change widens which models take the incremental path; it does not alter what that path computes. Soundness rests on three things:

  1. The admitted envelope is mathematically valid on the new boxes. For even p, x**p is convex on all of ℝ, so the three tangents underestimate and the secant overestimates on any finite box — the same construction already used on sign-definite boxes.
  2. The construction-time gate is unchanged in strength. _validate still requires the patched rows + aux bounds to reproduce build_milp_relaxation on six sign-diverse reachable boxes; any failure still leaves ok=False → the trusted per-node cold build.
  3. The _rowset change is a strengthening of the comparison, not a weakening. Dropping a row whose maximum over the column box already satisfies it provably leaves the feasible set unchanged, so the comparison remains an exact polytope-identity test. A row that genuinely cuts the box survives on both sides; a non-finite row maximum leaves the row in place (the conservative direction). It also closes a pre-existing blind spot: the degenerate-box case was argued sound in a comment and never validated, for sign-definite roots either.

Independently corroborated by the review's exact-rational check (944 boxes / 64,976 row assertions, 0 violations, with a firing control that produces 228 violations on the declined odd case).

  • Cannot produce a false certificate
  • No validation, fallback, or safety guard was weakened to make a check pass

Tests run (state the result — numbers, not adjectives)

  • pytest -m smoke828 passed, 16 skipped, 2 xpassed
  • pytest -m slow python/tests/test_adversarial_recent_fixes.py10 passed
  • cargo test -p discopt-core → N/A (no Rust touched)
  • ruff check python/ / ruff format --check python/ clean; mypy clean on the changed module

Plus test_861_monomial_span_zero.py 124 passed, and the incremental / spatial-deadline / root-build / cut-inherit / OBBT regression files 93 passed.

Regression test

python/tests/test_861_monomial_span_zero.py124 passed after; 19 failed against the pre-PR module (fail-before/pass-after verified by stashing only the source change). Covers the gate, Interval.__pow__ parity including infinities, the unbounded-box NaN regression end-to-end, feasible-point sampling, bound-neutrality against the same-flag cold build, the vacuous-row filter, the real ball_mk2_30, and the pinned residual.

  • Added a regression test that fails before / passes after

Bound-changing / performance change?

Not bound-changing in the §5 sense — the incremental path is contractually bound-neutral, so the bound-neutral verification regime applies rather than a default-off flag.

  • In-repo corpus panel (66 .nl; admission + root LP bound): baseline → PR gives 17 already-admitted with 0 root-bound drift, 0 regressed, 1 newly admitted (st_miqp5). st_miqp5 solves optimal, obj = bound = -333.8888902720728, gap_certified=True, node_count=1, incumbent independently feasibility-verified — identical to the pre-change result. Re-run after the review fixes: 0 further change in admission or root bounds.
  • Bound-neutrality, direct: patched LP value vs the same-flag cold build over 62 (model, box) pairs on straddling boxes — max |Δ| 3.8e-15, 0 drifts; the incremental bound never exceeded the richer cold path.
  • Differential validity: on fixed boxes the LP value never exceeded the brute-forced integer optimum; feasible-point sampling over straddling, one-sided and pinned sub-boxes found nothing cut.
  • Validation cost (the time_limit not honored: pre-B&B root setup (JAX compile + root NLP/OBBT) overruns the budget 2–13× (uninterruptible) #654 concern): the row-max is vectorized over all nonzeros at once, and the filtered _rowset is faster than the literal one (2.91 ms vs 4.46 ms on a 1080×2640 lift).

Residual

  1. ball_mk2_30 still returns no incumbent. Admission was necessary, not sufficient — the thin shell means no node LP rounds to the origin. This is primal work (the Integer / nonconvex-MINLP primal heuristics workstream (LP-based FP + sub-MIP RENS + structure-aware constructors) #844 family), which is why the issue stays open.
  2. Odd powers on a straddling root are still declined (ok=False → the trusted cold build). Closing that needs a fixed row count across the 2-facet/4-row switch, i.e. a change to the cold build's emission rather than to the patch.
  3. Corpus-wide admission sweep unmeasured (Finding 4 — the benchmark snapshot isn't available in this environment).

@jkitchin

Copy link
Copy Markdown
Owner Author

Review: SOLID WITH CAVEATS — two things to change before merge

The dangerous part of this PR is correct. The envelope is a valid outer approximation and I could not cut a feasible point. Two smaller items should be fixed first, one of which is a regression this PR introduces.


✅ Soundness verified — no feasible point is cut

The core claim held up under three independent checks:

  • Exact rational arithmetic (fractions.Fraction, no floats): 944 boxes / 64,976 row assertions, even p ∈ {2,4,6,8,10} on straddling, asymmetric ([-1,10], [-10,1], [-1e6,1]) and degenerate (lo==hi, [0,0]) boxes → 0 violations.
  • Firing control — the same checker on odd p over a straddling box (the case the gate still declines) produces 228 violations, so the probe genuinely detects an invalid envelope rather than passing vacuously.
  • Float fuzz at realistic scales, 1,120,000 row assertions → 0 violations.

The derivation matches the code: for even p, f'' = p(p-1)x^(p-2) ≥ 0 on all of ℝ, so tangents underestimate and the endpoint secant overestimates on any box. convex = (p % 2 == 0) or (li >= 0.0) correctly keeps odd-on-straddling declined.

End-to-end on assembled LPs (9 models, 144 boxes): 45,878 lifted feasible points, 709,950 row assertions → 0 cuts, 0 LP bound above a feasible objective, 0 drift vs the cold build. Control: tightening one row by 1e-3 surfaces 36 cuts, so that probe fires too.

The 602 apparent float violations on pathological boxes ([-1e6, 1e-6], p=10, values ~1e48) are catastrophic cancellation in rhs = fl - slope*li, and they occur at the same eps-normalized magnitude in the pre-existing sign-definite regime (2.6e-8 straddle vs 4.1e-8 negative). Not introduced here.


🔴 Finding 1 — Closes #861 is not accurate; the real instance still returns no incumbent

On the real minlplib/nl/ball_mk2_30.nl:

baseline (bbaf33ca^) this PR
300 s None in 0.5 s (declines) time_limit, objective=None, bound −24.896, 208,067 nodes, 300.2 s
120 s time_limit, objective=None, bound −25.892, 79,843 nodes

The structure is now admitted (ok=True, 30 monomials) and the bound is sound (≤ the 0.0 oracle) — but #861's stated symptom, "returns no incumbent", persists.

The regression test is a different model from the one in the issue:

real ball_mk2_30 :  min -Σ xᵢ        s.t. Σ(xᵢ² - 0.995825·xᵢ) ≤ 0
_ball_mk2_class  :  min Σ xᵢ²        s.t. |Σ (-1)ⁱ xᵢ| ≤ 1

The test's optimum sits at the origin and is found by the root LP — the whole 54-test file runs in 0.97 s including n=30 — so it cannot detect the real failure. This is the #727 RLT lesson CLAUDE.md cites: a mechanism validated only on a synthetic proxy can be a no-op on the real class.

Secondary consequence worth a decision: admitting this instance defeats the #858 require_incremental guard for it. It previously declined for free; it now consumes the entire fallback reserve and returns no primal — the exact "spend the budget for nothing" that guard was added to prevent. The deadline is honoured (300.2 s vs 300 s), so this is a full-budget spend, not an overrun. The comment edits in core.py / lp_spatial_bb.py note the instance "now MAPS … so it takes the incremental path" without recording that it still yields no incumbent.

Asks: Closes #861Contributes to #861; regression test to exercise the real instance (or a faithful reconstruction).


🔴 Finding 2 — _monomial_aux_bounds returns (nan, nan) on half-infinite boxes (regression)

python/discopt/_jax/incremental_mccormick.py:168-174. The new repeated-interval-multiplication form hits inf * 0 = nan, and min/max propagate it. Reproduced directly against main:

box (-inf, 0.0):
  p=3   PR=(nan, nan)   main=(-inf, 0.0)
  p=4   PR=(nan, nan)   main=( 0.0, inf)
  p=5   PR=(nan, nan)   main=(-inf, 0.0)
  p=6   PR=(nan, nan)   main=( 0.0, inf)

This is not confined to the newly-admitted class. A model with x ∈ [-inf, 0] carrying x**4 has root_sign = -1 — sign-definite, admitted before and after this PR. The structure validates ok=True (all six validation boxes are finite, so the gate never sees it) and the root assemble() then produces 2 NaNs in bounds, with solve_assembled → nan. Baseline on the identical model: 0 NaNs.

Mitigating: _monomial_rows already emitted NaN into A.data/b on that box pre-PR, the end-to-end solve returns None either way, and 0/18 admitted in-repo instances trigger it. So it is a latent hazard made strictly worse rather than a live false certificate — but a NaN bound entering B&B (where nan <= incumbent is always False) shouldn't ship knowingly.

It also contradicts the PR's own stated invariant: _monomial_aux_bounds(0.0, inf, p>=3) returns (0, inf) while Interval.__pow__ returns (-inf, inf) — i.e. the patched aux is tighter than the cold build, which the new docstring explicitly forbids. test_monomial_aux_bounds_match_interval_pow uses only finite boxes, so it sees neither case.

Ask: guard the p >= 3 loop on non-finite endpoints (delegate to Interval.__pow__, or return (-inf, inf)), and add half-infinite boxes to the parity test. Note this PR's own _rowset explicitly guards 0 * inf -> nan — the hazard was recognised in one place and missed in the other.


🟡 Finding 3 — Ap.shape != Af.shape gate weakening: defensible, and measured

_validate now compares only shape[1], with identity decided by vacuity-filtered row sets. Over 22 admitted models × 132 validation boxes:

  • 5 boxes hit a row-count difference (the old check would have declined). All 5 are the degen (pinned) trial — st_miqp5 21 vs 17, synthetic_p{2,4,6} 13 vs 1, ball_mk2_30 121 vs 1. Narrowly targeted, exactly as documented.
  • 799 patch-side / 639 cold-side rows dropped as vacuous; worst amount by which a dropped row actually cuts: 7.1e-15. The 1e-9 relative slack is not being exercised.

The polytope-identity argument is right (a row implied by the enforced column box is redundant, so dropping it from both sides preserves P ∩ box). Residual concern: a hard structural invariant became a relative-tolerance numeric test — slack = 1e-9*(1+|b|+|row_max|) would tolerate a genuinely-cutting row of ~1 unit on a row whose max is 1e9. Nothing in the corpus exercises that today.

Counter-evidence: on 920 random node boxes the gate never sees (23 models incl. real ball_mk2_30 with 30 straddling monomials), 318 comparable LP pairs → 0 value drifts, 0 patched bounds above cold.

Suggest recording the measured 7.1e-15 worst drop-excess in a comment so a future regression in that margin is visible.


🟡 Finding 4 — §5 regime and panel scope

Self-classifying as bound-neutral (regime 1, no feature flag) looks right: the envelope formula is unchanged; what widens is which models take the fast path, and that path is contractually required to reproduce the cold build. I reproduced the required evidence on the 66-file in-repo corpus:

admitted  base=17  pr=18   |  admitted in BOTH: 17
REGRESSED to declined:  0
NEWLY admitted:         1   -> st_miqp5.nl
ROOT-BOUND DRIFTS among both-admitted: 0

st_miqp5 then solves optimal, obj = bound = -333.8888902488093, gap_certified=True, incumbent independently feasible (0 violations), matching the MINLPLib reference −333.88889 to 1.4e-6.

Caveat: that panel is the in-repo corpus only, and the changed class has sample size n=1 there. Since the change widens admission, the corpus-wide blast radius is unmeasured — CLAUDE.md points at ~/Dropbox/projects/discopt-minlp-benchmark/ for exactly this case. A sweep for even-power monomials on straddling roots over the ~1,610-instance snapshot was started but didn't finish under load; that evidence is still missing.


Nits

  • test_spanning_monomial_envelope_cuts_no_feasible_point and test_spanning_monomial_bound_never_exceeds_the_box_optimum contain if bound is None: continue / if true is not None: paths with no executed-assertion counter — they can silently degrade to no-ops. The sibling bound-neutrality test does guard (assert compared >= 5); worth the same pattern.
  • _monomial_aux_bounds's "reproduces Interval.__pow__ exactly" is false on half-infinite boxes (Finding 2).
  • No new swallowed exceptions in the diff; the constructor's except Exception logs at DEBUG with a reason. Good.

Tests / CI

check result
pytest -m smoke 832 passed, 1 skipped, 2 xpassed, 0 failed
pytest -m slow test_adversarial_recent_fixes.py 10 passed
test_861_monomial_span_zero.py 54 passed; 19 failed / 35 passed against the pre-PR module — fails-before/passes-after verified
gh pr checks 873 all green, mergeStateStatus: CLEAN

Two caveats on methodology, for the record: an initial pytest run silently imported discopt from the main tree rather than the worktree and reported 19 bogus failures — every number above is from runs that asserted incremental_mccormick.__file__ resolves to the worktree. And machine load ranged 3.7–6.7 throughout, so nothing here rests on wall-clock; all of it is pass/fail, counts, and bound values.


Bottom line

The relaxation-envelope surface — the thing that made this risky — is fine, verified in exact arithmetic with a firing control. Change the two items above (issue-closing keyword + real-instance test; the non-finite guard) and this is good to merge.

claude added 2 commits July 26, 2026 17:03
…ng zero

`IncrementalMcCormickLP` declined EVERY monomial `x_i**p` whose root box
straddled zero, so a sign-mixed integer QCQP (the ball_mk2_30 class: 30
integers over [-1,1], one "thin shell" row) lost the incremental structure —
and with it the cuts, the feasibility pump and, under `require_incremental`
(#858), the whole LP-per-node solve, which returned no incumbent at all.

The gate was wider than the mathematics. Re-probing the cold build under the
flags the structure actually compares against (`skip_separable_floor`,
`skip_convex_lift`) gives the same 4-row secant/tangent envelope in EVERY sign
regime for even powers, and only 2 facets vs 4 for odd ones:

    x^2  spanning [-2,3] -> 4 rows   [1,3] -> 4   [-3,-1] -> 4
    x^4  spanning [-2,3] -> 4 rows   [1,3] -> 4   [-3,-1] -> 4
    x^3  spanning [-2,3] -> 2 rows   [1,3] -> 4   [-3,-1] -> 4

The 2026-07-02 T1.2 probe that produced the wide gate was run WITHOUT those
flags; the sign-dependence it saw for x^2/x^4 was the extra separable-floor row
`s >= 0`, which the incremental path never regenerates and never sees. Even p
has f'' = p(p-1)x^(p-2) >= 0 on all of R, hence one convexity and one envelope
shape; only an odd power is S-shaped across zero. Gate is now
`root_sign == 0 and p odd`.

Two prerequisites, both latent before this:

* `_monomial_aux_bounds` assumed monotonicity (endpoint min/max). On a
  straddling box that floors x^2 at min(l^2,u^2) > 0 and cuts off the true
  point x=0 — unsound, unreachable only because of the gate. It now reproduces
  `Interval.__pow__`, which is where the cold build gets its aux bound;
  matching (not tightening) is what keeps the path bound-neutral.
* `_validate`'s literal row-set equality could not validate a PINNED box
  (lb==ub, reached whenever integer branching fixes a variable): the cold build
  emits no envelope rows at zero width while the fixed pattern must fill its
  four reserved rows with the tangents/secant collapsed at the pinned point.
  Those rows are exactly tight, so `_rowset` now drops rows whose maximum over
  the column box already satisfies them. Dropping a row that cannot cut the box
  provably leaves the polytope unchanged, so the gate stays an exact
  polytope-identity test; it also closes a case that was previously argued
  sound in a comment and never actually exercised.

Verification (measurements, not adjectives):
* In-repo corpus panel (66 .nl, admission + root LP bound, OFF vs ON): 17
  already-admitted instances, 0 root-bound drift, 0 regressed to declined, 1
  newly admitted (st_miqp5) — which solves to -333.8888902720728,
  gap_certified=True, node_count=1, incumbent independently feasibility-
  verified, identical to the pre-change result.
* Bound-neutrality: patched LP value vs same-flag cold build over 62
  (model, box) pairs on straddling boxes — max |delta| 3.8e-15, 0 drifts; the
  incremental bound never exceeded the richer cold path.
* Feasible-point sampling on straddling/pinned sub-boxes: no envelope row and
  no aux bound cuts any (x, x**p).

Contributes to #861 — this closes the relaxation-coverage half. See the
follow-up commit for what the real instance shows still remains.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LMD1yUbtiLykRpmxzGigZk
…l-instance test

Addresses the review on PR #873. Three code changes plus an honest re-scoping of
what #861 does and does not close.

1. NON-FINITE BOXES PUT NaN IN THE NODE LP (regression introduced by the parent
   commit, plus a pre-existing sibling).

   `_monomial_aux_bounds`'s repeated-multiplication form hit `0 * ±inf = nan` and
   `min`/`max` propagated it, so an unbounded box returned `(nan, nan)`:

       box (-inf, 0.0):  p=3 -> (nan,nan)   p=4 -> (nan,nan)   p=5/6 -> (nan,nan)

   This is NOT confined to the newly-admitted class. A variable with `lb=-inf,
   ub=0` carrying `x**4` has `root_sign = -1` — sign-definite, admitted before AND
   after #861 — and all six validation boxes are finite, so the gate never sees it.
   Reproduced end-to-end on the parent commit: 2 NaNs in `bounds`, 0 on main.
   NaN in an LP is worse than a loose bound: every comparison against it is False,
   so `nan <= incumbent` can silently disable fathoming.

   The enclosure now delegates to `Interval.__pow__` when an endpoint is
   non-finite. It cannot be reproduced in closed form there: `Interval`
   outward-rounds after every step, so `[0,inf]**2` has lower end `-5e-324`, which
   at the next multiply gives `-inf` rather than a NaN-to-zero corner — hence
   `[0,inf]**3 = [-inf,inf]`, not `[0,inf]`. Claiming the tighter one would make
   the patched aux TIGHTER than the cold build, which this function's contract
   forbids. Delegation costs ~65us vs ~2us, so it is confined to the non-finite
   case; the finite fast path is unchanged (1.17us measured).

   Fixing only the enclosure left 4 NaNs in `A.data`/`b` from `_monomial_rows`
   (`inf - inf` in the tangent intercept). That path is latent on main too. It now
   emits four VACUOUS rows on a non-finite box, which is exactly the cold build's
   polytope there — `_emit_1d` bails under `_finite` and emits no rows at all — so
   this moves the patch toward the cold build on a box where it disagreed.

   Parity with `Interval.__pow__` now holds on all 196 (box, p) pairs over
   {-inf,-3,-1,0,1,2.5,+inf}^2 x p in 2..8: 0 mismatches, 0 NaNs.

2. Issue-closing keyword downgraded to "Contributes to", and a regression test on the REAL
   instance rather than only the synthetic class probe.

   On a faithful reconstruction of MINLPLib ball_mk2_30
   (`min -sum x_i  s.t.  sum(x_i^2 - 0.995825 x_i) <= 0`, `x_i` integer in [-1,1]),
   the structure IS now admitted (ok=True, 30 monomials) and the bound is sound —
   but the instance still returns NO incumbent: `objective=None`, bound -27.88 at a
   20 s budget (791 nodes) and -26.89 at 60 s (12236 nodes), both budgets honoured.

   So the issue's premise "the primal is not the problem; admitting the model is"
   is falsified: the thin shell means no node LP rounds to the origin. #861's
   relaxation-coverage half is closed; its stated symptom is not. The prior test
   model could not detect this — its optimum sits at the origin and the root LP
   finds it — which is the #727 lesson in CLAUDE.md about synthetic proxies.

   Side effect recorded, not silently accepted: ball_mk2_30 previously declined in
   0.5 s under `require_incremental` (#858) and now spends the whole fallback
   reserve for no primal. The guard's predicate ("the structure builds") is a proxy
   for "this path can produce a primal", and widening admission widened the gap.
   The comments in `core.py` / `lp_spatial_bb.py` now say so instead of implying
   the instance is fixed.

3. Review nits.
   * The measured worst drop-excess of the `_rowset` vacuity filter (7.1e-15, ~6
     orders below the 1e-9 relative slack) is recorded at the slack, so a future
     regression in that margin is visible.
   * The two tests with `if ... continue` paths now assert an executed-assertion
     count (648 row assertions / 4 brute-forced boxes) so they cannot silently
     degrade to no-ops.
   * The parity test covers half-infinite and doubly-infinite boxes and p up to 8.

Verification: corpus panel re-run — vs the parent commit, 0 change in admission
and 0 root-bound drift (still 17 both-admitted + st_miqp5 newly admitted vs
baseline). `pytest -m smoke` 828 passed / 16 skipped / 2 xpassed. Adversarial
suite 10 passed. `test_861_monomial_span_zero.py` 124 passed. Incremental /
spatial / OBBT regression files 93 passed. ruff + mypy clean.

Not done, and not claimed: the corpus-wide sweep over the ~4800-instance MINLPLib
snapshot. `~/Dropbox/projects/discopt-minlp-benchmark/` is not present in this
environment, so the admission blast radius beyond the 66-file in-repo corpus
(where the changed class has sample size 1) remains unmeasured.

Contributes to #861

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LMD1yUbtiLykRpmxzGigZk
@jkitchin
jkitchin force-pushed the claude/discopt-issue-861-oot05s branch from bbaf33c to d432294 Compare July 26, 2026 17:04

Copy link
Copy Markdown
Owner Author

Thanks — both blocking findings reproduced and fixed. Force-pushed bbaf33cad432294 as two commits: 90d10e6 is the original with only the commit message corrected (tree byte-identical, verified), 064b917 is the review response, so the delta reviews on its own. PR body updated in full.

Finding 2 — fixed, and it was bigger than the aux bound

Reproduced exactly: _monomial_aux_bounds(-inf, 0, 4)(nan, nan) on bbaf33ca, 2 NaNs in bounds on the sign-definite [-inf,0]/x**4 model, 0 on main.

The enclosure now delegates to Interval.__pow__ on a non-finite endpoint. Your second observation — that the patched aux was tighter than the cold build on [0,inf] — is what makes delegation the only correct option rather than a NaN guard: Interval outward-rounds after every step, so [0,inf]**2 has lower end -5e-324, which at the next multiply gives -inf instead of a NaN-to-zero corner. [0,inf]**3 is genuinely [-inf,inf]. I tried the NaN→0 convention alone first and it still diverged on 26 of 196 (box, p) pairs; only delegation reproduces it. Cost is ~65 µs vs ~2 µs, so it's gated on non-finite — the finite fast path measures unchanged at 1.17 µs.

Fixing the enclosure alone left 4 NaNs in A.data/b from _monomial_rows — you'd noted that as pre-existing, and my test would have passed while asserting only on bounds, which is exactly the kind of half-fix worth catching. _monomial_rows now emits four vacuous rows on a non-finite box; that is precisely the cold build's polytope there (_emit_1d bails under _finite and emits nothing), so the patch now agrees with the cold build on a box where it previously disagreed. Parity now holds on all 196 pairs over {-inf,-3,-1,0,1,2.5,+inf}² × p ∈ 2..8: 0 mismatches, 0 NaNs. The end-to-end test asserts on the whole assembled LP, not just the aux bounds.

I did not extend this to _bilinear_rows / _affine_square_rows, which have the same divergence shape (_emit_mccormick skips a row on a non-finite endpoint, the patch doesn't). Pre-existing and unrelated to the regression I introduced — flagging rather than widening scope unasked.

Finding 1 — accepted; you're right and the premise is falsified

The reconstruction reproduces your numbers. min -Σxᵢ s.t. Σ(xᵢ² − 0.995825xᵢ) ≤ 0, xᵢ ∈ {−1,0,1}: admitted (ok=True, 30 monomials), bound sound, objective=None — 791 nodes / bound −27.88 at 20 s, 12236 nodes / −26.89 at 60 s, both budgets honoured.

So #861's own premise — "the primal is not the problem; admitting the model is" — is falsified, and I've recorded it as a falsification in the plan doc rather than as a caveat. Keyword downgraded in the PR body and in both commit messages; a commit-message Closes would have auto-closed the issue on merge regardless of the body, which is worth noting for anyone hitting this later.

Three new tests: admission on the real instance (fails before, passes after), a bound-soundness test written so it keeps holding if a primal fix lands, and test_real_ball_mk2_30_still_finds_no_incumbent, which pins the residual and fails loudly the day it stops being true rather than freezing the bad behaviour into an assertion.

Your point that _ball_mk2_class can't detect the real failure is the important one and I've written the why into the fixture docstring: its optimum sits at the origin and the root LP finds it, so the whole file ran in 0.97 s and looked green. That's the #727 lesson landing on me directly.

The secondary consequence — recorded, not acted on

ball_mk2_30 previously declined in 0.5 s and now spends the entire fallback reserve for no primal. require_incremental's predicate ("the structure builds") is a proxy for "this path can produce a primal", and widening admission widened the gap between them. Closing that is primal work (#844), not a predicate change — so the core.py / lp_spatial_bb.py comments now state the trade explicitly instead of implying the instance is fixed. If you'd rather I tighten the guard in this PR, say so and I'll take it — I left it because it's a policy change to the fallback rather than a fix to what I broke.

Findings 3 & nits

7.1e-15 worst drop-excess recorded at the slack, with a note that the relative form is where a large-coefficient lift would first bite. Both if ... continue tests now assert an executed-assertion count (648 row assertions / 4 brute-forced boxes). Parity test extended to half-infinite and doubly-infinite boxes and p up to 8.

Finding 4 — still open, and I can't close it here

~/Dropbox/projects/discopt-minlp-benchmark/ isn't present in this environment, so the corpus-wide admission sweep remains unmeasured and the changed class still has sample size 1 in the in-repo panel. Saying that plainly rather than substituting a weaker panel and calling it done — it's listed as residual #3.

Re-verified after the fixes

check result
corpus panel, pre-review PR → post-review PR 0 change in admission, 0 root-bound drift
corpus panel, baseline → post-review PR 17 both-admitted, 0 drift, 0 regressed, 1 newly admitted (st_miqp5)
pytest -m smoke 828 passed, 16 skipped, 2 xpassed
pytest -m slow test_adversarial_recent_fixes.py 10 passed
test_861_monomial_span_zero.py 124 passed
incremental / spatial-deadline / root-build / cut-inherit / OBBT 93 passed
ruff + mypy clean

Also — thank you for flagging the import-path methodology trap. Every number here is from the same venv the module is installed into editable; I re-checked incremental_mccormick.__file__ after the force-push rewrite specifically because of that note.


Generated by Claude Code

claude added 2 commits July 26, 2026 18:13
Follow-up to the #873 review's "secondary consequence": since #861 admits
ball_mk2_30 into the LP-per-node engine, `Model.solve`'s no-incumbent fallback
runs it instead of declining under `require_incremental`, spends the whole
reserve, and finds no primal.

The obvious response — re-tighten the guard to exclude it again — is REJECTED,
on evidence, twice over.

1. No predicate can decide this in advance. The guard would have to answer "will
   a primal appear within the reserve". The same panel that shows ball_mk2_30
   (n=30) finding nothing shows ball_mk2_20 finding the exact optimum -0.0 —
   same family, same thin shell, opposite outcome. A "give up if no incumbent by
   X% of the reserve" rule would forfeit exactly the late incumbents this
   fallback exists to catch (tln4/tln5), and tuning X until ball_mk2_30 exits
   early is a single-instance fix, which CLAUDE.md §2 rejects.

2. The reserve was not producing nothing. It was producing something that got
   thrown away. The fallback merged its result into `result` only when that
   result carried an objective, so a sound dual bound computed inside the
   reserve was discarded along with it. Measured at a 30 s budget: the fallback
   proved `bound = -27.88` (<= the 0.0 oracle) while the solve reported
   `bound=None`.

So the bound merge now runs whether or not a primal was found. Soundness rests
on the same argument the merge already relied on: `_is_in_scope` admits only
MINIMIZE, both values are valid LOWER bounds, and the max of two valid lower
bounds is valid. No certificate is claimed without an incumbent — `status`,
`gap` and `gap_certified` still move only on the primal path, so a bound-only
merge cannot manufacture `gap_certified=True`.

Bound-changing, so it gets the differential treatment. Panel over the 12
fallback-reachable in-repo instances (nvs03/07/10/11/12/13/15, st_miqp1/2/3,
st_test1, st_testgr3) plus ball_mk2_{20,30}, `solve(time_limit=20)` before vs
after:

  identical (status, objective, bound, gap_certified):  13 / 14
  changed:                                               1  -> ball_mk2_30
                                                            bound None -> -27.883586
  certification regressions:                             0
  objective drift:                                       0
  bounds above their incumbent:                          0
  bounds above a known oracle:                           0
  bounds loosened:                                       0

Every certified instance keeps `bound == objective` and `gap_certified=True`;
the single change is a sound bound appearing where there was none.

Regression test `test_no_incumbent_fallback_still_reports_its_dual_bound`
asserts properties, not values (the bound tightens with the budget): a bound
exists, it never crosses the 0.0 oracle, and no certificate is claimed without
an incumbent. Fails before this change (`assert None is not None`), passes
after.

Verification: pytest -m smoke 828 passed / 16 skipped / 2 xpassed; adversarial
suite 10 passed; test_861_monomial_span_zero.py 126 passed; #844 fallback +
incremental + root-build regressions 22 passed; ruff + mypy clean.

Contributes to #861

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LMD1yUbtiLykRpmxzGigZk

Copy link
Copy Markdown
Owner Author

Took your "secondary consequence" item. Pushed d172ffa. I did not tighten the guard — I think that would have been the wrong fix, and measuring turned up a better one.

Why not tighten require_incremental

Two reasons, both from measurement rather than taste.

No predicate can decide this in advance. The guard would have to answer "will a primal appear within the reserve". In the panel below, ball_mk2_30 finds nothing — and ball_mk2_20, same family, same thin shell, finds the exact optimum -0.0. A "give up if no incumbent by X% of the reserve" rule would forfeit precisely the late incumbents this fallback exists to catch (tln4/tln5 are found deep in the reserve, not early), and tuning X until ball_mk2_30 exits early is a single-instance fix.

The reserve wasn't producing nothing — it was producing something that got thrown away. This is the part I'd missed and your framing led me to. Model.solve's fallback merges the engine's result only when it carries an objective, so the dual bound computed inside the reserve was discarded along with it:

Model.solve(time_limit=30):        status=time_limit  objective=None  bound=None
the fallback it just ran:          objective=None     bound=-27.88358602833255   (<= the 0.0 oracle)

So "spends the budget for nothing" was literally true, but the cause was reporting, not admission. The bound merge now runs whether or not a primal was found.

Soundness

Same argument the merge already relied on, just no longer conditioned on an incumbent it doesn't depend on: _is_in_scope admits only MINIMIZE, both values are valid lower bounds, and the max of two valid lower bounds is valid. status, gap and gap_certified still move only on the primal path, so a bound-only merge cannot manufacture gap_certified=True — verified explicitly on ball_mk2_30 (bound=-27.88, objective=None, gap_certified=False).

Bound-changing, so it gets the differential treatment. Panel over the 12 fallback-reachable in-repo instances (nvs03/07/10/11/12/13/15, st_miqp1/2/3, st_test1, st_testgr3) plus ball_mk2_{20,30}, solve(time_limit=20), before vs after:

identical (status, objective, bound, gap_certified) 13 / 14
changed 1ball_mk2_30, bound: None → -27.883586
certification regressions 0
objective drift 0
bounds above their incumbent 0
bounds above a known oracle 0
bounds loosened 0

Every certified instance keeps bound == objective and gap_certified=True. The single change is a sound bound appearing where there was none.

Test

test_no_incumbent_fallback_still_reports_its_dual_bound asserts properties rather than values, since the bound tightens with the budget: a bound exists, it never crosses the 0.0 oracle, and no certificate is claimed without an incumbent. Fails before (assert None is not None), passes after.

pytest -m smoke 828 passed / 16 skipped / 2 xpassed; adversarial 10 passed; test_861_monomial_span_zero.py 126 passed; #844 fallback + incremental + root-build regressions 22 passed; ruff + mypy clean.

Scope note

This touches core.py solve orchestration rather than the relaxation, so it's arguably a second topic in a one-topic PR. I put it here because it's a direct consequence of this PR's admission change and you raised it on this PR — but if you'd rather keep #873 to the monomial gate, say the word and I'll pull d172ffa onto its own branch and PR it separately. Residual #1 (ball_mk2_30 still finds no incumbent) is unchanged either way; that's still #844 primal work.


Generated by Claude Code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants