mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-25 16:32:35 +00:00
Code Activity

lp: add best-of-N efficacy-based Gomory row selection

Browse source 
Add lp.gomory_efficacy_select (default false) and lp.gomory_candidate_rows
(default 3). When enabled, Gomory cut rows are no longer chosen by how close
the basic variable is to an integer. Instead, gomory_candidate_rows
integer-infeasible GMI-clean rows are sampled uniformly at random, a cut is
built for each, and the most efficacious cuts whose efficacy
(k - t(x*))/||t||_2 is at least gomory_cut_efficacy_threshold are added (up to
num_cuts of them, best first).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-25 15:24:23 -07:00
parent 8d1dde407e
commit 11e95dafeb
5 changed files with 81 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -272,11 +272,15 @@ private:
unsigned m_lcube_flips = 16;
bool m_gomory_cut_efficacy_filter = false;
double m_gomory_cut_efficacy_threshold = 0.01;
bool m_gomory_efficacy_select = false;
unsigned m_gomory_candidate_rows = 3;
public:
bool lcube() const { return m_lcube; }
unsigned lcube_flips() const { return m_lcube_flips; }
bool gomory_cut_efficacy_filter() const { return m_gomory_cut_efficacy_filter; }
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; }
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; }