diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 7fdffc72db..08727dd872 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -526,13 +526,28 @@ public: lia_move gomory::get_gomory_cuts(unsigned num_cuts) { struct cut_result {lar_term t; mpq k; u_dependency *dep;}; - struct scored_cut {lar_term t; mpq k; u_dependency *dep; double eff;}; + struct scored_cut {lar_term t; mpq k; u_dependency *dep; double eff; bool is_frac;}; vector big_cuts; - vector scored_cuts; // candidates for best-of-N efficacy selection + vector scored_cuts; // candidates for efficacy-based selection const bool eff_select = lia.settings().gomory_efficacy_select(); - unsigned_vector columns_for_cuts = eff_select - ? gomory_select_random_rows(lia.settings().gomory_candidate_rows()) - : gomory_select_int_infeasible_vars(num_cuts); + const bool eff_augment = lia.settings().gomory_efficacy_augment(); + const bool eff_mode = eff_select || eff_augment; + + // In augment mode we keep one fractionality-selected cut (priority) and reserve the + // remaining slots for the most efficacious cuts built from random candidate rows. + unsigned_vector frac_cols; + unsigned_vector columns_for_cuts; + if (eff_augment) { + frac_cols = gomory_select_int_infeasible_vars(1); + columns_for_cuts = frac_cols; + for (unsigned j : gomory_select_random_rows(lia.settings().gomory_candidate_rows())) + if (!frac_cols.contains(j)) + columns_for_cuts.push_back(j); + } + else if (eff_select) + columns_for_cuts = gomory_select_random_rows(lia.settings().gomory_candidate_rows()); + else + columns_for_cuts = gomory_select_int_infeasible_vars(num_cuts); bool has_small_cut = false; // define inline helper functions @@ -570,14 +585,12 @@ public: else if (cc.m_polarity == row_polarity::MIN) lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE, ceil(lra.get_column_value(j).x), add_deps(cc.m_dep, row, j)); - // Best-of-N selection: collect every candidate cut that clears the efficacy - // threshold, then (after the loop) add the most efficacious ones. The row was - // picked at random rather than by the basic variable's fractionality, so the - // cut's efficacy is what decides whether and how strongly it is preferred. - if (eff_select) { + // Efficacy-based selection (select or augment): collect every candidate cut with + // its efficacy, then add the chosen ones after the loop. In augment mode the + // fractionality-selected row keeps priority; the rest compete on efficacy. + if (eff_mode) { double e = cut_efficacy(cc.m_t, cc.m_k); - if (e >= lia.settings().gomory_cut_efficacy_threshold()) - scored_cuts.push_back({cc.m_t, cc.m_k, cc.m_dep, e}); + scored_cuts.push_back({cc.m_t, cc.m_k, cc.m_dep, e, eff_augment && frac_cols.contains(j)}); continue; } @@ -598,14 +611,22 @@ public: return lia_move::cancelled; } - // best-of-N: add up to num_cuts of the most efficacious collected candidates - if (eff_select) { + // Add the selected efficacy-mode cuts: fractionality-priority cuts first (always + // kept, like the baseline), then the most efficacious remaining cuts that clear the + // threshold, up to num_cuts in total. + if (eff_mode) { std::stable_sort(scored_cuts.begin(), scored_cuts.end(), - [](scored_cut const& a, scored_cut const& b) { return a.eff > b.eff; }); + [](scored_cut const& a, scored_cut const& b) { + if (a.is_frac != b.is_frac) return a.is_frac; + return a.eff > b.eff; + }); + double thr = lia.settings().gomory_cut_efficacy_threshold(); unsigned added = 0; for (auto const& c : scored_cuts) { if (added >= num_cuts) break; + if (!c.is_frac && c.eff < thr) + continue; ++added; if (!is_small_cut(c.t)) { big_cuts.push_back({c.t, c.k, c.dep}); diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index dcb1d85925..daee7e5e87 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -18,6 +18,7 @@ def_module_params(module_name='lp', ('gomory_cut_efficacy_filter', BOOL, False, 'discard a generated Gomory cut whose efficacy (distance from the LP solution to the cut hyperplane, normalized by the cut coefficient norm) is below gomory_cut_efficacy_threshold'), ('gomory_cut_efficacy_threshold', DOUBLE, 0.01, 'minimal efficacy (normalized violation) required to keep a Gomory cut when gomory_cut_efficacy_filter or gomory_efficacy_select is enabled'), ('gomory_efficacy_select', BOOL, False, 'select Gomory cut rows by cut efficacy instead of by how close the basic variable is to an integer: pick gomory_candidate_rows integer-infeasible rows at random, build their cuts, and add the most efficacious ones whose efficacy is at least gomory_cut_efficacy_threshold'), - ('gomory_candidate_rows', UINT, 3, 'number of integer-infeasible rows sampled at random to build candidate Gomory cuts from when gomory_efficacy_select is enabled'), + ('gomory_efficacy_augment', BOOL, False, 'keep the standard (fractionality-based) Gomory cut(s) but diversify by efficacy: build the standard cuts plus gomory_candidate_rows random candidate cuts, always add the standard cut(s) first, then fill the remaining slots (up to the requested number of cuts) with the most efficacious remaining cuts whose efficacy is at least gomory_cut_efficacy_threshold'), + ('gomory_candidate_rows', UINT, 3, 'number of integer-infeasible rows sampled at random to build candidate Gomory cuts from when gomory_efficacy_select or gomory_efficacy_augment is enabled'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 614094a34a..5a09084546 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -52,6 +52,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_gomory_cut_efficacy_threshold = lp_p.gomory_cut_efficacy_threshold(); m_gomory_efficacy_select = lp_p.gomory_efficacy_select(); m_gomory_candidate_rows = lp_p.gomory_candidate_rows(); + m_gomory_efficacy_augment = lp_p.gomory_efficacy_augment(); unsigned hammer_period = lp_p.int_hammer_period(); SASSERT(hammer_period != 0); m_int_find_cube_period = hammer_period; diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 393af1e6a6..eff5c39e29 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -274,6 +274,7 @@ private: double m_gomory_cut_efficacy_threshold = 0.01; bool m_gomory_efficacy_select = false; unsigned m_gomory_candidate_rows = 3; + bool m_gomory_efficacy_augment = false; public: bool lcube() const { return m_lcube; } unsigned lcube_flips() const { return m_lcube_flips; } @@ -281,6 +282,7 @@ public: double gomory_cut_efficacy_threshold() const { return m_gomory_cut_efficacy_threshold; } bool gomory_efficacy_select() const { return m_gomory_efficacy_select; } unsigned gomory_candidate_rows() const { return m_gomory_candidate_rows; } + bool gomory_efficacy_augment() const { return m_gomory_efficacy_augment; } 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; }