From a6040a1f3d5d53191998d5d79fc08b0771f57251 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 28 May 2020 11:47:11 -0700 Subject: [PATCH] cautious remove_basis Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 34 +++++++++++++++++++++++++++ src/math/lp/lar_solver.h | 3 ++- src/math/lp/lp_core_solver_base.cpp | 1 + src/math/lp/lp_core_solver_base.h | 1 + src/math/lp/lp_core_solver_base_def.h | 12 ++++++++++ 5 files changed, 50 insertions(+), 1 deletion(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index b14c0e92f..4715d34be 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -565,6 +565,40 @@ bool lar_solver::remove_from_basis(unsigned j) { return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j); } +// val is the new value to be assigned to x[j] +// return true iff can find a new basic column that would be feasible +// after the pivoting +bool lar_solver::remove_from_basis(unsigned basic_j, const mpq& val) { + SASSERT(is_base(basic_j)); + impq del(0); + const auto& slv = m_mpq_lar_core_solver.m_r_solver; + bool grow = val < get_column_value(basic_j).x; // grow = true means that the monomial of the pivoted var has to grow + for (auto &c : A_r().m_rows[row_of_basic_column(basic_j)]) { + lpvar j = c.var(); + if (j == basic_j) { + SASSERT(c.coeff().is_one()); + continue; + } + + bool can_pivot = column_is_free(j); + if (!can_pivot && + ((grow && slv.monoid_can_increase(c))|| (!grow && slv.monoid_can_decrease(c)))) { + if (del.is_zero()) + del = impq(val) - get_column_value(basic_j); + + impq j_val = get_column_value(j) - del / c.coeff(); + if (inside_bounds(j, j_val)) + can_pivot = true; + } + + if (can_pivot) { + pivot_column_tableau(c.var(), row_of_basic_column(basic_j)); + return true; + } + } + return false; +} + lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const { if (tv::is_term(j_or_term)) { return get_term(j_or_term); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index a2bf376b9..fc0ddef45 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -260,6 +260,7 @@ class lar_solver : public column_namer { void update_delta_for_terms(const impq & delta, unsigned j, const vector&); void fill_vars_to_terms(vector> & vars_to_terms); bool remove_from_basis(unsigned); + bool remove_from_basis(unsigned, const mpq&); lar_term get_term_to_maximize(unsigned ext_j) const; bool sum_first_coords(const lar_term& t, mpq & val) const; void collect_rounded_rows_to_fix(); @@ -361,7 +362,7 @@ public: const ChangeReport& change_report) { if (is_base(j)) { TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";); - remove_from_basis(j); + remove_from_basis(j, val); } impq ival(val); diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp index 3a5a2020f..83da68d9d 100644 --- a/src/math/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -145,5 +145,6 @@ template bool lp::lp_core_solver_base::infeasibility_costs_ar template bool lp::lp_core_solver_base::infeasibility_costs_are_correct() const; template void lp::lp_core_solver_base >::calculate_pivot_row(unsigned int); template bool lp::lp_core_solver_base >::remove_from_basis(unsigned int); +template bool lp::lp_core_solver_base >::remove_from_basis(unsigned int, lp::numeric_pair const&); template void lp::lp_core_solver_base::solve_Bd(unsigned int, lp::indexed_vector&, lp::indexed_vector&) const; template void lp::lp_core_solver_base >::solve_Bd(unsigned int, lp::indexed_vector&, lp::indexed_vector&) const; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 60d0f3fe0..d911daa36 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -459,6 +459,7 @@ public: int pivots_in_column_and_row_are_different(int entering, int leaving) const; void pivot_fixed_vars_from_basis(); bool remove_from_basis(unsigned j); + bool remove_from_basis(unsigned j, const impq&); bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w); void init_basic_part_of_basis_heading() { unsigned m = m_basis.size(); diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 46fb0be76..42c2ddcf7 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -981,6 +981,18 @@ template bool lp_core_solver_base::remove_from_ba return false; } +template bool lp_core_solver_base::remove_from_basis(unsigned basic_j, const impq& val) { + indexed_vector w(m_basis.size()); // the buffer + unsigned i = m_basis_heading[basic_j]; + for (auto &c : m_A.m_rows[i]) { + if (c.var() == basic_j) + continue; + if (pivot_column_general(c.var(), basic_j, w)) + return true; + } + return false; +} + template bool lp_core_solver_base::infeasibility_costs_are_correct() const {