revise unit walk

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

src/sat/sat_solver.h

@@ -226,6 +226,8 @@ namespace sat {
         void mk_clause(literal l1, literal l2, bool learned = false);
         void mk_clause(literal l1, literal l2, literal l3, bool learned = false);        
 
+        random_gen& rand() { return m_rand; }
+
     protected:
         inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; }
         inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; }

src/sat/sat_unit_walk.cpp

@@ -8,6 +8,7 @@ Module Name:
 Abstract:
 
     unit walk local search procedure.
+
     A variant of UnitWalk. Hirsch and Kojevinkov, SAT 2001.
     This version uses a trail to reset assignments and integrates directly with the 
     watch list structure. Thus, assignments are not delayed and we avoid treating
@@ -16,11 +17,9 @@ Abstract:
     It uses standard DPLL approach for backracking, flipping the last decision literal that
     lead to a conflict. It restarts after evern 100 conflicts.
 
-    It does not attempt to add conflict clauses or alternate with
+    It does not attempt to add conflict clauses 
-    walksat.
 
-    It can receive conflict clauses from a concurrent CDCL solver and does not
+    It can receive conflict clauses from a concurrent CDCL solver 
-    create its own conflict clauses.
 
     The phase of variables is optionally sticky between rounds. We use a decay rate
     to compute stickiness of a variable.
@@ -31,20 +30,52 @@ Author:
 
 Revision History:
 
+    2018-11-5:
+      change reinitialization to use local search with limited timeouts to find phase and ordering of variables.
+
 --*/
 
