fix ema

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

src/sat/sat_clause.h

@@ -136,7 +136,7 @@ namespace sat {
        \brief Simple clause allocator that allows uint (32bit integers) to be used to reference clauses (even in 64bit machines).
     */
     class clause_allocator {
-        small_object_allocator    m_allocator;
+        sat_allocator    m_allocator;
         id_gen           m_id_gen;
     public:
         clause_allocator();

src/sat/sat_config.cpp

@@ -38,9 +38,16 @@ namespace sat {
             m_restart = RS_LUBY;
         else if (s == symbol("geometric"))
             m_restart = RS_GEOMETRIC;
+        else if (s == symbol("ema"))
+            m_restart = RS_EMA;
+        else if (s == symbol("static"))
+            m_restart = RS_STATIC;
         else
             throw sat_param_exception("invalid restart strategy");
 
+        m_fast_glue_avg = p.restart_emafastglue();
+        m_slow_glue_avg = p.restart_emaslowglue();
+        m_restart_margin = p.restart_margin();
         m_restart_fast = p.restart_fast();
         s = p.phase();
         if (s == symbol("always_false")) 

src/sat/sat_config.h

@@ -33,7 +33,9 @@ namespace sat {
 
     enum restart_strategy {
         RS_GEOMETRIC,
-        RS_LUBY
+        RS_LUBY,
+        RS_EMA,
+        RS_STATIC
     };
 
     enum gc_strategy {
@@ -90,7 +92,10 @@ namespace sat {
         bool               m_restart_fast;
         unsigned           m_restart_initial;
         double             m_restart_factor; // for geometric case
+        double             m_restart_margin; // for ema
         unsigned           m_restart_max;
+        double             m_fast_glue_avg;
+        double             m_slow_glue_avg;
         unsigned           m_inprocess_max;
         double             m_random_freq;
         unsigned           m_random_seed;

src/sat/sat_params.pyg

@@ -7,11 +7,14 @@ def_module_params('sat',
                           ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
                           ('phase.sticky', BOOL, False, 'use sticky phase caching for local search'),
                           ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
-                          ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
+                          ('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'),
-                          ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
+                          ('restart.initial', UINT, 2, 'initial restart (number of conflicts)'),
-                          ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
+                          ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),	               
-                          ('restart.fast', BOOL, False, 'use fast restart strategy.'),
+                          ('restart.fast', BOOL, True, 'use fast restart approach only removing less active literals.'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
+                          ('restart.margin', DOUBLE, 1.1, 'margin between fast and slow restart factors. For ema'),
+                          ('restart.emafastglue', DOUBLE, 3e-2, 'ema alpha factor for fast moving average'),
+                          ('restart.emaslowglue', DOUBLE, 1e-5, 'ema alpha factor for slow moving average'),
                           ('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'),

src/sat/sat_solver.cpp

@@ -53,6 +53,8 @@ namespace sat {
         m_qhead(0),
         m_scope_lvl(0),
         m_search_lvl(0),
+        m_fast_glue_avg(),
+        m_slow_glue_avg(),
         m_params(p),
         m_par_id(0),
         m_par_syncing_clauses(false) {
@@ -538,7 +540,6 @@ namespace sat {
         // walk clauses, reallocate them in an order that defragments memory and creates locality.
         for (literal lit : lits) {
             watch_list& wlist = m_watches[lit.index()];
-            // for (watch_list& wlist : m_watches) {            
             for (watched& w : wlist) {
                 if (w.is_clause()) {
                     clause& c1 = get_clause(w);
@@ -791,12 +792,11 @@ namespace sat {
         }
         
         if (m_config.m_propagate_prefetch) {
-            _mm_prefetch((const char*)(m_watches[l.index()].c_ptr()), _MM_HINT_T1);
+            _mm_prefetch((const char*)(&*(m_watches[l.index()].c_ptr())), _MM_HINT_T1);
         }
 
         SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
         SASSERT(l.sign()  || m_phase[v] == POS_PHASE);
-
         SASSERT(!l.sign() || value(v) == l_false);
         SASSERT(l.sign()  || value(v) == l_true);
         SASSERT(value(l) == l_true);
@@ -1059,16 +1059,14 @@ namespace sat {
                     return r;
                 pop_reinit(scope_lvl());
                 m_conflicts_since_restart = 0;
-                m_restart_threshold       = m_config.m_restart_initial;
+                m_restart_threshold = m_config.m_restart_initial;
             }
 
             // iff3_finder(*this)();
             simplify_problem();
             if (check_inconsistent()) return l_false;
 
-            if (m_config.m_max_conflicts == 0) {
+            if (reached_max_conflicts()) {
-                m_reason_unknown = "sat.max.conflicts";
-                IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
                 return l_undef;
             }
 
@@ -1079,9 +1077,7 @@ namespace sat {
                 if (r != l_undef)
                     return r;
 
-                if (m_conflicts_since_init > m_config.m_max_conflicts) {
+                if (reached_max_conflicts()) {
-                    m_reason_unknown = "sat.max.conflicts";
-                    IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";);
                     return l_undef;
                 }
 
@@ -1413,7 +1409,7 @@ namespace sat {
             return l_true;
         if (!resolve_conflict())
             return l_false;
-        if (m_conflicts_since_init > m_config.m_max_conflicts) 
+        if (reached_max_conflicts()) 
             return l_undef;
         if (should_restart()) 
             return l_undef;
@@ -1829,7 +1825,12 @@ namespace sat {
     }
 
     bool solver::should_restart() const {
-        return m_conflicts_since_restart > m_restart_threshold;
+        if (m_conflicts_since_restart <= m_restart_threshold) return false;
+        if (scope_lvl() < 2 + search_lvl()) return false;
+        if (m_config.m_restart != RS_EMA) return true;
+        return 
+            m_fast_glue_avg + search_lvl() <= scope_lvl() && 
+            m_config.m_restart_margin * m_slow_glue_avg <= m_fast_glue_avg;
     }
 
     void solver::restart(bool to_base) {
@@ -1843,31 +1844,39 @@ namespace sat {
                        << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
         }
         IF_VERBOSE(30, display_status(verbose_stream()););
-        unsigned num_scopes = 0;
+        pop_reinit(restart_level(to_base));
+        set_next_restart();
+    }
+
+    unsigned solver::restart_level(bool to_base) {
         if (to_base || scope_lvl() == search_lvl()) {
-            num_scopes = scope_lvl() - search_lvl();
+            return scope_lvl() - search_lvl();
         }
         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.
+            // pop trail from top
 #if 0
-            // pop the trail from top
+            unsigned n = 0;
             do {
-                bool_var prev = scope_literal(scope_lvl() - num_scopes - 1).var();
+                bool_var prev = scope_literal(scope_lvl() - n - 1).var();
                 if (m_case_split_queue.more_active(prev, next)) break;                
-                ++num_scopes;
+                ++n;
             }
-            while (num_scopes < scope_lvl() - search_lvl());
+            while (n < scope_lvl() - search_lvl());
-#else            
+            return n;
-            // 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 trail from bottom
+            unsigned n = search_lvl();
+            for (; n < scope_lvl() && m_case_split_queue.more_active(scope_literal(n).var(), next); ++n) {
+            }
+            return n - search_lvl();
         }
-        pop_reinit(num_scopes);
+    }
+
+    void solver::set_next_restart() {
         m_conflicts_since_restart = 0;
         switch (m_config.m_restart) {
         case RS_GEOMETRIC:
@@ -1877,6 +1886,11 @@ namespace sat {
             m_luby_idx++;
             m_restart_threshold = m_config.m_restart_initial * get_luby(m_luby_idx);
             break;
+        case RS_EMA:
+            m_restart_threshold = m_config.m_restart_initial;
+            break;
+        case RS_STATIC:
+            break;
         default:
             UNREACHABLE();
             break;
@@ -2356,6 +2370,8 @@ namespace sat {
         }
 
         unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr());
+        m_fast_glue_avg.update(glue);
+        m_slow_glue_avg.update(glue);
 
         pop_reinit(m_scope_lvl - new_scope_lvl);
         TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n"; display(tout););
@@ -3303,6 +3319,8 @@ namespace sat {
         m_rand.set_seed(m_config.m_random_seed);
         m_step_size = m_config.m_step_size_init;
         m_drat.updt_config();
+        m_fast_glue_avg.set_alpha(m_config.m_fast_glue_avg);
+        m_slow_glue_avg.set_alpha(m_config.m_slow_glue_avg);
     }
 
     void solver::collect_param_descrs(param_descrs & d) {
@@ -3849,6 +3867,17 @@ namespace sat {
         TRACE("sat", tout << m_core << "\n";);
     }
 
+    bool solver::reached_max_conflicts() {
+        if (m_config.m_max_conflicts == 0 || m_conflicts_since_init > m_config.m_max_conflicts) {
+            if (m_reason_unknown != "sat.max.conflicts") {
+                m_reason_unknown = "sat.max.conflicts";
+                IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";);
+            }
+            return true;
+        }
+        return false;
+    }
+
 
     lbool solver::get_bounded_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
         bool_var_set unfixed_vars;
@@ -3894,8 +3923,7 @@ namespace sat {
 
             extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
 
-            if (m_conflicts_since_init > m_config.m_max_conflicts) {
+            if (reached_max_conflicts()) {
-                IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";);
                 return l_undef;
             }
 

src/sat/sat_solver.h

@@ -41,6 +41,7 @@ Revision History:
 #include "util/params.h"
 #include "util/statistics.h"
 #include "util/stopwatch.h"
+#include "util/ema.h"
 #include "util/trace.h"
 #include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
@@ -137,6 +138,8 @@ namespace sat {
         unsigned                m_qhead;
         unsigned                m_scope_lvl;
         unsigned                m_search_lvl;
+        ema                     m_fast_glue_avg;
+        ema                     m_slow_glue_avg;
         literal_vector          m_trail;
         clause_wrapper_vector   m_clauses_to_reinit;
         std::string             m_reason_unknown;
@@ -416,7 +419,10 @@ namespace sat {
         void mk_model();
         bool check_model(model const & m) const;
         void restart(bool to_base);
+        unsigned restart_level(bool to_base);
         bool should_restart() const;
+        void set_next_restart();
+        bool reached_max_conflicts();
         void sort_watch_lits();
         void exchange_par();
         lbool check_par(unsigned num_lits, literal const* lits);

src/smt/theory_pb.cpp

@@ -782,7 +782,6 @@ namespace smt {
         if (pb.is_at_least_k(atom)) {
             return true;
         }
-        // TBD: other conditions
         return false;
     }
 
@@ -791,7 +790,6 @@ namespace smt {
         if (ctx.b_internalized(atom)) {
             return true;
         }
-
         if (!is_cardinality_constraint(atom)) {
             return false;
         }       
@@ -816,8 +814,7 @@ namespace smt {
 
         card* c = alloc(card, lit, bound, aux);
         
-        for (unsigned i = 0; i < num_args; ++i) {
+        for (expr* arg : *atom) {
-            expr* arg = atom->get_arg(i);
             c->add_arg(compile_arg(arg));
         }
 
@@ -2432,9 +2429,9 @@ namespace smt {
 
     void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
         uint_set nlits;
-        for (unsigned i = 0; i < lits.size(); ++i) {
+        for (literal lit : lits) {
-            SASSERT(get_context().get_assignment(lits[i]) == l_true);
+            SASSERT(get_context().get_assignment(lit) == l_true);
-            nlits.insert((~lits[i]).index());
+            nlits.insert((~lit).index());
         }
         SASSERT(get_context().get_assignment(l) == l_undef);
         SASSERT(get_context().get_assignment(c.lit()) == l_true);
@@ -2448,9 +2445,7 @@ namespace smt {
         }
         CTRACE("pb", (sum >= c.k()),
                display(tout << "invalid assign" , c, true);
-               for (unsigned i = 0; i < lits.size(); ++i) {
+               for (literal lit : lits) tout << lit << " ";
-                   tout << lits[i] << " ";
-               }
                tout << " => " << l << "\n";);
         SASSERT(sum < c.k());
     }

src/util/ema.h

@@ -7,7 +7,9 @@ Module Name:
 
 Abstract:
 
-    Exponential moving average in the style of CaDiCal.
+    Exponential moving average based on CaDiCal.
+    The exponential scheme used to adjust beta to alpha is 
+    described in Biere & Froelich, POS (Pragmatics of SAT) 2016.
 
 Author:
 
@@ -22,17 +24,27 @@ Revision History:
 class ema {
     double m_alpha, m_beta, m_value;
     unsigned m_period, m_wait;
-
+    bool invariant() const { return 0 <= m_alpha && m_alpha <= m_beta && m_beta <= 1; }
  public:
-    ema() { memset(this, 0, sizeof(*this)); }
+    ema(): m_alpha(0), m_beta(1), m_value(0), m_period(0), m_wait(0) {
+        SASSERT(invariant());
+    }
 
     ema(double alpha): 
         m_alpha(alpha), m_beta(1), m_value(0), 
-        m_period(0), m_wait(0) {}
+        m_period(0), m_wait(0) {
+        SASSERT(invariant());
+    }
 
-    double operator() const { return m_value; }
+    void set_alpha(double alpha) { 
+        m_alpha = alpha; 
+        SASSERT(invariant());
+    }
+
+    operator double () const { return m_value; }
 
     void update(double x) {
+        SASSERT(invariant());
         m_value += m_beta * (x - m_value);
         if (m_beta <= m_alpha || m_wait--) return;
         m_wait = m_period = 2*(m_period + 1) - 1;