better branching with usage_in_terms()

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

src/math/lp/int_branch.cpp

@@ -25,13 +25,9 @@ namespace lp {
 int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
 
 lia_move int_branch::operator()() {
-    int j = find_any_inf_int_column_basis_first();
-    return j == -1? lia_move::sat : create_branch_on_column(j);        
-}
-
-int int_branch::find_any_inf_int_column_basis_first() {
+    lra.move_non_basic_columns_to_bounds();
     int j = find_inf_int_base_column();
-    return j != -1 ? j : find_inf_int_nbasis_column();
+    return j == -1? lia_move::sat : create_branch_on_column(j);        
 }
 
 lia_move int_branch::create_branch_on_column(int j) {
@@ -55,22 +51,6 @@ lia_move int_branch::create_branch_on_column(int j) {
 }
 
 
-int int_branch::find_inf_int_nbasis_column() const {
-    unsigned n = 0;
-    int r = -1;
-    for (unsigned j : lra.r_nbasis()) {
-        SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
-        if (lia.column_is_int_inf(j)) {
-            if (n == 0) {
-                r = j;
-                n = 1;                    
-            } else if (lia.random() % (++n) == 0) {
-                r = j;
-            }
-        }
-    }
-    return r; 
-}
 
 int int_branch::find_inf_int_base_column() {
     int result = -1;
@@ -80,15 +60,17 @@ int int_branch::find_inf_int_base_column() {
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
     bool small = false;
+    unsigned prev_usage;
     for (unsigned j : lra.r_basis()) {
         SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
         if (!lia.column_is_int_inf(j))
             continue;
         bool boxed = lia.is_boxed(j);
+        unsigned usage =  2 * lra.usage_in_terms(j);
         if (small) {
             if (!boxed)
                 continue;
-            new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
+            new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage);
             if (new_range <= small_range_thresold) {
                 if (new_range < range) {
                     n = 1;
@@ -98,16 +80,17 @@ int int_branch::find_inf_int_base_column() {
                     result = j;                    
                 }
             }
-        } else if (boxed &&
-                   (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x)
-                   <= small_range_thresold) {
+        } else if (boxed && (
+                   (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage))
+                   <= small_range_thresold)) {
             small = true;
             result = j;
             n = 1;
-        } else if (result == -1) {
+        } else if (result == -1 || prev_usage < usage) {
             result = j;
+            prev_usage = usage;
             n      = 1;
-        } else if (lia.random() % (++n) == 0) {
+        } else if (prev_usage == usage && lia.random() % (++n) == 0) {
             result = j;
         }
     }

src/math/lp/int_branch.h

@@ -29,8 +29,6 @@ namespace lp {
         class lar_solver& lra;
         lia_move create_branch_on_column(int j);
         int find_inf_int_base_column();
-        int find_inf_int_nbasis_column() const;
-        int find_any_inf_int_column_basis_first();
 
     public:
         int_branch(int_solver& lia);

src/math/lp/lar_solver.cpp

@@ -323,6 +323,7 @@ void lar_solver::push() {
     m_term_count = m_terms.size();
     m_term_count.push();
     m_constraints.push();
+    m_usage_in_terms.push();
 }
 
 void lar_solver::clean_popped_elements(unsigned n, u_set& set) {
@@ -380,6 +381,7 @@ void lar_solver::pop(unsigned k) {
     m_settings.simplex_strategy() = m_simplex_strategy;
     lp_assert(sizes_are_correct());
     lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
+    m_usage_in_terms.pop(k);
     set_status(lp_status::UNKNOWN);
 }
 
@@ -1599,14 +1601,17 @@ unsigned lar_solver::external_to_column_index(unsigned ext_j) const {
 
 var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
     TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;);
-    var_index local_j;
+    var_index local_j;    
     SASSERT(!m_term_register.external_is_used(ext_j));
     lp_assert(!tv::is_term(ext_j));
     if (m_var_register.external_is_used(ext_j, local_j))
-        return local_j;
+        return local_j;    
     lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count());
     local_j = A_r().column_count();
     m_columns_to_ul_pairs.push_back(ul_pair(UINT_MAX));
+    while (m_usage_in_terms.size() <= ext_j) {
+        m_usage_in_terms.push_back(0);
+    }
     add_non_basic_var_to_core_fields(ext_j, is_int);
     lp_assert(sizes_are_correct());
     return local_j;
@@ -1775,6 +1780,9 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned
     m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1));
     if (use_lu())
         fill_last_row_of_A_d(A_d(), term);
+    for (const auto & c : *term)
+        m_usage_in_terms[c.column()] = m_usage_in_terms[c.column()] + 1;
+
 }
 
 void lar_solver::add_basic_var_to_core_fields() {

src/math/lp/lar_solver.h

@@ -101,6 +101,7 @@ class lar_solver : public column_namer {
     std::unordered_map<lar_term, std::pair<mpq, unsigned>, term_hasher, term_comparer>
     m_normalized_terms_to_columns;
     vector<impq>                                        m_backup_x;
+    stacked_vector<unsigned>                            m_usage_in_terms;
     // end of fields
 
     ////////////////// methods ////////////////////////////////
@@ -467,9 +468,13 @@ class lar_solver : public column_namer {
             return -1;
         }
     }
-
+    unsigned usage_in_terms(column_index j) const {
+        if (j >= m_usage_in_terms.size())
+            return 0;
+        return m_usage_in_terms[j];
+    }
     friend int_solver;
     friend int_branch;
-
+    
 };
 }