From 7caae3f5d235c8f7c4da1764ff3503566fbb0deb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 13 Apr 2020 11:54:52 -0700 Subject: [PATCH] small improvements in tableau in rows and bound propagation Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 2 -- src/math/lp/lar_solver.cpp | 11 +++++++- src/math/lp/lar_solver.h | 2 +- src/math/lp/lp_primal_core_solver.h | 41 ++++++++++++++++++++++++++--- 4 files changed, 49 insertions(+), 7 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index f8666521a..a1d86e6f3 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -60,8 +60,6 @@ public : for (const auto & c : m_row) { if ((m_column_of_l == -2) && (m_column_of_u == -2)) return; - if (c.coeff().is_big()) - return; analyze_bound_on_var_on_coeff(c.var(), c.coeff()); } if (m_column_of_u >= 0) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index ee08ac88e..f8fdb7a11 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -153,11 +153,20 @@ void lar_solver::analyze_new_bounds_on_row( ra_pos.analyze(); } +bool lar_solver::row_has_a_big_num(unsigned i) const { + for (const auto& c : A_r().m_rows[i]) { + if (c.coeff().is_big()) + return true; + } + return false; +} + void lar_solver::analyze_new_bounds_on_row_tableau( unsigned row_index, lp_bound_propagator & bp ) { - if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation) + if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation + || row_has_a_big_num(row_index)) return; lp_assert(use_tableau()); bound_analyzer_on_row>::analyze_row(A_r().m_rows[row_index], diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 53427955f..66dc8fa7a 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -144,7 +144,7 @@ public: bool column_is_free(unsigned j) const; const lar_term & get_term(unsigned j) const; - + bool row_has_a_big_num(unsigned i) const; public: // init region diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index 792e99c36..85326cbaa 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -442,8 +442,43 @@ public: void one_iteration(); void one_iteration_tableau(); + // this version assumes that the leaving already has the right value, and does not update it + void update_x_tableau_rows(unsigned entering, unsigned leaving, const X& delta) { + this->add_delta_to_x(entering, delta); + if (!this->m_using_infeas_costs) { + for (const auto & c : this->m_A.m_columns[entering]) { + if (leaving != this->m_basis[c.var()]) { + this->add_delta_to_x_and_track_feasibility(this->m_basis[c.var()], - delta * this->m_A.get_val(c)); + } + } + } else { // m_using_infeas_costs == true + lp_assert(this->column_is_feasible(entering)); + lp_assert(this->m_costs[entering] == zero_of_type()); + // m_d[entering] can change because of the cost change for basic columns. + for (const auto & c : this->m_A.m_columns[entering]) { + unsigned j = this->m_basis[c.var()]; + if (j != leaving) + this->add_delta_to_x(j, -delta * this->m_A.get_val(c)); + update_inf_cost_for_column_tableau(j); + if (is_zero(this->m_costs[j])) + this->remove_column_from_inf_set(j); + else + this->insert_column_into_inf_set(j); + } + } + } + + void update_basis_and_x_tableau_rows(int entering, int leaving, X const & tt) { + lp_assert(this->use_tableau()); + lp_assert(entering != leaving); + update_x_tableau_rows(entering, leaving, tt); + this->pivot_column_tableau(entering, this->m_basis_heading[leaving]); + this->change_basis(entering, leaving); + } + + void advance_on_entering_and_leaving_tableau_rows(int entering, int leaving, const X &theta ) { - this->update_basis_and_x_tableau(entering, leaving, theta); + update_basis_and_x_tableau_rows(entering, leaving, theta); this->track_column_feasibility(entering); } @@ -505,9 +540,9 @@ public: } const X& new_val_for_leaving = get_val_for_leaving(leaving); X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent; + this->m_x[leaving] = new_val_for_leaving; + this->remove_column_from_inf_set(leaving); advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta ); - lp_assert(this->m_x[leaving] == new_val_for_leaving); - lp_assert(this->column_is_feasible(leaving)); if (this->current_x_is_feasible()) this->set_status(lp_status::OPTIMAL); }