mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

lll_cube: exponential delay throttle on bail

Browse source 
Mirrors the nla_grobner pattern. State on int_solver:👿
  m_lll_cube_delay        - ticks to skip
  m_lll_cube_delay_base   - current penalty size, doubles on bail
                            (capped at 1024), decrements on success

After each bail the next |delay_base| invocations are short-circuited
in should_find_lll_cube(). Eliminates the bail-tighten feedback loop
that turned plain-cube wins into timeouts on instances such as
rings/ring_2exp14_7vars_4ite_unsat (22.8s -> 1.3s) and
cut_lemmas/20-vars/cut_lemma_03_011 (timeout -> 8.3s).

Adds stat 'arith-lll-cube-throttled' for visibility.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-05-15 14:08:51 -07:00
parent da9c720542
commit 8da9fc9779
2 changed files with 35 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/math/lp/int_solver.cpp
View file

@ -45,7 +45,10 @@ namespace lp {
dioph_eq m_dio;
int_gcd_test m_gcd;
unsigned m_initial_dio_calls_period;
unsigned m_lll_cube_delay = 0;
unsigned m_lll_cube_delay_base = 0;
static const unsigned LLL_CUBE_DELAY_CAP = 1024;
bool column_is_int_inf(unsigned j) const {
return lra.column_is_int(j) && (!lia.value_is_int(j));
}
@ -201,7 +204,32 @@ namespace lp {
unsigned period = settings().m_int_find_lll_cube_period;
if (period == 0)
return false;
return m_number_of_calls % period == 0;
if (m_number_of_calls % period != 0)
return false;
if (m_lll_cube_delay > 0) {
--m_lll_cube_delay;
settings().stats().m_lll_cube_throttled++;
return false;
}
return true;
}
// After int_cube_lll fires we record the outcome here so the next
// invocation gate (should_find_lll_cube) can back off when the
// heuristic keeps bailing on an unchanged-looking state.
void on_lll_cube_result(lia_move r) {
if (r == lia_move::sat) {
if (m_lll_cube_delay_base > 0)
--m_lll_cube_delay_base;
m_lll_cube_delay = 0;
return;
}
// bail: grow the penalty exponentially up to the cap.
if (m_lll_cube_delay_base == 0)
m_lll_cube_delay_base = 1;
else if (m_lll_cube_delay_base < LLL_CUBE_DELAY_CAP)
m_lll_cube_delay_base = std::min(m_lll_cube_delay_base * 2u, LLL_CUBE_DELAY_CAP);
m_lll_cube_delay = m_lll_cube_delay_base;
}
bool should_gomory_cut() {
@ -255,8 +283,10 @@ namespace lp {
if (r == lia_move::undef) r = patch_basic_columns();
if (r == lia_move::undef && should_find_cube()) {
r = int_cube(lia)();
if (r == lia_move::undef && settings().enable_lll_cube() && should_find_lll_cube())
if (r == lia_move::undef && settings().enable_lll_cube() && should_find_lll_cube()) {
r = int_cube_lll(lia)();
on_lll_cube_result(r);
}
}
if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();

2
src/math/lp/lp_settings.h
View file

@ -119,6 +119,7 @@ struct statistics {
unsigned m_lll_cube_bail_basis = 0;
unsigned m_lll_cube_bail_tighten = 0;
unsigned m_lll_cube_bail_infeasible = 0;
unsigned m_lll_cube_throttled = 0;
unsigned m_patches = 0;
unsigned m_patches_success = 0;
unsigned m_hnf_cutter_calls = 0;
@ -166,6 +167,7 @@ struct statistics {
st.update("arith-lll-cube-bail-basis", m_lll_cube_bail_basis);
st.update("arith-lll-cube-bail-tighten", m_lll_cube_bail_tighten);
st.update("arith-lll-cube-bail-infeasible", m_lll_cube_bail_infeasible);
st.update("arith-lll-cube-throttled", m_lll_cube_throttled);
st.update("arith-patches", m_patches);
st.update("arith-patches-success", m_patches_success);
st.update("arith-hnf-calls", m_hnf_cutter_calls);