diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 28377dcee0d..a283497c47c 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -25,13 +25,9 @@ namespace lp { int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {} lia_move int_branch::operator()() { - int j = find_any_inf_int_column_basis_first(); - return j == -1? lia_move::sat : create_branch_on_column(j); -} - -int int_branch::find_any_inf_int_column_basis_first() { + lra.move_non_basic_columns_to_bounds(); int j = find_inf_int_base_column(); - return j != -1 ? j : find_inf_int_nbasis_column(); + return j == -1? lia_move::sat : create_branch_on_column(j); } lia_move int_branch::create_branch_on_column(int j) { @@ -55,22 +51,6 @@ lia_move int_branch::create_branch_on_column(int j) { } -int int_branch::find_inf_int_nbasis_column() const { - unsigned n = 0; - int r = -1; - for (unsigned j : lra.r_nbasis()) { - SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j)); - if (lia.column_is_int_inf(j)) { - if (n == 0) { - r = j; - n = 1; - } else if (lia.random() % (++n) == 0) { - r = j; - } - } - } - return r; -} int int_branch::find_inf_int_base_column() { int result = -1; @@ -80,15 +60,17 @@ int int_branch::find_inf_int_base_column() { unsigned n = 0; lar_core_solver & lcs = lra.m_mpq_lar_core_solver; bool small = false; + unsigned prev_usage; for (unsigned j : lra.r_basis()) { SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j)); if (!lia.column_is_int_inf(j)) continue; bool boxed = lia.is_boxed(j); + unsigned usage = 2 * lra.usage_in_terms(j); if (small) { if (!boxed) continue; - new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x; + new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage); if (new_range <= small_range_thresold) { if (new_range < range) { n = 1; @@ -98,16 +80,17 @@ int int_branch::find_inf_int_base_column() { result = j; } } - } else if (boxed && - (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x) - <= small_range_thresold) { + } else if (boxed && ( + (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage)) + <= small_range_thresold)) { small = true; result = j; n = 1; - } else if (result == -1) { + } else if (result == -1 || prev_usage < usage) { result = j; + prev_usage = usage; n = 1; - } else if (lia.random() % (++n) == 0) { + } else if (prev_usage == usage && lia.random() % (++n) == 0) { result = j; } } diff --git a/src/math/lp/int_branch.h b/src/math/lp/int_branch.h index b9e265683c3..a7d72383a8d 100644 --- a/src/math/lp/int_branch.h +++ b/src/math/lp/int_branch.h @@ -29,8 +29,6 @@ namespace lp { class lar_solver& lra; lia_move create_branch_on_column(int j); int find_inf_int_base_column(); - int find_inf_int_nbasis_column() const; - int find_any_inf_int_column_basis_first(); public: int_branch(int_solver& lia); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index eb2c636d887..2f870d39dc3 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -323,6 +323,7 @@ void lar_solver::push() { m_term_count = m_terms.size(); m_term_count.push(); m_constraints.push(); + m_usage_in_terms.push(); } void lar_solver::clean_popped_elements(unsigned n, u_set& set) { @@ -380,6 +381,7 @@ void lar_solver::pop(unsigned k) { m_settings.simplex_strategy() = m_simplex_strategy; lp_assert(sizes_are_correct()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + m_usage_in_terms.pop(k); set_status(lp_status::UNKNOWN); } @@ -1599,14 +1601,17 @@ unsigned lar_solver::external_to_column_index(unsigned ext_j) const { var_index lar_solver::add_var(unsigned ext_j, bool is_int) { TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;); - var_index local_j; + var_index local_j; SASSERT(!m_term_register.external_is_used(ext_j)); lp_assert(!tv::is_term(ext_j)); if (m_var_register.external_is_used(ext_j, local_j)) - return local_j; + return local_j; lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count()); local_j = A_r().column_count(); m_columns_to_ul_pairs.push_back(ul_pair(UINT_MAX)); + while (m_usage_in_terms.size() <= ext_j) { + m_usage_in_terms.push_back(0); + } add_non_basic_var_to_core_fields(ext_j, is_int); lp_assert(sizes_are_correct()); return local_j; @@ -1775,6 +1780,9 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1)); if (use_lu()) fill_last_row_of_A_d(A_d(), term); + for (const auto & c : *term) + m_usage_in_terms[c.column()] = m_usage_in_terms[c.column()] + 1; + } void lar_solver::add_basic_var_to_core_fields() { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 796a1a43f6f..9f646ccd370 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -101,6 +101,7 @@ class lar_solver : public column_namer { std::unordered_map, term_hasher, term_comparer> m_normalized_terms_to_columns; vector m_backup_x; + stacked_vector m_usage_in_terms; // end of fields ////////////////// methods //////////////////////////////// @@ -467,9 +468,13 @@ class lar_solver : public column_namer { return -1; } } - + unsigned usage_in_terms(column_index j) const { + if (j >= m_usage_in_terms.size()) + return 0; + return m_usage_in_terms[j]; + } friend int_solver; friend int_branch; - + }; }