mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

opt: adopt exact strict supremum/infimum optima (fixes strict-optimum regression)

Browse source 
For a strict real optimum such as `maximize a` subject to `a < 0`, the
arithmetic solver returns the exact supremum `-epsilon` (a finite value with a
non-zero infinitesimal). Since #10028, opt_solver::maximize_objective defers
committing this hint to check_bound(), but check_bound() can never validate a
strict supremum: mk_ge() must drop the negative infinitesimal (the strict real
bound `a >= q - epsilon` is not expressible), so the assert+check is UNSAT and
the exact optimum is discarded in favor of the strictly smaller current model
value (e.g. -1/4 instead of -epsilon).

An earlier fix (#10052) re-committed the infinitesimal hint unconditionally and
was reverted (#10057) as unsound: for a shared-symbol objective (e.g. one whose
value depends on the auxiliary UF that encodes a `distinct` with > 32 integer
arguments) the LP relaxation only yields a hint that can strictly over-estimate
the true optimum.

This change follows the revert's prescription and gates the eager commit on a
proved-exact optimum. theory_lra now reports has_shared == false only when the
LP proved an exact OPTIMAL (integrality- and NLA-relaxed FEASIBLE hints report
has_shared == true), and opt_solver only adopts a finite strict-infinitesimal
value eagerly when that exact flag holds. This restores the strict single
objective supremum/infimum (issues #5720, discussion Z3Prover/bench#3059) while
keeping the shared-symbol hint deferred to validation, so the soundness fix of
#10028 is preserved. The eager commit is strictly narrower than the pre-#10028
behavior (it fires only for finite strict optima with a proved-exact status).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-07 01:10:06 -07:00 • committed by GitHub
parent d9d3be959c
commit cd9346d2cd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 42 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/opt/opt_solver.cpp
View file

@ -312,6 +312,16 @@ namespace opt {
inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
m_context.get_model(m_model);
inf_eps val2;
//
// 'has_shared' as returned by maximize() is false only when the
// arithmetic solver proved an *exact* optimum: a pure-LP optimum with
// no shared-symbol or integrality relaxation (theory_lra returns an
// exact optimum only for lp_status::OPTIMAL; theory_arith only when no
// shared symbols or nonlinear monomials are involved). Capture it
// before it is overwritten below; it tells us whether a strict
// supremum hint is trustworthy enough to adopt without validation.
//
bool exact_optimum = !has_shared;
has_shared = true;
TRACE(opt, tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";
if (m_model) tout << *m_model << "\n";);
@ -342,6 +352,28 @@ namespace opt {
return true;
}
//
// The arithmetic solver proved an exact optimum (exact_optimum) whose
// value is a strict supremum: a finite value carrying a non-zero
// infinitesimal, e.g. 'maximize a' subject to 'a < 0' yields -epsilon.
// Such a bound is genuinely achievable in the limit but cannot be
// re-validated by check_bound() below: mk_ge() has to drop the negative
// infinitesimal (the strict real bound 'a >= q - epsilon' is not
// expressible), so the subsequent assert+check is UNSAT and the hint
// would otherwise be discarded, leaving m_objective_values holding the
// strictly smaller current model value (regression from #10028;
// discussion Z3Prover/bench#3059). Adopt it here. This is restricted
// to proved-exact optima: for shared-symbol or relaxed hints
// (has_shared) the value may over-estimate the true optimum and is
// still deferred to validation below, so the soundness fix of #10028
// (and the revert of #10052) is preserved. update_objective() only
// ever raises the stored value, so a genuine larger model value still
// wins.
//
if (exact_optimum && val.is_finite() && !val.get_infinitesimal().is_zero() &&
val > m_objective_values[i])
m_objective_values[i] = val;
//
// retrieve value of objective from current model and update
// current optimal.

11
src/smt/theory_lra.cpp
View file

@ -4089,6 +4089,11 @@ public:
return value(v);
case lp::lp_status::FEASIBLE:
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
// FEASIBLE (as opposed to OPTIMAL) means the returned value is only
// a hint: the exact optimum could not be proved, e.g. integrality
// forced a fallback to a feasible assignment. Flag it as shared so
// the optimizer validates the bound instead of adopting it eagerly.
has_shared = true;
blocker = mk_gt(v);
return value(v);
default:
@ -4118,8 +4123,12 @@ public:
else {
st = max_with_lp(v, vi, term_max);
inf_eps nl_result;
if (max_with_nl(v, st, level, blocker, nl_result))
if (max_with_nl(v, st, level, blocker, nl_result)) {
// NLA returned a feasible hint rather than a proved optimum;
// mark it as shared so the optimizer validates it.
has_shared = true;
return nl_result;
}
}
return max_result(v, vi, st, blocker, has_shared);
}