From d36406f845cc761edd81f2628a21bdf602a8b509 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 15:12:02 -0700 Subject: [PATCH] adding BDD-based variable elimination routine Signed-off-by: Nikolaj Bjorner --- src/sat/CMakeLists.txt | 1 + src/sat/sat_bdd.cpp | 1 + src/sat/sat_bdd.h | 7 + src/sat/sat_elim_vars.cpp | 289 +++++++++++++++++++++++++++++++++++++ src/sat/sat_elim_vars.h | 61 ++++++++ src/sat/sat_simplifier.cpp | 14 +- src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.h | 1 + 8 files changed, 372 insertions(+), 3 deletions(-) create mode 100644 src/sat/sat_elim_vars.cpp create mode 100644 src/sat/sat_elim_vars.h diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index 7be6ffb45..88f4f3dd6 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -11,6 +11,7 @@ z3_add_component(sat sat_config.cpp sat_drat.cpp sat_elim_eqs.cpp + sat_elim_vars.cpp sat_iff3_finder.cpp sat_integrity_checker.cpp sat_local_search.cpp diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 216eec32f..4835b8580 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -506,6 +506,7 @@ namespace sat { bdd bdd::operator!() { return m->mk_not(*this); } bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); } bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); } + bdd& bdd::operator=(bdd const& other) { int r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 04aa1e8d7..da26c0b36 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -34,6 +34,7 @@ namespace sat { bdd(int root, bdd_manager* m); public: bdd(bdd & other); + bdd& operator=(bdd const& other); ~bdd(); bdd lo() const; bdd hi() const; @@ -44,6 +45,8 @@ namespace sat { bdd operator!(); bdd operator&&(bdd const& other); bdd operator||(bdd const& other); + bdd operator|=(bdd const& other) { return *this = *this || other; } + bdd operator&=(bdd const& other) { return *this = *this && other; } std::ostream& display(std::ostream& out) const; bool operator==(bdd const& other) const { return root == other.root; } bool operator!=(bdd const& other) const { return root != other.root; } @@ -190,9 +193,13 @@ namespace sat { bdd mk_var(unsigned i); bdd mk_nvar(unsigned i); + bdd mk_true() { return bdd(true_bdd, this); } + bdd mk_false() { return bdd(false_bdd, this); } bdd mk_not(bdd b); bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b); bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); } + bdd mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); } bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } bdd mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp new file mode 100644 index 000000000..4fb92c261 --- /dev/null +++ b/src/sat/sat_elim_vars.cpp @@ -0,0 +1,289 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_elim_vars.cpp + +Abstract: + + Helper class for eliminating variables + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-14 + +Revision History: + +--*/ + +#include "sat/sat_simplifier.h" +#include "sat/sat_elim_vars.h" +#include "sat/sat_solver.h" + +namespace sat{ + + elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20,10000) { + m_mark_lim = 0; + m_max_literals = 11; // p.resolution_occ_cutoff(); + } + + bool elim_vars::operator()(bool_var v) { + if (s.value(v) != l_undef) + return false; + + literal pos_l(v, false); + literal neg_l(v, true); + unsigned num_bin_pos = simp.get_num_non_learned_bin(pos_l); + if (num_bin_pos > m_max_literals) return false; + unsigned num_bin_neg = simp.get_num_non_learned_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(); + reset_mark(); + mark_var(v); + if (!mark_literals(pos_occs)) return false; + if (!mark_literals(neg_occs)) return false; + if (!mark_literals(pos_l)) return false; + if (!mark_literals(neg_l)) return false; + + // associate index with each variable. + unsigned index = 0; + for (bool_var w : m_vars) { + m_var2index[w] = index++; + } + bdd b1 = make_clauses(pos_l); + bdd b2 = make_clauses(neg_l); + bdd b3 = make_clauses(pos_occs); + bdd b4 = make_clauses(neg_occs); + bdd b0 = b1 && b2 && b3 && b4; + bdd b = m.mk_exists(m_var2index[v], b0); + TRACE("elim_vars", + tout << "eliminate " << v << "\n"; + tout << "clauses : " << clause_size << "\n"; + for (watched const& w : simp.get_wlist(~pos_l)) { + if (w.is_binary_non_learned_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()) { + tout << neg_l << " " << w.get_literal() << "\n"; + } + } + m.display(tout, b2); + clause_use_list::iterator itp = pos_occs.mk_iterator(); + while (!itp.at_end()) { + clause const& c = itp.curr(); + tout << c << "\n"; + itp.next(); + } + m.display(tout, b3); + clause_use_list::iterator itn = neg_occs.mk_iterator(); + while (!itn.at_end()) { + clause const& c = itn.curr(); + tout << c << "\n"; + itn.next(); + } + m.display(tout, b4); + tout << "eliminated:\n"; + tout << b << "\n"; + tout << m.cnf_size(b) << "\n"; + ); + std::cout << "num clauses: " << clause_size << " cnf size: " << m.cnf_size(b) << "\n"; + if (clause_size < m.cnf_size(b)) + return false; + + + literal_vector lits; + TRACE("elim_vars", + clause_vector clauses; + literal_vector units; + get_clauses(b0, lits, clauses, units); + for (clause* c : clauses) + tout << *c << "\n"; + for (literal l : units) + tout << l << "\n"; + for (clause* c : clauses) + s.m_cls_allocator.del_clause(c); + SASSERT(lits.empty()); + clauses.reset(); + units.reset(); + tout << "after elim:\n"; + get_clauses(b, lits, clauses, units); + for (clause* c : clauses) + tout << *c << "\n"; + for (literal l : units) + tout << l << "\n"; + for (clause* c : clauses) + s.m_cls_allocator.del_clause(c); + SASSERT(lits.empty()); + clauses.reset(); + ); + + return false; + + // 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); + 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); + s.m_eliminated[v] = true; + simp.remove_bin_clauses(pos_l); + simp.remove_bin_clauses(neg_l); + simp.remove_clauses(pos_occs, pos_l); + simp.remove_clauses(neg_occs, neg_l); + pos_occs.reset(); + neg_occs.reset(); + add_clauses(b, lits); + return true; + } + + void elim_vars::add_clauses(bdd const& b, literal_vector& lits) { + if (b.is_true()) { + // no-op + } + else if (b.is_false()) { + SASSERT(lits.size() > 0); + std::cout << lits << "\n"; + literal_vector c(lits); + if (simp.cleanup_clause(c)) + return; + + std::cout << c << "\n"; + + switch (c.size()) { + case 0: + UNREACHABLE(); + break; + case 1: + simp.propagate_unit(c[0]); + break; + case 2: + simp.add_non_learned_binary_clause(c[0],c[1]); + break; + default: { + clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false); + s.m_clauses.push_back(cp); + simp.m_use_list.insert(*cp); + break; + } + } + } + else { + unsigned v = m_vars[b.var()]; + lits.push_back(literal(v, false)); + add_clauses(b.lo(), lits); + lits.pop_back(); + lits.push_back(literal(v, true)); + add_clauses(b.hi(), lits); + lits.pop_back(); + } + } + + + void elim_vars::get_clauses(bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) { + if (b.is_true()) { + return; + } + if (b.is_false()) { + if (lits.size() > 1) { + clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), false); + clauses.push_back(c); + } + else { + units.push_back(lits.back()); + } + return; + } + + // if (v hi lo) + // (v | lo) & (!v | hi) + // if (v T lo) -> (v | lo) + unsigned v = m_vars[b.var()]; + lits.push_back(literal(v, false)); + get_clauses(b.lo(), lits, clauses, units); + lits.pop_back(); + lits.push_back(literal(v, true)); + get_clauses(b.hi(), lits, clauses, units); + lits.pop_back(); + } + + void elim_vars::reset_mark() { + m_vars.reset(); + m_mark.resize(s.num_vars()); + m_var2index.resize(s.num_vars()); + ++m_mark_lim; + if (m_mark_lim == 0) { + ++m_mark_lim; + m_mark.fill(0); + } + } + + void elim_vars::mark_var(bool_var v) { + if (m_mark[v] != m_mark_lim) { + m_mark[v] = m_mark_lim; + m_vars.push_back(v); + } + } + + bool elim_vars::mark_literals(clause_use_list & occs) { + clause_use_list::iterator it = occs.mk_iterator(); + while (!it.at_end()) { + clause const& c = it.curr(); + for (literal l : c) { + mark_var(l.var()); + } + if (num_vars() > m_max_literals) return false; + it.next(); + } + return true; + } + + 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()) { + mark_var(w.get_literal().var()); + } + } + return num_vars() <= m_max_literals; + } + + bdd elim_vars::make_clauses(clause_use_list & occs) { + bdd result = m.mk_true(); + clause_use_list::iterator it = occs.mk_iterator(); + while (!it.at_end()) { + clause const& c = it.curr(); + bdd cl = m.mk_false(); + for (literal l : c) { + cl |= mk_literal(l); + } + it.next(); + result &= cl; + } + return result; + } + + bdd elim_vars::make_clauses(literal lit) { + bdd result = m.mk_true(); + watch_list& wl = simp.get_wlist(~lit); + for (watched const& w : wl) { + if (w.is_binary_non_learned_clause()) { + result &= (mk_literal(lit) || mk_literal(w.get_literal())); + } + } + return result; + } + + bdd elim_vars::mk_literal(literal l) { + return l.sign() ? m.mk_nvar(m_var2index[l.var()]) : m.mk_var(m_var2index[l.var()]); + } + +}; + diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h new file mode 100644 index 000000000..f9d3b374c --- /dev/null +++ b/src/sat/sat_elim_vars.h @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_elim_vars.h + +Abstract: + + Helper class for eliminating variables + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-14 + +Revision History: + +--*/ +#ifndef SAT_ELIM_VARS_H_ +#define SAT_ELIM_VARS_H_ + +#include "sat/sat_types.h" +#include "sat/sat_bdd.h" + +namespace sat { + class solver; + class simplifier; + + class elim_vars { + friend class simplifier; + + simplifier& simp; + solver& s; + bdd_manager m; + + svector m_vars; + unsigned_vector m_mark; + unsigned m_mark_lim; + unsigned_vector m_var2index; + + unsigned m_max_literals; + + unsigned num_vars() const { return m_vars.size(); } + void reset_mark(); + void mark_var(bool_var v); + bool mark_literals(clause_use_list & occs); + bool mark_literals(literal lit); + bdd make_clauses(clause_use_list & occs); + bdd make_clauses(literal lit); + bdd mk_literal(literal l); + void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units); + void add_clauses(bdd const& b, literal_vector& lits); + + public: + elim_vars(simplifier& s); + bool operator()(bool_var v); + }; + +}; + +#endif diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 4d5946795..12923e0d0 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -21,6 +21,7 @@ Revision History: #include "sat/sat_simplifier.h" #include "sat/sat_simplifier_params.hpp" #include "sat/sat_solver.h" +#include "sat/sat_elim_vars.h" #include "util/stopwatch.h" #include "util/trace.h" @@ -1308,7 +1309,6 @@ namespace sat { 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; - m_elim_counter -= num_pos + num_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); @@ -1349,7 +1349,6 @@ namespace sat { collect_clauses(pos_l, m_pos_cls); collect_clauses(neg_l, m_neg_cls); - m_elim_counter -= num_pos * num_neg + before_lits; TRACE("resolution_detail", tout << "collecting number of after_clauses\n";); unsigned before_clauses = num_pos + num_neg; @@ -1371,6 +1370,8 @@ namespace sat { TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); + m_elim_counter -= num_pos * num_neg + before_lits; + // eliminate variable model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); @@ -1454,14 +1455,21 @@ namespace sat { elim_var_report rpt(*this); bool_var_vector vars; order_vars_for_elim(vars); + // sat::elim_vars elim_bdd(*this); + std::cout << "vars to elim: " << vars.size() << "\n"; for (bool_var v : vars) { checkpoint(); - if (m_elim_counter < 0) + if (m_elim_counter < 0) break; if (try_eliminate(v)) { m_num_elim_vars++; } +#if 0 + else if (elim_bdd(v)) { + m_num_elim_vars++; + } +#endif } m_pos_cls.finalize(); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index a38df3d3c..6ef0f8f18 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -49,6 +49,7 @@ namespace sat { class simplifier { friend class ba_solver; + friend class elim_vars; solver & s; unsigned m_num_calls; use_list m_use_list; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 020c1dc42..56071182b 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -179,6 +179,7 @@ namespace sat { friend class local_search; friend struct mk_stat; friend class ccc; + friend class elim_vars; public: solver(params_ref const & p, reslimit& l); ~solver();