diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index aec275b774..287a57fd06 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -45,6 +45,9 @@ namespace lp { int_gcd_test m_gcd; unsigned m_initial_dio_calls_period; unsigned m_lcube_period; + // The number of consecutive genuine dio calls that returned undef, reset on a dio + // conflict. Drives the decision to start running Gomory with dio. + unsigned m_dio_undef_in_a_row = 0; bool column_is_int_inf(unsigned j) const { return lra.column_is_int(j) && (!lia.value_is_int(j)); @@ -178,14 +181,16 @@ namespace lp { if (r == lia_move::conflict) { m_dio.explain(*this->m_ex); lia.settings().dio_calls_period() = m_initial_dio_calls_period; - lia.settings().dio_enable_gomory_cuts() = false; + m_dio_undef_in_a_row = 0; + lia.settings().stop_running_gomory_with_dio(); // dio was productive: stop running Gomory lia.settings().set_run_gcd_test(false); return lia_move::conflict; } if (r == lia_move::undef) { - lia.settings().dio_calls_period() *= 2; - if (lra.settings().dio_calls_period() >= 16) { - lia.settings().dio_enable_gomory_cuts() = true; + lia.settings().dio_calls_period() *= 2; // throttle dio scheduling on failure + ++m_dio_undef_in_a_row; + if (m_dio_undef_in_a_row >= lra.settings().dio_gomory_enable_period()) { + lia.settings().start_running_gomory_with_dio(); // dio persistently unproductive: start running Gomory lia.settings().set_run_gcd_test(true); } } @@ -193,9 +198,24 @@ namespace lp { } lp_settings& settings() { return lra.settings(); } + + // Decide whether a periodic heuristic fires on this call. When + // random_hammers 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_hammers()) + return settings().random_next(period) == 0; + return m_number_of_calls % period == 0; + } + bool should_find_cube() { - return m_number_of_calls % 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 @@ -203,7 +223,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() && m_number_of_calls % m_lcube_period == 0; + return settings().lcube() && hit_period(m_lcube_period); } lia_move find_lcube() { @@ -220,18 +240,24 @@ namespace lp { bool should_gomory_cut() { bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() || m_dio.some_terms_are_ignored(); - return dio_allows_gomory && m_number_of_calls % 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() && (m_number_of_calls % settings().dio_calls_period() == 0); + bool ret = lia.settings().dio() && hit_period(settings().dio_calls_period()); + if (!ret && lia.settings().dio_calls_period() > m_initial_dio_calls_period) { + unsigned dec = settings().dio_calls_period_decrease(); + unsigned& period = lia.settings().dio_calls_period(); + period = period > m_initial_dio_calls_period + dec ? period - dec : m_initial_dio_calls_period; + } + return ret; } // HNF bool should_hnf_cut() { return (!settings().dio() || settings().dio_enable_hnf_cuts()) - && settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0; + && settings().enable_hnf() && hit_period(settings().hnf_cut_period()); } lia_move hnf_cut() { @@ -266,12 +292,12 @@ namespace lp { ++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_cube()) r = int_cube(lia)(); if (r == lia_move::undef && should_find_lcube()) r = find_lcube(); if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds(); if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut(); - if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2); if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq(); + if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2); if (r == lia_move::undef) r = int_branch(lia)(); if (settings().get_cancel_flag()) r = lia_move::undef; return r; diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index e9604e04b8..29a10c2d52 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -5,11 +5,15 @@ def_module_params(module_name='lp', params=(('dio', BOOL, True, 'use Diophantine equalities'), ('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'), ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'), + ('dio_gomory_enable_period', UINT, 16, 'number of consecutive unproductive (undef) Diophantine-handler calls after which the controller starts running Gomory cuts and the gcd test alongside dio; a dio conflict resets the count and stops them; set very large to never start them this way so Gomory follows dio_cuts_enable_gomory only'), ('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_calls_period_decrease', UINT, 2, 'Amount by which dio_calls_period is decreased on each final_check() call where the Diophantine handler is not triggered, until it returns to its initial value'), ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), ('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'), + ('int_hammer_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_hammers', BOOL, True, 'draw the periodic integer 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 63836aafa7..affc299788 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -37,13 +37,21 @@ void lp::lp_settings::updt_params(params_ref const& _p) { auto eps = p.arith_epsilon(); m_epsilon = rational(std::max(1, (int)(100000*eps)), 100000); m_dio = lp_p.dio(); - m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory(); + m_dio_cuts_enable_gomory = lp_p.dio_cuts_enable_gomory(); + m_dio_gomory_enable_period = lp_p.dio_gomory_enable_period(); m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf(); m_dump_bound_lemmas = p.arith_dump_bound_lemmas(); m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_calls_period = lp_p.dio_calls_period(); + m_dio_calls_period_decrease = lp_p.dio_calls_period_decrease(); m_dio_run_gcd = lp_p.dio_run_gcd(); + m_random_hammers = lp_p.random_hammers(); m_lcube = lp_p.lcube(); m_lcube_flips = lp_p.lcube_flips(); + unsigned hammer_period = lp_p.int_hammer_period(); + SASSERT(hammer_period != 0); + m_int_find_cube_period = hammer_period; + m_int_gomory_cut_period = hammer_period; + m_hnf_cut_period = hammer_period; m_max_conflicts = p.max_conflicts(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index cb27b1628c..bc1f2044f5 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -258,12 +258,16 @@ private: bool m_print_external_var_name = false; bool m_propagate_eqs = false; bool m_dio = false; - bool m_dio_enable_gomory_cuts = false; + bool m_dio_cuts_enable_gomory = false; + bool m_run_gomory_with_dio = false; + unsigned m_dio_gomory_enable_period = 16; bool m_dio_enable_hnf_cuts = true; bool m_dump_bound_lemmas = false; bool m_dio_ignore_big_nums = false; unsigned m_dio_calls_period = 4; + unsigned m_dio_calls_period_decrease = 2; bool m_dio_run_gcd = true; + bool m_random_hammers = true; bool m_lcube = true; unsigned m_lcube_flips = 16; public: @@ -271,6 +275,10 @@ 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; } + unsigned dio_calls_period_decrease() const { return m_dio_calls_period_decrease; } + unsigned & dio_calls_period_decrease() { return m_dio_calls_period_decrease; } + bool random_hammers() const { return m_random_hammers; } + bool & random_hammers() { return m_random_hammers; } 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; } @@ -278,8 +286,19 @@ public: unsigned random_next() { return m_rand(); } unsigned random_next(unsigned u ) { return m_rand(u); } bool dio() { return m_dio; } - bool & dio_enable_gomory_cuts() { return m_dio_enable_gomory_cuts; } - bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; } + // Static config: did the user request Gomory cuts up front? (lp.dio_cuts_enable_gomory) + bool dio_cuts_enable_gomory() const { return m_dio_cuts_enable_gomory; } + // dio_calls_period at which the Diophantine back-off starts running Gomory (lp.dio_gomory_enable_period) + unsigned dio_gomory_enable_period() const { return m_dio_gomory_enable_period; } + // Runtime flag owned by the Diophantine controller, kept separate from the static + // config above so toggling it never clobbers the user's parameter: once dio has + // backed off enough it starts running Gomory cuts alongside dio, and a productive + // dio conflict stops them again. + void start_running_gomory_with_dio() { m_run_gomory_with_dio = true; } + void stop_running_gomory_with_dio() { m_run_gomory_with_dio = false; } + // Effective state read by should_gomory_cut(): allowed if either the user enabled it + // statically or the dio controller started running it, guarded by dio being active. + bool dio_enable_gomory_cuts() const { return m_dio && (m_dio_cuts_enable_gomory || m_run_gomory_with_dio); } bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; } bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; } bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; }