optionally throttle patch_basic_columns() especially useful in unsat cases

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Author: levnach

src/math/lp/int_solver.cpp

@@ -44,6 +44,7 @@ namespace lp {
         dioph_eq            m_dio;  
         int_gcd_test        m_gcd;
         unsigned            m_initial_dio_calls_period;
+        unsigned            m_patch_period = 1;
 
         bool column_is_int_inf(unsigned j) const {
             return lra.column_is_int(j) && (!lia.value_is_int(j));
@@ -52,6 +53,7 @@ namespace lp {
         imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) {
             m_hnf_cut_period = settings().hnf_cut_period();
             m_initial_dio_calls_period = settings().dio_calls_period();
+            m_patch_period = settings().m_int_patch_period;
         } 
 
         bool has_lower(unsigned j) const {
@@ -156,6 +158,11 @@ namespace lp {
                     try_patch_column(v, c.var(), delta_plus);
         }
 
+        bool should_patch() {
+            // period == 0 means no throttling (old behavior)
+            return settings().m_int_patch_period == 0 || m_number_of_calls % m_patch_period == 0;
+        }
+
         lia_move patch_basic_columns() {
             lia.settings().stats().m_patches++;
             lra.remove_fixed_vars_from_base();
@@ -165,8 +172,12 @@ namespace lp {
                     patch_basic_column(j);
             if (!lra.has_inf_int()) {
                 lia.settings().stats().m_patches_success++;
+                m_patch_period = std::max(1u, settings().m_int_patch_period);
                 return lia_move::sat;
             }
+            // Only throttle if enabled (period > 0)
+            if (settings().m_int_patch_period > 0 && m_patch_period < 16)
+                m_patch_period *= 2;
             return lia_move::undef;     
         }
 
@@ -244,7 +255,7 @@ namespace lp {
                 return lia_move::undef;
 
             ++m_number_of_calls;
-            if (r == lia_move::undef) r = patch_basic_columns();
+            if (r == lia_move::undef && should_patch()) r = patch_basic_columns();
             if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)();
             if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
             if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();

src/math/lp/lp_params_helper.pyg

@@ -8,6 +8,7 @@ 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_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),                          
+                          ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
+                          ('int_patch_period', UINT, 0, 'Period for patching integer columns (0 = no throttling, 1 = throttle adaptively)'),
                          ))
 

src/math/lp/lp_settings.cpp

@@ -43,5 +43,6 @@ 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_int_patch_period = lp_p.int_patch_period();
     m_max_conflicts = p.max_conflicts();
 }

src/math/lp/lp_settings.h

@@ -239,6 +239,7 @@ struct lp_settings {
     unsigned         column_number_threshold_for_using_lu_in_lar_solver = 4000;
     unsigned         m_int_gomory_cut_period = 4;
     unsigned         m_int_find_cube_period = 4;
+    unsigned         m_int_patch_period = 0;
 private:
     unsigned         m_hnf_cut_period = 4;
     bool             m_int_run_gcd_test = true;