mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixes in gomory cut

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-15 17:15:46 -07:00
parent 324396e403
commit 03d55426bb
3 changed files with 53 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -1704,10 +1704,11 @@ public:
TRACE("arith", tout << "canceled\n";); TRACE("arith", tout << "canceled\n";);
return l_undef; return l_undef;
} }
/*
if (!check_idiv_bounds()) { if (!check_idiv_bounds()) {
TRACE("arith", tout << "idiv bounds check\n";); TRACE("arith", tout << "idiv bounds check\n";);
return l_false; return l_false;
} }*/
lp::lar_term term; lp::lar_term term;
lp::mpq k; lp::mpq k;
lp::explanation ex; // TBD, this should be streamlined accross different explanations lp::explanation ex; // TBD, this should be streamlined accross different explanations

93
src/util/lp/gomory.cpp
View file

@ -39,57 +39,59 @@ class gomory::imp {
const impq & upper_bound(unsigned j) const { return m_int_solver.upper_bound(j); } const impq & upper_bound(unsigned j) const { return m_int_solver.upper_bound(j); }
constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); } constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); }
constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); } constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); }
bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); }
void int_case_in_gomory_cut(const mpq & a, unsigned x_j, void int_case_in_gomory_cut(const mpq & a, unsigned j,
mpq & lcm_den, const mpq& f_0, const mpq& one_minus_f_0) { mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) {
lp_assert(is_int(x_j)); lp_assert(is_int(j) && !a.is_int());
lp_assert(!a.is_int()); mpq fj = int_solver::fractional_part(a);
mpq f_j = int_solver::fractional_part(a); lp_assert(fj.is_pos());
TRACE("gomory_cut_detail", TRACE("gomory_cut_detail",
tout << a << " x_j" << x_j << " k = " << m_k << "\n"; tout << a << " j=" << j << " k = " << m_k;
tout << "f_j: " << f_j << "\n"; tout << ", fj: " << fj << ", ";
tout << "f_0: " << f_0 << "\n"; tout << "f0: " << f0 << ", ";
tout << "1 - f_0: " << 1 - f_0 << "\n"; tout << "1 - f0: " << 1 - f0 << ", ";
tout << "at_lower(" << x_j << ") = " << at_lower(x_j) << std::endl; tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl;
); );
lp_assert (!f_j.is_zero());
mpq new_a; mpq new_a;
if (at_lower(x_j)) { mpq one_minus_fj = 1 - fj;
if (f_j <= one_minus_f_0) { if (at_lower(j)) {
new_a = f_j / one_minus_f_0; bool go_for_pos_a = fj / one_minus_f0 < one_minus_fj / f0;
if (go_for_pos_a) {
new_a = fj / one_minus_f0;
} }
else { else {
new_a = (1 - f_j) / f_0; new_a = one_minus_fj / f0;
} }
m_k.addmul(new_a, lower_bound(x_j).x); m_k.addmul(new_a, lower_bound(j).x);
m_ex.push_justification(column_lower_bound_constraint(x_j), new_a); m_ex.push_justification(column_lower_bound_constraint(j), new_a);
} }
else { else {
lp_assert(at_upper(x_j)); bool go_for_pos_a = fj / f0 < one_minus_fj / one_minus_f0;
if (f_j <= f_0) { lp_assert(at_upper(j));
new_a = f_j / f_0; // the upper terms are inverted
if (go_for_pos_a) {
new_a = - fj / f0;
} }
else { else {
new_a = (mpq(1) - f_j) / one_minus_f_0; new_a = - one_minus_fj / one_minus_f0;
} }
new_a.neg(); // the upper terms are inverted m_k.addmul(new_a, upper_bound(j).x);
m_k.addmul(new_a, upper_bound(x_j).x); m_ex.push_justification(column_upper_bound_constraint(j), new_a);
m_ex.push_justification(column_upper_bound_constraint(x_j), new_a);
} }
TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << m_k << "\n";); TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << m_k << "\n";);
m_t.add_monomial(new_a, x_j); m_t.add_monomial(new_a, j);
lcm_den = lcm(lcm_den, denominator(new_a)); lcm_den = lcm(lcm_den, denominator(new_a));
} }
void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f_0, const mpq& one_minus_f_0) { void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) {
TRACE("gomory_cut_detail_real", tout << "real\n";); TRACE("gomory_cut_detail_real", tout << "real\n";);
mpq new_a; mpq new_a;
if (at_lower(x_j)) { if (at_lower(x_j)) {
if (a.is_pos()) { if (a.is_pos()) {
new_a = a / one_minus_f_0; new_a = a / one_minus_f0;
} }
else { else {
new_a = a / f_0; new_a = a / f0;
new_a.neg(); new_a.neg();
} }
m_k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than m_k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than
@ -99,11 +101,11 @@ class gomory::imp {
else { else {
lp_assert(at_upper(x_j)); lp_assert(at_upper(x_j));
if (a.is_pos()) { if (a.is_pos()) {
new_a = a / f_0; new_a = a / f0;
new_a.neg(); // the upper terms are inverted. new_a.neg(); // the upper terms are inverted.
} }
else { else {
new_a = a / one_minus_f_0; new_a = a / one_minus_f0;
} }
m_k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a; m_k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a;
m_ex.push_justification(column_upper_bound_constraint(x_j), new_a); m_ex.push_justification(column_upper_bound_constraint(x_j), new_a);
@ -173,23 +175,28 @@ public:
// gomory will be t <= k and the current solution has a property t > k // gomory will be t <= k and the current solution has a property t > k
m_k = 1; m_k = 1;
mpq lcm_den(1); mpq lcm_den(1);
unsigned x_j;
mpq a;
bool some_int_columns = false; bool some_int_columns = false;
mpq f_0 = int_solver::fractional_part(get_value(m_inf_col)); mpq f0 = int_solver::fractional_part(get_value(m_inf_col));
mpq one_min_f_0 = 1 - f_0; mpq one_min_f0 = 1 - f0;
for (const auto & p : m_row) { for (const auto & p : m_row) {
x_j = p.var(); unsigned j = p.var();
if (x_j == m_inf_col) if (column_is_fixed(j)) {
m_ex.push_justification(column_lower_bound_constraint(j));
m_ex.push_justification(column_upper_bound_constraint(j));
continue; continue;
}
if (j == m_inf_col) {
lp_assert(p.coeff() == one_of_type<mpq>());
TRACE("gomory_cut_detail", tout << "seeing basic var";);
continue;
}
// make the format compatible with the format used in: Integrating Simplex with DPLL(T) // make the format compatible with the format used in: Integrating Simplex with DPLL(T)
a = p.coeff(); mpq a = - p.coeff();
a.neg(); if (is_real(j))
if (is_real(x_j)) real_case_in_gomory_cut(a, j, f0, one_min_f0);
real_case_in_gomory_cut(a, x_j, f_0, one_min_f_0); else if (!a.is_int()) { // fj will be zero and no monomial will be added
else if (!a.is_int()) { // f_j will be zero and no monomial will be added
some_int_columns = true; some_int_columns = true;
int_case_in_gomory_cut(a, x_j, lcm_den, f_0, one_min_f_0); int_case_in_gomory_cut(a, j, lcm_den, f0, one_min_f0);
} }
} }

2
src/util/lp/lar_solver.cpp
View file

@ -1645,7 +1645,6 @@ void lar_solver::push_and_register_term(lar_term* t) {
// terms // terms
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v) { const mpq &m_v) {
TRACE("add_term_lar_solver", print_linear_combination_of_column_indices(coeffs, tout););
if (strategy_is_undecided()) if (strategy_is_undecided())
return add_term_undecided(coeffs, m_v); return add_term_undecided(coeffs, m_v);
@ -1657,6 +1656,7 @@ var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
if (m_settings.bound_propagation()) if (m_settings.bound_propagation())
m_rows_with_changed_bounds.insert(A_r().row_count() - 1); m_rows_with_changed_bounds.insert(A_r().row_count() - 1);
} }
CTRACE("add_term_lar_solver", !m_v.is_zero(), print_term(*m_terms.back(), tout););
lp_assert(m_var_register.size() == A_r().column_count()); lp_assert(m_var_register.size() == A_r().column_count());
return ret; return ret;
} }