-#include "sat_unit_walk.h"
+#include "sat/sat_unit_walk.h"
+#include "util/luby.h"
+
 
 namespace sat {
 
+    bool_var unit_walk::var_priority::peek(solver& s) {
+        while (m_head < m_vars.size()) {
+            bool_var v = m_vars[m_head];
+            unsigned idx = literal(v, false).index();
+            if (s.m_assignment[idx] == l_undef)
+                return v;            
+            ++m_head;
+        }
+        for (bool_var v : m_vars) {
+            if (s.m_assignment[literal(v, false).index()] == l_undef) {
+                IF_VERBOSE(0, verbose_stream() << "unassigned: " << v << "\n");
+            }
+        }
+        IF_VERBOSE(0, verbose_stream() << "(sat.unit-walk sat)\n");
+        return null_bool_var;
+    }
+
+    void unit_walk::var_priority::set_vars(solver& s) {
+        m_vars.reset();
+        for (unsigned v = 0; v < s.num_vars(); ++v) {            
+            if (!s.was_eliminated(v) && s.m_assignment[v] == l_undef) {
+                add(v);
+            }
+        }
+    }
+
+    bool_var unit_walk::var_priority::next(solver& s) {
+        bool_var v = peek(s);
+        ++m_head;
+        return v;
+    }
+
     unit_walk::unit_walk(solver& s):
-        s(s)
+        s(s) {
-    {
+        m_max_conflicts = 10000;
-        m_runs = 0;
-        m_periods = 0;
-        m_max_runs = UINT_MAX;
-        m_max_periods = 5000; // UINT_MAX; // TBD configure
-        m_max_conflicts = 100;
         m_sticky_phase = s.get_config().m_phase_sticky;
         m_flips = 0;
     }                        
@@ -63,67 +94,177 @@ namespace sat {
     lbool unit_walk::operator()() {
         scoped_set_unit_walk _scoped_set(this, s);
         init_runs();
-        for (m_runs = 0; m_runs < m_max_runs || m_max_runs == UINT_MAX; ++m_runs) {
+        init_propagation();
-            init_propagation();
+        init_phase();
-            init_phase();
+        while (true) {
-            for (m_periods = 0; m_periods < m_max_periods || m_max_periods == UINT_MAX; ++m_periods) {
+            if (!s.rlimit().inc()) {
-                if (!s.rlimit().inc()) return l_undef;
+                log_status();
-                lbool r = unit_propagation();
+                return l_undef;
-                if (r != l_undef) return r;                
+            }
-            }        
+            bool_var v = pqueue().next(s);
-        }
+            if (v == null_bool_var) {
-        return l_undef;
+                log_status();
-    }
+                return l_true;
-
+            }
-    lbool unit_walk::unit_propagation() {
-        init_propagation();     
-        while (!m_freevars.empty() && !inconsistent()) {
-            bool_var v = m_freevars.begin()[m_rand(m_freevars.size())];
             literal lit(v, !m_phase[v]);
             ++s.m_stats.m_decision;
             m_decisions.push_back(lit);
+            // IF_VERBOSE(0, verbose_stream() << "push " << lit << " " << m_decisions.size() << "\n");
+            pqueue().push();
             assign(lit);
             propagate();
             while (inconsistent() && !m_decisions.empty()) {
-                ++m_conflicts;
+                update_max_trail();
-                backtrack();
+                ++s.m_stats.m_conflict;
+                pop();
+                pqueue().pop();
                 propagate();
             }
-            if (m_conflicts >= m_max_conflicts && !m_freevars.empty()) {
+            if (inconsistent()) {
-                set_conflict();
+                log_status();
-                break;
+                return l_false;
+            }
+            bool do_reinit = s.m_stats.m_conflict >= m_max_conflicts;
+            if (do_reinit || pqueue().depth() > m_decisions.size()) { //  || pqueue().depth() <= 10
+                switch (update_priority()) {
+                case l_true: return l_true;
+                case l_false: break; // TBD
+                default: break;
+                }
+            }
+            if (do_reinit) {
+                refresh_solver();
             }
         }
-        if (!inconsistent()) {
+    }
-            log_status();
+
-            IF_VERBOSE(1, verbose_stream() << "(sat-unit-walk sat)\n";);
+    void unit_walk::pop() {
-            s.mk_model();
+        SASSERT (!m_decisions.empty());
-            return l_true;
+        literal dlit = m_decisions.back();
+        pop_decision();
+        m_inconsistent = false;
+        assign(~dlit);
+    }
+
+    void unit_walk::pop_decision() {
+        SASSERT (!m_decisions.empty());
+        literal dlit = m_decisions.back();
+        // IF_VERBOSE(0, verbose_stream() << "pop " << dlit << " " << m_decisions.size() << "\n");
+        literal lit;
+        do {
+            SASSERT(!m_trail.empty());
+            lit = m_trail.back(); 
+            s.m_assignment[lit.index()] = l_undef;
+            s.m_assignment[(~lit).index()] = l_undef;
+            m_trail.pop_back();
         }
-        return l_undef;
+        while (lit != dlit);
+        m_qhead = m_trail.size();
+        m_decisions.pop_back();
     }
 
     void unit_walk::init_runs() {
-        m_freevars.reset();
+        m_luby_index = 0;
+        m_restart_threshold = 1000;
+        m_max_trail = 0;
         m_trail.reset();
         m_decisions.reset();
         m_phase.resize(s.num_vars());
-        double2 d2;
+        m_phase_tf.resize(s.num_vars(), ema(1e-5));
-        d2.t = 1.0;
+        pqueue().reset();
-        d2.f = 1.0;
+        pqueue().set_vars(s);
-        m_phase_tf.resize(s.num_vars(), d2);
+        for (unsigned v = 0; v < s.num_vars(); ++v) {            
-        for (unsigned i = 0; i < s.num_vars(); ++i) {
+            m_phase_tf[v].update(50);
-            literal l(i, false);
-            if (!s.was_eliminated(l.var()) && s.m_assignment[l.index()] == l_undef)
-                m_freevars.insert(l.var());
         }
-        IF_VERBOSE(1, verbose_stream() << "num vars: " << s.num_vars() << " free vars: " << m_freevars.size() << "\n";);
+        m_ls.import(s, true);
+        m_rand.set_seed(s.rand()());
+        update_priority();
+    }
+
+    lbool unit_walk::update_priority() {
+        unsigned prefix_length = 0;
+        if (pqueue().depth() > m_decisions.size()) {
+            while (pqueue().depth() > m_decisions.size()) {
+                pqueue().dec_depth();
+            }
+            prefix_length = m_trail.size();
+            SASSERT(pqueue().depth() == m_decisions.size());
+        }
+        else if (pqueue().depth() == m_decisions.size()) {
+            prefix_length = m_trail.size();
+        }
+        else {
+            literal last = m_decisions[pqueue().depth()];
+            while (m_trail[prefix_length++] != last) {}
+            pqueue().inc_depth();
+        }
+        log_status();
+        IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk :update-priority " << pqueue().depth() << ")\n");
+        for (unsigned v = 0; v < s.num_vars(); ++v) {
+            m_ls.set_bias(v, m_phase_tf[v] >= 50 ? l_true : l_false);
+        }
+        for (literal lit : m_trail) {
+            m_ls.set_bias(lit.var(), lit.sign() ? l_false : l_true);
+        }
+        m_ls.rlimit().push(std::max(1u, pqueue().depth()));
+        lbool is_sat = m_ls.check(0, m_trail.c_ptr(), nullptr);
+        m_ls.rlimit().pop();
+
+        TRACE("sat", tout << "result of running bounded local search " << is_sat << "\n";);
+        IF_VERBOSE(0, verbose_stream() << "result of running local search " << is_sat << "\n";);
+        if (is_sat != l_undef) {
+            restart();
+        }
+        if (is_sat == l_true) {
+            for (unsigned v = 0; v < s.num_vars(); ++v) {
+                s.m_assignment[v] = m_ls.get_phase(v) ? l_true : l_false;
+            } 
+        }
+        
+        struct compare_break {
+            local_search& ls;
+            compare_break(local_search& ls): ls(ls) {}
+            int operator()(bool_var v, bool_var w) const {
+                double diff = ls.break_count(v) - ls.break_count(w);
+                return diff > 0;
+            }
+        };
+        compare_break cb(m_ls);
+        std::sort(pqueue().begin(), pqueue().end(), cb);
+        pqueue().rewind();
+        // assert variables are sorted from highest to lowest value.
+        
+        for (bool_var v : pqueue()) {
+            if (m_ls.cur_solution(v))                 
+                m_phase_tf[v].update(100);
+            else
+                m_phase_tf[v].update(0);
+        }
+        init_phase();
+
+        // restart
+        bool_var v = pqueue().peek(s);
+        if (is_sat == l_undef && v != null_bool_var && false) {
+            unsigned num_levels = 0;
+            while (m_decisions.size() > 0 && num_levels <= 50) {
+                bool_var w = m_decisions.back().var();
+                if (num_levels >= 15 && m_ls.break_count(w) >= m_ls.break_count(v)) {
+                    break;
+                }
+                ++num_levels;
+                pop_decision();
+                if (pqueue().depth() > m_decisions.size()) {
+                    pqueue().pop();                
+                }                
+            }
+            IF_VERBOSE(0, verbose_stream() << "backtrack levels " << num_levels << "\n");
+        }
+        return is_sat;
     }
 
     void unit_walk::init_phase() {
-        m_max_trail = 0;
         if (m_sticky_phase) {
-            for (bool_var v : m_freevars) {
+            for (bool_var v : pqueue()) {
                 if (s.m_phase[v] == POS_PHASE) {
                     m_phase[v] = true;
                 }
@@ -131,35 +272,73 @@ namespace sat {
                     m_phase[v] = false;
                 }
                 else {
-                    m_phase[v] = m_rand(100 * static_cast<unsigned>(m_phase_tf[v].t + m_phase_tf[v].f)) <= 100 * m_phase_tf[v].t;
+                    m_phase[v] = m_rand(100) <= m_phase_tf[v];
                 }
             }
         }
         else {
-            for (bool_var v : m_freevars) 
+            for (bool_var v : pqueue()) 
                 m_phase[v] = (m_rand(2) == 0); 
         }
     }
 
+    void unit_walk::refresh_solver() {
+        m_max_conflicts += m_conflict_offset ;
+        m_conflict_offset += 100; // 00;
+        if (s.m_par && s.m_par->copy_solver(s)) {
+            IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk fresh copy)\n";);
+            if (s.get_extension()) s.get_extension()->set_unit_walk(this);
+            init_runs();
+            init_phase();
+        }
+        if (should_restart()) {
+            restart();
+        }
+    }
+
+    bool unit_walk::should_restart() {
+        if (s.m_stats.m_conflict >= m_restart_threshold) {
+            m_restart_threshold = s.get_config().m_restart_initial * get_luby(m_luby_index);
+            ++m_luby_index;
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
+    void unit_walk::restart() {
+        IF_VERBOSE(1, verbose_stream() << "restart\n");
+        while (!m_decisions.empty()) {
+            pop_decision();
+        }
+        pqueue().reset();
+    }
+
+    void unit_walk::update_max_trail() {
+        if (m_max_trail == 0 || m_trail.size() > m_max_trail) {
+            m_max_trail = m_trail.size();
+            m_restart_threshold += 10000;
+            m_max_conflicts = s.m_stats.m_conflict + 20000;
+            log_status();
+        }
+    }
+
     void unit_walk::init_propagation() {
         if (s.m_par && s.m_par->copy_solver(s)) {
-            IF_VERBOSE(1, verbose_stream() << "(sat-unit-walk fresh copy)\n";);
+            IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk fresh copy)\n";);
             if (s.get_extension()) s.get_extension()->set_unit_walk(this);
             init_runs();
             init_phase();
         }
-        if (m_max_trail == 0 || m_trail.size() > m_max_trail) {
-            m_max_trail = m_trail.size();
-            log_status();
-        }
         for (literal lit : m_trail) {
             s.m_assignment[lit.index()] = l_undef;
             s.m_assignment[(~lit).index()] = l_undef;
-            m_freevars.insert(lit.var());
         }
         m_flips = 0;
         m_trail.reset();
-        m_conflicts = 0;
+        s.m_stats.m_conflict = 0;
+        m_conflict_offset = 10000;
         m_decisions.reset();
         m_qhead = 0;
         m_inconsistent = false;
@@ -171,6 +350,20 @@ namespace sat {
         // IF_VERBOSE(1, verbose_stream() << m_trail.size() << " " << inconsistent() << "\n";);
     }
 
+    std::ostream& unit_walk::display(std::ostream& out) const {
+        unsigned i = 0;
+        out << "num decisions: " << m_decisions.size() << "\n";
+        for (literal lit : m_trail) {
+            if (i < m_decisions.size() && m_decisions[i] == lit) {
+                out << "d " << i << ": ";
+                ++i;
+            }
+            out << lit << "\n";
+        }
+        s.display(verbose_stream());
+        return out;
+    }
+
     void unit_walk::propagate(literal l) {
         ++s.m_stats.m_propagate;
         literal not_l = ~l;
@@ -289,11 +482,12 @@ namespace sat {
     }
 
     void unit_walk::assign(literal lit) {
-        SASSERT(value(lit) == l_undef);
+        VERIFY(value(lit) == l_undef);
+        //VERIFY(!m_trail.contains(lit));
+        //VERIFY(!m_trail.contains(~lit));
         s.m_assignment[lit.index()] = l_true;
         s.m_assignment[(~lit).index()] = l_false;
         m_trail.push_back(lit);
-        m_freevars.remove(lit.var());
         if (s.get_extension() && s.is_external(lit.var())) {
             s.get_extension()->asserted(lit);       
         } 
@@ -307,28 +501,23 @@ namespace sat {
         bool_var v = l.var();
         m_phase[v] = !m_phase[v]; 
         if (m_sticky_phase) {
-            m_phase_tf[v].f *= 0.98;
+            if (m_phase[v]) m_phase_tf[v].update(100); else m_phase_tf[v].update(0);
-            m_phase_tf[v].t *= 0.98;
-            if (m_phase[v]) m_phase_tf[v].t += 1; else m_phase_tf[v].f += 1;
         }
     }
 
     void unit_walk::log_status() {
-        IF_VERBOSE(1, verbose_stream() << "(sat-unit-walk :trail " << m_max_trail 
+        IF_VERBOSE(1, verbose_stream() 
-                   << " :branches " << m_decisions.size()
+                   << "(sat.unit-walk"
-                   << " :free " << m_freevars.size() 
+                   << " :trail " << m_trail.size()
-                   << " :periods " << m_periods                    
+                   << " :depth " << m_decisions.size()
                    << " :decisions " << s.m_stats.m_decision
                    << " :propagations " << s.m_stats.m_propagate
+                   << " :conflicts " << s.m_stats.m_conflict 
                    << ")\n";);        
     }
 
     literal unit_walk::choose_literal() {
-        SASSERT(m_qhead < m_trail.size());
+        return m_trail[m_qhead++];
-        unsigned idx = m_rand(m_trail.size() - m_qhead);
-        std::swap(m_trail[m_qhead], m_trail[m_qhead + idx]);
-        literal lit = m_trail[m_qhead++];
-        return lit;
     }
 
     void unit_walk::set_conflict(literal l1, literal l2) {
@@ -346,25 +535,6 @@ namespace sat {
     void unit_walk::set_conflict() {
         m_inconsistent = true; 
     }
-
-    void unit_walk::backtrack() {
-        if (m_decisions.empty()) return;
-        literal dlit = m_decisions.back();
-        literal lit;
-        do {
-            SASSERT(!m_trail.empty());
-            lit = m_trail.back(); 
-            s.m_assignment[lit.index()] = l_undef;
-            s.m_assignment[(~lit).index()] = l_undef;
-            m_freevars.insert(lit.var());            
-            m_trail.pop_back();
-        }
-        while (lit != dlit);
-        m_inconsistent = false;
-        m_decisions.pop_back();
-        m_qhead = m_trail.size();
-        assign(~dlit);
-    }
     
 };
 

src/sat/sat_unit_walk.h

@@ -20,43 +20,74 @@ Revision History:
 #define SAT_UNIT_WALK_H_
 
 #include "sat/sat_solver.h"
+#include "sat/sat_local_search.h"
+#include "util/ema.h"
 
 namespace sat {
 
     class unit_walk {
+#if 0
         struct double2 {
             double t, f;
         };
+#endif
+        class var_priority {
+            svector<bool_var> m_vars;
+            unsigned_vector   m_lim;
+            unsigned          m_head;
+            unsigned          m_depth;
+        public:
+            var_priority() { m_depth = 0; m_head = 0; }
+            void rewind() { m_head = 0; for (unsigned& l : m_lim) l = 0; }
+            unsigned depth() const { return m_depth; }
+            void inc_depth() { ++m_depth; }
+            void dec_depth() { --m_depth; }
+            void reset() { m_lim.reset(); m_head = 0; m_depth = 0; }
+            void add(bool_var v) { m_vars.push_back(v); }
+            bool_var next(solver& s);
+            bool_var peek(solver& s);
+            void set_vars(solver& s);
+            void push() { m_lim.push_back(m_head); }
+            void pop() { m_head = m_lim.back(); m_lim.pop_back(); }    
+            bool empty() const { return m_lim.empty(); }
+            bool_var const* begin() const { return m_vars.begin(); }
+            bool_var const* end() const { return m_vars.end(); }
+            bool_var* begin() { return m_vars.begin(); }
+            bool_var* end() { return m_vars.end(); }
+        };
+
         solver&           s;
+        local_search      m_ls;
         random_gen        m_rand;
         svector<bool>     m_phase;
-        svector<double2> m_phase_tf;
+        svector<ema>      m_phase_tf;
-        indexed_uint_set  m_freevars;
+        var_priority      m_priorities;
-        unsigned          m_runs;
+        unsigned          m_luby_index;
-        unsigned          m_periods;
+        unsigned          m_restart_threshold;
 
         // settings
-        unsigned          m_max_runs;
-        unsigned          m_max_periods;
         unsigned          m_max_conflicts;
         bool              m_sticky_phase;
 
-        unsigned          m_propagations;
         unsigned          m_flips;
         unsigned          m_max_trail;
         unsigned          m_qhead;
         literal_vector    m_trail;
         bool              m_inconsistent;
         literal_vector    m_decisions;
-        unsigned          m_conflicts;
+        unsigned          m_conflict_offset;
 
-        void push();
+        bool should_restart();
-        void backtrack();
+        void restart();
+        void pop();
+        void pop_decision();
         void init_runs();
+        lbool update_priority();
         void init_phase();
         void init_propagation();
+        void refresh_solver();
+        void update_max_trail();
         void flip_phase(literal l); 
-        lbool unit_propagation();
         void propagate();
         void propagate(literal lit);
         literal choose_literal();
@@ -65,6 +96,7 @@ namespace sat {
         void set_conflict(clause const& c);
         inline lbool value(literal lit) { return s.value(lit); }
         void log_status();
+        var_priority& pqueue() { return m_priorities; }
     public:
 
         unit_walk(solver& s);