Changed lookahead backtrack. Parent lookahead re-use fix

src/sat/sat_lookahead.cpp

@@ -205,6 +205,12 @@ namespace sat {
 
     void lookahead::pre_select() {
         m_lookahead.reset();
+        for (bool_var x : m_freevars) { // tree lookahead may leave some literals fixed in lower truth levels
+            literal l(x, false);
+            set_undef(l);
+            set_undef(~l);
+        }
+//printf("m_freevars.size() = %d\n", m_freevars.size());
         if (select(scope_lvl())) {
             get_scc();
             if (inconsistent()) return;
@@ -1052,6 +1058,7 @@ namespace sat {
         scoped_level _sl(*this, level);
         SASSERT(m_search_mode == lookahead_mode::lookahead1);
         m_search_mode = lookahead_mode::lookahead2;
+        lookahead_backtrack();
         assign(lit);
         propagate();
         bool unsat = inconsistent();
@@ -1065,6 +1072,7 @@ namespace sat {
         SASSERT(m_search_mode == lookahead_mode::searching);
         m_search_mode = lookahead_mode::lookahead1;
         scoped_level _sl(*this, level);
+        lookahead_backtrack();
         unsigned old_sz = m_trail.size();
         assign(lit);
         propagate();
@@ -1107,6 +1115,41 @@ namespace sat {
         m_wstack.reset();
     }
 
+    void lookahead::lookahead_backtrack() {
+        //printf("before: m_trail.size() = %d\n", m_trail.size());
+        while (!m_trail.empty() && is_undef(m_trail.back())) {
+            m_trail.pop_back();
+        }
+        SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back());
+        m_qhead = std::min(m_qhead, m_trail.size());
+        //printf("after: m_trail.size() = %d\n", m_trail.size());
+    }
+    /*void lookahead::lookahead_backtrack() {
+        //return;
+        if (m_trail_lim.empty()) return;
+        unsigned old_sz = m_trail_lim.back();
+        unsigned j = m_trail.size();
+        while (j > old_sz) {
+        //while (m_qhead > old_sz) {
+            literal l = m_trail[j - 1];
+            //literal l = m_trail[m_qhead - 1];
+            if (is_fixed(l)) {
+                break;
+            }
+            else {
+                --j;
+                //--m_qhead;
+                SASSERT(is_undef(l));
+                //set_undef(l);
+                //for (unsigned idx : m_nary[(~l).index()]) {
+                //    ++m_nary_len[idx];
+                //}
+            }
+        }
+        //m_trail.shrink(m_qhead);
+        m_trail.shrink(j);
+        m_qhead = std::min(m_qhead, j);
+    }*/
 
     // 
     // The current version is modeled after CDCL SAT solving data-structures.
@@ -1304,7 +1347,6 @@ namespace sat {
         unsigned sz = m_nary_count[(~l).index()];
         literal lit;
         SASSERT(m_search_mode == lookahead_mode::searching);
-
         for (unsigned idx : m_nary[(~l).index()]) {
             if (sz-- == 0) break;
             unsigned len = --m_nary_literals[idx];
@@ -1485,7 +1527,7 @@ namespace sat {
             literal lit;
             while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
                 if (lit != l) {
-                    // SASSERT(m_nary[lit.index()] == pclauses[i]);
+                    SASSERT(m_nary[lit.index()][m_nary_count[lit.index()]] == pclauses[i]);
                     m_nary_count[lit.index()]++;
                 }
             }
@@ -1593,12 +1635,15 @@ namespace sat {
     void lookahead::propagate() {
         while (!inconsistent() && m_qhead < m_trail.size()) {
             unsigned i = m_qhead;
-            for (; i < m_trail.size() && !inconsistent(); ++i) {
+            unsigned sz = m_trail.size();
+            //for (; i < m_trail.size() && !inconsistent(); ++i) {
+            for (; i < sz && !inconsistent(); ++i) {
                 literal l = m_trail[i];
                 TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
                 propagate_binary(l);
             }
-            while (m_qhead < m_trail.size() && !inconsistent()) {
+            //while (m_qhead < m_trail.size() && !inconsistent()) {
+            while (m_qhead < sz && !inconsistent()) {
                 propagate_clauses(m_trail[m_qhead++]);
             }
             SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
@@ -1607,7 +1652,6 @@ namespace sat {
     }
 
     void lookahead::compute_lookahead_reward() {
-        init_lookahead_reward();
         TRACE("sat", display_lookahead(tout); );
         m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size());
         unsigned base = 2;
@@ -1630,56 +1674,36 @@ namespace sat {
                     IF_VERBOSE(30, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";);
                 }
                 TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";);
-                unsigned old_trail_sz = m_trail.size();
                 reset_lookahead_reward(lit);
-                push_lookahead1(lit, level);
+                unsigned num_units = push_lookahead1(lit, level);
-                do_double(lit, base);
+                update_lookahead_reward(lit, level);
+                unsigned old_trail_sz = m_trail.size();
+                unsigned dl_lvl = level;
+                num_units += do_double(lit, dl_lvl);
+                if (dl_lvl > level) {
+                    base = dl_lvl;
+                }
                 bool unsat = inconsistent();
-                unsigned num_units = m_trail.size() - old_trail_sz;
                 pop_lookahead1(lit, num_units); 
                 if (unsat) {
                     TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
-                    reset_lookahead_reward();
+                    lookahead_backtrack();
                     assign(~lit);
                     propagate();
-                    init_lookahead_reward();
                     change = true;
                     last_changed = lit;
                 }
-                else {
-                    update_lookahead_reward(lit, level);                        
-                }
                 SASSERT(inconsistent() || !is_unsat());
             }
             if (c_fixed_truth - 2 * m_lookahead.size() < base) {
                 break;
             }
-            reset_lookahead_reward();
-            init_lookahead_reward();
             base += 2 * m_lookahead.size();
         }
-        reset_lookahead_reward();
+        lookahead_backtrack();
         TRACE("sat", display_lookahead(tout); );
     }
 
-    void lookahead::init_lookahead_reward() {
-        TRACE("sat", tout << "init_lookahead_reward: " << m_qhead << "\n";);
-        m_qhead_lim.push_back(m_qhead);
-        m_trail_lim.push_back(m_trail.size());
-    }
-
-    void lookahead::reset_lookahead_reward() {
-        m_qhead = m_qhead_lim.back();
-        TRACE("sat", tout << "reset_lookahead_reward: " << m_qhead << "\n";);
-        unsigned old_sz = m_trail_lim.back();
-        for (unsigned i = old_sz; i < m_trail.size(); ++i) {
-            set_undef(m_trail[i]);
-        }
-        m_trail.shrink(old_sz);            
-        m_trail_lim.pop_back();
-        m_qhead_lim.pop_back();
-    }
-
     literal lookahead::select_literal() {
         literal l = null_literal;
         double h = 0;
@@ -1722,7 +1746,8 @@ namespace sat {
 
         // inherit propagation effect from parent.
         literal p = get_parent(l);
-        set_lookahead_reward(l, p == null_literal ? 0 : get_lookahead_reward(p));
+        set_lookahead_reward(l, (p == null_literal || is_undef(p) || is_fixed_at(p, c_fixed_truth)) ?
+                                0 : get_lookahead_reward(p));
     }
 
     bool lookahead::check_autarky(literal l, unsigned level) {
@@ -1773,10 +1798,9 @@ namespace sat {
                 TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] 
                       << " " 
                       << (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";);
-                reset_lookahead_reward();
+                lookahead_backtrack();
                 assign(l);
                 propagate();
-                init_lookahead_reward();
             }
             else {
                 ++m_stats.m_autarky_equivalences;
@@ -1800,12 +1824,13 @@ namespace sat {
         }
     }
 
-    void lookahead::do_double(literal l, unsigned& base) { 
+    unsigned lookahead::do_double(literal l, unsigned& base) {
+        unsigned num_units = 0;
         if (!inconsistent() && dl_enabled(l)) {
             if (get_lookahead_reward(l) > m_delta_trigger) {
                 if (dl_no_overflow(base)) {
                     ++m_stats.m_double_lookahead_rounds;
-                    double_look(l, base);
+                    num_units = double_look(l, base);
                     if (!inconsistent()) {
                         m_delta_trigger = get_lookahead_reward(l);
                         dl_disable(l);
@@ -1817,18 +1842,20 @@ namespace sat {
                 m_delta_trigger *= m_delta_decrease;
             }
         }
+        return num_units;
     }
 
-    void lookahead::double_look(literal l, unsigned& base) {
+    unsigned lookahead::double_look(literal l, unsigned& base) {
         SASSERT(!inconsistent());
         SASSERT(dl_no_overflow(base));
         base += m_lookahead.size();
         unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
         scoped_level _sl(*this, dl_truth);
         IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";);
-        init_lookahead_reward();
+        lookahead_backtrack();
         assign(l);
         propagate();
+        unsigned old_sz = m_trail.size();
         bool change = true;
         literal last_changed = null_literal;
         unsigned num_iterations = 0;
@@ -1850,20 +1877,19 @@ namespace sat {
                     TRACE("sat", tout << "unit: " << ~lit << "\n";);
                     ++m_stats.m_double_lookahead_propagations;
                     SASSERT(m_level == dl_truth);
-                    reset_lookahead_reward();
+                    lookahead_backtrack();
                     assign(~lit);
                     propagate();
                     change = true;
                     last_changed = lit;
-                    init_lookahead_reward();
                 }
             }
             base += 2 * m_lookahead.size();
             SASSERT(dl_truth >= base);
         }
-        reset_lookahead_reward();
         SASSERT(m_level == dl_truth);
         base = dl_truth;
+        return m_trail.size() - old_sz;
     }
 
     void lookahead::validate_assign(literal l) {
@@ -1899,11 +1925,11 @@ namespace sat {
 
     void lookahead::propagated(literal l) {
         assign(l);
-        for (unsigned i = m_trail.size() - 1; i < m_trail.size() && !inconsistent(); ++i) {
+        /*for (unsigned i = m_trail.size() - 1; i < m_trail.size() && !inconsistent(); ++i) {
             literal l = m_trail[i];
             TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
             propagate_binary(l);
-        }
+        }*/
         if (m_search_mode == lookahead_mode::lookahead1) {
             m_wstack.push_back(l);
         }

src/sat/sat_lookahead.h

@@ -89,7 +89,8 @@ namespace sat {
                 m_min_cutoff = 30;
                 m_preselect = false;
                 m_level_cand = 600;
-                m_delta_rho = (double)0.25;
+                //m_delta_rho = (double)0.25;
+                m_delta_rho = (double)0.5;
                 m_dl_max_iterations = 2;
                 m_tc1_limit = 10000000;
                 m_reward_type = ternary_reward;
@@ -436,6 +437,7 @@ namespace sat {
         bool push_lookahead2(literal lit, unsigned level);
         unsigned push_lookahead1(literal lit, unsigned level);
         void pop_lookahead1(literal lit, unsigned num_units);
+        void lookahead_backtrack();
         double mix_diff(double l, double r) const;
         clause const& get_clause(watch_list::iterator it) const;
         bool is_nary_propagation(clause const& c, literal l) const;
@@ -465,8 +467,8 @@ namespace sat {
             return is_fixed(lit) && (!is_false(lit) || m_stamp[lit.var()] >= level);
         }
 
-        void do_double(literal l, unsigned& base);
+        unsigned do_double(literal l, unsigned& base);
-        void double_look(literal l, unsigned& base);
+        unsigned double_look(literal l, unsigned& base);
         void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; }
         //void set_conflict() { TRACE("sat", tout << "conflict\n";); printf("CONFLICT\n"); m_inconsistent = true; }
         bool inconsistent() { return m_inconsistent; }