From 75bf942237a2e250855f37ba6493a46286f70924 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Jan 2018 21:15:07 -0800 Subject: [PATCH] throttle cce pass Signed-off-by: Nikolaj Bjorner --- src/sat/sat_integrity_checker.cpp | 2 +- src/sat/sat_simplifier.cpp | 211 ++++++++++++++++-------------- src/sat/sat_simplifier.h | 7 +- src/sat/sat_simplifier_params.pyg | 1 + 4 files changed, 117 insertions(+), 104 deletions(-) diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index 7a2cd9034..e0e285d56 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -64,7 +64,7 @@ namespace sat { return true; if (c.size() == 3) { - CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.is_learned()), tout << c << "\n"; + CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n"; tout << "watch_list:\n"; sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0])); tout << "\n";); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 7bf850469..831539351 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -94,23 +94,18 @@ namespace sat { bool simplifier::single_threaded() const { return s.m_config.m_num_threads == 1; } - bool simplifier::bce_enabled() const { + bool simplifier::bce_enabled_base() const { return - !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && - (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled()); - } - bool simplifier::acce_enabled() const { - return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; - } - bool simplifier::cce_enabled() const { - return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); - } - bool simplifier::abce_enabled() const { - return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; - } - bool simplifier::bca_enabled() const { - return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); + !m_incremental_mode && !s.tracking_assumptions() && + !m_learned_in_use_lists && m_num_calls >= m_bce_delay && single_threaded(); } + + bool simplifier::ate_enabled() const { return m_ate; } + bool simplifier::bce_enabled() const { return bce_enabled_base() && (m_bce || m_bce_at == m_num_calls || m_acce || m_abce || m_cce); } + bool simplifier::acce_enabled() const { return bce_enabled_base() && m_acce; } + bool simplifier::cce_enabled() const { return bce_enabled_base() && (m_cce || m_acce); } + bool simplifier::abce_enabled() const { return bce_enabled_base() && m_abce; } + bool simplifier::bca_enabled() const { return bce_enabled_base() && m_bca; } bool simplifier::elim_vars_bdd_enabled() const { return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); } @@ -219,7 +214,7 @@ namespace sat { } register_clauses(s.m_clauses); - if (bce_enabled() || abce_enabled() || bca_enabled()) { + if (bce_enabled() || bca_enabled() || ate_enabled()) { elim_blocked_clauses(); } @@ -1010,28 +1005,27 @@ namespace sat { enum elim_type { cce_t, acce_t, - abce_t - }; - - enum verdict_type { - at_t, // asymmetric tautology - bc_t, // blocked clause - no_t // neither + abce_t, + ate_t, + no_t }; void operator()() { - if (s.bce_enabled()) { - block_clauses(); - } - if (s.abce_enabled()) { - cce(); - } - if (s.cce_enabled()) { - cce(); - } if (s.acce_enabled()) { cce(); } + if (s.ate_enabled() && !s.abce_enabled() && !s.acce_enabled()) { + cce(); + } + if (s.cce_enabled() && !s.acce_enabled()) { + cce(); + } + if (s.abce_enabled() && !s.acce_enabled()) { + cce(); + } + if (s.bce_enabled() && !s.cce_enabled() && !s.abce_enabled()) { + block_clauses(); + } if (s.bca_enabled()) { bca(); } @@ -1223,7 +1217,8 @@ namespace sat { This routine removes literals that were not relevant to establishing it was blocked. */ void minimize_covered_clause(unsigned idx) { - // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";); + // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause + // << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";); for (literal l : m_tautology) VERIFY(s.is_marked(l)); for (literal l : m_covered_clause) s.unmark_visited(l); for (literal l : m_tautology) s.mark_visited(l); @@ -1369,14 +1364,25 @@ namespace sat { } template - verdict_type cla(literal& blocked, model_converter::kind& k) { - bool is_tautology = false; + elim_type cce(literal& blocked, model_converter::kind& k) { + bool is_tautology = false, first = true; + unsigned sz = 0, sz0 = m_covered_clause.size(); for (literal l : m_covered_clause) s.mark_visited(l); - unsigned num_iterations = 0, sz; + shuffle(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand); m_elim_stack.reset(); m_ala_qhead = 0; - k = model_converter::CCE; - unsigned sz0 = m_covered_clause.size(); + + switch (et) { + case abce_t: + k = model_converter::BLOCK_LIT; + break; + case cce_t: + k = model_converter::CCE; + break; + case acce_t: + k = model_converter::ACCE; + break; + } /* * For blocked clause elimination with asymmetric literal addition (ABCE) @@ -1385,56 +1391,48 @@ 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 (et == abce_t) { - if (add_ala()) { - for (literal l : m_covered_clause) s.unmark_visited(l); - return at_t; - } - for (unsigned i = 0; i < sz0; ++i) { - if (check_abce_tautology(m_covered_clause[i])) { - blocked = m_covered_clause[i]; - is_tautology = true; - break; - } - } - 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 ? bc_t : no_t; - } - /* - * For CCE we add the resolution intersection while checking if the clause becomes a tautology. - * For ACCE, in addition, we add literals. - */ - do { - do { - if (above_threshold(sz0)) break; - ++num_iterations; - sz = m_covered_clause.size(); + while (!is_tautology && m_covered_clause.size() > sz && !above_threshold(sz0)) { + SASSERT(!is_tautology); + if ((et == abce_t || et == acce_t || et == ate_t) && add_ala()) { + for (literal l : m_covered_clause) s.unmark_visited(l); + return ate_t; + } + + if (first) { + for (unsigned i = 0; i < sz0; ++i) { + if (check_abce_tautology(m_covered_clause[i])) { + blocked = m_covered_clause[i]; + is_tautology = true; + break; + } + } + first = false; + } + + if (is_tautology || et == abce_t) { + for (literal l : m_covered_clause) s.unmark_visited(l); + m_covered_clause.shrink(sz0); + return is_tautology ? abce_t : no_t; + } + + /* + * Add resolution intersection while checking if the clause becomes a tautology. + */ + sz = m_covered_clause.size(); + if (et == cce_t || et == acce_t) { is_tautology = add_cla(blocked); } - while (m_covered_clause.size() > sz && !is_tautology); - if (et == acce_t && !is_tautology) { - sz = m_covered_clause.size(); - if (add_ala()) { - for (literal l : m_covered_clause) s.unmark_visited(l); - return at_t; - } - k = model_converter::ACCE; - } - if (above_threshold(sz0)) break; } - while (m_covered_clause.size() > sz && !is_tautology); for (literal l : m_covered_clause) s.unmark_visited(l); - return is_tautology ? bc_t : no_t; + return is_tautology ? et : no_t; } // perform covered clause elimination. // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. template - verdict_type cce(clause& c, literal& blocked, model_converter::kind& k) { + elim_type cce(clause& c, literal& blocked, model_converter::kind& k) { m_clause = clause_wrapper(c); m_covered_clause.reset(); m_covered_antecedent.reset(); @@ -1443,11 +1441,11 @@ namespace sat { m_covered_antecedent.push_back(clause_ante()); } // shuffle(s.s.m_rand, m_covered_clause); - return cla(blocked, k); + return cce(blocked, k); } template - verdict_type cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) { + elim_type cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) { m_clause = clause_wrapper(l1, l2); m_covered_clause.reset(); m_covered_antecedent.reset(); @@ -1455,7 +1453,7 @@ namespace sat { m_covered_clause.push_back(l2); m_covered_antecedent.push_back(clause_ante()); m_covered_antecedent.push_back(clause_ante()); - return cla(blocked, k); + return cce(blocked, k); } template @@ -1481,21 +1479,22 @@ namespace sat { model_converter::kind k; for (watched & w : wlist) { if (!w.is_binary_non_learned_clause()) continue; + if (!select_clause(2)) continue; literal l2 = w.get_literal(); - switch (cce(l, l2, blocked, k)) { - case bc_t: - inc_bc(); - block_covered_binary(w, l, blocked, k); - w.set_learned(true); - s.s.set_learned1(l2, l, true); - break; - case at_t: - s.m_num_ate++; + elim_type r = cce(l, l2, blocked, k); + inc_bc(r); + switch (r) { + case ate_t: w.set_learned(true); s.s.set_learned1(l2, l, true); break; case no_t: break; + default: + block_covered_binary(w, l, blocked, k); + w.set_learned(true); + s.s.set_learned1(l2, l, true); + break; } } } @@ -1507,31 +1506,40 @@ namespace sat { for (clause* cp : s.s.m_clauses) { clause& c = *cp; if (c.was_removed() || c.is_learned()) continue; - switch (cce(c, blocked, k)) { - case bc_t: - inc_bc(); - block_covered_clause(c, blocked, k); - s.set_learned(c); - break; - case at_t: - s.m_num_ate++; + if (!select_clause(c.size())) continue; + elim_type r = cce(c, blocked, k); + inc_bc(r); + switch (r) { + case ate_t: s.set_learned(c); break; case no_t: break; + default: + block_covered_clause(c, blocked, k); + s.set_learned(c); + break; } } } - template - void inc_bc() { + void inc_bc(elim_type et) { switch (et) { case cce_t: s.m_num_cce++; break; case acce_t: s.m_num_acce++; break; case abce_t: s.m_num_abce++; break; + case ate_t: s.m_num_ate++; break; + default: break; } } + // select 25% of clauses size 2, 3 + // always try to remove larger clauses. + template + bool select_clause(unsigned sz) { + return et == ate_t || (sz > 3) || s.s.m_rand(4) == 0; + } + void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) { TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); VERIFY(!s.is_external(l)); @@ -2070,9 +2078,10 @@ namespace sat { m_acce = p.acce(); m_bca = p.bca(); m_abce = p.abce(); + m_ate = p.ate(); m_bce_delay = p.bce_delay(); - m_elim_blocked_clauses = p.elim_blocked_clauses(); - m_elim_blocked_clauses_at = p.elim_blocked_clauses_at(); + m_bce = p.elim_blocked_clauses(); + m_bce_at = p.elim_blocked_clauses_at(); m_retain_blocked_clauses = p.retain_blocked_clauses(); m_blocked_clause_limit = p.blocked_clause_limit(); m_res_limit = p.resolution_limit(); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index e0a0e6b67..086111f84 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -76,8 +76,9 @@ namespace sat { bool m_acce; // cce with asymetric literal addition bool m_bca; // blocked (binary) clause addition. unsigned m_bce_delay; - bool m_elim_blocked_clauses; - unsigned m_elim_blocked_clauses_at; + bool m_bce; // blocked clause elimination + bool m_ate; // asymmetric tautology elimination + unsigned m_bce_at; bool m_retain_blocked_clauses; unsigned m_blocked_clause_limit; bool m_incremental_mode; @@ -176,6 +177,8 @@ namespace sat { void elim_blocked_clauses(); bool single_threaded() const; // { return s.m_config.m_num_threads == 1; } + bool bce_enabled_base() const; + bool ate_enabled() const; bool bce_enabled() const; bool acce_enabled() const; bool cce_enabled() const; diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index f988c3c8b..4bbc490cc 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -4,6 +4,7 @@ def_module_params(module_name='sat', params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'), ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'), ('cce', BOOL, False, 'eliminate covered clauses'), + ('ate', BOOL, True, 'asymmetric tautology elimination'), ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'), ('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'),