From 2d17f0428a4675c76273f1d419ce4ac624eae5ba Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 27 Jun 2026 01:25:14 -0700 Subject: [PATCH] lp: remove dio_calls_period linear recovery that defeats dio backoff The Diophantine-handler scheduler in int_solver applies an exponential backoff: solve_dioph_eq() doubles dio_calls_period on every unproductive (undef) dio call to "throttle dio scheduling on failure", letting the solver escalate to Gomory cuts / branching once dio is persistently unproductive. should_solve_dioph_eq() additionally decreased dio_calls_period by a fixed amount (dio_calls_period_decrease, default 2) on every final_check where dio did not fire. Because non-firing calls vastly outnumber firing calls once the period grows, this linear per-call decrease overwhelms the geometric backoff and pins the period near its initial small value, so an unproductive dio keeps firing and the handoff to Gomory/branching never durably engages. On the nonlinear mixed Int/Real benchmark iss-8418/3.smt2 this causes a 20s timeout where the instance was previously solved as sat. Removing the linear recovery (and the now-unused dio_calls_period_decrease parameter) restores the intended backoff; the benchmark is solved sat in ~0.03s. The dio-before-Gomory ordering and the dio_gomory_enable_period gating are left unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/int_solver.cpp | 5 ----- src/math/lp/lp_params_helper.pyg | 1 - src/math/lp/lp_settings.cpp | 1 - src/math/lp/lp_settings.h | 3 --- 4 files changed, 10 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 287a57fd06..b305eb84ae 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -245,11 +245,6 @@ namespace lp { bool should_solve_dioph_eq() { 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; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 29a10c2d52..8099ac2bd6 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -9,7 +9,6 @@ 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_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'), diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index affc299788..3f15956814 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -43,7 +43,6 @@ void lp::lp_settings::updt_params(params_ref const& _p) { 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(); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index bc1f2044f5..926488c6d9 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -265,7 +265,6 @@ private: 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; @@ -275,8 +274,6 @@ 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; }