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

lp: add lp.random_cut_period to toggle randomized cut/cube gates

Browse source 
Introduce the boolean lp.random_cut_period parameter (default true).
When enabled, the periodic integer heuristic gates (find_cube, lcube,
hnf, gomory, dio) fire at random with the same 1/period expected rate;
when disabled they fall back to the deterministic every-k-th-call
modulus on m_number_of_calls. The shared hit_period() helper centralizes
this decision, and m_number_of_calls is restored for the deterministic
path.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-19 07:38:06 -07:00
parent 029ce10d22
commit 30dc804d25
4 changed files with 26 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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();

1
src/math/lp/lp_params_helper.pyg
View file

@ -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'),
))

1
src/math/lp/lp_settings.cpp
View file

@ -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();

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

@ -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; }