From d17248821ad047f889237ce20b6bdaa1465ceff9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Jun 2019 03:34:31 -0700 Subject: [PATCH] include chronological backtracking, two-phase sat, xor inprocessing, probsat, ddfw Signed-off-by: Nikolaj Bjorner --- src/sat/CMakeLists.txt | 2 + src/sat/ba_solver.cpp | 834 ++++++++++++++++++++++--- src/sat/ba_solver.h | 48 +- src/sat/sat_asymm_branch.cpp | 60 +- src/sat/sat_asymm_branch.h | 6 +- src/sat/sat_big.h | 1 + src/sat/sat_cleaner.cpp | 29 +- src/sat/sat_cleaner.h | 1 + src/sat/sat_config.cpp | 21 +- src/sat/sat_config.h | 19 +- src/sat/sat_ddfw.cpp | 594 ++++++++++++++++++ src/sat/sat_ddfw.h | 227 +++++++ src/sat/sat_extension.h | 1 + src/sat/sat_integrity_checker.cpp | 1 - src/sat/sat_justification.h | 16 +- src/sat/sat_local_search.cpp | 50 +- src/sat/sat_local_search.h | 73 ++- src/sat/sat_lookahead.cpp | 113 +++- src/sat/sat_lookahead.h | 19 +- src/sat/sat_parallel.cpp | 91 ++- src/sat/sat_parallel.h | 22 +- src/sat/sat_params.pyg | 21 +- src/sat/sat_prob.cpp | 296 +++++++++ src/sat/sat_prob.h | 160 +++++ src/sat/sat_simplifier.cpp | 30 +- src/sat/sat_solver.cpp | 972 +++++++++++++++++++++--------- src/sat/sat_solver.h | 123 +++- src/sat/sat_types.h | 25 +- src/sat/sat_unit_walk.cpp | 27 +- src/smt/smt_context.h | 2 +- src/tactic/tactic.cpp | 13 +- src/test/sat_local_search.cpp | 3 +- 32 files changed, 3246 insertions(+), 654 deletions(-) create mode 100644 src/sat/sat_ddfw.cpp create mode 100644 src/sat/sat_ddfw.h create mode 100644 src/sat/sat_prob.cpp create mode 100644 src/sat/sat_prob.h diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index 320a674a2..05de7e986 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -10,6 +10,7 @@ z3_add_component(sat sat_clause_use_list.cpp sat_cleaner.cpp sat_config.cpp + sat_ddfw.cpp sat_drat.cpp sat_elim_eqs.cpp sat_elim_vars.cpp @@ -20,6 +21,7 @@ z3_add_component(sat sat_model_converter.cpp sat_mus.cpp sat_parallel.cpp + sat_prob.cpp sat_probing.cpp sat_scc.cpp sat_simplifier.cpp diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index d97e3ee94..6dd5f3f09 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -84,9 +84,12 @@ namespace sat { } case ba_solver::pb_t: { ba_solver::pb const& p = cnstr.to_pb(); + bool first = true; for (ba_solver::wliteral wl : p) { + if (!first) out << "+ "; if (wl.first != 1) out << wl.first << " * "; out << wl.second << " "; + first = false; } out << " >= " << p.k(); break; @@ -332,7 +335,7 @@ namespace sat { SASSERT(validate_conflict(c)); if (c.is_xr() && value(lit) == l_true) lit.neg(); SASSERT(value(lit) == l_false); - set_conflict(justification::mk_ext_justification(c.index()), ~lit); + set_conflict(justification::mk_ext_justification(s().scope_lvl(), c.index()), ~lit); SASSERT(inconsistent()); } @@ -357,7 +360,7 @@ namespace sat { ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case. drat_add(lits, ps); } - assign(lit, justification::mk_ext_justification(c.index())); + assign(lit, justification::mk_ext_justification(s().scope_lvl(), c.index())); break; } } @@ -385,8 +388,9 @@ namespace sat { unsigned true_val = 0, slack = 0, num_false = 0; for (unsigned i = 0; i < p.size(); ++i) { literal l = p.get_lit(i); - if (s().was_eliminated(l.var())) { - SASSERT(p.learned()); + bool_var v = l.var(); + if (s().was_eliminated(v)) { + VERIFY(p.learned()); remove_constraint(p, "contains eliminated"); return; } @@ -410,18 +414,18 @@ namespace sat { else if (true_val >= p.k()) { if (p.lit() != null_literal) { IF_VERBOSE(100, display(verbose_stream() << "assign true literal ", p, true);); - s().assign(p.lit(), justification()); + s().assign_scoped(p.lit()); } remove_constraint(p, "is true"); } else if (slack + true_val < p.k()) { if (p.lit() != null_literal) { IF_VERBOSE(100, display(verbose_stream() << "assign false literal ", p, true);); - s().assign(~p.lit(), justification()); + s().assign_scoped(~p.lit()); } else { IF_VERBOSE(0, verbose_stream() << "unsat during simplification\n";); - s().set_conflict(justification()); + s().set_conflict(justification(0)); } remove_constraint(p, "is false"); } @@ -775,7 +779,6 @@ namespace sat { unwatch_literal(p[i].second, p); } p.set_num_watch(0); - DEBUG_CODE(for (wliteral wl : p) VERIFY(!is_watched(wl.second, p));); } @@ -826,7 +829,7 @@ namespace sat { if (k == 0) { if (p.lit() != null_literal) { - s().assign(p.lit(), justification()); + s().assign_scoped(p.lit()); } remove_constraint(p, "recompiled to true"); return; @@ -850,10 +853,10 @@ namespace sat { p.update_max_sum(); if (p.max_sum() < k) { if (p.lit() == null_literal) { - s().set_conflict(justification()); + s().set_conflict(justification(0)); } else { - s().assign(~p.lit(), justification()); + s().assign_scoped(~p.lit()); } remove_constraint(p, "recompiled to false"); return; @@ -886,6 +889,7 @@ namespace sat { for (wliteral wl : p) { literal l = wl.second; unsigned w = wl.first; + if (i > 0) out << "+ "; if (i++ == p.num_watch()) out << " | "; if (w > 1) out << w << " * "; out << l; @@ -928,9 +932,7 @@ namespace sat { bool ba_solver::init_watch(xr& x) { clear_watch(x); - if (x.lit() != null_literal && value(x.lit()) == l_false) { - x.negate(); - } + VERIFY(x.lit() == null_literal); TRACE("ba", display(tout, x, true);); unsigned sz = x.size(); unsigned j = 0; @@ -951,7 +953,6 @@ namespace sat { l = lvl(x[i]); } } - SASSERT(x.lit() == null_literal || value(x.lit()) == l_true); set_conflict(x, x[j]); } return false; @@ -975,30 +976,22 @@ namespace sat { unsigned sz = x.size(); TRACE("ba", tout << "assign: " << ~alit << "@" << lvl(~alit) << " " << x << "\n"; display(tout, x, true); ); - SASSERT(x.lit() == null_literal); + VERIFY(x.lit() == null_literal); SASSERT(value(alit) != l_undef); - unsigned index = 0; - for (; index < 2; ++index) { - if (x[index].var() == alit.var()) break; - } - if (index == 2) { - // literal is no longer watched. - // this can happen as both polarities of literals - // are put in watch lists and they are removed only - // one polarity at a time. - return l_undef; - } - SASSERT(x[index].var() == alit.var()); + unsigned index = (x[1].var() == alit.var()) ? 1 : 0; + VERIFY(x[index].var() == alit.var()); // find a literal to swap with: for (unsigned i = 2; i < sz; ++i) { - literal lit2 = x[i]; - if (value(lit2) == l_undef) { + literal lit = x[i]; + if (value(lit) == l_undef) { x.swap(index, i); - // unwatch_literal(alit, x); - watch_literal(lit2, x); - watch_literal(~lit2, x); - TRACE("ba", tout << "swap in: " << lit2 << " " << x << "\n";); + unwatch_literal(~alit, x); + // alit gets unwatched by propagate_core because we return l_undef + watch_literal(lit, x); + watch_literal(~lit, x); + // IF_VERBOSE(0, verbose_stream() << "swap " << lit << " " << alit << "\n"); + TRACE("ba", tout << "swap in: " << lit << " " << x << "\n";); return l_undef; } } @@ -1006,7 +999,7 @@ namespace sat { x.swap(0, 1); } // alit resides at index 1. - SASSERT(x[1].var() == alit.var()); + VERIFY(x[1].var() == alit.var()); if (value(x[0]) == l_undef) { bool p = parity(x, 1); assign(x, p ? ~x[0] : x[0]); @@ -1178,7 +1171,8 @@ namespace sat { literal consequent = s().m_not_l; justification js = s().m_conflict; TRACE("ba", tout << consequent << " " << js << "\n";); - m_conflict_lvl = s().get_max_lvl(consequent, js); + bool unique_max; + m_conflict_lvl = s().get_max_lvl(consequent, js, unique_max); if (m_conflict_lvl == 0) { return l_undef; } @@ -1315,7 +1309,11 @@ namespace sat { while (true) { consequent = lits[idx]; v = consequent.var(); - if (s().is_marked(v)) break; + if (s().is_marked(v)) { + if (s().lvl(v) == m_conflict_lvl) { + break; + } + } if (idx == 0) { IF_VERBOSE(2, verbose_stream() << "did not find marked literal\n";); goto bail_out; @@ -1513,7 +1511,8 @@ namespace sat { m_bound = 0; literal consequent = s().m_not_l; justification js = s().m_conflict; - m_conflict_lvl = s().get_max_lvl(consequent, js); + bool unique_max; + m_conflict_lvl = s().get_max_lvl(consequent, js, unique_max); if (m_conflict_lvl == 0) { return l_undef; } @@ -1736,7 +1735,7 @@ namespace sat { } if (m_lemma[0] == null_literal) { if (m_lemma.size() == 1) { - s().set_conflict(justification()); + s().set_conflict(justification(0)); } TRACE("ba", tout << "no asserting literal\n";); return false; @@ -1873,6 +1872,7 @@ namespace sat { m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); m_num_propagations_since_pop = 0; + m_max_xor_size = 5; } ba_solver::~ba_solver() { @@ -1960,6 +1960,9 @@ namespace sat { if (k == 0 && lit == null_literal) { return nullptr; } + if (!learned) { + for (wliteral wl : wlits) s().set_external(wl.second.var()); + } if (units || k == 1) { literal_vector lits; for (wliteral wl : wlits) lits.push_back(wl.second); @@ -1981,6 +1984,88 @@ namespace sat { add_xr(lits, false); } + bool ba_solver::all_distinct(literal_vector const& lits) { + init_visited(); + for (literal l : lits) { + if (is_visited(l.var())) { + return false; + } + mark_visited(l.var()); + } + return true; + } + + bool ba_solver::all_distinct(xr const& x) { + init_visited(); + for (literal l : x) { + if (is_visited(l.var())) { + return false; + } + mark_visited(l.var()); + } + return true; + } + + bool ba_solver::all_distinct(clause const& c) { + init_visited(); + for (literal l : c) { + if (is_visited(l.var())) { + return false; + } + mark_visited(l.var()); + } + return true; + } + + literal ba_solver::add_xor_def(literal_vector& lits, bool learned) { + unsigned sz = lits.size(); + SASSERT (sz > 1); + VERIFY(all_distinct(lits)); + init_visited(); + bool parity1 = true; + for (literal l : lits) { + mark_visited(l.var()); + parity1 ^= l.sign(); + } + for (auto const & w : get_wlist(lits[0])) { + if (w.get_kind() != watched::EXT_CONSTRAINT) continue; + constraint& c = index2constraint(w.get_ext_constraint_idx()); + if (!c.is_xr()) continue; + xr& x = c.to_xr(); + if (sz + 1 != x.size()) continue; + bool is_match = true; + literal l0 = null_literal; + bool parity2 = true; + for (literal l : x) { + if (!is_visited(l.var())) { + if (l0 == null_literal) { + l0 = l; + } + else { + is_match = false; + break; + } + } + else { + parity2 ^= l.sign(); + } + } + if (is_match) { + SASSERT(all_distinct(x)); + if (parity1 == parity2) l0.neg(); + if (!learned && x.learned()) { + set_non_learned(x); + } + return l0; + } + } + bool_var v = s().mk_var(true, true); + literal lit(v, false); + lits.push_back(~lit); + add_xr(lits, learned); + return lit; + } + ba_solver::constraint* ba_solver::add_xr(literal_vector const& lits, bool learned) { void * mem = m_allocator.allocate(xr::get_obj_size(lits.size())); xr* x = new (mem) xr(next_id(), lits); @@ -1993,6 +2078,7 @@ namespace sat { \brief return true to keep watching literal. */ bool ba_solver::propagate(literal l, ext_constraint_idx idx) { + TRACE("ba", tout << l << "\n";); SASSERT(value(l) == l_true); constraint& c = index2constraint(idx); if (c.lit() != null_literal && l.var() == c.lit().var()) { @@ -2084,20 +2170,21 @@ namespace sat { The idea is to collect premises based on xr resolvents. Variables that are repeated an even number of times cancel out. */ + void ba_solver::get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r) { unsigned level = lvl(l); bool_var v = l.var(); SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION); + // IF_VERBOSE(0, verbose_stream() << l << " : " << js << " " << xr_count << "\n"); TRACE("ba", tout << l << ": " << js << "\n"; for (unsigned i = 0; i <= index; ++i) tout << s().m_trail[i] << " "; tout << "\n"; s().display_units(tout); ); + unsigned num_marks = 0; - unsigned count = 0; while (true) { - TRACE("ba", tout << "process: " << l << "\n";); - ++count; + TRACE("ba", tout << "process: " << l << " " << js << "\n";); if (js.get_kind() == justification::EXT_JUSTIFICATION) { constraint& c = index2constraint(js.get_ext_justification_idx()); TRACE("ba", tout << c << "\n";); @@ -2109,7 +2196,7 @@ namespace sat { if (x[1].var() == l.var()) { x.swap(0, 1); } - SASSERT(x[0].var() == l.var()); + VERIFY(x[0].var() == l.var()); for (unsigned i = 1; i < x.size(); ++i) { literal lit(value(x[i]) == l_true ? x[i] : ~x[i]); inc_parity(lit.var()); @@ -2131,7 +2218,7 @@ namespace sat { l = s().m_trail[index]; v = l.var(); unsigned n = get_parity(v); - if (n > 0) { + if (n > 0 && lvl(l) == level) { reset_parity(v); num_marks -= n; if (n % 2 == 1) { @@ -2150,8 +2237,7 @@ namespace sat { // now walk the defined literals - for (unsigned i = 0; i < m_parity_trail.size(); ++i) { - literal lit = m_parity_trail[i]; + for (literal lit : m_parity_trail) { if (get_parity(lit.var()) % 2 == 1) { r.push_back(lit); } @@ -2303,7 +2389,10 @@ namespace sat { } void ba_solver::simplify(xr& x) { - // no-op + if (x.learned()) { + x.set_removed(); + m_constraint_removed = true; + } } void ba_solver::get_antecedents(literal l, card const& c, literal_vector& r) { @@ -2362,12 +2451,16 @@ namespace sat { } void ba_solver::unwatch_literal(literal lit, constraint& c) { - get_wlist(~lit).erase(watched(c.index())); + watched w(c.index()); + get_wlist(~lit).erase(w); + SASSERT(!is_watched(lit, c)); } void ba_solver::watch_literal(literal lit, constraint& c) { if (c.is_pure() && lit == ~c.lit()) return; - get_wlist(~lit).push_back(watched(c.index())); + SASSERT(!is_watched(lit, c)); + watched w(c.index()); + get_wlist(~lit).push_back(w); } void ba_solver::get_antecedents(literal l, constraint const& c, literal_vector& r) { @@ -2404,6 +2497,7 @@ namespace sat { } void ba_solver::remove_constraint(constraint& c, char const* reason) { + TRACE("ba", tout << "remove " << c << " " << reason << "\n";); IF_VERBOSE(21, display(verbose_stream() << "remove " << reason << " ", c, true);); nullify_tracking_literal(c); clear_watch(c); @@ -2652,12 +2746,12 @@ namespace sat { switch (c.tag()) { case card_t: for (literal l : c.to_card()) { - if (s().m_phase[l.var()] == (l.sign() ? NEG_PHASE : POS_PHASE)) ++r; + if (s().m_phase[l.var()] == !l.sign()) ++r; } break; case pb_t: for (wliteral l : c.to_pb()) { - if (s().m_phase[l.second.var()] == (l.second.sign() ? NEG_PHASE : POS_PHASE)) ++r; + if (s().m_phase[l.second.var()] == !l.second.sign()) ++r; } break; default: @@ -2835,6 +2929,48 @@ namespace sat { } } + void ba_solver::pre_simplify() { + VERIFY(s().at_base_lvl()); + barbet_init_parity(); + m_constraint_removed = false; + for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(*m_constraints[i]); + for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) pre_simplify(*m_learned[i]); + bool change = m_constraint_removed; + cleanup_constraints(); + if (change) { + // remove non-used variables. + init_use_lists(); + remove_unused_defs(); + set_non_external(); + } + } + + void ba_solver::pre_simplify(constraint& c) { + if (c.is_xr() && c.size() <= m_max_xor_size) { + unsigned sz = c.size(); + literal_vector& lits = m_barbet_clause; + bool parity = false; + xr const& x = c.to_xr(); + for (literal lit : x) { + parity ^= lit.sign(); + } + + // IF_VERBOSE(0, verbose_stream() << "blast: " << c << "\n"); + for (unsigned i = 0; i < (1ul << sz); ++i) { + if (m_barbet_parity[sz][i] == parity) { + lits.reset(); + for (unsigned j = 0; j < sz; ++j) { + lits.push_back(literal(x[j].var(), (0 != (i & (1 << j))))); + } + // IF_VERBOSE(0, verbose_stream() << lits << "\n"); + s().mk_clause(lits); + } + } + c.set_removed(); + m_constraint_removed = true; + } + } + void ba_solver::simplify() { if (!s().at_base_lvl()) s().pop_to_base_level(); unsigned trail_sz, count = 0; @@ -2850,24 +2986,26 @@ namespace sat { set_non_external(); if (get_config().m_elim_vars) elim_pure(); for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); + for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); unit_strengthen(); + extract_xor(); + merge_xor(); cleanup_clauses(); cleanup_constraints(); update_pure(); - ++count; + count++; } while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size())); - IF_VERBOSE(1, verbose_stream() << "(ba.simplify" - << " :vars " << s().num_vars() - trail_sz - << " :constraints " << m_constraints.size() - << " :lemmas " << m_learned.size() - << " :subsumes " << m_stats.m_num_bin_subsumes - + m_stats.m_num_clause_subsumes - + m_stats.m_num_pb_subsumes - << " :gc " << m_stats.m_num_gc - << ")\n";); + // validate_eliminated(); + + IF_VERBOSE(1, + unsigned subs = m_stats.m_num_bin_subsumes + m_stats.m_num_clause_subsumes + m_stats.m_num_pb_subsumes; + verbose_stream() << "(ba.simplify" << " :constraints " << m_constraints.size(); + if (!m_learned.empty()) verbose_stream() << " :lemmas " << m_learned.size(); + if (subs > 0) verbose_stream() << " :subsumes " << subs; + if (m_stats.m_num_gc > 0) verbose_stream() << " :gc " << m_stats.m_num_gc; + verbose_stream() << ")\n";); // IF_VERBOSE(0, s().display(verbose_stream())); // mutex_reduction(); @@ -2886,13 +3024,13 @@ namespace sat { * -> negate: ~lit == ~C */ void ba_solver::update_pure() { - // return; + //return; for (constraint* cp : m_constraints) { literal lit = cp->lit(); if (lit != null_literal && !cp->is_pure() && value(lit) == l_undef && - get_wlist(~lit).size() == 1 && + get_wlist(~lit).size() == 1 && m_clause_use_list.get(lit).empty()) { clear_watch(*cp); cp->negate(); @@ -3041,6 +3179,36 @@ namespace sat { flush_roots(*m_learned[i]); cleanup_constraints(); // validate(); + + // validate_eliminated(); + } + + void ba_solver::validate_eliminated() { + validate_eliminated(m_constraints); + validate_eliminated(m_learned); + } + + void ba_solver::validate_eliminated(ptr_vector const& cs) { + for (constraint const* c : cs) { + if (c->learned()) continue; + switch (c->tag()) { + case tag_t::card_t: + for (literal l : c->to_card()) { + VERIFY(!s().was_eliminated(l.var())); + } + break; + case tag_t::pb_t: + for (wliteral wl : c->to_pb()) { + VERIFY(!s().was_eliminated(wl.second.var())); + } + break; + case tag_t::xr_t: + for (literal l : c->to_xr()) { + VERIFY(!s().was_eliminated(l.var())); + } + break; + } + } } void ba_solver::recompile(constraint& c) { @@ -3211,7 +3379,7 @@ namespace sat { // handling of conditional cardinality as well. // if (!c.learned() && clausify(c.lit(), c.size(), c.begin(), c.k())) { - IF_VERBOSE(0, verbose_stream() << "clausify " << c << "\n";); + IF_VERBOSE(1, verbose_stream() << "clausify " << c << "\n";); // compiled } remove_constraint(c, "recompiled to clauses"); @@ -3410,21 +3578,27 @@ namespace sat { } } } - - unsigned ba_solver::set_non_external() { + + bool ba_solver::incremental_mode() const { sat_simplifier_params p(s().m_params); - // set variables to be non-external if they are not used in theory constraints. - unsigned ext = 0; bool incremental_mode = s().get_config().m_incremental && !p.override_incremental(); incremental_mode |= s().tracking_assumptions(); - for (unsigned v = 0; !incremental_mode && v < s().num_vars(); ++v) { - literal lit(v, false); - if (s().is_external(v) && - m_cnstr_use_list[lit.index()].empty() && - m_cnstr_use_list[(~lit).index()].empty()) { - s().set_non_external(v); - ++ext; - } + return incremental_mode; + } + + unsigned ba_solver::set_non_external() { + // set variables to be non-external if they are not used in theory constraints. + unsigned ext = 0; + if (!incremental_mode()) { + for (unsigned v = 0; v < s().num_vars(); ++v) { + literal lit(v, false); + if (s().is_external(v) && + m_cnstr_use_list[lit.index()].empty() && + m_cnstr_use_list[(~lit).index()].empty()) { + s().set_non_external(v); + ++ext; + } + } } // ensure that lemmas use only non-eliminated variables for (constraint* cp : m_learned) { @@ -3446,7 +3620,7 @@ namespace sat { if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) { IF_VERBOSE(100, verbose_stream() << "pure literal: " << lit << "\n";); - s().assign(lit, justification()); + s().assign_scoped(lit); return true; } return false; @@ -3578,13 +3752,448 @@ namespace sat { } } + // merge xors that contain cut variable + void ba_solver::merge_xor() { + unsigned sz = s().num_vars(); + for (unsigned i = 0; i < sz; ++i) { + literal lit(i, false); + unsigned index = lit.index(); + if (m_cnstr_use_list[index].size() == 2) { + constraint& c1 = *m_cnstr_use_list[index][0]; + constraint& c2 = *m_cnstr_use_list[index][1]; + if (c1.is_xr() && c2.is_xr() && + m_clause_use_list.get(lit).empty() && + m_clause_use_list.get(~lit).empty()) { + bool unique = true; + for (watched w : get_wlist(lit)) { + if (w.is_binary_clause()) unique = false; + } + for (watched w : get_wlist(~lit)) { + if (w.is_binary_clause()) unique = false; + } +#if 1 + if (!unique) continue; + xr const& x1 = c1.to_xr(); + xr const& x2 = c2.to_xr(); + literal_vector lits, dups; + bool parity = false; + init_visited(); + for (literal l : x1) { + mark_visited(l.var()); + lits.push_back(l); + } + for (literal l : x2) { + if (is_visited(l.var())) { + dups.push_back(l); + } + else { + lits.push_back(l); + } + } + init_visited(); + for (literal l : dups) mark_visited(l); + unsigned j = 0; + for (unsigned i = 0; i < lits.size(); ++i) { + literal l = lits[i]; + if (is_visited(l)) { + // skip + } + else if (is_visited(~l)) { + parity ^= true; + } + else { + lits[j++] = l; + } + } + lits.shrink(j); + if (!parity) lits[0].neg(); + IF_VERBOSE(0, verbose_stream() << "binary " << lits << " : " << c1 << " " << c2 << "\n"); + c1.set_removed(); + c2.set_removed(); + add_xr(lits, !c1.learned() && !c2.learned()); + m_constraint_removed = true; +#endif + } + } + } + } + + void ba_solver::extract_xor() { + if (!s().get_config().m_xor_solver) { + return; + } + barbet_extract_xor(); + return; + + for (clause* cp : s().m_clauses) { + clause& c = *cp; + if (c.was_removed() || c.size() <= 3 || !all_distinct(c)) continue; + init_visited(); + for (literal l : c) mark_visited(l); + literal l0 = c[0]; + literal l1 = c[1]; + if (extract_xor(c, l0) || + extract_xor(c, l1) || + extract_xor(c, ~l0)) { + m_simplify_change = true; + } + } + // extract xor from ternary clauses + unsigned sz = s().num_vars(); + m_ternary.reset(); + m_ternary.reserve(sz); + extract_ternary(s().m_clauses); + extract_ternary(s().m_learned); + for (unsigned v = 0; v < sz; ++v) { + ptr_vector& cs = m_ternary[v]; + for (unsigned i = 0; i < cs.size() && !cs[i]->is_learned(); ++i) { + clause& c = *cs[i]; + if (c.was_removed()) continue; + init_visited(); + for (literal l : c) mark_visited(l); + for (unsigned j = i + 1; j < cs.size(); ++j) { + if (extract_xor(c, *cs[j])) { + m_simplify_change = true; + break; + } + } + } + } + m_ternary.clear(); + } + + void ba_solver::extract_ternary(clause_vector const& clauses) { + for (clause* cp : clauses) { + clause& c = *cp; + if (!c.was_removed() && c.size() == 3 && all_distinct(c)) { + bool_var v = std::min(c[0].var(), std::min(c[1].var(), c[2].var())); + m_ternary[v].push_back(cp); + } + } + } + + void ba_solver::barbet_extract_xor() { + unsigned max_size = m_max_xor_size; + // we better have enough bits in the combination mask to + // handle clauses up to max_size. + // max_size = 5 -> 32 bits + // max_size = 6 -> 64 bits + SASSERT(sizeof(m_barbet_combination)*8 <= (1ull << static_cast(max_size))); + init_clause_filter(); + barbet_init_parity(); + m_barbet_var_position.resize(s().num_vars()); + for (clause* cp : s().m_clauses) { + cp->unmark_used(); + } + for (; max_size > 2; --max_size) { + for (clause* cp : s().m_clauses) { + clause& c = *cp; + if (c.size() == max_size && !c.was_removed() && !c.is_learned() && !c.was_used()) { + barbet_extract_xor(c); + } + } + } + m_clause_filters.clear(); + } + + void ba_solver::barbet_extract_xor(clause& c) { + SASSERT(c.size() > 2); + unsigned filter = get_clause_filter(c); + init_visited(); + bool parity = false; + unsigned mask = 0, i = 0; + for (literal l : c) { + m_barbet_var_position[l.var()] = i; + mark_visited(l.var()); + parity ^= l.sign(); + mask |= (l.sign() << (i++)); + } + m_barbet_clauses_to_remove.reset(); + m_barbet_clauses_to_remove.push_back(&c); + m_barbet_clause.resize(c.size()); + m_barbet_combination = 0; + // IF_VERBOSE(0, verbose_stream() << "barbet: " << c << " parity: " << parity << " mask: " << mask << "\n"); + barbet_set_combination(mask); + c.mark_used(); + for (literal l : c) { + for (auto const& cf : m_clause_filters[l.var()]) { + if ((filter == (filter | cf.m_filter)) && + !cf.m_clause->was_used() && + barbet_extract_xor(parity, c, *cf.m_clause)) { + barbet_add_xor(parity, c); + return; + } + } + // loop over binary clauses in watch list + for (watched const & w : get_wlist(l)) { + if (w.is_binary_clause() && is_visited(w.get_literal().var()) && w.get_literal().index() < l.index()) { + if (barbet_extract_xor(parity, c, ~l, w.get_literal())) { + barbet_add_xor(parity, c); + return; + } + } + } + l.neg(); + for (watched const & w : get_wlist(l)) { + if (w.is_binary_clause() && is_visited(w.get_literal().var()) && w.get_literal().index() < l.index()) { + if (barbet_extract_xor(parity, c, ~l, w.get_literal())) { + barbet_add_xor(parity, c); + return; + } + } + } + } + } + + void ba_solver::barbet_add_xor(bool parity, clause& c) { + for (clause* cp : m_barbet_clauses_to_remove) { + //IF_VERBOSE(0, verbose_stream() << "remove " << *cp << "\n"); + cp->set_removed(true); + } + m_clause_removed = true; + bool learned = false; + literal_vector lits; + for (literal l : c) { + lits.push_back(literal(l.var(), false)); + s().set_external(l.var()); + } + if (parity) lits[0].neg(); + // IF_VERBOSE(0, verbose_stream() << "mk: " << lits << "\n"); + add_xr(lits, learned); + } + + bool ba_solver::barbet_extract_xor(bool parity, clause& c, literal l1, literal l2) { + //IF_VERBOSE(0, verbose_stream() << "adding " << l1 << " " << l2 << "\n"); + SASSERT(is_visited(l1.var())); + SASSERT(is_visited(l2.var())); + m_barbet_missing.reset(); + unsigned mask = 0; + for (unsigned i = 0; i < c.size(); ++i) { + if (c[i].var() == l1.var()) { + mask |= (l1.sign() << i); + } + else if (c[i].var() == l2.var()) { + mask |= (l2.sign() << i); + } + else { + m_barbet_missing.push_back(i); + } + } + return barbet_update_combinations(c, parity, mask); + } + + bool ba_solver::barbet_extract_xor(bool parity, clause& c, clause& c2) { + bool parity2 = false; + for (literal l : c2) { + if (!is_visited(l.var())) return false; + parity2 ^= l.sign(); + } + if (c2.size() == c.size() && parity2 != parity) { + return false; + } + if (c2.size() == c.size()) { + m_barbet_clauses_to_remove.push_back(&c2); + c2.mark_used(); + } + // insert missing + unsigned mask = 0; + m_barbet_missing.reset(); + SASSERT(c2.size() <= c.size()); + for (unsigned i = 0; i < c.size(); ++i) { + m_barbet_clause[i] = null_literal; + } + for (literal l : c2) { + unsigned pos = m_barbet_var_position[l.var()]; + m_barbet_clause[pos] = l; + } + for (unsigned j = 0; j < c.size(); ++j) { + literal lit = m_barbet_clause[j]; + if (lit == null_literal) { + m_barbet_missing.push_back(j); + } + else { + mask |= (m_barbet_clause[j].sign() << j); + } + } + + return barbet_update_combinations(c, parity, mask); + } + + bool ba_solver::barbet_update_combinations(clause& c, bool parity, unsigned mask) { + unsigned num_missing = m_barbet_missing.size(); + for (unsigned k = 0; k < (1ul << num_missing); ++k) { + unsigned mask2 = mask; + for (unsigned i = 0; i < num_missing; ++i) { + if ((k & (1 << i)) != 0) { + mask2 |= 1ul << m_barbet_missing[i]; + } + } + barbet_set_combination(mask2); + } + // return true if xor clause is covered. + unsigned sz = c.size(); + for (unsigned i = 0; i < (1ul << sz); ++i) { + if (parity == m_barbet_parity[sz][i] && !barbet_get_combination(i)) { + return false; + } + } + return true; + } + + void ba_solver::barbet_init_parity() { + for (unsigned i = m_barbet_parity.size(); i <= m_max_xor_size; ++i) { + bool_vector bv; + for (unsigned j = 0; j < (1ul << i); ++j) { + bool parity = false; + for (unsigned k = 0; k < i; ++k) { + parity ^= ((j & (1 << k)) != 0); + } + bv.push_back(parity); + } + m_barbet_parity.push_back(bv); + } + } + + void ba_solver::init_clause_filter() { + m_clause_filters.reset(); + m_clause_filters.resize(s().num_vars()); + init_clause_filter(s().m_clauses); + init_clause_filter(s().m_learned); + } + + void ba_solver::init_clause_filter(clause_vector& clauses) { + for (clause* cp : clauses) { + clause& c = *cp; + if (c.size() <= m_max_xor_size && all_distinct(c)) { + clause_filter cf(get_clause_filter(c), cp); + for (literal l : c) { + m_clause_filters[l.var()].push_back(cf); + } + } + } + } + + unsigned ba_solver::get_clause_filter(clause& c) { + unsigned filter = 0; + for (literal l : c) { + filter |= 1 << ((l.var() % 32)); + } + return filter; + } + + + /** + * \brief replace (lit0, lit1, lit2), (lit0, ~lit1, ~lit2) + * by (lit0, lit), ~lit x lit1 x lit2 + */ + bool ba_solver::extract_xor(clause& c1, clause& c2) { + SASSERT(c1.size() == 3); + SASSERT(c2.size() == 3); + SASSERT(&c1 != &c2); + literal lit0, lit1, lit2; + if (is_visited(c2[0]) && is_visited(~c2[1]) && is_visited(~c2[2])) { + lit0 = c2[0]; + lit1 = c2[1]; + lit2 = c2[2]; + } + else if (is_visited(c2[1]) && is_visited(~c2[0]) && is_visited(~c2[2])) { + lit0 = c2[1]; + lit1 = c2[0]; + lit2 = c2[2]; + } + else if (is_visited(c2[2]) && is_visited(~c2[0]) && is_visited(~c2[1])) { + lit0 = c2[2]; + lit1 = c2[0]; + lit2 = c2[1]; + } + else { + return false; + } + c1.set_removed(true); + c2.set_removed(true); + m_clause_removed = true; + literal_vector lits; + lits.push_back(lit1); + lits.push_back(lit2); + literal lit = add_xor_def(lits); + lits.reset(); + lits.push_back(lit); + lits.push_back(lit0); + s().mk_clause(lits); + TRACE("ba", tout << c1 << " " << c2 << "\n";); + return true; + } + + bool ba_solver::extract_xor(clause& c, literal l0) { + watch_list & wlist = get_wlist(~l0); + unsigned sz = c.size(); + SASSERT(sz > 3); + for (watched const& w : wlist) { + if (!w.is_clause()) continue; + clause& c2 = s().get_clause(w); + if (c2.size() != sz || c2.was_removed()) continue; + bool is_xor = true; + literal lit1 = null_literal; + literal lit2 = null_literal; + for (literal l : c2) { + if (is_visited(l)) { + // no-op + } + else if (is_visited(~l) && lit1 == null_literal) { + lit1 = l; + } + else if (is_visited(~l) && lit2 == null_literal) { + lit2 = l; + } + else { + is_xor = false; + break; + } + } + if (is_xor && lit2 != null_literal && lit1 != lit2) { + // ensure all literals in c2 are distinct + // this destroys visited, so re-initialize it. + bool distinct = all_distinct(c2); + init_visited(); + for (literal l : c) mark_visited(l); + if (!distinct) { + continue; + } + literal_vector lits; + lits.push_back(lit1); + lits.push_back(lit2); + literal lit = add_xor_def(lits); + lits.reset(); + lits.push_back(lit); + for (literal l : c2) { + if (l != lit1 && l != lit2) { + lits.push_back(l); + } + } + s().mk_clause(lits); + c.set_removed(true); + c2.set_removed(true); + m_clause_removed = true; + TRACE("ba", tout << "xor " << lit1 << " " << lit2 << " : " << c << " " << c2 << "\nnew clause: " << lits << "\n";); + return true; + } + } + return false; + } + void ba_solver::cleanup_clauses() { - if (!m_clause_removed) return; + if (m_clause_removed) { + cleanup_clauses(s().m_clauses); + cleanup_clauses(s().m_learned); + } + } + + void ba_solver::cleanup_clauses(clause_vector& clauses) { // version in simplify first clears // all watch literals, then reinserts them. // this ensures linear time cleanup. - clause_vector::iterator it = s().m_clauses.begin(); - clause_vector::iterator end = s().m_clauses.end(); + clause_vector::iterator it = clauses.begin(); + clause_vector::iterator end = clauses.end(); clause_vector::iterator it2 = it; for (; it != end; ++it) { clause* c = *it; @@ -3599,14 +4208,15 @@ namespace sat { ++it2; } } - s().m_clauses.set_end(it2); + clauses.set_end(it2); } void ba_solver::cleanup_constraints() { - if (!m_constraint_removed) return; - cleanup_constraints(m_constraints, false); - cleanup_constraints(m_learned, true); - m_constraint_removed = false; + if (m_constraint_removed) { + cleanup_constraints(m_constraints, false); + cleanup_constraints(m_learned, true); + m_constraint_removed = false; + } } void ba_solver::cleanup_constraints(ptr_vector& cs, bool learned) { @@ -3723,8 +4333,8 @@ namespace sat { break; } if (s) { - ++m_stats.m_num_pb_subsumes; - p1.set_learned(false); + ++m_stats.m_num_pb_subsumes; + set_non_learned(p1); remove_constraint(*c, "subsumed"); } } @@ -3757,7 +4367,7 @@ namespace sat { TRACE("ba", tout << "subsume cardinality\n" << c1.index() << ":" << c1 << "\n" << c2.index() << ":" << c2 << "\n";); remove_constraint(c2, "subsumed"); ++m_stats.m_num_pb_subsumes; - c1.set_learned(false); + set_non_learned(c1); } else { TRACE("ba", tout << "self subsume cardinality\n";); @@ -3795,13 +4405,41 @@ namespace sat { TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";); removed_clauses.push_back(&c2); ++m_stats.m_num_clause_subsumes; - c1.set_learned(false); + set_non_learned(c1); } } it.next(); } } + void ba_solver::set_non_learned(constraint& c) { + literal lit = c.lit(); + if (lit != null_literal) { + s().set_external(lit.var()); + } + switch (c.tag()) { + case card_t: + for (literal lit : c.to_card()) { + s().set_external(lit.var()); + SASSERT(!s().was_eliminated(lit.var())); + } + break; + case pb_t: + for (wliteral wl : c.to_pb()) { + s().set_external(wl.second.var()); + SASSERT(!s().was_eliminated(wl.second.var())); + } + break; + default: + for (literal lit : c.to_xr()) { + s().set_external(lit.var()); + SASSERT(!s().was_eliminated(lit.var())); + } + break; + } + c.set_learned(false); + } + void ba_solver::binary_subsumption(card& c1, literal lit) { if (c1.k() + 1 != c1.size()) return; SASSERT(is_visited(lit)); @@ -3814,9 +4452,9 @@ namespace sat { watched w = *it; if (w.is_binary_clause() && is_visited(w.get_literal())) { ++m_stats.m_num_bin_subsumes; - IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";); + IF_VERBOSE(20, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";); if (!w.is_learned()) { - c1.set_learned(false); + set_non_learned(c1); } } else { @@ -3879,7 +4517,7 @@ namespace sat { if (lit == null_literal) { for (literal l : lits) { if (value(l) == l_undef) { - s().assign(l, justification()); + s().assign_scoped(l); } } } @@ -4581,9 +5219,9 @@ namespace sat { ineq notC = negate(m_B); literal l3 = translate_to_sat(s0, translation, notC); if (l3 == null_literal) return true; - s0.assign(l1, justification()); - s0.assign(l2, justification()); - s0.assign(l3, justification()); + s0.assign_scoped(l1); + s0.assign_scoped(l2); + s0.assign_scoped(l3); lbool is_sat = s0.check(); TRACE("ba", s0.display(tout << "trying sat encoding");); if (is_sat == l_false) return true; @@ -4720,6 +5358,9 @@ namespace sat { bool ba_solver::check_model(model const& m) const { bool ok = true; for (constraint const* c : m_constraints) { + if (c->was_removed()) { + continue; + } if (c->is_pure() && c->lit() != null_literal && m[c->lit().var()] == (c->lit().sign() ? l_true : l_false)) { continue; } @@ -4741,3 +5382,4 @@ namespace sat { }; + diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index dbbc48993..56cebe557 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -26,6 +26,7 @@ Revision History: #include "sat/sat_lookahead.h" #include "sat/sat_unit_walk.h" #include "sat/sat_big.h" +#include "util/small_object_allocator.h" #include "util/scoped_ptr_vector.h" #include "util/sorting_network.h" @@ -331,6 +332,7 @@ namespace sat { unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); } void cleanup_clauses(); + void cleanup_clauses(clause_vector& clauses); void cleanup_constraints(); void cleanup_constraints(ptr_vector& cs, bool learned); void remove_constraint(constraint& c, char const* reason); @@ -347,7 +349,9 @@ namespace sat { void init_watch(bool_var v); void clear_watch(constraint& c); lbool add_assign(constraint& c, literal l); + bool incremental_mode() const; void simplify(constraint& c); + void pre_simplify(constraint& c); void nullify_tracking_literal(constraint& c); void set_conflict(constraint& c, literal lit); void assign(constraint& c, literal lit); @@ -355,6 +359,8 @@ namespace sat { void get_antecedents(literal l, constraint const& c, literal_vector & r); bool validate_conflict(constraint const& c) const; bool validate_unit_propagation(constraint const& c, literal alit) const; + void validate_eliminated(); + void validate_eliminated(ptr_vector const& cs); void attach_constraint(constraint const& c); void detach_constraint(constraint const& c); lbool eval(constraint const& c) const; @@ -365,6 +371,7 @@ namespace sat { void recompile(constraint& c); void split_root(constraint& c); unsigned next_id() { return m_constraint_id++; } + void set_non_learned(constraint& c); // cardinality @@ -391,6 +398,40 @@ namespace sat { void get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r); void get_antecedents(literal l, xr const& x, literal_vector & r); void simplify(xr& x); + void extract_xor(); + void merge_xor(); + struct clause_filter { + unsigned m_filter; + clause* m_clause; + clause_filter(unsigned f, clause* cp): + m_filter(f), m_clause(cp) {} + }; + typedef svector bool_vector; + unsigned m_max_xor_size; + vector> m_clause_filters; // index of clauses. + unsigned m_barbet_combination; // bit-mask of parities that have been found + vector m_barbet_parity; // lookup parity for clauses + clause_vector m_barbet_clauses_to_remove; // remove clauses that become xors + unsigned_vector m_barbet_var_position; // position of var in main clause + literal_vector m_barbet_clause; // reference clause with literals sorted according to main clause + unsigned_vector m_barbet_missing; // set of indices not occurring in clause. + void init_clause_filter(); + void init_clause_filter(clause_vector& clauses); + inline void barbet_set_combination(unsigned mask) { m_barbet_combination |= (1 << mask); } + inline bool barbet_get_combination(unsigned mask) const { return (m_barbet_combination & (1 << mask)) != 0; } + void barbet_extract_xor(); + void barbet_init_parity(); + void barbet_extract_xor(clause& c); + bool barbet_extract_xor(bool parity, clause& c, clause& c2); + bool barbet_extract_xor(bool parity, clause& c, literal l1, literal l2); + bool barbet_update_combinations(clause& c, bool parity, unsigned mask); + void barbet_add_xor(bool parity, clause& c); + unsigned get_clause_filter(clause& c); + + vector> m_ternary; + void extract_ternary(clause_vector const& clauses); + bool extract_xor(clause& c, literal l); + bool extract_xor(clause& c1, clause& c2); bool clausify(xr& x); void flush_roots(xr& x); lbool eval(xr const& x) const; @@ -445,7 +486,7 @@ namespace sat { inline void assign(literal l, justification j) { if (m_lookahead) m_lookahead->assign(l); else if (m_unit_walk) m_unit_walk->assign(l); - else m_solver->assign(l, j); + else m_solver->assign(l, j); } inline void set_conflict(justification j, literal l) { if (m_lookahead) m_lookahead->set_conflict(); @@ -519,6 +560,10 @@ namespace sat { constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned); constraint* add_pb_ge(literal l, svector const& wlits, unsigned k, bool learned); constraint* add_xr(literal_vector const& lits, bool learned); + literal add_xor_def(literal_vector& lits, bool learned = false); + bool all_distinct(literal_vector const& lits); + bool all_distinct(xr const& x); + bool all_distinct(clause const& cl); void copy_core(ba_solver* result, bool learned); void copy_constraints(ba_solver* result, ptr_vector const& constraints); @@ -540,6 +585,7 @@ namespace sat { check_result check() override; void push() override; void pop(unsigned n) override; + void pre_simplify() override; void simplify() override; void clauses_modifed() override; lbool get_phase(bool_var v) override; diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index f89b20897..0e4472c93 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -32,6 +32,7 @@ namespace sat { updt_params(p); reset_statistics(); m_calls = 0; + m_touch_index = 0; } struct clause_size_lt { @@ -103,6 +104,7 @@ namespace sat { unsigned eliml0 = m_elim_learned_literals; unsigned elim = m_elim_literals; process(nullptr, s.m_clauses); + if (learned) process(nullptr, s.m_learned); s.propagate(false); IF_VERBOSE(4, if (m_elim_learned_literals > eliml0) verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";); @@ -168,13 +170,14 @@ namespace sat { CASSERT("asymm_branch", s.check_invariant()); TRACE("asymm_branch_detail", s.display(tout);); report rpt(*this); - svector saved_phase(s.m_phase); + svector saved_phase(s.m_phase); bool change = true; unsigned counter = 0; while (change && counter < 2) { ++counter; change = false; + s.m_touch_index++; if (m_asymm_branch_sampled) { big big(s.m_rand); if (process(big, true)) change = true; @@ -185,9 +188,10 @@ namespace sat { } if (m_asymm_branch) { m_counter = 0; - if (process(true)) change = true; + if (process(false)) change = true; m_counter = -m_counter; } + m_touch_index = s.m_touch_index; } s.m_phase = saved_phase; @@ -196,6 +200,7 @@ namespace sat { m_asymm_branch_limit = UINT_MAX; CASSERT("asymm_branch", s.check_invariant()); + } /** @@ -222,24 +227,12 @@ namespace sat { } }; - void asymm_branch::sort(big& big, clause const& c) { - sort(big, c.begin(), c.end()); + bool asymm_branch::is_touched(bool_var v) const { + return s.m_touched[v] >= m_touch_index; } - void asymm_branch::radix_sort(big& big, literal_vector& lits) { - const unsigned d = 4; - const unsigned w = 20; // 1M variable cap - unsigned sz = lits.size(); - m_tmp.reserve(sz); - for (unsigned p = 0; p < w/d; ++p) { - unsigned on[16]; - memset(on, 0, 16*sizeof(unsigned)); - for (literal l : lits) on[(big.get_left(l) >> 4*p) & 15]++; - for (unsigned i = 1; i < 16; ++i) on[i] += on[i-1]; - for (unsigned i = sz; i-- > 0; ) - m_tmp[--on[(big.get_left(lits[i]) >> 4*p) & 15]] = lits[i]; - for (unsigned i = sz; i-- > 0; ) lits[i] = m_tmp[i]; - } + void asymm_branch::sort(big& big, clause const& c) { + sort(big, c.begin(), c.end()); } void asymm_branch::sort(big& big, literal const* begin, literal const* end) { @@ -253,10 +246,6 @@ namespace sat { std::sort(m_pos.begin(), m_pos.end(), cmp); std::sort(m_neg.begin(), m_neg.end(), cmp); - // alternative: worse - // radix_sort(big, m_pos); - // radix_sort(big, m_neg); - IF_VERBOSE(100, for (literal l : m_pos) verbose_stream() << big.get_left(l) << " "; verbose_stream() << "\n"; @@ -286,22 +275,6 @@ namespace sat { return false; } - void asymm_branch::minimize(big& big, literal_vector& lemma) { - big.ensure_big(s, true); - sort(big, lemma.begin(), lemma.end()); - uhle(big); - if (!m_to_delete.empty()) { - unsigned j = 0; - for (unsigned i = 0; i < lemma.size(); ++i) { - literal l = lemma[i]; - if (!m_to_delete.contains(l)) { - lemma[j++] = l; - } - } - lemma.shrink(j); - } - } - void asymm_branch::uhle(big& big) { m_to_delete.reset(); if (m_to_delete.empty()) { @@ -365,6 +338,9 @@ namespace sat { bool asymm_branch::propagate_literal(clause const& c, literal l) { + if (!is_touched(l.var())) { + return false; + } SASSERT(!s.inconsistent()); TRACE("asymm_branch_detail", tout << "assigning: " << l << "\n";); s.assign_scoped(l); @@ -439,13 +415,7 @@ namespace sat { scoped_d.del_clause(); return false; default: - c.shrink(new_sz); - if (s.m_config.m_drat && new_sz < old_sz) { - s.m_drat.add(c, true); - c.restore(old_sz); - s.m_drat.del(c); - c.shrink(new_sz); - } + s.shrink(c, old_sz, new_sz); return true; } } diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 4d032022c..75b37dcca 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -36,6 +36,7 @@ namespace sat { int64_t m_counter; random_gen m_rand; unsigned m_calls; + unsigned m_touch_index; // config bool m_asymm_branch; @@ -57,9 +58,10 @@ namespace sat { struct compare_left; + bool is_touched(bool_var v) const; + void sort(big& big, literal const* begin, literal const* end); void sort(big & big, clause const& c); - void radix_sort(big & big, literal_vector& lits); bool uhle(scoped_detach& scoped_d, big & big, clause & c); @@ -100,8 +102,6 @@ namespace sat { void collect_statistics(statistics & st) const; void reset_statistics(); - void minimize(big& big, literal_vector& lemma); - void init_search() { m_calls = 0; } inline void dec(unsigned c) { m_counter -= c; } diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index e682f9dfc..61b4a6f46 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -82,6 +82,7 @@ namespace sat { int get_right(literal l) const { return m_right[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; } literal get_root(literal l); + bool is_root(literal l) { return get_root(l) == l; } bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); } void display(std::ostream& out) const; diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 093e6221f..5731c21b6 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -133,18 +133,12 @@ namespace sat { s.del_clause(c); break; default: - c.shrink(new_sz); + s.shrink(c, sz, new_sz); *it2 = *it; it2++; if (!c.frozen()) { s.attach_clause(c); } - if (s.m_config.m_drat && new_sz < sz) { - s.m_drat.add(c, true); - c.restore(sz); - s.m_drat.del(c); - c.shrink(new_sz); - } break; } } @@ -173,12 +167,33 @@ namespace sat { } }; + bool cleaner::is_clean() const { + for (clause* cp : s.m_clauses) { + for (literal lit : *cp) { + if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false; + } + } + for (clause* cp : s.m_learned) { + for (literal lit : *cp) { + if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false; + } + } + unsigned idx = 0; + for (auto& wlist : s.m_watches) { + literal lit = to_literal(idx); + if (s.value(lit) != l_undef && s.lvl(lit) == 0 && !wlist.empty()) return false; + ++idx; + } + return true; + } + /** \brief Return true if cleaner executed. */ bool cleaner::operator()(bool force) { CASSERT("cleaner_bug", s.check_invariant()); unsigned trail_sz = s.m_trail.size(); + s.propagate(false); // make sure that everything was propagated. TRACE("sat_cleaner_bug", s.display(tout); s.display_watches(tout);); if (s.m_inconsistent) diff --git a/src/sat/sat_cleaner.h b/src/sat/sat_cleaner.h index 4ffc0be10..c740e81bf 100644 --- a/src/sat/sat_cleaner.h +++ b/src/sat/sat_cleaner.h @@ -40,6 +40,7 @@ namespace sat { public: cleaner(solver & s); + bool is_clean() const; bool operator()(bool force = false); void collect_statistics(statistics & st) const; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 78d93880c..5e903ecce 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -54,32 +54,40 @@ namespace sat { m_phase = PS_ALWAYS_FALSE; else if (s == symbol("always_true")) m_phase = PS_ALWAYS_TRUE; + else if (s == symbol("basic_caching")) + m_phase = PS_BASIC_CACHING; else if (s == symbol("caching")) - m_phase = PS_CACHING; + m_phase = PS_SAT_CACHING; else if (s == symbol("random")) m_phase = PS_RANDOM; else throw sat_param_exception("invalid phase selection strategy"); - m_phase_caching_on = p.phase_caching_on(); - m_phase_caching_off = p.phase_caching_off(); + m_rephase_base = p.rephase_base(); + m_search_sat_conflicts = p.search_sat_conflicts(); + m_search_unsat_conflicts = p.search_unsat_conflicts(); m_phase_sticky = p.phase_sticky(); m_restart_initial = p.restart_initial(); m_restart_factor = p.restart_factor(); m_restart_max = p.restart_max(); + m_activity_scale = 100; m_propagate_prefetch = p.propagate_prefetch(); m_inprocess_max = p.inprocess_max(); m_random_freq = p.random_freq(); m_random_seed = p.random_seed(); - if (m_random_seed == 0) + if (m_random_seed == 0) { m_random_seed = _p.get_uint("random_seed", 0); + } m_burst_search = p.burst_search(); m_max_conflicts = p.max_conflicts(); m_num_threads = p.threads(); + m_ddfw_search = p.ddfw_search(); + m_ddfw_threads = p.ddfw_threads(); + m_prob_search = p.prob_search(); m_local_search = p.local_search(); m_local_search_threads = p.local_search_threads(); if (p.local_search_mode() == symbol("gsat")) @@ -89,6 +97,7 @@ namespace sat { m_local_search_dbg_flips = p.local_search_dbg_flips(); m_unit_walk = p.unit_walk(); m_unit_walk_threads = p.unit_walk_threads(); + m_binspr = false; // unsound :-( p.binspr(); m_lookahead_simplify = p.lookahead_simplify(); m_lookahead_double = p.lookahead_double(); m_lookahead_simplify_bca = p.lookahead_simplify_bca(); @@ -159,6 +168,9 @@ namespace sat { m_force_cleanup = p.force_cleanup(); + m_backtrack_scopes = p.backtrack_scopes(); + m_backtrack_init_conflicts = p.backtrack_conflicts(); + m_minimize_lemmas = p.minimize_lemmas(); m_core_minimize = p.core_minimize(); m_core_minimize_partial = p.core_minimize_partial(); @@ -217,6 +229,7 @@ namespace sat { throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected"); m_card_solver = p.cardinality_solver(); + m_xor_solver = p.xor_solver(); sat_simplifier_params sp(_p); m_elim_vars = sp.elim_vars(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 5203b0838..0c1eb48cc 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -27,7 +27,8 @@ namespace sat { enum phase_selection { PS_ALWAYS_TRUE, PS_ALWAYS_FALSE, - PS_CACHING, + PS_BASIC_CACHING, + PS_SAT_CACHING, PS_RANDOM }; @@ -86,9 +87,10 @@ namespace sat { struct config { unsigned long long m_max_memory; phase_selection m_phase; - unsigned m_phase_caching_on; - unsigned m_phase_caching_off; + unsigned m_search_sat_conflicts; + unsigned m_search_unsat_conflicts; bool m_phase_sticky; + unsigned m_rephase_base; bool m_propagate_prefetch; restart_strategy m_restart; bool m_restart_fast; @@ -96,6 +98,7 @@ namespace sat { double m_restart_factor; // for geometric case double m_restart_margin; // for ema unsigned m_restart_max; + unsigned m_activity_scale; double m_fast_glue_avg; double m_slow_glue_avg; unsigned m_inprocess_max; @@ -104,12 +107,16 @@ namespace sat { unsigned m_burst_search; unsigned m_max_conflicts; unsigned m_num_threads; + bool m_ddfw_search; + unsigned m_ddfw_threads; + bool m_prob_search; unsigned m_local_search_threads; bool m_local_search; local_search_mode m_local_search_mode; bool m_local_search_dbg_flips; unsigned m_unit_walk_threads; bool m_unit_walk; + bool m_binspr; bool m_lookahead_simplify; bool m_lookahead_simplify_bca; cutoff_t m_lookahead_cube_cutoff; @@ -143,11 +150,16 @@ namespace sat { bool m_force_cleanup; + // backtracking + unsigned m_backtrack_scopes; + unsigned m_backtrack_init_conflicts; bool m_minimize_lemmas; bool m_dyn_sub_res; bool m_core_minimize; bool m_core_minimize_partial; + + // drat proofs bool m_drat; bool m_drat_binary; symbol m_drat_file; @@ -155,6 +167,7 @@ namespace sat { bool m_drat_check_sat; bool m_card_solver; + bool m_xor_solver; pb_resolve m_pb_resolve; pb_lemma_format m_pb_lemma_format; diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp new file mode 100644 index 000000000..3986de214 --- /dev/null +++ b/src/sat/sat_ddfw.cpp @@ -0,0 +1,594 @@ +/*++ + Copyright (c) 2019 Microsoft Corporation + + Module Name: + + sat_ddfw.cpp + + Abstract: + + DDFW Local search module for clauses + + Author: + + Nikolaj Bjorner, Marijn Heule 2019-4-23 + + + Notes: + + http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf + + + Todo: + - rephase strategy + - experiment with backoff schemes for restarts + - parallel sync + --*/ + +#include "util/luby.h" +#include "sat/sat_ddfw.h" +#include "sat/sat_solver.h" +#include "sat/sat_params.hpp" + +namespace sat { + + ddfw::~ddfw() { + for (auto& ci : m_clauses) { + m_alloc.del_clause(ci.m_clause); + } + } + + + lbool ddfw::check(unsigned sz, literal const* assumptions, parallel* p) { + init(sz, assumptions); + flet _p(m_par, p); + while (m_limit.inc() && m_min_sz > 0) { + if (should_reinit_weights()) do_reinit_weights(); + else if (do_flip()) ; + else if (should_restart()) do_restart(); + else if (should_parallel_sync()) do_parallel_sync(); + else shift_weights(); + } + return m_min_sz == 0 ? l_true : l_undef; + } + + void ddfw::log() { + double sec = m_stopwatch.get_current_seconds(); + double kflips_per_sec = (m_flips - m_last_flips) / (1000.0 * sec); + if (m_last_flips == 0) { + IF_VERBOSE(0, verbose_stream() << "(sat.ddfw :unsat :models :kflips/sec :flips :restarts :reinits :unsat_vars :shifts"; + if (m_par) verbose_stream() << " :par"; + verbose_stream() << ")\n"); + } + IF_VERBOSE(0, verbose_stream() << "(sat.ddfw " + << std::setw(07) << m_min_sz + << std::setw(07) << m_models.size() + << std::setw(10) << kflips_per_sec + << std::setw(10) << m_flips + << std::setw(10) << m_restart_count + << std::setw(10) << m_reinit_count + << std::setw(10) << m_unsat_vars.size() + << std::setw(10) << m_shifts; + if (m_par) verbose_stream() << std::setw(10) << m_parsync_count; + verbose_stream() << ")\n"); + m_stopwatch.start(); + m_last_flips = m_flips; + } + + bool ddfw::do_flip() { + bool_var v = pick_var(); + if (reward(v) > 0 || (reward(v) == 0 && m_rand(100) <= m_config.m_use_reward_zero_pct)) { + flip(v); + if (m_unsat.size() <= m_min_sz) save_best_values(); + return true; + } + return false; + } + + bool_var ddfw::pick_var() { + double sum_pos = 0; + unsigned n = 1; + bool_var v0 = null_bool_var; + for (bool_var v : m_unsat_vars) { + int r = reward(v); + if (r > 0) { + sum_pos += score(r); + } + else if (r == 0 && sum_pos == 0 && (m_rand() % (n++)) == 0) { + v0 = v; + } + } + if (sum_pos > 0) { + double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos; + for (bool_var v : m_unsat_vars) { + int r = reward(v); + if (r > 0) { + lim_pos -= score(r); + if (lim_pos <= 0) { + if (m_par) update_reward_avg(v); + return v; + } + } + } + } + if (v0 != null_bool_var) { + return v0; + } + return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size())); + } + + /** + * TBD: map reward value to a score, possibly through an exponential function, such as + * exp(-tau/r), where tau > 0 + */ + double ddfw::mk_score(unsigned r) { + return r; + } + + + void ddfw::add(unsigned n, literal const* c) { + clause* cls = m_alloc.mk_clause(n, c, false); + unsigned idx = m_clauses.size(); + m_clauses.push_back(clause_info(cls, m_config.m_init_clause_weight)); + for (literal lit : *cls) { + m_use_list.reserve(lit.index()+1); + m_vars.reserve(lit.var()+1); + m_use_list[lit.index()].push_back(idx); + } + } + + void ddfw::add(solver const& s) { + for (auto& ci : m_clauses) { + m_alloc.del_clause(ci.m_clause); + } + m_clauses.reset(); + m_use_list.reset(); + m_num_non_binary_clauses = 0; + + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + add(1, s.m_trail.c_ptr() + i); + } + unsigned sz = s.m_watches.size(); + for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { + literal l1 = ~to_literal(l_idx); + watch_list const & wlist = s.m_watches[l_idx]; + for (watched const& w : wlist) { + if (!w.is_binary_non_learned_clause()) + continue; + literal l2 = w.get_literal(); + if (l1.index() > l2.index()) + continue; + literal ls[2] = { l1, l2 }; + add(2, ls); + } + } + for (clause* c : s.m_clauses) { + add(c->size(), c->begin()); + } + m_num_non_binary_clauses = s.m_clauses.size(); + } + + void ddfw::add_assumptions() { + for (unsigned i = 0; i < m_assumptions.size(); ++i) { + add(1, m_assumptions.c_ptr() + i); + } + } + + void ddfw::init(unsigned sz, literal const* assumptions) { + m_assumptions.reset(); + m_assumptions.append(sz, assumptions); + add_assumptions(); + for (unsigned v = 0; v < num_vars(); ++v) { + literal lit(v, false), nlit(v, true); + value(v) = (m_rand() % 2) == 0; // m_use_list[lit.index()].size() >= m_use_list[nlit.index()].size(); + } + init_clause_data(); + flatten_use_list(); + + m_reinit_count = 0; + m_reinit_next = m_config.m_reinit_base; + + m_restart_count = 0; + m_restart_next = m_config.m_restart_base*2; + + m_parsync_count = 0; + m_parsync_next = m_config.m_parsync_base; + + m_min_sz = m_unsat.size(); + m_flips = 0; + m_last_flips = 0; + m_shifts = 0; + m_stopwatch.start(); + } + + void ddfw::reinit(solver& s) { + add(s); + add_assumptions(); + if (s.m_best_phase_size > 0) { + for (unsigned v = 0; v < num_vars(); ++v) { + value(v) = s.m_best_phase[v]; + reward(v) = 0; + make_count(v) = 0; + } + } + init_clause_data(); + flatten_use_list(); + } + + void ddfw::flatten_use_list() { + m_use_list_index.reset(); + m_flat_use_list.reset(); + for (auto const& ul : m_use_list) { + m_use_list_index.push_back(m_flat_use_list.size()); + m_flat_use_list.append(ul); + } + m_use_list_index.push_back(m_flat_use_list.size()); + } + + + void ddfw::flip(bool_var v) { + ++m_flips; + literal lit = literal(v, !value(v)); + literal nlit = ~lit; + SASSERT(is_true(lit)); + for (unsigned cls_idx : use_list(*this, lit)) { + clause_info& ci = m_clauses[cls_idx]; + ci.del(lit); + unsigned w = ci.m_weight; + // cls becomes false: flip any variable in clause to receive reward w + switch (ci.m_num_trues) { + case 0: { + m_unsat.insert(cls_idx); + clause const& c = get_clause(cls_idx); + for (literal l : c) { + inc_reward(l, w); + inc_make(l); + } + inc_reward(lit, w); + break; + } + case 1: + dec_reward(to_literal(ci.m_trues), w); + break; + default: + break; + } + } + for (unsigned cls_idx : use_list(*this, nlit)) { + clause_info& ci = m_clauses[cls_idx]; + unsigned w = ci.m_weight; + // the clause used to have a single true (pivot) literal, now it has two. + // Then the previous pivot is no longer penalized for flipping. + switch (ci.m_num_trues) { + case 0: { + m_unsat.remove(cls_idx); + clause const& c = get_clause(cls_idx); + for (literal l : c) { + dec_reward(l, w); + dec_make(l); + } + dec_reward(nlit, w); + break; + } + case 1: + inc_reward(to_literal(ci.m_trues), w); + break; + default: + break; + } + ci.add(nlit); + } + value(v) = !value(v); + } + + bool ddfw::should_reinit_weights() { + return m_flips >= m_reinit_next; + } + + void ddfw::do_reinit_weights() { + log(); + + if (m_reinit_count % 2 == 0) { + for (auto& ci : m_clauses) { + ci.m_weight += 1; + } + } + else { + for (auto& ci : m_clauses) { + if (ci.is_true()) { + ci.m_weight = m_config.m_init_clause_weight; + } + else { + ci.m_weight = m_config.m_init_clause_weight + 1; + } + } + } + init_clause_data(); + ++m_reinit_count; + m_reinit_next += m_reinit_count * m_config.m_reinit_base; + } + + void ddfw::init_clause_data() { + for (unsigned v = 0; v < num_vars(); ++v) { + make_count(v) = 0; + reward(v) = 0; + } + m_unsat_vars.reset(); + m_unsat.reset(); + unsigned sz = m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + auto& ci = m_clauses[i]; + clause const& c = get_clause(i); + ci.m_trues = 0; + ci.m_num_trues = 0; + for (literal lit : c) { + if (is_true(lit)) { + ci.add(lit); + } + } + switch (ci.m_num_trues) { + case 0: + for (literal lit : c) { + inc_reward(lit, ci.m_weight); + inc_make(lit); + } + m_unsat.insert(i); + break; + case 1: + dec_reward(to_literal(ci.m_trues), ci.m_weight); + break; + default: + break; + } + } + } + + bool ddfw::should_restart() { + return m_flips >= m_restart_next; + } + + void ddfw::do_restart() { + reinit_values(); + init_clause_data(); + m_restart_next += m_config.m_restart_base*get_luby(++m_restart_count); + } + + /** + \brief the higher the bias, the lower the probability to deviate from the value of the bias + during a restart. + bias = 0 -> flip truth value with 50% + |bias| = 1 -> toss coin with 25% probability + |bias| = 2 -> toss coin with 12.5% probability + etc + */ + void ddfw::reinit_values() { + for (unsigned i = 0; i < num_vars(); ++i) { + int b = bias(i); + if (0 == (m_rand() % (1 + abs(b)))) { + value(i) = (m_rand() % 2) == 0; + } + else { + value(i) = bias(i) > 0; + } + } + } + + bool ddfw::should_parallel_sync() { + return m_par != nullptr && m_flips >= m_parsync_next; + } + + void ddfw::do_parallel_sync() { + if (m_par->from_solver(*this)) { + // Sum exp(xi) / exp(a) = Sum exp(xi - a) + double max_avg = 0; + for (unsigned v = 0; v < num_vars(); ++v) { + max_avg = std::max(max_avg, (double)m_vars[v].m_reward_avg); + } + double sum = 0; + for (unsigned v = 0; v < num_vars(); ++v) { + sum += exp(m_config.m_itau * (m_vars[v].m_reward_avg - max_avg)); + } + if (sum == 0) { + sum = 0.01; + } + m_probs.reset(); + for (unsigned v = 0; v < num_vars(); ++v) { + m_probs.push_back(exp(m_config.m_itau * (m_vars[v].m_reward_avg - max_avg)) / sum); + } + m_par->to_solver(*this); + } + ++m_parsync_count; + m_parsync_next *= 3; + m_parsync_next /= 2; + } + + void ddfw::save_best_values() { + if (m_unsat.empty()) { + m_model.reserve(num_vars()); + for (unsigned i = 0; i < num_vars(); ++i) { + m_model[i] = to_lbool(value(i)); + } + } + if (m_unsat.size() < m_min_sz) { + m_models.reset(); + // skip saving the first model. + for (unsigned v = 0; v < num_vars(); ++v) { + int& b = bias(v); + if (abs(b) > 3) { + b = b > 0 ? 3 : -3; + } + } + } + unsigned h = value_hash(); + if (!m_models.contains(h)) { + for (unsigned v = 0; v < num_vars(); ++v) { + bias(v) += value(v) ? 1 : -1; + } + m_models.insert(h); + if (m_models.size() > m_config.m_max_num_models) { + m_models.erase(*m_models.begin()); + } + } + m_min_sz = m_unsat.size(); + } + + unsigned ddfw::value_hash() const { + unsigned s0 = 0, s1 = 0; + for (auto const& vi : m_vars) { + s0 += vi.m_value; + s1 += s0; + } + return s1; + } + + + /** + \brief Filter on whether to select a satisfied clause + 1. with some probability prefer higher weight to lesser weight. + 2. take into account number of trues ? + 3. select multiple clauses instead of just one per clause in unsat. + */ + + bool ddfw::select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n) { + if (cn.m_num_trues == 0 || cn.m_weight < max_weight) { + return false; + } + if (cn.m_weight > max_weight) { + n = 2; + return true; + } + return (m_rand() % (n++)) == 0; + } + + unsigned ddfw::select_max_same_sign(unsigned cf_idx) { + clause const& c = get_clause(cf_idx); + unsigned sz = c.size(); + unsigned max_weight = 2; + unsigned max_trues = 0; + unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause. + unsigned n = 1; + for (literal lit : c) { + for (unsigned cn_idx : use_list(*this, lit)) { + auto& cn = m_clauses[cn_idx]; + if (select_clause(max_weight, max_trues, cn, n)) { + cl = cn_idx; + max_weight = cn.m_weight; + max_trues = cn.m_num_trues; + } + } + } + return cl; + } + + void ddfw::shift_weights() { + ++m_shifts; + for (unsigned cf_idx : m_unsat) { + auto& cf = m_clauses[cf_idx]; + SASSERT(!cf.is_true()); + unsigned cn_idx = select_max_same_sign(cf_idx); + while (cn_idx == UINT_MAX) { + unsigned idx = (m_rand() * m_rand()) % m_clauses.size(); + auto & cn = m_clauses[idx]; + if (cn.is_true() && cn.m_weight >= 2) { + cn_idx = idx; + } + } + auto & cn = m_clauses[cn_idx]; + SASSERT(cn.is_true()); + unsigned wn = cn.m_weight; + SASSERT(wn >= 2); + unsigned inc = (wn > 2) ? 2 : 1; + SASSERT(wn - inc >= 1); + cf.m_weight += inc; + cn.m_weight -= inc; + for (literal lit : get_clause(cf_idx)) { + inc_reward(lit, inc); + } + if (cn.m_num_trues == 1) { + inc_reward(to_literal(cn.m_trues), inc); + } + } + // DEBUG_CODE(invariant();); + } + + std::ostream& ddfw::display(std::ostream& out) const { + unsigned num_cls = m_clauses.size(); + for (unsigned i = 0; i < num_cls; ++i) { + out << get_clause(i) << " "; + auto const& ci = m_clauses[i]; + out << ci.m_num_trues << " " << ci.m_weight << "\n"; + } + for (unsigned v = 0; v < num_vars(); ++v) { + out << v << ": " << reward(v) << "\n"; + } + out << "unsat vars: "; + for (bool_var v : m_unsat_vars) { + out << v << " "; + } + out << "\n"; + return out; + } + + void ddfw::invariant() { + // every variable in unsat vars is in a false clause. + for (bool_var v : m_unsat_vars) { + bool found = false; + for (unsigned cl : m_unsat) { + for (literal lit : get_clause(cl)) { + if (lit.var() == v) { found = true; break; } + } + if (found) break; + } + if (!found) IF_VERBOSE(0, verbose_stream() << "unsat var not found: " << v << "\n"; ); + VERIFY(found); + } + for (unsigned v = 0; v < num_vars(); ++v) { + int v_reward = 0; + literal lit(v, !value(v)); + for (unsigned j : m_use_list[lit.index()]) { + clause_info const& ci = m_clauses[j]; + if (ci.m_num_trues == 1) { + SASSERT(lit == to_literal(ci.m_trues)); + v_reward -= ci.m_weight; + } + } + for (unsigned j : m_use_list[(~lit).index()]) { + clause_info const& ci = m_clauses[j]; + if (ci.m_num_trues == 0) { + v_reward += ci.m_weight; + } + } + IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n"); + SASSERT(reward(v) == v_reward); + } + for (auto const& ci : m_clauses) { + SASSERT(ci.m_weight > 0); + } + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause_info const& ci = m_clauses[i]; + bool found = false; + for (literal lit : get_clause(i)) { + if (is_true(lit)) found = true; + } + SASSERT(ci.is_true() == found); + SASSERT(found == !m_unsat.contains(i)); + } + // every variable in a false clause is in unsat vars + for (unsigned cl : m_unsat) { + for (literal lit : get_clause(cl)) { + SASSERT(m_unsat_vars.contains(lit.var())); + } + } + } + + void ddfw::updt_params(params_ref const& _p) { + sat_params p(_p); + m_config.m_init_clause_weight = p.ddfw_init_clause_weight(); + m_config.m_use_reward_zero_pct = p.ddfw_use_reward_pct(); + m_config.m_reinit_base = p.ddfw_reinit_base(); + m_config.m_restart_base = p.ddfw_restart_base(); + } + +} + diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h new file mode 100644 index 000000000..c74d3fe06 --- /dev/null +++ b/src/sat/sat_ddfw.h @@ -0,0 +1,227 @@ +/*++ + Copyright (c) 2019 Microsoft Corporation + + Module Name: + + sat_ddfw.h + + Abstract: + + DDFW Local search module for clauses + + Author: + + Nikolaj Bjorner, Marijn Heule 2019-4-23 + + Notes: + + http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf + + --*/ +#ifndef _SAT_DDFW_ +#define _SAT_DDFW_ + +#include "util/uint_set.h" +#include "util/rlimit.h" +#include "util/params.h" +#include "util/ema.h" +#include "sat/sat_clause.h" +#include "sat/sat_types.h" + +namespace sat { + class solver; + class parallel; + + class ddfw : public i_local_search { + + struct clause_info { + clause_info(clause* cl, unsigned init_weight): m_weight(init_weight), m_trues(0), m_num_trues(0), m_clause(cl) {} + unsigned m_weight; // weight of clause + unsigned m_trues; // set of literals that are true + unsigned m_num_trues; // size of true set + clause* m_clause; + bool is_true() const { return m_num_trues > 0; } + void add(literal lit) { ++m_num_trues; m_trues += lit.index(); } + void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); } + }; + + struct config { + config() { reset(); } + unsigned m_use_reward_zero_pct; + unsigned m_init_clause_weight; + unsigned m_max_num_models; + unsigned m_restart_base; + unsigned m_reinit_base; + unsigned m_parsync_base; + double m_itau; + void reset() { + m_init_clause_weight = 8; + m_use_reward_zero_pct = 15; + m_max_num_models = (1 << 10); + m_restart_base = 100333; + m_reinit_base = 10000; + m_parsync_base = 333333; + m_itau = 0.5; + } + }; + + struct var_info { + var_info(): m_value(false), m_reward(0), m_make_count(0), m_bias(0), m_reward_avg(1e-5) {} + bool m_value; + int m_reward; + unsigned m_make_count; + int m_bias; + ema m_reward_avg; + }; + + config m_config; + reslimit m_limit; + clause_allocator m_alloc; + svector m_clauses; + literal_vector m_assumptions; + svector m_vars; // var -> info + svector m_probs; // var -> probability of flipping + svector m_scores; // reward -> score + model m_model; // var -> best assignment + + vector m_use_list; + unsigned_vector m_flat_use_list; + unsigned_vector m_use_list_index; + + indexed_uint_set m_unsat; + indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses + random_gen m_rand; + unsigned m_num_non_binary_clauses; + unsigned m_restart_count, m_reinit_count, m_parsync_count; + uint64_t m_restart_next, m_reinit_next, m_parsync_next; + uint64_t m_flips, m_last_flips, m_shifts; + unsigned m_min_sz; + hashtable> m_models; + stopwatch m_stopwatch; + + parallel* m_par; + + class use_list { + ddfw& p; + unsigned i; + public: + use_list(ddfw& p, literal lit): + p(p), i(lit.index()) {} + unsigned const* begin() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i]; } + unsigned const* end() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i+1]; } + }; + + void flatten_use_list(); + + double mk_score(unsigned r); + + inline double score(unsigned r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; } + + inline unsigned num_vars() const { return m_vars.size(); } + + inline unsigned& make_count(bool_var v) { return m_vars[v].m_make_count; } + + inline bool& value(bool_var v) { return m_vars[v].m_value; } + + inline bool value(bool_var v) const { return m_vars[v].m_value; } + + inline int& reward(bool_var v) { return m_vars[v].m_reward; } + + inline int reward(bool_var v) const { return m_vars[v].m_reward; } + + inline int& bias(bool_var v) { return m_vars[v].m_bias; } + + unsigned value_hash() const; + + inline bool is_true(literal lit) const { return value(lit.var()) != lit.sign(); } + + inline clause const& get_clause(unsigned idx) const { return *m_clauses[idx].m_clause; } + + inline unsigned get_weight(unsigned idx) const { return m_clauses[idx].m_weight; } + + inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); } + + void update_reward_avg(bool_var v) { m_vars[v].m_reward_avg.update(reward(v)); } + + unsigned select_max_same_sign(unsigned cf_idx); + + inline void inc_make(literal lit) { + bool_var v = lit.var(); + if (make_count(v)++ == 0) m_unsat_vars.insert(v); + } + + inline void dec_make(literal lit) { + bool_var v = lit.var(); + if (--make_count(v) == 0) m_unsat_vars.remove(v); + } + + inline void inc_reward(literal lit, int inc) { reward(lit.var()) += inc; } + + inline void dec_reward(literal lit, int inc) { reward(lit.var()) -= inc; } + + // flip activity + bool do_flip(); + bool_var pick_var(); + void flip(bool_var v); + void save_best_values(); + + // shift activity + void shift_weights(); + + // reinitialize weights activity + bool should_reinit_weights(); + void do_reinit_weights(); + inline bool select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n); + + // restart activity + bool should_restart(); + void do_restart(); + void reinit_values(); + + // parallel integration + bool should_parallel_sync(); + void do_parallel_sync(); + + void log(); + + void init(unsigned sz, literal const* assumptions); + + void init_clause_data(); + + void invariant(); + + void add(unsigned sz, literal const* c); + + void add_assumptions(); + + public: + + ddfw(): m_par(nullptr) {} + + ~ddfw() override; + + lbool check(unsigned sz, literal const* assumptions, parallel* p) override; + + void updt_params(params_ref const& p) override; + + model const& get_model() const override { return m_model; } + + reslimit& rlimit() override { return m_limit; } + + void set_seed(unsigned n) override { m_rand.set_seed(n); } + + void add(solver const& s) override; + + std::ostream& display(std::ostream& out) const; + + // for parallel integration + unsigned num_non_binary_clauses() const override { return m_num_non_binary_clauses; } + void reinit(solver& s) override; + + void collect_statistics(statistics& st) const override {} + + double get_priority(bool_var v) const override { return m_probs[v]; } + }; +} + +#endif diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 446569e84..191384582 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -62,6 +62,7 @@ namespace sat { virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma virtual void push() = 0; virtual void pop(unsigned n) = 0; + virtual void pre_simplify() = 0; virtual void simplify() = 0; // have a way to replace l by r in all constraints virtual bool set_root(literal l, literal r) { return false; } diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index 32feaa2c7..266da96e9 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -135,7 +135,6 @@ namespace sat { VERIFY(s.m_decision.size() == s.num_vars()); VERIFY(s.m_eliminated.size() == s.num_vars()); VERIFY(s.m_external.size() == s.num_vars()); - VERIFY(s.m_level.size() == s.num_vars()); VERIFY(s.m_mark.size() == s.num_vars()); VERIFY(s.m_activity.size() == s.num_vars()); VERIFY(s.m_phase.size() == s.num_vars()); diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h index 497d636c8..0357621f9 100644 --- a/src/sat/sat_justification.h +++ b/src/sat/sat_justification.h @@ -25,17 +25,20 @@ namespace sat { public: enum kind { NONE, BINARY, TERNARY, CLAUSE, EXT_JUSTIFICATION }; private: + unsigned m_level; size_t m_val1; unsigned m_val2; - justification(ext_justification_idx idx, kind k):m_val1(idx), m_val2(k) {} + justification(unsigned lvl, ext_justification_idx idx, kind k):m_level(lvl), m_val1(idx), m_val2(k) {} unsigned val1() const { return static_cast(m_val1); } public: - justification():m_val1(0), m_val2(NONE) {} - explicit justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {} - justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {} - explicit justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {} - static justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); } + justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {} + explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {} + justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {} + explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {} + static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); } + unsigned level() const { return m_level; } + kind get_kind() const { return static_cast(m_val2 & 7); } bool is_none() const { return m_val2 == NONE; } @@ -72,6 +75,7 @@ namespace sat { out << "external"; break; } + out << " @" << j.level(); return out; } }; diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index cdb90e2a0..8465b4abe 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -216,10 +216,10 @@ namespace sat { void local_search::set_best_unsat() { m_best_unsat = m_unsat_stack.size(); - if (m_best_unsat == 1) { - constraint const& c = m_constraints[m_unsat_stack[0]]; - IF_VERBOSE(2, display(verbose_stream() << "single unsat:", c)); - } + m_best_phase.reserve(m_vars.size()); + for (unsigned i = m_vars.size(); i-- > 0; ) { + m_best_phase[i] = m_vars[i].m_value; + } } void local_search::verify_solution() const { @@ -351,7 +351,16 @@ namespace sat { m_par(nullptr) { } - void local_search::import(solver& s, bool _init) { + void local_search::reinit(solver& s) { + import(s, true); + if (s.m_best_phase_size > 0) { + for (unsigned i = num_vars(); i-- > 0; ) { + set_phase(i, s.m_best_phase[i]); + } + } + } + + void local_search::import(solver const& s, bool _init) { flet linit(m_initializing, true); m_is_pb = false; m_vars.reset(); @@ -364,7 +373,7 @@ namespace sat { if (m_config.phase_sticky()) { unsigned v = 0; for (var_info& vi : m_vars) { - vi.m_bias = s.m_phase[v++] == POS_PHASE ? 98 : 2; + vi.m_bias = s.m_phase[v++] ? 98 : 2; } } @@ -495,7 +504,7 @@ namespace sat { lbool local_search::check() { - return check(0, nullptr); + return check(0, nullptr, nullptr); } #define PROGRESS(tries, flips) \ @@ -530,7 +539,25 @@ namespace sat { } total_flips += step; PROGRESS(tries, total_flips); - if (m_par && m_par->get_phase(*this)) { + if (m_par) { + double max_avg = 0; + for (unsigned v = 0; v < num_vars(); ++v) { + max_avg = std::max(max_avg, (double)m_vars[v].m_slow_break); + } + double sum = 0; + for (unsigned v = 0; v < num_vars(); ++v) { + sum += exp(m_config.itau() * (m_vars[v].m_slow_break - max_avg)); + } + if (sum == 0) { + sum = 0.01; + } + for (unsigned v = 0; v < num_vars(); ++v) { + m_vars[v].m_break_prob = exp(m_config.itau() * (m_vars[v].m_slow_break - max_avg)) / sum; + } + + m_par->to_solver(*this); + } + if (m_par && m_par->from_solver(*this)) { reinit(); } if (tries % 10 == 0 && !m_unsat_stack.empty()) { @@ -834,11 +861,10 @@ namespace sat { } - void local_search::set_phase(bool_var v, lbool f) { + void local_search::set_phase(bool_var v, bool f) { unsigned& bias = m_vars[v].m_bias; - if (f == l_true && bias < 100) bias++; - if (f == l_false && bias > 0) bias--; - // f == l_undef ? + if (f && bias < 100) bias++; + if (!f && bias > 0) bias--; } void local_search::set_bias(bool_var v, lbool f) { diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 00c38e481..3c7e2b0e3 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -36,6 +36,7 @@ namespace sat { local_search_mode m_mode; bool m_phase_sticky; bool m_dbg_flips; + double m_itau; friend class local_search; @@ -53,6 +54,7 @@ namespace sat { m_mode = local_search_mode::wsat; m_phase_sticky = false; m_dbg_flips = false; + m_itau = 0.5; } unsigned random_seed() const { return m_random_seed; } @@ -60,6 +62,7 @@ namespace sat { local_search_mode mode() const { return m_mode; } bool phase_sticky() const { return m_phase_sticky; } bool dbg_flips() const { return m_dbg_flips; } + double itau() const { return m_itau; } void set_random_seed(unsigned s) { m_random_seed = s; } void set_best_known_value(unsigned v) { m_best_known_value = v; } @@ -67,7 +70,7 @@ namespace sat { }; - class local_search { + class local_search : public i_local_search { struct pbcoeff { unsigned m_constraint_id; @@ -102,6 +105,7 @@ namespace sat { literal_vector m_bin[2]; unsigned m_flips; ema m_slow_break; + double m_break_prob; var_info(): m_value(true), m_bias(50), @@ -111,7 +115,8 @@ namespace sat { m_score(0), m_slack_score(0), m_flips(0), - m_slow_break(1e-5) + m_slow_break(1e-5), + m_break_prob(0) {} }; @@ -134,6 +139,7 @@ namespace sat { local_search_config m_config; vector m_vars; // variables + svector m_best_phase; // best value in round svector m_units; // unit clauses vector m_constraints; // all constraints literal_vector m_assumptions; // temporary assumptions @@ -167,7 +173,6 @@ namespace sat { parallel* m_par; model m_model; - 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++; } inline void dec_score(bool_var v) { m_vars[v].m_score--; } @@ -223,48 +228,58 @@ namespace sat { void extract_model(); void add_clause(unsigned sz, literal const* c); 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; + lbool check(); + + unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars + public: local_search(); - reslimit& rlimit() { return m_limit; } + ~local_search() override; + + reslimit& rlimit() override { return m_limit; } - ~local_search(); + lbool check(unsigned sz, literal const* assumptions, parallel* p) override; + + unsigned num_non_binary_clauses() const override { return m_num_non_binary_clauses; } + + void add(solver const& s) override { import(s, false); } + + model const& get_model() const override { return m_model; } + + void collect_statistics(statistics& st) const override; + + void updt_params(params_ref const& p) override {} + + void set_seed(unsigned n) override { config().set_random_seed(n); } + + void reinit(solver& s) override; + + // used by unit-walk + void set_phase(bool_var v, bool f); + + void set_bias(bool_var v, lbool f); + + bool get_best_phase(bool_var v) const { return m_best_phase[v]; } + + inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; } + + double get_priority(bool_var v) const override { return m_vars[v].m_break_prob; } + + void import(solver const& s, bool init); void add_cardinality(unsigned sz, literal const* c, unsigned k); void add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k); - - lbool check(); - - lbool check(unsigned sz, literal const* assumptions, parallel* p = nullptr); local_search_config& config() { return m_config; } - 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); - - 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_lookahead.cpp b/src/sat/sat_lookahead.cpp index 74ac831d8..824055bae 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -102,7 +102,6 @@ namespace sat { literal l = lits.back(); lits.pop_back(); SASSERT(!m_binary[(~l).index()].empty()); - IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";); SASSERT(m_binary[(~l).index()].back() == ~to_literal(idx)); m_binary[(~l).index()].pop_back(); ++m_stats.m_del_binary; @@ -1655,6 +1654,77 @@ namespace sat { return result; } + void lookahead::get_clauses(literal_vector& clauses, unsigned max_clause_size) { + // push binary clauses + unsigned num_lits = m_s.num_vars() * 2; + for (unsigned idx = 0; idx < num_lits; ++idx) { + literal u = to_literal(idx); + if (m_s.was_eliminated(u.var()) || is_false(u) || is_true(u)) continue; + for (literal v : m_binary[idx]) { + if (u.index() < v.index() && !m_s.was_eliminated(v.var()) && !is_false(v) && !is_true(v)) { + clauses.push_back(~u); + clauses.push_back(v); + clauses.push_back(null_literal); + } + } + } + // push ternary clauses + for (unsigned idx = 0; idx < num_lits; ++idx) { + literal u = to_literal(idx); + if (is_true(u) || is_false(u)) continue; + unsigned sz = m_ternary_count[u.index()]; + for (binary const& b : m_ternary[u.index()]) { + if (sz-- == 0) break; + if (u.index() > b.m_v.index() || u.index() > b.m_u.index()) + continue; + if (is_true(b.m_u) || is_true(b.m_v)) + continue; + if (is_false(b.m_u) && is_false(b.m_v)) + continue; + clauses.push_back(u); + if (!is_false(b.m_u)) clauses.push_back(b.m_u); + if (!is_false(b.m_v)) clauses.push_back(b.m_v); + clauses.push_back(null_literal); + } + } + + // push n-ary clauses + for (unsigned idx = 0; idx < num_lits; ++idx) { + literal u = to_literal(idx); + unsigned sz = m_nary_count[u.index()]; + for (nary* n : m_nary[u.index()]) { + if (sz-- == 0) break; + unsigned sz0 = clauses.size(); + if (n->size() > max_clause_size) continue; + for (literal lit : *n) { + if (is_true(lit)) { + clauses.shrink(sz0); + break; + } + if (!is_false(lit)) { + clauses.push_back(lit); + } + } + if (clauses.size() > sz0) { + clauses.push_back(null_literal); + } + } + } + + TRACE("sat", + for (literal lit : clauses) { + if (lit == null_literal) { + tout << "\n"; + } + else { + tout << lit << " "; + } + } + tout << "\n"; + m_s.display(tout); + ); + } + void lookahead::propagate_binary(literal l) { literal_vector const& lits = m_binary[l.index()]; TRACE("sat", tout << l << " => " << lits << "\n";); @@ -1687,10 +1757,14 @@ namespace sat { unsigned base = 2; bool change = true; literal last_changed = null_literal; - while (change && !inconsistent()) { + unsigned ops = 0; + m_max_ops = 100000; + while (change && !inconsistent() && ops < m_max_ops) { change = false; - for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { + IF_VERBOSE(10, verbose_stream() << "(sat.lookahead :compute-reward " << m_lookahead.size() << ")\n"); + for (unsigned i = 0; !inconsistent() && i < m_lookahead.size() && ops < m_max_ops; ++i) { checkpoint(); + ++ops; literal lit = m_lookahead[i].m_lit; if (lit == last_changed) { SASSERT(!change); @@ -1714,13 +1788,11 @@ namespace sat { num_units += do_double(lit, dl_lvl); if (dl_lvl > level) { base = dl_lvl; - //SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset); SASSERT(get_level(m_trail.back()) == base); } unsat = inconsistent(); pop_lookahead1(lit, num_units); } - // VERIFY(!missed_propagation()); if (unsat) { TRACE("sat", tout << "backtracking and setting " << ~lit << "\n";); lookahead_backtrack(); @@ -2165,6 +2237,29 @@ namespace sat { return l_undef; } + + void lookahead::display_lookahead_scores(std::ostream& out) { + scoped_ext _scoped_ext(*this); + m_select_lookahead_vars.reset(); + init_search(); + scoped_level _sl(*this, c_fixed_truth); + m_search_mode = lookahead_mode::searching; + literal l = choose_base(); + if (l == null_literal) { + out << "null\n"; + return; + } + for (auto const& l : m_lookahead) { + literal lit = l.m_lit; + if (!lit.sign() && is_undef(lit)) { + double diff1 = get_lookahead_reward(lit); + double diff2 = get_lookahead_reward(~lit); + out << lit << " " << diff1 << " " << diff2 << "\n"; + } + } + } + + void lookahead::init_model() { m_model.reset(); for (unsigned i = 0; i < m_num_vars; ++i) { @@ -2255,7 +2350,13 @@ namespace sat { } } + + literal lookahead::choose() { + return choose_base(); + } + + literal lookahead::choose_base() { literal l = null_literal; while (l == null_literal && !inconsistent()) { pre_select(); @@ -2284,7 +2385,7 @@ namespace sat { init(learned); if (inconsistent()) return; inc_istamp(); - choose(); + choose_base(); if (inconsistent()) return; SASSERT(m_trail_lim.empty()); unsigned num_units = 0; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index f6103ee7c..21246f790 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -20,9 +20,9 @@ Notes: #ifndef _SAT_LOOKAHEAD_H_ #define _SAT_LOOKAHEAD_H_ -// #define OLD_NARY 0 -#include "sat_elim_eqs.h" +#include "util/small_object_allocator.h" +#include "sat/sat_elim_eqs.h" namespace sat { @@ -247,6 +247,7 @@ namespace sat { stats m_stats; model m_model; cube_state m_cube_state; + unsigned m_max_ops; // cap number of operations used to compute lookahead reward. //scoped_ptr m_ext; // --------------------------------------- @@ -510,6 +511,7 @@ namespace sat { void propagate_binary(literal l); void propagate(); literal choose(); + literal choose_base(); void compute_lookahead_reward(); literal select_literal(); void update_binary_clause_reward(literal l1, literal l2); @@ -605,6 +607,13 @@ namespace sat { std::ostream& display(std::ostream& out) const; std::ostream& display_summary(std::ostream& out) const; + + /** + \brief display lookahead scores as a sequence of: + \n + */ + void display_lookahead_scores(std::ostream& out); + model const& get_model(); void collect_statistics(statistics& st) const; @@ -612,6 +621,12 @@ namespace sat { double literal_occs(literal l); double literal_big_occs(literal l); + /** + \brief retrieve clauses as one vector of literals. + clauses are separated by null-literal + */ + void get_clauses(literal_vector& clauses, unsigned max_clause_size); + sat::config const& get_config() const { return m_s.get_config(); } }; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index c66552ac5..c783f4636 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -16,10 +16,9 @@ Author: Revision History: --*/ -#include "sat_parallel.h" -#include "sat_clause.h" -#include "sat_solver.h" - +#include "sat/sat_parallel.h" +#include "sat/sat_clause.h" +#include "sat/sat_solver.h" namespace sat { @@ -205,27 +204,7 @@ namespace sat { return (c.size() <= 40 && c.glue() <= 8) || c.glue() <= 2; } - void parallel::_set_phase(solver& s) { - if (!m_phase.empty()) { - m_phase.reserve(s.num_vars(), l_undef); - for (unsigned i = 0; i < s.num_vars(); ++i) { - if (s.value(i) != l_undef) { - m_phase[i] = s.value(i); - continue; - } - switch (s.m_phase[i]) { - case POS_PHASE: - m_phase[i] = l_true; - break; - case NEG_PHASE: - m_phase[i] = l_false; - break; - default: - m_phase[i] = l_undef; - break; - } - } - } + void parallel::_from_solver(solver& s) { if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) { // time to update local search with new clauses. // there could be multiple local search engines running at the same time. @@ -236,47 +215,53 @@ namespace sat { } } - void parallel::set_phase(solver& s) { - std::lock_guard lock(m_mux); - _set_phase(s); + + bool parallel::_to_solver(solver& s) { + if (m_priorities.empty()) { + return false; + } + for (bool_var v = 0; v < m_priorities.size(); ++v) { + s.update_activity(v, m_priorities[v]); + } + return true; } - void parallel::get_phase(solver& s) { + void parallel::from_solver(solver& s) { std::lock_guard lock(m_mux); - _get_phase(s); + _from_solver(s); } - void parallel::_get_phase(solver& s) { - if (!m_phase.empty()) { - m_phase.reserve(s.num_vars(), l_undef); - for (unsigned i = 0; i < s.num_vars(); ++i) { - switch (m_phase[i]) { - case l_false: s.m_phase[i] = NEG_PHASE; break; - case l_true: s.m_phase[i] = POS_PHASE; break; - default: break; - } - } + bool parallel::to_solver(solver& s) { + std::lock_guard lock(m_mux); + return _to_solver(s); + } + + void parallel::_to_solver(i_local_search& s) { + m_priorities.reset(); + for (bool_var v = 0; m_solver_copy && v < m_solver_copy->num_vars(); ++v) { + m_priorities.push_back(s.get_priority(v)); } } - bool parallel::get_phase(local_search& s) { + bool parallel::_from_solver(i_local_search& s) { bool copied = false; - { - std::lock_guard lock(m_mux); - m_consumer_ready = true; - if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) { - copied = true; - s.import(*m_solver_copy.get(), true); - } - 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_consumer_ready = true; + if (m_solver_copy) { + copied = true; + s.reinit(*m_solver_copy.get()); } return copied; } + bool parallel::from_solver(i_local_search& s) { + std::lock_guard lock(m_mux); + return _from_solver(s); + } + + void parallel::to_solver(i_local_search& s) { + std::lock_guard lock(m_mux); + _to_solver(s); + } bool parallel::copy_solver(solver& s) { bool copied = false; diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index a55cc17da..34116a111 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -28,8 +28,6 @@ Revision History: namespace sat { - class local_search; - class parallel { // shared pool of learned clauses. @@ -54,8 +52,10 @@ namespace sat { bool enable_add(clause const& c) const; void _get_clauses(solver& s); - void _get_phase(solver& s); - void _set_phase(solver& s); + void _from_solver(solver& s); + bool _to_solver(solver& s); + bool _from_solver(i_local_search& s); + void _to_solver(i_local_search& s); typedef hashtable index_set; literal_vector m_units; @@ -65,10 +65,10 @@ namespace sat { std::mutex m_mux; // for exchange with local search: - svector m_phase; unsigned m_num_clauses; scoped_ptr m_solver_copy; bool m_consumer_ready; + svector m_priorities; scoped_limits m_scoped_rlimit; vector m_limits; @@ -102,13 +102,13 @@ namespace sat { // receive clauses from shared clause pool void get_clauses(solver& s); - // exchange phase of variables. - void set_phase(solver& s); - - void get_phase(solver& s); + // exchange from solver state to local search and back. + void from_solver(solver& s); + bool to_solver(solver& s); + + bool from_solver(i_local_search& s); + void to_solver(i_local_search& s); - bool get_phase(local_search& s); - bool copy_solver(solver& s); }; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 178132f63..59738db5c 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -2,10 +2,11 @@ def_module_params('sat', export=True, description='propositional SAT solver', params=(max_memory_param(), - ('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, caching, random'), - ('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'), - ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'), - ('phase.sticky', BOOL, False, 'use sticky phase caching for local search'), + ('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, basic_caching, random, caching'), + ('phase.sticky', BOOL, True, 'use sticky phase caching'), + ('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'), + ('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'), + ('rephase.base', UINT, 1000, 'number of conflicts per rephase '), ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'), ('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'), ('restart.initial', UINT, 2, 'initial restart (number of conflicts)'), @@ -36,6 +37,8 @@ def_module_params('sat', ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('core.minimize', BOOL, False, 'minimize computed core'), ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), + ('backtrack.scopes', UINT, 100, 'number of scopes to enable chronological backtracking'), + ('backtrack.conflicts', UINT, 4000, 'number of conflicts before enabling chronological backtracking'), ('threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), @@ -48,12 +51,20 @@ def_module_params('sat', ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'), ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'), ('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'), + ('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'), + ('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'), + ('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'), + ('ddfw.restart_base', UINT, 100000, 'number of flips used a starting point for hessitant restart backoff'), + ('ddfw.reinit_base', UINT, 10000, 'increment basis for geometric backoff scheme of re-initialization of weights'), + ('ddfw.threads', UINT, 0, 'number of ddfw threads to run in parallel with sat solver'), + ('prob_search', BOOL, False, 'use probsat local search instead of CDCL'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), ('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'), ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), + ('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. # So if the value is 10, at most 1024 cubes will be generated of length 10. @@ -64,6 +75,7 @@ def_module_params('sat', # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables # at the time of the last conflict. The fraction is increased every time the cutoff is created. # - adative_psat: Cut based on psat_heur in an adaptive way. + ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'), @@ -72,6 +84,7 @@ def_module_params('sat', ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), + ('lookahead_scores', BOOL, False, 'extract lookahead scores. A utility that can only be used from the DIMACS front-end'), ('lookahead.double', BOOL, True, 'enable doubld lookahead'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), diff --git a/src/sat/sat_prob.cpp b/src/sat/sat_prob.cpp new file mode 100644 index 000000000..b56316f81 --- /dev/null +++ b/src/sat/sat_prob.cpp @@ -0,0 +1,296 @@ +/*++ + Copyright (c) 2019 Microsoft Corporation + + Module Name: + + sat_prob.cpp + + Abstract: + + PROB Local search module for clauses + + Author: + + Nikolaj Bjorner 2019-4-23 + + Notes: + + --*/ + +#include "sat/sat_prob.h" +#include "sat/sat_solver.h" +#include "util/luby.h" + +namespace sat { + + prob::~prob() { + for (clause* cp : m_clause_db) { + m_alloc.del_clause(cp); + } + } + + lbool prob::check(unsigned n, literal const* assumptions, parallel* p) { + VERIFY(n == 0); + init(); + while (m_limit.inc() && m_best_min_unsat > 0) { + if (should_restart()) do_restart(); + else flip(); + } + if (m_best_min_unsat == 0) { + return l_true; + } + return l_undef; + } + + void prob::flip() { + bool_var v = pick_var(); + flip(v); + if (m_unsat.size() < m_best_min_unsat) { + save_best_values(); + } + } + + bool_var prob::pick_var() { + unsigned cls_idx = m_unsat.elem_at(m_rand() % m_unsat.size()); + double sum_prob = 0; + unsigned i = 0; + clause const& c = get_clause(cls_idx); + for (literal lit : c) { + double prob = m_prob_break[m_breaks[lit.var()]]; + m_probs[i++] = prob; + sum_prob += prob; + } + double lim = sum_prob * ((double)m_rand() / m_rand.max_value()); + do { + lim -= m_probs[--i]; + } + while (lim >= 0 && i > 0); + return c[i].var(); + } + + void prob::flip(bool_var v) { + ++m_flips; + literal lit = literal(v, !m_values[v]); + literal nlit = ~lit; + SASSERT(is_true(lit)); + for (unsigned cls_idx : use_list(*this, lit)) { + clause_info& ci = m_clauses[cls_idx]; + ci.del(lit); + switch (ci.m_num_trues) { + case 0: + m_unsat.insert(cls_idx); + dec_break(lit); + break; + case 1: + inc_break(to_literal(ci.m_trues)); + break; + default: + break; + } + } + for (unsigned cls_idx : use_list(*this, nlit)) { + clause_info& ci = m_clauses[cls_idx]; + switch (ci.m_num_trues) { + case 0: + m_unsat.remove(cls_idx); + inc_break(nlit); + break; + case 1: + dec_break(to_literal(ci.m_trues)); + break; + default: + break; + } + ci.add(nlit); + } + m_values[v] = !m_values[v]; + } + + void prob::add(unsigned n, literal const* c) { + clause* cls = m_alloc.mk_clause(n, c, false); + unsigned idx = m_clause_db.size(); + m_clause_db.push_back(cls); + m_clauses.push_back(clause_info()); + for (literal lit : *cls) { + m_values.reserve(lit.var()+1); + m_breaks.reserve(lit.var()+1); + m_use_list.reserve(lit.index()+1); + m_use_list[lit.index()].push_back(idx); + } + m_probs.reserve(n+1); + } + + void prob::add(solver const& s) { + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + add(1, s.m_trail.c_ptr() + i); + } + unsigned sz = s.m_watches.size(); + for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { + literal l1 = ~to_literal(l_idx); + watch_list const & wlist = s.m_watches[l_idx]; + for (watched const& w : wlist) { + if (!w.is_binary_non_learned_clause()) + continue; + literal l2 = w.get_literal(); + if (l1.index() > l2.index()) + continue; + literal ls[2] = { l1, l2 }; + add(2, ls); + } + } + for (clause* c : s.m_clauses) { + add(c->size(), c->begin()); + } + } + + void prob::save_best_values() { + m_best_min_unsat = m_unsat.size(); + m_best_values.reserve(m_values.size()); + m_model.reserve(m_values.size()); + for (unsigned i = 0; i < m_values.size(); ++i) { + m_best_values[i] = m_values[i]; + m_model[i] = to_lbool(m_values[i]); + } + } + + void prob::flatten_use_list() { + m_use_list_index.reset(); + m_flat_use_list.reset(); + for (auto const& ul : m_use_list) { + m_use_list_index.push_back(m_flat_use_list.size()); + m_flat_use_list.append(ul); + } + m_use_list_index.push_back(m_flat_use_list.size()); + } + + void prob::init_clauses() { + for (unsigned& b : m_breaks) { + b = 0; + } + m_unsat.reset(); + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause_info& ci = m_clauses[i]; + ci.m_num_trues = 0; + ci.m_trues = 0; + clause const& c = get_clause(i); + for (literal lit : c) { + if (is_true(lit)) { + ci.add(lit); + } + } + switch (ci.m_num_trues) { + case 0: + m_unsat.insert(i); + break; + case 1: + inc_break(to_literal(ci.m_trues)); + break; + default: + break; + } + } + } + + void prob::auto_config() { + unsigned max_len = 0; + for (clause* cp : m_clause_db) { + max_len = std::max(max_len, cp->size()); + } + // ProbSat magic constants + switch (max_len) { + case 0: case 1: case 2: case 3: m_config.m_cb = 2.5; break; + case 4: m_config.m_cb = 2.85; break; + case 5: m_config.m_cb = 3.7; break; + case 6: m_config.m_cb = 5.1; break; + default: m_config.m_cb = 5.4; break; + } + + unsigned max_num_occ = 0; + for (auto const& ul : m_use_list) { + max_num_occ = std::max(max_num_occ, ul.size()); + } + // vodoo from prob-sat + m_prob_break.reserve(max_num_occ+1); + for (int i = 0; i <= static_cast(max_num_occ); ++i) { + m_prob_break[i] = pow(m_config.m_cb, -i); + } + } + + void prob::log() { + double sec = m_stopwatch.get_current_seconds(); + double kflips_per_sec = m_flips / (1000.0 * sec); + IF_VERBOSE(0, verbose_stream() + << sec << " sec. " + << (m_flips/1000) << " kflips " + << m_best_min_unsat << " unsat " + << kflips_per_sec << " kflips/sec " + << m_restart_count << " restarts\n"); + } + + void prob::init() { + flatten_use_list(); + init_random_values(); + init_clauses(); + auto_config(); + save_best_values(); + m_restart_count = 1; + m_flips = 0; + m_next_restart = m_config.m_restart_offset; + m_stopwatch.start(); + } + + void prob::init_random_values() { + for (unsigned v = 0; v < m_values.size(); ++v) { + m_values[v] = (m_rand() % 2 == 0); + } + } + + void prob::init_best_values() { + for (unsigned v = 0; v < m_values.size(); ++v) { + m_values[v] = m_best_values[v]; + } + } + + void prob::init_near_best_values() { + for (unsigned v = 0; v < m_values.size(); ++v) { + if (m_rand(100) < m_config.m_prob_random_init) { + m_values[v] = !m_best_values[v]; + } + else { + m_values[v] = m_best_values[v]; + } + } + } + + void prob::do_restart() { + reinit_values(); + init_clauses(); + m_next_restart += m_config.m_restart_offset*get_luby(m_restart_count++); + log(); + } + + bool prob::should_restart() { + return m_flips >= m_next_restart; + } + + void prob::reinit_values() { + init_near_best_values(); + } + + std::ostream& prob::display(std::ostream& out) const { + unsigned num_cls = m_clauses.size(); + for (unsigned i = 0; i < num_cls; ++i) { + out << get_clause(i) << " "; + auto const& ci = m_clauses[i]; + out << ci.m_num_trues << "\n"; + } + return out; + } + + void prob::invariant() { + + } + +} + diff --git a/src/sat/sat_prob.h b/src/sat/sat_prob.h new file mode 100644 index 000000000..a2fdbb4e1 --- /dev/null +++ b/src/sat/sat_prob.h @@ -0,0 +1,160 @@ +/*++ + Copyright (c) 2019 Microsoft Corporation + + Module Name: + + sat_prob.h + + Abstract: + + PROB Local search module for clauses + + Author: + + Nikolaj Bjorner 2019-4-23 + + Notes: + + http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf + + --*/ +#ifndef _SAT_PROB_ +#define _SAT_PROB_ + +#include "util/uint_set.h" +#include "util/rlimit.h" +#include "sat/sat_clause.h" +#include "sat/sat_types.h" + +namespace sat { + class solver; + + class prob : public i_local_search { + + struct clause_info { + clause_info(): m_trues(0), m_num_trues(0) {} + unsigned m_trues; // set of literals that are true + unsigned m_num_trues; // size of true set + bool is_true() const { return m_num_trues > 0; } + void add(literal lit) { ++m_num_trues; m_trues += lit.index(); } + void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); } + }; + + struct config { + unsigned m_prob_random_init; + unsigned m_restart_offset; + double m_cb; + double m_eps; + config() { reset(); } + void reset() { + m_prob_random_init = 4; + m_restart_offset = 1000000; + m_cb = 2.85; + m_eps = 0.9; + } + }; + + config m_config; + reslimit m_limit; + clause_allocator m_alloc; + clause_vector m_clause_db; + svector m_clauses; + svector m_values, m_best_values; + unsigned m_best_min_unsat; + vector m_use_list; + unsigned_vector m_flat_use_list; + unsigned_vector m_use_list_index; + svector m_prob_break; + svector m_probs; + indexed_uint_set m_unsat; + random_gen m_rand; + unsigned_vector m_breaks; + uint64_t m_flips; + uint64_t m_next_restart; + unsigned m_restart_count; + stopwatch m_stopwatch; + model m_model; + + class use_list { + prob& p; + unsigned i; + public: + use_list(prob& p, literal lit): + p(p), i(lit.index()) {} + unsigned const* begin() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i]; } + unsigned const* end() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i+1]; } + }; + + void flatten_use_list(); + + bool is_true(literal lit) const { return m_values[lit.var()] != lit.sign(); } + + inline clause const& get_clause(unsigned idx) const { return *m_clause_db[idx]; } + + inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); } + + inline void inc_break(literal lit) { m_breaks[lit.var()]++; } + + inline void dec_break(literal lit) { m_breaks[lit.var()]--; } + + void flip(); + + bool_var pick_var(); + + void flip(bool_var v); + + void reinit_values(); + + void save_best_values(); + + void init(); + + void init_random_values(); + + void init_best_values(); + + void init_near_best_values(); + + void init_clauses(); + + void auto_config(); + + bool should_restart(); + + void do_restart(); + + void invariant(); + + void log(); + + void add(unsigned sz, literal const* c); + + public: + prob() {} + + ~prob() override; + + lbool check(unsigned sz, literal const* assumptions, parallel* p) override; + + void set_seed(unsigned n) override { m_rand.set_seed(n); } + + reslimit& rlimit() override { return m_limit; } + + void add(solver const& s) override; + + model const& get_model() const override { return m_model; } + + std::ostream& display(std::ostream& out) const; + + void updt_params(params_ref const& p) override {} + + unsigned num_non_binary_clauses() const override { return 0; } + + void collect_statistics(statistics& st) const override {} + + void reinit(solver& s) override { UNREACHABLE(); } + + }; +} + +#endif diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 86094d7a3..95d60491c 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -189,7 +189,7 @@ namespace sat { return; if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled()) return; - + initialize(); CASSERT("sat_solver", s.check_invariant()); @@ -352,12 +352,7 @@ namespace sat { s.del_clause(c); break; default: - if (s.m_config.m_drat && sz0 != sz) { - s.m_drat.add(c, true); - c.restore(sz0); - s.m_drat.del(c); - c.shrink(sz); - } + s.shrink(c, sz0, sz); *it2 = *it; it2++; if (!c.frozen()) { @@ -613,7 +608,12 @@ namespace sat { } } if (j < sz && !r) { - c.shrink(j); + if (j > 2) { + s.shrink(c, sz, j); + } + else { + c.shrink(j); + } } return r; } @@ -715,12 +715,6 @@ namespace sat { remove_clause(c, sz0 != sz); break; default: - if (s.m_config.m_drat && sz0 != sz) { - s.m_drat.add(c, true); - c.restore(sz0); - s.m_drat.del(c); - c.shrink(sz); - } TRACE("elim_lit", tout << "result: " << c << "\n";); m_sub_todo.insert(c); break; @@ -911,12 +905,6 @@ namespace sat { remove_clause(c, sz != sz0); continue; default: - if (s.m_config.m_drat && sz != sz0) { - s.m_drat.add(c, true); - c.restore(sz0); - s.m_drat.del(c); - c.shrink(sz); - } break; } } @@ -1981,7 +1969,7 @@ namespace sat { model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); save_clauses(mc_entry, m_neg_cls); - s.m_eliminated[v] = true; + s.set_eliminated(v, true); m_elim_counter -= num_pos * num_neg + before_lits; for (auto & c1 : m_pos_cls) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8a5da7531..357c4f5ca 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -20,20 +20,22 @@ Revision History: #include #include -#include "sat/sat_solver.h" -#include "sat/sat_integrity_checker.h" -#include "sat/sat_lookahead.h" -#include "sat/sat_unit_walk.h" #include "util/luby.h" #include "util/trace.h" #include "util/max_cliques.h" #include "util/gparams.h" +#include "sat/sat_solver.h" +#include "sat/sat_integrity_checker.h" +#include "sat/sat_lookahead.h" +#include "sat/sat_unit_walk.h" +#include "sat/sat_ddfw.h" +#include "sat/sat_prob.h" #ifdef _MSC_VER # include #endif -// define to update glue during propagation -#define UPDATE_GLUE +#define ENABLE_TERNARY true + namespace sat { @@ -53,6 +55,7 @@ namespace sat { m_mus(*this), m_inconsistent(false), m_searching(false), + m_conflict(justification(0)), m_num_frozen(0), m_activity_inc(128), m_case_split_queue(m_activity), @@ -61,6 +64,9 @@ namespace sat { m_search_lvl(0), m_fast_glue_avg(), m_slow_glue_avg(), + m_fast_glue_backup(), + m_slow_glue_backup(), + m_trail_avg(), m_params(p), m_par_id(0), m_par_syncing_clauses(false) { @@ -71,6 +77,7 @@ namespace sat { m_next_simplify = 0; m_num_checkpoints = 0; m_simplifications = 0; + m_touch_index = 0; m_ext = nullptr; m_cuber = nullptr; m_local_search = nullptr; @@ -110,9 +117,9 @@ namespace sat { m_decision.reset(); m_eliminated.reset(); m_activity.reset(); - m_level.reset(); m_mark.reset(); m_lit_mark.reset(); + m_best_phase.reset(); m_phase.reset(); m_prev_phase.reset(); m_assigned_since_gc.reset(); @@ -137,9 +144,10 @@ namespace sat { bool dvar = src.m_decision[v] != 0; VERIFY(v == mk_var(ext, dvar)); if (src.was_eliminated(v)) { - m_eliminated[v] = true; + set_eliminated(v, true); } m_phase[v] = src.m_phase[v]; + m_best_phase[v] = src.m_best_phase[v]; m_prev_phase[v] = src.m_prev_phase[v]; // inherit activity: @@ -208,6 +216,12 @@ namespace sat { } IF_VERBOSE(2, verbose_stream() << "(sat.copy :learned " << num_learned << ")\n";); } + m_best_phase_size = src.m_best_phase_size; + if (m_best_phase_size > 0) { + for (bool_var v = 0; v < num_vars(); ++v) { + m_best_phase[v] = src.m_best_phase[v]; + } + } m_user_scope_literals.reset(); m_user_scope_literals.append(src.m_user_scope_literals); @@ -225,22 +239,23 @@ namespace sat { bool_var solver::mk_var(bool ext, bool dvar) { m_model_is_current = false; m_stats.m_mk_var++; - bool_var v = m_level.size(); + bool_var v = m_justification.size(); m_watches.push_back(watch_list()); m_watches.push_back(watch_list()); m_assignment.push_back(l_undef); m_assignment.push_back(l_undef); - m_justification.push_back(justification()); + m_justification.push_back(justification(UINT_MAX)); m_decision.push_back(dvar); m_eliminated.push_back(false); m_external.push_back(ext); + m_touched.push_back(0); m_activity.push_back(0); - m_level.push_back(UINT_MAX); m_mark.push_back(false); m_lit_mark.push_back(false); m_lit_mark.push_back(false); - m_phase.push_back(PHASE_NOT_AVAILABLE); - m_prev_phase.push_back(PHASE_NOT_AVAILABLE); + m_phase.push_back(false); + m_best_phase.push_back(false); + m_prev_phase.push_back(false); m_assigned_since_gc.push_back(false); m_last_conflict.push_back(0); m_last_propagation.push_back(0); @@ -254,12 +269,12 @@ namespace sat { } void solver::set_non_external(bool_var v) { - m_external[v] = 0; + m_external[v] = false; } void solver::set_external(bool_var v) { if (m_external[v] != 0) return; - m_external[v] = 1; + m_external[v] = true; if (!m_ext) return; lbool val = value(v); @@ -278,6 +293,11 @@ namespace sat { } } + void solver::set_eliminated(bool_var v, bool f) { + m_eliminated[v] = f; + } + + clause* solver::mk_clause(unsigned num_lits, literal * lits, bool learned) { m_model_is_current = false; DEBUG_CODE({ @@ -316,7 +336,7 @@ namespace sat { if (!c.was_removed() && m_config.m_drat && !m_drat.is_cleaned(c)) { m_drat.del(c); } - dealloc_clause(&c); + dealloc_clause(&c); if (m_searching) m_stats.m_del_clause++; } @@ -351,32 +371,38 @@ namespace sat { if (learned && m_par) m_par->share_clause(*this, lits[0], lits[1]); return nullptr; case 3: - return mk_ter_clause(lits, learned); + if (ENABLE_TERNARY) { + return mk_ter_clause(lits, learned); + } default: return mk_nary_clause(num_lits, lits, learned); } } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { + m_touched[l1.var()] = m_touch_index; + m_touched[l2.var()] = m_touch_index; + if (find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) { - assign_core(l1, 0, justification(l2)); + assign_unit(l1); return; } if (find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) { - assign_core(l2, 0, justification(l1)); + assign_unit(l2); return; } watched* w0 = find_binary_watch(get_wlist(~l1), l2); if (w0) { + TRACE("sat", tout << "found binary " << l1 << " " << l2 << "\n";); if (w0->is_learned() && !learned) { w0->set_learned(false); + w0 = find_binary_watch(get_wlist(~l2), l1); + VERIFY(w0); + w0->set_learned(false); } - else { - return; + if (propagate_bin_clause(l1, l2) && !learned && !at_base_lvl() && !at_search_lvl()) { + m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); } - w0 = find_binary_watch(get_wlist(~l2), l1); - VERIFY(w0); - w0->set_learned(false); return; } if (m_config.m_drat) @@ -394,13 +420,21 @@ namespace sat { bool solver::propagate_bin_clause(literal l1, literal l2) { if (value(l2) == l_false) { - m_stats.m_bin_propagate++; - assign(l1, justification(l2)); + if (value(l1) == l_false) { + TRACE("sat", tout << "conflict " << l1 << " " << l2 << "\n";); + set_conflict(justification(std::max(lvl(l1), lvl(l2)), l1, l2)); + } + else { + m_stats.m_bin_propagate++; + //TRACE("sat", tout << "propagate " << l1 << " <- " << ~l2 << "\n";); + assign(l1, justification(lvl(l2), l2)); + } return true; } else if (value(l1) == l_false) { m_stats.m_bin_propagate++; - assign(l2, justification(l1)); + //TRACE("sat", tout << "propagate " << l2 << " <- " << ~l1 << "\n";); + assign(l2, justification(lvl(l1), l1) ); return true; } return false; @@ -414,6 +448,7 @@ namespace sat { clause * solver::mk_ter_clause(literal * lits, bool learned) { + VERIFY(ENABLE_TERNARY); m_stats.m_mk_ter_clause++; clause * r = alloc_clause(3, lits, learned); bool reinit = attach_ter_clause(*r); @@ -422,10 +457,14 @@ namespace sat { m_learned.push_back(r); else m_clauses.push_back(r); + for (literal l : *r) { + m_touched[l.var()] = m_touch_index; + } return r; } bool solver::attach_ter_clause(clause & c) { + VERIFY(ENABLE_TERNARY); bool reinit = false; if (m_config.m_drat) m_drat.add(c, c.is_learned()); TRACE("sat", tout << c << "\n";); @@ -436,17 +475,17 @@ namespace sat { if (!at_base_lvl()) { if (value(c[1]) == l_false && value(c[2]) == l_false) { m_stats.m_ter_propagate++; - assign(c[0], justification(c[1], c[2])); + assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2])); reinit = true; } else if (value(c[0]) == l_false && value(c[2]) == l_false) { m_stats.m_ter_propagate++; - assign(c[1], justification(c[0], c[2])); + assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2])); reinit = true; } else if (value(c[0]) == l_false && value(c[1]) == l_false) { m_stats.m_ter_propagate++; - assign(c[2], justification(c[0], c[1])); + assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1])); reinit = true; } } @@ -468,6 +507,9 @@ namespace sat { if (m_config.m_drat) { m_drat.add(*r, learned); } + for (literal l : *r) { + m_touched[l.var()] = m_touch_index; + } return r; } @@ -487,13 +529,21 @@ namespace sat { } if (value(c[0]) == l_false) { - m_stats.m_propagate++; - assign(c[1], justification(cls_off)); + m_stats.m_propagate++; + unsigned level = lvl(c[0]); + for (unsigned i = c.size(); i-- > 2; ) { + level = std::max(level, lvl(c[i])); + } + assign(c[1], justification(level, cls_off)); reinit = true; } else if (value(c[1]) == l_false) { m_stats.m_propagate++; - assign(c[0], justification(cls_off)); + unsigned level = lvl(c[1]); + for (unsigned i = c.size(); i-- > 2; ) { + level = std::max(level, lvl(c[i])); + } + assign(c[0], justification(level, cls_off)); reinit = true; } } @@ -511,7 +561,7 @@ namespace sat { void solver::attach_clause(clause & c, bool & reinit) { SASSERT(c.size() > 2); reinit = false; - if (c.size() == 3) + if (ENABLE_TERNARY && c.size() == 3) reinit = attach_ter_clause(c); else reinit = attach_nary_clause(c); @@ -531,6 +581,23 @@ namespace sat { } } + void solver::shrink(clause& c, unsigned old_sz, unsigned new_sz) { + SASSERT(new_sz > 2); + SASSERT(old_sz >= new_sz); + if (old_sz != new_sz) { + c.shrink(new_sz); + for (literal l : c) { + m_touched[l.var()] = m_touch_index; + } + if (m_config.m_drat) { + m_drat.add(c, true); + c.restore(old_sz); + m_drat.del(c); + c.shrink(new_sz); + } + } + } + bool solver::memory_pressure() { return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size(); } @@ -744,7 +811,7 @@ namespace sat { } void solver::detach_clause(clause & c) { - if (c.size() == 3) + if (ENABLE_TERNARY && c.size() == 3) detach_ter_clause(c); else detach_nary_clause(c); @@ -776,22 +843,21 @@ namespace sat { m_not_l = not_l; } - void solver::assign_core(literal l, unsigned _lvl, justification j) { + void solver::assign_core(literal l, justification j) { SASSERT(value(l) == l_undef); - TRACE("sat_assign_core", tout << l << " " << j << " level: " << _lvl << "\n";); - if (_lvl == 0 && m_config.m_drat) { - m_drat.add(l, !j.is_none()); + TRACE("sat_assign_core", tout << l << " " << j << "\n";); + if (j.level() == 0) { + if (m_config.m_drat) m_drat.add(l, m_searching); + j = justification(0); // erase justification for level 0 } - - if (at_base_lvl()) { - j = justification(); // erase justification for level 0 + else { + VERIFY(!at_base_lvl()); } m_assignment[l.index()] = l_true; m_assignment[(~l).index()] = l_false; bool_var v = l.var(); - m_level[v] = scope_lvl(); m_justification[v] = j; - m_phase[v] = static_cast(l.sign()); + m_phase[v] = !l.sign(); m_assigned_since_gc[v] = true; m_trail.push_back(l); @@ -829,8 +895,8 @@ namespace sat { #endif } - SASSERT(!l.sign() || m_phase[v] == NEG_PHASE); - SASSERT(l.sign() || m_phase[v] == POS_PHASE); + SASSERT(!l.sign() || !m_phase[v]); + SASSERT(l.sign() || m_phase[v]); SASSERT(!l.sign() || value(v) == l_false); SASSERT(l.sign() || value(v) == l_true); SASSERT(value(l) == l_true); @@ -870,7 +936,8 @@ namespace sat { m_cleaner.dec(); if (m_inconsistent) return false; l = m_trail[m_qhead]; - TRACE("sat_propagate", tout << "propagating: " << l << " " << m_justification[l.var()] << "\n";); + unsigned curr_level = lvl(l); + TRACE("sat_propagate", tout << "propagating: " << l << " " << m_justification[l.var()] << "\n"; ); m_qhead++; not_l = ~l; SASSERT(value(l) == l_true); @@ -893,11 +960,11 @@ namespace sat { switch (value(l1)) { case l_false: CONFLICT_CLEANUP(); - set_conflict(justification(not_l), ~l1); + set_conflict(justification(curr_level, not_l), ~l1); return false; case l_undef: m_stats.m_bin_propagate++; - assign_core(l1, scope_lvl(), justification(not_l)); + assign_core(l1, justification(curr_level, not_l)); break; case l_true: break; // skip @@ -912,15 +979,15 @@ namespace sat { val2 = value(l2); if (val1 == l_false && val2 == l_undef) { m_stats.m_ter_propagate++; - assign_core(l2, scope_lvl(), justification(l1, not_l)); + assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l)); } else if (val1 == l_undef && val2 == l_false) { m_stats.m_ter_propagate++; - assign_core(l1, scope_lvl(), justification(l2, not_l)); + assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l)); } else if (val1 == l_false && val2 == l_false) { CONFLICT_CLEANUP(); - set_conflict(justification(l1, not_l), ~l2); + set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2); return false; } *it2 = *it; @@ -958,6 +1025,8 @@ namespace sat { VERIFY(c[1] == not_l); literal * l_it = c.begin() + 2; literal * l_end = c.end(); + unsigned assign_level = curr_level; + unsigned max_index = 1; for (; l_it != l_end; ++l_it) { if (value(*l_it) != l_false) { c[1] = *l_it; @@ -968,26 +1037,43 @@ namespace sat { } } SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef); + if (assign_level != scope_lvl()) { + for (unsigned i = 2; i < c.size(); ++i) { + unsigned level = lvl(c[i]); + if (level > assign_level) { + assign_level = level; + max_index = i; + } + } + IF_VERBOSE(20, verbose_stream() << "lower assignment level " << assign_level << " scope: " << scope_lvl() << "\n"); + } + if (value(c[0]) == l_false) { + assign_level = std::max(assign_level, lvl(c[0])); c.mark_used(); CONFLICT_CLEANUP(); - set_conflict(justification(cls_off)); + set_conflict(justification(assign_level, cls_off)); return false; } else { - *it2 = *it; - it2++; + if (max_index != 1) { + IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n"); + std::swap(c[1], c[max_index]); + m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); + } + else { + *it2 = *it; + it2++; + } m_stats.m_propagate++; c.mark_used(); - assign_core(c[0], scope_lvl(), justification(cls_off)); -#ifdef UPDATE_GLUE + assign_core(c[0], justification(assign_level, cls_off)); if (update && c.is_learned() && c.glue() > 2) { unsigned glue; if (num_diff_levels_below(c.size(), c.begin(), c.glue()-1, glue)) { c.set_glue(glue); } } -#endif } end_clause_case: break; @@ -1030,6 +1116,11 @@ namespace sat { return r; } + void solver::display_lookahead_scores(std::ostream& out) { + lookahead lh(*this); + lh.display_lookahead_scores(out); + } + lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) { bool is_first = !m_cuber; if (is_first) { @@ -1057,7 +1148,7 @@ namespace sat { literal l(v, false); if (mdl[v] != l_true) l.neg(); push(); - assign_core(l, scope_lvl(), justification()); + assign_core(l, justification(scope_lvl())); } mk_model(); break; @@ -1081,10 +1172,19 @@ namespace sat { IF_VERBOSE(2, verbose_stream() << "(sat.solver)\n";); SASSERT(at_base_lvl()); + if (m_config.m_ddfw_search) { + m_cleaner(true); + return do_ddfw_search(num_lits, lits); + } + if (m_config.m_prob_search) { + m_cleaner(true); + return do_prob_search(num_lits, lits); + } if (m_config.m_local_search) { + m_cleaner(true); return do_local_search(num_lits, lits); } - if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) { + if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || m_config.m_ddfw_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) { SASSERT(scope_lvl() == 0); return check_par(num_lits, lits); } @@ -1092,6 +1192,7 @@ namespace sat { if (m_mc.empty() && gparams::get_ref().get_bool("model_validate", false)) { m_clone = alloc(solver, m_params, m_rlimit); m_clone->copy(*this); + m_clone->set_extension(nullptr); } try { init_search(); @@ -1101,16 +1202,18 @@ namespace sat { init_assumptions(num_lits, lits); propagate(false); if (check_inconsistent()) return l_false; - cleanup(m_config.m_force_cleanup); + do_cleanup(m_config.m_force_cleanup); if (m_config.m_unit_walk) { return do_unit_walk(); } + if (m_config.m_gc_burst) { // force gc m_conflicts_since_gc = m_gc_threshold + 1; - gc(); + do_gc(); } + if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) { m_restart_threshold = m_config.m_burst_search; lbool r = bounded_search(); @@ -1120,47 +1223,18 @@ namespace sat { m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; } - - if (reached_max_conflicts()) { - return l_undef; - } - - // iff3_finder(*this)(); - simplify_problem(); - if (check_inconsistent()) return l_false; - - if (reached_max_conflicts()) { - return l_undef; - } - - while (true) { - SASSERT(!inconsistent()); - - lbool r = bounded_search(); - if (r != l_undef) - return r; - - if (reached_max_conflicts()) { - return l_undef; - } - - restart(!m_config.m_restart_fast); - simplify_problem(); - if (check_inconsistent()) return l_false; - gc(); - - if (m_config.m_restart_max <= m_restarts) { - m_reason_unknown = "sat.max.restarts"; - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); - return l_undef; - } - if (m_config.m_inprocess_max <= m_simplifications) { - m_reason_unknown = "sat.max.inprocess"; - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";); - return l_undef; - } - + lbool is_sat = l_undef; + while (is_sat == l_undef && !should_cancel()) { + if (inconsistent()) is_sat = resolve_conflict_core(); + else if (should_propagate()) propagate(true); + else if (do_cleanup(false)) continue; + else if (should_gc()) do_gc(); + else if (should_rephase()) do_rephase(); + else if (should_restart()) do_restart(!m_config.m_restart_fast); + else if (should_simplify()) do_simplify(); + else if (!decide()) is_sat = final_check(); } + return is_sat; } catch (const abort_solver &) { m_reason_unknown = "sat.giveup"; @@ -1169,25 +1243,66 @@ namespace sat { } } + bool solver::should_cancel() { + if (limit_reached() || memory_exceeded()) { + return true; + } + if (m_config.m_restart_max <= m_restarts) { + m_reason_unknown = "sat.max.restarts"; + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); + return true; + } + if (m_config.m_inprocess_max <= m_simplifications) { + m_reason_unknown = "sat.max.inprocess"; + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";); + return true; + } + if (reached_max_conflicts()) { + return true; + } + return false; + } + enum par_exception_kind { DEFAULT_EX, ERROR_EX }; - lbool solver::do_local_search(unsigned num_lits, literal const* lits) { + lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) { scoped_limits scoped_rl(rlimit()); - SASSERT(!m_local_search); - m_local_search = alloc(local_search); - local_search& srch = *m_local_search; - srch.import(*this, false); + SASSERT(m_local_search); + i_local_search& srch = *m_local_search; + srch.add(*this); scoped_rl.push_child(&srch.rlimit()); lbool r = srch.check(num_lits, lits, nullptr); - m_model = srch.get_model(); + if (r == l_true) { + m_model = srch.get_model(); + } m_local_search = nullptr; dealloc(&srch); return r; } + lbool solver::do_local_search(unsigned num_lits, literal const* lits) { + SASSERT(!m_local_search); + m_local_search = alloc(local_search); + return invoke_local_search(num_lits, lits); + } + + lbool solver::do_ddfw_search(unsigned num_lits, literal const* lits) { + if (m_ext) return l_undef; + SASSERT(!m_local_search); + m_local_search = alloc(ddfw); + return invoke_local_search(num_lits, lits); + } + + lbool solver::do_prob_search(unsigned num_lits, literal const* lits) { + if (m_ext) return l_undef; + SASSERT(!m_local_search); + m_local_search = alloc(prob); + return invoke_local_search(num_lits, lits); + } + lbool solver::do_unit_walk() { unit_walk srch(*this); lbool r = srch(); @@ -1195,21 +1310,31 @@ namespace sat { } lbool solver::check_par(unsigned num_lits, literal const* lits) { - scoped_ptr_vector ls; + scoped_ptr_vector ls; scoped_ptr_vector uw; int num_extra_solvers = m_config.m_num_threads - 1; int num_local_search = static_cast(m_config.m_local_search_threads); int num_unit_walk = static_cast(m_config.m_unit_walk_threads); - int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk; + int num_ddfw = m_ext ? 0 : static_cast(m_config.m_ddfw_threads); + int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk + num_ddfw; for (int i = 0; i < num_local_search; ++i) { local_search* l = alloc(local_search); - l->import(*this, false); - l->config().set_random_seed(m_config.m_random_seed + i); + l->updt_params(m_params); + l->add(*this); + l->set_seed(m_config.m_random_seed + i); ls.push_back(l); } + // set up ddfw search + for (int i = 0; i < num_ddfw; ++i) { + ddfw* d = alloc(ddfw); + d->updt_params(m_params); + d->set_seed(m_config.m_random_seed + i); + d->add(*this); + ls.push_back(d); + } // set up unit walk - vector lims(num_unit_walk); + vector lims(num_unit_walk + num_ddfw); for (int i = 0; i < num_unit_walk; ++i) { solver* s = alloc(solver, m_params, lims[i]); s->copy(*this); @@ -1218,7 +1343,7 @@ namespace sat { } int local_search_offset = num_extra_solvers; - int unit_walk_offset = num_extra_solvers + num_local_search; + int unit_walk_offset = num_extra_solvers + num_local_search + num_ddfw; int main_solver_offset = unit_walk_offset + num_unit_walk; #define IS_AUX_SOLVER(i) (0 <= i && i < num_extra_solvers) @@ -1421,36 +1546,39 @@ namespace sat { return false; push(); m_stats.m_decision++; - lbool phase = m_ext ? m_ext->get_phase(next) : l_undef; + lbool lphase = m_ext ? m_ext->get_phase(next) : l_undef; + bool phase = lphase == l_true; - if (phase == l_undef) { + if (lphase == l_undef) { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: - phase = l_true; + phase = true; break; case PS_ALWAYS_FALSE: - phase = l_false; + phase = false; break; - case PS_CACHING: - if ((m_phase_cache_on || m_config.m_phase_sticky) && m_phase[next] != PHASE_NOT_AVAILABLE) { - phase = m_phase[next] == POS_PHASE ? l_true : l_false; + case PS_BASIC_CACHING: + phase = m_phase[next]; + break; + case PS_SAT_CACHING: + if (m_search_state == s_unsat) { + phase = m_phase[next]; } else { - phase = l_false; + phase = m_best_phase[next]; } break; case PS_RANDOM: - phase = to_lbool((m_rand() % 2) == 0); + phase = (m_rand() % 2) == 0; break; default: UNREACHABLE(); - phase = l_false; + phase = false; break; } } - SASSERT(phase != l_undef); - literal next_lit(next, phase == l_false); + literal next_lit(next, !phase); TRACE("sat_decide", tout << scope_lvl() << ": next-case-split: " << next_lit << "\n";); assign_scoped(next_lit); return true; @@ -1465,7 +1593,8 @@ namespace sat { if (is_sat != l_true) return is_sat; } - gc(); + SASSERT(!inconsistent()); + do_gc(); if (!decide()) { lbool is_sat = final_check(); @@ -1476,6 +1605,11 @@ namespace sat { } } + bool solver::should_propagate() const { + return !inconsistent() && m_qhead < m_trail.size(); + } + + lbool solver::propagate_and_backjump_step(bool& done) { done = true; propagate(true); @@ -1486,13 +1620,15 @@ namespace sat { return l_false; if (reached_max_conflicts()) return l_undef; + if (should_rephase()) + do_rephase(); if (at_base_lvl()) { - cleanup(false); // cleaner may propagate frozen clauses + do_cleanup(false); // cleaner may propagate frozen clauses if (inconsistent()) { TRACE("sat", tout << "conflict at level 0\n";); return l_false; } - gc(); + do_gc(); } done = false; return l_true; @@ -1527,7 +1663,14 @@ namespace sat { else { return false; } - } + } + + + struct clause_size_lt { + bool operator()(clause const * c1, clause const * c2) const { + return c1->size() < c2->size(); + } + }; void solver::init_assumptions(unsigned num_lits, literal const* lits) { if (num_lits == 0 && m_user_scope_literals.empty()) { @@ -1607,7 +1750,7 @@ namespace sat { void solver::reinit_assumptions() { if (tracking_assumptions() && at_base_lvl() && !inconsistent()) { - TRACE("sat", tout << m_assumptions << "\n";); + TRACE("sat", tout << "assumptions: " << m_assumptions << " user scopes: " << m_user_scope_literals << "\n";); if (!propagate(false)) return; push(); for (literal lit : m_user_scope_literals) { @@ -1618,14 +1761,19 @@ namespace sat { if (inconsistent()) break; assign_scoped(lit); } - propagate(false); + if (!inconsistent()) propagate(false); TRACE("sat", + tout << "consistent: " << !inconsistent() << "\n"; for (literal a : m_assumptions) { index_set s; if (m_antecedents.find(a.var(), s)) { tout << a << ": "; display_index_set(tout, s) << "\n"; } - }); + } + for (literal lit : m_user_scope_literals) { + tout << "user " << lit << "\n"; + } + ); } } @@ -1650,8 +1798,15 @@ namespace sat { void solver::init_search() { m_model_is_current = false; m_phase_counter = 0; - m_phase_cache_on = m_config.m_phase_sticky; + m_search_state = s_unsat; + m_search_unsat_conflicts = m_config.m_search_unsat_conflicts; + m_search_sat_conflicts = m_config.m_search_sat_conflicts; + m_search_next_toggle = m_search_unsat_conflicts; + m_best_phase_size = 0; + m_rephase_lim = 0; + m_rephase_inc = 0; m_conflicts_since_restart = 0; + m_force_conflict_analysis = false; m_restart_threshold = m_config.m_restart_initial; m_luby_idx = 1; m_gc_threshold = m_config.m_gc_initial; @@ -1677,11 +1832,14 @@ namespace sat { } + bool solver::should_simplify() const { + return m_conflicts_since_init >= m_next_simplify; + } /** \brief Apply all simplifications. */ - void solver::simplify_problem() { - if (m_conflicts_since_init < m_next_simplify) { + void solver::do_simplify() { + if (!should_simplify()) { return; } log_stats(); @@ -1699,6 +1857,10 @@ namespace sat { m_scc(); CASSERT("sat_simplify_bug", check_invariant()); + + if (m_ext) { + m_ext->pre_simplify(); + } m_simplifier(false); @@ -1730,6 +1892,7 @@ namespace sat { } reinit_assumptions(); + if (inconsistent()) return; if (m_next_simplify == 0) { m_next_simplify = m_config.m_next_simplify1; @@ -1740,7 +1903,25 @@ namespace sat { m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max; } - if (m_par) m_par->set_phase(*this); + if (m_par) { + m_par->from_solver(*this); + if (m_par->to_solver(*this)) { + m_activity_inc = 128; + } + } + +#if 0 + static unsigned file_no = 0; + #pragma omp critical (print_sat) + { + ++file_no; + std::ostringstream ostrm; + ostrm << "s" << file_no << ".txt"; + std::ofstream ous(ostrm.str()); + display(ous); + } +#endif + } bool solver::set_root(literal l, literal r) { @@ -1771,16 +1952,16 @@ namespace sat { for (bool_var v = 0; v < num; v++) { if (!was_eliminated(v)) { m_model[v] = value(v); - m_phase[v] = (value(v) == l_true) ? POS_PHASE : NEG_PHASE; + m_phase[v] = value(v) == l_true; } } TRACE("sat_mc_bug", m_mc.display(tout);); #if 0 - IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); + IF_VERBOSE(2, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); for (auto p : big::s_del_bin) { if (value(p.first) != l_true && value(p.second) != l_true) { - IF_VERBOSE(0, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n"); + IF_VERBOSE(2, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n"); } } #endif @@ -1801,14 +1982,20 @@ namespace sat { if (m_clone && !check_clauses(m_model)) { IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(10, m_mc.display(verbose_stream())); - IF_VERBOSE(10, display_model(verbose_stream())); + IF_VERBOSE(1, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); + throw solver_exception("check model failed"); } - if (m_clone && !m_clone->check_model(m_model)) { - IF_VERBOSE(1, m_mc.display(verbose_stream())); - IF_VERBOSE(1, display_units(verbose_stream())); - throw solver_exception("check model failed (for cloned solver)"); + TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); + + if (m_clone) { + IF_VERBOSE(1, verbose_stream() << "\"checking model (on original set of clauses)\"\n";); + if (!m_clone->check_model(m_model)) { + IF_VERBOSE(1, m_mc.display(verbose_stream())); + IF_VERBOSE(1, display_units(verbose_stream())); + throw solver_exception("check model failed (for cloned solver)"); + } } } @@ -1952,7 +2139,7 @@ namespace sat { IF_VERBOSE(1, verbose_stream() << str); } - void solver::restart(bool to_base) { + void solver::do_restart(bool to_base) { m_stats.m_restart++; m_restarts++; if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) { @@ -1964,6 +2151,7 @@ namespace sat { } log_stats(); } + TRACE("sat", tout << "restart " << restart_level(to_base) << "\n";); IF_VERBOSE(30, display_status(verbose_stream());); TRACE("sat", tout << "restart " << restart_level(to_base) << "\n";); pop_reinit(restart_level(to_base)); @@ -1998,6 +2186,16 @@ namespace sat { } } + + void solver::update_activity(bool_var v, double p) { + unsigned old_act = m_activity[v]; + unsigned new_act = (unsigned) (num_vars() * m_config.m_activity_scale * p); + m_activity[v] = new_act; + if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) { + m_case_split_queue.activity_changed_eh(v, new_act > old_act); + } + } + void solver::set_next_restart() { m_conflicts_since_restart = 0; switch (m_config.m_restart) { @@ -2026,12 +2224,18 @@ namespace sat { // // ----------------------- - void solver::gc() { - if (m_conflicts_since_gc <= m_gc_threshold) - return; - if (m_config.m_gc_strategy == GC_DYN_PSM && !at_base_lvl()) - return; + bool solver::should_gc() const { + return + m_conflicts_since_gc > m_gc_threshold && + (m_config.m_gc_strategy != GC_DYN_PSM || at_base_lvl()); + } + + void solver::do_gc() { + if (!should_gc()) return; + TRACE("sat", tout << m_conflicts_since_gc << " " << m_gc_threshold << "\n";); unsigned gc = m_stats.m_gc_clause; + m_conflicts_since_gc = 0; + m_gc_threshold += m_config.m_gc_increment; IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { @@ -2048,6 +2252,10 @@ namespace sat { gc_psm_glue(); break; case GC_DYN_PSM: + if (!m_assumptions.empty()) { + gc_glue_psm(); + break; + } if (!at_base_lvl()) return; gc_dyn_psm(); @@ -2060,8 +2268,6 @@ namespace sat { if (gc > 0 && should_defrag()) { defrag_clauses(); } - m_conflicts_since_gc = 0; - m_gc_threshold += m_config.m_gc_increment; CASSERT("sat_gc_bug", check_invariant()); } @@ -2185,7 +2391,7 @@ namespace sat { bool solver::can_delete(clause const & c) const { if (c.on_reinit_stack()) return false; - if (c.size() == 3) { + if (ENABLE_TERNARY && c.size() == 3) { return can_delete3(c[0],c[1],c[2]) && can_delete3(c[1],c[0],c[2]) && @@ -2328,15 +2534,7 @@ namespace sat { mk_bin_clause(c[0], c[1], true); return false; default: - if (new_sz != sz) { - c.shrink(new_sz); - if (m_config.m_drat) { - m_drat.add(c, true); - c.restore(sz); - m_drat.del(c); - c.shrink(new_sz); - } - } + shrink(c, sz, new_sz); attach_clause(c); return true; } @@ -2348,13 +2546,8 @@ namespace sat { unsigned solver::psm(clause const & c) const { unsigned r = 0; for (literal l : c) { - if (l.sign()) { - if (m_phase[l.var()] == NEG_PHASE) - r++; - } - else { - if (m_phase[l.var()] == POS_PHASE) - r++; + if (l.sign() ^ m_phase[l.var()]) { + r++; } } return r; @@ -2368,17 +2561,18 @@ namespace sat { bool solver::resolve_conflict() { while (true) { - bool r = resolve_conflict_core(); + lbool r = resolve_conflict_core(); CASSERT("sat_check_marks", check_marks()); // after pop, clauses are reinitialized, this may trigger another conflict. - if (!r) + if (r == l_false) return false; if (!inconsistent()) return true; } } - bool solver::resolve_conflict_core() { + + lbool solver::resolve_conflict_core() { m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; @@ -2386,37 +2580,49 @@ namespace sat { if (m_step_size > m_config.m_step_size_min) { m_step_size -= m_config.m_step_size_dec; } - - m_conflict_lvl = get_max_lvl(m_not_l, m_conflict); - TRACE("sat_verbose", tout << "conflict detected at level " << m_conflict_lvl << " for "; - if (m_not_l == literal()) tout << "null literal\n"; - else tout << m_not_l << "\n";); + bool unique_max; + m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max); + justification js = m_conflict; if (m_conflict_lvl <= 1 && tracking_assumptions()) { + TRACE("sat", tout << "unsat core\n";); resolve_conflict_for_unsat_core(); - return false; + return l_false; } if (m_conflict_lvl == 0) { - return false; + TRACE("sat", tout << "conflict level is 0\n";); + return l_false; } - forget_phase_of_vars(m_conflict_lvl); + // force_conflict_analysis is used instead of relying on normal propagation to assign m_not_l + // at the backtracking level. This is the case where the external theories miss propagations + // that only get triggered after decisions. + + if (unique_max && !m_force_conflict_analysis) { + TRACE("sat", tout << "unique max " << js << " " << m_not_l << "\n";); + pop_reinit(m_scope_lvl - m_conflict_lvl + 1); + m_force_conflict_analysis = true; + ++m_stats.m_backtracks; + return l_undef; + } + m_force_conflict_analysis = false; + + updt_phase_of_vars(); if (m_ext) { switch (m_ext->resolve_conflict()) { case l_true: learn_lemma_and_backjump(); - return true; + return l_undef; case l_undef: break; case l_false: // backjumping was taken care of internally. - return true; + return l_undef; } } - m_lemma.reset(); unsigned idx = skip_literals_above_conflict_level(); @@ -2424,19 +2630,25 @@ namespace sat { // save space for first uip m_lemma.push_back(null_literal); + TRACE("sat_conflict_detail", + tout << "resolve: " << m_not_l << " " + << " js: " << js + << " idx: " << idx + << " trail: " << m_trail.size() + << " @" << m_conflict_lvl << "\n";); + unsigned num_marks = 0; literal consequent = null_literal; if (m_not_l != null_literal) { - TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";); + TRACE("sat_conflict_detail", tout << "not_l: " << m_not_l << "\n";); process_antecedent(m_not_l, num_marks); consequent = ~m_not_l; } - justification js = m_conflict; - do { - TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; - tout << "num_marks: " << num_marks << ", js: " << js << "\n";); + TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << " @" << (consequent==null_literal?m_conflict_lvl:lvl(consequent)) << "\n"; + tout << "num_marks: " << num_marks << "\n"; + display_justification(tout, js) << "\n";); switch (js.get_kind()) { case justification::NONE: @@ -2450,7 +2662,7 @@ namespace sat { break; case justification::CLAUSE: { clause & c = get_clause(js); - unsigned i = 0; + unsigned i = 0; if (consequent != null_literal) { SASSERT(c[0] == consequent || c[1] == consequent); if (c[0] == consequent) { @@ -2461,7 +2673,7 @@ namespace sat { i = 2; } } - unsigned sz = c.size(); + unsigned sz = c.size(); for (; i < sz; i++) process_antecedent(~c[i], num_marks); break; @@ -2476,17 +2688,20 @@ namespace sat { UNREACHABLE(); break; } - + + bool_var c_var; while (true) { - literal l = m_trail[idx]; - if (is_marked(l.var())) - break; + consequent = m_trail[idx]; + c_var = consequent.var(); + if (is_marked(c_var)) { + if (lvl(c_var) == m_conflict_lvl) { + break; + } + SASSERT(lvl(c_var) < m_conflict_lvl); + } SASSERT(idx > 0); idx--; } - - consequent = m_trail[idx]; - bool_var c_var = consequent.var(); SASSERT(lvl(consequent) == m_conflict_lvl); js = m_justification[c_var]; idx--; @@ -2499,49 +2714,83 @@ namespace sat { m_lemma[0] = ~consequent; learn_lemma_and_backjump(); - return true; + return l_undef; } void solver::learn_lemma_and_backjump() { TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";); - - unsigned new_scope_lvl = 0; - if (!m_lemma.empty()) { - if (m_config.m_minimize_lemmas) { - minimize_lemma(); - reset_lemma_var_marks(); - if (m_config.m_dyn_sub_res) - dyn_sub_res(); - TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";); - } - else - reset_lemma_var_marks(); - - literal_vector::iterator it = m_lemma.begin(); - literal_vector::iterator end = m_lemma.end(); - ++it; - for(; it != end; ++it) { - bool_var var = (*it).var(); - new_scope_lvl = std::max(new_scope_lvl, lvl(var)); + + if (m_lemma.empty()) { + pop_reinit(m_scope_lvl); + mk_clause_core(0, nullptr, true); + return; + } + + if (m_config.m_minimize_lemmas) { + minimize_lemma(); + reset_lemma_var_marks(); + if (m_config.m_dyn_sub_res) + dyn_sub_res(); + TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";); + } + else { + reset_lemma_var_marks(); + } + + unsigned backtrack_lvl = lvl(m_lemma[0]); + unsigned backjump_lvl = 0; + for (unsigned i = m_lemma.size(); i-- > 1;) { + unsigned level = lvl(m_lemma[i]); + backjump_lvl = std::max(level, backjump_lvl); + } + // with scope tracking and chronological backtracking, + // consequent may not be at highest decision level. + if (backtrack_lvl < backjump_lvl) { + backtrack_lvl = backjump_lvl; + for (unsigned i = m_lemma.size(); i-- > 1;) { + if (lvl(m_lemma[i]) == backjump_lvl) { + TRACE("sat", tout << "swap " << m_lemma[0] << "@" << lvl(m_lemma[0]) << m_lemma[1] << "@" << backjump_lvl << "\n";); + std::swap(m_lemma[i], m_lemma[0]); + break; + } } } - - unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr()); + + unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr()); m_fast_glue_avg.update(glue); m_slow_glue_avg.update(glue); - pop_reinit(m_scope_lvl - new_scope_lvl); - TRACE("sat_conflict_detail", tout << glue << " " << new_scope_lvl << "\n";); + + // compute whether to use backtracking or backjumping + unsigned num_scopes = m_scope_lvl - backjump_lvl; + + if (use_backjumping(num_scopes)) { + ++m_stats.m_backjumps; + pop_reinit(num_scopes); + } + else { + TRACE("sat", tout << "backtrack " << (m_scope_lvl - backtrack_lvl + 1) << " scopes\n";); + ++m_stats.m_backtracks; + pop_reinit(m_scope_lvl - backtrack_lvl + 1); + } clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true); if (lemma) { lemma->set_glue(glue); - if (m_par) m_par->share_clause(*this, *lemma); } - - TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n";); + if (m_par && lemma) { + m_par->share_clause(*this, *lemma); + } + TRACE("sat_conflict_detail", tout << "consistent " << (!m_inconsistent) << " scopes: " << scope_lvl() << " backtrack: " << backtrack_lvl << " backjump: " << backjump_lvl << "\n";); decay_activity(); updt_phase_counters(); } + bool solver::use_backjumping(unsigned num_scopes) { + return + num_scopes > 0 && + (num_scopes <= m_config.m_backtrack_scopes || + m_conflicts_since_init <= m_config.m_backtrack_init_conflicts); + } + void solver::process_antecedent_for_unsat_core(literal antecedent) { bool_var var = antecedent.var(); SASSERT(var < num_vars()); @@ -2696,31 +2945,40 @@ namespace sat { set_model(m_mus.get_model()); IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";); } - } - unsigned solver::get_max_lvl(literal not_l, justification js) { - if (!m_ext || at_base_lvl()) - return scope_lvl(); + unsigned solver::get_max_lvl(literal not_l, justification js, bool& unique_max) { + unique_max = true; + unsigned level = 0; + + if (not_l != null_literal) { + level = lvl(not_l); + } switch (js.get_kind()) { case justification::NONE: + level = std::max(level, js.level()); + return level; case justification::BINARY: + level = update_max_level(js.get_literal(), level, unique_max); + return level; case justification::TERNARY: - case justification::CLAUSE: { - return scope_lvl(); - } - case justification::EXT_JUSTIFICATION: { - unsigned r = 0; + level = update_max_level(js.get_literal1(), level, unique_max); + level = update_max_level(js.get_literal2(), level, unique_max); + return level; + case justification::CLAUSE: + for (literal l : get_clause(js)) { + level = update_max_level(l, level, unique_max); + } + return level; + case justification::EXT_JUSTIFICATION: SASSERT(not_l != null_literal); - r = lvl(not_l); fill_ext_antecedents(~not_l, js); for (literal l : m_ext_antecedents) { - r = std::max(r, lvl(l)); + level = update_max_level(l, level, unique_max); } - return r; - } + return level; default: UNREACHABLE(); return 0; @@ -2780,30 +3038,117 @@ namespace sat { m_ext->get_antecedents(consequent, js.get_ext_justification_idx(), m_ext_antecedents); } - void solver::forget_phase_of_vars(unsigned from_lvl) { + bool solver::is_two_phase() const { + return m_config.m_phase == PS_SAT_CACHING; + } + + bool solver::is_sat_phase() const { + return is_two_phase() && m_search_state == s_sat; + } + + void solver::updt_phase_of_vars() { + unsigned from_lvl = m_conflict_lvl; unsigned head = from_lvl == 0 ? 0 : m_scopes[from_lvl - 1].m_trail_lim; unsigned sz = m_trail.size(); for (unsigned i = head; i < sz; i++) { - literal l = m_trail[i]; - bool_var v = l.var(); - TRACE("forget_phase", tout << "forgetting phase of l: " << l << "\n";); - m_phase[v] = PHASE_NOT_AVAILABLE; + bool_var v = m_trail[i].var(); + TRACE("forget_phase", tout << "forgetting phase of v" << v << "\n";); + m_phase[v] = m_rand() % 2 == 0; } + if (is_sat_phase() && head >= m_best_phase_size) { + m_best_phase_size = head; + IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n"); + for (unsigned i = 0; i < head; ++i) { + bool_var v = m_trail[i].var(); + m_best_phase[v] = m_phase[v]; + } + } + } + + bool solver::should_toggle_search_state() { + if (m_search_state == s_unsat) { + m_trail_avg.update(m_trail.size()); + } + return + (m_phase_counter >= m_search_next_toggle) && + (m_search_state == s_sat || m_trail.size() > 0.50*m_trail_avg); + } + + void solver::do_toggle_search_state() { + + if (is_two_phase()) { + m_best_phase_size = 0; + std::swap(m_fast_glue_backup, m_fast_glue_avg); + std::swap(m_slow_glue_backup, m_slow_glue_avg); + if (m_search_state == s_sat) { + m_search_unsat_conflicts += m_config.m_search_unsat_conflicts; + } + else { + m_search_sat_conflicts += m_config.m_search_sat_conflicts; + } + } + + if (m_search_state == s_unsat) { + m_search_state = s_sat; + m_search_next_toggle = m_search_sat_conflicts; + } + else { + m_search_state = s_unsat; + m_search_next_toggle = m_search_unsat_conflicts; + } + + m_phase_counter = 0; + } + + bool solver::should_rephase() { + return m_conflicts_since_init > m_rephase_lim; + } + + void solver::do_rephase() { + switch (m_config.m_phase) { + case PS_ALWAYS_TRUE: + for (auto& p : m_phase) p = true; + break; + case PS_ALWAYS_FALSE: + for (auto& p : m_phase) p = false; + break; + case PS_BASIC_CACHING: + switch (m_rephase_lim % 4) { + case 0: + for (auto& p : m_phase) p = (m_rand() % 2) == 0; + break; + case 1: + for (auto& p : m_phase) p = false; + break; + case 2: + for (auto& p : m_phase) p = !p; + break; + default: + break; + } + break; + case PS_SAT_CACHING: + if (m_search_state == s_sat) { + for (unsigned i = 0; i < m_phase.size(); ++i) { + m_phase[i] = m_best_phase[i]; + } + } + break; + case PS_RANDOM: + for (auto& p : m_phase) p = (m_rand() % 2) == 0; + break; + default: + UNREACHABLE(); + break; + } + m_rephase_inc += m_config.m_rephase_base; + m_rephase_lim += m_rephase_inc; } void solver::updt_phase_counters() { m_phase_counter++; - if (m_phase_cache_on) { - if (m_phase_counter >= m_config.m_phase_caching_on) { - m_phase_counter = 0; - m_phase_cache_on = false; - } - } - else { - if (m_phase_counter >= m_config.m_phase_caching_off) { - m_phase_counter = 0; - m_phase_cache_on = true; - } + if (should_toggle_search_state()) { + do_toggle_search_state(); } } @@ -2995,6 +3340,38 @@ namespace sat { m_lvl_set.insert(lvl(l)); } + /** + \brief Minimize lemma using binary resolution + */ + bool solver::minimize_lemma_binres() { + SASSERT(!m_lemma.empty()); + SASSERT(m_unmark.empty()); + unsigned sz = m_lemma.size(); + unsigned num_reduced = 0; + for (unsigned i = 1; i < sz; ++i) { + mark_lit(m_lemma[i]); + } + watch_list const& wlist = get_wlist(m_lemma[0]); + for (watched const& w : wlist) { + if (w.is_binary_clause() && is_marked_lit(w.get_literal())) { + unmark_lit(~w.get_literal()); + num_reduced++; + } + } + if (num_reduced > 0) { + unsigned j = 1; + for (unsigned i = 1; i < sz; ++i) { + if (is_marked_lit(m_lemma[i])) { + m_lemma[j++] = m_lemma[i]; + unmark_lit(m_lemma[i]); + } + } + m_lemma.shrink(j); + } + + return num_reduced > 0; + } + /** \brief Minimize the number of literals in m_lemma. The main idea is to remove literals that are implied by other literals in m_lemma and/or literals @@ -3014,10 +3391,7 @@ namespace sat { m_unmark.push_back(l.var()); } else { - if (j != i) { - m_lemma[j] = m_lemma[i]; - } - j++; + m_lemma[j++] = m_lemma[i]; } } @@ -3250,7 +3624,7 @@ namespace sat { unsigned new_lvl = scope_lvl() - num_scopes; scope & s = m_scopes[new_lvl]; m_inconsistent = false; - unassign_vars(s.m_trail_lim); + unassign_vars(s.m_trail_lim, new_lvl); m_scope_lvl -= num_scopes; m_scopes.shrink(new_lvl); reinit_clauses(s.m_clauses_to_reinit_lim); @@ -3258,15 +3632,20 @@ namespace sat { m_ext->pop_reinit(); } - void solver::unassign_vars(unsigned old_sz) { + void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) { SASSERT(old_sz <= m_trail.size()); + SASSERT(m_replay_assign.empty()); unsigned i = m_trail.size(); while (i != old_sz) { --i; literal l = m_trail[i]; + bool_var v = l.var(); + if (lvl(v) <= new_lvl) { + m_replay_assign.push_back(l); + continue; + } m_assignment[l.index()] = l_undef; m_assignment[(~l).index()] = l_undef; - bool_var v = l.var(); SASSERT(value(v) == l_undef); m_case_split_queue.unassign_var_eh(v); if (m_config.m_branching_heuristic == BH_LRB) { @@ -3282,9 +3661,14 @@ namespace sat { m_canceled[v] = m_stats.m_conflict; } } - m_trail.shrink(old_sz); - m_qhead = old_sz; - SASSERT(m_qhead == m_trail.size()); + m_trail.shrink(old_sz); + m_qhead = m_trail.size(); + if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n"); + for (unsigned i = m_replay_assign.size(); i-- > 0; ) { + m_trail.push_back(m_replay_assign[i]); + } + + m_replay_assign.reset(); } void solver::reinit_clauses(unsigned old_sz) { @@ -3403,8 +3787,8 @@ namespace sat { v = w + 1; // v is an index of a variable that does not occur in solver state. - if (v < m_level.size()) { - for (bool_var i = v; i < m_level.size(); ++i) { + if (v < m_justification.size()) { + for (bool_var i = v; i < m_justification.size(); ++i) { m_case_split_queue.del_var_eh(i); m_probing.reset_cache(literal(i, true)); m_probing.reset_cache(literal(i, false)); @@ -3415,11 +3799,12 @@ namespace sat { m_decision.shrink(v); m_eliminated.shrink(v); m_external.shrink(v); + m_touched.shrink(v); m_activity.shrink(v); - m_level.shrink(v); m_mark.shrink(v); m_lit_mark.shrink(2*v); m_phase.shrink(v); + m_best_phase.shrink(v); m_prev_phase.shrink(v); m_assigned_since_gc.shrink(v); m_simplifier.reset_todos(); @@ -3443,7 +3828,7 @@ namespace sat { for (unsigned i = 0; i < m_trail.size(); ++i) { if (m_trail[i] == lit) { TRACE("sat", tout << m_trail << "\n";); - unassign_vars(i); + unassign_vars(i, 0); break; } } @@ -3476,6 +3861,9 @@ namespace sat { m_drat.updt_config(); m_fast_glue_avg.set_alpha(m_config.m_fast_glue_avg); m_slow_glue_avg.set_alpha(m_config.m_slow_glue_avg); + m_fast_glue_backup.set_alpha(m_config.m_fast_glue_avg); + m_slow_glue_backup.set_alpha(m_config.m_slow_glue_avg); + m_trail_avg.set_alpha(m_config.m_slow_glue_avg); } void solver::collect_param_descrs(param_descrs & d) { @@ -3608,7 +3996,7 @@ namespace sat { void solver::display_units(std::ostream & out) const { unsigned level = 0; - for (literal lit : m_trail) { + for (literal lit : m_trail) { if (lvl(lit) > level) { level = lvl(lit); out << level << ": "; @@ -3617,6 +4005,9 @@ namespace sat { out << " "; } out << lit << " "; + if (lvl(lit) < level) { + out << "@" << lvl(lit) << " "; + } display_justification(out, m_justification[lit.var()]) << "\n"; } } @@ -3635,7 +4026,7 @@ namespace sat { std::ostream& solver::display_justification(std::ostream & out, justification const& js) const { switch (js.get_kind()) { case justification::NONE: - out << "none "; // << js.level(); + out << "none @" << js.level(); break; case justification::BINARY: out << "binary " << js.get_literal() << "@" << lvl(js.get_literal()); @@ -3835,11 +4226,13 @@ namespace sat { // Simplification // // ----------------------- - void solver::cleanup(bool force) { - if (!at_base_lvl() || inconsistent()) - return; - if (m_cleaner(force) && m_ext) - m_ext->clauses_modifed(); + bool solver::do_cleanup(bool force) { + if (at_base_lvl() && !inconsistent() && m_cleaner(force)) { + if (m_ext) + m_ext->clauses_modifed(); + return true; + } + return false; } void solver::simplify(bool learned) { @@ -4092,7 +4485,7 @@ namespace sat { extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); - simplify_problem(); + do_simplify(); if (check_inconsistent()) { fixup_consequence_core(); return l_false; @@ -4110,20 +4503,15 @@ namespace sat { extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); - if (reached_max_conflicts()) { - return l_undef; - } - - restart(true); - simplify_problem(); + do_restart(true); + do_simplify(); if (check_inconsistent()) { fixup_consequence_core(); return l_false; } - gc(); + do_gc(); - if (m_config.m_restart_max <= num_iterations) { - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); + if (should_cancel()) { return l_undef; } } @@ -4134,8 +4522,8 @@ namespace sat { m_antecedents.reset(); literal_set unfixed_lits(lits), assumptions(asms); bool_var_set unfixed_vars; - for (unsigned i = 0; i < lits.size(); ++i) { - unfixed_vars.insert(lits[i].var()); + for (literal lit : lits) { + unfixed_vars.insert(lit.var()); } pop_to_base_level(); @@ -4191,10 +4579,6 @@ namespace sat { propagate(false); ++num_resolves; } - if (false && scope_lvl() == search_lvl()) { - is_sat = l_undef; - break; - } } extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); @@ -4207,7 +4591,7 @@ namespace sat { else { is_sat = bounded_search(); if (is_sat == l_undef) { - restart(true); + do_restart(true); } extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); } @@ -4431,7 +4815,7 @@ namespace sat { clause_vector const & cs = *(vs[i]); for (clause* cp : cs) { clause & c = *cp; - if (c.size() == 3) + if (ENABLE_TERNARY && c.size() == 3) num_ter++; else num_cls++; @@ -4473,6 +4857,8 @@ namespace sat { st.update("sat units", m_units); st.update("sat elim bool vars res", m_elim_var_res); st.update("sat elim bool vars bdd", m_elim_var_bdd); + st.update("sat backjumps", m_backjumps); + st.update("sat backtracks", m_backtracks); } void stats::reset() { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 47e226cc4..a44b91749 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -19,7 +19,7 @@ Revision History: #ifndef SAT_SOLVER_H_ #define SAT_SOLVER_H_ - +#include #include "sat/sat_types.h" #include "sat/sat_clause.h" #include "sat/sat_watched.h" @@ -71,6 +71,8 @@ namespace sat { unsigned m_elim_var_res; unsigned m_elim_var_bdd; unsigned m_units; + unsigned m_backtracks; + unsigned m_backjumps; stats() { reset(); } void reset(); void collect_statistics(statistics & st) const; @@ -80,6 +82,8 @@ namespace sat { public: struct abort_solver {}; protected: + enum search_state { s_sat, s_unsat }; + bool m_checkpoint_enabled; config m_config; stats m_stats; @@ -116,7 +120,9 @@ namespace sat { svector m_lit_mark; svector m_eliminated; svector m_external; - svector m_level; + unsigned_vector m_touched; + unsigned m_touch_index; + literal_vector m_replay_assign; // branch variable selection: svector m_activity; unsigned m_activity_inc; @@ -128,17 +134,27 @@ namespace sat { int m_action; double m_step_size; // phase - svector m_phase; - svector m_prev_phase; + svector m_phase; + svector m_best_phase; + svector m_prev_phase; svector m_assigned_since_gc; - bool m_phase_cache_on; + search_state m_search_state; + unsigned m_search_unsat_conflicts; + unsigned m_search_sat_conflicts; + unsigned m_search_next_toggle; unsigned m_phase_counter; + unsigned m_best_phase_size; + unsigned m_rephase_lim; + unsigned m_rephase_inc; var_queue m_case_split_queue; unsigned m_qhead; unsigned m_scope_lvl; unsigned m_search_lvl; ema m_fast_glue_avg; ema m_slow_glue_avg; + ema m_fast_glue_backup; + ema m_slow_glue_backup; + ema m_trail_avg; literal_vector m_trail; clause_wrapper_vector m_clauses_to_reinit; std::string m_reason_unknown; @@ -163,7 +179,7 @@ namespace sat { bool m_par_syncing_clauses; class lookahead* m_cuber; - class local_search* m_local_search; + class i_local_search* m_local_search; statistics m_aux_stats; @@ -174,6 +190,7 @@ namespace sat { friend class simplifier; friend class scc; friend class big; + friend class binspr; friend class elim_eqs; friend class asymm_branch; friend class probing; @@ -184,6 +201,8 @@ namespace sat { friend class parallel; friend class lookahead; friend class local_search; + friend class ddfw; + friend class prob; friend class unit_walk; friend struct mk_stat; friend class elim_vars; @@ -251,6 +270,7 @@ namespace sat { void attach_clause(clause & c, bool & reinit); void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); } void set_learned(clause& c, bool learned); + void shrink(clause& c, unsigned old_sz, unsigned new_sz); void set_learned(literal l1, literal l2, bool learned); void set_learned1(literal l1, literal l2, bool learned); void add_ate(clause& c) { m_mc.add_ate(c); } @@ -285,7 +305,7 @@ namespace sat { // ----------------------- public: bool inconsistent() const override { return m_inconsistent; } - unsigned num_vars() const override { return m_level.size(); } + unsigned num_vars() const override { return m_justification.size(); } unsigned num_clauses() const override; void num_binary(unsigned& given, unsigned& learned) const; unsigned num_restarts() const { return m_restarts; } @@ -293,7 +313,7 @@ namespace sat { void set_external(bool_var v) override; void set_non_external(bool_var v) override; bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } - void set_eliminated(bool_var v, bool f) override { m_eliminated[v] = f; } + void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } @@ -301,40 +321,55 @@ namespace sat { bool at_base_lvl() const override { return m_scope_lvl == 0; } lbool value(literal l) const { return static_cast(m_assignment[l.index()]); } lbool value(bool_var v) const { return static_cast(m_assignment[literal(v, false).index()]); } - unsigned lvl(bool_var v) const { return m_level[v]; } - unsigned lvl(literal l) const { return m_level[l.var()]; } + unsigned lvl(bool_var v) const { return m_justification[v].level(); } + unsigned lvl(literal l) const { return m_justification[l.var()].level(); } unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } unsigned trail_size() const { return m_trail.size(); } literal trail_literal(unsigned i) const override { return m_trail[i]; } literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; } void assign(literal l, justification j) { - TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";); + TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";); switch (value(l)) { case l_false: set_conflict(j, ~l); break; - case l_undef: assign_core(l, scope_lvl(), j); break; + case l_undef: assign_core(l, j); break; case l_true: return; } } - void assign_core(literal l, unsigned lvl, justification jst); - void assign_unit(literal l) { assign(l, justification()); } - void assign_scoped(literal l) { assign(l, justification()); } + void assign_unit(literal l) { assign(l, justification(0)); } + void assign_scoped(literal l) { assign(l, justification(scope_lvl())); } + void assign_core(literal l, justification jst); void set_conflict(justification c, literal not_l); void set_conflict(justification c) { set_conflict(c, null_literal); } - void set_conflict() { set_conflict(justification()); } + void set_conflict() { set_conflict(justification(0)); } lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); } - void checkpoint() { - if (!m_checkpoint_enabled) return; + + bool limit_reached() { if (!m_rlimit.inc()) { m_mc.reset(); m_model_is_current = false; TRACE("sat", tout << "canceled\n";); + m_reason_unknown = "sat.canceled"; + return true; + } + return false; + } + + bool memory_exceeded() { + ++m_num_checkpoints; + if (m_num_checkpoints < 10) return false; + m_num_checkpoints = 0; + return memory::get_allocation_size() > m_config.m_max_memory; + } + + void checkpoint() { + if (!m_checkpoint_enabled) return; + if (limit_reached()) { throw solver_exception(Z3_CANCELED_MSG); } - ++m_num_checkpoints; - if (m_num_checkpoints < 10) return; - m_num_checkpoints = 0; - if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); + if (memory_exceeded()) { + throw solver_exception(Z3_MAX_MEMORY_MSG); + } } void set_par(parallel* p, unsigned id); bool canceled() { return !m_rlimit.inc(); } @@ -358,7 +393,6 @@ namespace sat { void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; } bool check_inconsistent(); - // ----------------------- // // Propagation @@ -369,6 +403,7 @@ namespace sat { bool propagate(bool update); protected: + bool should_propagate() const; bool propagate_core(bool update); // ----------------------- @@ -391,6 +426,8 @@ namespace sat { void set_activity(bool_var v, unsigned act); lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level); + + void display_lookahead_scores(std::ostream& out); protected: @@ -398,6 +435,7 @@ namespace sat { unsigned m_restarts; unsigned m_restart_next_out; unsigned m_conflicts_since_restart; + bool m_force_conflict_analysis; unsigned m_simplifications; unsigned m_restart_threshold; unsigned m_luby_idx; @@ -427,22 +465,28 @@ namespace sat { void reinit_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; - void simplify_problem(); + bool should_simplify() const; + void do_simplify(); void mk_model(); bool check_model(model const & m) const; - void restart(bool to_base); + void do_restart(bool to_base); svector m_last_positions; unsigned m_last_position_log; unsigned m_restart_logs; unsigned restart_level(bool to_base); void log_stats(); + bool should_cancel(); bool should_restart() const; void set_next_restart(); + void update_activity(bool_var v, double p); bool reached_max_conflicts(); void sort_watch_lits(); void exchange_par(); lbool check_par(unsigned num_lits, literal const* lits); lbool do_local_search(unsigned num_lits, literal const* lits); + lbool do_ddfw_search(unsigned num_lits, literal const* lits); + lbool do_prob_search(unsigned num_lits, literal const* lits); + lbool invoke_local_search(unsigned num_lits, literal const* lits); lbool do_unit_walk(); // ----------------------- @@ -451,7 +495,8 @@ namespace sat { // // ----------------------- protected: - void gc(); + bool should_gc() const; + void do_gc(); void gc_glue(); void gc_psm(); void gc_glue_psm(); @@ -492,18 +537,31 @@ namespace sat { unsigned m_conflict_lvl; literal_vector m_lemma; literal_vector m_ext_antecedents; + bool use_backjumping(unsigned num_scopes); bool resolve_conflict(); - bool resolve_conflict_core(); + lbool resolve_conflict_core(); void learn_lemma_and_backjump(); - unsigned get_max_lvl(literal consequent, justification js); + inline unsigned update_max_level(literal lit, unsigned lvl2, bool& unique_max) { + unsigned lvl1 = lvl(lit); + if (lvl1 < lvl2) return lvl2; + unique_max = lvl1 > lvl2; + return lvl1; + } + unsigned get_max_lvl(literal consequent, justification js, bool& unique_max); void process_antecedent(literal antecedent, unsigned & num_marks); void resolve_conflict_for_unsat_core(); void process_antecedent_for_unsat_core(literal antecedent); void process_consequent_for_unsat_core(literal consequent, justification const& js); void fill_ext_antecedents(literal consequent, justification js); unsigned skip_literals_above_conflict_level(); - void forget_phase_of_vars(unsigned from_lvl); + void updt_phase_of_vars(); void updt_phase_counters(); + void do_toggle_search_state(); + bool should_toggle_search_state(); + bool is_sat_phase() const; + bool is_two_phase() const; + bool should_rephase(); + void do_rephase(); svector m_diff_levels; unsigned num_diff_levels(unsigned num, literal const * lits); bool num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue); @@ -518,8 +576,9 @@ namespace sat { bool implied_by_marked(literal lit); void reset_unmark(unsigned old_size); void updt_lemma_lvl_set(); - void reset_lemma_var_marks(); bool minimize_lemma(); + bool minimize_lemma_binres(); + void reset_lemma_var_marks(); bool dyn_sub_res(); // ----------------------- @@ -531,7 +590,7 @@ namespace sat { void pop(unsigned num_scopes); void pop_reinit(unsigned num_scopes); - void unassign_vars(unsigned old_sz); + void unassign_vars(unsigned old_sz, unsigned new_lvl); void reinit_clauses(unsigned old_sz); literal_vector m_user_scope_literals; @@ -556,7 +615,7 @@ namespace sat { // // ----------------------- public: - void cleanup(bool force); + bool do_cleanup(bool force); void simplify(bool learned = true); void asymmetric_branching(); unsigned scc_bin(); diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index cbe0cab4c..e373a5713 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -29,6 +29,10 @@ Revision History: #include "util/stopwatch.h" #include +class params_ref; +class reslimit; +class statistics; + namespace sat { #define SAT_VB_LVL 10 @@ -120,11 +124,8 @@ namespace sat { typedef approx_set_tpl var_approx_set; - enum phase { - POS_PHASE, NEG_PHASE, PHASE_NOT_AVAILABLE - }; - class solver; + class parallel; class lookahead; class unit_walk; class clause; @@ -257,6 +258,22 @@ namespace sat { inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) { return out << mk_lits_pp(ls.size(), ls.c_ptr()); } + + class i_local_search { + public: + virtual ~i_local_search() {} + virtual void add(solver const& s) = 0; + virtual void updt_params(params_ref const& p) = 0; + virtual void set_seed(unsigned s) = 0; + virtual lbool check(unsigned sz, literal const* assumptions, parallel* par) = 0; + virtual void reinit(solver& s) = 0; + virtual unsigned num_non_binary_clauses() const = 0; + virtual reslimit& rlimit() = 0; + virtual model const& get_model() const = 0; + virtual void collect_statistics(statistics& st) const = 0; + virtual double get_priority(bool_var v) const { return 0; } + + }; }; #endif diff --git a/src/sat/sat_unit_walk.cpp b/src/sat/sat_unit_walk.cpp index 8c7a6c6f9..3f7905872 100644 --- a/src/sat/sat_unit_walk.cpp +++ b/src/sat/sat_unit_walk.cpp @@ -45,8 +45,10 @@ namespace sat { while (m_head < m_vars.size()) { bool_var v = m_vars[m_head]; unsigned idx = literal(v, false).index(); - if (s.m_assignment[idx] == l_undef) + if (s.m_assignment[idx] == l_undef) { + // IF_VERBOSE(0, verbose_stream() << "pop " << v << "\n"); return v; + } ++m_head; } for (bool_var v : m_vars) { @@ -54,17 +56,21 @@ namespace sat { IF_VERBOSE(0, verbose_stream() << "unassigned: " << v << "\n"); } } + IF_VERBOSE(0, verbose_stream() << "#vars: " << m_vars.size() << "\n"); IF_VERBOSE(0, verbose_stream() << "(sat.unit-walk sat)\n"); return null_bool_var; } void unit_walk::var_priority::set_vars(solver& s) { m_vars.reset(); + s.pop_to_base_level(); + for (unsigned v = 0; v < s.num_vars(); ++v) { - if (!s.was_eliminated(v) && s.m_assignment[v] == l_undef) { + if (!s.was_eliminated(v) && s.value(v) == l_undef) { add(v); } } + IF_VERBOSE(0, verbose_stream() << "num vars " << m_vars.size() << "\n";); } bool_var unit_walk::var_priority::next(solver& s) { @@ -215,7 +221,7 @@ namespace sat { switch (is_sat) { case l_true: for (unsigned v = 0; v < s.num_vars(); ++v) { - s.m_assignment[v] = m_ls.get_phase(v) ? l_true : l_false; + s.m_assignment[v] = m_ls.get_best_phase(v) ? l_true : l_false; } return l_true; case l_false: @@ -239,8 +245,7 @@ namespace sat { local_search& ls; compare_break(local_search& ls): ls(ls) {} int operator()(bool_var v, bool_var w) const { - double diff = ls.break_count(v) - ls.break_count(w); - return diff > 0; + return ls.get_priority(v) > ls.get_priority(w); } }; @@ -249,22 +254,14 @@ namespace sat { std::sort(pqueue().begin(), pqueue().end(), cb); for (bool_var v : pqueue()) { m_phase_tf[v].update(m_ls.cur_solution(v) ? 100 : 0); - m_phase[v] = m_ls.cur_solution(v); + m_phase[v] = l_true == m_ls.cur_solution(v); } pqueue().rewind(); } void unit_walk::init_phase() { for (bool_var v : pqueue()) { - if (s.m_phase[v] == POS_PHASE) { - m_phase[v] = true; - } - else if (s.m_phase[v] == NEG_PHASE) { - m_phase[v] = false; - } - else { - m_phase[v] = m_rand(100) < m_phase_tf[v]; - } + m_phase[v] = s.m_phase[v]; } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 2eef102c9..8cda47983 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -421,7 +421,7 @@ namespace smt { return m_activity[v]; } - void set_activity(bool_var v, double const & act) { + void set_activity(bool_var v, double act) { m_activity[v] = act; } diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 53a3c4a24..fb1951680 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -165,11 +165,18 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p } catch (tactic_exception & ex) { reason_unknown = ex.msg(); + if (r.size() > 0) pr = r[0]->pr(0); return l_undef; } - TRACE("tactic_check_sat", + TRACE("tactic", tout << "r.size(): " << r.size() << "\n"; - for (unsigned i = 0; i < r.size(); i++) r[i]->display(tout);); + for (unsigned i = 0; i < r.size(); i++) r[i]->display_with_dependencies(tout);); + + if (r.size() > 0) { + pr = r[0]->pr(0); + TRACE("tactic", tout << pr << "\n";); + } + if (is_decided_sat(r)) { model_converter_ref mc = r[0]->mc(); @@ -192,7 +199,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p } else { if (models_enabled && !r.empty()) { - model_converter_ref mc = r[0]->mc(); + model_converter_ref mc = r[0]->mc(); model_converter2model(m, mc.get(), md); if (mc) (*mc)(labels); diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index 46d96d637..e501c53fa 100644 --- a/src/test/sat_local_search.cpp +++ b/src/test/sat_local_search.cpp @@ -46,7 +46,6 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea std::cout << "Objective function format error. They have different lengths.\n"; return false; } - // read the constraints, one at a time int k; @@ -124,6 +123,6 @@ void tst_sat_local_search(char ** argv, int argc, int& i) { cancel_eh eh(local_search.rlimit()); scoped_ctrl_c ctrlc(eh, false, true); scoped_timer timer(cutoff_time*1000, &eh); - local_search.check(); + local_search.check(0, nullptr, nullptr); }