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

@@ -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;
     }
 
 }
-

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();