From 4076820fe7cea74b7db34a317f60aa500b35ee48 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 25 Jun 2026 17:23:04 -0700 Subject: [PATCH] lp: add cross-round orthogonality for efficacy Gomory cut selection Add lp.gomory_cut_orthogonality (default false), lp.gomory_recent_cuts (default 5) and lp.gomory_parallelism_threshold (default 0.9). When efficacy selection (select or augment) is active and orthogonality is enabled, a non-priority candidate cut is skipped when its parallelism |a.b|/(||a|| ||b||) with an already-selected cut this round, or with one of the last gomory_recent_cuts cuts added in previous rounds (kept in int_solver::m_recent_cuts), exceeds gomory_parallelism_threshold. Adds lar_term::find_coeff and gomory::cut_parallelism. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/gomory.cpp | 44 +++++++++++++++++++++++++++++++- src/math/lp/gomory.h | 1 + src/math/lp/int_solver.h | 1 + src/math/lp/lar_term.h | 6 +++++ src/math/lp/lp_params_helper.pyg | 3 +++ src/math/lp/lp_settings.cpp | 3 +++ src/math/lp/lp_settings.h | 6 +++++ 7 files changed, 63 insertions(+), 1 deletion(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 08727dd872..2924d2ac8c 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -505,6 +505,23 @@ public: return cut_efficacy(t, k) >= lia.settings().gomory_cut_efficacy_threshold(); } + // Parallelism (cosine similarity) of two cut left-hand sides: |a.b|/(||a||_2 ||b||_2), + // in [0,1]. Near 1 means the cuts are nearly parallel (redundant); near 0 means they are + // orthogonal (diverse). Cuts with disjoint support have dot product 0, hence parallelism 0. + double gomory::cut_parallelism(const lar_term& a, const lar_term& b) { + mpq dot(0), na(0), nb(0); + for (lar_term::ival p : a) { + na += p.coeff() * p.coeff(); + if (const mpq* q = b.find_coeff(p.j())) + dot += p.coeff() * (*q); + } + for (lar_term::ival p : b) + nb += p.coeff() * p.coeff(); + if (na.is_zero() || nb.is_zero()) + return 0.0; + return std::abs(dot.get_double()) / std::sqrt(na.get_double() * nb.get_double()); + } + // Uniformly sample up to num_rows integer-infeasible rows that are valid Gomory cut // targets, without ranking them by how close the basic variable is to an integer. // This is the selection used by gomory_efficacy_select: row quality is judged later by @@ -613,21 +630,46 @@ public: // 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. + // threshold, up to num_cuts in total. When orthogonality is enabled, a non-priority + // candidate that is too parallel to an already-selected cut or to one of the recently + // added cuts (kept across rounds in lia.m_recent_cuts) is skipped as redundant. if (eff_mode) { std::stable_sort(scored_cuts.begin(), scored_cuts.end(), [](scored_cut const& a, scored_cut const& b) { if (a.is_frac != b.is_frac) return a.is_frac; return a.eff > b.eff; }); + const bool ortho = lia.settings().gomory_cut_orthogonality(); + const double par_thr = lia.settings().gomory_parallelism_threshold(); double thr = lia.settings().gomory_cut_efficacy_threshold(); + vector selected_terms; // cuts accepted in this round, for orthogonality + auto too_parallel = [&](const lar_term& t) { + for (auto const& s : selected_terms) + if (cut_parallelism(t, s) > par_thr) + return true; + for (auto const& s : lia.m_recent_cuts) + if (cut_parallelism(t, s) > par_thr) + return true; + return false; + }; + auto remember_cut = [&](const lar_term& t) { + if (!ortho) + return; + selected_terms.push_back(t); + lia.m_recent_cuts.push_back(t); + while (lia.m_recent_cuts.size() > lia.settings().gomory_recent_cuts()) + lia.m_recent_cuts.erase(lia.m_recent_cuts.begin()); + }; unsigned added = 0; for (auto const& c : scored_cuts) { if (added >= num_cuts) break; if (!c.is_frac && c.eff < thr) continue; + if (ortho && !c.is_frac && too_parallel(c.t)) + continue; ++added; + remember_cut(c.t); if (!is_small_cut(c.t)) { big_cuts.push_back({c.t, c.k, c.dep}); continue; diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h index 4b128691b2..df686a9eca 100644 --- a/src/math/lp/gomory.h +++ b/src/math/lp/gomory.h @@ -32,6 +32,7 @@ namespace lp { bool is_gomory_cut_target(lpvar j); bool cut_has_enough_efficacy(const lar_term& t, const mpq& k); double cut_efficacy(const lar_term& t, const mpq& k); + double cut_parallelism(const lar_term& a, const lar_term& b); u_dependency* add_deps(u_dependency*, const row_strip&, lpvar); public: lia_move get_gomory_cuts(unsigned num_cuts); diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 3373c2ed61..1a2f9ae278 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -46,6 +46,7 @@ class int_solver { lar_core_solver& lrac; imp* m_imp; vector m_equalities; + vector m_recent_cuts; // rolling history of recently added cut LHS vectors (orthogonality) bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m); bool is_boxed(unsigned j) const; bool is_free(unsigned j) const; diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index b2d7774937..7e3d7445a9 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -159,6 +159,12 @@ public: return it->get_data().m_value; } + // returns nullptr if the column j does not occur in the term + const mpq * find_coeff(unsigned j) const { + const auto* it = m_coeffs.find_core(j); + return it == nullptr ? nullptr : &it->get_data().m_value; + } + mpq & get_coeff(unsigned j){ auto* it = m_coeffs.find_core(j); SASSERT(it != nullptr); diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index daee7e5e87..ae5589ad5e 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -20,5 +20,8 @@ def_module_params(module_name='lp', ('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_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'), + ('gomory_cut_orthogonality', BOOL, False, 'when selecting Gomory cuts by efficacy (gomory_efficacy_select or gomory_efficacy_augment), skip a candidate cut that is too parallel to an already-selected cut or to one of the last gomory_recent_cuts added cuts, keeping the added cuts diverse'), + ('gomory_recent_cuts', UINT, 5, 'number of recently added Gomory cuts remembered across rounds to enforce orthogonality against when gomory_cut_orthogonality is enabled'), + ('gomory_parallelism_threshold', DOUBLE, 0.9, 'a candidate Gomory cut is rejected for being redundant when its parallelism |a.b|/(||a|| ||b||) with an already-selected or recent cut exceeds this value, only relevant when gomory_cut_orthogonality is enabled'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 5a09084546..32cbd9c840 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -53,6 +53,9 @@ void lp::lp_settings::updt_params(params_ref const& _p) { 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(); + m_gomory_cut_orthogonality = lp_p.gomory_cut_orthogonality(); + m_gomory_recent_cuts = lp_p.gomory_recent_cuts(); + m_gomory_parallelism_threshold = lp_p.gomory_parallelism_threshold(); 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 eff5c39e29..5db64868eb 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -275,6 +275,9 @@ private: bool m_gomory_efficacy_select = false; unsigned m_gomory_candidate_rows = 3; bool m_gomory_efficacy_augment = false; + bool m_gomory_cut_orthogonality = false; + unsigned m_gomory_recent_cuts = 5; + double m_gomory_parallelism_threshold = 0.9; public: bool lcube() const { return m_lcube; } unsigned lcube_flips() const { return m_lcube_flips; } @@ -283,6 +286,9 @@ public: 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; } + bool gomory_cut_orthogonality() const { return m_gomory_cut_orthogonality; } + unsigned gomory_recent_cuts() const { return m_gomory_recent_cuts; } + double gomory_parallelism_threshold() const { return m_gomory_parallelism_threshold; } 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; }