ccc

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

contrib/cmake/src/sat/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(sat
     card_extension.cpp
     dimacs.cpp
     sat_asymm_branch.cpp
+    sat_ccc.cpp
     sat_clause.cpp
     sat_clause_set.cpp
     sat_clause_use_list.cpp

src/sat/card_extension.cpp

@@ -26,8 +26,7 @@ namespace sat {
         m_index(index),
         m_lit(lit),
         m_k(k),
-        m_size(lits.size())
+        m_size(lits.size()) {
-    {
         for (unsigned i = 0; i < lits.size(); ++i) {
             m_lits[i] = lits[i];
         }
@@ -42,6 +41,27 @@ namespace sat {
         SASSERT(m_size >= m_k && m_k > 0);
     }
 
+    card_extension::pb::pb(unsigned index, literal lit, svector<card_extension::wliteral> const& wlits, unsigned k):
+        m_index(index),
+        m_lit(lit),
+        m_k(k),
+        m_size(wlits.size()) {
+        for (unsigned i = 0; i < wlits.size(); ++i) {
+            m_wlits[i] = wlits[i];
+        }
+    }
+
+    void card_extension::pb::negate() {
+        m_lit.neg();
+        unsigned w = 0;
+        for (unsigned i = 0; i < m_size; ++i) {
+            m_wlits[i].second.neg();
+            w += m_wlits[i].first;
+        }
+        m_k = w - m_k + 1;
+        SASSERT(w >= m_k && m_k > 0);
+    }
+
     card_extension::xor::xor(unsigned index, literal lit, literal_vector const& lits):
         m_index(index),
         m_lit(lit),
@@ -191,6 +211,15 @@ namespace sat {
         SASSERT(s().inconsistent());
     }
 
+    // pb:
+    void card_extension::init_watch(pb& p, bool is_true) {
+        NOT_IMPLEMENTED_YET();
+    }
+
+
+
+
+    // xor:
     void card_extension::clear_watch(xor& x) {
         unwatch_literal(x[0], &x);
         unwatch_literal(x[1], &x);         
@@ -510,7 +539,7 @@ namespace sat {
                     process_card(c, offset);
                     ++m_stats.m_num_card_resolves;
                 }
-                else {
+                else if (is_xor_index(index)) {
                     // jus.push_back(js);
                     m_lemma.reset();
                     m_bound += offset;
@@ -521,6 +550,12 @@ namespace sat {
                     }
                     ++m_stats.m_num_xor_resolves;
                 }
+                else if (is_pb_index(index)) {
+                    NOT_IMPLEMENTED_YET();
+                }
+                else {
+                    UNREACHABLE();
+                }
                 break;
             }
             default:
@@ -758,7 +793,7 @@ namespace sat {
     }
 
     void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
-        unsigned index = 2*m_cards.size();
+        unsigned index = 4*m_cards.size();
         literal lit = v == null_bool_var ? null_literal : literal(v, false);
         card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
         m_cards.push_back(c);
@@ -774,9 +809,26 @@ namespace sat {
         }
     }
 
+    void card_extension::add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k) {
+        unsigned index = 4*m_pb.size() + 0x11;
+        literal lit = v == null_bool_var ? null_literal : literal(v, false);
+        pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
+        m_pb.push_back(p);
+        if (v == null_bool_var) {
+            init_watch(*p, true);
+            m_pb_axioms.push_back(p);
+        }
+        else {
+            init_watch(v);
+            m_var_infos[v].m_pb = p;
+            m_var_trail.push_back(v);
+        }
+    }
+
+
     void card_extension::add_xor(bool_var v, literal_vector const& lits) {
         m_has_xor = true;
-        unsigned index = 2*m_xors.size()+1;
+        unsigned index = 4*m_xors.size() + 0x01;
         xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, literal(v, false), lits);
         m_xors.push_back(x);
         init_watch(v);
@@ -819,7 +871,7 @@ namespace sat {
         unsigned level = lvl(l);
         bool_var v = l.var();
         SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION);
-        SASSERT(!is_card_index(js.get_ext_justification_idx()));
+        SASSERT(is_xor_index(js.get_ext_justification_idx()));
         TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";);
 
         unsigned num_marks = 0;
@@ -828,7 +880,7 @@ namespace sat {
             ++count;
             if (js.get_kind() == justification::EXT_JUSTIFICATION) {
                 unsigned idx = js.get_ext_justification_idx();
-                if (is_card_index(idx)) {
+                if (!is_xor_index(idx)) {
                     r.push_back(l);
                 }
                 else {
@@ -912,7 +964,7 @@ namespace sat {
                 r.push_back(~c[i]);
             }
         }
-        else {
+        else if (is_xor_index(idx)) {
             xor& x = index2xor(idx);
             if (x.lit() != null_literal) r.push_back(x.lit());
             TRACE("sat", display(tout << l << " ", x, true););
@@ -931,6 +983,12 @@ namespace sat {
                 r.push_back(value(x[i]) == l_true ? x[i] : ~x[i]);                
             }
         }
+        else if (is_pb_index(idx)) {
+            NOT_IMPLEMENTED_YET();
+        }
+        else {
+            UNREACHABLE();
+        }
     }
 
 
@@ -1281,13 +1339,19 @@ namespace sat {
             }
             out << ">= " << c.k();
         }
-        else {
+        else if (is_xor_index(idx)) {
             xor& x = index2xor(idx);
             out << "xor " << x.lit() << ": ";
             for (unsigned i = 0; i < x.size(); ++i) {
                 out << x[i] << " ";
             }            
         }
+        else if (is_pb_index(idx)) {
+            NOT_IMPLEMENTED_YET();
+        }
+        else {
+            UNREACHABLE();
+        }
         return out;
     }
 
@@ -1382,7 +1446,7 @@ namespace sat {
                 }
                 if (c.lit() != null_literal) p.push(~c.lit(), offset*c.k());
             }
-            else {
+            else if (is_xor_index(index)) {
                 literal_vector ls;
                 get_antecedents(lit, index, ls);                
                 p.reset(offset);
@@ -1392,6 +1456,12 @@ namespace sat {
                 literal lxor = index2xor(index).lit();                
                 if (lxor != null_literal) p.push(~lxor, offset);
             }
+            else if (is_pb_index(index)) {
+                NOT_IMPLEMENTED_YET();
+            }
+            else {
+                UNREACHABLE();
+            }
             break;
         }
         default:

src/sat/card_extension.h

@@ -58,6 +58,26 @@ namespace sat {
             void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
             void negate();                       
         };
+        
+        typedef std::pair<unsigned, literal> wliteral;
+
+        class pb {
+            unsigned       m_index;
+            literal        m_lit;
+            unsigned       m_k;
+            unsigned       m_size;
+            wliteral       m_wlits[0];
+        public:
+            static size_t get_obj_size(unsigned num_lits) { return sizeof(card) + num_lits * sizeof(wliteral); }
+            pb(unsigned index, literal lit, svector<wliteral> const& wlits, unsigned k);
+            unsigned index() const { return m_index; }
+            literal lit() const { return m_lit; }
+            wliteral operator[](unsigned i) const { return m_wlits[i]; }
+            unsigned k() const { return m_k; }
+            unsigned size() const { return m_size; }
+            void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
+            void negate();                       
+        };
 
         class xor {
             unsigned       m_index;
@@ -85,20 +105,28 @@ namespace sat {
 
         typedef ptr_vector<card> card_watch;
         typedef ptr_vector<xor> xor_watch;
+        typedef ptr_vector<pb>  pb_watch;
         struct var_info {
             card_watch* m_card_watch[2];
+            pb_watch*   m_pb_watch[2];
             xor_watch*  m_xor_watch;
             card*       m_card;
+            pb*         m_pb;
             xor*        m_xor;
-            var_info(): m_xor_watch(0), m_card(0), m_xor(0) {
+            var_info(): m_xor_watch(0), m_card(0), m_xor(0), m_pb(0) {
                 m_card_watch[0] = 0;
                 m_card_watch[1] = 0;
+                m_pb_watch[0] = 0;
+                m_pb_watch[1] = 0;
             }
             void reset() {
                 dealloc(m_card);
                 dealloc(m_xor);
+                dealloc(m_pb);
                 dealloc(card_extension::set_tag_non_empty(m_card_watch[0]));
                 dealloc(card_extension::set_tag_non_empty(m_card_watch[1]));
+                dealloc(card_extension::set_tag_non_empty(m_pb_watch[0]));
+                dealloc(card_extension::set_tag_non_empty(m_pb_watch[1]));
                 dealloc(card_extension::set_tag_non_empty(m_xor_watch));
             }
         };
@@ -125,8 +153,10 @@ namespace sat {
 
         ptr_vector<card>    m_cards;
         ptr_vector<xor>     m_xors;
+        ptr_vector<pb>      m_pb;
 
         scoped_ptr_vector<card> m_card_axioms;
+        scoped_ptr_vector<pb>   m_pb_axioms;
 
         // watch literals
         svector<var_info>   m_var_infos;
@@ -173,11 +203,17 @@ namespace sat {
         lbool add_assign(xor& x, literal alit);
         void asserted_xor(literal l, ptr_vector<xor>* xors, xor* x);
 
-        bool is_card_index(unsigned idx) const { return 0 == (idx & 0x1); }
+        bool is_card_index(unsigned idx) const { return 0x00 == (idx & 0x11); }
-        card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 1]; }
+        bool is_xor_index(unsigned idx) const { return 0x01 == (idx & 0x11); }
-        xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 1]; }
+        bool is_pb_index(unsigned idx) const { return 0x11 == (idx & 0x11); }
+        card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 2]; }
+        xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 2]; }
+        pb&  index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pb[idx >> 2]; }
+
         void get_xor_antecedents(literal l, unsigned inddex, justification js, literal_vector& r);
 
+        void init_watch(pb& p, bool is_true);
+
 
         template<typename T>
         bool remove(ptr_vector<T>& ts, T* t) {
@@ -233,6 +269,7 @@ namespace sat {
         virtual ~card_extension();
         virtual void set_solver(solver* s) { m_solver = s; }
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
+        void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void    add_xor(bool_var v, literal_vector const& lits);
         virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
         virtual bool resolve_conflict();

src/sat/sat_ccc.cpp

@@ -0,0 +1,271 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_ccc.cpp
+
+Abstract:
+   
+    A variant of Concurrent Cube and Conquer
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-4-17
+
+Notes:
+
+--*/
+
+#include "sat_solver.h"
+#include "sat_lookahead.h"
+#include "sat_ccc.h"
+
+using namespace sat;
+
+lbool ccc::cube() {
+    unsigned branch_id = 0;
+    unsigned_vector id_trail;
+
+    lookahead lh(s);
+    lh.init_search();
+    lh.m_model.reset();
+
+    lookahead::scoped_level _sl(lh, lh.c_fixed_truth);
+    literal_vector trail;
+    lh.m_search_mode = lookahead_mode::searching;
+    while (!m_cancel) {
+        // remove old branch ids from id_trail.
+        while (id_trail.size() > trail.size()) {
+            id_trail.pop_back();
+        }
+        TRACE("sat", lh.display(tout););
+        lh.inc_istamp();
+        s.checkpoint();
+        if (lh.inconsistent()) {
+            if (!lh.backtrack(trail)) return l_false;
+            continue;
+        }
+
+        // check if CDCL solver got ahead.
+        bool repeat = false;
+        #pragma omp critical (ccc_solved)
+        {
+            if (!m_solved.empty()) {
+                unsigned solved_id = m_solved.top();
+                if (id_trail.contains(solved_id)) {
+                    lh.set_conflict();
+                }
+                else {
+                    m_solved.pop();
+                }
+                repeat = true;
+            }
+        }
+        if (repeat) continue;
+
+        ++branch_id;
+        if (!trail.empty()) {
+            #pragma omp critical (ccc_decisions)
+            {
+                m_decisions.push(decision(branch_id, trail.size()-1, trail.back()));
+            }
+        }
+
+        literal l = lh.choose();
+        if (lh.inconsistent()) {
+            if (!lh.backtrack(trail)) return l_false;
+            continue;
+        }
+        if (l == null_literal) {
+            m_model = lh.get_model();
+            return l_true;
+        }
+
+        // update trail and set of ids
+        id_trail.push_back(branch_id);
+        trail.push_back(l);
+        SASSERT(id_trail.size() == trail.size());
+
+        TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
+        ++lh.m_stats.m_decisions;
+        IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";);
+        lh.push(l, lh.c_fixed_truth);
+        SASSERT(lh.inconsistent() || !lh.is_unsat());
+    }
+    return l_undef;
+}
+
+lbool ccc::conquer(solver& s) {
+    try {
+        if (s.inconsistent()) return l_false;
+        s.init_search();
+        s.propagate(false);
+        if (s.inconsistent()) return l_false;
+        s.init_assumptions(0, 0);
+        s.propagate(false);
+        if (s.check_inconsistent()) return l_false;
+        s.cleanup();
+        s.simplify_problem();
+        if (s.check_inconsistent()) return l_false;
+
+        unsigned_vector ids;
+        
+        while (true) {
+            SASSERT(!s.inconsistent());
+            
+            lbool r = bounded_search(s, ids);
+            if (r != l_undef)
+                return r;
+            
+            if (s.m_conflicts > s.m_config.m_max_conflicts) {
+                IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << s.m_conflicts << "\")\n";);
+                return l_undef;
+            }
+            
+            s.restart();
+            s.simplify_problem();
+            if (s.check_inconsistent()) return l_false;
+            s.gc();                       
+        }
+    }
+    catch (solver::abort_solver) {
+        return l_undef;
+    }
+}
+
+lbool ccc::bounded_search(solver& s, unsigned_vector& ids) {
+    decision d;
+
+    while (true) {
+        s.checkpoint();
+        bool done = false;
+        while (!done) {
+            lbool is_sat = s.propagate_and_backjump_step(done); 
+            if (is_sat != l_true) return is_sat;
+        }
+
+        if (s.m_scope_lvl < ids.size()) {
+            while (ids.size() > s.m_scope_lvl + 1) ids.pop_back();
+            unsigned id = ids.back();
+            ids.pop_back();
+            #pragma omp critical (ccc_solved)
+            {
+                m_solved.push(id);
+            }
+        }
+
+        s.gc();
+
+        bool cube_decision = false;
+        #pragma omp critical (ccc_decisions)
+        {
+            if (!m_decisions.empty()) {
+                d = m_decisions.pop();
+                cube_decision = true;
+            }
+        }
+        if (cube_decision) {
+            if (d.m_depth > ids.size()) continue;
+            ids.push_back(d.m_id);
+            s.pop_reinit(s.m_scope_lvl - d.m_depth); // TBD: check alignment of scopes
+            s.push();
+            s.assign(d.m_last, justification());
+        }
+        else if (!s.decide()) {
+            lbool is_sat = s.final_check();
+            if (is_sat != l_undef) {
+                return is_sat;
+            }
+        }
+    }
+}
+
+
+lbool ccc::search() {
+    enum par_exception_kind {
+        DEFAULT_EX,
+        ERROR_EX
+    };
+
+    m_cancel = false;
+
+    scoped_limits      scoped_rlimit(s.rlimit());
+    vector<reslimit>   limits;
+    ptr_vector<solver> solvers;
+    int finished_id = -1;
+    std::string        ex_msg;
+    par_exception_kind ex_kind;
+    unsigned error_code = 0;
+    lbool result = l_undef;
+    bool canceled = false;
+
+    int num_threads = s.m_config.m_num_threads + 1;
+    for (int i = 1; i < num_threads; ++i) {
+        limits.push_back(reslimit());
+    }
+
+    for (int i = 1; i < num_threads; ++i) {
+        s.m_params.set_uint("random_seed", s.m_rand());
+        solvers[i] = alloc(sat::solver, s.m_params, limits[i]);
+        solvers[i]->copy(s);
+        scoped_rlimit.push_child(&solvers[i]->rlimit());            
+    }
+
+    #pragma omp parallel for
+    for (int i = 0; i < num_threads; ++i) {
+        try {                
+            lbool r = l_undef;
+            if (i == 0) {
+                r = cube();
+            }
+            else {
+                r = conquer(*solvers[i-1]);
+            }
+            bool first = false;
+            #pragma omp critical (par_solver)
+            {
+                if (finished_id == -1) {
+                    finished_id = i;
+                    first = true;
+                    result = r;
+                }
+            }
+            if (first) {
+                for (unsigned j = 0; j < solvers.size(); ++j) {
+                    solvers[j]->rlimit().cancel();
+                }
+                // cancel lookahead solver:
+                m_cancel = true;
+            }
+        }
+        catch (z3_error & err) {
+            error_code = err.error_code();
+            ex_kind = ERROR_EX;                
+        }
+        catch (z3_exception & ex) {
+            ex_msg = ex.msg();
+            ex_kind = DEFAULT_EX;    
+        }
+    }
+
+    if (finished_id > 0 && result == l_true) {
+        // set model from auxiliary solver
+        m_model = solvers[finished_id - 1]->get_model();
+    }
+
+    for (unsigned i = 0; i < solvers.size(); ++i) {            
+        dealloc(solvers[i]);
+    }
+    
+    if (finished_id == -1) {
+        switch (ex_kind) {
+        case ERROR_EX: throw z3_error(error_code);
+            default: throw default_exception(ex_msg.c_str());
+        }
+    }
+
+
+    return result;
+}
+

src/sat/sat_ccc.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_ccc.h
+
+Abstract:
+   
+    A variant of Concurrent Cube and Conquer
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-4-17
+
+Notes:
+
+--*/
+#ifndef _SAT_CCC_H_
+#define _SAT_CCC_H_
+
+#include "queue.h"
+
+namespace sat {
+
+    class ccc {
+        struct decision {
+            unsigned m_id;
+            unsigned m_depth;
+            literal  m_last;
+            decision(unsigned id, unsigned d, literal last):
+                m_id(id), m_depth(d), m_last(last) {}
+            decision(): m_id(0), m_depth(0), m_last(null_literal) {}
+        };
+
+        solver&         s;    
+        queue<unsigned> m_solved;
+        queue<decision> m_decisions;
+        model           m_model;
+        volatile bool   m_cancel;
+
+        struct config {
+            config() {
+            }
+        };
+
+        struct stats {
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        lbool conquer(solver& s);
+        lbool bounded_search(solver& s, unsigned_vector& ids);
+
+        lbool cube();
+
+    public:
+        ccc(solver& s): s(s) {}
+
+        lbool search();
+              
+    };
+}
+
+#endif
+

src/sat/sat_config.cpp

@@ -82,6 +82,7 @@ namespace sat {
         m_max_conflicts   = p.max_conflicts();
         m_num_threads     = p.threads();
         m_local_search    = p.local_search();
+        m_local_search_threads    = p.local_search_threads();
         m_lookahead_search = p.lookahead_search();
 
         // These parameters are not exposed

src/sat/sat_config.h

@@ -58,7 +58,8 @@ namespace sat {
         unsigned           m_burst_search;
         unsigned           m_max_conflicts;
         unsigned           m_num_threads;
-        unsigned           m_local_search;
+        unsigned           m_local_search_threads;
+        bool               m_local_search;
         bool               m_lookahead_search;
 
         unsigned           m_simplify_mult1;

src/sat/sat_lookahead.h

@@ -61,6 +61,8 @@ namespace sat {
     class lookahead {
         solver& s;
 
+        friend class ccc;
+
         struct config {
             double   m_dl_success;
             float    m_alpha;
@@ -70,6 +72,7 @@ namespace sat {
             unsigned m_level_cand;
             float    m_delta_rho;
             unsigned m_dl_max_iterations;
+            unsigned m_tc1_limit;
 
             config() {
                 m_max_hlevel = 50;
@@ -79,6 +82,7 @@ namespace sat {
                 m_level_cand = 600;
                 m_delta_rho = (float)0.9995;
                 m_dl_max_iterations = 32;
+                m_tc1_limit = 10000000;
             }
         };
 
@@ -126,6 +130,8 @@ namespace sat {
         vector<literal_vector> m_binary;        // literal: binary clauses
         unsigned_vector        m_binary_trail;  // trail of added binary clauses
         unsigned_vector        m_binary_trail_lim; 
+        unsigned               m_num_tc1;
+        unsigned_vector        m_num_tc1_lim;
         unsigned               m_qhead;         // propagation queue head
         unsigned_vector        m_qhead_lim;
         clause_vector          m_clauses;       // non-binary clauses
@@ -314,8 +320,11 @@ namespace sat {
                         assign(u);        
                         return false;
                     }
-                    IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";);
+                    if (m_num_tc1 < m_config.m_tc1_limit) {
-                    add_binary(u, w);
+                        ++m_num_tc1;
+                        IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";);
+                        add_binary(u, w);
+                    }
                 }
             }
             return true;
@@ -1055,11 +1064,10 @@ namespace sat {
             unsigned trail_sz = s.init_trail_size();
             for (unsigned i = 0; i < trail_sz; ++i) {
                 literal l = s.m_trail[i];
-				if (!s.was_eliminated(l.var()))
+                if (!s.was_eliminated(l.var())) {
-				{
+                    if (s.m_config.m_drat) m_drat.add(l, false);
-					if (s.m_config.m_drat) m_drat.add(l, false);
+                    assign(l);
-					assign(l);
+                }
-				}
             }
             propagate();
             m_qhead = m_trail.size();
@@ -1090,6 +1098,7 @@ namespace sat {
             SASSERT(m_search_mode == lookahead_mode::searching);
             m_binary_trail_lim.push_back(m_binary_trail.size());
             m_trail_lim.push_back(m_trail.size());
+            m_num_tc1_lim.push_back(m_num_tc1);
             m_retired_clause_lim.push_back(m_retired_clauses.size());
             m_retired_ternary_lim.push_back(m_retired_ternary.size());
             m_qhead_lim.push_back(m_qhead);
@@ -1116,6 +1125,9 @@ namespace sat {
             }
             m_trail.shrink(old_sz); // reset assignment.
             m_trail_lim.pop_back();
+            
+            m_num_tc1 = m_num_tc1_lim.back();
+            m_num_tc1_lim.pop_back();
 
             // unretire clauses
             old_sz = m_retired_clause_lim.back();
@@ -1792,11 +1804,17 @@ namespace sat {
             return out;
         }
 
+        void init_search() {
+            m_search_mode = lookahead_mode::searching;
+            scoped_level _sl(*this, c_fixed_truth);
+            init();            
+        }
 
     public:
         lookahead(solver& s) : 
             s(s), 
             m_drat(s),
+            m_num_tc1(0),
             m_level(2),
             m_prefix(0) {
         }
@@ -1806,11 +1824,7 @@ namespace sat {
         }
         
         lbool check() {
-            {
+            init_search();
-                m_search_mode = lookahead_mode::searching;
-                scoped_level _sl(*this, c_fixed_truth);
-                init();
-            }
             return search();
         }
 

src/sat/sat_params.pyg

@@ -28,6 +28,7 @@ def_module_params('sat',
                           ('drat.check', BOOL, False, 'build up internal proof and check'),
                           ('cardinality.solver', BOOL, False, 'use cardinality solver'),
 	                  ('xor.solver', BOOL, False, 'use xor solver'),
-                          ('local_search', UINT, 0, 'number of local search threads to find satisfiable solution'),
+                          ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
+                          ('local_search', BOOL, False, 'use local search instead of CDCL'),
                           ('lookahead_search', BOOL, False, 'use lookahead solver')
                        ))

src/sat/sat_solver.cpp

@@ -787,7 +787,10 @@ namespace sat {
         if (m_config.m_lookahead_search && num_lits == 0) {
             return lookahead_search();
         }
-        if ((m_config.m_num_threads > 1 || m_config.m_local_search > 0) && !m_par) {
+        if (m_config.m_local_search) {
+            return do_local_search(num_lits, lits);
+        }
+        if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0) && !m_par) {
             return check_par(num_lits, lits);
         }
         flet<bool> _searching(m_searching, true);
@@ -859,6 +862,18 @@ namespace sat {
         ERROR_EX
     };
 
+    lbool solver::do_local_search(unsigned num_lits, literal const* lits) {
+        scoped_limits scoped_rl(rlimit());
+        local_search srch;
+        srch.config().set_seed(m_config.m_random_seed);
+        srch.import(*this, false);
+        scoped_rl.push_child(&srch.rlimit());
+        lbool r = srch.check(num_lits, lits, 0);
+        m_model = srch.get_model();
+        // srch.collect_statistics(m_lookahead_stats);
+        return r;
+    }
+
     lbool solver::lookahead_search() {
         lookahead lh(*this);
         lbool r = l_undef;
@@ -876,9 +891,9 @@ namespace sat {
 
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
         scoped_ptr_vector<local_search> ls;
-        int num_threads = static_cast<int>(m_config.m_num_threads + m_config.m_local_search);
+        int num_threads = static_cast<int>(m_config.m_num_threads + m_config.m_local_search_threads);
         int num_extra_solvers = m_config.m_num_threads - 1;
-        int num_local_search  = static_cast<int>(m_config.m_local_search);
+        int num_local_search  = static_cast<int>(m_config.m_local_search_threads);
         for (int i = 0; i < num_local_search; ++i) {
             local_search* l = alloc(local_search);
             l->config().set_seed(m_config.m_random_seed + i);

src/sat/sat_solver.h

@@ -160,6 +160,7 @@ namespace sat {
         friend class lookahead;
         friend class local_search;
         friend struct mk_stat;
+        friend class ccc;
     public:
         solver(params_ref const & p, reslimit& l);
         ~solver();
@@ -349,6 +350,7 @@ namespace sat {
         void exchange_par();
         lbool check_par(unsigned num_lits, literal const* lits);
         lbool lookahead_search();
+        lbool do_local_search(unsigned num_lits, literal const* lits);
 
         // -----------------------
         //
@@ -465,7 +467,7 @@ namespace sat {
         lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_vector>& conseq);
 
         // initialize and retrieve local search.
-        local_search& init_local_search();
+        // local_search& init_local_search();
 
     private:
 

src/util/memory_manager.cpp

@@ -57,6 +57,7 @@ static void throw_out_of_memory() {
     {
         g_memory_out_of_memory = true;
     }
+
     if (g_exit_when_out_of_memory) {
         std::cerr << g_out_of_memory_msg << "\n";
         exit(ERR_MEMOUT);

src/util/queue.h

@@ -0,0 +1,61 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    queue.h
+
+Abstract:
+   
+    Generic queue.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-4-17
+
+Notes:
+
+--*/
+#ifndef _QUEUE_H_
+#define _QUEUE_H_
+
+#include "vector.h"
+
+template<class T>
+class queue {
+    vector<T> m_elems;
+    unsigned  m_head;
+    unsigned  m_capacity;
+    
+public:
+    
+    queue(): m_head(0), m_capacity(0) {}
+
+    void push(T const& t) { m_elems.push_back(t); }
+
+    bool empty() const { 
+        return m_head == m_elems.size(); 
+    }
+
+    T top() const {
+        return m_elems[m_head];
+    }
+
+    T pop() { 
+        SASSERT(!empty());
+        m_capacity = std::max(m_capacity, m_elems.size());
+        SASSERT(m_head < m_elems.size()); 
+        if (2 * m_head > m_capacity && m_capacity > 10) {
+            for (unsigned i = 0; i < m_elems.size() - m_head; ++i) {
+                m_elems[i] = m_elems[i + m_head];
+            }
+            m_elems.shrink(m_elems.size() - m_head);
+            m_head = 0;
+        } 
+        return m_elems[m_head++];        
+    }
+
+};
+
+#endif
+