diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index ae541c32e..ec40082b5 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -34,6 +34,7 @@ namespace lp { int_solver& lia; lar_solver& lra; lar_core_solver& lrac; + unsigned m_number_of_calls = 0; lar_term m_t; // the term to return in the cut bool m_upper; // cut is an upper bound explanation *m_ex; // the conflict explanation @@ -193,12 +194,22 @@ namespace lp { lp_settings& settings() { return lra.settings(); } + // Decide whether a periodic heuristic fires on this call. When + // random_cut_period is enabled the gate is drawn at random with the + // same 1/period expected rate instead of a deterministic "every k-th + // call" modulus: a deterministic period can phase-lock with the search + // on some families and drown the solver in conflicts while another + // handler is starved; randomizing the gate breaks that resonance. + bool hit_period(unsigned period) { + if (period <= 1) + return true; + if (settings().random_cut_period()) + return settings().random_next(period) == 0; + return m_number_of_calls % period == 0; + } + bool should_find_cube() { - // Draw the decision at random instead of using a fixed "every k-th - // call" modulus, mirroring should_gomory_cut: a deterministic period - // can phase-lock with the search, while randomizing the gate (same - // 1/period expected rate) breaks that resonance. - return settings().random_next(settings().m_int_find_cube_period) == 0; + return hit_period(settings().m_int_find_cube_period); } // The largest cube test is throttled exponentially: when the polyhedron @@ -206,7 +217,7 @@ namespace lp { // later, after more constraints are added, so each failure doubles the // period and a success resets it. bool should_find_lcube() { - return settings().lcube() && settings().random_next(m_lcube_period) == 0; + return settings().lcube() && hit_period(m_lcube_period); } lia_move find_lcube() { @@ -223,23 +234,18 @@ namespace lp { bool should_gomory_cut() { bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() || m_dio.some_terms_are_ignored(); - // Draw the decision at random instead of using a fixed "every k-th - // call" modulus. A deterministic period can phase-lock with the - // search on some UNSAT families and drown the solver in theory - // conflicts while the Diophantine handler is starved; randomizing - // the gate (same 1/period expected rate) breaks that resonance. - return dio_allows_gomory && settings().random_next(settings().m_int_gomory_cut_period) == 0; + return dio_allows_gomory && hit_period(settings().m_int_gomory_cut_period); } bool should_solve_dioph_eq() { - return lia.settings().dio() && (settings().random_next(settings().dio_calls_period()) == 0); + return lia.settings().dio() && hit_period(settings().dio_calls_period()); } // HNF bool should_hnf_cut() { return (!settings().dio() || settings().dio_enable_hnf_cuts()) - && settings().enable_hnf() && settings().random_next(settings().hnf_cut_period()) == 0; + && settings().enable_hnf() && hit_period(settings().hnf_cut_period()); } lia_move hnf_cut() { @@ -272,6 +278,7 @@ namespace lp { if (settings().get_cancel_flag()) return lia_move::undef; + ++m_number_of_calls; 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 && should_find_lcube()) r = find_lcube(); diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 8059c0735..41e3998a2 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -12,5 +12,6 @@ def_module_params(module_name='lp', ('lcube', BOOL, True, 'use the largest cube test for integer feasibility'), ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'), ('cut_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'), + ('random_cut_period', BOOL, True, 'draw the integer cut/cube heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 52d8ea4f0..aecfb5bd2 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -43,6 +43,7 @@ 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_random_cut_period = lp_p.random_cut_period(); m_lcube = lp_p.lcube(); m_lcube_flips = lp_p.lcube_flips(); unsigned cut_period = lp_p.cut_period(); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index cb27b1628..cf164db98 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -264,6 +264,7 @@ private: bool m_dio_ignore_big_nums = false; unsigned m_dio_calls_period = 4; bool m_dio_run_gcd = true; + bool m_random_cut_period = true; bool m_lcube = true; unsigned m_lcube_flips = 16; public: @@ -271,6 +272,8 @@ public: unsigned lcube_flips() const { return m_lcube_flips; } unsigned dio_calls_period() const { return m_dio_calls_period; } unsigned & dio_calls_period() { return m_dio_calls_period; } + bool random_cut_period() const { return m_random_cut_period; } + bool & random_cut_period() { return m_random_cut_period; } bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; }