variations on unit-walk

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

src/sat/sat_config.cpp

@@ -90,6 +90,7 @@ namespace sat {
         m_unit_walk       = p.unit_walk();
         m_unit_walk_threads = p.unit_walk_threads();
         m_lookahead_simplify = p.lookahead_simplify();
+        m_lookahead_double = p.lookahead_double();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
         if (p.lookahead_reward() == symbol("heule_schur")) 
             m_lookahead_reward = heule_schur_reward;

src/sat/sat_config.h

@@ -128,6 +128,7 @@ namespace sat {
         double             m_lookahead_cube_psat_clause_base;
         double             m_lookahead_cube_psat_trigger;
         reward_t           m_lookahead_reward;
+        bool               m_lookahead_double;
         bool               m_lookahead_global_autarky;
         double             m_lookahead_delta_fraction;
         bool               m_lookahead_use_learned;

src/sat/sat_local_search.cpp

@@ -591,18 +591,40 @@ namespace sat {
         m_unsat_stack.push_back(c);
     }
 
+    void local_search::pick_flip_lookahead() {
+        unsigned num_unsat = m_unsat_stack.size();
+        constraint const& c = m_constraints[m_unsat_stack[m_rand() % num_unsat]];
+        literal best = null_literal;
+        unsigned best_make = UINT_MAX;
+        for (literal lit : c.m_literals) {
+            if (!is_unit(lit) && is_true(lit)) {
+                flip_walksat(lit.var());
+                if (propagate(~lit) && best_make > m_unsat_stack.size()) {
+                    best = lit;
+                    best_make = m_unsat_stack.size();
+                }
+                flip_walksat(lit.var());
+                propagate(lit);
+            }
+        }
+        if (best != null_literal) {
+            flip_walksat(best.var());
+            propagate(~best);
+        }        
+        else {
+            std::cout << "no best\n";
+        }
+    }
+
     void local_search::pick_flip_walksat() {
     reflip:
         bool_var best_var = null_bool_var;
         unsigned n = 1;
         bool_var v = null_bool_var;
         unsigned num_unsat = m_unsat_stack.size();
-        constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]];
+        constraint const& c = m_constraints[m_unsat_stack[m_rand() % num_unsat]];
-        // VERIFY(c.m_k < constraint_value(c));
         unsigned reflipped = 0;
         bool is_core = m_unsat_stack.size() <= 10;
-        // TBD: dynamic noise strategy 
-        //if (m_rand() % 100 < 98) {
         if (m_rand() % 10000 <= m_noise) {
             // take this branch with 98% probability.
             // find the first one, to fast break the rest    

src/sat/sat_local_search.h

@@ -202,6 +202,7 @@ namespace sat {
         void init_slack();
         void init_scores();
         void init_goodvars();        
+        void pick_flip_lookahead();
         void pick_flip_walksat();
         void flip_walksat(bool_var v);
         bool propagate(literal lit);

src/sat/sat_lookahead.cpp

@@ -1812,7 +1812,7 @@ namespace sat {
 
     unsigned lookahead::do_double(literal l, unsigned& base) {
         unsigned num_units = 0;
-        if (!inconsistent() && dl_enabled(l)) {
+        if (!inconsistent() && dl_enabled(l) && get_config().m_lookahead_double) {
             if (get_lookahead_reward(l) > m_delta_trigger) {
                 if (dl_no_overflow(base)) {
                     ++m_stats.m_double_lookahead_rounds;
@@ -2013,6 +2013,7 @@ namespace sat {
     }
 
     bool lookahead::backtrack(literal_vector& trail, svector<bool> & is_decision) {
+        m_cube_state.m_backtracks++;
         while (inconsistent()) {
             if (trail.empty()) return false;
             if (is_decision.back()) {
@@ -2033,6 +2034,7 @@ namespace sat {
     void lookahead::update_cube_statistics(statistics& st) {
         st.update("lh cube cutoffs", m_cube_state.m_cutoffs);
         st.update("lh cube conflicts", m_cube_state.m_conflicts);        
+        st.update("lh cube backtracks", m_cube_state.m_backtracks);        
     }
 
     double lookahead::psat_heur() {

src/sat/sat_lookahead.h

@@ -181,6 +181,7 @@ namespace sat {
             double         m_psat_threshold;
             unsigned       m_conflicts;
             unsigned       m_cutoffs;
+            unsigned       m_backtracks;
             cube_state() { reset(); }
             void reset() { 
                 m_first = true;
@@ -190,7 +191,7 @@ namespace sat {
                 m_psat_threshold = dbl_max;
                 reset_stats();
             }
-            void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }
+            void reset_stats() { m_conflicts = 0; m_cutoffs = 0; m_backtracks = 0;}
             void inc_conflict() { ++m_conflicts; }
             void inc_cutoff() { ++m_cutoffs; }
         };

src/sat/sat_params.pyg

@@ -72,6 +72,7 @@ def_module_params('sat',
                           ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'),
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
+                          ('lookahead.double', BOOL, True, 'enable doubld lookahead'),
                           ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'),
                           ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
                           ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),

src/sat/sat_unit_walk.cpp

@@ -76,7 +76,6 @@ namespace sat {
     unit_walk::unit_walk(solver& s):
         s(s) {
         m_max_conflicts = 10000;
-        m_sticky_phase = s.get_config().m_phase_sticky;
         m_flips = 0;
     }                        
 
@@ -96,60 +95,64 @@ namespace sat {
         init_runs();
         init_propagation();
         init_phase();
-        while (true) {
+        lbool st = l_undef;
-            if (!s.rlimit().inc()) {
+        while (s.rlimit().inc() && st == l_undef) {
-                log_status();
+            if (inconsistent() && !m_decisions.empty()) do_pop();
-                return l_undef;
+            else if (inconsistent()) st = l_false; 
-            }
+            else if (should_backjump()) st = do_backjump();
-            bool_var v = pqueue().next(s);
+            else st = decide();
-            if (v == null_bool_var) {
-                log_status();
-                return l_true;
-            }
-            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()) {
-                update_max_trail();
-                ++s.m_stats.m_conflict;
-                pop();
-                pqueue().pop();
-                propagate();
-            }
-            if (inconsistent()) {
-                log_status();
-                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();
-            }
         }
+        log_status();
+        return st;
+    }
+
+    void unit_walk::do_pop() {
+        update_max_trail();
+        ++s.m_stats.m_conflict;
+        pop();
+        propagate();
+    }
+
+    lbool unit_walk::decide() {
+        bool_var v = pqueue().next(s);
+        if (v == null_bool_var) {
+            return l_true;
+        }
+        literal lit(v, !m_phase[v]);
+        ++s.m_stats.m_decision;
+        m_decisions.push_back(lit);
+        pqueue().push();
+        assign(lit);
+        propagate();
+        return l_undef;
+    }
+
+    bool unit_walk::should_backjump() {
+        return 
+            s.m_stats.m_conflict >= m_max_conflicts && m_decisions.size() > 20;
+    } 
+
+    lbool unit_walk::do_backjump() {
+        unsigned backjump_level = m_decisions.size(); // - (m_decisions.size()/20);
+        switch (update_priority(backjump_level)) {
+        case l_true: return l_true;
+        case l_false: break; // TBD
+        default: break;
+        }
+        refresh_solver();
+        return l_undef;
     }
 
     void unit_walk::pop() {
         SASSERT (!m_decisions.empty());
         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());
@@ -161,6 +164,8 @@ namespace sat {
         while (lit != dlit);
         m_qhead = m_trail.size();
         m_decisions.pop_back();
+        pqueue().pop();
+        m_inconsistent = false;
     }
 
     void unit_walk::init_runs() {
@@ -178,120 +183,100 @@ namespace sat {
         }
         m_ls.import(s, true);
         m_rand.set_seed(s.rand()());
-        update_priority();
+        update_priority(0);
     }
 
-    lbool unit_walk::update_priority() {
+    lbool unit_walk::do_local_search(unsigned num_rounds) {
-        unsigned prefix_length = 0;
+        unsigned prefix_length = (0*m_trail.size())/10;
-        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()));
+        m_ls.rlimit().push(num_rounds);
-        lbool is_sat = m_ls.check(0, m_trail.c_ptr(), nullptr);
+        lbool is_sat = m_ls.check(prefix_length, 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() {
+    lbool unit_walk::update_priority(unsigned level) {
-        if (m_sticky_phase) {
+
-            for (bool_var v : pqueue()) {
+        while (m_decisions.size() > level) {
-                if (s.m_phase[v] == POS_PHASE) {
+            pop_decision();
-                    m_phase[v] = true;
-                }
-                else if (s.m_phase[v] == NEG_PHASE) {
-                    m_phase[v] = false;
-                }
-                else {
-                    m_phase[v] = m_rand(100) <= m_phase_tf[v];
-                }
-            }
         }
-        else {
+        IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk :update-priority " << m_decisions.size() << "\n");
-            for (bool_var v : pqueue()) 
+
-                m_phase[v] = (m_rand(2) == 0); 
+        unsigned num_rounds = 50;
+        log_status();
+
+        lbool is_sat = do_local_search(num_rounds);
+        switch (is_sat) {
+        case l_true:
+            for (unsigned v = 0; v < s.num_vars(); ++v) {
+                s.m_assignment[v] = m_ls.get_phase(v) ? l_true : l_false;
+            } 
+            return l_true;
+        case l_false:
+            if (m_decisions.empty()) {
+                return l_false;
+            }
+            else {
+                pop();
+                return l_undef;
+            }
+        default:
+            update_pqueue();
+            return l_undef;
+        }        
+    }
+
+    /**
+     * \brief Reshuffle variables in the priority queue using the break counts from local search.
+     */
+    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;
+        }
+    };
+
+    void unit_walk::update_pqueue() {
+        compare_break cb(m_ls);
+        std::sort(pqueue().begin(), pqueue().end(), cb);        
+        for (bool_var v : pqueue()) {
+            m_phase_tf[v].update(m_ls.cur_solution(v) ? 100 : 0);
+            m_phase[v] = m_ls.cur_solution(v);
+        }
+        pqueue().rewind();
+    }
+
+    void unit_walk::init_phase() {
+        for (bool_var v : pqueue()) {
+            if (s.m_phase[v] == POS_PHASE) {
+                m_phase[v] = true;
+            }
+            else if (s.m_phase[v] == NEG_PHASE) {
+                m_phase[v] = false;
+            }
+            else {
+                m_phase[v] = m_rand(100) < m_phase_tf[v];
+            }
         }
     }
 
     void unit_walk::refresh_solver() {
         m_max_conflicts += m_conflict_offset ;
-        m_conflict_offset += 100; // 00;
+        m_conflict_offset += 10000;
         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()) {
+        if (false && should_restart()) {
             restart();
         }
     }
@@ -308,11 +293,9 @@ namespace sat {
     }
 
     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() {
@@ -483,8 +466,6 @@ namespace sat {
 
     void unit_walk::assign(literal lit) {
         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);
@@ -494,15 +475,13 @@ namespace sat {
         if (m_phase[lit.var()] == lit.sign()) {
             ++m_flips;
             flip_phase(lit);
+            m_phase_tf[lit.var()].update(m_phase[lit.var()] ? 100 : 0);        
         }
     }
 
     void unit_walk::flip_phase(literal l) {
         bool_var v = l.var();
         m_phase[v] = !m_phase[v]; 
-        if (m_sticky_phase) {
-            if (m_phase[v]) m_phase_tf[v].update(100); else m_phase_tf[v].update(0);
-        }
     }
 
     void unit_walk::log_status() {

src/sat/sat_unit_walk.h

@@ -35,14 +35,10 @@ namespace sat {
             svector<bool_var> m_vars;
             unsigned_vector   m_lim;
             unsigned          m_head;
-            unsigned          m_depth;
         public:
-            var_priority() { m_depth = 0; m_head = 0; }
+            var_priority() { m_head = 0; }
-            void rewind() { m_head = 0; for (unsigned& l : m_lim) l = 0; }
+            void reset() { m_lim.reset(); m_head = 0;}
-            unsigned depth() const { return m_depth; }
+            void rewind() { for (unsigned& l : m_lim) l = 0; m_head = 0;}
-            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);
@@ -67,7 +63,6 @@ namespace sat {
 
         // settings
         unsigned          m_max_conflicts;
-        bool              m_sticky_phase;
 
         unsigned          m_flips;
         unsigned          m_max_trail;
@@ -78,11 +73,17 @@ namespace sat {
         unsigned          m_conflict_offset;
 
         bool should_restart();
+        void do_pop();
+        bool should_backjump();
+        lbool do_backjump();
+        lbool do_local_search(unsigned num_rounds);
+        lbool decide();
         void restart();
         void pop();
         void pop_decision();
         void init_runs();
-        lbool update_priority();
+        lbool update_priority(unsigned level);
+        void update_pqueue();
         void init_phase();
         void init_propagation();
         void refresh_solver();