From 35fea6f4d304e194e082518e4b1940b753a3d7ae Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 18 Jun 2026 12:23:10 -0700 Subject: [PATCH] lp: expose integer cut/cube period as lp.cut_period parameter The find_cube, hnf and gomory integer heuristics were all throttled by a hardcoded period of 4 (m_int_find_cube_period, m_hnf_cut_period, m_int_gomory_cut_period). Make this value tunable through the new lp.cut_period parameter (default 4, preserving current behavior) so the period can be swept (e.g. 3/4/5) for benchmarking. A value of 0 is clamped to 1. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/lp_params_helper.pyg | 1 + src/math/lp/lp_settings.cpp | 6 ++++++ 2 files changed, 7 insertions(+) diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index e9604e04b..8059c0735 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -11,5 +11,6 @@ def_module_params(module_name='lp', ('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'), + ('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'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 63836aafa..52d8ea4f0 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -45,5 +45,11 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_run_gcd = lp_p.dio_run_gcd(); m_lcube = lp_p.lcube(); m_lcube_flips = lp_p.lcube_flips(); + unsigned cut_period = lp_p.cut_period(); + if (cut_period == 0) + cut_period = 1; + m_int_find_cube_period = cut_period; + m_int_gomory_cut_period = cut_period; + m_hnf_cut_period = cut_period; m_max_conflicts = p.max_conflicts(); }