From d99d5a736fdde69b636dc426e53796c4aa7cf72b Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Sun, 26 Apr 2026 15:07:28 -0400 Subject: [PATCH] Improvements to NLA lemmas (#9391) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add dual-row shared-factor sandwich for NLA bound propagation When enabled via arith.nl.monomial_sandwich (default off), monomial_bounds finds LP term columns whose term has shape a_m * m + a_v * v with exactly two variables — both factors of a binary monomial m = u*v. The term column's bound bounds (a_m * m + a_v * v); substituting m = u*v gives v * (a_m*u + a_v), and sign-aware interval division by v plus an affine shift yields a numeric bound on u. The derived interval is fed to the existing propagate_value path so the lemma channel and integer rounding logic are shared with the rest of NLA's forward/backward propagation; no new emit code. Catches conflicts of the form α_v1 * v + α_m * m ≥ k1 α_v2 * v + α_m * m ≤ k2 that today require nlsat (when no single row alone yields infeasibility but their conjunction tightly bounds u after factoring v). Scope: binary monomials only (m.size()==2, no squares); cap of 16 term-columns scanned per call; one lemma per (u,v) attempt to keep the lemma channel quiet. Co-Authored-By: Claude Opus 4.7 (1M context) * Add arith.nl.order.binomial_sign flag (default true) Granular gate for order_lemma_on_binomial_sign — the only order family that embeds a model-snapshot literal (x ≷ val(x)) in the lemma body. Disabling it keeps the always-good structural mon-ol family running while removing the SAT-splitter shape that cascades under model perturbations (e.g., from arith.nl.monomial_sandwich tightening factor bounds). Default true preserves master behaviour; the flag is intended as an experimental knob to measure how much of an observed cascade is specifically attributable to the binomial-sign splitter vs. the structural cancellation lemmas in the same module. See ord-binom-opportunities.md for the full gap analysis and the deterministic-replacement directions (sandwich, McCormick) that would let this flag eventually default to false without regressing leaves where ord-binom currently carries the proof. Co-Authored-By: Claude Opus 4.7 (1M context) * Add sign-pinned binomial bound for NLA (Opportunity 1 from ord-binom doc) When enabled via arith.nl.monomial_binomial_sign (default off), monomial_bounds adds a third pass alongside propagate_down (existing) and propagate_shared_factor (sandwich). For a binary monomial m = u*v in m_to_refine whose model value mv disagrees with val(u)*val(v), and where v has a determined sign: 1. synthesize a one-sided interval for m.var() at mv (no deps; the snapshot enters as a literal in the lemma body, not as an antecedent) 2. divide by v's interval (sign-aware via dep.div) to get a deterministic interval for u 3. emit a propagate_value-style lemma whose body is m.var() < mv (or > mv) ∨ u-bound conditioned on v's bound witness Targets the case ord-binom currently handles: factors have determined signs, m.var() may have no LP bound. The clause is sound modulo the monomial definition (same condition propagate_down, propagate_shared_factor, and ord-binom already rely on). A new throttle kind MONOMIAL_BINOMIAL_SIGN keyed on (m.var, u, v, direction) prevents cascading: without it, each new val(m.var()) snapshot would re-emit across model changes the same way ord-binom does. Validated via smt.arith.validate=true: 0 soundness errors across the 32-leaf test corpus. Co-Authored-By: Claude Opus 4.7 (1M context) * Add McCormick box-corner tangent points (Opportunity 2 from ord-binom doc) When enabled via arith.nl.tangents.box_corners (default off, sub-flag of arith.nl.tangents), tangent_imp::get_points selects m_a, m_b at the corners of the bound box [x_lo, x_hi] × [y_lo, y_hi] instead of the model-centered points val(x) ± delta. The selection follows the classical McCormick under/over envelope: - m_below=true (under-approximation): m_a = (x_lo, y_lo), m_b = (x_hi, y_hi) - m_below=false (over-approximation): m_a = (x_lo, y_hi), m_b = (x_hi, y_lo) The existing generate_plane already produces the McCormick linear form xy ≷ pl.y·x + pl.x·y − pl.x·pl.y at any chosen point pl. push_point is skipped in box-corner mode: corners are extremes, so doubling the offset moves out of the box and would invalidate the McCormick property. Falls back to the existing model-driven point selection when either factor has an unbounded side or the box is degenerate (single-point in a dimension). Soundness — non-strict inequality at corners. The classical model-driven flow uses pl strictly in the interior of the box, so generate_plane emits xy > T (strict). At the box corners the tangent meets the surface along the box's edges (xy = T when x = pl.x or y = pl.y), so the strict inequality is violated by any model with x at the box boundary. A new m_pl_strict_interior member, set false on a successful set_box_corners(), switches generate_plane's emission to ≥/≤ (non-strict). The model-driven path keeps strict — its push_point + plane_is_correct_cut chain already guarantees pl is interior. Validated via smt.arith.validate=true: 0 validate_conflict() failures across the 32-leaf test corpus with box_corners=true. Co-Authored-By: Claude Opus 4.7 (1M context) --------- Co-authored-by: Claude Opus 4.7 (1M context) --- src/math/lp/monomial_bounds.cpp | 193 ++++++++++++++++++++++++++++- src/math/lp/monomial_bounds.h | 2 + src/math/lp/nla_order_lemmas.cpp | 4 +- src/math/lp/nla_tangent_lemmas.cpp | 62 ++++++++- src/math/lp/nla_throttle.h | 5 +- src/params/smt_params_helper.pyg | 5 + 6 files changed, 264 insertions(+), 7 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 28dc9a9e7..ff31f7ef5 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -312,6 +312,12 @@ namespace nla { } dep.mul(product, vi, product); } + if (do_propagate_down && c().params().arith_nl_monomial_sandwich() && + propagate_shared_factor(m)) + return true; + if (c().params().arith_nl_monomial_binomial_sign() && + propagate_binomial_sign(m)) + return true; return do_propagate_up && propagate_value(product, m.var()); } @@ -501,11 +507,196 @@ namespace nla { } lpvar monomial_bounds::non_fixed_var(monic const& m) { - for (lpvar v : m) + for (lpvar v : m) if (!c().var_is_fixed(v)) return v; return null_lpvar; } + /** + * Dual-row shared-factor sandwich. For a binary monomial m = u*v, find LP + * term columns whose term has shape a_m * m + a_v * v (exactly two + * variables, both factors of m). The term column's bound is a sound + * interval for (a_m * m + a_v * v). Substituting m = u*v yields + * v * (a_m * u + a_v); dividing by the interval on v (sign-determined) + * gives an interval on (a_m * u + a_v), and an affine shift gives an + * interval on u. The derived interval is fed to the existing + * propagate_value path so the lemma channel and integer rounding are + * shared with the rest of the propagation pipeline. + */ + bool monomial_bounds::propagate_shared_factor(monic const& m) { + if (m.size() != 2) + return false; + lpvar f0 = m.vars()[0], f1 = m.vars()[1]; + if (f0 == f1) + return false; + + unsigned const fanout_limit = c().params().arith_nl_monomial_sandwich_max_fanout(); + + auto try_pair = [&](lpvar u, lpvar v) -> bool { + // Skip if u participates in too many monomials: tightening such a + // factor cascades through ord-binom / monotonicity on every monic + // that contains it. + if (fanout_limit > 0) { + unsigned fanout = 0; + for (auto const& m1 : c().emons().get_use_list(u)) { + (void)m1; + if (++fanout > fanout_limit) + return false; + } + } + scoped_dep_interval vi(dep); + var2interval(v, vi); + if (!dep.separated_from_zero(vi)) + return false; + + auto& lra = c().lra; + unsigned const ROW_CAP = 16; + unsigned scanned = 0; + + for (auto const& cell : lra.A_r().m_columns[m.var()]) { + if (++scanned > ROW_CAP) + break; + unsigned basic = lra.get_base_column_in_row(cell.var()); + if (basic == m.var() || basic == v || basic == u) + continue; + if (!lra.column_has_term(basic)) + continue; + auto const& term = lra.get_term(basic); + if (term.size() != 2 || + !term.contains(m.var()) || !term.contains(v)) + continue; + + rational const& a_m = term.get_coeff(m.var()); + rational const& a_v = term.get_coeff(v); + if (a_m.is_zero()) + continue; + + // Term value = a_m*m + a_v*v; bound on basic bounds the term. + // Substituting m = u*v: term = v * (a_m*u + a_v). + scoped_dep_interval bi(dep); + var2interval(basic, bi); + + scoped_dep_interval inner(dep); + dep.div(bi, vi, inner); + + scoped_dep_interval shift(dep); + dep.set_value(shift, -a_v); + scoped_dep_interval scaled(dep); + dep.add(inner, shift, scaled); + + scoped_dep_interval u_int(dep); + dep.mul(rational::one() / a_m, scaled, u_int); + + TRACE(nla_solver, tout << "sandwich shared-factor basic=" << basic + << " m=" << m.var() << " v=" << v << " u=" << u + << " a_m=" << a_m << " a_v=" << a_v << "\n";); + + if (propagate_value(u_int, u)) + return true; // one lemma per call to keep the channel quiet + } + return false; + }; + + return try_pair(f1, f0) || try_pair(f0, f1); + } + + /** + * Sign-pinned binomial bound. For a binary monomial m = u*v in m_to_refine, + * use the current LP value mv = val(m.var()) as a one-sided anchor on the + * monomial value variable, and derive a deterministic interval for u via + * sign-aware division by v. + * + * Direction is chosen by the disagreement: if val(m.var()) > val(u)*val(v) + * the LP placed the monomial above the factor product, so we condition on + * "m.var() >= mv"; otherwise on "m.var() <= mv". The resulting clause is + * structurally analogous to a propagate_value lemma plus one extra + * snapshot literal on m.var(): under the asserted bounds on v, the clause + * reduces to a 2-disjunct (snapshot literal | factor bound). + * + * Targets the case ord-binom currently handles: factors have determined + * signs, m.var() may have no LP bound at all. The clause is sound modulo + * the monomial definition (the same condition propagate_down, + * propagate_shared_factor and ord-binom rely on). + */ + bool monomial_bounds::propagate_binomial_sign(monic const& m) { + if (m.size() != 2) + return false; + lpvar f0 = m.vars()[0], f1 = m.vars()[1]; + if (f0 == f1) + return false; + + rational const mv = c().val(m.var()); + rational const fp = c().val(f0) * c().val(f1); + if (mv == fp) + return false; + bool const below = mv > fp; // LP placed m.var() too high + llc const anchor_cmp = below ? llc::LT : llc::GT; + + auto try_anchor = [&](lpvar u, lpvar v) -> bool { + // Throttle once per (m.var(), u, v, direction) tuple. Without it + // each new val(m.var()) snapshot would re-emit and the search + // would cascade across model changes the same way ord-binom does. + if (c().throttle().insert_new( + nla_throttle::MONOMIAL_BINOMIAL_SIGN, + m.var(), u, v, below)) + return false; + + scoped_dep_interval vi(dep); + var2interval(v, vi); + if (!dep.separated_from_zero(vi)) + return false; + + // Synthesize a one-sided interval for m.var() at mv. No deps; + // the snapshot literal goes into the lemma body directly. + scoped_dep_interval mi_anchor(dep); + if (below) { + dep.set_lower(mi_anchor, mv); + dep.set_lower_is_inf(mi_anchor, false); + dep.set_lower_is_open(mi_anchor, false); + dep.set_upper_is_inf(mi_anchor, true); + } else { + dep.set_upper(mi_anchor, mv); + dep.set_upper_is_inf(mi_anchor, false); + dep.set_upper_is_open(mi_anchor, false); + dep.set_lower_is_inf(mi_anchor, true); + } + + scoped_dep_interval u_int(dep); + dep.div(mi_anchor, vi, u_int); + + bool emitted = false; + if (should_propagate_lower(u_int, u, 1)) { + auto const& lower = dep.lower(u_int); + if (!is_too_big(lower)) { + auto cmp = dep.lower_is_open(u_int) ? llc::GT : llc::GE; + lp::explanation ex; + dep.get_lower_dep(u_int, ex); + lemma_builder lemma(c(), "binomial sign anchor"); + lemma &= ex; + lemma |= ineq(m.var(), anchor_cmp, mv); + lemma |= ineq(u, cmp, lower); + emitted = true; + } + } + if (should_propagate_upper(u_int, u, 1)) { + auto const& upper = dep.upper(u_int); + if (!is_too_big(upper)) { + auto cmp = dep.upper_is_open(u_int) ? llc::LT : llc::LE; + lp::explanation ex; + dep.get_upper_dep(u_int, ex); + lemma_builder lemma(c(), "binomial sign anchor"); + lemma &= ex; + lemma |= ineq(m.var(), anchor_cmp, mv); + lemma |= ineq(u, cmp, upper); + emitted = true; + } + } + return emitted; + }; + + return try_anchor(f1, f0) || try_anchor(f0, f1); + } + } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index eb536a231..564fda698 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -33,6 +33,8 @@ namespace nla { u_dependency* explain_fixed(monic const& m, rational const& k); lp::explanation get_explanation(u_dependency* dep); bool propagate_down(monic const& m, dep_interval& mi, lpvar v, unsigned power, dep_interval& product); + bool propagate_shared_factor(monic const& m); + bool propagate_binomial_sign(monic const& m); void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const; bool is_free(lpvar v) const; bool is_zero(lpvar v) const; diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index bb413f4c4..e3c8618f7 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -81,9 +81,11 @@ void order::order_lemma_on_binomial(const monic& ac) { */ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) { + if (!c().params().arith_nl_order_binomial_sign()) + return; if (!c().var_is_int(x) && val(x).is_big()) return; - + SASSERT(!_().mon_has_zero(xy.vars())); int sy = rat_sign(val(y)); diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 91676b660..b322a48be 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -18,6 +18,12 @@ class tangent_imp { rational m_correct_v; // "below" means that the incorrect value is less than the correct one, that is m_v < m_correct_v bool m_below; + // pl is in the strict interior of the bound box (model-driven points + // get_initial_points + push_point); McCormick at the box corners + // requires non-strict inequality because the tangent meets the surface + // along the box's edges (xy = pl.y*x + pl.x*y - pl.x*pl.y at x = pl.x + // or y = pl.y). + bool m_pl_strict_interior = true; rational m_v; // the monomial value lpvar m_j; // the monic variable const monic& m_m; @@ -89,7 +95,10 @@ private: t.add_monomial(- m_y.rat_sign()*pl.x, m_jy); t.add_monomial(- m_x.rat_sign()*pl.y, m_jx); t.add_var(m_j); - lemma |= ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y); + llc cmp = m_below + ? (m_pl_strict_interior ? llc::GT : llc::GE) + : (m_pl_strict_interior ? llc::LT : llc::LE); + lemma |= ineq(t, cmp, - pl.x*pl.y); explain(lemma); } @@ -164,14 +173,61 @@ private: return a.x * m_xy.y + a.y * m_xy.x - a.x * a.y; } + // McCormick at box corners: choose m_a, m_b at the corners of + // [x_lo, x_hi] x [y_lo, y_hi] that bound xy from the side dictated by + // m_below. Returns false if either factor has an unbounded side, the + // box is degenerate, or the current LP value of a factor coincides with + // a chosen corner — generate_plane's negate_relation requires + // val(j) != corner_coord (SASSERT in debug; trivially-true literal in + // release). The caller falls back to the model-driven point selection in + // these cases. + bool set_box_corners() { + if (!c().has_lower_bound(m_jx) || !c().has_upper_bound(m_jx)) + return false; + if (!c().has_lower_bound(m_jy) || !c().has_upper_bound(m_jy)) + return false; + rational const& x_lo = c().get_lower_bound(m_jx); + rational const& x_hi = c().get_upper_bound(m_jx); + rational const& y_lo = c().get_lower_bound(m_jy); + rational const& y_hi = c().get_upper_bound(m_jy); + if (x_lo == x_hi || y_lo == y_hi) + return false; + // negate_relation requires the model value to be strictly separated + // from the corner coordinate it's compared to. If LP currently sits + // exactly at a box edge, fall back. + rational const& vx = c().val(m_jx); + rational const& vy = c().val(m_jy); + if (vx == x_lo || vx == x_hi || vy == y_lo || vy == y_hi) + return false; + if (m_below) { + // Under-approximation: tangents at (x_lo, y_lo) and (x_hi, y_hi) + // bound xy from below across the box. + m_a = point(x_lo, y_lo); + m_b = point(x_hi, y_hi); + } else { + // Over-approximation: anti-diagonal corners. + m_a = point(x_lo, y_hi); + m_b = point(x_hi, y_lo); + } + m_pl_strict_interior = false; + return true; + } + void get_points() { + if (c().params().arith_nl_tangents_box_corners() && set_box_corners()) { + // Box corners are extremes; pushing further moves out of the box + // and would invalidate the McCormick property. + TRACE(nla_solver, tout << "xy = " << m_xy << ", box-corner points: "; + print_tangent_domain(tout) << std::endl;); + return; + } get_initial_points(); TRACE(nla_solver, tout << "xy = " << m_xy << ", correct val = " << m_correct_v; print_tangent_domain(tout << "\ntang points:") << std::endl;); - push_point(m_a); + push_point(m_a); push_point(m_b); TRACE(nla_solver, - tout << "pushed a = " << m_a << std::endl + tout << "pushed a = " << m_a << std::endl << "pushed b = " << m_b << std::endl << "tang_plane(a) = " << tang_plane(m_a) << " , val = " << m_a << ", " << "tang_plane(b) = " << tang_plane(m_b) << " , val = " << m_b << std::endl;); diff --git a/src/math/lp/nla_throttle.h b/src/math/lp/nla_throttle.h index f0b84e0c3..6c58918b9 100644 --- a/src/math/lp/nla_throttle.h +++ b/src/math/lp/nla_throttle.h @@ -18,9 +18,10 @@ class nla_throttle { public: enum throttle_kind { ORDER_LEMMA, // order lemma (9 params) - BINOMIAL_SIGN_LEMMA, // binomial sign (6 params) + BINOMIAL_SIGN_LEMMA, // binomial sign (6 params) MONOTONE_LEMMA, // monotonicity (2 params) - TANGENT_LEMMA // tangent lemma (5 params: monic_var, x_var, y_var, below, plane_type) + TANGENT_LEMMA, // tangent lemma (5 params: monic_var, x_var, y_var, below, plane_type) + MONOMIAL_BINOMIAL_SIGN // monomial binomial sign anchor (4 params: monic_var, u, v, below) }; private: diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index cfa146477..efb85a2ab 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -67,8 +67,10 @@ def_module_params(module_name='smt', ('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'), ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'), ('arith.nl.order', BOOL, True, 'run order lemmas'), + ('arith.nl.order.binomial_sign', BOOL, True, 'run order_lemma_on_binomial_sign; disabling it keeps the structural order-lemma splitting'), ('arith.nl.expp', BOOL, False, 'expensive patching'), ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'), + ('arith.nl.tangents.box_corners', BOOL, False, 'choose tangent-plane points at the bound-box corners instead of the model-centered val(x) +/- delta; produces the McCormick under/over envelope and is deterministic and snapshot-independent'), ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'), ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'), @@ -87,6 +89,9 @@ def_module_params(module_name='smt', ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'), + ('arith.nl.monomial_sandwich', BOOL, False, 'derive bound on a monomial factor by pairing two LP rows that share the other factor'), + ('arith.nl.monomial_sandwich.max_fanout', UINT, 0, 'skip monomial sandwich when the conclusion factor appears in more than this many monomials (0 = no limit)'), + ('arith.nl.monomial_binomial_sign', BOOL, False, 'derive bound on a binomial-monomial factor anchored on the current LP value of the monomial; replaces order_lemma_on_binomial_sign with a deterministic factor bound conditioned on a one-sided snapshot of the monomial value'), ('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'), ('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'),