From be81861e06505431574963b237d3225350ea05e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Aug 2026 12:50:38 -0700 Subject: [PATCH] Refine monomial bound optimization Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 6c23d8f6-b6fc-44f8-947f-b46d09bc36b7 --- src/math/lp/monomial_bounds.cpp | 49 ++++++++++++++++----------------- src/math/lp/monomial_bounds.h | 4 +-- 2 files changed, 25 insertions(+), 28 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index eab39c9d01..0b8f2bbbb9 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -937,7 +937,7 @@ namespace nla { } // Primal-simplex walk maximizing/minimizing 'v' (theory_arith::max_min). - void monomial_bounds::mm_optimize(lpvar v, bool maximize) { + bool monomial_bounds::mm_optimize(lpvar v, bool maximize, rational& opt_value) { auto& s = c().lra; unsigned best_efforts = 0; unsigned const max_efforts = 20; @@ -1013,9 +1013,17 @@ namespace nla { } if (!has_bound && x_i == null_lpvar && x_j == null_lpvar) - return; // objective is unbounded in the chosen direction - if (x_j == null_lpvar) - return; // optimized: no improving move remains + return false; // objective is unbounded in the chosen direction + if (x_j == null_lpvar) { + if (best_efforts == 0) { + if (s.get_column_value(v).y != 0) + return false; + opt_value = s.get_column_value(v).x; + return true; + } + + return false; // optimized: no improving move remains + } // a non-unit integral quantum means the exact optimum may not be // reachable in integral steps: count it as best-effort progress. @@ -1026,17 +1034,17 @@ namespace nla { // move x_j directly to its own bound if (inc && s.column_has_upper_bound(x_j)) { if (best.max_gain.is_zero()) - return; + return false; mm_update_value(x_j, best.max_gain); continue; } if (!inc && s.column_has_lower_bound(x_j)) { if (best.max_gain.is_zero()) - return; + return false; mm_update_value(x_j, -best.max_gain); continue; } - return; // unbounded + return false; // unbounded } // x_j can move exactly across to its opposite bound without pivoting @@ -1056,13 +1064,11 @@ namespace nla { bool inc_xi = inc ? a_ij.is_neg() : a_ij.is_pos(); mm_move_to_bound(x_i, inc_xi, best_efforts); } + return false; } - // Read the implied bound on 'v' off its final tableau row and round it to - // respect the integrality of integer columns (theory_arith::mk_bound_from_row - // + normalize_bound). Returns the joined explanation, or nullptr if no bound - // is implied (e.g. a required bound on a row variable is missing). - u_dependency* monomial_bounds::mm_bound_from_row(lpvar v, bool maximize, rational& bound) { + // Read the dependencies for the bounds on v. + u_dependency* monomial_bounds::mm_dep_from_row(lpvar v, bool maximize) { auto& s = c().lra; if (!s.is_base(v)) return nullptr; @@ -1073,7 +1079,6 @@ namespace nla { if (e.var() == v) { a_v = e.coeff(); break; } if (a_v.is_zero()) return nullptr; - lp::impq acc(0); u_dependency* dep = nullptr; for (auto const& e : row) { if (e.var() == v) @@ -1086,20 +1091,14 @@ namespace nla { if (use_upper) { if (!s.column_has_upper_bound(k)) return nullptr; - acc += s.column_upper_bound(k) * ck; dep = s.join_deps(dep, s.get_column_upper_bound_witness(k)); } else { if (!s.column_has_lower_bound(k)) return nullptr; - acc += s.column_lower_bound(k) * ck; dep = s.join_deps(dep, s.get_column_lower_bound_witness(k)); } } - if (s.column_is_int(v)) - bound = maximize ? lp::floor(acc) : lp::ceil(acc); - else - bound = acc.x; return dep; } @@ -1108,22 +1107,20 @@ namespace nla { if (!s.is_feasible()) return nullptr; bool maximize = !is_lower; - mm_optimize(j, maximize); - rational b(0); - u_dependency* dep = mm_bound_from_row(j, maximize, b); + if (!mm_optimize(j, maximize, bound)) + return nullptr; + u_dependency* dep = mm_dep_from_row(j, maximize); if (!dep) return nullptr; if (is_lower) { - if (s.column_has_lower_bound(j) && b <= s.column_lower_bound(j).x) + if (s.column_has_lower_bound(j) && bound <= s.column_lower_bound(j).x) return nullptr; } else { - if (s.column_has_upper_bound(j) && b >= s.column_upper_bound(j).x) + if (s.column_has_upper_bound(j) && bound >= s.column_upper_bound(j).x) return nullptr; } - bound = b; return dep; } } - diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index c88285ff53..fcc206efe4 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -82,8 +82,8 @@ namespace nla { bool mm_pick_var_to_leave(lpvar x_j, bool inc, rational& a_ij, mm_gain& g, lpvar& x_i) const; bool mm_move_to_bound(lpvar x_i, bool inc, unsigned& best_efforts); void mm_update_value(lpvar j, lp::impq const& delta); - void mm_optimize(lpvar v, bool maximize); - u_dependency* mm_bound_from_row(lpvar v, bool maximize, rational& bound); + bool mm_optimize(lpvar v, bool maximize, rational& opt_value); + u_dependency* mm_dep_from_row(lpvar v, bool maximize); public: monomial_bounds(core* core); void generate_lemmas();