From 1d936e2384d3bbf875ee906c64d39eb668d6b64f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 5 Jul 2026 02:31:15 -0700 Subject: [PATCH] opt: keep infinitesimal LP optimum instead of falling back to model value When an objective's optimum is an open (strict) bound, the arithmetic relaxation returns a value carrying a non-zero infinitesimal (e.g. minimizing a real x subject to x > 0, whose infimum is the unattained 0, reported as "epsilon"). opt_solver::maximize_objective validates such a hint with check_bound(), which asserts the objective is >= val via mk_ge and searches for a model reaching it. mk_ge cannot faithfully encode the infinitesimal (it drops a negative infinitesimal and turns a positive one into a strict bound), so this validation always fails spuriously for an open optimum. Since #10028 (fdc32d0e6) stopped committing the hint before validation, this false negative now discards the true infinitesimal optimum and reports an attainable - strictly worse - model value instead (x = 1 rather than epsilon). Treat a hint with a non-zero infinitesimal as valid in check_bound: for such open bounds the relaxation value is exact. Hints without an infinitesimal (such as the integer objective of #10028) are still validated normally, so that fix is preserved. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/opt_solver.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index eb8b4dd6cb..b9175d2daf 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -358,9 +358,25 @@ namespace opt { // // check that "val" obtained from optimization hint is a valid bound. + // + // A hint with a non-zero infinitesimal denotes an *open* (strict) + // optimum: the objective approaches "val" but no concrete model attains + // it (e.g. minimizing a real x subject to x > 0, whose infimum is the + // unattained 0, reported as "epsilon"). check_bound validates a hint by + // asserting the objective is >= val (mk_ge) and searching for a model + // that reaches it, but mk_ge cannot faithfully encode the infinitesimal + // (a negative infinitesimal is dropped, a positive one becomes a strict + // bound), so this search always fails spuriously for an open optimum. + // In that case the arithmetic relaxation value is exact, so accept the + // hint rather than discarding the true optimum and falling back to an + // attainable - and therefore strictly worse - model value (issue #5314). + // Hints without an infinitesimal (such as the integer objective of + // #10028) are still validated normally, preserving that fix. // auto check_bound = [&]() { SASSERT(has_shared); + if (!val.get_infinitesimal().is_zero()) + return true; return bound_value(i, val) && l_true == m_context.check(0, nullptr); };