From f847d039bc4f6c79874727f6da6cb2ecc070211b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Oct 2023 20:57:54 -0700 Subject: [PATCH] use the simple version of move_non_basic_column_to_bounds --- src/math/lp/gomory.cpp | 2 +- src/math/lp/int_branch.cpp | 2 +- src/math/lp/int_cube.cpp | 2 +- src/math/lp/lar_solver.cpp | 50 +++++++++++++++++--------------------- src/math/lp/lar_solver.h | 4 +-- 5 files changed, 27 insertions(+), 33 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 775025018..e4267cbd4 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -417,7 +417,7 @@ int gomory::find_basic_var() { } lia_move gomory::operator()() { - lra.move_non_basic_columns_to_bounds(true); + lra.move_non_basic_columns_to_bounds(); int j = find_basic_var(); if (j == -1) return lia_move::undef; diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 4bfe2b827..d6262a4d0 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -24,7 +24,7 @@ namespace lp { int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {} lia_move int_branch::operator()() { - lra.move_non_basic_columns_to_bounds(true); + lra.move_non_basic_columns_to_bounds(); int j = find_inf_int_base_column(); return j == -1? lia_move::sat : create_branch_on_column(j); } diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index da724a543..9ef9aa341 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -43,7 +43,7 @@ namespace lp { if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) { TRACE("cube", tout << "cannot find a feasible solution";); lra.pop(); - lra.move_non_basic_columns_to_bounds(false); + lra.move_non_basic_columns_to_bounds(); // it can happen that we found an integer solution here return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 931e74f57..c3f0cd771 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -402,7 +402,7 @@ namespace lp { void lar_solver::prepare_costs_for_r_solver(const lar_term& term) { TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); - move_non_basic_columns_to_bounds(false); + move_non_basic_columns_to_bounds(); auto& rslv = m_mpq_lar_core_solver.m_r_solver; lp_assert(costs_are_zeros_for_r_solver()); lp_assert(reduced_costs_are_zeroes_for_r_solver()); @@ -419,11 +419,11 @@ namespace lp { lp_assert(rslv.reduced_costs_are_correct_tableau()); } - void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) { + void lar_solver::move_non_basic_columns_to_bounds() { auto& lcs = m_mpq_lar_core_solver; bool change = false; for (unsigned j : lcs.m_r_nbasis) { - if (move_non_basic_column_to_bounds(j, shift_randomly)) + if (move_non_basic_column_to_bounds(j)) change = true; } if (!change) @@ -434,46 +434,40 @@ namespace lp { find_feasible_solution(); } - bool lar_solver::move_non_basic_column_to_bounds(unsigned j, bool force_change) { + bool lar_solver::move_non_basic_column_to_bounds(unsigned j) { auto& lcs = m_mpq_lar_core_solver; auto& val = lcs.m_r_x[j]; switch (lcs.m_column_types()[j]) { case column_type::boxed: { - bool at_l = val == lcs.m_r_lower_bounds()[j]; - bool at_u = (!at_l && (val == lcs.m_r_upper_bounds()[j])); - if (!at_l && !at_u) { - if (m_settings.random_next() % 2) - set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]); - else - set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]); - return true; - } - else if (force_change && m_settings.random_next() % 3 == 0) { - set_value_for_nbasic_column(j, - at_l ? lcs.m_r_upper_bounds()[j] : lcs.m_r_lower_bounds()[j]); - return true; - } - break; - } - case column_type::lower_bound: + const auto& l = lcs.m_r_lower_bounds()[j]; + if (val == l || val == lcs.m_r_upper_bounds()[j]) return false; + set_value_for_nbasic_column(j, l); + return true; + } + + case column_type::lower_bound: { + const auto& l = lcs.m_r_lower_bounds()[j]; if (val != lcs.m_r_lower_bounds()[j]) { - set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]); + set_value_for_nbasic_column(j, l); return true; } - break; + return false; + } case column_type::fixed: - case column_type::upper_bound: - if (val != lcs.m_r_upper_bounds()[j]) { - set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]); + case column_type::upper_bound: { + const auto & u = lcs.m_r_upper_bounds()[j]; + if (val != u) { + set_value_for_nbasic_column(j, u); return true; } - break; + return false; + } case column_type::free_column: if (column_is_int(j) && !val.is_int()) { set_value_for_nbasic_column(j, impq(floor(val))); return true; } - break; + return false; default: SASSERT(false); } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 09cb7796c..d902f9a3a 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -635,8 +635,8 @@ class lar_solver : public column_namer { return *m_terms[t.id()]; } lp_status find_feasible_solution(); - void move_non_basic_columns_to_bounds(bool); - bool move_non_basic_column_to_bounds(unsigned j, bool); + void move_non_basic_columns_to_bounds(); + bool move_non_basic_column_to_bounds(unsigned j); inline bool r_basis_has_inf_int() const { for (unsigned j : r_basis()) { if (column_is_int(j) && !column_value_is_int(j))