From be4e883669e0d9a4b02bddca4d63bb9203ec72aa Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Wed, 5 Aug 2026 12:35:32 -0700 Subject: [PATCH] opt: don't stop the search on a stalled delta-rational objective (#10412) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Problem `optsmt::geometric_lex` terminates the search when `maximize_objective` returns the same blocker twice: ```cpp if (bound == last_bound) break; ``` That fixed-point test is unreliable for a **delta-rational optimum** `r + k*delta` with `k > 0`. `theory_lra::mk_ge` builds the blocker from the *rational part and a strictness flag only*: ```cpp rational r = val.get_rational(); bool is_strict = val.get_infinitesimal().is_pos(); ... b = a.mk_le(mk_obj(v), a.mk_numeral(r, is_int)); // k is discarded ``` So two consecutive stalled rounds at `r + k1*delta` and `r + k2*delta` produce the *identical* literal, the loop breaks, and the stalled value is reported as the optimum. Such a value is not a proven optimum — it only records that the arithmetic solver could not move off the bound it was just given. ## Symptom ```smt2 (declare-const a Real) (declare-const b Real) (assert (xor (= 0.0 b) (> (mod (to_int (- a)) 50) 3))) (minimize a) (check-sat) (get-objectives) ``` `a` is unbounded below — `b = 0` with `a = -50k` satisfies the constraint for every `k`. But master reports a finite value whenever the integer cut/cube heuristics run less often than the default period: ``` $ z3 lp.int_hammer_period=64 small.smt2 sat (objectives (a (+ (/ 1.0 4.0) (* (- 1.0) epsilon)))) ; wrong, should be -oo ``` ## Change When the blocker has collapsed and the objective carries a *positive* infinitesimal, force a strictly larger rational step instead of giving up. If that step is infeasible the loop still terminates normally through the `l_false` branch with the best proven bound, so the change cannot weaken a genuine optimum. ## Validation - **Unit tests**: 94/94 pass. - **New regression coverage**: `tst_scaled_min` now also runs at `lp.int_hammer_period` 16/32/64/128. It **fails on master** (`infinity coeff: 0` — a finite value for an unbounded objective) and **passes with this change**. - **Differential testing** against master on randomly generated optimization benchmarks (`-T:10`, no crashes anywhere): | corpus | files | diffs | crashes | |---|---|---|---| | linear, `int_hammer_period=4` | 3000 | 0 | 0 | | linear, `int_hammer_period=64` | 3000 | 0 | 0 | | nonlinear / `mod` / `to_int` / box+lex+pareto | 490 | 5 | 0 | All 5 differences were checked against an independent satisfiability oracle, and **master is wrong in every one**: | case | master | this PR | oracle | |---|---|---|---| | `maximize (* -5.0 x0)` | `5 + 5ε` | `25` | `= 25` sat, `> 25` unsat → **25 is optimal** | | `minimize (+ (* -3.0 x0) (* 3.0 x1))` | `237/5 - ε` | `-oo` | `< -1000000` sat → **unbounded** | | `minimize (+ (* -5.0 x2) ...)`, box | `290 - 5ε` | `321/2` | `< 170` sat → master's value unreachable | | `minimize (* 5.0 x1)` | `495/4 - 5ε` | `487/4 - 5ε` | `<= 487/4` sat → strictly better | | `minimize (+ (* -1.0 x3) (* 4.0 x3) (* 4.0 x2))` | `-4ε` | `-36` | `= -36` sat, `< -36` unsat → **-36 is optimal** | Three become exactly optimal and two strictly closer to the true optimum; no case regressed. ## Note This addresses the `optsmt` side of the fixed-point test. The underlying cause — `theory_lra::mk_ge` dropping the infinitesimal coefficient `k` when building a blocker — is the same root issue that #10269 addresses in the LRA path, and a complete fix there would make this guard redundant rather than conflict with it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/optsmt.cpp | 16 ++++++++++++++++ src/test/api.cpp | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 5a2b4457b0..82caa8fa12 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -270,6 +270,22 @@ namespace opt { // to_int, prevent the LP from seeing the full feasible region. if (m_lower[obj_index].is_finite() && m_lower[obj_index] > obj) bound = m_s->mk_ge(obj_index, m_lower[obj_index]); + if (bound == last_bound && obj.get_infinitesimal().is_pos()) { + // The objective sits infinitesimally above the strict + // bound asserted in the previous round: r + k*delta with + // k > 0. Such a value is not a proven optimum, it only + // says the arithmetic solver could not move off the + // bound it was just given. Its blocker is built from + // the rational part alone, so it collapses onto the + // previous blocker and the search would stop here and + // report the stalled value as the optimum. Force a + // strictly larger rational step instead; if the step is + // infeasible the loop terminates through the l_false + // branch below with the best proven bound. + m_s->push(); + ++num_scopes; + bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step)); + } if (bound == last_bound) break; } diff --git a/src/test/api.cpp b/src/test/api.cpp index 7b1bf1303f..e1d337cf9a 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation #include "util/util.h" #include "util/trace.h" #include +#include #include "util/trace.h" void test_apps() { @@ -423,8 +424,39 @@ void test_scaled_minimize_unbounded() { std::cout << "scaled minimize unbounded test done" << std::endl; } +// Sets a global parameter for the duration of the scope and restores the +// previous value on exit. +class scoped_global_param { + std::string m_id; + std::string m_old; + bool m_had = false; +public: + scoped_global_param(char const* id, char const* value) : m_id(id) { + Z3_string v = nullptr; + m_had = Z3_global_param_get(id, &v); + if (m_had && v) + m_old = v; + Z3_global_param_set(id, value); + } + ~scoped_global_param() { + if (m_had) + Z3_global_param_set(m_id.c_str(), m_old.c_str()); + } +}; + void tst_scaled_min() { test_scaled_minimize_unbounded(); + + // The same objectives must stay unbounded when the integer cut/cube + // heuristics run less often. At these periods the LRA optimizer stalls at + // a delta-rational value r + k*delta, whose blocker degenerates to the same + // 'objective > r' literal in consecutive rounds; the search used to stop + // there and report a finite value for an unbounded objective. + for (unsigned period : {16u, 32u, 64u, 128u}) { + std::cout << "lp.int_hammer_period=" << period << std::endl; + scoped_global_param _period("lp.int_hammer_period", std::to_string(period).c_str()); + test_scaled_minimize_unbounded(); + } } void tst_max_rev() {