From 90fe0aa0f32d4cf66f3503c249d1878a39c0cf3c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Thu, 30 Jul 2026 12:45:06 -0700 Subject: [PATCH] Imp fix (#10304) For every row with only one non-fixed variable in nla_core.cpp, core::propagate, fix this variable. --------- Signed-off-by: Lev Nachmanson Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/math/lp/lar_solver.cpp | 32 ++++++++++++++++++ src/math/lp/lar_solver.h | 3 ++ src/math/lp/monomial_bounds.cpp | 56 ++++++++++++++++++++++++++++++++ src/math/lp/monomial_bounds.h | 1 + src/math/lp/nla_core.cpp | 8 +++-- src/params/smt_params_helper.pyg | 1 + 6 files changed, 99 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index a47eb6ede6..3f5bdbff46 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1150,6 +1150,38 @@ namespace lp { ex.push_back(ci); } + u_dependency* lar_solver::get_bound_constraint_witnesses_for_fixed_in_row(unsigned row_index) { + u_dependency* dep = nullptr; + for (auto const& e : get_row(row_index)) + if (column_is_fixed(e.var())) + dep = join_deps(dep, get_bound_constraint_witnesses_for_column(e.var())); + return dep; + } + + /** + \brief A row is an equality sum_j a_j x_j = 0. If every column in it is fixed + except one, that row determines the remaining column: a_k x_k = - sum_{j != k} a_j v_j. + Set j to that column and value to -(sum a_j v_j) / a_k, and return true. + */ + bool lar_solver::row_determines_column(unsigned row_index, lpvar& j, mpq& value) const { + j = null_lpvar; + mpq coeff, sum(0); + for (auto const& e : get_row(row_index)) { + if (column_is_fixed(e.var())) { + sum += e.coeff() * get_lower_bound(e.var()).x; + continue; + } + if (j != null_lpvar) + return false; + j = e.var(); + coeff = e.coeff(); + } + if (j == null_lpvar || coeff.is_zero()) + return false; + value = -sum / coeff; + return true; + } + void lar_solver::remove_fixed_vars_from_base() { // this will allow to disable and restore the tracking of the touched rows flet f(get_core_solver().m_r_solver.m_touched_rows, nullptr); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index d361496224..73ada4f1dd 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -516,6 +516,9 @@ public: return dep; } + u_dependency* get_bound_constraint_witnesses_for_fixed_in_row(unsigned row_index); + bool row_determines_column(unsigned row_index, lpvar& j, mpq& value) const; + std::ostream& print_expl(std::ostream& out, const explanation& exp) const { for (auto p : exp) constraints().display( diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index fa0c3251a4..7b685db9e8 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -677,6 +677,62 @@ namespace nla { return new_bound; } + /** + \brief Fix the columns determined by rows that are already all but fixed. + + lar_solver::row_determines_column finds a row in which every column but one + is fixed together with the value that row forces on the remaining column; + both bounds of that column are then set to it. This is constant folding + over the row, with no simplex involved. + + Only columns occurring in a monomial are considered: the point is the + effect on nonlinear reasoning, not tighter arithmetic in general. + is_linear takes a monic with at most one non-fixed factor out of nonlinear + reasoning altogether, so fixing one column can linearize every monomial it + occurs in at once. lar_solver does not derive these values on its own, + since it only analyzes rows touched by a pivot and theory_lra drops an + implied bound with no matching atom. + + Only one pass is made. A fixpoint loop would find strictly more, but this + runs on every nonlinear propagation, so a later round mostly finds what the + next call would have found anyway. Fixing every determined column measured + better than capping how many one call may fix. + */ + bool monomial_bounds::propagate_fixed_rows() { + auto& lra = c().lra; + if (!c().params().arith_nl_propagate_fixed_rows()) + return false; + + indexed_uint_set nl_vars; + for (auto const& m : c().emons()) { + nl_vars.insert(m.var()); + for (lpvar k : m.vars()) + nl_vars.insert(k); + } + + bool propagated = false; + for (unsigned i = 0; i < lra.row_count(); ++i) { + if (lra.get_row(i).size() > 32) + continue; + lpvar free_j; + rational value; + if (!lra.row_determines_column(i, free_j, value)) + continue; + if (!nl_vars.contains(free_j)) + continue; + if (lra.column_has_lower_bound(free_j) && lra.column_has_upper_bound(free_j) && + lra.get_lower_bound(free_j).x == value && lra.get_upper_bound(free_j).x == value) + continue; + u_dependency* dep = lra.get_bound_constraint_witnesses_for_fixed_in_row(i); + lra.update_column_type_and_bound(free_j, lp::lconstraint_kind::GE, value, dep); + lra.update_column_type_and_bound(free_j, lp::lconstraint_kind::LE, value, dep); + propagated = true; + } + if (propagated) + lra.find_feasible_solution(); + return propagated; + } + // ================================================================ // max_min: incremental LP bound optimization. // diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index cc9738eb07..3a27bad11a 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -89,6 +89,7 @@ namespace nla { void generate_lemmas(); bool tighten_lp_bounds(); bool propagate_changed_bounds(); + bool propagate_fixed_rows(); // Maximize (is_lower == false) or minimize (is_lower == true) column j // over the LP tableau and, if the resulting bound improves j's current diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index dcbbfdbb87..66224d24ba 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1540,8 +1540,12 @@ void core::set_use_nra_model(bool m) { bool core::propagate() { clear(); - bool propagated = m_monomial_bounds.tighten_lp_bounds(); - if (m_monomial_bounds.propagate_changed_bounds()) + bool propagated = false; + if (m_monomial_bounds.propagate_fixed_rows()) + propagated = true; + if (m_monomial_bounds.tighten_lp_bounds()) + propagated = true; + if (m_monomial_bounds.propagate_changed_bounds()) propagated = true; m_monics_with_changed_bounds.reset(); if (propagated) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 19f3e951fe..3c04bc5a43 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -101,6 +101,7 @@ def_module_params(module_name='smt', ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), + ('arith.nl.propagate_fixed_rows', BOOL, True, 'scan LP rows for fixed variables'), ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),