From 458a5f62af7a654cbc998e037dbeb39f13bbf204 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 4 Jul 2026 12:41:15 -0700 Subject: [PATCH] Fix inconsistent optimization result with unvalidated LP bound (#10028) When an objective shares symbols with other theories (e.g. it occurs inside the auxiliary uninterpreted function used to encode a large `distinct`), the arithmetic relaxation only yields a HINT for the optimum, which may over-estimate the true optimum and be unachievable by any model. opt_solver::maximize_objective committed this hint into m_objective_values *before* validating it with check_bound, and never rolled it back when validation failed. Meanwhile optsmt::geometric_lex ignored the boolean return value and asserted the blocker derived from the unachievable hint, terminating the search prematurely. The result was a reported optimum that neither is achievable nor matches the returned model (e.g. objective 20 with a model where x9 = 500, while the true optimum is 55). Fix: - opt_solver.cpp: do not commit the hint before it is validated. When validation fails, update_objective now records the actual (achievable) model value instead of the stale over-estimate. The no-model case keeps its previous behavior. - optsmt.cpp: geometric_lex now honors the validation result. When the hint could not be validated, it discards the poisoned blocker and tightens from the real model value, so the search keeps converging toward the true optimum. When the hint is valid, behavior is unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/opt_solver.cpp | 24 ++++++++++++++++++++---- src/opt/optsmt.cpp | 11 +++++++++-- 2 files changed, 29 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 586f22698b7..6c71bed1af4 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -319,12 +319,28 @@ namespace opt { m_models.set(i, m_last_model.get()); TRACE(opt, tout << "maximize " << i << " " << val << " " << m_objective_values[i] << " " << blocker << "\n";); - if (val > m_objective_values[i]) { - m_objective_values[i] = val; - } + // + // 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 + // 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(). + // - if (!m_last_model) + if (!m_last_model) { + // Without a model there is nothing to validate 'val' against; keep + // the previous behavior of adopting the (possibly infinite) hint. + if (val > m_objective_values[i]) + m_objective_values[i] = val; return true; + } // // retrieve value of objective from current model and update diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index f3ed1aaf91f..5a2b4457b06 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -233,7 +233,7 @@ namespace opt { if (is_sat == l_true) m_s->display(tout); ); if (is_sat == l_true) { - m_s->maximize_objective(obj_index, bound); + bool bound_valid = m_s->maximize_objective(obj_index, bound); m_s->get_model(m_model); SASSERT(m_model); inf_eps obj = m_s->saved_objective_value(obj_index); @@ -250,7 +250,14 @@ namespace opt { else { ++steps; } - if (delta_per_step > rational::one() || (obj == last_objective && is_int)) { + // When maximize_objective could not validate its arithmetic + // hint (bound_valid == false), the blocker it produced refers to + // that unachievable hint and must not be used. 'obj' now holds + // 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)) { m_s->push(); ++num_scopes; bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));