diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index b65abfd23..47cb29694 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -26,7 +26,8 @@ Notes: namespace sat { void local_search::init() { - + flet _init(m_initializing, true); + m_unsat_stack.reset(); for (unsigned i = 0; i < m_assumptions.size(); ++i) { add_clause(1, m_assumptions.c_ptr() + i); } @@ -37,7 +38,7 @@ namespace sat { if (m_config.phase_sticky()) { for (var_info& vi : m_vars) if (!vi.m_unit) - vi.m_value = vi.m_bias < 100; + vi.m_value = vi.m_bias > 50; } else { for (var_info& vi : m_vars) @@ -45,42 +46,14 @@ namespace sat { vi.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); - - if (m_config.mode() == local_search_mode::gsat) { - uint_set is_neighbor; - for (bool_var v = 0; v < num_vars(); ++v) { - is_neighbor.reset(); - bool pol = true; - var_info& vi = m_vars[v]; - for (unsigned k = 0; k < 2; pol = !pol, k++) { - for (auto const& wi : m_vars[v].m_watch[pol]) { - constraint const& c = m_constraints[wi.m_constraint_id]; - for (literal lit : c) { - bool_var w = lit.var(); - if (w == v || is_neighbor.contains(w)) continue; - is_neighbor.insert(w); - vi.m_neighbors.push_back(w); - } - } - } - } - } - - for (auto const& c : ob_constraint) { - coefficient_in_ob_constraint[c.var_id] = c.coefficient; - } - set_parameters(); } void local_search::init_cur_solution() { for (var_info& vi : m_vars) { - // use bias with a small probability if (!vi.m_unit) { - if (m_rand() % 10 < 5 || m_config.phase_sticky()) { + if (m_config.phase_sticky()) { vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias); } else { @@ -116,7 +89,6 @@ namespace sat { coeff_vector& falsep = m_vars[v].m_watch[!is_true]; for (auto const& coeff : falsep) { constraint& c = m_constraints[coeff.m_constraint_id]; - //SASSERT(falsep[i].m_coeff == 1); // will --slack if (c.m_slack <= 0) { dec_slack_score(v); @@ -125,7 +97,6 @@ namespace sat { } } for (auto const& coeff : truep) { - //SASSERT(coeff.m_coeff == 1); constraint& c = m_constraints[coeff.m_constraint_id]; // will --true_terms_count[c] // will ++slack @@ -151,22 +122,19 @@ namespace sat { void local_search::reinit() { - IF_VERBOSE(1, verbose_stream() << "(sat-local-search reinit)\n";); - if (true || !m_is_pb) { - // - // the following methods does NOT converge for pseudo-boolean - // can try other way to define "worse" and "better" - // the current best noise is below 1000 - // - if (m_best_unsat_rate > m_last_best_unsat_rate) { - // worse - m_noise -= m_noise * 2 * m_noise_delta; - m_best_unsat_rate *= 1000.0; - } - else { - // better - m_noise += (10000 - m_noise) * m_noise_delta; - } + // + // the following methods does NOT converge for pseudo-boolean + // can try other way to define "worse" and "better" + // the current best noise is below 1000 + // + if (m_best_unsat_rate > m_last_best_unsat_rate) { + // worse + m_noise -= m_noise * 2 * m_noise_delta; + m_best_unsat_rate *= 1000.0; + } + else { + // better + m_noise += (10000 - m_noise) * m_noise_delta; } for (constraint & c : m_constraints) { @@ -186,11 +154,9 @@ namespace sat { m_vars.back().m_score = INT_MIN; 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 = 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; m_vars[i].m_conf_change = true; m_vars[i].m_in_goodvar_stack = false; m_vars[i].m_score = 0; @@ -208,6 +174,7 @@ namespace sat { if (m_is_unsat) { IF_VERBOSE(0, verbose_stream() << "unsat during reinit\n"); } + DEBUG_CODE(verify_slack();); } bool local_search::propagate(literal lit) { @@ -230,9 +197,9 @@ namespace sat { return false; } if (unit) { - for (literal lit : m_prop_queue) { - VERIFY(is_true(lit)); - add_unit(lit); + for (literal lit2 : m_prop_queue) { + VERIFY(is_true(lit2)); + add_unit(lit2, lit); } } return true; @@ -253,32 +220,7 @@ namespace sat { constraint const& c = m_constraints[m_unsat_stack[0]]; IF_VERBOSE(2, display(verbose_stream() << "single unsat:", c)); } - } - - void local_search::calculate_and_update_ob() { - unsigned i, v; - 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 > m_best_objective_value) { - m_best_solution.reset(); - for (unsigned v = 0; v < num_vars(); ++v) { - m_best_solution.push_back(cur_solution(v)); - } - m_best_objective_value = objective_value; - } - } - - bool local_search::all_objectives_are_met() const { - for (unsigned i = 0; i < ob_constraint.size(); ++i) { - bool_var v = ob_constraint[i].var_id; - if (!cur_solution(v)) return false; - } - return true; - } + } void local_search::verify_solution() const { IF_VERBOSE(0, verbose_stream() << "verifying solution\n"); @@ -289,10 +231,24 @@ namespace sat { void local_search::verify_unsat_stack() const { for (unsigned i : m_unsat_stack) { constraint const& c = m_constraints[i]; + if (c.m_k >= constraint_value(c)) { + IF_VERBOSE(0, display(verbose_stream() << i << " ", c) << "\n"); + IF_VERBOSE(0, verbose_stream() << "units " << m_units << "\n"); + } VERIFY(c.m_k < constraint_value(c)); } } + bool local_search::verify_goodvar() const { + unsigned g = 0; + for (unsigned v = 0; v < num_vars(); ++v) { + if (conf_change(v) && score(v) > 0) { + ++g; + } + } + return g == m_goodvar_stack.size(); + } + unsigned local_search::constraint_coeff(constraint const& c, literal l) const { for (auto const& pb : m_vars[l.var()].m_watch[is_pos(l)]) { if (pb.m_constraint_id == c.m_id) return pb.m_coeff; @@ -301,6 +257,24 @@ namespace sat { return 0; } + void local_search::verify_constraint(constraint const& c) const { + unsigned value = constraint_value(c); + IF_VERBOSE(11, display(verbose_stream() << "verify ", c);); + TRACE("sat", display(verbose_stream() << "verify ", c);); + if (c.m_k < value) { + IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c) << "value: " << value << "\n";); + } + } + + void local_search::verify_slack(constraint const& c) const { + VERIFY(constraint_value(c) + c.m_slack == c.m_k); + } + + void local_search::verify_slack() const { + for (constraint const& c : m_constraints) { + verify_slack(c); + } + } unsigned local_search::constraint_value(constraint const& c) const { unsigned value = 0; @@ -311,15 +285,6 @@ namespace sat { } return value; } - - void local_search::verify_constraint(constraint const& c) const { - unsigned value = constraint_value(c); - IF_VERBOSE(11, display(verbose_stream() << "verify ", c);); - TRACE("sat", display(verbose_stream() << "verify ", c);); - if (c.m_k < value) { - IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c) << "value: " << value << "\n";); - } - } void local_search::add_clause(unsigned sz, literal const* c) { add_cardinality(sz, c, sz - 1); @@ -328,7 +293,7 @@ namespace sat { // ~c <= k void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { if (sz == 1 && k == 0) { - add_unit(c[0]); + add_unit(c[0], null_literal); return; } if (k == 1 && sz == 2) { @@ -353,7 +318,7 @@ namespace sat { // c * coeffs <= k void local_search::add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { if (sz == 1 && k == 0) { - add_unit(~c[0]); + add_unit(~c[0], null_literal); return; } unsigned id = m_constraints.size(); @@ -366,15 +331,19 @@ namespace sat { } } - void local_search::add_unit(literal lit) { + void local_search::add_unit(literal lit, literal exp) { bool_var v = lit.var(); if (is_unit(lit)) return; - VERIFY(!m_units.contains(v)); - m_vars[v].m_bias = lit.sign() ? 0 : 100; + SASSERT(!m_units.contains(v)); + if (m_vars[v].m_value == lit.sign() && !m_initializing) { + flip_walksat(v); + } m_vars[v].m_value = !lit.sign(); + m_vars[v].m_bias = lit.sign() ? 0 : 100; m_vars[v].m_unit = true; + m_vars[v].m_explain = exp; m_units.push_back(v); - verify_unsat_stack(); + DEBUG_CODE(verify_unsat_stack();); } local_search::local_search() : @@ -383,19 +352,19 @@ namespace sat { } void local_search::import(solver& s, bool _init) { + flet linit(m_initializing, true); m_is_pb = false; m_vars.reset(); m_constraints.reset(); m_units.reset(); m_unsat_stack.reset(); - m_vars.reserve(s.num_vars()); + m_config.set_config(s.get_config()); + if (m_config.phase_sticky()) { unsigned v = 0; for (var_info& vi : m_vars) { - if (!vi.m_unit) - vi.m_bias = s.m_phase[v] == POS_PHASE ? 100 : 0; - ++v; + vi.m_bias = s.m_phase[v++] == POS_PHASE ? 98 : 2; } } @@ -524,9 +493,6 @@ namespace sat { local_search::~local_search() { } - void local_search::add_soft(bool_var v, int weight) { - ob_constraint.push_back(ob_term(v, weight)); - } lbool local_search::check() { return check(0, nullptr); @@ -534,7 +500,7 @@ namespace sat { #define PROGRESS(tries, flips) \ if (tries % 10 == 0 || m_unsat_stack.empty()) { \ - IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ + IF_VERBOSE(1, verbose_stream() << "(sat.local-search" \ << " :flips " << flips \ << " :noise " << m_noise \ << " :unsat " << /*m_unsat_stack.size()*/ m_best_unsat \ @@ -547,10 +513,10 @@ namespace sat { m_last_best_unsat_rate = 1; reinit(); + DEBUG_CODE(verify_slack();); timer timer; timer.start(); unsigned step = 0, total_flips = 0, tries = 0; - PROGRESS(tries, total_flips); for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { ++m_stats.m_num_restarts; @@ -572,39 +538,7 @@ namespace sat { reinit(); } } - } - - void local_search::gsat() { - reinit(); - bool_var flipvar; - timer timer; - timer.start(); - unsigned tries, step = 0, total_flips = 0; - for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) { - reinit(); - for (step = 1; step <= m_max_steps; ) { - // feasible - if (m_unsat_stack.empty()) { - calculate_and_update_ob(); - if (m_best_objective_value >= m_best_known_value) { - break; - } - } - if (m_unsat_stack.size() < m_best_unsat) { - set_best_unsat(); - } - flipvar = pick_var_gsat(); - flip_gsat(flipvar); - m_vars[flipvar].m_time_stamp = step++; - } - 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(0, total_flips); } lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) { @@ -612,28 +546,24 @@ namespace sat { m_model.reset(); m_assumptions.reset(); m_assumptions.append(sz, assumptions); + unsigned num_units = m_units.size(); init(); - - switch (m_config.mode()) { - case local_search_mode::gsat: - gsat(); - break; - case local_search_mode::wsat: - walksat(); - break; + walksat(); + + // remove unit clauses + for (unsigned i = m_units.size(); i-- > num_units; ) { + m_vars[m_units[i]].m_unit = false; } - - // remove unit clauses from assumptions. - m_constraints.shrink(num_constraints() - sz); + m_units.shrink(num_units); + m_vars.pop_back(); // remove sentinel variable TRACE("sat", display(tout);); lbool result; if (m_is_unsat) { - // result = l_false; - result = l_undef; + result = l_false; } - else if (m_unsat_stack.empty() && all_objectives_are_met()) { + else if (m_unsat_stack.empty()) { verify_solution(); extract_model(); result = l_true; @@ -641,7 +571,7 @@ namespace sat { else { result = l_undef; } - IF_VERBOSE(1, verbose_stream() << "(sat-local-search " << result << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(sat.local-search " << result << ")\n";); IF_VERBOSE(20, display(verbose_stream());); return result; } @@ -763,7 +693,7 @@ namespace sat { if (is_true(lit)) { flip_walksat(best_var); } - add_unit(~lit); + add_unit(~lit, null_literal); if (!propagate(~lit)) { IF_VERBOSE(0, verbose_stream() << "unsat\n"); m_is_unsat = true; @@ -779,6 +709,7 @@ namespace sat { } void local_search::flip_walksat(bool_var flipvar) { + ++m_stats.m_num_flips; VERIFY(!is_unit(flipvar)); m_vars[flipvar].m_value = !cur_solution(flipvar); @@ -794,6 +725,7 @@ namespace sat { constraint& c = m_constraints[ci]; int old_slack = c.m_slack; c.m_slack -= pbc.m_coeff; + DEBUG_CODE(verify_slack(c);); if (c.m_slack < 0 && old_slack >= 0) { // from non-negative to negative: sat -> unsat unsat(ci); } @@ -803,220 +735,21 @@ namespace sat { constraint& c = m_constraints[ci]; int old_slack = c.m_slack; c.m_slack += pbc.m_coeff; + DEBUG_CODE(verify_slack(c);); if (c.m_slack >= 0 && old_slack < 0) { // from negative to non-negative: unsat -> sat sat(ci); } } - // verify_unsat_stack(); - } - - void local_search::flip_gsat(bool_var flipvar) { - // already changed truth value!!!! - m_vars[flipvar].m_value = !cur_solution(flipvar); - - unsigned v; - int org_flipvar_score = score(flipvar); - int org_flipvar_slack_score = slack_score(flipvar); - - bool flip_is_true = cur_solution(flipvar); - coeff_vector& truep = m_vars[flipvar].m_watch[flip_is_true]; - coeff_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true]; - - // update related clauses and neighbor vars - for (unsigned i = 0; i < truep.size(); ++i) { - constraint & c = m_constraints[truep[i].m_constraint_id]; - //++true_terms_count[c]; - --c.m_slack; - switch (c.m_slack) { - case -2: // from -1 to -2 - for (literal l : c) { - v = l.var(); - // flipping the slack increasing var will no longer satisfy this constraint - if (is_true(l)) { - //score[v] -= constraint_weight[c]; - dec_score(v); - } - } - break; - case -1: // from 0 to -1: sat -> unsat - for (literal l : c) { - v = l.var(); - inc_cscc(v); - //score[v] += constraint_weight[c]; - inc_score(v); - // slack increasing var - if (is_true(l)) - inc_slack_score(v); - } - unsat(truep[i].m_constraint_id); - break; - case 0: // from 1 to 0 - for (literal l : c) { - v = l.var(); - // flip the slack decreasing var will falsify this constraint - if (is_false(l)) { - // score[v] -= constraint_weight[c]; - dec_score(v); - dec_slack_score(v); - } - } - break; - default: - break; - } - } - for (pbcoeff const& f : falsep) { - constraint& c = m_constraints[f.m_constraint_id]; - //--true_terms_count[c]; - ++c.m_slack; - switch (c.m_slack) { - case 1: // from 0 to 1 - for (literal l : c) { - v = l.var(); - // flip the slack decreasing var will no long falsify this constraint - if (is_false(l)) { - //score[v] += constraint_weight[c]; - inc_score(v); - inc_slack_score(v); - } - } - break; - case 0: // from -1 to 0: unsat -> sat - for (literal l : c) { - v = l.var(); - inc_cscc(v); - //score[v] -= constraint_weight[c]; - dec_score(v); - // slack increasing var no longer sat this var - if (is_true(l)) - dec_slack_score(v); - } - sat(f.m_constraint_id); - break; - case -1: // from -2 to -1 - for (literal l : c) { - v = l.var(); - // flip the slack increasing var will satisfy this constraint - if (is_true(l)) { - //score[v] += constraint_weight[c]; - inc_score(v); - } - } - break; - default: - break; - } - } - m_vars[flipvar].m_score = -org_flipvar_score; - m_vars[flipvar].m_slack_score = -org_flipvar_slack_score; - m_vars[flipvar].m_conf_change = false; - m_vars[flipvar].m_cscc = 0; - - /* update CCD */ - // remove the vars no longer goodvar in goodvar stack - for (unsigned i = m_goodvar_stack.size(); i > 0;) { - --i; - v = m_goodvar_stack[i]; - if (score(v) <= 0) { - m_goodvar_stack[i] = m_goodvar_stack.back(); - m_goodvar_stack.pop_back(); - m_vars[v].m_in_goodvar_stack = false; - } - } - // update all flipvar's neighbor's conf_change to true, add goodvar/okvar - - var_info& vi = m_vars[flipvar]; - for (auto v : vi.m_neighbors) { - m_vars[v].m_conf_change = true; - if (score(v) > 0 && !already_in_goodvar_stack(v)) { - m_goodvar_stack.push_back(v); - m_vars[v].m_in_goodvar_stack = true; - } - } - } - - bool local_search::tie_breaker_sat(bool_var v, bool_var best_var) { - // most improvement on objective value - int v_imp = cur_solution(v) ? -coefficient_in_ob_constraint.get(v, 0) : coefficient_in_ob_constraint.get(v, 0); - int b_imp = cur_solution(best_var) ? -coefficient_in_ob_constraint.get(best_var, 0) : coefficient_in_ob_constraint.get(best_var, 0); - // std::cout << v_imp << "\n"; - // break tie 1: max imp - // break tie 2: conf_change - // break tie 3: time_stamp - - return - (v_imp > b_imp) || - ((v_imp == b_imp) && - ((conf_change(v) && !conf_change(best_var)) || - ((conf_change(v) == conf_change(best_var)) && - (time_stamp(v) < time_stamp(best_var))))); - } - - bool local_search::tie_breaker_ccd(bool_var v, bool_var best_var) { - // break tie 1: max score - // break tie 2: max slack_score - // break tie 3: cscc - // break tie 4: oldest one - return - ((score(v) > score(best_var)) || - ((score(v) == score(best_var)) && - ((slack_score(v) > slack_score(best_var)) || - ((slack_score(v) == slack_score(best_var)) && - ((cscc(v) > cscc(best_var)) || - ((cscc(v) == cscc(best_var)) && - (time_stamp(v) < time_stamp(best_var)))))))); - } - - bool_var local_search::pick_var_gsat() { - bool_var best_var = m_vars.size()-1; // sentinel variable - // SAT Mode - if (m_unsat_stack.empty()) { - //std::cout << "as\t"; - for (auto const& c : ob_constraint) { - bool_var v = c.var_id; - if (tie_breaker_sat(v, best_var)) - best_var = v; - } - return best_var; - } - - // Unsat Mode: CCD > RD - // CCD mode - if (!m_goodvar_stack.empty()) { - //++ccd; - best_var = m_goodvar_stack[0]; - for (bool_var v : m_goodvar_stack) { - if (tie_breaker_ccd(v, best_var)) - best_var = v; - } - return best_var; - } - - // Diversification Mode - constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; // a random unsat constraint - // Within c, from all slack increasing var, choose the oldest one - for (literal l : c) { - bool_var v = l.var(); - if (is_true(l) && time_stamp(v) < time_stamp(best_var)) - best_var = v; - } - return best_var; + DEBUG_CODE(verify_unsat_stack();); } void local_search::set_parameters() { m_rand.set_seed(m_config.random_seed()); m_best_known_value = m_config.best_known_value(); - 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; - } - + m_max_steps = std::min(static_cast(20 * num_vars()), static_cast(1 << 17)); // cut steps off at 100K + TRACE("sat", tout << "seed:\t" << m_config.random_seed() << '\n'; tout << "best_known_value:\t" << m_config.best_known_value() << '\n'; @@ -1062,7 +795,9 @@ namespace sat { } std::ostream& local_search::display(std::ostream& out, unsigned v, var_info const& vi) const { - return out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n"; + out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias; + if (vi.m_unit) out << " u " << vi.m_explain; + return out << "\n"; } void local_search::collect_statistics(statistics& st) const { @@ -1078,26 +813,6 @@ namespace sat { } - bool local_search::check_goodvar() { - unsigned g = 0; - for (unsigned v = 0; v < num_vars(); ++v) { - if (conf_change(v) && score(v) > 0) { - ++g; - if (!already_in_goodvar_stack(v)) - std::cout << "3\n"; - } - } - if (g == m_goodvar_stack.size()) - return true; - else { - if (g < m_goodvar_stack.size()) - std::cout << "1\n"; - else - std::cout << "2\n"; // delete too many - return false; - } - } - void local_search::set_phase(bool_var v, lbool f) { unsigned& bias = m_vars[v].m_bias; if (f == l_true && bias < 100) bias++; @@ -1105,4 +820,13 @@ namespace sat { // f == l_undef ? } + void local_search::set_bias(bool_var v, lbool f) { + switch (f) { + case l_true: m_vars[v].m_bias = 99; break; + case l_false: m_vars[v].m_bias = 1; break; + default: break; + } + + } + } diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 849b4f26b..f1ef29158 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -36,6 +36,16 @@ namespace sat { local_search_mode m_mode; bool m_phase_sticky; bool m_dbg_flips; + + friend class local_search; + + void set_config(config const& cfg) { + m_mode = cfg.m_local_search_mode; + m_random_seed = cfg.m_random_seed; + m_phase_sticky = cfg.m_phase_sticky; + m_dbg_flips = cfg.m_local_search_dbg_flips; + } + public: local_search_config() { m_random_seed = 0; @@ -54,12 +64,6 @@ namespace sat { void set_random_seed(unsigned s) { m_random_seed = s; } void set_best_known_value(unsigned v) { m_best_known_value = v; } - void set_config(config const& cfg) { - m_mode = cfg.m_local_search_mode; - m_random_seed = cfg.m_random_seed; - m_phase_sticky = cfg.m_phase_sticky; - m_dbg_flips = cfg.m_local_search_dbg_flips; - } }; @@ -74,12 +78,6 @@ namespace sat { typedef svector bool_vector; typedef svector coeff_vector; - // data structure for a term in objective function - struct ob_term { - bool_var var_id; // variable id, begin with 1 - int coefficient; // non-zero integer - ob_term(bool_var v, int c): var_id(v), coefficient(c) {} - }; struct stats { unsigned m_num_flips; @@ -93,12 +91,12 @@ namespace sat { unsigned m_bias; // bias for current solution in percentage. // if bias is 0, then value is always false, if 100, then always true bool m_unit; // is this a unit literal + literal m_explain; // explanation for unit assignment bool m_conf_change; // whether its configure changes since its last flip bool m_in_goodvar_stack; int m_score; int m_slack_score; int m_time_stamp; // the flip time stamp - int m_cscc; // how many times its constraint state configure changes since its last flip bool_var_vector m_neighbors; // neighborhood variables coeff_vector m_watch[2]; literal_vector m_bin[2]; @@ -112,7 +110,6 @@ namespace sat { m_in_goodvar_stack(false), m_score(0), m_slack_score(0), - m_cscc(0), m_flips(0), m_slow_break(1e-5) {} @@ -132,19 +129,44 @@ namespace sat { literal const* end() const { return m_literals.end(); } }; - stats m_stats; - local_search_config m_config; - - // objective function: maximize - svector ob_constraint; // the objective function *constraint*, sorted in descending order - - // information about the variable - int_vector coefficient_in_ob_constraint; // var! initialized to be 0 + stats m_stats; + local_search_config m_config; + vector m_vars; // variables + svector m_units; // unit clauses + vector m_constraints; // all constraints + literal_vector m_assumptions; // temporary assumptions + literal_vector m_prop_queue; // propagation queue + unsigned m_num_non_binary_clauses; + bool m_is_pb; + bool m_is_unsat; + unsigned_vector m_unsat_stack; // store all the unsat constraints + unsigned_vector m_index_in_unsat_stack; // which position is a constraint in the unsat_stack + + // configuration changed decreasing variables (score>0 and conf_change==true) + bool_var_vector m_goodvar_stack; + bool m_initializing; + + + // information about solution + unsigned m_best_unsat; + double m_best_unsat_rate; + double m_last_best_unsat_rate; + // for non-known instance, set as maximal + int m_best_known_value = INT_MAX; // best known value for this instance + + unsigned m_max_steps = (1 << 30); + + // dynamic noise + double m_noise = 9800; // normalized by 10000 + double m_noise_delta = 0.05; + + reslimit m_limit; + random_gen m_rand; + parallel* m_par; + model m_model; - vector m_vars; - svector m_units; inline int score(bool_var v) const { return m_vars[v].m_score; } inline void inc_score(bool_var v) { m_vars[v].m_score++; } @@ -157,21 +179,10 @@ namespace sat { inline bool already_in_goodvar_stack(bool_var v) const { return m_vars[v].m_in_goodvar_stack; } inline bool conf_change(bool_var v) const { return m_vars[v].m_conf_change; } inline int time_stamp(bool_var v) const { return m_vars[v].m_time_stamp; } - inline int cscc(bool_var v) const { return m_vars[v].m_cscc; } - inline void inc_cscc(bool_var v) { m_vars[v].m_cscc++; } - - inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; } inline void set_best_unsat(); /* TBD: other scores */ - vector m_constraints; - - literal_vector m_assumptions; - literal_vector m_prop_queue; - - unsigned m_num_non_binary_clauses; - bool m_is_pb; inline bool is_pos(literal t) const { return !t.sign(); } inline bool is_true(bool_var v) const { return cur_solution(v); } @@ -182,101 +193,37 @@ namespace sat { unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint - unsigned constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; } - // unsat constraint stack - bool m_is_unsat; - unsigned_vector m_unsat_stack; // store all the unsat constraints - unsigned_vector m_index_in_unsat_stack; // which position is a constraint in the unsat_stack - - // configuration changed decreasing variables (score>0 and conf_change==true) - bool_var_vector m_goodvar_stack; - - - // information about solution - unsigned m_best_unsat; - double m_best_unsat_rate; - double m_last_best_unsat_rate; - 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 m_max_steps = (1 << 30); - - // dynamic noise - double m_noise = 9800; // normalized by 10000 - double m_noise_delta = 0.05; - - reslimit m_limit; - random_gen m_rand; - parallel* m_par; - model m_model; - void init(); void reinit(); void reinit_orig(); void init_cur_solution(); void init_slack(); void init_scores(); - void init_goodvars(); - - bool_var pick_var_gsat(); - - void flip_gsat(bool_var v); - + void init_goodvars(); void pick_flip_walksat(); - void flip_walksat(bool_var v); - bool propagate(literal lit); - void add_propagation(literal lit); - void walksat(); - - void gsat(); - void unsat(unsigned c); - void sat(unsigned c); - - bool tie_breaker_sat(bool_var v1, bool_var v2); - - bool tie_breaker_ccd(bool_var v1, bool_var v2); - void set_parameters(); - - void calculate_and_update_ob(); - - bool all_objectives_are_met() const; - void verify_solution() const; - void verify_unsat_stack() const; - void verify_constraint(constraint const& c) const; - + void verify_slack(constraint const& c) const; + void verify_slack() const; + bool verify_goodvar() const; unsigned constraint_value(constraint const& c) const; - unsigned constraint_coeff(constraint const& c, literal l) const; - void print_info(std::ostream& out); - void extract_model(); - - bool check_goodvar(); - void add_clause(unsigned sz, literal const* c); - - void add_unit(literal lit); - + void add_unit(literal lit, literal explain); std::ostream& display(std::ostream& out) const; - std::ostream& display(std::ostream& out, constraint const& c) const; - std::ostream& display(std::ostream& out, unsigned v, var_info const& vi) const; public: @@ -287,8 +234,6 @@ namespace sat { ~local_search(); - void add_soft(bool_var v, int weight); - void add_cardinality(unsigned sz, literal const* c, unsigned k); void add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k); @@ -307,8 +252,14 @@ namespace sat { void set_phase(bool_var v, lbool f); + void set_bias(bool_var v, lbool f); + bool get_phase(bool_var v) const { return is_true(v); } + inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; } + + double break_count(bool_var v) const { return m_vars[v].m_slow_break; } + model& get_model() { return m_model; } void collect_statistics(statistics& st) const; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4c5a8ac3d..f18db1d20 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1172,7 +1172,6 @@ namespace sat { SASSERT(!m_local_search); m_local_search = alloc(local_search); local_search& srch = *m_local_search; - srch.config().set_config(m_config); srch.import(*this, false); scoped_rl.push_child(&srch.rlimit()); lbool r = srch.check(num_lits, lits, nullptr); @@ -1197,9 +1196,8 @@ namespace sat { int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk; for (int i = 0; i < num_local_search; ++i) { local_search* l = alloc(local_search); - l->config().set_config(m_config); - l->config().set_random_seed(m_config.m_random_seed + i); l->import(*this, false); + l->config().set_random_seed(m_config.m_random_seed + i); ls.push_back(l); }