diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 4eeb5dc4a..f95696b3d 100644 --- a/src/sat/sat_clause.h +++ b/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(); diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 2bf20100b..c7f2377c9 100644 --- a/src/sat/sat_config.cpp +++ b/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")) diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 9153f8b14..37efe69ed 100644 --- a/src/sat/sat_config.h +++ b/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; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 324882894..ce40949da 100644 --- a/src/sat/sat_params.pyg +++ b/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.initial', UINT, 100, 'initial restart (number of conflicts)'), - ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), - ('restart.fast', BOOL, False, 'use fast restart strategy.'), + ('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'), + ('restart.initial', UINT, 2, 'initial restart (number of conflicts)'), + ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), + ('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'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d69a9cb4a..ee194721e 100644 --- a/src/sat/sat_solver.cpp +++ b/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) { - m_reason_unknown = "sat.max.conflicts"; - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";); + if (reached_max_conflicts()) { 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) { - m_reason_unknown = "sat.max.conflicts"; - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";); + if (reached_max_conflicts()) { 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()); -#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(); + while (n < scope_lvl() - search_lvl()); + return n; #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& 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_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";); + if (reached_max_conflicts()) { return l_undef; } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 634bf2788..1c5e10616 100644 --- a/src/sat/sat_solver.h +++ b/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); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 4c2d8e8c6..b93de3073 100644 --- a/src/smt/theory_pb.cpp +++ b/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) { - expr* arg = atom->get_arg(i); + for (expr* arg : *atom) { 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) { - SASSERT(get_context().get_assignment(lits[i]) == l_true); - nlits.insert((~lits[i]).index()); + for (literal lit : lits) { + SASSERT(get_context().get_assignment(lit) == l_true); + 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) { - tout << lits[i] << " "; - } + for (literal lit : lits) tout << lit << " "; tout << " => " << l << "\n";); SASSERT(sum < c.k()); } diff --git a/src/util/ema.h b/src/util/ema.h index 9d5e33a34..5a32e021c 100644 --- a/src/util/ema.h +++ b/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;