From 5cdfa7cd1cf5e5209213421238ab916eb03d0585 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Feb 2019 17:43:15 -0800 Subject: [PATCH] variations on unit-walk Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 1 + src/sat/sat_local_search.cpp | 30 +++- src/sat/sat_local_search.h | 1 + src/sat/sat_lookahead.cpp | 4 +- src/sat/sat_lookahead.h | 3 +- src/sat/sat_params.pyg | 1 + src/sat/sat_unit_walk.cpp | 257 ++++++++++++++++------------------- src/sat/sat_unit_walk.h | 19 +-- 9 files changed, 163 insertions(+), 154 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 57adf5132..08336b1e4 100644 --- a/src/sat/sat_config.cpp +++ b/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; diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 79baa621e..b8d0ca0f5 100644 --- a/src/sat/sat_config.h +++ b/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; diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 47cb29694..7c3ebb688 100644 --- a/src/sat/sat_local_search.cpp +++ b/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()]]; - // VERIFY(c.m_k < constraint_value(c)); + constraint const& c = m_constraints[m_unsat_stack[m_rand() % num_unsat]]; 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 diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index f1ef29158..00c38e481 100644 --- a/src/sat/sat_local_search.h +++ b/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); diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 557624db5..74ac831d8 100644 --- a/src/sat/sat_lookahead.cpp +++ b/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 & 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() { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 606fd2b8c..f6103ee7c 100644 --- a/src/sat/sat_lookahead.h +++ b/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; } }; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 0fdb1aa70..88b196d04 100644 --- a/src/sat/sat_params.pyg +++ b/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'), diff --git a/src/sat/sat_unit_walk.cpp b/src/sat/sat_unit_walk.cpp index 56f5a2d1e..314c275f3 100644 --- a/src/sat/sat_unit_walk.cpp +++ b/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) { - if (!s.rlimit().inc()) { - log_status(); - return l_undef; - } - bool_var v = pqueue().next(s); - 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(); - } + lbool st = l_undef; + while (s.rlimit().inc() && st == l_undef) { + if (inconsistent() && !m_decisions.empty()) do_pop(); + else if (inconsistent()) st = l_false; + else if (should_backjump()) st = do_backjump(); + else st = decide(); } + 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() { - unsigned prefix_length = 0; - 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"); + lbool unit_walk::do_local_search(unsigned num_rounds) { + unsigned prefix_length = (0*m_trail.size())/10; 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())); - lbool is_sat = m_ls.check(0, m_trail.c_ptr(), nullptr); + m_ls.rlimit().push(num_rounds); + 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() { - if (m_sticky_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]; - } - } + lbool unit_walk::update_priority(unsigned level) { + + while (m_decisions.size() > level) { + pop_decision(); } - else { - for (bool_var v : pqueue()) - m_phase[v] = (m_rand(2) == 0); + IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk :update-priority " << m_decisions.size() << "\n"); + + 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() { diff --git a/src/sat/sat_unit_walk.h b/src/sat/sat_unit_walk.h index 0551d3192..2aead871f 100644 --- a/src/sat/sat_unit_walk.h +++ b/src/sat/sat_unit_walk.h @@ -35,14 +35,10 @@ namespace sat { svector m_vars; unsigned_vector m_lim; unsigned m_head; - unsigned m_depth; public: - var_priority() { m_depth = 0; m_head = 0; } - void rewind() { m_head = 0; for (unsigned& l : m_lim) l = 0; } - unsigned depth() const { return m_depth; } - void inc_depth() { ++m_depth; } - void dec_depth() { --m_depth; } - void reset() { m_lim.reset(); m_head = 0; m_depth = 0; } + var_priority() { m_head = 0; } + void reset() { m_lim.reset(); m_head = 0;} + void rewind() { for (unsigned& l : m_lim) l = 0; m_head = 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();