From c0188a7ec032c6105ae383c557d85b7d5dc9add9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 13:16:04 -0700 Subject: [PATCH] fix autarky detection Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 31 +++++++++++++-- src/sat/sat_local_search.h | 7 ++++ src/sat/sat_lookahead.h | 75 +++++++++++++++++++++++++----------- 3 files changed, 87 insertions(+), 26 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 92173ff4b..c9a947712 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -137,6 +137,17 @@ namespace sat { } void local_search::reinit() { + // 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) { + // worse + noise = noise - noise * 2 * noise_delta; + } + else { + // better + noise = noise + (10000 - noise) * noise_delta; + } for (unsigned i = 0; i < m_constraints.size(); ++i) { constraint& c = m_constraints[i]; c.m_slack = c.m_k; @@ -370,11 +381,16 @@ namespace sat { if (tries % 10 == 0 || m_unsat_stack.empty()) { \ IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ << " :flips " << flips \ - << " :unsat " << m_unsat_stack.size() \ + << " :noise " << noise \ + << " :unsat " << /*m_unsat_stack.size()*/ 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; + + reinit(); timer timer; timer.start(); @@ -382,12 +398,17 @@ 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(); + } for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) { pick_flip_walksat(); } total_flips += step; PROGRESS(tries, total_flips); - if (m_par && tries % 30 == 0) { + if (m_par && tries % 20 == 0) { m_par->get_phase(*this); reinit(); } @@ -483,7 +504,9 @@ namespace sat { unsigned num_unsat = m_unsat_stack.size(); constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; SASSERT(c.m_k < constraint_value(c)); - if (m_rand() % 100 < 98) { + // TBD: dynamic noise strategy + //if (m_rand() % 100 < 98) { + if (m_rand() % 10000 >= noise) { // take this branch with 98% probability. // find the first one, to fast break the rest unsigned best_bsb = 0; @@ -533,7 +556,7 @@ namespace sat { best_var = v; n = 1; } - else {// if (bb == best_bb) + else {// if (bsb == best_bb) ++n; if (m_rand() % n == 0) { best_var = v; diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 108df4e6d..7fb5396fe 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -164,6 +164,9 @@ namespace sat { // information about solution + unsigned best_unsat; + double best_unsat_rate; + double 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 @@ -172,6 +175,10 @@ namespace sat { unsigned m_max_steps = (1 << 30); + // dynamic noise + unsigned noise = 400; // normalized by 10000 + double noise_delta = 0.05; + // for tuning int s_id = 0; // strategy id diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index ac985c23c..fa9fea724 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -220,7 +220,7 @@ namespace sat { // ---------------------------------------- void add_binary(literal l1, literal l2) { - TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";); + TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";); SASSERT(l1 != l2); // don't add tautologies and don't add already added binaries if (~l1 == l2) return; @@ -375,7 +375,7 @@ namespace sat { progress = false; float mean = sum / (float)(m_candidates.size() + 0.0001); sum = 0; - for (unsigned i = 0; i < m_candidates.size(); ++i) { + for (unsigned i = 0; i < m_candidates.size() && m_candidates.size() >= max_num_cand * 2; ++i) { if (m_candidates[i].m_rating >= mean) { sum += m_candidates[i].m_rating; } @@ -1133,11 +1133,14 @@ namespace sat { m_search_mode = lookahead_mode::searching; // convert windfalls to binary clauses. if (!unsat) { + literal nlit = ~lit; for (unsigned i = 0; i < m_wstack.size(); ++i) { ++m_stats.m_windfall_binaries; + literal l2 = m_wstack[i]; //update_prefix(~lit); //update_prefix(m_wstack[i]); - add_binary(~lit, m_wstack[i]); + TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";); + add_binary(nlit, l2); } } m_wstack.reset(); @@ -1280,6 +1283,9 @@ namespace sat { else { TRACE("sat", tout << "propagating " << l << ": " << c << "\n";); SASSERT(is_undef(c[0])); + DEBUG_CODE(for (unsigned i = 2; i < c.size(); ++i) { + SASSERT(is_false(c[i])); + }); *it2 = *it; it2++; propagated(c[0]); @@ -1354,7 +1360,7 @@ namespace sat { TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";); reset_wnb(lit); push_lookahead1(lit, level); - do_double(lit, base); + //do_double(lit, base); bool unsat = inconsistent(); pop_lookahead1(lit); if (unsat) { @@ -1433,30 +1439,55 @@ namespace sat { set_wnb(l, p == null_literal ? 0 : get_wnb(p)); } - void update_wnb(literal l, unsigned level) { - if (m_weighted_new_binaries == 0) { - { - scoped_level _sl(*this, level); - clause_vector::const_iterator it = m_full_watches[l.index()].begin(), end = m_full_watches[l.index()].end(); - for (; it != end; ++it) { - clause& c = *(*it); - unsigned sz = c.size(); - bool found = false; - - for (unsigned i = 0; !found && i < sz; ++i) { - found = is_true(c[i]); - } - IF_VERBOSE(2, verbose_stream() << "skip autarky\n";); - if (!found) return; + bool check_autarky(literal l, unsigned level) { + // no propagations are allowed to reduce clauses. + clause_vector::const_iterator it = m_full_watches[l.index()].begin(); + clause_vector::const_iterator end = m_full_watches[l.index()].end(); + for (; it != end; ++it) { + clause& c = *(*it); + unsigned sz = c.size(); + bool found = false; + for (unsigned i = 0; !found && i < sz; ++i) { + found = is_true(c[i]); + if (found) { + TRACE("sat", tout << c[i] << " is true in " << c << "\n";); } } - if (get_wnb(l) == 0) { + IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";); + if (!found) return false; + } + // + // bail out if there is a pending binary propagation. + // In general, we would have to check, recursively that + // a binary propagation does not create reduced clauses. + // + literal_vector const& lits = m_binary[l.index()]; + TRACE("sat", tout << l << ": " << lits << "\n";); + for (unsigned i = 0; i < lits.size(); ++i) { + literal l2 = lits[i]; + if (is_true(l2)) continue; + SASSERT(!is_false(l2)); + return false; + } + + return true; + } + + void update_wnb(literal l, unsigned level) { + if (m_weighted_new_binaries == 0) { + if (!check_autarky(l, level)) { + // skip + } + else if (get_wnb(l) == 0) { ++m_stats.m_autarky_propagations; IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";); - TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] << "\n";); + + TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] + << " " + << (!m_binary[l.index()].empty() || !m_full_watches[l.index()].empty()) << "\n";); reset_wnb(); assign(l); - propagate(); + propagate(); init_wnb(); } else {