From 8da9fc97795e31ec120f947345dbb74f1557c1b1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 15 May 2026 14:08:51 -0700 Subject: [PATCH] lll_cube: exponential delay throttle on bail Mirrors the nla_grobner pattern. State on int_solver::imp: 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> --- src/math/lp/int_solver.cpp | 36 +++++++++++++++++++++++++++++++++--- src/math/lp/lp_settings.h | 2 ++ 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 4897b2c08..843e78349 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -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(); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index d91771052..58c9fb476 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -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);