n/a

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

src/sat/sat_config.cpp

@@ -115,9 +115,11 @@ namespace sat {
         m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base();
         m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger();
         m_lookahead_global_autarky = p.lookahead_global_autarky();
+        m_lookahead_use_learned = p.lookahead_use_learned();
+
 
         // These parameters are not exposed
-        m_simplify_mult1  = _p.get_uint("simplify_mult1", 300);
+        m_next_simplify1  = _p.get_uint("next_simplify", 30000);
         m_simplify_mult2  = _p.get_double("simplify_mult2", 1.5);
         m_simplify_max    = _p.get_uint("simplify_max", 500000);
         // --------------------------------

src/sat/sat_config.h

@@ -113,9 +113,10 @@ namespace sat {
         double             m_lookahead_cube_psat_trigger;
         reward_t           m_lookahead_reward;
         bool               m_lookahead_global_autarky;
+        bool               m_lookahead_use_learned;
 
         bool               m_incremental;
-        unsigned           m_simplify_mult1;
+        unsigned           m_next_simplify1;
         double             m_simplify_mult2;
         unsigned           m_simplify_max;
         unsigned           m_simplify_delay;

src/sat/sat_lookahead.cpp

@@ -2227,7 +2227,7 @@ namespace sat {
     void lookahead::init_search() {
         m_search_mode = lookahead_mode::searching;
         scoped_level _sl(*this, c_fixed_truth);
-        init(true);            
+        init(m_s.m_config.m_lookahead_use_learned);            
     }
 
     void lookahead::checkpoint() {

src/sat/sat_params.pyg

@@ -12,7 +12,7 @@ def_module_params('sat',
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
                           ('restart.fast', BOOL, False, 'use fast restart strategy.'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
-                          ('variable_decay', UINT, 120, 'multiplier (divided by 100) for the VSIDS activity increement'), 
+                          ('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increement'), 
                           ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
                           ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
                           ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),
@@ -56,6 +56,7 @@ def_module_params('sat',
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
+                          ('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'),
                           ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))

src/sat/sat_solver.cpp

@@ -532,17 +532,15 @@ namespace sat {
         for (clause* c : m_clauses) c->unmark_used();
         for (clause* c : m_learned) c->unmark_used();
 
-#if 0
         svector<bool_var> vars;
         for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i);
         std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this));
         literal_vector lits;
-        for (bool_var v : vars) lits.push_back(to_literal(v)), lits.push_back(~to_literal(v));
+        for (bool_var v : vars) lits.push_back(literal(v, false)), lits.push_back(literal(v, true));
         // walk clauses, reallocate them in an order that defragments memory and creates locality.
-        //for (literal lit : lits) {
+        for (literal lit : lits) {
-        //watch_list& wlist = m_watches[lit.index()];
+            watch_list& wlist = m_watches[lit.index()];
-#endif
+            // for (watch_list& wlist : m_watches) {            
-        for (watch_list& wlist : m_watches) {            
             for (watched& w : wlist) {
                 if (w.is_clause()) {
                     clause& c1 = get_clause(w);
@@ -795,7 +793,7 @@ namespace sat {
         }
         
         if (m_config.m_propagate_prefetch) {
-            _mm_prefetch((char const*)(m_watches.c_ptr() + l.index()), 0);
+            _mm_prefetch((const char*)(m_watches[l.index()].c_ptr()), 1);
         }
 
         SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
@@ -1502,7 +1500,6 @@ namespace sat {
         SASSERT(m_search_lvl == 1);
     }
 
-
     void solver::update_min_core() {
         if (!m_min_core_valid || m_core.size() < m_min_core.size()) {
             m_min_core.reset();
@@ -1533,8 +1530,7 @@ namespace sat {
         push();
         reset_assumptions();
         TRACE("sat", tout << "reassert: " << m_min_core << "\n";);
-        for (unsigned i = 0; i < m_min_core.size(); ++i) {
+        for (literal lit : m_min_core) {
-            literal lit = m_min_core[i];
             SASSERT(is_external(lit.var()));
             add_assumption(lit);
             assign(lit, justification());
@@ -1554,12 +1550,12 @@ namespace sat {
                 assign(m_assumptions[i], justification());
             }
             TRACE("sat",
-                 for (unsigned i = 0; i < m_assumptions.size(); ++i) {
+                  for (literal a : m_assumptions) {
-                     index_set s;
+                      index_set s;
-                     if (m_antecedents.find(m_assumptions[i].var(), s)) {
+                      if (m_antecedents.find(a.var(), s)) {
-                         tout << m_assumptions[i] << ": "; display_index_set(tout, s) << "\n";
+                          tout << a << ": "; display_index_set(tout, s) << "\n";
-                     }
+                      }
-                 });
+                  });
         }
     }
 
@@ -1602,7 +1598,6 @@ namespace sat {
 
     /**
        \brief Apply all simplifications.
-
     */
     void solver::simplify_problem() {
         if (m_conflicts_since_init < m_next_simplify) {
@@ -1657,7 +1652,7 @@ namespace sat {
         reinit_assumptions();
 
         if (m_next_simplify == 0) {
-            m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1;
+            m_next_simplify = m_config.m_next_simplify1;
         }
         else {
             m_next_simplify = static_cast<unsigned>(m_conflicts_since_init * m_config.m_simplify_mult2);
@@ -1853,15 +1848,23 @@ namespace sat {
         }
         else {
             bool_var next = m_case_split_queue.min_var();
+
+            // Implementations of Marijn's idea of reusing the 
+            // trail when the next decision literal has lower precedence.
+#if 0
+            // pop the trail from top
             do {
-                scope& s = m_scopes[scope_lvl() - num_scopes - 1];
+                bool_var prev = scope_literal(scope_lvl() - num_scopes - 1).var();
-                bool_var prev = m_trail[s.m_trail_lim].var();
+                if (m_case_split_queue.more_active(prev, next)) break;                
-                //IF_VERBOSE(0, verbose_stream() << "more active: " << m_case_split_queue.more_active(next, prev) << "\n");
-                if (!m_case_split_queue.more_active(next, prev)) break;                
                 ++num_scopes;
             }
             while (num_scopes < scope_lvl() - search_lvl());
-            //IF_VERBOSE(0, verbose_stream() << "backtrack " << num_scopes << " " << scope_lvl() - search_lvl() << "\n");
+#else            
+            // pop the trail from bottom
+            unsigned n = search_lvl();
+            for (; n < scope_lvl() && m_case_split_queue.more_active(scope_literal(n).var(), next); ++n) ;
+            num_scopes = n - search_lvl();
+#endif
         }
         pop_reinit(num_scopes);
         m_conflicts_since_restart = 0;
@@ -2860,7 +2863,8 @@ namespace sat {
        \brief Reset the mark of the variables in the current lemma.
     */
     void solver::reset_lemma_var_marks() {
-        if (m_config.m_branching_heuristic == BH_LRB) {
+        if (m_config.m_branching_heuristic == BH_LRB ||
+            m_config.m_branching_heuristic == BH_VSIDS) {
             update_lrb_reasoned();
         }        
         literal_vector::iterator it  = m_lemma.begin();
@@ -2917,6 +2921,7 @@ namespace sat {
         if (!is_marked(v)) {
             mark(v);
             m_reasoned[v]++;
+            inc_activity(v);
             m_lemma.push_back(lit);
         }
     }

src/sat/sat_solver.h

@@ -297,6 +297,7 @@ namespace sat {
         unsigned lvl(literal l) const { return m_level[l.var()]; }
         unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
         literal  trail_literal(unsigned i) const { return m_trail[i]; }
+        literal  scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
         void assign(literal l, justification j) {
             TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
             switch (value(l)) {