From ad98c2df8e1315f372292db082e63b9f49d7142d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 5 Dec 2021 09:44:11 -0800 Subject: [PATCH] remove the bound on total iterations in simplex Signed-off-by: Lev Nachmanson --- src/math/lp/lar_core_solver_def.h | 12 +++++++++--- src/math/lp/lp_dual_core_solver_def.h | 7 ++----- src/math/lp/lp_dual_simplex_def.h | 3 --- src/math/lp/lp_primal_core_solver_def.h | 8 ++------ src/math/lp/lp_primal_core_solver_tableau_def.h | 4 +--- src/math/lp/lp_settings.h | 2 -- src/math/lp/lp_settings_def.h | 2 -- src/math/lp/lp_solver.h | 8 +------- src/smt/theory_lra.cpp | 2 +- src/test/lp/lp.cpp | 4 ---- 10 files changed, 16 insertions(+), 36 deletions(-) diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 06f414d11..f20aa7e6b 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -179,11 +179,17 @@ void lar_core_solver::solve() { } lp_assert(!settings().use_tableau() || r_basis_is_OK()); } - if (m_r_solver.get_status() == lp_status::INFEASIBLE) { + switch (m_r_solver.get_status()) + { + case lp_status::INFEASIBLE: fill_not_improvable_zero_sum(); - } - else if (m_r_solver.get_status() != lp_status::UNBOUNDED) { + break; + case lp_status::CANCELLED: + case lp_status::UNBOUNDED: // do nothing in these cases + break; + default: // adjust the status to optimal m_r_solver.set_status(lp_status::OPTIMAL); + break; } lp_assert(r_basis_is_OK()); lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); diff --git a/src/math/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h index 1e6553458..4a847fe85 100644 --- a/src/math/lp/lp_dual_core_solver_def.h +++ b/src/math/lp/lp_dual_core_solver_def.h @@ -100,10 +100,7 @@ template bool lp_dual_core_solver::done() { if (this->get_status() == lp_status::OPTIMAL) { return true; } - if (this->total_iterations() > this->m_settings.max_total_number_of_iterations) { // debug !!!! - this->set_status(lp_status::ITERATIONS_EXHAUSTED); - return true; - } + return false; // todo, need to be more cases } @@ -747,6 +744,6 @@ template void lp_dual_core_solver::solve() { // s one_iteration(); } while (this->get_status() != lp_status::FLOATING_POINT_ERROR && this->get_status() != lp_status::DUAL_UNBOUNDED && this->get_status() != lp_status::OPTIMAL && this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements - && this->total_iterations() <= this->m_settings.max_total_number_of_iterations); + ); } } diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h index 1b12106ea..34079cd94 100644 --- a/src/math/lp/lp_dual_simplex_def.h +++ b/src/math/lp/lp_dual_simplex_def.h @@ -31,9 +31,6 @@ template void lp_dual_simplex::decide_on_status_a break; case lp_status::DUAL_UNBOUNDED: lp_unreachable(); - case lp_status::ITERATIONS_EXHAUSTED: - this->m_status = lp_status::ITERATIONS_EXHAUSTED; - break; case lp_status::TIME_EXHAUSTED: this->m_status = lp_status::TIME_EXHAUSTED; break; diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index aeaf485a7..75eff208a 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -956,8 +956,6 @@ template unsigned lp_primal_core_solver::solve() && this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements && - this->total_iterations() <= this->m_settings.max_total_number_of_iterations - && !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)); lp_assert(this->get_status() == lp_status::FLOATING_POINT_ERROR @@ -1097,10 +1095,8 @@ template bool lp_primal_core_solver::done() { return true; } if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) { - this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true; - } - if (this->total_iterations() >= this->m_settings.max_total_number_of_iterations) { - this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true; + this->set_status(lp_status::CANCELLED); + return true; } return false; } diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index 115e1a344..03f07115b 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -182,9 +182,7 @@ unsigned lp_primal_core_solver::solve_with_tableau() { if (this->m_settings.get_cancel_flag() || this->iters_with_no_cost_growing() > this->m_settings.max_number_of_iterations_with_no_improvements - || - this->total_iterations() > this->m_settings.max_total_number_of_iterations - ) { + ) { this->set_status(lp_status::CANCELLED); break; // from the loop } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 7a0fef5c7..2be55dcb1 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -71,7 +71,6 @@ enum class lp_status { FEASIBLE, FLOATING_POINT_ERROR, TIME_EXHAUSTED, - ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE, CANCELLED @@ -210,7 +209,6 @@ public: double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros double ignore_epsilon_of_harris { 10e-5 }; unsigned max_number_of_iterations_with_no_improvements { 2000000 }; - unsigned max_total_number_of_iterations { 20000000 }; double time_limit; // the maximum time limit of the total run time in seconds // dual section double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h index 247cb98d3..4c783049c 100644 --- a/src/math/lp/lp_settings_def.h +++ b/src/math/lp/lp_settings_def.h @@ -45,7 +45,6 @@ const char* lp_status_to_string(lp_status status) { case lp_status::FEASIBLE: return "FEASIBLE"; case lp_status::FLOATING_POINT_ERROR: return "FLOATING_POINT_ERROR"; case lp_status::TIME_EXHAUSTED: return "TIME_EXHAUSTED"; - case lp_status::ITERATIONS_EXHAUSTED: return "ITERATIONS_EXHAUSTED"; case lp_status::EMPTY: return "EMPTY"; case lp_status::UNSTABLE: return "UNSTABLE"; default: @@ -62,7 +61,6 @@ lp_status lp_status_from_string(std::string status) { if (status == "FEASIBLE") return lp_status::FEASIBLE; if (status == "FLOATING_POINT_ERROR") return lp_status::FLOATING_POINT_ERROR; if (status == "TIME_EXHAUSTED") return lp_status::TIME_EXHAUSTED; - if (status == "ITERATIONS_EXHAUSTED") return lp_status::ITERATIONS_EXHAUSTED; if (status == "EMPTY") return lp_status::EMPTY; lp_unreachable(); return lp_status::UNKNOWN; // it is unreachable diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h index 9b0b8fb0a..68beca06f 100644 --- a/src/math/lp/lp_solver.h +++ b/src/math/lp/lp_solver.h @@ -158,13 +158,7 @@ public: m_settings.time_limit = time_limit_in_seconds; } - void set_max_iterations_per_stage(unsigned max_iterations) { - m_settings.max_total_number_of_iterations = max_iterations; - } - - unsigned get_max_iterations_per_stage() const { - return m_settings.max_total_number_of_iterations; - } + protected: bool problem_is_empty(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index e89508b1c..5c2f5bf1b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3095,7 +3095,7 @@ public: default: TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, - // FLOATING_POINT_ERROR, TIME_EXAUSTED, ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE + // FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE return l_undef; } } diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 9d24d2787..85f87ef52 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2651,10 +2651,6 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read solver->settings().presolve_with_double_solver_for_lar = true; } - std::string iter = args_parser.get_option_value("--max_iters"); - if (!iter.empty()) { - solver->settings().max_total_number_of_iterations = atoi(iter.c_str()); - } if (args_parser.option_is_used("--compare_with_primal")){ if (reader == nullptr) { std::cout << "cannot compare with primal, the reader is null " << std::endl;