mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 01:36:48 +00:00
Code Activity

nla: re-linearize violated monomials with fixed factors at final check

Browse source 
A monomial whose factors except at most one are fixed is linear.
propagate_linear_bound handles it once and retires it via set_propagated,
but when its defining row m = k*w is satisfied by the model of the moment
the row is skipped and the relation is recorded nowhere; when the model
later moves, the only handles left are refine_pseudo_linear case splits
or a horner/grobner round per final check. On the fstar regression suite
(F* proof obligations over 32/64-bit arithmetic, where pow2 constants
fix the scaling factors for good) this is the main gap between
arith.solver=6 and arith.solver=2, whose propagate_linear_monomial
re-asserts the equality whenever a monomial becomes linear.

The new pass runs from core::propagate() on entry to every final check
and installs the defining relation of every monomial that the current
model violates, bypassing the latch. Two guards keep it from regressing
the families that broke every earlier attempt:

- only violated monomials are touched. Recording rows for satisfied
  monomials (arith.nl.propagate_linear_monomials_eagerly) was measured
  to lose over 500 QF_NIA instances to tableau growth.

- the row-installing path m = k*w is reserved for fixed-factor products
  wider than 16 bits. A small k is the signature of factors fixed by
  branch enumeration; installing m = 3*w rows at deep decision levels
  turned queries-Pulse.Lib.HashTable.Spec-1 from 0.1s into a timeout,
  while the genuine wins all fire with k = 2^32 or 2^64. The row-free
  paths (m fixed to a constant) are plain bound updates and stay
  ungated.

Measured on ~/dev/z3test/regressions/fstar (rlimit, arith.solver=6):
  FStar.UInt128-1            503423 -> 148856
  queries-FStar.UInt128-10  3866608 -> 2702063
  FStar-UInt128-axiom        321515 -> 226608
  queries-...HashTable.Spec  unchanged (223336)
  FStar.Matrix-2             unchanged (seed noise per earlier analysis)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
Lev Nachmanson 2026-08-03 10:40:14 -07:00 • committed by Lev Nachmanson
parent 40953fa703
commit 953f85e1ab
4 changed files with 75 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

69
src/math/lp/monomial_bounds.cpp
View file

@ -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<lp::constraint_index> cs;

3
src/math/lp/monomial_bounds.h
View file

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

5
src/math/lp/nla_core.cpp
View file

@ -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)

1
src/params/smt_params_helper.pyg
View file

@ -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)'),