working on adding basic cores to efficient SAT solver

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

src/muz/pdr/pdr_smt_context_manager.h

@@ -21,7 +21,6 @@ Revision History:
 #define _PDR_SMT_CONTEXT_MANAGER_H_
 
 #include "smt_kernel.h"
-#include "sat_solver.h"
 #include "func_decl_dependencies.h"
 #include "dl_util.h"
 

src/sat/sat_params.pyg

@@ -17,4 +17,5 @@ def_module_params('sat',
                           ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
                           ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
-                          ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses')))
+                          ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
+                          ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

src/sat/sat_solver.cpp

@@ -685,8 +685,8 @@ namespace sat {
     // Search
     //
     // -----------------------
-    lbool solver::check() {
+    lbool solver::check(unsigned num_lits, literal const* lits) {
-        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";);
+        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the efficient SAT solver)\n";);
         SASSERT(scope_lvl() == 0);
 #ifdef CLONE_BEFORE_SOLVING
         if (m_mc.empty()) {
@@ -697,6 +697,7 @@ namespace sat {
         try {
             if (inconsistent()) return l_false;
             init_search();
+            init_assumptions(num_lits, lits);
             propagate(false);
             if (inconsistent()) return l_false;
             cleanup();
@@ -706,6 +707,7 @@ namespace sat {
                 if (r != l_undef)
                     return r;
                 pop(scope_lvl());
+                reinit_assumptions();
                 m_conflicts_since_restart = 0;
                 m_restart_threshold       = m_config.m_restart_initial;
             }
@@ -851,6 +853,40 @@ namespace sat {
         }
     }
 
+    void solver::init_assumptions(unsigned num_lits, literal const* lits) {
+        if (num_lits == 0) {
+            return;
+        }
+        push();
+        m_assumptions.reset();
+        m_assumption_set.reset();
+        for (unsigned i = 0; i < num_lits; ++i) {
+            literal l = lits[i];
+            SASSERT(is_external(l.var()));
+            m_assumption_set.insert(l);
+            m_assumptions.push_back(l);
+            mk_clause(1, &l); 
+        }
+    }
+
+    void solver::reinit_assumptions() {
+        if (tracking_assumptions()) {
+            push();
+            for (unsigned i = 0; i < m_assumptions.size(); ++i) {
+                literal l = m_assumptions[i];
+                mk_clause(1, &l); 
+            }
+        }
+    }
+
+    bool solver::tracking_assumptions() const {
+        return !m_assumptions.empty();
+    }
+
+    bool solver::is_assumption(literal l) const {
+        return tracking_assumptions() && m_assumption_set.contains(l);
+    }
+
     void solver::init_search() {
         m_phase_counter           = 0;
         m_phase_cache_on          = false;
@@ -986,6 +1022,7 @@ namespace sat {
                    << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
         IF_VERBOSE(30, display_status(verbose_stream()););
         pop(scope_lvl());
+        reinit_assumptions();
         m_conflicts_since_restart = 0;
         switch (m_config.m_restart) {
         case RS_GEOMETRIC:
@@ -1305,7 +1342,7 @@ namespace sat {
 
     bool solver::resolve_conflict() {
         while (true) {
-            bool r = resolve_conflict_core();
+            bool r = resolve_conflict_core(false);
             CASSERT("sat_check_marks", check_marks());
             // after pop, clauses are reinitialized, this may trigger another conflict.
             if (!r)
@@ -1315,7 +1352,7 @@ namespace sat {
         }
     }
 
-    bool solver::resolve_conflict_core() {
+    bool solver::resolve_conflict_core(bool generate_core) {
         TRACE("sat_conflict", tout << "conflict detected\n";);
 
         m_stats.m_conflict++;
@@ -1324,8 +1361,21 @@ namespace sat {
         m_conflicts_since_gc++;
 
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
-        if (m_conflict_lvl == 0)
+        if (!generate_core && m_conflict_lvl <= 1 && tracking_assumptions()) {
+            resolve_conflict_core(true);
+            m_core.reset();
+            for (unsigned i = 0; i < m_lemma.size(); ++i) {
+                literal l = ~m_lemma[i];
+                if (is_assumption(l)) {
+                    m_core.push_back(l);
+                }
+            }
             return false;
+        }
+        if (m_conflict_lvl == 0) {
+            return false;
+        }
+
         m_lemma.reset();
 
         forget_phase_of_vars(m_conflict_lvl);
@@ -1337,7 +1387,7 @@ namespace sat {
         unsigned num_marks = 0;
         if (m_not_l != null_literal) {
             TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";);
-            process_antecedent(m_not_l, num_marks);
+            process_antecedent(generate_core, m_not_l, num_marks);
         }
 
         literal consequent = m_not_l;
@@ -1350,11 +1400,11 @@ namespace sat {
             case justification::NONE:
                 break;
             case justification::BINARY:
-                process_antecedent(~(js.get_literal()), num_marks);
+                process_antecedent(generate_core, ~(js.get_literal()), num_marks);
                 break;
             case justification::TERNARY:
-                process_antecedent(~(js.get_literal1()), num_marks);
+                process_antecedent(generate_core, ~(js.get_literal1()), num_marks);
-                process_antecedent(~(js.get_literal2()), num_marks);
+                process_antecedent(generate_core, ~(js.get_literal2()), num_marks);
                 break;
             case justification::CLAUSE: {
                 clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
@@ -1365,13 +1415,13 @@ namespace sat {
                         i = 1;
                     }
                     else {
-                        process_antecedent(~c[0], num_marks);
+                        process_antecedent(generate_core, ~c[0], num_marks);
                         i = 2;
                     }
                 }
                 unsigned sz  = c.size();
                 for (; i < sz; i++)
-                    process_antecedent(~c[i], num_marks);
+                    process_antecedent(generate_core, ~c[i], num_marks);
                 break;
             }
             case justification::EXT_JUSTIFICATION: {
@@ -1379,7 +1429,7 @@ namespace sat {
                 literal_vector::iterator it  = m_ext_antecedents.begin();
                 literal_vector::iterator end = m_ext_antecedents.end();
                 for (; it != end; ++it)
-                    process_antecedent(*it, num_marks);
+                    process_antecedent(generate_core, *it, num_marks);
                 break;
             }
             default:
@@ -1408,7 +1458,7 @@ namespace sat {
         m_lemma[0] = ~consequent;
         TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 
-        if (m_config.m_minimize_lemmas) {
+        if (m_config.m_minimize_lemmas && !generate_core) {
             minimize_lemma();
             reset_lemma_var_marks();
             if (m_config.m_dyn_sub_res)
@@ -1431,15 +1481,24 @@ namespace sat {
 
         pop(m_scope_lvl - new_scope_lvl);
         TRACE("sat_conflict_detail", display(tout); tout << "assignment:\n"; display_assignment(tout););
-        clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
+        if (!generate_core) {
-        if (lemma) {
+            clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
-            lemma->set_glue(glue);
+            if (lemma) {
+                lemma->set_glue(glue);
+            }
         }
         decay_activity();
         updt_phase_counters();
         return true;
     }
 
+    void solver::mk_unsat_core() {
+        m_core.reset();
+        m_not_l;
+        m_conflict;
+        
+    }
+
     unsigned solver::get_max_lvl(literal consequent, justification js) {
         if (!m_ext)
             return scope_lvl();
@@ -1514,14 +1573,14 @@ namespace sat {
         return idx;
     }
 
-    void solver::process_antecedent(literal antecedent, unsigned & num_marks) {
+    void solver::process_antecedent(bool generate_core, literal antecedent, unsigned & num_marks) {
         bool_var var     = antecedent.var();
         unsigned var_lvl = lvl(var);
         SASSERT(var < num_vars());
         if (!is_marked(var) && var_lvl > 0) {
             mark(var);
             inc_activity(var);
-            if (var_lvl == m_conflict_lvl)
+            if (var_lvl == m_conflict_lvl && !generate_core)
                 num_marks++;
             else
                 m_lemma.push_back(~antecedent);

src/sat/sat_solver.h

@@ -118,6 +118,9 @@ namespace sat {
         stopwatch               m_stopwatch;
         params_ref              m_params;
         scoped_ptr<solver>      m_clone; // for debugging purposes
+        literal_vector          m_assumptions;
+        literal_set             m_assumption_set;
+        literal_vector          m_core;
 
         void del_clauses(clause * const * begin, clause * const * end);
 
@@ -250,8 +253,9 @@ namespace sat {
         //
         // -----------------------
     public:
-        lbool check();
+        lbool check(unsigned num_lits = 0, literal const* lits = 0);
         model const & get_model() const { return m_model; }
+        literal_vector const& get_core() const { return m_core; }
         model_converter const & get_model_converter() const { return m_mc; }
 
     protected:
@@ -267,6 +271,11 @@ namespace sat {
         bool_var next_var();
         lbool bounded_search();
         void init_search();
+        void init_assumptions(unsigned num_lits, literal const* lits);
+        void reinit_assumptions();
+        bool tracking_assumptions() const;
+        bool is_assumption(literal l) const;
+        void mk_unsat_core();
         void simplify_problem();
         void mk_model();
         bool check_model(model const & m) const;
@@ -311,9 +320,9 @@ namespace sat {
         literal_vector m_lemma;
         literal_vector m_ext_antecedents;
         bool resolve_conflict();
-        bool resolve_conflict_core();
+        bool resolve_conflict_core(bool generate_core);
         unsigned get_max_lvl(literal consequent, justification js);
-        void process_antecedent(literal antecedent, unsigned & num_marks);
+        void process_antecedent(bool generate_coe, literal antecedent, unsigned & num_marks);
         void fill_ext_antecedents(literal consequent, justification js);
         unsigned skip_literals_above_conflict_level();
         void forget_phase_of_vars(unsigned from_lvl);

src/sat/tactic/atom2bool_var.cpp

@@ -90,8 +90,9 @@ struct collect_boolean_interface_proc {
     template<typename T>
     void operator()(T const & g) {
         unsigned sz = g.size();
-        for (unsigned i = 0; i < sz; i++)
+        for (unsigned i = 0; i < sz; i++) {
             process(g.form(i));
+        }
     }
     
     void operator()(unsigned sz, expr * const * fs) {

src/sat/tactic/goal2sat.cpp

@@ -360,14 +360,40 @@ struct goal2sat::imp {
         SASSERT(m_result_stack.empty());
     }
 
+    void add_assumption(expr* d, expr* literal_d) {
+        
+    }
+
 
     void operator()(goal const & g) {
         m_interface_vars.reset();
         collect_boolean_interface(g, m_interface_vars);
-        
         unsigned size = g.size();
+        expr_ref f(m), d_new(m);
+        ptr_vector<expr> deps;
         for (unsigned idx = 0; idx < size; idx++) {
-            expr * f = g.form(idx);
+            f = g.form(idx);
+            // Add assumptions.
+            if (g.dep(idx)) {
+                expr_dependency * dep = g.dep(idx);
+                deps.reset();
+                m.linearize(dep, deps);
+                for (unsigned i = 0; i < deps.size(); ++i) {
+                    expr * d = deps[i];
+                    expr * d1;
+                    SASSERT(m.is_bool(d));
+                    if (is_uninterp_const(d)) {
+                        add_assumption(d, d);
+                    }
+                    else if (m.is_not(d, d1) && is_uninterp_const(d1)) {
+                        add_assumption(d, d);
+                    }
+                    else {
+                        // create fresh variable, map back to dependency.
+                        add_assumption(d, d_new);
+                    }
+                }
+            }
             process(f);
         }
     }

src/sat/tactic/sat_tactic.cpp

@@ -46,8 +46,8 @@ class sat_tactic : public tactic {
                         expr_dependency_ref & core) {
             mc = 0; pc = 0; core = 0;
             fail_if_proof_generation("sat", g);
-            fail_if_unsat_core_generation("sat", g);
             bool produce_models = g->models_enabled();
+            bool produce_core = g->unsat_core_enabled();
             TRACE("before_sat_solver", g->display(tout););
             g->elim_redundancies();
 

src/shell/dimacs_frontend.cpp

@@ -22,6 +22,7 @@ Revision History:
 #include"timeout.h"
 #include"dimacs.h"
 #include"sat_solver.h"
+#include"gparams.h"
 
 extern bool          g_display_statistics;
 static sat::solver * g_solver = 0;
@@ -63,11 +64,73 @@ static void display_model(sat::solver const & s) {
     std::cout << "\n";
 }
 
+static void display_core(sat::solver const& s, vector<sat::literal_vector> const& tracking_clauses) {
+    std::cout << "core\n";
+    sat::literal_vector const& c = s.get_core();
+    for (unsigned i = 0; i < c.size(); ++i) {
+        sat::literal_vector const& cls = tracking_clauses[c[i].var()];
+        for (unsigned j = 0; j < cls.size(); ++j) {
+            std::cout << cls[j] << " ";
+        }
+        std::cout << "\n";
+    }
+}
+
+static void track_clause(sat::solver& dst,
+                         sat::literal_vector& lits,
+                         sat::literal_vector& assumptions,
+                         vector<sat::literal_vector>& tracking_clauses) {
+    sat::literal lit = sat::literal(dst.mk_var(true, false), false);
+    tracking_clauses.set(lit.var(), lits);
+    lits.push_back(~lit);
+    dst.mk_clause(lits.size(), lits.c_ptr());
+    assumptions.push_back(lit);            
+}
+
+
+static void track_clauses(sat::solver const& src, 
+                          sat::solver& dst, 
+                          sat::literal_vector& assumptions,
+                          vector<sat::literal_vector>& tracking_clauses) {
+    for (sat::bool_var v = 0; v < src.num_vars(); ++v) {
+        dst.mk_var(false, true);
+    }
+    sat::literal_vector lits;
+    sat::literal lit;
+    sat::clause * const * it  = src.begin_clauses();
+    sat::clause * const * end = src.end_clauses();
+    svector<sat::solver::bin_clause> bin_clauses;
+    src.collect_bin_clauses(bin_clauses, false);
+    tracking_clauses.reserve(2*src.num_vars() + (end - it) + bin_clauses.size());
+
+    for (sat::bool_var v = 1; v < src.num_vars(); ++v) {
+        if (src.value(v) != l_undef) {
+            bool sign = src.value(v) == l_false;
+            lits.reset();
+            lits.push_back(sat::literal(v, sign));
+            track_clause(dst, lits, assumptions, tracking_clauses);
+        }
+    }
+    for (; it != end; ++it) {
+        lits.reset();
+        sat::clause& cls = *(*it);
+        lits.append(cls.end()-cls.begin(), cls.begin());
+        track_clause(dst, lits, assumptions, tracking_clauses);
+    }
+    for (unsigned i = 0; i < bin_clauses.size(); ++i) {
+        lits.reset();
+        lits.push_back(bin_clauses[i].first);
+        lits.push_back(bin_clauses[i].second);        
+        track_clause(dst, lits, assumptions, tracking_clauses);
+    }
+}
+
+
 unsigned read_dimacs(char const * file_name) {
     g_start_time = clock();
     register_on_timeout_proc(on_timeout);
     signal(SIGINT, on_ctrl_c);
-    params_ref p;
+    params_ref p = gparams::get_module("sat");
     p.set_bool("produce_models", true);
     sat::solver solver(p, 0);
     g_solver = &solver;
@@ -85,17 +148,32 @@ unsigned read_dimacs(char const * file_name) {
     }
     IF_VERBOSE(20, solver.display_status(verbose_stream()););
     
-    lbool r = solver.check();
+    lbool r;
+    vector<sat::literal_vector> tracking_clauses;
+    sat::solver solver2(p, 0);
+    if (p.get_bool("dimacs.core", false)) {
+        g_solver = &solver2;        
+        sat::literal_vector assumptions;
+        track_clauses(solver, solver2, assumptions, tracking_clauses);
+        solver2.display(std::cout);
+        r = g_solver->check(assumptions.size(), assumptions.c_ptr());
+    }
+    else {
+        r = g_solver->check();
+    }
     switch (r) {
     case l_true: 
         std::cout << "sat\n"; 
-        display_model(solver);
+        display_model(*g_solver);
         break;
     case l_undef: 
         std::cout << "unknown\n"; 
         break;
     case l_false: 
         std::cout << "unsat\n"; 
+        if (p.get_bool("dimacs.core", false)) {
+            display_core(*g_solver, tracking_clauses);
+        }
         break;
     }
     if (g_display_statistics)