Randomize lit to take

This means it will be more likely to be removed. When looking at another
lit, another time.

Author: msoos

src/comp_analyzer.cpp

@@ -277,10 +277,6 @@ void CompAnalyzer::initialize(
     assert(cl.size() > 2);
     const uint32_t long_cl_off = long_clauses_data.size();
 
-    Lit example_blocking = NOT_A_LIT;
-    auto& blk_lits = clid_to_blocking_lits[max_clid];
-    if (!blk_lits.empty()) example_blocking = blk_lits[0];
-
     if (cl.size() > 3) {
       Lit blk_lit = cl[cl.size()/2];
       for(const auto&l: cl) long_clauses_data.push_back(l);
@@ -291,7 +287,7 @@ void CompAnalyzer::initialize(
         ClData d;
         d.id = max_clid;
         d.blk_lit = blk_lit;
-        d.example_blocking = example_blocking;
+        d.example_blocking = NOT_A_LIT;
         d.off = long_cl_off;
         unif_occ_long[var].push_back(d);
       }
@@ -305,7 +301,7 @@ void CompAnalyzer::initialize(
         ClData d;
         d.id = max_clid;
         d.blk_lit = lits[0];
-        d.example_blocking = example_blocking;
+        d.example_blocking = NOT_A_LIT;
         d.off = lits[1].raw();
         unif_occ_long[l.var()].push_back(d);
       }
@@ -391,11 +387,17 @@ void CompAnalyzer::initialize(
       }
     }
 
-    // check longs
+    // check longs & adjust blocking lits to random ones
     for(uint32_t v = 0; v < unif_occ_long.size(); v++) {
       assert(unif_occ_long[v].size() == holder.size_long(v));
       for(uint32_t i = 0; i < unif_occ_long[v].size(); i++) {
         assert(unif_occ_long[v][i] == holder.begin_long(v)[i]);
+        auto& d = holder.begin_long(v)[i];
+        auto& blk_lits = clid_to_blocking_lits[d.id];
+        if (!blk_lits.empty()) {
+          std::uniform_int_distribution<uint32_t> dist(0, blk_lits.size()-1);
+          d.example_blocking = blk_lits[dist(mtrand)];
+        }
       }
     }
   }