Perf branch (#4710)

* avoid creating rows with  all but one fixed columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* pb

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* once in a while flip bounds of boxed variables during move_nbasic_to_bounds

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* flip rarely

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* flip rarely

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* flip rarely

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* return an empty model when lar_solver is not ready

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* randomly change bounded base var on demand only

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* randomly change bounded base var on demand only

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/gomory.cpp

@@ -388,19 +388,14 @@ int gomory::find_basic_var() {
     int result = -1;
     unsigned n = 0;
     unsigned min_row_size = UINT_MAX;
-
     // Prefer smaller row size
-    // Prefer boxed to non-boxed
-    // Prefer smaller ranges
-
 
     for (unsigned j : lra.r_basis()) {
         if (!lia.column_is_int_inf(j))
             continue;
         const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(j));
         if (!is_gomory_cut_target(row)) 
             continue;
-
         IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
         if (min_row_size == UINT_MAX || 
             2*row.size() < min_row_size || 
@@ -414,7 +409,7 @@ int gomory::find_basic_var() {
 }
 
 lia_move gomory::operator()() {
-    lra.move_non_basic_columns_to_bounds();
+    lra.move_non_basic_columns_to_bounds(true);
     int j = find_basic_var();
     if (j == -1) return lia_move::undef;
     unsigned r = lia.row_of_basic_column(j);

src/math/lp/int_branch.cpp

@@ -25,8 +25,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();
-    int j = find_inf_int_base_column();
+    int j = find_inf_int_column();
     return j == -1? lia_move::sat : create_branch_on_column(j);        
 }
 
@@ -51,27 +50,24 @@ lia_move int_branch::create_branch_on_column(int j) {
 }
 
 
-int int_branch::find_inf_int_base_column() {
+int int_branch::find_inf_int_column() {
     int result = -1;
     mpq range;
     mpq new_range;
     mpq small_range_thresold(1024);
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
     unsigned prev_usage = 0; // to quiet down the compile
-    unsigned k = 0;
     unsigned usage;
-    unsigned j;
+    unsigned j = 0;
     // this loop looks for a column with the most usages, but breaks when
     // a column with a small span of bounds is found
-    for (; k < lra.r_basis().size(); k++) {
-        j = lra.r_basis()[k];
+    for (; j < lra.column_count(); j++) {
         if (!lia.column_is_int_inf(j))
             continue;
         usage = lra.usage_in_terms(j);
         if (lia.is_boxed(j) &&  (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) {
-            result = j;
-            k++;            
+            result = j++;
             n = 1;
             break;
         }
@@ -83,14 +79,12 @@ int int_branch::find_inf_int_base_column() {
             result = j;
         }
     }
-    SASSERT(k == lra.r_basis().size() || n == 1);
+
     // this loop looks for boxed columns with a small span
-    for (; k < lra.r_basis().size(); k++) {
-        j = lra.r_basis()[k];
-        usage = lra.usage_in_terms(j);
+    for (; j < lra.column_count(); j++) {
         if (!lia.column_is_int_inf(j) || !lia.is_boxed(j))
             continue;
-        SASSERT(!lia.is_fixed(j));
+        usage = lra.usage_in_terms(j);
         new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage);
         if (new_range < range) {
             n = 1;

src/math/lp/int_branch.h

@@ -28,7 +28,7 @@ namespace lp {
         class int_solver& lia;
         class lar_solver& lra;
         lia_move create_branch_on_column(int j);
-        int find_inf_int_base_column();
+        int find_inf_int_column();
 
     public:
         int_branch(int_solver& lia);

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();
+            lra.move_non_basic_columns_to_bounds(false);
             // it can happen that we found an integer solution here
             return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
         }

src/math/lp/int_solver.h

@@ -68,10 +68,9 @@ class int_solver {
     bool                m_upper;           // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
     hnf_cutter          m_hnf_cutter;
     unsigned            m_hnf_cut_period;
-
 public:
     int_solver(lar_solver& lp);
-
+    
     // main function to check that the solution provided by lar_solver is valid for integral values,
     // or provide a way of how it can be adjusted.
     lia_move check(explanation *);

src/math/lp/lar_solver.cpp

@@ -210,7 +210,7 @@ lp_status lar_solver::solve() {
             detect_rows_with_changed_bounds();
     }
 
-    m_columns_with_changed_bound.clear();
+    clear_columns_with_changed_bounds();
     return m_status;
 }
 
@@ -272,7 +272,7 @@ void lar_solver::pop(unsigned k) {
 
     m_mpq_lar_core_solver.pop(k);
     remove_non_fixed_from_fixed_var_table();
-    clean_popped_elements(n, m_columns_with_changed_bound);
+    clean_popped_elements(n, m_columns_with_changed_bounds);
     clean_popped_elements(n, m_incorrect_columns);
 
     unsigned m = A_r().row_count();
@@ -335,7 +335,7 @@ bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const {
 void lar_solver::set_costs_to_zero(const lar_term& term) {
     auto & rslv = m_mpq_lar_core_solver.m_r_solver;
     auto & jset = m_mpq_lar_core_solver.m_r_solver.inf_set(); // hijack this set that should be empty right now
-    lp_assert(jset.is_empty());
+    lp_assert(jset.empty());
 
     for (const auto & p : term) {
         unsigned j = p.column();
@@ -361,7 +361,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
 void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {        
     TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
     m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
-    move_non_basic_columns_to_bounds();
+    move_non_basic_columns_to_bounds(false);
     auto & rslv = m_mpq_lar_core_solver.m_r_solver;
     rslv.set_using_infeas_costs(false);
     lp_assert(costs_are_zeros_for_r_solver());
@@ -379,53 +379,63 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
     lp_assert(rslv.reduced_costs_are_correct_tableau());
 }
 
-void lar_solver::move_non_basic_columns_to_bounds() {
+void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) {
     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))
+        if (move_non_basic_column_to_bounds(j, shift_randomly))
             change = true;
     }
-
-    if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs && change)
+    if (!change)
+        return;
+    if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs)
         update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
 
-    if (change) {
-        find_feasible_solution();
-    }
+    find_feasible_solution();
 }
 
-bool lar_solver::move_non_basic_column_to_bounds(unsigned j) {
+bool lar_solver::move_non_basic_column_to_bounds(unsigned j, bool force_change) {
     auto & lcs = m_mpq_lar_core_solver;
     auto & val = lcs.m_r_x[j];
     switch (lcs.m_column_types()[j]) {
-    case column_type::boxed:
-        if (val != lcs.m_r_lower_bounds()[j] && val != lcs.m_r_upper_bounds()[j]) {
-            if (m_settings.random_next() % 2 == 0)
+    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;
-        }
-        break;
+        } 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:
         if (val != lcs.m_r_lower_bounds()[j]) {
             set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);
             return true;
         }
         break;
+    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]);
             return true;
         }
         break;
-    default:
+    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;
+    default:
+        SASSERT(false);        
     }
     return false;
 }
@@ -728,17 +738,17 @@ void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
 }
 
 void lar_solver::detect_rows_with_changed_bounds() {
-    for (auto j : m_columns_with_changed_bound)
+    for (auto j : m_columns_with_changed_bounds)
         detect_rows_with_changed_bounds_for_column(j);
 }
 
 void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds() {
-    for (auto j : m_columns_with_changed_bound)
+    for (auto j : m_columns_with_changed_bounds)
         update_x_and_inf_costs_for_column_with_changed_bounds(j);
 }
 
 void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() {
-    for (auto j : m_columns_with_changed_bound)
+    for (auto j : m_columns_with_changed_bounds)
         update_x_and_inf_costs_for_column_with_changed_bounds(j);
 
     if (tableau_with_costs()) {
@@ -867,15 +877,6 @@ void lar_solver::copy_from_mpq_matrix(static_matrix<U, V> & matr) {
     }
 }
 
-
-bool lar_solver::try_to_set_fixed(column_info<mpq> & ci) {
-    if (ci.upper_bound_is_set() && ci.lower_bound_is_set() && ci.get_upper_bound() == ci.get_lower_bound() && !ci.is_fixed()) {
-        ci.set_fixed_value(ci.get_upper_bound());
-        return true;
-    }
-    return false;
-}
-
 bool lar_solver::all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side) {
     for (auto it : left_side) {
         if (! var_is_registered(it.second))
@@ -1114,7 +1115,8 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 
 // (x, y) != (x', y') => (x + delta*y) != (x' + delta*y')
 void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
-    if (!(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE)) {
+    if (!(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE) ||
+        !m_columns_with_changed_bounds.empty()) {
         variable_values.clear();
         return;
     }
@@ -1549,7 +1551,7 @@ bool lar_solver::external_is_used(unsigned v) const {
 void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) {
     register_new_ext_var_index(ext_j, is_int);
     m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
-    m_columns_with_changed_bound.increase_size_by_one();
+    increase_by_one_columns_with_changed_bounds();
     add_new_var_to_core_fields_for_mpq(false); // false for not adding a row
     if (use_lu())
         add_new_var_to_core_fields_for_doubles(false);
@@ -1710,7 +1712,7 @@ void lar_solver::add_basic_var_to_core_fields() {
     bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver();
     lp_assert(!use_lu || A_r().column_count() == A_d().column_count());
     m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
-    m_columns_with_changed_bound.increase_size_by_one();
+    increase_by_one_columns_with_changed_bounds();
     m_incorrect_columns.increase_size_by_one();
     m_rows_with_changed_bounds.increase_size_by_one();
     add_new_var_to_core_fields_for_mpq(true);
@@ -2019,7 +2021,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
             if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
             m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
             set_upper_bound_witness(j, ci);
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
 	}
 	break;
     case GT:
@@ -2034,7 +2036,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
                 return;
             }
             m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
             set_lower_bound_witness(j, ci);
             m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]? column_type::fixed : column_type::boxed);
 	}
@@ -2074,7 +2076,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
             }
             m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
             set_upper_bound_witness(j, ci);
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
             m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j]? column_type::fixed : column_type::boxed);
 	}
 	break;
@@ -2087,7 +2089,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
                 return;
             }
             m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
             set_lower_bound_witness(j, ci);
 	}
 	break;
@@ -2124,7 +2126,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
             if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
             m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
             set_upper_bound_witness(j, ci);
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
 	}
 	break;
     case GT:
@@ -2136,7 +2138,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
                 set_infeasible_column(j);
             }
             m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
             set_lower_bound_witness(j, ci);
             m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]? column_type::fixed : column_type::boxed);
 	}
@@ -2161,7 +2163,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
 }
 void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
     lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j));
-    m_columns_with_changed_bound.insert(j);
+    insert_to_columns_with_changed_bounds(j);
 
     mpq y_of_bound(0);
     switch (kind) {
@@ -2181,7 +2183,7 @@ void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kin
 	{
             auto low = numeric_pair<mpq>(right_side, y_of_bound);
             m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-            m_columns_with_changed_bound.insert(j);
+            insert_to_columns_with_changed_bounds(j);
             set_lower_bound_witness(j, ci);
             m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
 	}