mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

lp: add cross-round orthogonality for efficacy Gomory cut selection

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-06-25 17:23:04 -07:00
parent c4ac986c42
commit 4076820fe7
7 changed files with 63 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/math/lp/gomory.cpp
View file

@ -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<lar_term> 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;

1
src/math/lp/gomory.h
View file

@ -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<mpq>&, lpvar);
public:
lia_move get_gomory_cuts(unsigned num_cuts);

1
src/math/lp/int_solver.h
View file

@ -46,6 +46,7 @@ class int_solver {
lar_core_solver& lrac;
imp* m_imp;
vector<equality> m_equalities;
vector<lar_term> 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;

6
src/math/lp/lar_term.h
View file

@ -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);

3
src/math/lp/lp_params_helper.pyg
View file

@ -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'),
))

3
src/math/lp/lp_settings.cpp
View file

@ -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;

6
src/math/lp/lp_settings.h
View file

@ -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; }