From 5a2b072ddf781e9b1205935e4a68ff3ed166441e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Jan 2018 20:32:06 -0800 Subject: [PATCH] working on completing ATE/ALA for acce and abce Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 15 +- src/sat/ba_solver.h | 5 +- src/sat/sat_asymm_branch.cpp | 63 +++++-- src/sat/sat_asymm_branch.h | 8 +- src/sat/sat_asymm_branch_params.pyg | 2 +- src/sat/sat_big.cpp | 47 ++++- src/sat/sat_big.h | 19 +- src/sat/sat_clause.cpp | 2 - src/sat/sat_clause.h | 15 +- src/sat/sat_clause_use_list.cpp | 8 +- src/sat/sat_clause_use_list.h | 30 +-- src/sat/sat_cleaner.cpp | 3 +- src/sat/sat_config.cpp | 4 +- src/sat/sat_elim_vars.cpp | 14 +- src/sat/sat_extension.h | 2 +- src/sat/sat_iff3_finder.cpp | 2 +- src/sat/sat_integrity_checker.cpp | 12 +- src/sat/sat_lookahead.cpp | 35 ++-- src/sat/sat_lookahead.h | 6 +- src/sat/sat_params.pyg | 4 +- src/sat/sat_scc.cpp | 38 +--- src/sat/sat_scc.h | 8 +- src/sat/sat_scc_params.pyg | 2 +- src/sat/sat_simplifier.cpp | 282 +++++++++++++++++++++------- src/sat/sat_simplifier.h | 2 + src/sat/sat_simplifier_params.pyg | 2 +- src/sat/sat_solver.cpp | 52 +++-- src/sat/sat_solver.h | 1 + src/sat/sat_watched.h | 13 +- 29 files changed, 466 insertions(+), 230 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index d29f81fca..55a7713ce 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -3282,21 +3282,26 @@ namespace sat { extension* ba_solver::copy(solver* s) { ba_solver* result = alloc(ba_solver); result->set_solver(s); - copy_core(result); + copy_core(result, false); return result; } - extension* ba_solver::copy(lookahead* s) { + extension* ba_solver::copy(lookahead* s, bool learned) { ba_solver* result = alloc(ba_solver); result->set_lookahead(s); - copy_core(result); + copy_core(result, learned); return result; } - void ba_solver::copy_core(ba_solver* result) { + void ba_solver::copy_core(ba_solver* result, bool learned) { + copy_constraints(result, m_constraints); + if (learned) copy_constraints(result, m_learned); + } + + void ba_solver::copy_constraints(ba_solver* result, ptr_vector const& constraints) { literal_vector lits; svector wlits; - for (constraint* cp : m_constraints) { + for (constraint* cp : constraints) { switch (cp->tag()) { case card_t: { card const& c = cp->to_card(); diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 6e5c00e38..d950cb8cc 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -462,7 +462,8 @@ namespace sat { constraint* add_pb_ge(literal l, svector const& wlits, unsigned k, bool learned); constraint* add_xor(literal_vector const& lits, bool learned); - void copy_core(ba_solver* result); + void copy_core(ba_solver* result, bool learned); + void copy_constraints(ba_solver* result, ptr_vector const& constraints); public: ba_solver(); virtual ~ba_solver(); @@ -489,7 +490,7 @@ namespace sat { virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const; virtual void collect_statistics(statistics& st) const; virtual extension* copy(solver* s); - virtual extension* copy(lookahead* s); + virtual extension* copy(lookahead* s, bool learned); virtual void find_mutexes(literal_vector& lits, vector & mutexes); virtual void pop_reinit(); virtual void gc(); diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index dfe94c5f4..1b37e4dbc 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -67,22 +67,28 @@ namespace sat { } }; - bool asymm_branch::process(big* big) { + void asymm_branch::process_bin(big& big) { + unsigned elim = big.reduce_tr(s); + m_hidden_tautologies += elim; + } + + bool asymm_branch::process(big& big, bool learned) { unsigned elim0 = m_elim_literals; unsigned eliml0 = m_elim_learned_literals; for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) { - unsigned elim = m_elim_literals; - if (big) big->init_big(s, true); - process(big, s.m_clauses); - if (big) process(big, s.m_learned); + unsigned elim = m_elim_literals + m_hidden_tautologies; + big.init(s, learned); + process(&big, s.m_clauses); + process(&big, s.m_learned); + process_bin(big); s.propagate(false); if (s.m_inconsistent) break; - unsigned num_elim = m_elim_literals - elim; + unsigned num_elim = m_elim_literals + m_hidden_tautologies - elim; IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";); if (num_elim == 0) break; - if (num_elim > 1000) + if (num_elim > 100) i = 0; } IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) @@ -90,6 +96,16 @@ namespace sat { return m_elim_literals > elim0; } + bool asymm_branch::process(bool learned) { + unsigned eliml0 = m_elim_learned_literals; + unsigned elim = m_elim_literals; + process(nullptr, s.m_clauses); + s.propagate(false); + IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) + verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";); + return m_elim_literals > elim; + } + void asymm_branch::process(big* big, clause_vector& clauses) { int64 limit = -m_asymm_branch_limit; @@ -138,10 +154,22 @@ namespace sat { s.propagate(false); if (s.m_inconsistent) return; - report rpt(*this); - svector saved_phase(s.m_phase); - process(&big); - s.m_phase = saved_phase; + report rpt(*this); + + for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) { + unsigned elim = m_elim_literals; + big.reinit(); + process(&big, s.m_clauses); + process(&big, s.m_learned); + process_bin(big); + unsigned num_elim = m_elim_literals - elim; + IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";); + if (num_elim == 0) + break; + if (num_elim > 1000) + i = 0; + } + s.propagate(false); } void asymm_branch::operator()(bool force) { @@ -168,12 +196,16 @@ namespace sat { ++counter; change = false; if (m_asymm_branch_sampled) { - big big; - if (process(&big)) change = true; + big big(s.m_rand, true); + if (process(big, true)) change = true; + } + if (m_asymm_branch_sampled) { + big big(s.m_rand, false); + if (process(big, false)) change = true; } if (m_asymm_branch) { m_counter = 0; - if (process(nullptr)) change = true; + if (process(true)) change = true; m_counter = -m_counter; } } @@ -399,7 +431,7 @@ namespace sat { bool asymm_branch::process_sampled(big& big, clause & c) { scoped_detach scoped_d(s, c); sort(big, c); - if (c.is_learned() && uhte(big, c)) { + if ((c.is_learned() || !big.learned()) && uhte(big, c)) { ++m_hidden_tautologies; scoped_d.del_clause(); return false; @@ -408,7 +440,6 @@ namespace sat { } bool asymm_branch::process(clause & c) { - if (c.is_blocked()) return true; TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";); SASSERT(s.scope_lvl() == 0); SASSERT(s.m_qhead == s.m_trail.size()); diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 226684c85..fb8048c37 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -66,7 +66,9 @@ namespace sat { bool re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz); - bool process(big* big); + bool process(bool learned); + + bool process(big& big, bool learned); bool process(clause & c); @@ -75,6 +77,8 @@ namespace sat { void process(big* big, clause_vector & c); bool process_all(clause & c); + + void process_bin(big& big); bool flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz); @@ -85,7 +89,7 @@ namespace sat { public: asymm_branch(solver & s, params_ref const & p); - void operator()(bool force = false); + void operator()(bool force); void operator()(big& big); diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg index 0fd19d500..b04b5ff01 100644 --- a/src/sat/sat_asymm_branch_params.pyg +++ b/src/sat/sat_asymm_branch_params.pyg @@ -4,6 +4,6 @@ def_module_params(module_name='sat', params=(('asymm_branch', BOOL, True, 'asymmetric branching'), ('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'), ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'), - ('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'), + ('asymm_branch.sampled', BOOL, True, 'use sampling based asymmetric branching based on binary implication graph'), ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'), ('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause'))) diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 5b32911f1..b35930e96 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -21,10 +21,13 @@ Revision History: namespace sat { - big::big() {} + big::big(random_gen& rand, bool binary): + m_rand(rand) { + m_binary = binary; + } - void big::init_big(solver& s, bool learned) { - init_adding_edges(s.num_vars()); + void big::init(solver& s, bool learned) { + init_adding_edges(s.num_vars(), learned); unsigned num_lits = m_num_vars * 2; literal_vector lits; SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size()); @@ -44,7 +47,12 @@ namespace sat { done_adding_edges(); } - void big::init_adding_edges(unsigned num_vars) { + void big::reinit() { + done_adding_edges(); + } + + void big::init_adding_edges(unsigned num_vars, bool learned) { + m_learned = learned; m_num_vars = num_vars; unsigned num_lits = m_num_vars * 2; m_dag.reset(); @@ -129,9 +137,36 @@ namespace sat { m_right[i] = ++dfs_num; } } - for (unsigned i = 0; i < num_lits; ++i) { - VERIFY(m_left[i] < m_right[i]); + DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);}); + } + + unsigned big::reduce_tr(solver& s) { + if (!m_binary && learned()) return 0; + unsigned num_lits = s.num_vars() * 2; + unsigned idx = 0; + unsigned elim = 0; + for (watch_list & wlist : s.m_watches) { + literal u = to_literal(idx++); + watch_list::iterator it = wlist.begin(); + watch_list::iterator itprev = it; + watch_list::iterator end = wlist.end(); + for (; it != end; ++it) { + watched& w = *it; + if (learned() ? w.is_binary_learned_clause() : w.is_binary_clause()) { + literal v = w.get_literal(); + if (reaches(u, v) && u != get_parent(v)) { + ++elim; + // could turn non-learned non-binary tautology into learned binary. + s.get_wlist(~v).erase(watched(~u, w.is_learned())); + continue; + } + } + *itprev = *it; + itprev++; + } + wlist.set_end(itprev); } + return elim; } void big::display(std::ostream& out) const { diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 9896a3215..8477ad186 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -27,32 +27,41 @@ namespace sat { class solver; class big { - random_gen m_rand; + random_gen& m_rand; unsigned m_num_vars; vector m_dag; svector m_roots; svector m_left, m_right; literal_vector m_root, m_parent; + bool m_learned; + bool m_binary; // is the BIG produced from binary clauses or hyper-binary resolution? void init_dfs_num(); struct pframe; public: - big(); + big(random_gen& rand, bool binary); /** \brief initialize a BIG from a solver. */ - void init_big(solver& s, bool learned); + void init(solver& s, bool learned); + + void reinit(); /** \brief initialize a BIG externally by adding implications. */ - void init_adding_edges(unsigned num_vars); + void init_adding_edges(unsigned num_vars, bool learned); void add_edge(literal u, literal v); void done_adding_edges(); - void ensure_big(solver& s, bool learned) { if (m_left.empty()) init_big(s, learned); } + void ensure_big(solver& s, bool learned) { if (m_left.empty()) init(s, learned); } + + unsigned reduce_tr(solver& s); + + // does it include learned binaries? + bool learned() const { return m_learned; } int get_left(literal l) const { return m_left[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; } diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 8b7a4ca46..3600ac1a3 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -29,7 +29,6 @@ namespace sat { m_capacity(sz), m_removed(false), m_learned(learned), - m_blocked(false), m_used(false), m_frozen(false), m_reinit_stack(false), @@ -165,7 +164,6 @@ namespace sat { if (c.was_removed()) out << "x"; if (c.strengthened()) out << "+"; if (c.is_learned()) out << "*"; - if (c.is_blocked()) out << "b"; return out; } diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 76f1a9ad3..7bacf0777 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -50,7 +50,6 @@ 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 @@ -66,6 +65,7 @@ namespace sat { literal & operator[](unsigned idx) { SASSERT(idx < m_size); return m_lits[idx]; } literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; } bool is_learned() const { return m_learned; } + void set_learned() { SASSERT(!is_learned()); m_learned = true; } void unset_learned() { SASSERT(is_learned()); m_learned = false; } void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } } bool strengthened() const { return m_strengthened; } @@ -92,9 +92,6 @@ 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; } @@ -161,6 +158,16 @@ namespace sat { public: clause_wrapper(literal l1, literal l2):m_l1_idx(l1.to_uint()), m_l2_idx(l2.to_uint()) {} clause_wrapper(clause & c):m_cls(&c), m_l2_idx(null_literal.to_uint()) {} + clause_wrapper& operator=(clause_wrapper const& other) { + if (other.is_binary()) { + m_l1_idx = other.m_l1_idx; + } + else { + m_cls = other.m_cls; + } + m_l2_idx = other.m_l2_idx; + return *this; + } bool is_binary() const { return m_l2_idx != null_literal.to_uint(); } unsigned size() const { return is_binary() ? 2 : m_cls->size(); } diff --git a/src/sat/sat_clause_use_list.cpp b/src/sat/sat_clause_use_list.cpp index 363ef784e..7ca0aa2c6 100644 --- a/src/sat/sat_clause_use_list.cpp +++ b/src/sat/sat_clause_use_list.cpp @@ -27,11 +27,11 @@ namespace sat { if (!c->was_removed()) sz++; SASSERT(sz == m_size); - unsigned blocked = 0; + unsigned redundant = 0; for (clause* c : m_clauses) - if (c->is_blocked()) - blocked++; - SASSERT(blocked == m_num_blocked); + if (c->is_learned()) + redundant++; + SASSERT(redundant == m_num_redundant); return true; } diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index 08b50086a..c028ad713 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -30,24 +30,24 @@ namespace sat { class clause_use_list { clause_vector m_clauses; unsigned m_size; - unsigned m_num_blocked; + unsigned m_num_redundant; public: clause_use_list() { STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";); m_size = 0; - m_num_blocked = 0; + m_num_redundant = 0; } unsigned size() const { return m_size; } - unsigned num_blocked() const { - return m_num_blocked; + unsigned num_redundant() const { + return m_num_redundant; } - - unsigned non_blocked_size() const { - return m_size - m_num_blocked; + + unsigned num_irredundant() const { + return m_size - m_num_redundant; } bool empty() const { return size() == 0; } @@ -58,7 +58,7 @@ namespace sat { SASSERT(!c.was_removed()); m_clauses.push_back(&c); m_size++; - if (c.is_blocked()) ++m_num_blocked; + if (c.is_learned()) ++m_num_redundant; } void erase_not_removed(clause & c) { @@ -67,7 +67,7 @@ namespace sat { SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; - if (c.is_blocked()) --m_num_blocked; + if (c.is_learned()) --m_num_redundant; } void erase(clause & c) { @@ -75,25 +75,25 @@ namespace sat { SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; - if (c.is_blocked()) --m_num_blocked; + if (c.is_learned()) --m_num_redundant; } void block(clause const& c) { - SASSERT(c.is_blocked()); - ++m_num_blocked; + SASSERT(c.is_learned()); + ++m_num_redundant; SASSERT(check_invariant()); } void unblock(clause const& c) { - SASSERT(!c.is_blocked()); - --m_num_blocked; + SASSERT(!c.is_learned()); + --m_num_redundant; SASSERT(check_invariant()); } void reset() { m_clauses.finalize(); m_size = 0; - m_num_blocked = 0; + m_num_redundant = 0; } bool check_invariant() const; diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index e52cf139f..286cc1661 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -137,8 +137,7 @@ namespace sat { SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); if (new_sz == 2) { TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";); - if (!c.is_blocked()) - s.mk_bin_clause(c[0], c[1], c.is_learned()); + s.mk_bin_clause(c[0], c[1], c.is_learned()); s.del_clause(c); } else { diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index b67666993..c3352797e 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -111,8 +111,8 @@ namespace sat { m_lookahead_global_autarky = p.lookahead_global_autarky(); // These parameters are not exposed - m_simplify_mult1 = _p.get_uint("simplify_mult1", 300); - m_simplify_mult2 = _p.get_double("simplify_mult2", 1.5); + m_simplify_mult1 = _p.get_uint("simplify_mult1", 100); + m_simplify_mult2 = _p.get_double("simplify_mult2", 1.2); m_simplify_max = _p.get_uint("simplify_max", 500000); // -------------------------------- diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index a2e6b445b..0adcc95ef 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -43,7 +43,7 @@ namespace sat{ 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.non_blocked_size() + neg_occs.non_blocked_size(); + unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.num_irredundant() + neg_occs.num_irredundant(); if (clause_size == 0) { return false; } @@ -307,13 +307,11 @@ namespace sat{ bdd result = m.mk_true(); for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) { clause const& c = it.curr(); - if (!c.is_blocked()) { - bdd cl = m.mk_false(); - for (literal l : c) { - cl |= mk_literal(l); - } - result &= cl; - } + bdd cl = m.mk_false(); + for (literal l : c) { + cl |= mk_literal(l); + } + result &= cl; } return result; } diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 7db5d63ec..ff23c9be7 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -72,7 +72,7 @@ namespace sat { virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0; virtual void collect_statistics(statistics& st) const = 0; virtual extension* copy(solver* s) = 0; - virtual extension* copy(lookahead* s) = 0; + virtual extension* copy(lookahead* s, bool learned) = 0; virtual void find_mutexes(literal_vector& lits, vector & mutexes) = 0; virtual void gc() = 0; virtual void pop_reinit() = 0; diff --git a/src/sat/sat_iff3_finder.cpp b/src/sat/sat_iff3_finder.cpp index af7a6f438..8bbfc0ce0 100644 --- a/src/sat/sat_iff3_finder.cpp +++ b/src/sat/sat_iff3_finder.cpp @@ -73,7 +73,7 @@ namespace sat { It assumes wlist have been sorted using iff3_lt */ static bool contains(watch_list const & wlist, literal l1, literal l2) { - watched k(l1, l2); + watched k(l1, l2, false); if (wlist.size() < SMALL_WLIST) return wlist.contains(k); iff3_lt lt; diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index bdc72602d..f68dc80df 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -28,8 +28,8 @@ namespace sat { } // for ternary clauses - static bool contains_watched(watch_list const & wlist, literal l1, literal l2) { - return wlist.contains(watched(l1, l2)); + static bool contains_watched(watch_list const & wlist, literal l1, literal l2, bool learned) { + return wlist.contains(watched(l1, l2, learned)); } // for nary clauses @@ -64,13 +64,13 @@ namespace sat { return true; if (c.size() == 3) { - CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n"; + CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.learned()), tout << c << "\n"; tout << "watch_list:\n"; sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0])); tout << "\n";); - VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2])); - VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2])); - VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1])); + VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.is_learned())); + VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2], c.is_learned())); + VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1], c.is_learned())); } else { if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 3339bc4e6..94f73dffc 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -989,7 +989,7 @@ namespace sat { m_freevars.insert(v); } - void lookahead::init() { + void lookahead::init(bool learned) { m_delta_trigger = 0.0; m_delta_decrease = 0.0; m_config.m_dl_success = 0.8; @@ -1010,6 +1010,8 @@ namespace sat { for (auto& w : wlist) { if (!w.is_binary_clause()) continue; + if (!learned && w.is_learned()) + continue; literal l2 = w.get_literal(); if (l.index() < l2.index() && !m_s.was_eliminated(l2.var())) add_binary(l, l2); @@ -1017,7 +1019,7 @@ namespace sat { } copy_clauses(m_s.m_clauses, false); - copy_clauses(m_s.m_learned, true); + if (learned) copy_clauses(m_s.m_learned, true); // copy units unsigned trail_sz = m_s.init_trail_size(); @@ -1030,7 +1032,7 @@ namespace sat { } if (m_s.m_ext) { - m_ext = m_s.m_ext->copy(this); + m_ext = m_s.m_ext->copy(this, learned); } propagate(); m_qhead = m_trail.size(); @@ -2223,7 +2225,7 @@ namespace sat { void lookahead::init_search() { m_search_mode = lookahead_mode::searching; scoped_level _sl(*this, c_fixed_truth); - init(); + init(true); } void lookahead::checkpoint() { @@ -2255,13 +2257,13 @@ namespace sat { /** \brief simplify set of clauses by extracting units from a lookahead at base level. */ - void lookahead::simplify() { + void lookahead::simplify(bool learned) { scoped_ext _scoped_ext(*this); SASSERT(m_prefix == 0); SASSERT(m_watches.empty()); m_search_mode = lookahead_mode::searching; scoped_level _sl(*this, c_fixed_truth); - init(); + init(learned); if (inconsistent()) return; inc_istamp(); literal l = choose(); @@ -2311,12 +2313,11 @@ namespace sat { elim(roots, to_elim); if (get_config().m_lookahead_simplify_asymm_branch) { - big_asymm_branch(); + big_asymm_branch(learned); } - if (get_config().m_lookahead_simplify_bca) { + if (learned && get_config().m_lookahead_simplify_bca) { add_hyper_binary(); - } - + } } } m_lookahead.reset(); @@ -2327,11 +2328,11 @@ namespace sat { for strengthening clauses. */ - void lookahead::big_asymm_branch() { + void lookahead::big_asymm_branch(bool learned) { unsigned num_lits = m_s.num_vars() * 2; unsigned idx = 0; - big big; - big.init_adding_edges(m_s.num_vars()); + big big(m_s.m_rand, false); + big.init_adding_edges(m_s.num_vars(), learned); for (auto const& lits : m_binary) { literal u = get_parent(to_literal(idx++)); if (u == null_literal) continue; @@ -2370,8 +2371,8 @@ namespace sat { } } - big big; - big.init_big(m_s, true); + big big(m_s.m_rand, false); + big.init(m_s, true); svector> candidates; unsigned_vector bin_size(num_lits); @@ -2395,7 +2396,7 @@ namespace sat { } for (unsigned count = 0; count < 5; ++count) { - big.init_big(m_s, true); + big.init(m_s, true); unsigned k = 0; union_find_default_ctx ufctx; union_find uf(ufctx); @@ -2418,7 +2419,7 @@ namespace sat { } } } - std::cout << candidates.size() << " -> " << k << "\n"; + // std::cout << candidates.size() << " -> " << k << "\n"; if (k == candidates.size()) break; candidates.shrink(k); if (k == 0) break; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 75ce4fe6d..794d868f1 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -488,7 +488,7 @@ namespace sat { // initialization void init_var(bool_var v); - void init(); + void init(bool learned); void copy_clauses(clause_vector const& clauses, bool learned); nary * copy_clause(clause const& c); @@ -555,7 +555,7 @@ namespace sat { void add_hyper_binary(); - void big_asymm_branch(); + void big_asymm_branch(bool learned); double psat_heur(); @@ -600,7 +600,7 @@ namespace sat { /** \brief simplify set of clauses by extracting units from a lookahead at base level. */ - void simplify(); + void simplify(bool learned); std::ostream& display(std::ostream& out) const; std::ostream& display_summary(std::ostream& out) const; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index c8d47ddd3..3630365d6 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -50,8 +50,8 @@ def_module_params('sat', ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), - ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'), - ('lookahead_simplify.asymm_branch', BOOL, False, 'apply asymmetric branch simplification with lookahead simplifier'), + ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), + ('lookahead_simplify.asymm_branch', BOOL, True, 'apply asymmetric branch simplification with lookahead simplifier'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 4bd16c5c5..484cb93ff 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -26,7 +26,8 @@ Revision History: namespace sat { scc::scc(solver & s, params_ref const & p): - m_solver(s) { + m_solver(s), + m_big(s.m_rand, true) { reset_statistics(); updt_params(p); } @@ -237,41 +238,16 @@ namespace sat { unsigned scc::reduce_tr(bool learned) { unsigned num_lits = m_solver.num_vars() * 2; init_big(learned); - - unsigned idx = 0; - unsigned elim = m_num_elim_bin; - for (watch_list & wlist : m_solver.m_watches) { - literal u = to_literal(idx++); - watch_list::iterator it = wlist.begin(); - watch_list::iterator itprev = it; - watch_list::iterator end = wlist.end(); - for (; it != end; ++it) { - watched& w = *it; - if (learned ? w.is_binary_learned_clause() : w.is_binary_clause()) { - literal v = w.get_literal(); - if (reaches(u, v) && u != get_parent(v)) { - ++m_num_elim_bin; - m_solver.get_wlist(~v).erase(watched(~u, w.is_learned())); - } - else { - *itprev = *it; - itprev++; - } - } - else { - *itprev = *it; - itprev++; - } - } - wlist.set_end(itprev); - } - return m_num_elim_bin - elim; + unsigned num_elim = m_big.reduce_tr(m_solver); + m_num_elim_bin += num_elim; + return num_elim; } void scc::reduce_tr() { unsigned quota = 0, num_reduced = 0; while ((num_reduced = reduce_tr(false)) > quota) { quota = std::max(100u, num_reduced / 2); } - while ((num_reduced = reduce_tr(true)) > quota) { quota = std::max(100u, num_reduced / 2); } + quota = 0; + while ((num_reduced = reduce_tr(true)) > quota) { quota = std::max(100u, num_reduced / 2); } } void scc::collect_statistics(statistics & st) const { diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index 5e61e557e..146bd2366 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -56,16 +56,12 @@ namespace sat { /* \brief create binary implication graph and associated data-structures to check transitivity. */ - void init_big(bool learned) { m_big.init_big(m_solver, learned); } + void init_big(bool learned) { m_big.init(m_solver, learned); } void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); } int get_left(literal l) const { return m_big.get_left(l); } int get_right(literal l) const { return m_big.get_right(l); } - literal get_parent(literal l) const { return m_big.get_parent(l); } literal get_root(literal l) const { return m_big.get_root(l); } - bool reaches(literal u, literal v) const { return m_big.reaches(u, v); } - bool connected(literal u, literal v) const { - return m_big.connected(u, v); - } + bool connected(literal u, literal v) const { return m_big.connected(u, v); } }; }; diff --git a/src/sat/sat_scc_params.pyg b/src/sat/sat_scc_params.pyg index 0bf88a0cd..ead4eeb96 100644 --- a/src/sat/sat_scc_params.pyg +++ b/src/sat/sat_scc_params.pyg @@ -2,5 +2,5 @@ def_module_params(module_name='sat', class_name='sat_scc_params', export=True, params=(('scc', BOOL, True, 'eliminate Boolean variables by computing strongly connected components'), - ('scc.tr', BOOL, False, 'apply transitive reduction, eliminate redundant binary clauses'), )) + ('scc.tr', BOOL, True, 'apply transitive reduction, eliminate redundant binary clauses'), )) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index de59966e6..106cc791e 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -150,7 +150,8 @@ namespace sat { inline void simplifier::block_clause(clause & c) { if (m_retain_blocked_clauses) { - c.block(); + m_need_cleanup = true; + c.set_learned(); m_use_list.block(c); } else { @@ -160,7 +161,7 @@ namespace sat { } inline void simplifier::unblock_clause(clause & c) { - c.unblock(); + c.unset_learned(); m_use_list.unblock(c); } @@ -231,7 +232,6 @@ namespace sat { if (bce_enabled() || abce_enabled() || bca_enabled()) { elim_blocked_clauses(); } - if (!m_need_cleanup) si.check_watches(); if (!learned) { m_num_calls++; @@ -265,6 +265,8 @@ namespace sat { if (m_need_cleanup || vars_eliminated) { TRACE("after_simplifier", tout << "cleanning watches...\n";); cleanup_watches(); + move_clauses(s.m_learned, true); + move_clauses(s.m_clauses, false); cleanup_clauses(s.m_learned, true, vars_eliminated, m_learned_in_use_lists); cleanup_clauses(s.m_clauses, false, vars_eliminated, true); } @@ -302,6 +304,26 @@ namespace sat { } } + void simplifier::move_clauses(clause_vector& cs, bool learned) { + clause_vector::iterator it = cs.begin(); + clause_vector::iterator it2 = it; + clause_vector::iterator end = cs.end(); + for (; it != end; ++it) { + clause & c = *(*it); + if (learned && !c.is_learned()) { + s.m_clauses.push_back(&c); + } + else if (!learned && c.is_learned()) { + s.m_learned.push_back(&c); + } + else { + *it2 = *it; + ++it2; + } + } + cs.set_end(it2); + } + void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) { TRACE("sat", tout << "cleanup_clauses\n";); clause_vector::iterator it = cs.begin(); @@ -309,6 +331,7 @@ namespace sat { clause_vector::iterator end = cs.end(); for (; it != end; ++it) { clause & c = *(*it); + VERIFY(learned == c.is_learned()); if (c.was_removed()) { s.del_clause(c); continue; @@ -350,10 +373,10 @@ namespace sat { s.del_clause(c); continue; } - // clause became a problem clause - if (learned && !c.is_learned()) { + // clause became a learned clause + if (!learned && c.is_learned()) { SASSERT(!c.frozen()); - s.m_clauses.push_back(&c); + s.m_learned.push_back(&c); continue; } *it2 = *it; @@ -433,7 +456,6 @@ 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); for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { clause & c2 = it.curr(); @@ -474,17 +496,15 @@ namespace sat { literal_vector::iterator l_it = m_bs_ls.begin(); for (; it != end; ++it, ++l_it) { clause & c2 = *(*it); - if (!c2.was_removed() && !c1.is_blocked() && *l_it == null_literal) { + if (!c2.was_removed() && *l_it == null_literal) { // 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() && !c1.is_blocked()) { + else if (!c2.was_removed()) { // subsumption resolution TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";); elim_lit(c2, *l_it); @@ -544,7 +564,6 @@ 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(); for (; !it.at_end(); it.next()) { @@ -955,16 +974,19 @@ namespace sat { literal_vector m_covered_clause; literal_vector m_intersection; literal_vector m_new_intersection; + literal_vector m_blocked_binary; svector m_in_intersection; sat::model_converter::elim_stackv m_elim_stack; unsigned m_ala_qhead; + clause_wrapper m_clause; blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l, vector & wlist): s(_s), m_counter(limit), mc(_mc), - m_queue(l, wlist) { + m_queue(l, wlist), + m_clause(null_literal, null_literal) { m_in_intersection.resize(s.s.num_vars() * 2, false); } @@ -977,25 +999,34 @@ namespace sat { return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); } + enum elim_type { + cce_t, + acce_t, + abce_t + }; + + enum verdict_type { + at_t, // asymmetric tautology + bc_t, // blocked clause + no_t // neither + }; + void operator()() { - integrity_checker si(s.s); - //si.check_watches(); if (s.bce_enabled()) { block_clauses(); } - //si.check_watches(); if (s.abce_enabled()) { - cce(); + cce(); } - //si.check_watches(); if (s.cce_enabled()) { - cce(); + cce(); + } + if (s.acce_enabled()) { + cce(); } - //si.check_watches(); if (s.bca_enabled()) { bca(); } - //si.check_watches(); } void block_clauses() { @@ -1022,13 +1053,12 @@ namespace sat { return; } integrity_checker si(s.s); - //si.check_watches(); process_clauses(l); process_binary(l); - //si.check_watches(); - } + } void process_binary(literal l) { + m_blocked_binary.reset(); model_converter::entry* new_entry = 0; watch_list & wlist = s.get_wlist(~l); m_counter -= wlist.size(); @@ -1046,6 +1076,7 @@ namespace sat { if (all_tautology(l)) { block_binary(it, l, new_entry); s.m_num_blocked_clauses++; + m_blocked_binary.push_back(l2); } else { *it2 = *it; it2++; @@ -1053,6 +1084,12 @@ namespace sat { s.unmark_visited(l2); } wlist.set_end(it2); + if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) { + IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";); + for (literal lit2 : m_blocked_binary) { + s.s.mk_bin_clause(l, lit2, true); + } + } } void process_clauses(literal l) { @@ -1062,7 +1099,7 @@ namespace sat { clause_use_list::iterator it = occs.mk_iterator(); for (; !it.at_end(); it.next()) { clause & c = it.curr(); - if (c.is_blocked()) continue; + if (c.is_learned()) continue; m_counter -= c.size(); SASSERT(c.contains(l)); s.mark_all_but(c, l); @@ -1118,7 +1155,7 @@ namespace sat { for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { bool tautology = false; clause & c = it.curr(); - if (c.is_blocked() && !adding) continue; + if (c.is_learned() && !adding) continue; for (literal lit : c) { if (s.is_marked(~lit) && lit != ~l) { tautology = true; @@ -1159,7 +1196,7 @@ namespace sat { clause_use_list & neg_occs = s.m_use_list.get(~l); for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { clause & c = it.curr(); - if (c.is_blocked()) continue; + if (c.is_learned()) continue; bool tautology = false; for (literal lit : c) { if (s.is_marked(~lit) && lit != ~l) { @@ -1172,24 +1209,107 @@ namespace sat { return true; } + bool revisit_binary(literal l1, literal l2) const { + return m_clause.is_binary() && + ((m_clause[0] == l1 && m_clause[1] == l2) || + (m_clause[0] == l2 && m_clause[1] == l1)); + } + + bool revisit_ternary(literal l1, literal l2, literal l3) const { + return m_clause.size() == 3 && + ((m_clause[0] == l1 && m_clause[1] == l2 && m_clause[2] == l3) || + (m_clause[0] == l2 && m_clause[1] == l1 && m_clause[2] == l3) || + (m_clause[0] == l2 && m_clause[1] == l3 && m_clause[2] == l1) || + (m_clause[0] == l1 && m_clause[1] == l3 && m_clause[2] == l2) || + (m_clause[0] == l3 && m_clause[1] == l1 && m_clause[2] == l2) || + (m_clause[0] == l3 && m_clause[1] == l2 && m_clause[2] == l1)); + } + + bool revisit_clause(clause const& c) const { + return !m_clause.is_binary() && (m_clause.get_clause() == &c); + } + /* * C \/ l l \/ lit * ------------------- * C \/ l \/ ~lit + * + * C \/ lit \/ l l \/ lit + * ------------------------ + * l \/ lit C \/ lit \/ l can be removed + * + * C \/ l1 \/ ... \/ lk l1 \/ ... \/ lk \/ lit + * ----------------------------------------------- + * C \/ l1 \/ ... \/ lk \/ ~lit + * unless C contains lit, and it is a tautology. */ - void add_ala() { + bool add_ala() { for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) { literal l = m_covered_clause[m_ala_qhead]; for (watched & w : s.get_wlist(~l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); - if (!s.is_marked(lit) && !s.is_marked(~lit)) { + if (revisit_binary(l, lit)) continue; + if (s.is_marked(lit)) { + IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";); + return true; + } + if (!s.is_marked(~lit)) { + IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";); m_covered_clause.push_back(~lit); s.mark_visited(~lit); } } + else if (w.is_ternary_clause() && !w.is_learned()) { + literal lit1 = w.get_literal1(); + literal lit2 = w.get_literal2(); + if (revisit_ternary(l, lit1, lit2)) continue; + if (s.is_marked(lit1) && s.is_marked(lit2)) { + IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " ternary: " << l << " " << lit1 << " " << lit2 << "\n";); + return true; + } + if (s.is_marked(lit1) && !s.is_marked(~lit2)) { + IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternary " << l << " " << lit1 << " " << lit2 << " " << (~lit2) << "\n";); + m_covered_clause.push_back(~lit2); + s.mark_visited(~lit2); + continue; + } + if (s.is_marked(lit2) && !s.is_marked(~lit1)) { + IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternay " << l << " " << lit1 << " " << lit2 << " " << (~lit1) << "\n";); + m_covered_clause.push_back(~lit1); + s.mark_visited(~lit1); + continue; + } + } + else if (w.is_clause()) { + clause & c = s.s.get_clause(w.get_clause_offset()); + if (c.is_learned()) continue; + if (revisit_clause(c)) continue; + literal lit1 = null_literal; + bool ok = true; + for (literal lit : c) { + if (lit == l) continue; + if (s.is_marked(lit)) continue; + if (!s.is_marked(~lit) && lit1 == null_literal) { + lit1 = lit; + } + else { + ok = false; + break; + } + } + if (!ok) continue; + if (lit1 == null_literal) { + IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " clause " << c << "\n";); + return true; + } + IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " clause " << c << " " << (~lit1) << "\n";); + m_covered_clause.push_back(~lit1); + s.mark_visited(~lit1); + } } } + return false; } @@ -1220,11 +1340,12 @@ namespace sat { } bool above_threshold(unsigned sz0) const { - return sz0 * 10 < m_covered_clause.size(); + if (sz0 * 400 < m_covered_clause.size()) IF_VERBOSE(0, verbose_stream() << "above threshold " << sz0 << " " << m_covered_clause.size() << "\n";); + return sz0 * 400 < m_covered_clause.size(); } - template - bool cla(literal& blocked, model_converter::kind& k) { + template + verdict_type cla(literal& blocked, model_converter::kind& k) { bool is_tautology = false; for (literal l : m_covered_clause) s.mark_visited(l); unsigned num_iterations = 0, sz; @@ -1240,9 +1361,9 @@ namespace sat { * So we record sz0, the original set of literals in the clause, mark additional literals, * and then check if any of the first sz0 literals are blocked. */ - if (s.abce_enabled() && !use_ri) { - add_ala(); - for (unsigned i = 0; i < sz0; ++i) { + if (et == abce_t) { + if (add_ala()) return at_t; + for (unsigned i = 0; !is_tautology && i < sz0; ++i) { if (check_abce_tautology(m_covered_clause[i])) { blocked = m_covered_clause[i]; is_tautology = true; @@ -1252,7 +1373,7 @@ namespace sat { k = model_converter::BLOCK_LIT; // actually ABCE for (literal l : m_covered_clause) s.unmark_visited(l); m_covered_clause.shrink(sz0); - return is_tautology; + return is_tautology ? bc_t : no_t; } /* @@ -1268,53 +1389,56 @@ namespace sat { } while (m_covered_clause.size() > sz && !is_tautology); if (above_threshold(sz0)) break; - if (s.acce_enabled() && !is_tautology) { + if (et == acce_t && !is_tautology) { sz = m_covered_clause.size(); - add_ala(); + if (add_ala()) return at_t; k = model_converter::ACCE; } } while (m_covered_clause.size() > sz && !is_tautology); // if (is_tautology) std::cout << num_iterations << " " << m_covered_clause.size() << " " << sz0 << " " << is_tautology << " " << m_elim_stack.size() << "\n"; for (literal l : m_covered_clause) s.unmark_visited(l); - return is_tautology && !above_threshold(sz0); + return (is_tautology && !above_threshold(sz0)) ? bc_t : no_t; } // perform covered clause elimination. // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. - template - bool cce(clause& c, literal& blocked, model_converter::kind& k) { + template + verdict_type cce(clause& c, literal& blocked, model_converter::kind& k) { + m_clause = clause_wrapper(c); m_covered_clause.reset(); for (literal l : c) m_covered_clause.push_back(l); - return cla(blocked, k); + return cla(blocked, k); } - template - bool cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) { + template + verdict_type cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) { + m_clause = clause_wrapper(l1, l2); m_covered_clause.reset(); m_covered_clause.push_back(l1); m_covered_clause.push_back(l2); - return cla(blocked, k); + return cla(blocked, k); } - template + template void cce() { insert_queue(); - cce_clauses(); - cce_binary(); + cce_clauses(); + cce_binary(); } - template + template void cce_binary() { while (!m_queue.empty() && m_counter >= 0) { s.checkpoint(); - process_cce_binary(m_queue.next()); + process_cce_binary(m_queue.next()); } } - template + template void process_cce_binary(literal l) { + m_blocked_binary.reset(); literal blocked = null_literal; watch_list & wlist = s.get_wlist(~l); m_counter -= wlist.size(); @@ -1329,29 +1453,51 @@ namespace sat { continue; } literal l2 = it->get_literal(); - if (cce(l, l2, blocked, k)) { + switch (cce(l, l2, blocked, k)) { + case bc_t: block_covered_binary(it, l, blocked, k); s.m_num_covered_clauses++; - } - else { + m_blocked_binary.push_back(l2); + break; + case at_t: + s.m_num_ate++; + m_blocked_binary.push_back(l2); + break; + case no_t: *it2 = *it; it2++; + break; } } wlist.set_end(it2); + if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) { + IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";); + for (literal lit2 : m_blocked_binary) { + s.s.mk_bin_clause(l, lit2, true); + } + } } - template + template void cce_clauses() { m_to_remove.reset(); literal blocked; model_converter::kind k; for (clause* cp : s.s.m_clauses) { clause& c = *cp; - if (!c.was_removed() && !c.is_blocked() && cce(c, blocked, k)) { - block_covered_clause(c, blocked, k); - s.m_num_covered_clauses++; + if (!c.was_removed() && !c.is_learned()) { + switch (cce(c, blocked, k)) { + case bc_t: + block_covered_clause(c, blocked, k); + s.m_num_covered_clauses++; + break; + case at_t: + m_to_remove.push_back(&c); + break; + case no_t: + break; + } } } for (clause* c : m_to_remove) { @@ -1456,7 +1602,7 @@ namespace sat { clause_use_list::iterator it = neg_occs.mk_iterator(); for (; !it.at_end(); it.next()) { clause & c = it.curr(); - if (c.is_blocked()) continue; + if (c.is_learned()) continue; m_counter -= c.size(); unsigned sz = c.size(); unsigned i; @@ -1485,11 +1631,13 @@ namespace sat { stopwatch m_watch; unsigned m_num_blocked_clauses; unsigned m_num_covered_clauses; + unsigned m_num_ate; unsigned m_num_added_clauses; blocked_cls_report(simplifier & s): m_simplifier(s), m_num_blocked_clauses(s.m_num_blocked_clauses), m_num_covered_clauses(s.m_num_covered_clauses), + m_num_ate(s.m_num_ate), m_num_added_clauses(s.m_num_bca) { m_watch.start(); } @@ -1503,6 +1651,8 @@ namespace sat { << (m_simplifier.m_num_covered_clauses - m_num_covered_clauses) << " :added-clauses " << (m_simplifier.m_num_bca - m_num_added_clauses) + << " :ate " + << (m_simplifier.m_num_ate - m_num_ate) << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } @@ -1571,7 +1721,7 @@ namespace sat { void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) { clause_use_list const & cs = m_use_list.get(l); for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { - if (!it.curr().is_blocked()) { + if (!it.curr().is_learned()) { r.push_back(clause_wrapper(it.curr())); SASSERT(r.back().size() == it.curr().size()); } @@ -1715,8 +1865,8 @@ namespace sat { 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.non_blocked_size() + num_bin_pos; - unsigned num_neg = neg_occs.non_blocked_size() + num_bin_neg; + unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos; + unsigned num_neg = neg_occs.num_irredundant() + num_bin_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); @@ -1726,12 +1876,12 @@ namespace sat { unsigned before_lits = num_bin_pos*2 + num_bin_neg*2; for (auto it = pos_occs.mk_iterator(); !it.at_end(); it.next()) { - if (!it.curr().is_blocked()) + if (!it.curr().is_learned()) before_lits += it.curr().size(); } for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { - if (!it.curr().is_blocked()) + if (!it.curr().is_learned()) before_lits += it.curr().size(); } @@ -1847,7 +1997,7 @@ namespace sat { ~elim_var_report() { m_watch.stop(); IF_VERBOSE(SAT_VB_LVL, - verbose_stream() << " (sat-resolution :elim-bool-vars " + verbose_stream() << " (sat-resolution :elim-vars " << (m_simplifier.m_num_elim_vars - m_num_elim_vars) << " :threshold " << m_simplifier.m_elim_counter << mem_stat() @@ -1921,6 +2071,7 @@ namespace sat { st.update("elim blocked clauses", m_num_blocked_clauses); st.update("elim covered clauses", m_num_covered_clauses); st.update("blocked clauses added", m_num_bca); + st.update("asymmetric tautologies eliminated", m_num_ate); } void simplifier::reset_statistics() { @@ -1931,5 +2082,6 @@ namespace sat { m_num_elim_lits = 0; m_num_elim_vars = 0; m_num_bca = 0; + m_num_ate = 0; } }; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 589061df5..69a444954 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -107,6 +107,7 @@ namespace sat { unsigned m_num_sub_res; unsigned m_num_elim_lits; unsigned m_num_bca; + unsigned m_num_ate; bool m_learned_in_use_lists; unsigned m_old_num_elim_vars; @@ -159,6 +160,7 @@ namespace sat { void mark_as_not_learned(literal l1, literal l2); void cleanup_watches(); + void move_clauses(clause_vector & cs, bool learned); void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists); bool is_external(bool_var v) const; diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index 32d318536..f988c3c8b 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -8,7 +8,7 @@ def_module_params(module_name='sat', ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'), ('bca', BOOL, False, 'blocked clause addition - add blocked binary clauses'), ('bce_delay', UINT, 0, 'delay eliminate blocked clauses until simplification round'), - ('retain_blocked_clauses', BOOL, False, 'retain blocked clauses for propagation, hide them from variable elimination'), + ('retain_blocked_clauses', BOOL, True, 'retain blocked clauses as lemmas'), ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'), ('override_incremental', BOOL, False, 'override incemental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'), ('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 2dd459372..0c2d34dac 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -173,11 +173,9 @@ namespace sat { for (clause* c : src.m_clauses) { buffer.reset(); for (literal l : *c) buffer.push_back(l); - clause* c1 = mk_clause_core(buffer); - if (c1 && c->is_blocked()) { - c1->block(); - } + mk_clause_core(buffer); } + // copy high quality lemmas unsigned num_learned = 0; for (clause* c : src.m_learned) { @@ -398,9 +396,9 @@ namespace sat { bool solver::attach_ter_clause(clause & c) { bool reinit = false; - m_watches[(~c[0]).index()].push_back(watched(c[1], c[2])); - m_watches[(~c[1]).index()].push_back(watched(c[0], c[2])); - m_watches[(~c[2]).index()].push_back(watched(c[0], c[1])); + m_watches[(~c[0]).index()].push_back(watched(c[1], c[2], c.is_learned())); + m_watches[(~c[1]).index()].push_back(watched(c[0], c[2], c.is_learned())); + m_watches[(~c[2]).index()].push_back(watched(c[0], c[1], c.is_learned())); if (!at_base_lvl()) { if (value(c[1]) == l_false && value(c[2]) == l_false) { m_stats.m_ter_propagate++; @@ -1508,6 +1506,7 @@ namespace sat { CASSERT("sat_simplify_bug", check_invariant()); si.check_watches(); + m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); @@ -1517,11 +1516,6 @@ namespace sat { CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); } - if (m_config.m_lookahead_simplify) { - lookahead lh(*this); - lh.simplify(); - lh.collect_statistics(m_aux_stats); - } sort_watch_lits(); CASSERT("sat_simplify_bug", check_invariant()); @@ -1529,7 +1523,7 @@ namespace sat { CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - m_asymm_branch(); + m_asymm_branch(false); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); @@ -1538,6 +1532,17 @@ namespace sat { m_ext->simplify(); } + if (m_config.m_lookahead_simplify) { + lookahead lh(*this); + lh.simplify(true); + lh.collect_statistics(m_aux_stats); + } + if (false && m_config.m_lookahead_simplify) { + lookahead lh(*this); + lh.simplify(false); + lh.collect_statistics(m_aux_stats); + } + TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n");); reinit_assumptions(); @@ -1639,7 +1644,7 @@ namespace sat { bool ok = true; for (clause const* cp : m_clauses) { clause const & c = *cp; - if (!c.satisfied_by(m) && !c.is_blocked()) { + if (!c.satisfied_by(m)) { IF_VERBOSE(0, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";); TRACE("sat", tout << "failed: " << c << "\n"; tout << "assumptions: " << m_assumptions << "\n"; @@ -3282,6 +3287,19 @@ namespace sat { return num_cls + m_clauses.size() + m_learned.size(); } + void solver::num_binary(unsigned& given, unsigned& learned) const { + given = learned = 0; + unsigned l_idx = 0; + for (auto const& wl : m_watches) { + literal l = ~to_literal(l_idx++); + for (auto const& w : wl) { + if (w.is_binary_clause() && l.index() < w.get_literal().index()) { + if (w.is_learned()) ++learned; else ++given; + } + } + } + } + void solver::display_dimacs(std::ostream & out) const { out << "p cnf " << num_vars() << " " << num_clauses() << "\n"; for (literal lit : m_trail) { @@ -4054,10 +4072,12 @@ namespace sat { } void mk_stat::display(std::ostream & out) const { + unsigned given, learned; + m_solver.num_binary(given, learned); if (!m_solver.m_clauses.empty()) - out << " :clauses " << m_solver.m_clauses.size(); + out << " :clauses " << m_solver.m_clauses.size() + given << "/" << given; if (!m_solver.m_learned.empty()) { - out << " :learned " << (m_solver.m_learned.size() - m_solver.m_num_frozen); + out << " :learned " << (m_solver.m_learned.size() + learned - m_solver.m_num_frozen) << "/" << learned; if (m_solver.m_num_frozen > 0) out << " :frozen " << m_solver.m_num_frozen; } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e37fa3cca..8b97dc7ea 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -263,6 +263,7 @@ namespace sat { bool inconsistent() const { return m_inconsistent; } unsigned num_vars() const { return m_level.size(); } unsigned num_clauses() const; + void num_binary(unsigned& given, unsigned& learned) const; unsigned num_restarts() const { return m_restarts; } bool is_external(bool_var v) const { return m_external[v] != 0; } bool is_external(literal l) const { return is_external(l.var()); } diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index e66197878..88b6f3e51 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -53,15 +53,16 @@ namespace sat { SASSERT(learned || is_binary_non_learned_clause()); } - watched(literal l1, literal l2) { + watched(literal l1, literal l2, bool learned) { SASSERT(l1 != l2); if (l1.index() > l2.index()) std::swap(l1, l2); m_val1 = l1.to_uint(); - m_val2 = static_cast(TERNARY) + (l2.to_uint() << 2); + m_val2 = static_cast(TERNARY) + (static_cast(learned) << 2) + (l2.to_uint() << 3); SASSERT(is_ternary_clause()); SASSERT(get_literal1() == l1); SASSERT(get_literal2() == l2); + SASSERT(is_learned() == learned); } unsigned val2() const { return m_val2; } @@ -91,12 +92,12 @@ namespace sat { bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); } bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); } - void set_not_learned() { SASSERT(is_learned()); m_val2 = static_cast(BINARY); SASSERT(!is_learned()); } - void set_learned() { SASSERT(!is_learned()); m_val2 = static_cast(BINARY) + (1u << 2); SASSERT(is_learned()); } + void set_not_learned() { SASSERT(is_learned()); m_val2 &= 0x3; SASSERT(!is_learned()); } + void set_learned() { SASSERT(!is_learned()); m_val2 |= 0x4; SASSERT(is_learned()); } bool is_ternary_clause() const { return get_kind() == TERNARY; } literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast(m_val1)); } - literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); } + literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); } bool is_clause() const { return get_kind() == CLAUSE; } clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast(m_val1); } @@ -135,7 +136,7 @@ namespace sat { watched* find_binary_watch(watch_list & wlist, literal l); watched const* find_binary_watch(watch_list const & wlist, literal l); bool erase_clause_watch(watch_list & wlist, clause_offset c); - inline void erase_ternary_watch(watch_list & wlist, literal l1, literal l2) { wlist.erase(watched(l1, l2)); } + inline void erase_ternary_watch(watch_list & wlist, literal l1, literal l2) { wlist.erase(watched(l1, l2, true)); wlist.erase(watched(l1, l2, false)); } class clause_allocator; std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist);