mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-01 21:08:55 +00:00
Code Activity

lp: try Diophantine handler before Gomory cuts in int_solver::check

Browse source 
Gomory was dispatched before the Diophantine handler, so on calls where
both were scheduled Gomory ran first and preempted dio (dio only runs
when r==undef). Since dio_enable_gomory_cuts is cleared only by a dio
conflict, preemption prevented that clear from firing while undef
back-offs kept re-enabling it: once dio_calls_period crossed 16, Gomory
latched on and starved the Diophantine handler.

Reordering dio before Gomory lets a productive dio conflict preempt
Gomory naturally. On ring_2exp6_8vars_7ite_unsat (seed 555,
dio_calls_period=2) this turns a 600s timeout into a 70s solve, with no
regression at the default period (49s).

Also adds the lp.dio_calls_period_trace diagnostic flag and per-hammer
trace (gated by that flag, off by default) used to diagnose this.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-23 10:26:00 -07:00
parent 294b6ce18a
commit 166a96b814
4 changed files with 36 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -180,8 +180,9 @@ namespace lp {
lia.settings().dio_calls_period() = m_initial_dio_calls_period;
lia.settings().dio_enable_gomory_cuts() = false;
lia.settings().set_run_gcd_test(false);
IF_VERBOSE(2, verbose_stream() << "dio_period: call " << m_number_of_calls
<< " conflict reset period=" << lia.settings().dio_calls_period() << "\n";);
if (lia.settings().dio_calls_period_trace())
verbose_stream() << "dio_period: call " << m_number_of_calls
<< " conflict reset period=" << lia.settings().dio_calls_period() << "\n";
return lia_move::conflict;
}
if (r == lia_move::undef) {
@ -190,14 +191,29 @@ namespace lp {
lia.settings().dio_enable_gomory_cuts() = true;
lia.settings().set_run_gcd_test(true);
}
IF_VERBOSE(2, verbose_stream() << "dio_period: call " << m_number_of_calls
<< " undef double period=" << lia.settings().dio_calls_period()
<< (lia.settings().dio_enable_gomory_cuts() ? " (gomory+gcd on)" : "") << "\n";);
if (lia.settings().dio_calls_period_trace())
verbose_stream() << "dio_period: call " << m_number_of_calls
<< " undef double period=" << lia.settings().dio_calls_period()
<< (lia.settings().dio_enable_gomory_cuts() ? " (gomory+gcd on)" : "") << "\n";
}
return r;
}
lp_settings& settings() { return lra.settings(); }
void trace_hammer(char const* name, lia_move r) {
if (r == lia_move::undef || !settings().dio_calls_period_trace())
return;
char const* res =
r == lia_move::sat ? "sat" :
r == lia_move::branch ? "branch" :
r == lia_move::cut ? "cut" :
r == lia_move::conflict ? "conflict" :
r == lia_move::continue_with_check ? "continue" :
r == lia_move::cancelled ? "cancelled" : "undef";
verbose_stream() << "hammer: call " << m_number_of_calls
<< " " << name << " -> " << res << "\n";
}
// Decide whether a periodic heuristic fires on this call. When
// random_hammers is enabled the gate is drawn at random with the same
@ -248,8 +264,9 @@ namespace lp {
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;
IF_VERBOSE(2, verbose_stream() << "dio_period: call " << m_number_of_calls
<< " idle decrease period=" << period << "\n";);
if (settings().dio_calls_period_trace())
verbose_stream() << "dio_period: call " << m_number_of_calls
<< " idle decrease period=" << period << "\n";
}
return ret;
}
@ -285,6 +302,7 @@ namespace lp {
if (m_gcd.should_apply() || (settings().dio() && m_dio.some_terms_are_ignored()))
r = m_gcd();
trace_hammer("gcd", r);
check_return_helper pc(lra);
@ -293,13 +311,14 @@ 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_lcube()) r = find_lcube();
trace_hammer("patch", r);
if (r == lia_move::undef && should_find_cube()) { r = int_cube(lia)(); trace_hammer("cube", r); }
if (r == lia_move::undef && should_find_lcube()) { r = find_lcube(); trace_hammer("lcube", r); }
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_hnf_cut()) { r = hnf_cut(); trace_hammer("hnf", r); }
if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();
if (r == lia_move::undef) r = int_branch(lia)();
if (r == lia_move::undef && should_gomory_cut()) { r = gomory(lia).get_gomory_cuts(2); trace_hammer("gomory", r); }
if (r == lia_move::undef) { r = int_branch(lia)(); trace_hammer("branch", r); }
if (settings().get_cancel_flag()) r = lia_move::undef;
return r;
}

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

@ -9,6 +9,7 @@ def_module_params(module_name='lp',
('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_calls_period_trace', BOOL, False, 'Trace the evolution of dio_calls_period (the Diophantine call guard) to the verbose stream at each change point: conflict reset, undef doubling, and idle decrease'),
('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'),

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_calls_period_decrease = lp_p.dio_calls_period_decrease();
m_dio_calls_period_trace = lp_p.dio_calls_period_trace();
m_dio_run_gcd = lp_p.dio_run_gcd();
m_random_hammers = lp_p.random_hammers();
m_lcube = lp_p.lcube();

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;
unsigned m_dio_calls_period_decrease = 2;
bool m_dio_calls_period_trace = false;
bool m_dio_run_gcd = true;
bool m_random_hammers = true;
bool m_lcube = true;
@ -275,6 +276,8 @@ public:
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 dio_calls_period_trace() const { return m_dio_calls_period_trace; }
bool & dio_calls_period_trace() { return m_dio_calls_period_trace; }
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; }