From e2fb4fbd387f06bd670146163df11ee650eb50cd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 13 Jan 2024 19:01:21 -1000 Subject: [PATCH] fix dependencies for Gomory polarity Signed-off-by: Lev Nachmanson --- src/math/lp/gomory.cpp | 42 +++++++++++++++++++++++++++++------------- src/math/lp/gomory.h | 2 +- 2 files changed, 30 insertions(+), 14 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 2f8eaf8fc..84165cd20 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -69,14 +69,16 @@ struct create_cut { // here we have the product of new_a*(xj - lb(j)), so new_a*lb(j) is added to m_k new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); lp_assert(new_a.is_pos()); - m_k.addmul(new_a, lower_bound(j).x); + m_k.addmul(new_a, lower_bound(j).x); + push_explanation(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); // here we have the expression new_a*(xj - ub), so new_a*ub(j) is added to m_k new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); lp_assert(new_a.is_neg()); - m_k.addmul(new_a, upper_bound(j).x); + m_k.addmul(new_a, upper_bound(j).x); + push_explanation(column_upper_bound_constraint(j)); } m_t.add_monomial(new_a, j); TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << "\n";); @@ -286,21 +288,14 @@ public: m_one_minus_fj = 1 - m_fj; int_case_in_gomory_cut(j); } - bool lb = at_lower(j); - if (lb) { - push_explanation(column_lower_bound_constraint(j)); - } else { - SASSERT(at_upper(j)); - push_explanation(column_upper_bound_constraint(j)); - } if (p.coeff().is_pos()) { - if (lb) + if (at_lower(j)) set_polarity(row_polarity::MAX); else set_polarity(row_polarity::MIN); } else { - if (lb) + if (at_lower(j)) set_polarity(row_polarity::MIN); else set_polarity(row_polarity::MAX); @@ -440,6 +435,27 @@ public: return ret; } + u_dependency* gomory::add_deps(u_dependency* dep, const row_strip& row, lpvar basic_var) { + u_dependency* ret = dep; + for (const auto& p : row) { + lpvar j = p.var(); + if (j == basic_var) + continue; + if (lia.is_fixed(j)) + continue; + if (lia.is_real(j)) continue; + if (!p.coeff().is_int()) continue; + // the explanation for all above have been already added + if (lia.at_lower(j)) + ret = lia.lra.dep_manager().mk_join(lia.column_lower_bound_constraint(j), ret); + else { + SASSERT(lia.at_upper(j)); + ret = lia.lra.dep_manager().mk_join(lia.column_upper_bound_constraint(j), ret); + } + } + return ret; + } + lia_move gomory::get_gomory_cuts(unsigned num_cuts) { struct cut_result {lar_term t; mpq k; u_dependency *dep;}; vector big_cuts; @@ -478,9 +494,9 @@ public: } SASSERT(test_row_polarity(lia, row, j) == cc.m_polarity); if (cc.m_polarity == row_polarity::MAX) - lra.update_column_type_and_bound(j, lp::lconstraint_kind::LE, floor(lra.get_column_value(j).x), cc.m_dep); + lra.update_column_type_and_bound(j, lp::lconstraint_kind::LE, floor(lra.get_column_value(j).x), add_deps(cc.m_dep, row, j)); 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), cc.m_dep); + 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)); if (!is_small_cut(lia.m_t)) { big_cuts.push_back({cc.m_t, cc.m_k, cc.m_dep}); diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h index 2586a4d31..8354bf01f 100644 --- a/src/math/lp/gomory.h +++ b/src/math/lp/gomory.h @@ -30,7 +30,7 @@ namespace lp { lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row); unsigned_vector gomory_select_int_infeasible_vars(unsigned num_cuts); bool is_gomory_cut_target(lpvar j); - lia_move get_cut(lpvar j); + u_dependency* add_deps(u_dependency*, const row_strip&, lpvar); public: lia_move get_gomory_cuts(unsigned num_cuts); gomory(int_solver& lia);