From 6a21c160ebcb566b9b4cd8331f9932a0ad75d4a6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 5 Jul 2026 01:04:46 -0700 Subject: [PATCH] opt: fix timeout on real-valued optimization with open (strict) optima Commit fdc32d0e6 ("Fix inconsistent optimization result with unvalidated LP bound (#10028)") regressed lexicographic/single real optimization whose optimum is an open infimum/supremum (a strict inequality that no model attains). Such objectives now time out instead of reporting the correct optimum. Root cause: the #10028 fix deferred committing the LP optimization hint in opt_solver::maximize_objective until validated by check_bound(), and added a `!bound_valid` term to optsmt::geometric_lex's blocker-tightening condition. For a real objective with an open optimum, mk_ge() drops the negative infinitesimal, so check_bound() legitimately fails (the strict optimum is not attained), leaving bound_valid == false. geometric_lex then falls back to coarse model-derived +1 stepping (delta_per_step is pinned to 1 for reals) across a potentially huge range, which does not converge. The #10028 problem is integer (a Golomb-ruler encoding with a large `distinct`). Both changed behaviors only make sense for integer objectives, so gate them on `is_int`: - opt_solver::maximize_objective: commit the hint eagerly for real objectives (pre-#10028 behavior); keep the deferred, validated commit for integer objectives. - optsmt::geometric_lex: only take the model-derived tightening branch on an invalid bound when the objective is integer (`!bound_valid && is_int`). This restores the exact pre-#10028 code path for reals while leaving the integer path unchanged. Validated by rebuilding z3 and re-running inputs/issues/iss-1851/bug-1.smt2 (byte-exact match with the recorded oracle) and confirming the #10028 integer reproducer still returns a consistent true optimum. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/opt_solver.cpp | 26 +++++++++++++++++++------- src/opt/optsmt.cpp | 9 +++++++-- 2 files changed, 26 insertions(+), 9 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index eb8b4dd6cb..e22127d048 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -320,19 +320,31 @@ namespace opt { TRACE(opt, tout << "maximize " << i << " " << val << " " << m_objective_values[i] << " " << blocker << "\n";); // - // Do NOT commit 'val' to m_objective_values yet: 'val' is only an - // optimization hint from the arithmetic relaxation. When the - // objective shares symbols with other theories (e.g. it occurs inside - // an uninterpreted function such as the auxiliary function used to - // encode large 'distinct' constraints) the hint can over-estimate the - // true optimum and may not be achievable by any model. Committing it - // prematurely and then failing validation (check_bound below) would + // Do NOT commit 'val' to m_objective_values yet for INTEGER objectives: + // 'val' is only an optimization hint from the arithmetic relaxation. + // When the objective shares symbols with other theories (e.g. it occurs + // inside an uninterpreted function such as the auxiliary function used + // to encode large 'distinct' constraints) the hint can over-estimate + // the true optimum and may not be achievable by any model. Committing + // it prematurely and then failing validation (check_bound below) would // leave m_objective_values holding an unachievable bound that callers // such as optsmt::geometric_lex report as the optimum, together with a // model that does not attain it (issue #10028). The value is only // committed after it has been validated, or replaced by the value of // an actual model in update_objective(). // + // Real-valued objectives are different: their optimum can be an open + // infimum/supremum (a strict inequality) that no model attains, so the + // validation below legitimately fails even though 'val' is the correct + // optimum. Deferring the commit there would make saved_objective_value() + // report a suboptimal model value and make geometric_lex fall back to + // coarse +1 stepping over a possibly huge range (timeout). Restore the + // pre-#10028 behavior for reals by committing the hint eagerly; only + // integer objectives use the deferred, validated commit. + // + bool is_int_obj = arith_util(m).is_int(m_objective_terms.get(i)); + if (!is_int_obj && val > m_objective_values[i]) + m_objective_values[i] = val; if (!m_model) { // Without a model there is nothing to validate 'val' against; keep diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 5a2b4457b0..713696a094 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -256,8 +256,13 @@ namespace opt { // the value of an actual model, so replace the blocker with a // model-derived tightening so the search keeps making progress // toward the true optimum instead of terminating prematurely - // (issue #10028). - if (!bound_valid || delta_per_step > rational::one() || (obj == last_objective && is_int)) { + // (issue #10028). This only applies to integer objectives: for + // real objectives the optimum may be an open infimum/supremum + // that no model attains, so 'bound' correctly holds the LP + // blocker for that strict optimum and switching to coarse +1 + // stepping (delta_per_step is pinned to 1 for reals) would fail + // to converge over a large range. + if ((!bound_valid && is_int) || delta_per_step > rational::one() || (obj == last_objective && is_int)) { m_s->push(); ++num_scopes; bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));