sketch backbone code

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/smt_context.cpp

@@ -279,6 +279,7 @@ namespace smt {
         m_assignment[(~l).index()] = l_false;
         bool_var_data & d          = get_bdata(l.var());
         set_justification(l.var(), d, j);
+        ++m_phase_scores[l.sign()][l.var()];
         d.m_scope_lvl              = m_scope_lvl;
         if (m_fparams.m_restart_adaptive && d.m_phase_available) {
             m_agility             *= m_fparams.m_agility_factor;

src/smt/smt_context.h

@@ -191,7 +191,6 @@ namespace smt {
         unsigned_vector             m_lit_occs;    //!< occurrence count of literals
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
-        // updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
 
         struct lit_node : dll_base<lit_node> {
             literal lit;
@@ -200,6 +199,7 @@ namespace smt {
         lit_node* m_dll_lits;
 
         svector<double> m_lit_scores[2];
+        svector<double> m_phase_scores[2];
 
         clause_vector               m_aux_clauses;
         clause_vector               m_lemmas;

src/smt/smt_internalizer.cpp

@@ -933,8 +933,11 @@ namespace smt {
         m_activity.reserve(v+1);
         m_lit_scores[0].reserve(v + 1);
         m_lit_scores[1].reserve(v + 1);
-
         m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
+        m_phase_scores[0].reserve(v + 1);
+        m_phase_scores[1].reserve(v + 1);
+        m_phase_scores[0][v] = m_phase_scores[1][v] = 0.0;
+
         m_bool_var2expr.reserve(v+1);
         m_bool_var2expr[v] = n;
         literal l(v, false);

src/smt/smt_parallel.cpp

@@ -559,6 +559,90 @@ namespace smt {
         }
     }
 
+    expr_ref_vector parallel::worker::find_backbone_candidates() {
+        expr_ref_vector backbone_candidates(m);
+        // Find backbone candidates based on the current state of the worker
+
+        unsigned k = 5;
+        svector<std::pair<double, expr*>> top_k; // will hold at most k elements
+
+        for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
+            if (ctx->get_assignment(v) != l_undef)
+                continue;
+            expr* e = ctx->bool_var2expr(v);
+            if (!e)
+                continue;
+
+            auto score1 = ctx->m_phase_scores[0][v]; // assigned to true
+            auto score2 = ctx->m_phase_scores[1][v]; // assigned to false
+
+            ctx->m_phase_scores[0][v] /= 2; // decay the scores
+            ctx->m_phase_scores[1][v] /= 2;
+
+            if (score1 == 0 && score2 == 0)
+                continue;
+
+            if (score1 == 0) {
+                backbone_candidates.push_back(expr_ref(e, m));
+                continue;
+            }
+
+            if (score2 == 0) {
+                backbone_candidates.push_back(expr_ref(m.mk_not(e), m));
+                continue;
+            }
+
+            if (score1 == score2)
+                continue;
+
+            if (score1 >= score2) {
+                double ratio = score1 / score2;
+//                insert by absolute value
+            }
+            else {
+                double ratio = - score2 / score1;
+                //                insert by absolute value
+            }
+        }
+        // post-process top_k to get the top k elements
+
+        return backbone_candidates;
+    }
+
+    // 
+    // Assume the negation of all candidates (or a batch of them)
+    // run the solver with a low budget of conflicts
+    // if the unsat core contains a single candidate we have found a backbone literal
+    // 
+    void parallel::worker::test_backbone_candidates(expr_ref_vector const& candidates) {
+
+        unsigned sz = asms.size();
+        for (expr* e : candidates)
+            asms.push_back(mk_not(m, e));
+
+        ctx->get_fparams().m_max_conflicts = 100;
+        lbool r = l_undef;
+        try {
+            r = ctx->check(asms.size(), asms.data());
+        }
+        catch (z3_error& err) {
+            b.set_exception(err.error_code());
+        }
+        catch (z3_exception& ex) {
+            b.set_exception(ex.what());
+        }
+        catch (...) {
+            b.set_exception("unknown exception");
+        }
+        asms.shrink(sz);
+        if (r == l_false) {
+            auto core = ctx->unsat_core();
+            LOG_WORKER(2, " backbone core:\n"; for (auto c : core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n");                          
+        }
+
+        // TODO
+    }
+
     expr_ref_vector parallel::worker::get_split_atoms() {
         unsigned k = 2;
 

src/smt/smt_parallel.h

@@ -144,6 +144,9 @@ namespace smt {
             void update_max_thread_conflicts() {
                 m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
             } // allow for backoff scheme of conflicts within the thread for cube timeouts.
+
+            expr_ref_vector find_backbone_candidates();
+            void test_backbone_candidates(expr_ref_vector const& candidates);
         public:
             worker(unsigned id, parallel& p, expr_ref_vector const& _asms);
             void run();