diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 23260bbf65..f0d6085de6 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -244,15 +244,19 @@ namespace nla { return false; lpvar w, fixed_to_zero; - if (!is_linear(m, w, fixed_to_zero)) + if (!is_linear(m, w, fixed_to_zero)) return false; c().emons().set_propagated(m); + return linearize(m, w, fixed_to_zero); + } + + bool monomial_bounds::linearize(monic const& m, lpvar w, lpvar fixed_to_zero) { bool propagated = false; if (fixed_to_zero != null_lpvar) { propagated = propagate_fixed_to_zero(m, fixed_to_zero); - } + } else { rational k = fixed_var_product(m, w); if (w == null_lpvar) @@ -265,6 +269,67 @@ namespace nla { return propagated; } + /** + \brief Linearize the violated monomials that have at most one non-fixed + factor, ignoring the is_propagated latch. + + propagate_linear_bound sees a linear monomial once: it records the + defining relation and retires the monomial via set_propagated. When that + relation happens to be satisfied by the model of the moment, + propagate_nonfixed skips adding the defining row, so the relation is + recorded nowhere; as soon as the model moves, the monomial is violated + again and the only handles left are a case split (refine_pseudo_linear) + or a horner/grobner round per final check. + + This pass runs from core::propagate(), which theory_lra invokes on entry + to every final check, so the repaired LP is re-solved and the surviving + violations still get their regular horner/grobner round. Only monomials + the current model violates are linearized: the guards of propagate_fixed + / propagate_nonfixed cannot dismiss such a row as redundant, and every + row added repairs an actual violation. Recording the row unconditionally + instead (even when the model satisfies it) was measured to lose over 500 + QF_NIA instances: there factors are fixed by branching, and the rows, + re-added on every branch, grow the tableau for no benefit. Restricting + the pass to violated monomials keeps the wins without that regression. + */ + bool monomial_bounds::propagate_violated_linear_monomials() { + if (!c().lra.is_feasible()) + return false; + bool propagated = false; + for (auto const& m : c().emons()) { + if (c().check_monic(m)) + continue; + lpvar w, fixed_to_zero; + if (!is_linear(m, w, fixed_to_zero)) + continue; + // The pass pays off when the factors are fixed for good (bound + // propagation from structural facts, e.g. pow2 constants in F* + // queries): the same defining row then repairs the violation for + // the rest of the search. When the factors are fixed by branching + // instead, each branch re-fixes them to another small value, and + // the rows, popped by the next backjump, only perturb the search + // (installing m = 3*w rows at deep decision levels was measured to + // turn a 0.1s F* query into a timeout). A small fixed-factor + // product is the signature of enumeration, so the row-installing + // path is reserved for products too wide to be branch-enumerated. + // The row-free paths (m fixed to a constant) are plain bound + // updates and stay ungated. + if (fixed_to_zero == null_lpvar && w != null_lpvar) { + rational k = fixed_var_product(m, w); + if (k.is_int() && k.bitsize() <= 16) + continue; + } + if (linearize(m, w, fixed_to_zero)) { + propagated = true; + TRACE(nla_solver, tout << "linearized violated monomial " << m + << ", scope " << c().lra.get_scope_level() << "\n";); + } + if (c().lra.get_status() == lp::lp_status::INFEASIBLE) + break; + } + return propagated; + } + lp::explanation monomial_bounds::get_explanation(u_dependency* dep) { lp::explanation exp; svector cs; diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index a433073df8..86c0a2ec47 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -50,9 +50,11 @@ namespace nla { // when all but one variable of a monomial are fixed, the monomial is // linear and its value/equality can be propagated into the LP solver. bool propagate_linear_bound(monic & m); + bool linearize(monic const& m, lpvar w, lpvar fixed_to_zero); bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero); rational fixed_var_product(monic const& m, lpvar w); + // ---------------------------------------------------------------- // max_min: incremental LP bound optimization. // @@ -91,6 +93,7 @@ namespace nla { bool tighten_lp_bounds(); bool propagate_linear_bounds(); bool propagate_changed_bounds(); + bool propagate_violated_linear_monomials(); bool propagate_fixed_rows(); bool optimize_nl_bounds(); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 855fa65d52..606155e24a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1545,7 +1545,10 @@ bool core::propagate() { propagated = true; if (m_monomial_bounds.tighten_lp_bounds()) propagated = true; - if (m_monomial_bounds.propagate_changed_bounds()) + if (m_monomial_bounds.propagate_changed_bounds()) + propagated = true; + if (params().arith_nl_linearize_violated_monomials() && + m_monomial_bounds.propagate_violated_linear_monomials()) 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 5f65fa6ce2..643b5e9e26 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -100,6 +100,7 @@ def_module_params(module_name='smt', ('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'), + ('arith.nl.linearize_violated_monomials', BOOL, True, 'in final check, install the defining row m = k*w for violated monomials with at most one non-fixed factor before resorting to case splits and horner/grobner'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), ('arith.nl.propagate_fixed_rows', BOOL, False, '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)'),