From 8811d784154b0eaf64aa72137d097d66123df4ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Oct 2017 21:28:48 -0700 Subject: [PATCH] compress elimination stack representation Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 22 +++--- src/sat/sat_model_converter.h | 12 +-- src/sat/sat_simplifier.cpp | 128 ++++++++++++++++++++++---------- 3 files changed, 108 insertions(+), 54 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c79cd2944..14443a2f7 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -38,16 +38,15 @@ namespace sat { return *this; } - void model_converter::process_stack(model & m, literal_vector const& stack) const { + void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const { SASSERT(!stack.empty()); unsigned sz = stack.size(); - SASSERT(stack[sz - 1] == null_literal); - for (unsigned i = sz - 1; i-- > 0; ) { - literal lit = stack[i]; // this is the literal that is pivoted on. It is repeated + for (unsigned i = sz; i-- > 0; ) { + unsigned csz = stack[i].first; + literal lit = stack[i].second; bool sat = false; - for (; i > 0 && stack[--i] != null_literal;) { - if (sat) continue; - sat = value_at(stack[i], m) == l_true; + for (unsigned j = 0; !sat && j < csz; ++j) { + sat = value_at(c[j], m) == l_true; } if (!sat) { m[lit.var()] = lit.sign() ? l_false : l_true; @@ -66,6 +65,7 @@ namespace sat { bool sat = false; bool var_sign = false; unsigned index = 0; + literal_vector clause; for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause @@ -74,13 +74,15 @@ namespace sat { } elim_stack* s = it->m_elim_stack[index]; if (s) { - process_stack(m, s->stack()); + process_stack(m, clause, s->stack()); } sat = false; ++index; + clause.reset(); continue; } + clause.push_back(l); if (sat) continue; bool sign = l.sign(); @@ -190,13 +192,13 @@ namespace sat { // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } - void model_converter::insert(entry & e, literal_vector const& c, literal_vector const& elims) { + void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) { SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true))); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(alloc(elim_stack, elims)); + e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims)); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 00fd637b7..dcbe450a8 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -39,18 +39,20 @@ namespace sat { class model_converter { public: + typedef svector> elim_stackv; + class elim_stack { unsigned m_refcount; - literal_vector m_stack; + elim_stackv m_stack; public: - elim_stack(literal_vector const& stack): + elim_stack(elim_stackv const& stack): m_refcount(0), m_stack(stack) { } ~elim_stack() { } void inc_ref() { ++m_refcount; } void dec_ref() { if (0 == --m_refcount) dealloc(this); } - literal_vector const& stack() const { return m_stack; } + elim_stackv const& stack() const { return m_stack; } }; enum kind { ELIM_VAR = 0, BLOCK_LIT }; @@ -74,7 +76,7 @@ namespace sat { private: vector m_entries; - void process_stack(model & m, literal_vector const& stack) const; + void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const; public: model_converter(); @@ -86,7 +88,7 @@ namespace sat { void insert(entry & e, clause const & c); void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); - void insert(entry & c, literal_vector const& covered_clause, literal_vector const& elim_stack); + void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack); bool empty() const { return m_entries.empty(); } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b09d180c0..b967ade06 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -965,6 +965,7 @@ namespace sat { literal l = m_queue.next(); process(l); } + cce(); } // @@ -1027,55 +1028,106 @@ namespace sat { literal_vector m_covered_clause; literal_vector m_intersection; - literal_vector m_elim_stack; + sat::model_converter::elim_stackv m_elim_stack; + unsigned m_ala_qhead; - bool cla(literal lit) { + /* + * C \/ l l \/ lit + * ------------------- + * C \/ l \/ ~lit + */ + void 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_clause()) { + literal lit = w.get_literal(); + if (!s.is_marked(lit) && !s.is_marked(~lit)) { + //std::cout << "ALA " << ~lit << "\n"; + m_covered_clause.push_back(~lit); + s.mark_visited(~lit); + } + } + } + } + } + + bool add_cla(literal& blocked) { + for (unsigned i = 0; i < m_covered_clause.size(); ++i) { + m_intersection.reset(); + if (ri(m_covered_clause[i], m_intersection)) { + blocked = m_covered_clause[i]; + return true; + } + 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; + } + + bool cla(literal& blocked) { bool is_tautology = false; for (literal l : m_covered_clause) s.mark_visited(l); unsigned num_iterations = 0, sz; m_elim_stack.reset(); + m_ala_qhead = 0; do { - ++num_iterations; - sz = m_covered_clause.size(); - for (unsigned i = 0; i < m_covered_clause.size(); ++i) { - m_intersection.reset(); - if (ri(m_covered_clause[i], m_intersection) && m_covered_clause[i] == lit) { - is_tautology = true; - break; - } - 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.append(m_covered_clause); // the current clause - m_elim_stack.push_back(m_covered_clause[i]); // the pivot literal - m_elim_stack.push_back(null_literal); // null demarcation - } + do { + ++num_iterations; + sz = m_covered_clause.size(); + is_tautology = add_cla(blocked); } + while (m_covered_clause.size() > sz && !is_tautology); + break; + //if (is_tautology) break; + //sz = m_covered_clause.size(); + // unsound? add_ala(); } - while (m_covered_clause.size() > sz && !is_tautology); + while (m_covered_clause.size() > sz); for (literal l : m_covered_clause) s.unmark_visited(l); - if (is_tautology) std::cout << "taut: " << num_iterations << "\n"; + // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n"; return is_tautology; } // perform covered clause elimination. // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. - bool cce(clause& c, literal lit) { + bool cce(clause& c, literal& blocked) { m_covered_clause.reset(); for (literal l : c) m_covered_clause.push_back(l); - return cla(lit); + return cla(blocked); } - bool cce(literal lit, literal l2) { + bool cce(literal lit, literal l2, literal& blocked) { m_covered_clause.reset(); m_covered_clause.push_back(lit); m_covered_clause.push_back(l2); - return cla(lit); + return cla(blocked); + } + + void cce() { + m_to_remove.reset(); + 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); + s.m_num_covered_clauses++; + } + } + for (clause* c : m_to_remove) { + s.remove_clause(*c); + } + m_to_remove.reset(); } void process(literal l) { @@ -1085,6 +1137,7 @@ namespace sat { return; } + literal blocked = null_literal; m_to_remove.reset(); { clause_use_list & occs = s.m_use_list.get(l); @@ -1095,14 +1148,10 @@ namespace sat { SASSERT(c.contains(l)); s.mark_all_but(c, l); if (all_tautology(l)) { - s.unmark_all(c); block_clause(c, l, new_entry); s.m_num_blocked_clauses++; } - else if (cce(c, l)) { - block_covered_clause(c, l, new_entry); - s.m_num_covered_clauses++; - } + s.unmark_all(c); it.next(); } } @@ -1127,8 +1176,9 @@ namespace sat { block_binary(it, l, new_entry); s.m_num_blocked_clauses++; } - else if (cce(l, l2)) { - block_covered_binary(it, l, new_entry); + 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 { @@ -1163,9 +1213,9 @@ namespace sat { mc.insert(*new_entry, m_covered_clause, m_elim_stack); } - void prepare_block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { + void prepare_block_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { if (new_entry == 0) - new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); + new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.var())); literal l2 = it->get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";); s.remove_bin_clause_half(l2, l, it->is_learned()); @@ -1173,12 +1223,12 @@ namespace sat { } void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { - prepare_block_binary(it, l, new_entry); + prepare_block_binary(it, l, l, new_entry); mc.insert(*new_entry, l, it->get_literal()); } - void block_covered_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { - prepare_block_binary(it, l, new_entry); + void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { + prepare_block_binary(it, l, blocked, new_entry); mc.insert(*new_entry, m_covered_clause, m_elim_stack); }