Trying example blocking lit

msoos · msoos · commit 4c9ede14811b · 2025-03-16T20:22:25.000+01:00
diff --git a/src/comp_analyzer.cpp b/src/comp_analyzer.cpp
@@ -30,6 +30,7 @@ THE SOFTWARE.
 #include <cstdint>
 #include <cstdint>
 #include <memory>
+#include <ratio>
 
 using namespace GanakInt;
 
@@ -40,6 +41,160 @@ inline std::ostream& operator<<(std::ostream& os, const ClData& d)
   return os;
 }
 
+void CompAnalyzer::calc_blocked(
+    const LiteralIndexedVector<LitWatchList> & watches,
+    const ClauseAllocator* alloc, const vector<ClauseOfs>& long_irred_cls)
+{
+  const uint32_t n = max_var+1;
+  lit_to_blocked_clids.resize(n*2);
+  if (counter->get_opt_indep_support_end() >= max_var+1) {
+    verb_print(1, "No need to calculate blocked clauses, as all vars are opt independent");
+    return;
+  }
+  const double start_time = cpu_time();
+
+  // build occ lists
+  vector<vector<Lit>> id_to_cl;
+  vector<vector<uint32_t>> occs;
+  occs.resize(n*2);
+  uint32_t clid_bin_start;
+
+  if (true) {
+    uint32_t clid = 1;
+    id_to_cl.resize(1);
+    vector<Lit> tmp;
+    for (const auto& off: long_irred_cls) {
+      const Clause& cl = *alloc->ptr(off);
+      assert(cl.size() > 2);
+      tmp.clear();
+      tmp.insert(tmp.end(), cl.begin(), cl.end());
+      for(const auto& l: cl) occs[l.raw()].push_back(clid);
+      id_to_cl.push_back(tmp);
+      assert(id_to_cl.size()-1 == clid);
+      clid++;
+    }
+    clid_bin_start = clid;
+
+    for (uint32_t v = 1; v < n; v++) {
+      for(uint32_t i = 0; i < 2; i++) {
+        Lit l(v, i);
+        for (const auto& bincl: watches[l].binaries) {
+          if (bincl.irred()) {
+            tmp.clear();
+            tmp.push_back(l);
+            tmp.push_back(bincl.lit());
+            occs[tmp[0].raw()].push_back(clid);
+            occs[tmp[1].raw()].push_back(clid);
+            id_to_cl.push_back(tmp);
+            assert(id_to_cl.size()-1 == clid);
+            clid++;
+          }
+        }
+      }
+    }
+  }
+
+  uint32_t blocked_tot = 0;
+  vector<char> seen(n*2, 0);
+  vector<char> seen_set(n*2, 0);
+  vector<Lit> seed_set_clear;
+  for (uint32_t v = 1; v < n; v++) {
+    for(uint32_t i = 0; i < 2; i++) {
+      vector<uint32_t> clids_blocked;
+      Lit l_set(v, i);
+      cout << "lit set: " << l_set << endl;
+      vector<Lit> prop_q;
+      prop_q.push_back(l_set);
+      // slow propagation..
+      /* SLOW_DEBUG_DO(for(const auto& l: seen_set) assert(l == 0)); */
+      for(const auto& l: seen_set) assert(l == 0);
+      while(!prop_q.empty()) {
+        Lit p = prop_q.back();
+        seen_set[p.raw()] = 1;
+        seed_set_clear.push_back(p);
+        prop_q.pop_back();
+        for(const auto& cl_id: occs[l_set.neg().raw()]) {
+          const auto& cl = id_to_cl[cl_id];
+          bool sat = false;
+          uint32_t unk = 0;
+          Lit lit_unk = Lit();
+          for(const auto& l: cl) {
+            if (seen_set[l.raw()]) {
+              sat = 1;
+              break;
+            }
+            if (seen[l.neg().raw()]) continue;
+            unk++;
+            lit_unk = l;
+            if (unk > 1) break;
+          }
+          if (sat) continue;
+          if (unk == 1) prop_q.push_back(lit_unk);
+        }
+      }
+
+      for(uint32_t clid = 1; clid < clid_bin_start; clid++) {
+        const auto& cl = id_to_cl[clid-1];
+
+        // already satisfied
+        bool sat_already = false;
+        for(const auto& l: cl) if (seen_set[l.raw()]) {
+          sat_already = true;
+          break;
+        }
+        if (sat_already) continue;
+
+        // cannot actually be blocked
+        bool could_be_blocked = false;
+        for(const auto& l: cl) if (l.var() >= counter->get_opt_indep_support_end()) {
+          could_be_blocked = true;
+          break;
+        }
+        if (!could_be_blocked) continue;
+        /* cout << "cl to block: " << cl << endl; */
+
+        bool blocked = false;
+        /* SLOW_DEBUG_DO(for(const auto& l: seen) assert(l == 0)); */
+        for(const auto& l: seen) assert(l == 0);
+        for(const auto& l: cl) seen[l.raw()] = 1;
+        for(const auto& l: cl) if (l.var() >= counter->get_opt_indep_support_end()) {
+          // could be blocked on this var
+          // must be blocked relative to all other clauses it could be resolved with
+          blocked = true;
+          for(const auto& clid2: occs[l.neg().raw()]) {
+            bool blocked_rel_this = false;
+            const auto& cl2 = id_to_cl[clid2];
+            for(const auto& l2: cl2) {
+              if (l2.neg() == l) continue; // resolve on this, skip
+              if (seen_set[l2.raw()]|| seen[l2.neg().raw()]) { //satisfied or blocked
+                /* cout << "blocked with cl2 " << cl2 << " on: " << l2 << " -- actually, set instead? " << (int)(l2 == l_set) << endl; */
+                blocked_rel_this = true;
+                break;
+              }
+            }
+            if (!blocked_rel_this) {
+              blocked = false;
+              break;
+            }
+          }
+          if (!blocked) continue; // try next var
+          if (blocked) {
+            cout << "BINGO! cl: " << cl << " blocked on: " << l << " given: " << l_set << endl;
+            clids_blocked.push_back(clid);
+            break;
+          }
+        }
+        for(const auto& l: cl) seen[l.raw()] = 0;
+      }
+
+      blocked_tot += clids_blocked.size();
+      lit_to_blocked_clids[l_set.raw()] = clids_blocked;
+    }
+    for(const auto& l: seed_set_clear) seen_set[l.raw()] = 0;
+  }
+  verb_print(1, "Blocked tot: " << blocked_tot << " avg: " << (double)blocked_tot/(double)(n*2-2) << " T: " << cpu_time()-start_time);
+}
+
 // Builds occ lists and sets things up, Done exactly ONCE for a whole counting runkk
 // this sets up unif_occ
 void CompAnalyzer::initialize(
@@ -60,7 +215,8 @@ void CompAnalyzer::initialize(
     return a.size() < b.size();
   };
   auto long_irred_cls = _long_irred_cls;
-  std::sort(long_irred_cls.begin(), long_irred_cls.end(), mysorter);
+  std::stable_sort(long_irred_cls.begin(), long_irred_cls.end(), mysorter);
+  calc_blocked(watches, alloc, long_irred_cls);
 
   max_clid = 1;
   max_tri_clid = 1;
@@ -74,17 +230,34 @@ void CompAnalyzer::initialize(
     const Clause& cl = *alloc->ptr(off);
     assert(cl.size() > 2);
     const uint32_t long_cl_off = long_clauses_data.size();
+
+      Lit example_blocking = NOT_A_LIT;
+      bool found = false;
+      for (int32_t v = n-1; v >= 1; v--) {
+        for(uint32_t i2 = 0; i2 < 2; i2++) {
+          Lit b = Lit(v, i2);
+          const auto& list = lit_to_blocked_clids[b.raw()];
+          if (std::find(list.begin(), list.end(), max_clid) != list.end()) {
+            example_blocking = b;
+            cout << "Example blocking: " << example_blocking << " for cl: " << cl << " id: " << max_clid << endl;
+            found = true;
+            break;
+          }
+        }
+        if (found) break;
+      }
+
     if (cl.size() > 3) {
       Lit blk_lit = cl[cl.size()/2];
       for(const auto&l: cl) long_clauses_data.push_back(l);
       long_clauses_data.push_back(SENTINEL_LIT);
-
       for(const auto& l: cl) {
         const uint32_t var = l.var();
         assert(var < n);
         ClData d;
         d.id = max_clid;
         d.blk_lit = blk_lit;
+        d.example_blocking = example_blocking;
         d.off = long_cl_off;
         unif_occ_long[var].push_back(d);
       }
@@ -98,6 +271,7 @@ void CompAnalyzer::initialize(
         ClData d;
         d.id = max_clid;
         d.blk_lit = lits[0];
+        d.example_blocking = example_blocking;
         d.off = lits[1].raw();
         unif_occ_long[l.var()].push_back(d);
       }
@@ -342,7 +516,8 @@ void CompAnalyzer::record_comp(const uint32_t var, const uint32_t sup_comp_long_
         if (archetype.clause_unvisited_in_sup_comp(d.id)) {
           const Lit l1 = d.get_lit1();
           const Lit l2 = d.get_lit2();
-          if (is_true(l1) || is_true(l2)) {
+          if (is_true(l1) || is_true(l2) ||
+              (d.example_blocking != NOT_A_LIT && is_true(d.example_blocking))) {
             archetype.clear_cl(d.id);
             sat = true;
             /* goto end_sat; */
@@ -355,7 +530,8 @@ void CompAnalyzer::record_comp(const uint32_t var, const uint32_t sup_comp_long_
         } else continue;
       } else {
         if (archetype.clause_unvisited_in_sup_comp(d.id)) {
-          if (is_true(d.blk_lit)) {
+          if (is_true(d.blk_lit) ||
+              (d.example_blocking != NOT_A_LIT && is_true(d.example_blocking))) {
             archetype.clear_cl(d.id);
             sat = true;
             goto end_sat;
diff --git a/src/comp_analyzer.hpp b/src/comp_analyzer.hpp
@@ -52,6 +52,7 @@ struct ClData {
   uint32_t id;
   uint32_t off;
   Lit blk_lit;
+  Lit example_blocking = NOT_A_LIT;
   bool operator==(const ClData& other) const {
     return id == other.id && off == other.off && blk_lit == other.blk_lit;
   }
@@ -178,6 +179,10 @@ class CompAnalyzer {
   CompArchetype& get_archetype() { return archetype; }
 
 private:
+  void calc_blocked(const LiteralIndexedVector<LitWatchList> & literals,
+      const ClauseAllocator* alloc, const vector<ClauseOfs>& long_irred_cls);
+  vector<vector<uint32_t>> lit_to_blocked_clids;
+
   // the id of the last clause
   // note that clause ID is the clause number,
   // different from the offset of the clause in the literal pool
