From 76eed064ebca58884d57c3b28404537cee265949 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Oct 2017 22:19:05 -0700 Subject: [PATCH] bug fixes, prepare for retaining blocked clauses Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 15 +- src/sat/ba_solver.h | 2 +- src/sat/sat_clause.cpp | 1 + src/sat/sat_clause.h | 4 + src/sat/sat_clause_use_list.cpp | 16 +- src/sat/sat_clause_use_list.h | 57 +++-- src/sat/sat_elim_vars.cpp | 19 +- src/sat/sat_local_search.cpp | 2 +- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_simplifier.cpp | 346 +++++++++++++++++------------- src/sat/sat_simplifier.h | 10 +- src/sat/sat_simplifier_params.pyg | 2 + src/sat/sat_solver.cpp | 37 ++-- src/sat/sat_solver.h | 4 +- src/sat/sat_watched.h | 11 +- src/shell/dimacs_frontend.cpp | 39 +++- 16 files changed, 333 insertions(+), 234 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index ab2352253..a8a09d3ff 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2761,8 +2761,8 @@ namespace sat { } } - unsigned ba_solver::get_num_non_learned_bin(literal l) { - return s().m_simplifier.get_num_non_learned_bin(l); + unsigned ba_solver::get_num_unblocked_bin(literal l) { + return s().m_simplifier.get_num_unblocked_bin(l); } /* @@ -2831,8 +2831,8 @@ namespace sat { value(lit) == l_undef && use_count(lit) == 1 && use_count(~lit) == 1 && - get_num_non_learned_bin(lit) == 0 && - get_num_non_learned_bin(~lit) == 0) { + get_num_unblocked_bin(lit) == 0 && + get_num_unblocked_bin(~lit) == 0) { remove_constraint(c, "unused def"); } break; @@ -2876,7 +2876,7 @@ namespace sat { bool ba_solver::elim_pure(literal lit) { if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && - use_count(~lit) == 0 && get_num_non_learned_bin(~lit) == 0) { + use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) { IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";); s().assign(lit, justification()); return true; @@ -3163,9 +3163,12 @@ namespace sat { if (w.is_binary_clause() && is_marked(w.get_literal())) { ++m_stats.m_num_bin_subsumes; // IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";); - if (!w.is_binary_non_learned_clause()) { + if (w.is_learned()) { c1.set_learned(false); } + else if (w.is_blocked()) { + w.set_unblocked(); + } } else { if (it != it2) { diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 09903f889..16c853423 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -262,7 +262,7 @@ namespace sat { void mark_visited(literal l) { m_visited[l.index()] = true; } void unmark_visited(literal l) { m_visited[l.index()] = false; } bool is_marked(literal l) const { return m_visited[l.index()] != 0; } - unsigned get_num_non_learned_bin(literal l); + unsigned get_num_unblocked_bin(literal l); literal get_min_occurrence_literal(card const& c); void init_use_lists(); void remove_unused_defs(); diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 15c97b509..206dfcf40 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -29,6 +29,7 @@ namespace sat { m_capacity(sz), m_removed(false), m_learned(learned), + m_blocked(false), m_used(false), m_frozen(false), m_reinit_stack(false), diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 556385696..8fd7b52cf 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -46,6 +46,7 @@ namespace sat { unsigned m_used:1; unsigned m_frozen:1; unsigned m_reinit_stack:1; + unsigned m_blocked; unsigned m_inact_rounds:8; unsigned m_glue:8; unsigned m_psm:8; // transient field used during gc @@ -86,6 +87,9 @@ namespace sat { unsigned inact_rounds() const { return m_inact_rounds; } bool frozen() const { return m_frozen; } void freeze() { SASSERT(is_learned()); SASSERT(!frozen()); m_frozen = true; } + bool is_blocked() const { return m_blocked; } + void block() { SASSERT(!m_blocked); SASSERT(!is_learned()); m_blocked = true; } + void unblock() { SASSERT(m_blocked); SASSERT(!is_learned()); m_blocked = false; } void unfreeze() { SASSERT(is_learned()); SASSERT(frozen()); m_frozen = false; } static var_approx_set approx(unsigned num, literal const * lits); void set_glue(unsigned glue) { m_glue = glue > 255 ? 255 : glue; } diff --git a/src/sat/sat_clause_use_list.cpp b/src/sat/sat_clause_use_list.cpp index 5ee5b4cda..363ef784e 100644 --- a/src/sat/sat_clause_use_list.cpp +++ b/src/sat/sat_clause_use_list.cpp @@ -22,17 +22,20 @@ Revision History: namespace sat { bool clause_use_list::check_invariant() const { -#ifdef LAZY_USE_LIST unsigned sz = 0; - for (unsigned i = 0; i < m_clauses.size(); i++) - if (!m_clauses[i]->was_removed()) + for (clause* c : m_clauses) + if (!c->was_removed()) sz++; SASSERT(sz == m_size); -#endif + unsigned blocked = 0; + for (clause* c : m_clauses) + if (c->is_blocked()) + blocked++; + SASSERT(blocked == m_num_blocked); + return true; } -#ifdef LAZY_USE_LIST void clause_use_list::iterator::consume() { while (true) { if (m_i == m_size) @@ -44,14 +47,11 @@ namespace sat { m_i++; } } -#endif clause_use_list::iterator::~iterator() { -#ifdef LAZY_USE_LIST while (m_i < m_size) next(); m_clauses.shrink(m_j); -#endif } }; diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index 121345f21..08b50086a 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -24,30 +24,30 @@ Revision History: namespace sat { -#define LAZY_USE_LIST - /** \brief Clause use list with delayed deletion. */ class clause_use_list { clause_vector m_clauses; -#ifdef LAZY_USE_LIST unsigned m_size; -#endif + unsigned m_num_blocked; public: clause_use_list() { STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";); -#ifdef LAZY_USE_LIST m_size = 0; -#endif + m_num_blocked = 0; } unsigned size() const { -#ifdef LAZY_USE_LIST return m_size; -#else - return m_clauses.size(); -#endif + } + + unsigned num_blocked() const { + return m_num_blocked; + } + + unsigned non_blocked_size() const { + return m_size - m_num_blocked; } bool empty() const { return size() == 0; } @@ -57,58 +57,59 @@ namespace sat { SASSERT(!m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.push_back(&c); -#ifdef LAZY_USE_LIST m_size++; -#endif + if (c.is_blocked()) ++m_num_blocked; } void erase_not_removed(clause & c) { STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";); -#ifdef LAZY_USE_LIST SASSERT(m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; -#else - m_clauses.erase(&c); -#endif + if (c.is_blocked()) --m_num_blocked; } void erase(clause & c) { STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";); -#ifdef LAZY_USE_LIST SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; -#else - m_clauses.erase(&c); -#endif + if (c.is_blocked()) --m_num_blocked; + } + + void block(clause const& c) { + SASSERT(c.is_blocked()); + ++m_num_blocked; + SASSERT(check_invariant()); + } + + void unblock(clause const& c) { + SASSERT(!c.is_blocked()); + --m_num_blocked; + SASSERT(check_invariant()); } void reset() { m_clauses.finalize(); -#ifdef LAZY_USE_LIST m_size = 0; -#endif + m_num_blocked = 0; } bool check_invariant() const; // iterate & compress - class iterator { + class iterator { clause_vector & m_clauses; unsigned m_size; unsigned m_i; -#ifdef LAZY_USE_LIST unsigned m_j; void consume(); -#endif + public: iterator(clause_vector & v):m_clauses(v), m_size(v.size()), m_i(0) { -#ifdef LAZY_USE_LIST m_j = 0; consume(); -#endif } ~iterator(); bool at_end() const { return m_i == m_size; } @@ -117,10 +118,8 @@ namespace sat { SASSERT(!at_end()); SASSERT(!m_clauses[m_i]->was_removed()); m_i++; -#ifdef LAZY_USE_LIST m_j++; consume(); -#endif } }; diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 86954d037..59210a266 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -37,13 +37,13 @@ namespace sat{ literal pos_l(v, false); literal neg_l(v, true); - unsigned num_bin_pos = simp.get_num_non_learned_bin(pos_l); + unsigned num_bin_pos = simp.get_num_unblocked_bin(pos_l); if (num_bin_pos > m_max_literals) return false; - unsigned num_bin_neg = simp.get_num_non_learned_bin(neg_l); + unsigned num_bin_neg = simp.get_num_unblocked_bin(neg_l); if (num_bin_neg > m_max_literals) return false; clause_use_list & pos_occs = simp.m_use_list.get(pos_l); clause_use_list & neg_occs = simp.m_use_list.get(neg_l); - unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.size() + neg_occs.size(); + unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.non_blocked_size() + neg_occs.non_blocked_size(); if (clause_size == 0) { return false; } @@ -85,8 +85,8 @@ namespace sat{ // eliminate variable simp.m_pos_cls.reset(); simp.m_neg_cls.reset(); - simp.collect_clauses(pos_l, simp.m_pos_cls); - simp.collect_clauses(neg_l, simp.m_neg_cls); + simp.collect_clauses(pos_l, simp.m_pos_cls, false); + simp.collect_clauses(neg_l, simp.m_neg_cls, false); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); simp.save_clauses(mc_entry, simp.m_pos_cls); simp.save_clauses(mc_entry, simp.m_neg_cls); @@ -122,13 +122,13 @@ namespace sat{ TRACE("elim_vars", tout << "eliminate " << v << "\n"; for (watched const& w : simp.get_wlist(~pos_l)) { - if (w.is_binary_non_learned_clause()) { + if (w.is_binary_unblocked_clause()) { tout << pos_l << " " << w.get_literal() << "\n"; } } m.display(tout, b1); for (watched const& w : simp.get_wlist(~neg_l)) { - if (w.is_binary_non_learned_clause()) { + if (w.is_binary_unblocked_clause()) { tout << neg_l << " " << w.get_literal() << "\n"; } } @@ -294,7 +294,7 @@ namespace sat{ bool elim_vars::mark_literals(literal lit) { watch_list& wl = simp.get_wlist(lit); for (watched const& w : wl) { - if (w.is_binary_non_learned_clause()) { + if (w.is_binary_unblocked_clause()) { mark_var(w.get_literal().var()); } } @@ -306,6 +306,7 @@ namespace sat{ clause_use_list::iterator it = occs.mk_iterator(); while (!it.at_end()) { clause const& c = it.curr(); + if (c.is_blocked()) continue; bdd cl = m.mk_false(); for (literal l : c) { cl |= mk_literal(l); @@ -320,7 +321,7 @@ namespace sat{ bdd result = m.mk_true(); watch_list& wl = simp.get_wlist(~lit); for (watched const& w : wl) { - if (w.is_binary_non_learned_clause()) { + if (w.is_binary_unblocked_clause()) { result &= (mk_literal(lit) || mk_literal(w.get_literal())); } } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 5cc19a174..3a9e48182 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -304,7 +304,7 @@ namespace sat { watch_list::const_iterator it = wlist.begin(); watch_list::const_iterator end = wlist.end(); for (; it != end; ++it) { - if (!it->is_binary_non_learned_clause()) + if (!it->is_binary_unblocked_clause()) continue; literal l2 = it->get_literal(); if (l1.index() > l2.index()) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 4bb7ba180..ff2bac39f 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -965,7 +965,7 @@ namespace sat { if (m_s.was_eliminated(l.var())) continue; watch_list const & wlist = m_s.m_watches[l_idx]; for (auto& w : wlist) { - if (!w.is_binary_non_learned_clause()) + if (!w.is_binary_clause()) continue; literal l2 = w.get_literal(); if (l.index() < l2.index() && !m_s.was_eliminated(l2.var())) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index cd46f1916..b0ef9e3e9 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -34,26 +34,29 @@ namespace sat { } void use_list::insert(clause & c) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - m_use_list[c[i].index()].insert(c); - } + for (literal l : c) + m_use_list[l.index()].insert(c); } void use_list::erase(clause & c) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - m_use_list[c[i].index()].erase(c); - } + for (literal l : c) + m_use_list[l.index()].erase(c); } void use_list::erase(clause & c, literal l) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - literal l2 = c[i]; + for (literal l2 : c) if (l2 != l) m_use_list[l2.index()].erase(c); - } + } + + void use_list::block(clause& c) { + for (literal l : c) + m_use_list[l.index()].block(c); + } + + void use_list::unblock(clause& c) { + for (literal l : c) + m_use_list[l.index()].unblock(c); } simplifier::simplifier(solver & _s, params_ref const & p): @@ -99,9 +102,8 @@ namespace sat { } inline void simplifier::remove_clause_core(clause & c) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) - insert_elim_todo(c[i].var()); + for (literal l : c) + insert_elim_todo(l.var()); m_sub_todo.erase(c); c.set_removed(true); TRACE("resolution_bug", tout << "del_clause: " << c << "\n";); @@ -118,6 +120,20 @@ namespace sat { m_use_list.erase(c, l); } + inline void simplifier::block_clause(clause & c) { +#if 1 + remove_clause(c); +#else + c.block(); + m_use_list.block(c); +#endif + } + + inline void simplifier::unblock_clause(clause & c) { + c.unblock(); + m_use_list.unblock(c); + } + inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) { SASSERT(s.get_wlist(~l1).contains(watched(l2, learned))); s.get_wlist(~l1).erase(watched(l2, learned)); @@ -238,10 +254,7 @@ namespace sat { \brief Eliminate all ternary and clause watches. */ void simplifier::cleanup_watches() { - vector::iterator it = s.m_watches.begin(); - vector::iterator end = s.m_watches.end(); - for (; it != end; ++it) { - watch_list & wlist = *it; + for (watch_list& wlist : s.m_watches) { watch_list::iterator it2 = wlist.begin(); watch_list::iterator itprev = it2; watch_list::iterator end2 = wlist.end(); @@ -345,11 +358,9 @@ namespace sat { \brief Return the variable in c with the minimal number positive+negative occurrences. */ bool_var simplifier::get_min_occ_var(clause const & c) const { - literal l_best = c[0]; - unsigned best = m_use_list.get(l_best).size() + m_use_list.get(~l_best).size(); - unsigned sz = c.size(); - for (unsigned i = 1; i < sz; i++) { - literal l = c[i]; + literal l_best = null_literal; + unsigned best = UINT_MAX; + for (literal l : c) { unsigned num = m_use_list.get(l).size() + m_use_list.get(~l).size(); if (num < best) { l_best = l; @@ -394,6 +405,7 @@ namespace sat { */ void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits, literal target) { + if (c1.is_blocked()) return; clause_use_list const & cs = m_use_list.get(target); clause_use_list::iterator it = cs.mk_iterator(); while (!it.at_end()) { @@ -424,7 +436,7 @@ namespace sat { } /** - \brief Perform backward subsumption and self-subsumption resolution using c. + \brief Perform backward subsumption and self-subsumption resolution using c1. */ void simplifier::back_subsumption1(clause & c1) { m_bs_cs.reset(); @@ -440,11 +452,13 @@ namespace sat { // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) c1.unset_learned(); + else if (c1.is_blocked() && !c2.is_learned() && !c2.is_blocked()) + unblock_clause(c1); TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); remove_clause(c2); m_num_subsumed++; } - else if (!c2.was_removed()) { + else if (!c2.was_removed() && !c1.is_blocked()) { // subsumption resolution TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";); elim_lit(c2, *l_it); @@ -466,11 +480,9 @@ namespace sat { \brief Return the literal in c with the minimal number of occurrences. */ literal simplifier::get_min_occ_var0(clause const & c) const { - literal l_best = c[0]; - unsigned best = m_use_list.get(l_best).size(); - unsigned sz = c.size(); - for (unsigned i = 1; i < sz; i++) { - literal l = c[i]; + literal l_best = null_literal; + unsigned best = UINT_MAX; + for (literal l : c) { unsigned num = m_use_list.get(l).size(); if (num < best) { l_best = l; @@ -485,21 +497,19 @@ namespace sat { Otherwise return false */ bool simplifier::subsumes0(clause const & c1, clause const & c2) { - unsigned sz2 = c2.size(); - for (unsigned i = 0; i < sz2; i++) - mark_visited(c2[i]); + for (literal l : c2) + mark_visited(l); bool r = true; - unsigned sz1 = c1.size(); - for (unsigned i = 0; i < sz1; i++) { - if (!is_marked(c1[i])) { + for (literal l : c1) { + if (!is_marked(l)) { r = false; break; } } - for (unsigned i = 0; i < sz2; i++) - unmark_visited(c2[i]); + for (literal l : c2) + unmark_visited(l); return r; } @@ -508,6 +518,7 @@ namespace sat { \brief Collect the clauses subsumed by c1 (using the occurrence list of target). */ void simplifier::collect_subsumed0_core(clause const & c1, clause_vector & out, literal target) { + if (c1.is_blocked()) return; clause_use_list const & cs = m_use_list.get(target); clause_use_list::iterator it = cs.mk_iterator(); while (!it.at_end()) { @@ -540,10 +551,8 @@ namespace sat { void simplifier::back_subsumption0(clause & c1) { m_bs_cs.reset(); collect_subsumed0(c1, m_bs_cs); - clause_vector::iterator it = m_bs_cs.begin(); - clause_vector::iterator end = m_bs_cs.end(); - for (; it != end; ++it) { - clause & c2 = *(*it); + for (clause* cp : m_bs_cs) { + clause & c2 = *cp; // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) c1.unset_learned(); @@ -951,13 +960,17 @@ namespace sat { return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); } - void operator()(unsigned num_vars) { + void insert_queue(unsigned num_vars) { for (bool_var v = 0; v < num_vars; v++) { if (process_var(v)) { insert(literal(v, false)); insert(literal(v, true)); } } + } + + void block_clauses(unsigned num_vars) { + insert_queue(num_vars); while (!m_queue.empty()) { s.checkpoint(); if (m_counter < 0) @@ -965,7 +978,73 @@ namespace sat { literal l = m_queue.next(); process(l); } - cce(); + } + + void operator()(unsigned num_vars) { + block_clauses(num_vars); + if (s.m_elim_covered_clauses) + cce(); + } + + void process(literal l) { + TRACE("blocked_clause", tout << "processing: " << l << "\n";); + model_converter::entry * new_entry = 0; + if (!process_var(l.var())) { + return; + } + + literal blocked = null_literal; + m_to_remove.reset(); + { + clause_use_list & occs = s.m_use_list.get(l); + clause_use_list::iterator it = occs.mk_iterator(); + while (!it.at_end()) { + clause & c = it.curr(); + if (c.is_blocked()) continue; + m_counter -= c.size(); + SASSERT(c.contains(l)); + s.mark_all_but(c, l); + if (all_tautology(l)) { + block_clause(c, l, new_entry); + s.m_num_blocked_clauses++; + } + s.unmark_all(c); + it.next(); + } + } + for (clause* c : m_to_remove) + s.block_clause(*c); + + { + watch_list & wlist = s.get_wlist(~l); + m_counter -= wlist.size(); + watch_list::iterator it = wlist.begin(); + watch_list::iterator it2 = it; + watch_list::iterator end = wlist.end(); + for (; it != end; ++it) { + if (!it->is_binary_clause() || it->is_blocked()) { + *it2 = *it; + it2++; + continue; + } + literal l2 = it->get_literal(); + s.mark_visited(l2); + if (all_tautology(l)) { + block_binary(it, l, new_entry); + s.m_num_blocked_clauses++; + } + else if (s.m_elim_covered_clauses && cce(l, l2, blocked)) { + block_covered_binary(it, l, blocked); + s.m_num_covered_clauses++; + } + else { + *it2 = *it; + it2++; + } + s.unmark_visited(l2); + } + wlist.set_end(it2); + } } // @@ -976,7 +1055,7 @@ namespace sat { if (!process_var(l.var())) return false; bool first = true; for (watched & w : s.get_wlist(l)) { - if (w.is_binary_non_learned_clause()) { + if (w.is_binary_unblocked_clause()) { literal lit = w.get_literal(); if (s.is_marked(~lit) && lit != ~l) continue; if (!first) { @@ -992,6 +1071,7 @@ namespace sat { while (!it.at_end()) { bool tautology = false; clause & c = it.curr(); + if (c.is_blocked()) continue; for (literal lit : c) { if (s.is_marked(~lit) && lit != ~l) { tautology = true; @@ -1007,16 +1087,9 @@ namespace sat { } else { unsigned j = 0; - unsigned sz = inter.size(); - for (unsigned i = 0; i < sz; ++i) { - literal lit1 = inter[i]; - for (literal lit2 : c) { - if (lit1 == lit2) { - inter[j++] = lit1; - break; - } - } - } + for (literal lit : inter) + if (c.contains(lit)) + inter[j++] = lit; inter.shrink(j); if (j == 0) return false; } @@ -1052,6 +1125,14 @@ namespace sat { } } + + /* + * C \/ l ~l \/ lit \/ D_i for i = 1...N all the clauses that have ~l + * ------------------------- + * C \/ l \/ lit + * + * + */ bool add_cla(literal& blocked) { for (unsigned i = 0; i < m_covered_clause.size(); ++i) { m_intersection.reset(); @@ -1059,15 +1140,15 @@ namespace sat { blocked = m_covered_clause[i]; return true; } + if (!m_intersection.empty()) { + m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i])); + } for (literal l : m_intersection) { if (!s.is_marked(l)) { s.mark_visited(l); m_covered_clause.push_back(l); } } - if (!m_intersection.empty()) { - m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i])); - } } return false; } @@ -1085,14 +1166,18 @@ namespace sat { is_tautology = add_cla(blocked); } while (m_covered_clause.size() > sz && !is_tautology); +#if 1 break; - //if (is_tautology) break; - //sz = m_covered_clause.size(); - // unsound? add_ala(); +#else + // check for soundness? + if (is_tautology) break; + sz = m_covered_clause.size(); + add_ala(); +#endif } while (m_covered_clause.size() > sz); for (literal l : m_covered_clause) s.unmark_visited(l); - // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n"; + if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n"; return is_tautology; } @@ -1105,9 +1190,9 @@ namespace sat { return cla(blocked); } - bool cce(literal lit, literal l2, literal& blocked) { + bool cce(literal l1, literal l2, literal& blocked) { m_covered_clause.reset(); - m_covered_clause.push_back(lit); + m_covered_clause.push_back(l1); m_covered_clause.push_back(l2); return cla(blocked); } @@ -1117,79 +1202,17 @@ namespace sat { literal blocked; for (clause* cp : s.s.m_clauses) { clause& c = *cp; - if (c.was_removed()) continue; - if (cce(c, blocked)) { - model_converter::entry * new_entry = 0; - block_covered_clause(c, blocked, new_entry); + if (!c.was_removed() && !c.is_blocked() && cce(c, blocked)) { + block_covered_clause(c, blocked); s.m_num_covered_clauses++; } } for (clause* c : m_to_remove) { - s.remove_clause(*c); + s.block_clause(*c); } m_to_remove.reset(); } - void process(literal l) { - TRACE("blocked_clause", tout << "processing: " << l << "\n";); - model_converter::entry * new_entry = 0; - if (!process_var(l.var())) { - return; - } - - literal blocked = null_literal; - m_to_remove.reset(); - { - clause_use_list & occs = s.m_use_list.get(l); - clause_use_list::iterator it = occs.mk_iterator(); - while (!it.at_end()) { - clause & c = it.curr(); - m_counter -= c.size(); - SASSERT(c.contains(l)); - s.mark_all_but(c, l); - if (all_tautology(l)) { - block_clause(c, l, new_entry); - s.m_num_blocked_clauses++; - } - s.unmark_all(c); - it.next(); - } - } - for (clause* c : m_to_remove) { - s.remove_clause(*c); - } - { - watch_list & wlist = s.get_wlist(~l); - m_counter -= wlist.size(); - watch_list::iterator it = wlist.begin(); - watch_list::iterator it2 = it; - watch_list::iterator end = wlist.end(); - for (; it != end; ++it) { - if (!it->is_binary_clause()) { - *it2 = *it; - it2++; - continue; - } - literal l2 = it->get_literal(); - s.mark_visited(l2); - if (all_tautology(l)) { - block_binary(it, l, new_entry); - s.m_num_blocked_clauses++; - } - else if (cce(l, l2, blocked)) { - model_converter::entry * blocked_entry = 0; - block_covered_binary(it, l, blocked, blocked_entry); - s.m_num_covered_clauses++; - } - else { - *it2 = *it; - it2++; - } - s.unmark_visited(l2); - } - wlist.set_end(it2); - } - } void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) { TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); @@ -1208,7 +1231,8 @@ namespace sat { mc.insert(*new_entry, c); } - void block_covered_clause(clause& c, literal l, model_converter::entry *& new_entry) { + void block_covered_clause(clause& c, literal l) { + model_converter::entry * new_entry = 0; prepare_block_clause(c, l, new_entry); mc.insert(*new_entry, m_covered_clause, m_elim_stack); } @@ -1227,7 +1251,8 @@ namespace sat { mc.insert(*new_entry, l, it->get_literal()); } - void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { + void block_covered_binary(watch_list::iterator it, literal l, literal blocked) { + model_converter::entry * new_entry = 0; prepare_block_binary(it, l, blocked, new_entry); mc.insert(*new_entry, m_covered_clause, m_elim_stack); } @@ -1236,7 +1261,7 @@ namespace sat { watch_list & wlist = s.get_wlist(l); m_counter -= wlist.size(); for (auto const& w : wlist) { - if (w.is_binary_non_learned_clause() && + if (w.is_binary_unblocked_clause() && !s.is_marked(~w.get_literal())) return false; } @@ -1245,6 +1270,7 @@ namespace sat { clause_use_list::iterator it = neg_occs.mk_iterator(); while (!it.at_end()) { clause & c = it.curr(); + if (c.is_blocked()) continue; m_counter -= c.size(); unsigned sz = c.size(); unsigned i; @@ -1300,11 +1326,11 @@ namespace sat { elim(s.num_vars()); } - unsigned simplifier::get_num_non_learned_bin(literal l) const { + unsigned simplifier::get_num_unblocked_bin(literal l) const { unsigned r = 0; watch_list const & wlist = get_wlist(~l); for (auto & w : wlist) { - if (w.is_binary_non_learned_clause()) + if (w.is_binary_unblocked_clause()) r++; } return r; @@ -1315,8 +1341,8 @@ namespace sat { literal neg_l(v, true); unsigned num_pos = m_use_list.get(pos_l).size(); unsigned num_neg = m_use_list.get(neg_l).size(); - unsigned num_bin_pos = get_num_non_learned_bin(pos_l); - unsigned num_bin_neg = get_num_non_learned_bin(neg_l); + unsigned num_bin_pos = get_num_unblocked_bin(pos_l); + unsigned num_bin_neg = get_num_unblocked_bin(neg_l); unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos; CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";); @@ -1353,20 +1379,32 @@ namespace sat { /** \brief Collect clauses and binary clauses containing l. */ - void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) { + void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) { clause_use_list const & cs = m_use_list.get(l); clause_use_list::iterator it = cs.mk_iterator(); while (!it.at_end()) { - r.push_back(clause_wrapper(it.curr())); - SASSERT(r.back().size() == it.curr().size()); + if (!it.curr().is_blocked() || include_blocked) { + r.push_back(clause_wrapper(it.curr())); + SASSERT(r.back().size() == it.curr().size()); + } it.next(); } watch_list & wlist = get_wlist(~l); - for (auto & w : wlist) { - if (w.is_binary_non_learned_clause()) { - r.push_back(clause_wrapper(l, w.get_literal())); - SASSERT(r.back().size() == 2); + if (include_blocked) { + for (auto & w : wlist) { + if (w.is_binary_non_learned_clause2()) { + r.push_back(clause_wrapper(l, w.get_literal())); + SASSERT(r.back().size() == 2); + } + } + } + else { + for (auto & w : wlist) { + if (w.is_binary_unblocked_clause()) { + r.push_back(clause_wrapper(l, w.get_literal())); + SASSERT(r.back().size() == 2); + } } } } @@ -1503,12 +1541,12 @@ namespace sat { literal pos_l(v, false); literal neg_l(v, true); - unsigned num_bin_pos = get_num_non_learned_bin(pos_l); - unsigned num_bin_neg = get_num_non_learned_bin(neg_l); + unsigned num_bin_pos = get_num_unblocked_bin(pos_l); + unsigned num_bin_neg = get_num_unblocked_bin(neg_l); clause_use_list & pos_occs = m_use_list.get(pos_l); clause_use_list & neg_occs = m_use_list.get(neg_l); - unsigned num_pos = pos_occs.size() + num_bin_pos; - unsigned num_neg = neg_occs.size() + num_bin_neg; + unsigned num_pos = pos_occs.non_blocked_size() + num_bin_pos; + unsigned num_neg = neg_occs.non_blocked_size() + num_bin_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); @@ -1520,7 +1558,8 @@ namespace sat { { clause_use_list::iterator it = pos_occs.mk_iterator(); while (!it.at_end()) { - before_lits += it.curr().size(); + if (!it.curr().is_blocked()) + before_lits += it.curr().size(); it.next(); } } @@ -1528,7 +1567,8 @@ namespace sat { { clause_use_list::iterator it2 = neg_occs.mk_iterator(); while (!it2.at_end()) { - before_lits += it2.curr().size(); + if (!it2.curr().is_blocked()) + before_lits += it2.curr().size(); it2.next(); } } @@ -1546,8 +1586,8 @@ namespace sat { m_pos_cls.reset(); m_neg_cls.reset(); - collect_clauses(pos_l, m_pos_cls); - collect_clauses(neg_l, m_neg_cls); + collect_clauses(pos_l, m_pos_cls, false); + collect_clauses(neg_l, m_neg_cls, false); TRACE("resolution_detail", tout << "collecting number of after_clauses\n";); @@ -1676,6 +1716,7 @@ namespace sat { void simplifier::updt_params(params_ref const & _p) { sat_simplifier_params p(_p); + m_elim_covered_clauses = p.elim_covered_clauses(); m_elim_blocked_clauses = p.elim_blocked_clauses(); m_elim_blocked_clauses_at = p.elim_blocked_clauses_at(); m_blocked_clause_limit = p.blocked_clause_limit(); @@ -1693,6 +1734,7 @@ namespace sat { m_subsumption = p.subsumption(); m_subsumption_limit = p.subsumption_limit(); m_elim_vars = p.elim_vars(); + m_elim_vars_bdd = p.elim_vars_bdd(); } void simplifier::collect_param_descrs(param_descrs & r) { diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index fdfabb513..d58babfef 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -40,6 +40,8 @@ namespace sat { public: void init(unsigned num_vars); void insert(clause & c); + void block(clause & c); + void unblock(clause & c); void erase(clause & c); void erase(clause & c, literal l); clause_use_list & get(literal l) { return m_use_list[l.index()]; } @@ -69,6 +71,7 @@ namespace sat { int m_elim_counter; // config + bool m_elim_covered_clauses; bool m_elim_blocked_clauses; unsigned m_elim_blocked_clauses_at; unsigned m_blocked_clause_limit; @@ -87,6 +90,7 @@ namespace sat { bool m_subsumption; unsigned m_subsumption_limit; bool m_elim_vars; + bool m_elim_vars_bdd; // stats unsigned m_num_blocked_clauses; @@ -119,6 +123,8 @@ namespace sat { void remove_clause_core(clause & c); void remove_clause(clause & c); void remove_clause(clause & c, literal l); + void block_clause(clause & c); + void unblock_clause(clause & c); void remove_bin_clause_half(literal l1, literal l2, bool learned); bool_var get_min_occ_var(clause const & c) const; @@ -157,10 +163,10 @@ namespace sat { struct blocked_clause_elim; void elim_blocked_clauses(); - unsigned get_num_non_learned_bin(literal l) const; + unsigned get_num_unblocked_bin(literal l) const; unsigned get_to_elim_cost(bool_var v) const; void order_vars_for_elim(bool_var_vector & r); - void collect_clauses(literal l, clause_wrapper_vector & r); + void collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked); clause_wrapper_vector m_pos_cls; clause_wrapper_vector m_neg_cls; literal_vector m_new_cls; diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index ff2944987..9a7812586 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -2,6 +2,7 @@ def_module_params(module_name='sat', class_name='sat_simplifier_params', export=True, params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'), + ('elim_covered_clauses', BOOL, False, 'eliminate covered clauses'), ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'), ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'), ('resolution', BOOL, True, 'eliminate boolean variables using resolution'), @@ -16,5 +17,6 @@ def_module_params(module_name='sat', ('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('elim_vars', BOOL, True, 'enable variable elimination during simplification'), + ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'), ('subsumption', BOOL, True, 'eliminate subsumed clauses'), ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index ca1fc7801..1b117b0a7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -117,7 +117,7 @@ namespace sat { assign(src.m_trail[i], justification()); } - // copy binary clauses + // copy binary clauses that are unblocked. { unsigned sz = src.m_watches.size(); for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { @@ -125,7 +125,7 @@ namespace sat { if (src.was_eliminated(l.var())) continue; watch_list const & wlist = src.m_watches[l_idx]; for (auto & wi : wlist) { - if (!wi.is_binary_non_learned_clause()) + if (!wi.is_binary_unblocked_clause()) continue; literal l2 = wi.get_literal(); if (l.index() > l2.index() || @@ -142,7 +142,10 @@ namespace sat { for (clause* c : src.m_clauses) { buffer.reset(); for (literal l : *c) buffer.push_back(l); - mk_clause_core(buffer); + clause* c1 = mk_clause_core(buffer); + if (c1 && c->is_blocked()) { + c1->block(); + } } // copy high quality lemmas for (clause* c : src.m_learned) { @@ -1558,8 +1561,8 @@ namespace sat { m_mc(m_model); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); -#ifndef _EXTERNAL_RELEASE - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model\"\n";); +// #ifndef _EXTERNAL_RELEASE + IF_VERBOSE(1, verbose_stream() << "\"checking model\"\n";); if (!check_model(m_model)) throw solver_exception("check model failed"); @@ -1568,7 +1571,7 @@ namespace sat { if (!m_clone->check_model(m_model)) throw solver_exception("check model failed (for cloned solver)"); } -#endif +// #endif } bool solver::check_model(model const & m) const { @@ -3124,17 +3127,14 @@ namespace sat { for (unsigned l_idx = 0; l_idx < sz; l_idx++) { literal l = to_literal(l_idx); l.neg(); - watch_list const & wlist = m_watches[l_idx]; - watch_list::const_iterator it = wlist.begin(); - watch_list::const_iterator end = wlist.end(); - for (; it != end; ++it) { - if (!it->is_binary_clause()) + for (watched const& w : m_watches[l_idx]) { + if (!w.is_binary_clause()) continue; - if (!learned && it->is_learned()) + if (!learned && w.is_learned()) continue; - else if (learned && learned_only && !it->is_learned()) + else if (learned && learned_only && !w.is_learned()) continue; - literal l2 = it->get_literal(); + literal l2 = w.get_literal(); if (l.index() > l2.index()) continue; TRACE("cleanup_bug", tout << "collected: " << l << " " << l2 << "\n";); @@ -3168,13 +3168,10 @@ namespace sat { for (unsigned l_idx = 0; l_idx < sz; l_idx++) { literal l = to_literal(l_idx); l.neg(); - watch_list const & wlist = m_watches[l_idx]; - watch_list::const_iterator it = wlist.begin(); - watch_list::const_iterator end = wlist.end(); - for (; it != end; ++it) { - if (!it->is_binary_clause()) + for (watched const& w : m_watches[l_idx]) { + if (!w.is_binary_clause()) continue; - literal l2 = it->get_literal(); + literal l2 = w.get_literal(); if (l.index() > l2.index()) continue; out << "(" << l << " " << l2 << ")\n"; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 58d2824c7..2c5a04104 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -220,8 +220,8 @@ namespace sat { protected: void del_clause(clause & c); clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned); - void mk_clause_core(literal_vector const& lits) { mk_clause_core(lits.size(), lits.c_ptr()); } - void mk_clause_core(unsigned num_lits, literal * lits) { mk_clause_core(num_lits, lits, false); } + clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); } + clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); } void mk_clause_core(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_clause_core(2, lits); } void mk_bin_clause(literal l1, literal l2, bool learned); bool propagate_bin_clause(literal l1, literal l2); diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index d1333c314..f18e08999 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -50,7 +50,7 @@ namespace sat { SASSERT(is_binary_clause()); SASSERT(get_literal() == l); SASSERT(is_learned() == learned); - SASSERT(learned || is_binary_non_learned_clause()); + SASSERT(learned || is_binary_unblocked_clause()); } watched(literal l1, literal l2) { @@ -85,8 +85,15 @@ namespace sat { literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(static_cast(m_val1)); } void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); } bool is_learned() const { SASSERT(is_binary_clause()); return (m_val2 >> 2) == 1; } - bool is_binary_non_learned_clause() const { return m_val2 == 0; } + + bool is_binary_unblocked_clause() const { return m_val2 == 0; } + bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); } + bool is_binary_non_learned_clause2() const { return is_binary_clause() && !is_learned(); } + void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast(BINARY); SASSERT(!is_learned()); } + void set_blocked() { SASSERT(is_binary_clause()); SASSERT(!is_learned()); m_val2 |= (1 << 3); } + bool is_blocked() const { SASSERT(is_binary_clause()); return 0 != (m_val2 & (1 << 3)); } + void set_unblocked() { SASSERT(is_binary_clause()); SASSERT(is_blocked()); m_val2 &= ~(1u << 3u); } bool is_ternary_clause() const { return get_kind() == TERNARY; } literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast(m_val1)); } diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index c47da9b1f..50c542043 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -21,9 +21,9 @@ Revision History: #include #include "util/timeout.h" #include "util/rlimit.h" +#include "util/gparams.h" #include "sat/dimacs.h" #include "sat/sat_solver.h" -#include "util/gparams.h" extern bool g_display_statistics; static sat::solver * g_solver = 0; @@ -126,6 +126,42 @@ static void track_clauses(sat::solver const& src, } } +void verify_solution(char const * file_name) { + params_ref p = gparams::get_module("sat"); + p.set_bool("produce_models", true); + reslimit limit; + sat::solver solver(p, limit); + std::ifstream in(file_name); + if (in.bad() || in.fail()) { + std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; + exit(ERR_OPEN_FILE); + } + parse_dimacs(in, solver); + + sat::model const & m = g_solver->get_model(); + for (unsigned i = 1; i < m.size(); i++) { + sat::literal lit(i, false); + switch (m[i]) { + case l_false: lit.neg(); break; + case l_undef: break; + case l_true: break; + } + solver.mk_clause(1, &lit); + } + lbool r = solver.check(); + switch (r) { + case l_false: + std::cout << "model checking failed\n"; + break; + case l_true: + std::cout << "model validated\n"; + break; + default: + std::cout << "inconclusive model\n"; + break; + } +} + unsigned read_dimacs(char const * file_name) { g_start_time = clock(); register_on_timeout_proc(on_timeout); @@ -164,6 +200,7 @@ unsigned read_dimacs(char const * file_name) { switch (r) { case l_true: std::cout << "sat\n"; + if (file_name) verify_solution(file_name); display_model(*g_solver); break; case l_undef: