From 40df1949f52d2d9a196aeff0d4839b8d12d62735 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Mar 2017 10:18:12 -0800 Subject: [PATCH] tweaking local search Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 87 ++++++++++++++++++++++-------------- src/sat/sat_local_search.h | 8 +++- src/sat/sat_parallel.cpp | 17 ++++--- src/sat/sat_parallel.h | 1 + src/sat/sat_solver.cpp | 5 +-- 5 files changed, 74 insertions(+), 44 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 0cf509693..b8376a02e 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -64,10 +64,8 @@ namespace sat { } void local_search::init_cur_solution() { - //cur_solution.resize(num_vars() + 1, false); - for (unsigned v = 1; v < num_vars(); ++v) { + for (unsigned v = 0; v < num_vars(); ++v) { cur_solution[v] = (m_rand() % 2 == 1); - //std::cout << cur_solution[v] << '\n'; } } @@ -172,6 +170,14 @@ namespace sat { 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 { for (unsigned i = 0; i < m_constraints.size(); ++i) { @@ -179,14 +185,19 @@ namespace sat { } } - void local_search::verify_constraint(constraint const& c) const { + unsigned local_search::constraint_value(constraint const& c) const { unsigned value = 0; for (unsigned i = 0; i < c.size(); ++i) { value += is_true(c[i]) ? 1 : 0; } + return value; + } + + void local_search::verify_constraint(constraint const& c) const { + unsigned value = constraint_value(c); if (c.m_k < value) { - display(std::cout << "violated constraint: ", c); - std::cout << "value: " << value << "\n"; + IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c); + verbose_stream() << "value: " << value << "\n";); UNREACHABLE(); } } @@ -319,10 +330,6 @@ namespace sat { bool_var flipvar; timer timer; timer.start(); - // ################## start ###################### - IF_VERBOSE(1, verbose_stream() << "Unsat stack size: " << m_unsat_stack.size() << "\n";); - //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n"; - //std::cout << num_vars() << '\n'; unsigned tries, step = 0; for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) { reinit(); @@ -336,29 +343,37 @@ namespace sat { } flipvar = pick_var(); flip(flipvar); - m_vars[flipvar].m_time_stamp = step; - //if (!m_limit.inc()) break;pick_flip(); } - IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << "(sat-local :tries " << tries << " :steps " << (tries - 1) * max_steps + step - << " :unsat " << m_unsat_stack.size() << " :time " << timer.get_seconds() << ")\n";); - // the following is for tesing + IF_VERBOSE(1, if (tries % 10 == 0) + verbose_stream() << "(sat-local-search" + << " :tries " << tries + << " :steps " << (tries - 1) * max_steps + step + << " :unsat " << m_unsat_stack.size() + << " :time " << timer.get_seconds() << ")\n";); // tell the SAT solvers about the phase of variables. - //if (m_par && tries % 10 == 0) { - //m_par->set_phase(*this); + if (m_par && tries % 10 == 0) { + m_par->set_phase(*this); + } } // remove unit clauses from assumptions. m_constraints.shrink(num_constraints); - //print_solution(); - if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true + + TRACE("sat", display(tout);); + + lbool result; + if (m_unsat_stack.empty() && all_objectives_are_met()) { verify_solution(); extract_model(); - return l_true; + result = l_true; } - // TBD: adjust return status - return l_undef; + else { + result = l_undef; + } + IF_VERBOSE(1, verbose_stream() << "(sat-local-search " << result << ")\n";); + return result; } @@ -589,17 +604,18 @@ namespace sat { exit(-1); } - /*std::cout << "seed:\t" << m_config.seed() << '\n'; - std::cout << "cutoff time:\t" << m_config.cutoff_time() << '\n'; - std::cout << "strategy id:\t" << m_config.strategy_id() << '\n'; - std::cout << "best_known_value:\t" << m_config.best_known_value() << '\n'; - std::cout << "max_steps:\t" << max_steps << '\n'; - */ + TRACE("sat", + tout << "seed:\t" << m_config.seed() << '\n'; + tout << "cutoff time:\t" << m_config.cutoff_time() << '\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'; + ); } - void local_search::print_info() { - for (unsigned v = 1; v < num_vars(); ++v) { - std::cout << v << "\t" << m_vars[v].m_neighbors.size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n'; + void local_search::print_info(std::ostream& out) { + for (unsigned v = 0; v < num_vars(); ++v) { + out << "v" << v << "\t" << m_vars[v].m_neighbors.size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n'; } } @@ -614,11 +630,11 @@ namespace sat { for (unsigned i = 0; i < m_constraints.size(); ++i) { constraint const& c = m_constraints[i]; display(out, c); - } + } } void local_search::display(std::ostream& out, constraint const& c) const { - out << c.m_literals << " <= " << c.m_k << "\n"; + out << c.m_literals << " <= " << c.m_k << " lhs value: " << constraint_value(c) << "\n"; } void local_search::display(std::ostream& out, unsigned v, var_info const& vi) const { @@ -644,4 +660,9 @@ namespace sat { return false; } } + + void local_search::set_phase(bool_var v, bool f) { + std::cout << v << " " << f << "\n"; + } + } diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index c0d6f35d8..4f067404d 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -177,11 +177,15 @@ namespace sat { void calculate_and_update_ob(); + bool all_objectives_are_met() const; + void verify_solution() const; void verify_constraint(constraint const& c) const; - void print_info(); + unsigned constraint_value(constraint const& c) const; + + void print_info(std::ostream& out); void extract_model(); @@ -215,7 +219,7 @@ namespace sat { unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars - void set_phase(bool_var v, bool f) {} + void set_phase(bool_var v, bool f); bool get_phase(bool_var v) const { return is_true(v); } diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index c4bd66a8e..8a1127546 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -141,6 +141,7 @@ namespace sat { limit = m_units.size(); _get_phase(s); + _set_phase(s); } } @@ -207,9 +208,8 @@ namespace sat { return (c.size() <= 40 && c.glue() <= 8) || c.glue() <= 2; } - void parallel::set_phase(solver& s) { - #pragma omp critical (par_solver) - { + void parallel::_set_phase(solver& s) { + if (!m_phase.empty()) { m_phase.reserve(s.num_vars(), 0); for (unsigned i = 0; i < s.num_vars(); ++i) { if (s.value(i) != l_undef) { @@ -230,6 +230,13 @@ namespace sat { } } + void parallel::set_phase(solver& s) { + #pragma omp critical (par_solver) + { + _set_phase(s); + } + } + void parallel::get_phase(solver& s) { #pragma omp critical (par_solver) { @@ -254,8 +261,7 @@ namespace sat { void parallel::set_phase(local_search& s) { #pragma omp critical (par_solver) { - m_phase.reserve(s.num_vars(), 0); - for (unsigned i = 0; i < s.num_vars(); ++i) { + for (unsigned i = 0; i < m_phase.size(); ++i) { if (m_phase[i] < 0) { s.set_phase(i, false); } @@ -263,6 +269,7 @@ namespace sat { s.set_phase(i, true); } } + m_phase.reserve(s.num_vars(), 0); } } diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index ffbed5c0c..cb68dd0f9 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -53,6 +53,7 @@ namespace sat { bool enable_add(clause const& c) const; void _get_clauses(solver& s); void _get_phase(solver& s); + void _set_phase(solver& s); typedef hashtable index_set; literal_vector m_units; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3dbe87206..a135ceee3 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -868,7 +868,6 @@ namespace sat { m_local_search = alloc(local_search, *this); m_local_search->config().set_seed(m_config.m_random_seed); } - 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); @@ -891,7 +890,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); + r = m_local_search->check(num_lits, lits, &par); } else { r = check(num_lits, lits); @@ -903,7 +902,6 @@ namespace sat { finished_id = i; first = true; result = r; - std::cout << finished_id << " " << r << "\n"; } } if (first) { @@ -943,7 +941,6 @@ namespace sat { m_core.reset(); m_core.append(par.get_solver(finished_id).get_core()); } - std::cout << result << " id: " << finished_id << " is-local: " << (IS_LOCAL_SEARCH(finished_id)) << "\n"; if (result == l_true && finished_id != -1 && IS_LOCAL_SEARCH(finished_id)) { set_model(m_local_search->get_model()); }