From fda5809c89529a1848d47b5232aee761976627c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Mar 2017 14:40:58 -0800 Subject: [PATCH] local search updates Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 182 ++++++++++-------- src/sat/sat_local_search.h | 32 ++-- src/sat/sat_lookahead.h | 347 +++++++++++++++++++++-------------- src/sat/sat_parallel.cpp | 16 +- src/sat/sat_parallel.h | 6 +- src/sat/sat_solver.cpp | 29 ++- src/sat/sat_solver.h | 1 - 7 files changed, 364 insertions(+), 249 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index e297386e6..3dc37471e 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -1,21 +1,21 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: +Module Name: sat_local_search.cpp - Abstract: +Abstract: Local search module for cardinality clauses. - Author: +Author: Sixue Liu 2017-2-21 - Notes: +Notes: - --*/ +--*/ #include "sat_local_search.h" #include "sat_solver.h" @@ -27,10 +27,18 @@ namespace sat { void local_search::init() { + for (unsigned i = 0; i < m_assumptions.size(); ++i) { + add_clause(1, m_assumptions.c_ptr() + i); + } + // add sentinel variable. m_vars.push_back(var_info()); - best_solution.resize(num_vars() + 1, false); + for (unsigned v = 0; v < num_vars(); ++v) { + m_vars[v].m_value = (0 == (m_rand() % 2)); + } + + m_best_solution.resize(num_vars() + 1, false); m_index_in_unsat_stack.resize(num_constraints(), 0); coefficient_in_ob_constraint.resize(num_vars() + 1, 0); @@ -58,13 +66,12 @@ namespace sat { set_parameters(); } - void local_search::reinit() { - reinit_orig(); - } - void local_search::init_cur_solution() { for (unsigned v = 0; v < num_vars(); ++v) { - m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias); + // use bias half the time. + if (m_rand() % 100 < 50) { + m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias); + } } } @@ -114,16 +121,16 @@ namespace sat { // init goodvars void local_search::init_goodvars() { - goodvar_stack.reset(); + m_goodvar_stack.reset(); for (unsigned v = 0; v < num_vars(); ++v) { if (score(v) > 0) { // && conf_change[v] == true m_vars[v].m_in_goodvar_stack = true; - goodvar_stack.push_back(v); + m_goodvar_stack.push_back(v); } } } - void local_search::reinit_orig() { + void local_search::reinit() { for (unsigned i = 0; i < m_constraints.size(); ++i) { constraint& c = m_constraints[i]; c.m_slack = c.m_k; @@ -132,7 +139,7 @@ namespace sat { // init unsat stack m_unsat_stack.reset(); - // init solution: random now + // init solution using the bias init_cur_solution(); // init varibale information @@ -142,7 +149,7 @@ namespace sat { m_vars.back().m_conf_change = false; m_vars.back().m_slack_score = INT_MIN; m_vars.back().m_cscc = 0; - m_vars.back().m_time_stamp = max_steps + 1; + m_vars.back().m_time_stamp = m_max_steps + 1; for (unsigned i = 0; i < num_vars(); ++i) { m_vars[i].m_time_stamp = 0; m_vars[i].m_cscc = 1; @@ -158,18 +165,18 @@ namespace sat { void local_search::calculate_and_update_ob() { unsigned i, v; - objective_value = 0; + int objective_value = 0; for (i = 0; i < ob_constraint.size(); ++i) { v = ob_constraint[i].var_id; if (cur_solution(v)) objective_value += ob_constraint[i].coefficient; } - if (objective_value > best_objective_value) { - best_solution.reset(); + if (objective_value > m_best_objective_value) { + m_best_solution.reset(); for (unsigned v = 0; v < num_vars(); ++v) { - best_solution.push_back(cur_solution(v)); + m_best_solution.push_back(cur_solution(v)); } - best_objective_value = objective_value; + m_best_objective_value = objective_value; } } @@ -230,8 +237,13 @@ namespace sat { } } - local_search::local_search(solver& s) : + local_search::local_search() : m_par(0) { + } + + void local_search::import(solver& s, bool _init) { + m_vars.reset(); + m_constraints.reset(); m_vars.reserve(s.num_vars()); @@ -268,6 +280,7 @@ namespace sat { clause& c = *(*it); add_clause(c.size(), c.begin()); } + m_num_non_binary_clauses = s.m_clauses.size(); // copy cardinality clauses card_extension* ext = dynamic_cast(s.get_extension()); @@ -316,6 +329,9 @@ namespace sat { // SASSERT(ext->m_xors.empty()); } + if (_init) { + init(); + } } local_search::~local_search() { @@ -329,30 +345,32 @@ namespace sat { return check(0, 0); } -#define PROGRESS(tries, total_steps) \ +#define PROGRESS(tries, flips) \ if (tries % 10 == 0 || m_unsat_stack.empty()) { \ IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ - << " :tries " << tries \ - << " :steps " << total_steps \ + << " :flips " << flips \ << " :unsat " << m_unsat_stack.size() \ - << " :time " << timer.get_seconds() << ")\n";); \ + << " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \ } void local_search::walksat() { reinit(); timer timer; timer.start(); - unsigned step = 0, total_steps = 0, max_steps = (1 << 17), tries = 0; - PROGRESS(tries, total_steps); + unsigned step = 0, total_flips = 0, tries = 0; + PROGRESS(tries, total_flips); for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { - for (step = 0; step < max_steps && !m_unsat_stack.empty(); ++step) { + for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) { pick_flip_walksat(); } - total_steps += step; - PROGRESS(tries, total_steps); + total_flips += step; + PROGRESS(tries, total_flips); + if (m_par && tries % 30 == 0) { + m_par->get_phase(*this); + reinit(); + } } - PROGRESS(tries, total_steps); } void local_search::gsat() { @@ -361,14 +379,14 @@ namespace sat { bool_var flipvar; timer timer; timer.start(); - unsigned tries, step = 0, total_steps = 0; + unsigned tries, step = 0, total_flips = 0; for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) { reinit(); - for (step = 1; step <= max_steps; ) { + for (step = 1; step <= m_max_steps; ) { // feasible if (m_unsat_stack.empty()) { calculate_and_update_ob(); - if (best_objective_value >= best_known_value) { + if (m_best_objective_value >= m_best_known_value) { break; } } @@ -376,24 +394,21 @@ namespace sat { flip_gsat(flipvar); m_vars[flipvar].m_time_stamp = step++; } - total_steps += step; - PROGRESS(tries, total_steps); + total_flips += step; + PROGRESS(tries, total_flips); // tell the SAT solvers about the phase of variables. if (m_par && tries % 10 == 0) { m_par->get_phase(*this); } } - PROGRESS(tries, total_steps); } lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) { flet _p(m_par, p); m_model.reset(); - unsigned num_constraints = m_constraints.size(); - for (unsigned i = 0; i < sz; ++i) { - add_clause(1, assumptions + i); - } + m_assumptions.reset(); + m_assumptions.append(sz, assumptions); init(); switch (m_config.mode()) { @@ -407,7 +422,7 @@ namespace sat { // remove unit clauses from assumptions. - m_constraints.shrink(num_constraints); + m_constraints.shrink(num_constraints() - sz); TRACE("sat", display(tout);); @@ -441,7 +456,8 @@ namespace sat { } void local_search::pick_flip_walksat() { - m_good_vars.reset(); + 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()]]; @@ -454,7 +470,7 @@ namespace sat { literal l; for (; !is_true(*cit); ++cit) { SASSERT(cit != cend); } l = *cit; - v = l.var(); + best_var = v = l.var(); bool tt = cur_solution(v); int_vector const& falsep = m_vars[v].m_watch[!tt]; int_vector::const_iterator it = falsep.begin(), end = falsep.end(); @@ -465,7 +481,6 @@ namespace sat { else if (slack == 0) best_bsb += num_unsat; } - m_good_vars.push_back(v); ++cit; for (; cit != cend; ++cit) { l = *cit; @@ -494,11 +509,14 @@ namespace sat { if (it == end) { if (bsb < best_bsb) { best_bsb = bsb; - m_good_vars.reset(); - m_good_vars.push_back(v); + best_var = v; + n = 1; } else {// if (bb == best_bb) - m_good_vars.push_back(v); + ++n; + if (m_rand() % n == 0) { + best_var = v; + } } } } @@ -506,32 +524,36 @@ namespace sat { } else { for (unsigned i = 0; i < c.size(); ++i) { - if (is_true(c[i])) - m_good_vars.push_back(c[i].var()); + if (is_true(c[i])) { + if (m_rand() % n == 0) { + best_var = c[i].var(); + } + ++n; + } } } - SASSERT(!m_good_vars.empty()); - //std::cout << m_good_vars.size() << "\n"; - flip_walksat(m_good_vars[m_rand() % m_good_vars.size()]); + flip_walksat(best_var); } void local_search::flip_walksat(bool_var flipvar) { m_vars[flipvar].m_value = !cur_solution(flipvar); bool flip_is_true = cur_solution(flipvar); - int_vector& truep = m_vars[flipvar].m_watch[flip_is_true]; - int_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true]; + int_vector const& truep = m_vars[flipvar].m_watch[flip_is_true]; + int_vector const& falsep = m_vars[flipvar].m_watch[!flip_is_true]; - for (unsigned i = 0; i < truep.size(); ++i) { - unsigned ci = truep[i]; + int_vector::const_iterator it = truep.begin(), end = truep.end(); + for (; it != end; ++it) { + unsigned ci = *it; constraint& c = m_constraints[ci]; --c.m_slack; if (c.m_slack == -1) { // from 0 to -1: sat -> unsat unsat(ci); } } - for (unsigned i = 0; i < falsep.size(); ++i) { - unsigned ci = falsep[i]; + it = falsep.begin(), end = falsep.end(); + for (; it != end; ++it) { + unsigned ci = *it; constraint& c = m_constraints[ci]; ++c.m_slack; if (c.m_slack == 0) { // from -1 to 0: unsat -> sat @@ -647,12 +669,12 @@ namespace sat { /* update CCD */ // remove the vars no longer goodvar in goodvar stack - for (unsigned i = goodvar_stack.size(); i > 0;) { + for (unsigned i = m_goodvar_stack.size(); i > 0;) { --i; - v = goodvar_stack[i]; + v = m_goodvar_stack[i]; if (score(v) <= 0) { - goodvar_stack[i] = goodvar_stack.back(); - goodvar_stack.pop_back(); + m_goodvar_stack[i] = m_goodvar_stack.back(); + m_goodvar_stack.pop_back(); m_vars[v].m_in_goodvar_stack = false; } } @@ -664,7 +686,7 @@ namespace sat { v = vi.m_neighbors[i]; m_vars[v].m_conf_change = true; if (score(v) > 0 && !already_in_goodvar_stack(v)) { - goodvar_stack.push_back(v); + m_goodvar_stack.push_back(v); m_vars[v].m_in_goodvar_stack = true; } } @@ -717,11 +739,11 @@ namespace sat { // Unsat Mode: CCD > RD // CCD mode - if (!goodvar_stack.empty()) { + if (!m_goodvar_stack.empty()) { //++ccd; - best_var = goodvar_stack[0]; - for (unsigned i = 1; i < goodvar_stack.size(); ++i) { - bool_var v = goodvar_stack[i]; + best_var = m_goodvar_stack[0]; + for (unsigned i = 1; i < m_goodvar_stack.size(); ++i) { + bool_var v = m_goodvar_stack[i]; if (tie_breaker_ccd(v, best_var)) best_var = v; } @@ -742,24 +764,26 @@ namespace sat { } void local_search::set_parameters() { - + SASSERT(s_id == 0); m_rand.set_seed(m_config.seed()); //srand(m_config.seed()); s_id = m_config.strategy_id(); - best_known_value = m_config.best_known_value(); + m_best_known_value = m_config.best_known_value(); - if (s_id == 0) - max_steps = 2 * (num_vars() - 1); - else { - std::cout << "Invalid strategy id!" << std::endl; - exit(-1); + switch (m_config.mode()) { + case local_search_mode::gsat: + m_max_steps = 2 * num_vars(); + break; + case local_search_mode::wsat: + m_max_steps = std::min(static_cast(20 * num_vars()), static_cast(1 << 17)); // cut steps off at 100K + break; } TRACE("sat", tout << "seed:\t" << m_config.seed() << '\n'; tout << "strategy id:\t" << m_config.strategy_id() << '\n'; tout << "best_known_value:\t" << m_config.best_known_value() << '\n'; - tout << "max_steps:\t" << max_steps << '\n'; + tout << "max_steps:\t" << m_max_steps << '\n'; ); } @@ -808,10 +832,10 @@ namespace sat { std::cout << "3\n"; } } - if (g == goodvar_stack.size()) + if (g == m_goodvar_stack.size()) return true; else { - if (g < goodvar_stack.size()) + if (g < m_goodvar_stack.size()) std::cout << "1\n"; else std::cout << "2\n"; // delete too many diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 5f76f4934..76de2d0e7 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -134,6 +134,10 @@ namespace sat { vector m_constraints; + literal_vector m_assumptions; + + unsigned m_num_non_binary_clauses; + inline bool is_pos(literal t) const { return !t.sign(); } inline bool is_true(bool_var v) const { return cur_solution(v); } inline bool is_true(literal l) const { return cur_solution(l.var()) != l.sign(); } @@ -143,26 +147,23 @@ namespace sat { unsigned constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; } - // int_vector nb_slack; // constraint_k - ob_var(same in ob) - none_ob_true_terms_count. if < 0: some ob var might be flipped to false, result in an ob decreasing - // bool_vector has_true_ob_terms; // unsat constraint stack - int_vector m_unsat_stack; // store all the unsat constraits - int_vector m_index_in_unsat_stack; // which position is a contraint in the unsat_stack + unsigned_vector m_unsat_stack; // store all the unsat constraits + unsigned_vector m_index_in_unsat_stack; // which position is a contraint in the unsat_stack // configuration changed decreasing variables (score>0 and conf_change==true) - int_vector goodvar_stack; + bool_var_vector m_goodvar_stack; - svector m_good_vars; // candidate variables to flip on. // information about solution - int objective_value; // the objective function value corresponds to the current solution - bool_vector best_solution; // !var: the best solution so far - int best_objective_value = -1; // the objective value corresponds to the best solution so far - // for non-known instance, set as maximal - int best_known_value = INT_MAX; // best known value for this instance + int m_objective_value; // the objective function value corresponds to the current solution + bool_vector m_best_solution; // !var: the best solution so far + int m_best_objective_value = -1; // the objective value corresponds to the best solution so far + // for non-known instance, set as maximal + int m_best_known_value = INT_MAX; // best known value for this instance - unsigned max_steps = 2000000000; // < 2147483647 + unsigned m_max_steps = (1 << 30); // for tuning int s_id = 0; // strategy id @@ -228,9 +229,10 @@ namespace sat { void display(std::ostream& out, unsigned v, var_info const& vi) const; + public: - local_search(solver& s); + local_search(); reslimit& rlimit() { return m_limit; } @@ -248,6 +250,10 @@ namespace sat { unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars + unsigned num_non_binary_clauses() const { return m_num_non_binary_clauses; } + + void import(solver& s, bool init); + void set_phase(bool_var v, lbool f); bool get_phase(bool_var v) const { return is_true(v); } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 5504cf6e0..3356763c0 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -77,8 +77,6 @@ namespace sat { literal_vector m_trail; // trail of units unsigned_vector m_trail_lim; - literal_vector m_units; // units learned during lookahead - unsigned_vector m_units_lim; vector m_binary; // literal: binary clauses unsigned_vector m_binary_trail; // trail of added binary clauses unsigned_vector m_binary_trail_lim; @@ -96,7 +94,9 @@ namespace sat { svector m_rating; // var: pre-selection rating unsigned m_bstamp_id; // unique id for binary implication. unsigned m_istamp_id; // unique id for managing double lookaheads - char_vector m_assignment; // literal: assignment + unsigned_vector m_stamp; // var: timestamp with truth value + unsigned m_level; // current level, = 2 * m_trail_lim.size() + const unsigned c_fixed_truth = UINT_MAX - 1; vector m_watches; // literal: watch structure svector m_lits; // literal: attributes. float m_weighted_new_binaries; // metric associated with current lookahead1 literal. @@ -106,6 +106,33 @@ namespace sat { search_mode m_search_mode; // mode of search statistics m_stats; + // --------------------------------------- + // truth values + + inline bool is_fixed(literal l) const { return m_stamp[l.var()] >= m_level; } + inline bool is_undef(literal l) const { return !is_fixed(l); } + inline bool is_undef(bool_var v) const { return m_stamp[v] < m_level; } + inline bool is_false(literal l) const { return is_fixed(l) && (bool)((m_stamp[l.var()] & 0x1) ^ l.sign()); } // even iff l.sign() + inline bool is_true(literal l) const { return is_fixed(l) && !(bool)((m_stamp[l.var()] & 0x1) ^ l.sign()); } + inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); } + inline void set_undef(literal l) { m_stamp[l.var()] = 0; } + + // set the level within a scope of the search. + class scoped_level { + lookahead& m_parent; + unsigned m_save; + public: + scoped_level(lookahead& p, unsigned l): + m_parent(p), m_save(p.m_level) { + p.m_level = l; + } + ~scoped_level() { + m_parent.m_level = m_save; + } + }; + + // ---------------------------------------- + void add_binary(literal l1, literal l2) { SASSERT(l1 != l2); SASSERT(~l1 != l2); @@ -182,6 +209,7 @@ namespace sat { \brief main routine for adding a new binary clause dynamically. */ void try_add_binary(literal u, literal v) { + SASSERT(m_search_mode == searching); SASSERT(u.var() != v.var()); set_bstamps(~u); if (is_stamped(~v)) { @@ -292,7 +320,7 @@ namespace sat { m_candidates.reset(); float sum = 0; for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { - SASSERT(l_undef == value(*it)); + SASSERT(is_undef(*it)); bool_var x = *it; if (!newbies) { // TBD filter out candidates based on prefix strings or similar method @@ -376,20 +404,13 @@ namespace sat { float sum = 0, tsum = 0; literal_vector::iterator it = m_binary[l.index()].begin(), end = m_binary[l.index()].end(); for (; it != end; ++it) { - if (is_free(*it)) sum += h[it->index()]; + if (is_undef(*it)) sum += h[it->index()]; } // TBD walk ternary clauses. sum = (float)(0.1 + afactor*sum + sqfactor*tsum); return std::min(m_config.m_max_score, sum); } - bool is_free(literal l) const { - return !is_unit(l); - } - bool is_unit(literal l) const { - return false; // TBD track variables that are units - } - // ------------------------------------ // Implication graph // Compute implication ordering and strongly connected components. @@ -638,7 +659,7 @@ namespace sat { } SASSERT(2*m_lookahead.size() == offset); TRACE("sat", for (unsigned i = 0; i < m_lookahead.size(); ++i) - tout << m_lookahead[i].m_lit << " : " << m_lookahead[i].m_offset << "\n";); + tout << m_lookahead[i].m_lit << " : " << m_lookahead[i].m_offset << "\n";); } // ------------------------------------ @@ -655,8 +676,8 @@ namespace sat { clause_offset cls_off = m_cls_allocator.get_offset(&c); m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off)); m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off)); - SASSERT(value(c[0]) == l_undef); - SASSERT(value(c[1]) == l_undef); + SASSERT(is_undef(c[0])); + SASSERT(is_undef(c[1])); } } @@ -668,6 +689,9 @@ namespace sat { } void detach_ternary(literal l1, literal l2, literal l3) { + NOT_IMPLEMENTED_YET(); + // there is a clause corresponding to a ternary watch group. + // the clause could be retired / detached. m_retired_ternary.push_back(ternary(l1, l2, l3)); erase_ternary_watch(get_wlist(~l1), l2, l3); erase_ternary_watch(get_wlist(~l2), l1, l3); @@ -680,8 +704,6 @@ namespace sat { // initialization void init_var(bool_var v) { - m_assignment.push_back(l_undef); - m_assignment.push_back(l_undef); m_binary.push_back(literal_vector()); m_binary.push_back(literal_vector()); m_watches.push_back(watch_list()); @@ -738,7 +760,6 @@ namespace sat { unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { literal l = s.m_trail[i]; - m_units.push_back(l); assign(l); } } @@ -746,15 +767,15 @@ namespace sat { // ------------------------------------ // search - void push(literal lit, search_mode mode) { + void push(literal lit, unsigned level) { m_binary_trail_lim.push_back(m_binary_trail.size()); - m_units_lim.push_back(m_units.size()); m_trail_lim.push_back(m_trail.size()); m_retired_clause_lim.push_back(m_retired_clauses.size()); m_qhead_lim.push_back(m_qhead); m_trail.push_back(lit); m_search_modes.push_back(m_search_mode); - m_search_mode = mode; + m_search_mode = searching; + scoped_level _sl(*this, level); assign(lit); propagate(); } @@ -766,6 +787,7 @@ namespace sat { m_search_mode = m_search_modes.back(); m_search_modes.pop_back(); + // not for lookahead // unretire clauses unsigned rsz = m_retired_clause_lim.back(); for (unsigned i = rsz; i < m_retired_clauses.size(); ++i) { @@ -774,6 +796,7 @@ namespace sat { m_retired_clauses.resize(rsz); m_retired_clause_lim.pop_back(); + // m_search_mode == searching // remove local binary clauses unsigned old_sz = m_binary_trail_lim.back(); m_binary_trail_lim.pop_back(); @@ -781,30 +804,31 @@ namespace sat { del_binary(m_binary_trail[i]); } + // not for lookahead. + // m_freevars only for main search // undo assignments for (unsigned i = m_trail.size(); i > m_trail_lim.size(); ) { --i; literal l = m_trail[i]; + set_undef(l); m_freevars.insert(l.var()); - m_assignment[l.index()] = l_undef; - m_assignment[(~l).index()] = l_undef; } m_trail.shrink(m_trail_lim.size()); // reset assignment. m_trail_lim.pop_back(); - // add implied binary clauses - unsigned new_unit_sz = m_units_lim.back(); - for (unsigned i = new_unit_sz; i < m_units.size(); ++i) { - try_add_binary(~m_trail.back(), m_units[i]); - } - m_units.shrink(new_unit_sz); - m_units_lim.pop_back(); - // reset propagation queue m_qhead_lim.pop_back(); m_qhead = m_qhead_lim.back(); } + void push_lookahead2(literal lit) { + + } + + void pop_lookahead2() { + + } + float mix_diff(float l, float r) const { return l + r + (1 << 10) * l * r; } clause const& get_clause(watch_list::iterator it) const { @@ -813,14 +837,13 @@ namespace sat { } bool is_nary_propagation(clause const& c, literal l) const { - bool r = c.size() > 2 && ((c[0] == l && value(c[1]) == l_false) || (c[1] == l && value(c[0]) == l_false)); - DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(value(c[j]) == l_false);); + bool r = c.size() > 2 && ((c[0] == l && is_false(c[1])) || (c[1] == l && is_false(c[0]))); + DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(is_false(c[j]));); return r; } void propagate_clauses(literal l) { - SASSERT(value(l) == l_true); - SASSERT(value(~l) == l_false); + SASSERT(is_true(l)); if (inconsistent()) return; watch_list& wlist = m_watches[l.index()]; watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end(); @@ -833,20 +856,24 @@ namespace sat { UNREACHABLE(); // we avoid adding ternary clauses for now. literal l1 = it->get_literal1(); literal l2 = it->get_literal2(); - lbool val1 = value(l1); - lbool val2 = value(l2); - if (val1 == l_false && val2 == l_undef) { - m_stats.m_propagations++; - assign(l2); + if (is_fixed(l1)) { + if (is_false(l1)) { + if (is_undef(l2)) { + m_stats.m_propagations++; + assign(l2); + } + else if (is_false(l2)) { + set_conflict(); + } + } } - else if (val1 == l_undef && val2 == l_false) { - m_stats.m_propagations++; - assign(l1); + else if (is_fixed(l2)) { + if (is_false(l2)) { + m_stats.m_propagations++; + assign(l1); + } } - else if (val1 == l_false && val2 == l_false) { - set_conflict(); - } - else if (val1 == l_undef && val2 == l_undef) { + else { switch (m_search_mode) { case searching: detach_ternary(l, l1, l2); @@ -866,10 +893,10 @@ namespace sat { case watched::CLAUSE: { clause_offset cls_off = it->get_clause_offset(); clause & c = *(s.m_cls_allocator.get_clause(cls_off)); - TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); + TRACE("sat", tout << "propagating " << c << "\n";); if (c[0] == ~l) std::swap(c[0], c[1]); - if (value(c[0]) == l_true) { + if (is_true(c[0])) { it2->set_clause(c[0], cls_off); it2++; break; @@ -878,7 +905,7 @@ namespace sat { literal * l_end = c.end(); bool found = false; for (; l_it != l_end && !found; ++l_it) { - if (value(*l_it) != l_false) { + if (!is_false(*l_it)) { found = true; c[1] = *l_it; *l_it = ~l; @@ -888,10 +915,10 @@ namespace sat { if (found) { found = false; for (; l_it != l_end && !found; ++l_it) { - found = value(*l_it) != l_false; + found = !is_false(*l_it); } // normal clause was converted to a binary clause. - if (!found && value(c[1]) == l_undef && value(c[0]) == l_undef) { + if (!found && is_undef(c[1]) && is_undef(c[0])) { switch (m_search_mode) { case searching: detach_clause(c); @@ -906,11 +933,11 @@ namespace sat { } break; } - if (value(c[0]) == l_false) { + if (is_false(c[0])) { set_conflict(); } else { - SASSERT(value(c[0]) == l_undef); + SASSERT(is_undef(c[0])); *it2 = *it; it2++; m_stats.m_propagations++; @@ -929,14 +956,7 @@ namespace sat { for (; it != end; ++it, ++it2) { *it2 = *it; } - wlist.set_end(it2); - - - // - // TBD: count binary clauses created by propagation. - // They used to be in the watch list of l.index(), - // both new literals in watch list should be unassigned. - // + wlist.set_end(it2); } void propagate_binary(literal l) { @@ -958,78 +978,100 @@ namespace sat { } literal choose() { - literal l; - while (!choose1(l)) {}; + literal l = null_literal; + while (l == null_literal) { + pre_select(); + if (m_lookahead.empty()) { + break; + } + compute_wnb(); + if (inconsistent()) { + break; + } + l = select_literal(); + } return l; } - // TBD: - // Handle scope properly for nested implications. - // Suppose u -> v, and u -> w and we process v first, then the - // consequences of v should remain when processing u. - // March and sat11.w solve this by introducing timestamps on truth values. - // regular push/pop doesn't really work here: we basically need a traversal of the - // lookahead tree and push/pop according to that (or adapt timestamps) - // - bool choose1(literal& l) { - pre_select(); - l = null_literal; - if (m_lookahead.empty()) { - return true; - } - float h = 0; - unsigned count = 1; + void compute_wnb() { + init_wnb(); for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { literal lit = m_lookahead[i].m_lit; - if (value(lit) != l_undef) { + if (!is_undef(lit)) { continue; } - SASSERT(value(lit) == l_undef); - SASSERT(!inconsistent()); - reset_wnb(lit); - push(lit, lookahead1); - do_double(lit); - if (inconsistent()) { - pop(); + push_lookahead1(lit, 2 + m_lookahead[i].m_offset); + bool unsat = inconsistent(); + // TBD do_double(lit); + pop_lookahead1(); + update_wnb(lit); + if (unsat) { + reset_wnb(); assign(~lit); propagate(); - continue; + init_wnb(); } - update_wnb(lit); - float diff1 = m_weighted_new_binaries; - pop(); - - reset_wnb(~lit); - push(~lit, lookahead1); - do_double(~lit); - if (inconsistent()) { - pop(); - assign(lit); - propagate(); - continue; - } - update_wnb(~lit); - float diff2 = m_weighted_new_binaries; - pop(); + } + reset_wnb(); + } + void init_wnb() { + m_qhead_lim.push_back(m_qhead); + m_trail_lim.push_back(m_trail.size()); + } + + void reset_wnb() { + m_qhead = m_qhead_lim.back(); + 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 select_literal() { + literal l = null_literal; + float h = 0; + unsigned count = 1; + for (unsigned i = 0; i < m_lookahead.size(); ++i) { + literal lit = m_lookahead[i].m_lit; + if (lit.sign() || !is_undef(lit)) { + continue; + } + float diff1 = get_wnb(lit), diff2 = get_wnb(~lit); float mixd = mix_diff(diff1, diff2); + if (mixd == h) ++count; if (mixd > h || (mixd == h && s.m_rand(count) == 0)) { - CTRACE("sat", l != null_literal, tout << lit << " diff1: " << diff1 << " diff2: " << diff2 << "\n";); - if (mixd > h) count = 1; else ++count; + CTRACE("sat", l != null_literal, tout << lit << " " << mixd << "\n";); + if (mixd > h) count = 1; h = mixd; l = diff1 < diff2 ? lit : ~lit; } } - return l != null_literal || inconsistent(); + return l; + } + + void push_lookahead1(literal lit, unsigned level) { + m_search_modes.push_back(m_search_mode); + m_search_mode = lookahead1; + scoped_level _sl(*this, level); + assign(lit); + propagate(); + } + + void pop_lookahead1() { + SASSERT(!inconsistent()); + m_search_mode = m_search_modes.back(); + m_search_modes.pop_back(); } void set_wnb(literal l, float f) { m_lits[l.index()].m_wnb = f; } void inc_wnb(literal l, float f) { m_lits[l.index()].m_wnb += f; } float get_wnb(literal l) const { return m_lits[l.index()].m_wnb; } - bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; } - void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; } void reset_wnb(literal l) { m_weighted_new_binaries = 0; @@ -1048,24 +1090,27 @@ namespace sat { } } + bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; } + void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; } + void double_look() { bool unsat; for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { literal lit = m_lookahead[i].m_lit; - if (value(lit) != l_undef) continue; + if (!is_undef(lit)) continue; - push(lit, lookahead2); + push_lookahead2(lit); unsat = inconsistent(); - pop(); + pop_lookahead2(); if (unsat) { TRACE("sat", tout << "unit: " << ~lit << "\n";); assign(~lit); continue; } - push(~lit, lookahead2); + push_lookahead2(~lit); unsat = inconsistent(); - pop(); + pop_lookahead2(); if (unsat) { TRACE("sat", tout << "unit: " << lit << "\n";); assign(lit); @@ -1073,31 +1118,25 @@ namespace sat { } } - bool is_fixed(literal l) const { return value(l) != l_undef; } - bool is_contrary(literal l) const { return value(l) == l_false; } - bool is_true(literal l) const { return value(l) == l_true; } + void set_conflict() { m_inconsistent = true; } - lbool value(literal l) const { return static_cast(m_assignment[l.index()]); } - lbool value(bool_var v) const { return value(literal(v, false)); } + bool inconsistent() { return m_inconsistent; } + unsigned scope_lvl() const { return m_trail_lim.size(); } void assign(literal l) { - switch (value(l)) { - case l_true: - break; - case l_false: - set_conflict(); - break; - default: - m_assignment[l.index()] = l.sign() ? l_false : l_true; - m_assignment[(~l).index()] = l.sign() ? l_false : l_true; + if (is_undef(l)) { + set_true(l); m_trail.push_back(l); - m_freevars.remove(l.var()); - break; + if (m_search_mode == searching) { + m_freevars.remove(l.var()); + } + } + else if (is_false(l)) { + set_conflict(); } } - bool inconsistent() { return m_inconsistent; } void do_double(literal l) { if (!inconsistent() && scope_lvl() > 0 && dl_enabled(l)) { @@ -1115,7 +1154,8 @@ namespace sat { bool backtrack(literal_vector& trail) { if (trail.empty()) return false; pop(); - assign(~trail.back()); + assign(~trail.back()); + propagate(); trail.pop_back(); return true; } @@ -1124,6 +1164,7 @@ namespace sat { literal_vector trail; m_search_mode = searching; while (true) { + TRACE("sat", display(tout);); inc_istamp(); s.checkpoint(); literal l = choose(); @@ -1135,19 +1176,55 @@ namespace sat { return l_true; } TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); - push(l, searching); + push(l, c_fixed_truth); trail.push_back(l); } } + std::ostream& display_binary(std::ostream& out) const { + for (unsigned i = 0; i < m_binary.size(); ++i) { + literal_vector const& lits = m_binary[i]; + if (!lits.empty()) { + out << to_literal(i) << " -> " << lits << "\n"; + } + } + return out; + } + + std::ostream& display_clauses(std::ostream& out) const { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + out << *m_clauses[i] << "\n"; + } + return out; + } + + std::ostream& display_values(std::ostream& out) const { + for (unsigned i = 0; i < m_trail.size(); ++i) { + literal l = m_trail[i]; + out << l << " " << m_stamp[l.var()] << "\n"; + } + return out; + } + + public: - lookahead(solver& s) : s(s) { + lookahead(solver& s) : + s(s), + m_level(0) { + scoped_level _sl(*this, c_fixed_truth); init(); } lbool check() { return search(); } + + std::ostream& display(std::ostream& out) const { + display_values(out); + display_binary(out); + display_clauses(out); + return out; + } }; } diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 4eb247fc0..6652bfc3e 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -139,9 +139,6 @@ namespace sat { } } limit = m_units.size(); - - _get_phase(s); - _set_phase(s); } } @@ -228,6 +225,12 @@ namespace sat { break; } } + if (90 * m_num_clauses > 100 * s.m_clauses.size() && !m_solver_copy) { + // time to update local search with new clauses. + IF_VERBOSE(1, verbose_stream() << "(sat-parallel refresh local search " << m_num_clauses << " -> " << s.m_clauses.size() << ")\n";); + m_solver_copy = alloc(solver, s.m_params, s.rlimit()); + m_solver_copy->copy(s); + } } } @@ -261,10 +264,16 @@ namespace sat { void parallel::get_phase(local_search& s) { #pragma omp critical (par_solver) { + if (m_solver_copy) { + s.import(*m_solver_copy.get(), true); + m_solver_copy = 0; + } for (unsigned i = 0; i < m_phase.size(); ++i) { s.set_phase(i, m_phase[i]); + m_phase[i] = l_undef; } m_phase.reserve(s.num_vars(), l_undef); + m_num_clauses = s.num_non_binary_clauses(); } } @@ -275,6 +284,7 @@ namespace sat { for (unsigned i = 0; i < s.num_vars(); ++i) { m_phase[i] = s.get_phase(i) ? l_true : l_false; } + m_num_clauses = s.num_non_binary_clauses(); } } diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index 4d8e4a82d..b93384bd6 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -60,7 +60,11 @@ namespace sat { index_set m_unit_set; literal_vector m_lits; vector_pool m_pool; - svector m_phase; + + // for exchange with local search: + svector m_phase; + unsigned m_num_clauses; + scoped_ptr m_solver_copy; scoped_limits m_scoped_rlimit; vector m_limits; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 01657951d..e6508ea51 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -82,15 +82,15 @@ namespace sat { void solver::copy(solver const & src) { pop_to_base_level(); - SASSERT(m_mc.empty() && src.m_mc.empty()); - SASSERT(at_search_lvl()); // create new vars if (num_vars() < src.num_vars()) { for (bool_var v = num_vars(); v < src.num_vars(); v++) { - SASSERT(!src.was_eliminated(v)); bool ext = src.m_external[v] != 0; bool dvar = src.m_decision[v] != 0; VERIFY(v == mk_var(ext, dvar)); + if (src.was_eliminated(v)) { + m_eliminated[v] = true; + } } } // @@ -854,19 +854,14 @@ namespace sat { ERROR_EX }; - local_search& solver::init_local_search() { - if (!m_local_search) { - m_local_search = alloc(local_search, *this); - } - return *m_local_search.get(); - } - lbool solver::check_par(unsigned num_lits, literal const* lits) { bool use_local_search = m_config.m_local_search; + scoped_ptr ls; if (use_local_search) { - m_local_search = alloc(local_search, *this); - m_local_search->config().set_seed(m_config.m_random_seed); + ls = alloc(local_search); + ls->config().set_seed(m_config.m_random_seed); + ls->import(*this, false); } int num_threads = static_cast(m_config.m_num_threads) + (use_local_search ? 1 : 0); int num_extra_solvers = num_threads - 1 - (use_local_search ? 1 : 0); @@ -890,7 +885,7 @@ namespace sat { r = par.get_solver(i).check(num_lits, lits); } else if (IS_LOCAL_SEARCH(i)) { - r = m_local_search->check(num_lits, lits, &par); + r = ls->check(num_lits, lits, &par); } else { r = check(num_lits, lits); @@ -905,8 +900,8 @@ namespace sat { } } if (first) { - if (m_local_search) { - m_local_search->rlimit().cancel(); + if (ls) { + ls->rlimit().cancel(); } for (int j = 0; j < num_extra_solvers; ++j) { if (i != j) { @@ -942,13 +937,13 @@ namespace sat { m_core.append(par.get_solver(finished_id).get_core()); } if (result == l_true && finished_id != -1 && IS_LOCAL_SEARCH(finished_id)) { - set_model(m_local_search->get_model()); + set_model(ls->get_model()); } if (!canceled) { rlimit().reset_cancel(); } set_par(0, 0); - m_local_search = 0; + ls = 0; if (finished_id == -1) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 5ca668ff8..c35a0296c 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -90,7 +90,6 @@ namespace sat { probing m_probing; mus m_mus; // MUS for minimal core extraction drat m_drat; // DRAT for generating proofs - scoped_ptr m_local_search; bool m_inconsistent; bool m_searching; // A conflict is usually a single justification. That is, a justification