From fdc32d0e60a625ea8c7b3fd12880a0eb7acf6a00 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 4 Jul 2026 17:28:42 -0700 Subject: [PATCH] Fix inconsistent optimization result with unvalidated LP bound (#10028) (#10040) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #10028. ## Problem Minimizing an integer variable over a problem containing a large `distinct` constraint returned an **inconsistent** result: the reported optimum did not match the returned model, and it was not the true optimum. Reproducer from the issue (a Golomb-ruler problem, true optimum = 55): ```python import z3 n, U = 10, 500 x = [z3.Int(f"x{i}") for i in range(n)] o = z3.Optimize() for xi in x: o.add(xi >= 0, xi <= U) o.add(x[0] == 0) for i in range(n - 1): o.add(x[i] < x[i + 1]) o.add(z3.Distinct([x[j] - x[i] for i in range(n) for j in range(i + 1, n)])) h = o.minimize(x[n - 1]) print(o.check(), o.lower(h), o.upper(h), o.model()[x[n - 1]]) # sat 20 20 500 <-- objective 20, but model has x9 = 500 (and 20 is unsat) ``` ## Root cause A `distinct` with more than 32 arguments is encoded with a fresh uninterpreted sort and function (`smt_internalizer.cpp`), so the objective variable becomes a *shared symbol* whose feasible values depend on EUF as well as arithmetic. The arithmetic relaxation therefore only produces a **hint** for the optimum, which may over-estimate it and be unachievable. Two combined defects: - `opt_solver::maximize_objective` committed the hint into `m_objective_values` **before** validating it with `check_bound`, and never rolled it back when validation failed. `update_objective` only ever *raises* the stored value, so the real (achievable) model value was discarded. - `optsmt::geometric_lex` **ignored** the boolean return value and asserted the blocker derived from the unachievable hint, so the very next `check_sat` was UNSAT and the search terminated prematurely, reporting the bogus bound together with a non-matching model. ## Fix - `opt_solver.cpp`: do not commit the hint before it is validated. On validation failure, `update_objective` now records the actual achievable model value. The no-model early-return 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, the condition reduces to the original expression and behavior is unchanged. After the fix the same reproducer produces consistent, monotonically-improving bounds (325 → 85 → … → 58 → … → 55), and the reported objective always matches the returned model. ## Testing Exact-optimum, fast-terminating checks (all correct): EUF-forced minimum (= 5), `distinct(x, 0..32)` minimize (= 33), Golomb n=8 (= 34), plus basic min/max, real objective, box, lex, pareto, and weighted soft/maxsat. Regression suites, rebuilt in **both Release and Debug**: | Suite | Release | Debug | |-------|---------|-------| | `test-z3 /a` | 92 passed, 0 failed | 92 passed, 0 failed | | z3test `regressions/smt2` (908 files, `model_validate=true`) | 0 failures | 0 failures | 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 586f22698b..6c71bed1af 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 f3ed1aaf91..5a2b4457b0 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));