adding BDD-based variable elimination routine

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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); }
 

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); }

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()]);
+    }
+
+};
+

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<bool_var> 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

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();

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;

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();