From 352f8b6cb974bb3c6c2edb24ac8dd2883d3e682f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Apr 2017 13:04:57 -0700 Subject: [PATCH] fixing local search Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 30 ++++++++++++++++++------------ src/sat/sat_local_search.h | 8 ++++---- src/sat/sat_parallel.cpp | 12 +++++------- src/sat/sat_parallel.h | 2 ++ src/sat/sat_solver.cpp | 3 +++ 5 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 6b0205cc2..c5e7fcf54 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -70,9 +70,10 @@ namespace sat { void local_search::init_cur_solution() { for (unsigned v = 0; v < num_vars(); ++v) { - // use bias half the time. - if (m_rand() % 100 < 10) { - m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias); + // use bias with a small probability + if (m_rand() % 100 < 3) { + //m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias); + m_vars[v].m_value = (50 < m_vars[v].m_bias); } } } @@ -140,14 +141,17 @@ namespace sat { // 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 (best_unsat_rate >= last_best_unsat_rate) { +#if 0 + 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; } +#endif for (unsigned i = 0; i < m_constraints.size(); ++i) { constraint& c = m_constraints[i]; c.m_slack = c.m_k; @@ -178,6 +182,8 @@ namespace sat { init_slack(); init_scores(); init_goodvars(); + + m_best_unsat = m_unsat_stack.size(); } void local_search::calculate_and_update_ob() { @@ -382,13 +388,13 @@ namespace sat { IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ << " :flips " << flips \ << " :noise " << m_noise \ - << " :unsat " << /*m_unsat_stack.size()*/ best_unsat \ + << " :unsat " << /*m_unsat_stack.size()*/ m_best_unsat \ << " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \ } void local_search::walksat() { - best_unsat_rate = 1; - last_best_unsat_rate = 1; + m_best_unsat_rate = 1; + m_last_best_unsat_rate = 1; reinit(); @@ -398,10 +404,10 @@ namespace sat { PROGRESS(tries, total_flips); for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { - if (m_unsat_stack.size() < best_unsat) { - best_unsat = m_unsat_stack.size(); - last_best_unsat_rate = best_unsat_rate; - best_unsat_rate = (double)m_unsat_stack.size() / num_constraints(); + if (m_unsat_stack.size() < m_best_unsat) { + m_best_unsat = m_unsat_stack.size(); + m_last_best_unsat_rate = m_best_unsat_rate; + m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints(); } for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) { pick_flip_walksat(); @@ -506,7 +512,7 @@ namespace sat { SASSERT(c.m_k < constraint_value(c)); // TBD: dynamic noise strategy //if (m_rand() % 100 < 98) { - if (m_rand() % 10000 >= m_noise) { + if (m_rand() % 10000 <= m_noise) { // take this branch with 98% probability. // find the first one, to fast break the rest unsigned best_bsb = 0; diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 678eee60a..918f5328d 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -164,9 +164,9 @@ namespace sat { // information about solution - unsigned best_unsat; - double best_unsat_rate; - double last_best_unsat_rate; + 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 @@ -176,7 +176,7 @@ namespace sat { unsigned m_max_steps = (1 << 30); // dynamic noise - double m_noise = 400; // normalized by 10000 + double m_noise = 9800; // normalized by 10000 double m_noise_delta = 0.05; // for tuning diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 67d446a29..0b9a5bcb3 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -115,12 +115,16 @@ namespace sat { m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]); m_solvers[i]->copy(s); m_solvers[i]->set_par(this, i); - m_scoped_rlimit.push_child(&m_solvers[i]->rlimit()); + push_child(m_solvers[i]->rlimit()); } s.set_par(this, num_extra_solvers); s.m_params.set_sym("phase", saved_phase); } + void parallel::push_child(reslimit& rl) { + m_scoped_rlimit.push_child(&rl); + } + void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { if (s.m_par_syncing_clauses) return; @@ -268,12 +272,6 @@ namespace sat { { if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) { s.import(*m_solver_copy.get(), true); - m_num_clauses = s.num_non_binary_clauses(); - SASSERT(s.num_non_binary_clauses() == m_solver_copy->m_clauses.size()); - m_solver_copy = 0; - } - if (m_num_clauses < s.num_non_binary_clauses()) { - m_num_clauses = s.num_non_binary_clauses(); } for (unsigned i = 0; i < m_phase.size(); ++i) { s.set_phase(i, m_phase[i]); diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index b93384bd6..ffdfddf55 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -78,6 +78,8 @@ namespace sat { void init_solvers(solver& s, unsigned num_extra_solvers); + void push_child(reslimit& rl); + // reserve space void reserve(unsigned num_owners, unsigned sz) { m_pool.reserve(num_owners, sz); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 66ebb189f..d25c8bdee 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -875,6 +875,9 @@ namespace sat { sat::parallel par(*this); par.reserve(num_threads, 1 << 12); par.init_solvers(*this, num_extra_solvers); + for (unsigned i = 0; i < ls.size(); ++i) { + par.push_child(ls[i]->rlimit()); + } int finished_id = -1; std::string ex_msg; par_exception_kind ex_kind;