From bee2b4574377af9323f5c081c948454688887b4c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 6 Feb 2026 10:14:39 -1000 Subject: [PATCH] optionally throttle patch_basic_columns() especially useful in unsat cases Signed-off-by: Lev Nachmanson --- src/math/lp/int_solver.cpp | 13 ++++++++++++- src/math/lp/lp_params_helper.pyg | 3 ++- src/math/lp/lp_settings.cpp | 1 + src/math/lp/lp_settings.h | 1 + 4 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index cf0878597..c4de2c3ff 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -44,6 +44,7 @@ namespace lp { dioph_eq m_dio; int_gcd_test m_gcd; unsigned m_initial_dio_calls_period; + unsigned m_patch_period = 1; bool column_is_int_inf(unsigned j) const { return lra.column_is_int(j) && (!lia.value_is_int(j)); @@ -52,6 +53,7 @@ namespace lp { imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) { m_hnf_cut_period = settings().hnf_cut_period(); m_initial_dio_calls_period = settings().dio_calls_period(); + m_patch_period = settings().m_int_patch_period; } bool has_lower(unsigned j) const { @@ -156,6 +158,11 @@ namespace lp { try_patch_column(v, c.var(), delta_plus); } + bool should_patch() { + // period == 0 means no throttling (old behavior) + return settings().m_int_patch_period == 0 || m_number_of_calls % m_patch_period == 0; + } + lia_move patch_basic_columns() { lia.settings().stats().m_patches++; lra.remove_fixed_vars_from_base(); @@ -165,8 +172,12 @@ namespace lp { patch_basic_column(j); if (!lra.has_inf_int()) { lia.settings().stats().m_patches_success++; + m_patch_period = std::max(1u, settings().m_int_patch_period); return lia_move::sat; } + // Only throttle if enabled (period > 0) + if (settings().m_int_patch_period > 0 && m_patch_period < 16) + m_patch_period *= 2; return lia_move::undef; } @@ -244,7 +255,7 @@ namespace lp { return lia_move::undef; ++m_number_of_calls; - if (r == lia_move::undef) r = patch_basic_columns(); + if (r == lia_move::undef && should_patch()) r = patch_basic_columns(); if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)(); 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_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index c3d50ab86..a903ae343 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -8,6 +8,7 @@ def_module_params(module_name='lp', ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'), ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'), ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'), - ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), + ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), + ('int_patch_period', UINT, 0, 'Period for patching integer columns (0 = no throttling, 1 = throttle adaptively)'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 42d6d8ef6..5b18e8239 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -43,5 +43,6 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_calls_period = lp_p.dio_calls_period(); m_dio_run_gcd = lp_p.dio_run_gcd(); + m_int_patch_period = lp_p.int_patch_period(); m_max_conflicts = p.max_conflicts(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 9c1345e1b..f3745b87b 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -239,6 +239,7 @@ public: unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; unsigned m_int_gomory_cut_period = 4; unsigned m_int_find_cube_period = 4; + unsigned m_int_patch_period = 0; private: unsigned m_hnf_cut_period = 4; bool m_int_run_gcd_test = true;