bcd

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

src/api/c++/z3++.h

@@ -2781,7 +2781,8 @@ namespace z3 {
             m_opt = o.m_opt;
         }
         optimize(context& c, optimize& src):object(c) {
-            m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt);
+            m_opt = Z3_mk_optimize(c); 
+            Z3_optimize_inc_ref(c, m_opt);
             add(expr_vector(c, src.assertions()));
             for (expr const& o : expr_vector(c, src.objectives())) minimize(o);            
         }

src/sat/CMakeLists.txt

@@ -19,6 +19,7 @@ z3_add_component(sat
     sat_drat.cpp
     sat_elim_eqs.cpp
     sat_elim_vars.cpp
+    sat_bcd.cpp
     sat_iff3_finder.cpp
     sat_integrity_checker.cpp
     sat_local_search.cpp

src/sat/sat_aig_simplifier.cpp

@@ -151,6 +151,7 @@ namespace sat {
     }
 
     void aig_simplifier::operator()() {
+
         report _report(*this);
         TRACE("aig_simplifier", s.display(tout););
         unsigned n = 0, i = 0;

src/sat/sat_bcd.cpp

@@ -0,0 +1,356 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sat_bcd.cpp
+
+Abstract:
+
+    Find candidate equivalent literals based on blocked clause decomposition.
+    Based on LPAR-19 paper by Biere & Heule.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-09-27.
+
+
+Revision History:
+
+*/
+
+#include "util/trace.h"
+#include "util/bit_vector.h"
+#include "util/map.h"
+#include "sat/sat_bcd.h"
+#include "sat/sat_solver.h"
+
+namespace sat {
+    
+    bcd::bcd(solver & s): s(s) {}
+
+    bcd::~bcd() {
+        cleanup();
+    }
+
+    struct bcd::scoped_cleanup {
+        bcd& f;
+        scoped_cleanup(bcd& f):f(f) {}
+        ~scoped_cleanup() { f.cleanup(); }        
+    };
+
+    struct bcd::report {
+        bcd& f;
+        report(bcd& f):f(f) {}
+        ~report() {
+            IF_VERBOSE(1, verbose_stream() << "Decomposed set " << f.m_L.size() << " rest: " << f.m_R.size() << "\n";);
+            TRACE("sat",
+                  tout << "Decomposed set " << f.m_L.size() << "\n";
+                  for (bclause b : f.m_L) tout << b.lit << ": " << *b.cls << "\n";
+                  tout << "Remainder " << f.m_R.size() << "\n";
+                  for (bclause b : f.m_R) tout << b.lit << ": " << *b.cls << "\n";);            
+        }
+    };
+
+    void bcd::operator()(union_find<>& uf) {
+        scoped_cleanup _sc(*this);
+        report _report(*this);
+        pure_decompose();
+        post_decompose();
+        sat_sweep();
+        extract_partition(uf);
+    }    
+
+    void bcd::operator()(clause_vector& clauses, svector<bin_clause>& bins) {
+        scoped_cleanup _sc(*this);
+        report _report(*this);
+        pure_decompose();
+        post_decompose();
+        for (bclause bc : m_L) {
+            if (bc.cls->size() == 2) 
+                bins.push_back(bin_clause((*bc.cls)[0], (*bc.cls)[1]));
+            else 
+                clauses.push_back(bc.cls);                
+        }
+    }
+
+    void bcd::init(use_list& ul) {
+        for (clause* cls : s.clauses()) {
+            if (!cls->was_removed()) {
+                ul.insert(*cls);
+                register_clause(cls);
+            }
+        }
+        bin_clauses bc;
+        s.collect_bin_clauses(bc, false, false); // exclude roots.
+        for (auto b : bc) {
+            literal lits[2] = { b.first, b.second };
+            clause* cls = s.cls_allocator().mk_clause(2, lits, false);
+            ul.insert(*cls);
+            m_bin_clauses.push_back(cls);
+            register_clause(cls);
+        }
+        TRACE("sat", for (clause* cls : m_clauses) if (cls) tout << *cls << "\n";);
+    }
+
+    void bcd::register_clause(clause* cls) {
+        m_clauses.setx(cls->id(), cls, nullptr);
+    }
+
+    void bcd::unregister_clause(clause const& cls) {
+        m_clauses.setx(cls.id(), 0, nullptr);
+    }
+
+    void bcd::pure_decompose() {
+        use_list ul;
+        ul.init(s.num_vars());
+        init(ul);
+        //
+        // while F != empty
+        //   pick a clause and variable x in clause.
+        //   get use list U1 of x and U2 of ~x
+        //   assume |U1| >= |U2|
+        //   add U1 to clause set.
+        //
+        for (clause* cls : m_clauses) {
+            if (cls) {
+                pure_decompose(ul, (*cls)[s.rand()() % cls->size()]);
+            }
+        }
+    }
+
+    void bcd::pure_decompose(use_list& ul, literal lit) {
+        svector<bclause> tmpL, tmpR;
+        pure_decompose(ul,  lit, tmpL);
+        pure_decompose(ul, ~lit, tmpR);
+        if (tmpL.size() < tmpR.size()) {
+            std::swap(tmpL, tmpR);
+        }
+        m_L.append(tmpL);
+        m_R.append(tmpR);
+        TRACE("bcd", tout << lit << " " << "pos: " << tmpL.size() << " " << "neg: " << tmpR.size() << "\n";);
+    }
+    
+    void bcd::pure_decompose(use_list& ul, literal lit, svector<bclause>& clauses) {
+        clause_use_list& uses = ul.get(lit); 
+        auto it = uses.mk_iterator();
+        for (; !it.at_end(); it.next()) {
+            clause& cls = it.curr();
+            if (m_clauses[cls.id()]) {
+                clauses.push_back(bclause(lit, &cls));
+                unregister_clause(cls);
+            }
+        }
+    }
+
+    void bcd::post_decompose() {
+        m_marked.reset();
+        m_marked.resize(2*s.num_vars(), false);
+        use_list ul;
+        ul.init(s.num_vars());
+        for (bclause bc : m_L) {
+            ul.insert(*bc.cls);
+        }
+
+        // cheap pass: add clauses from R in order
+        // such that they are blocked with respect to
+        // predecessors.
+        reset_removed();
+        unsigned j = 0;
+        for (bclause const & bc : m_R) {
+            literal lit = find_blocked(ul, *bc.cls);
+            if (lit != null_literal) {
+                m_L.push_back(bc);
+                set_removed(*bc.cls);
+                ul.insert(*bc.cls); 
+            }
+            else {
+                m_R[j++] = bc;
+            }
+        }
+        m_R.shrink(j);
+
+#if 0
+        // Super expensive pass: add clauses from R as long
+        // as BCE produces the empty set of clauses.
+        j = 0;
+        for (bclause const& bc : m_R) {
+            if (!bce(ul, *bc.cls)) {
+                m_R[j++] = bc;
+            }
+        }        
+        m_R.shrink(j);
+#endif
+    }
+
+    // Note: replay blocked clause elimination:
+    // Suppose C u { c1 } is blocked. 
+    // annotate each clause by blocking literal.
+    // for new clause c2, check if C u { c2 } is blocked.
+    // For each c in C record which literal it is blocked.
+    // (Order the clauses in C by block ordering)
+    // l | c is blocked, 
+    // => c2 contains ~l => check if c c2 is blocked
+    //  
+    bool bcd::bce(use_list& ul, clause& cls0) {
+        IF_VERBOSE(1, verbose_stream() << "bce " << m_L.size() << " " << m_R.size() << " " << cls0 << "\n";);
+        svector<bclause>&  live_clauses = m_live_clauses;
+        live_clauses.reset();
+        ul.insert(cls0);
+        m_new_L.reset();
+        m_new_L.push_back(bclause(cls0[0], &cls0));
+        bool removed = false;
+        reset_removed();
+        for (bclause bc : m_L) {
+            literal lit = find_blocked(ul, *bc.cls);
+            if (lit == null_literal) {
+                live_clauses.push_back(bc);
+            }
+            else {
+                set_removed(*bc.cls);
+                removed = true;
+                m_new_L.push_back(bclause(lit, bc.cls));
+            }
+        }
+        while (removed) {
+            removed = false;
+            unsigned j = 0;
+            for (bclause bc : live_clauses) {
+                literal lit = find_blocked(ul, *bc.cls);
+                if (lit == null_literal) {
+                    live_clauses[j++] = bc;
+                }
+                else {
+                    set_removed(*bc.cls);
+                    removed = true;
+                    m_new_L.push_back(bclause(lit, bc.cls));
+                }
+            }
+            live_clauses.shrink(j);
+        }
+        if (live_clauses.empty()) {
+            m_L.reset();
+            m_L.append(m_new_L);
+        }
+        else {
+            ul.erase(cls0);
+        }
+        return live_clauses.empty();
+    }
+
+    literal bcd::find_blocked(use_list& ul, clause const& cls) {
+        TRACE("bcd", tout << cls << "\n";);
+
+        for (literal lit : cls) {            
+            m_marked[(~lit).index()] = true;
+        }
+        literal result = null_literal;
+        for (literal lit : cls) {
+            if (is_blocked(ul, lit)) {
+                TRACE("bcd", tout << "is blocked " << lit << " : " << cls << "\n";);
+                result = lit;
+                break;
+            }
+        }
+        for (literal lit : cls) {
+            m_marked[(~lit).index()] = false;
+        }
+        return result;
+    }
+
+    bool bcd::is_blocked(use_list& ul, literal lit) const {
+        auto has_blocked_lit = [&,this](clause const& c) { 
+            for (literal lit2 : c) 
+                if (m_marked[lit2.index()] && ~lit != lit2) {
+                    return true; 
+                }
+            return false; 
+        };
+        auto it = ul.get(~lit).mk_iterator();
+        for (; !it.at_end(); it.next()) {
+            clause & cls = it.curr();
+            if (!is_removed(cls) && !has_blocked_lit(cls))
+                return false;
+        }
+        return true;
+    }
+
+    void bcd::init_rbits() {
+        m_rbits.reset();        
+        for (unsigned i = 0; i < s.num_vars(); ++i) {
+            uint64_t lo = s.rand()() + (s.rand()() << 16ull);
+            uint64_t hi = s.rand()() + (s.rand()() << 16ull);
+            m_rbits.push_back(lo + (hi << 32ull));
+        }
+    }
+    
+    uint64_t bcd::eval_clause(clause const& cls) const {
+        uint64_t b = 0ull;
+        for (literal lit : cls) {
+            b |= lit.sign() ? ~m_rbits[lit.var()] : m_rbits[lit.var()];
+        }
+        return b;
+    }
+
+    void bcd::sat_sweep() {
+        init_rbits();
+        m_L.reverse();
+        for (bclause& bc : m_L) {
+            uint64_t b = eval_clause(*bc.cls);
+            // v = 0, b = 0 => v := 1
+            // v = 0, b = 1 => v := 0
+            // v = 1, b = 0 => v := 0
+            // v = 1, b = 1 => v := 1
+            m_rbits[bc.lit.var()] ^= ~b;
+            if (0 != ~b) IF_VERBOSE(0, verbose_stream() << "fix " << bc.lit << " " << *bc.cls << "\n");
+            VERIFY(0 == ~eval_clause(*bc.cls));
+        }
+        DEBUG_CODE(verify_sweep(););
+    }
+
+    void bcd::verify_sweep() {
+        for (bclause const& bc : m_L) {
+            VERIFY(0 == ~eval_clause(*bc.cls));
+        }
+    }
+    
+    void bcd::extract_partition(union_find<>& uf) {
+        u64_map<unsigned> table;
+        for (unsigned i = 2 * s.num_vars(); i-- > 0; ) {
+            uf.mk_var();
+        }
+        unsigned num_merge = 0;
+        for (unsigned i = 0; i < s.num_vars(); ++i) {
+            uint64_t val = m_rbits[i];
+            literal lit(i, false);
+            unsigned index = UINT_MAX;
+            if (s.was_eliminated(lit) || s.value(lit) != l_undef) {
+                // skip
+            }
+            else if (table.find(val, index)) {
+                IF_VERBOSE(0, verbose_stream() << "merge " << val << " " << lit << " " << to_literal(index) << "\n");
+                uf.merge(lit.index(), index);
+                ++num_merge;
+            }
+            else if (table.find(~val, index)) {
+                IF_VERBOSE(0, verbose_stream() << "merge " << val << " " << (~lit) << " " << to_literal(index) << "\n");
+                uf.merge((~lit).index(), index);
+                ++num_merge;
+            }
+            else {
+                table.insert(val, lit.index());
+            }
+        }
+        IF_VERBOSE(0, verbose_stream() << "num merge: " << num_merge << "\n");
+        TRACE("sat", uf.display(tout););
+    }
+
+    void bcd::cleanup() {
+        s.del_clauses(m_bin_clauses);
+        m_bin_clauses.reset();
+        m_clauses.reset();
+        m_L.reset();
+        m_R.reset();
+    }
+
+};

src/sat/sat_bcd.h

@@ -0,0 +1,77 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sat_bcd.h
+
+Abstract:
+
+    Blocked Clause Decomposition.
+    Exposes a partition of literals based on randomly simulating the BCD.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-09-27.
+
+Revision History:
+
+----*/
+#pragma once
+
+#include"sat/sat_types.h"
+#include"sat/sat_simplifier.h"
+#include"util/union_find.h"
+
+namespace sat {
+
+    class solver;
+
+    class bcd {
+        struct report;
+        struct scoped_cleanup;
+
+        typedef std::pair<literal, literal> bin_clause;
+        typedef svector<bin_clause> bin_clauses;        
+        struct bclause {
+            clause* cls;
+            literal lit;
+            bclause(literal lit, clause* cls):cls(cls), lit(lit) {}
+        };
+        solver &          s;
+        clause_vector     m_clauses;
+        svector<bclause>  m_L, m_R, m_live_clauses, m_new_L;
+        clause_vector     m_bin_clauses;
+        svector<uint64_t> m_rbits;
+        svector<bool>     m_marked;
+        svector<bool>     m_removed; // set of clauses removed (not considered in clause set during BCE)
+
+        void init(use_list& ul);
+        void register_clause(clause* cls);
+        void unregister_clause(clause const& cls);
+        void reset_removed() { m_removed.reset(); }
+        void set_removed(clause const& c) { m_removed.setx(c.id(), true, false); }
+        bool is_removed(clause const& c) const { return m_removed.get(c.id(), false); }
+        void pure_decompose();
+        void pure_decompose(use_list& ul, literal lit);
+        void pure_decompose(use_list& ul, literal lit, svector<bclause>& clauses);
+        void post_decompose();
+        literal find_blocked(use_list& ul, clause const& cls);
+        bool bce(use_list& ul, clause& cls);
+        bool is_blocked(use_list& ul, literal lit) const;
+        void init_rbits();
+        void init_reconstruction_stack();
+        void sat_sweep();
+        void cleanup();
+        uint64_t eval_clause(clause const& cls) const;
+        void verify_sweep();
+        void extract_partition(union_find<>&);
+    public:
+        bcd(solver & s);
+        ~bcd();
+        void operator()(clause_vector& clauses, svector<bin_clause>& bins);
+        void operator()(union_find<>& uf);
+    };
+
+};
+

src/sat/sat_clause_use_list.h

@@ -73,7 +73,7 @@ namespace sat {
         void erase(clause & c) { 
             STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";);
             SASSERT(m_clauses.contains(&c)); 
-            SASSERT(c.was_removed()); 
+            // SASSERT(c.was_removed()); 
             m_size--; 
             if (c.is_learned()) --m_num_redundant;
         }

src/sat/sat_cutset.cpp

@@ -175,8 +175,4 @@ namespace sat {
         return out;
     }
 
-    void cut::sort() {
-        std::sort(m_elems, m_elems + m_size);
-    }
-
 }

src/sat/sat_cutset.h

@@ -67,7 +67,6 @@ namespace sat {
                 return true;
             }
         }
-        void sort();
         void negate() { set_table(~m_table); }
         void set_table(uint64_t t) { m_table = t & table_mask(); }
         uint64_t table() const { return (m_table | m_dont_care) & table_mask(); }

src/sat/sat_solver.h

@@ -196,16 +196,17 @@ namespace sat {
 
         friend class integrity_checker;
         friend class cleaner;
-        friend class simplifier;
-        friend class scc;
+        friend class asymm_branch;
         friend class big;
         friend class binspr;
+        friend class drat;
         friend class elim_eqs;
-        friend class asymm_branch;
-        friend class probing;
+        friend class bcd;
         friend class iff3_finder;
         friend class mus;
-        friend class drat;
+        friend class probing;
+        friend class simplifier;
+        friend class scc;
         friend class ba_solver;
         friend class anf_simplifier;
         friend class aig_simplifier;

src/util/map.h

@@ -277,6 +277,11 @@ struct u_hash { unsigned operator()(unsigned u) const { return u; } };
 
 struct u_eq { bool operator()(unsigned u1, unsigned u2) const { return u1 == u2; } };
 
+
+struct u64_hash { unsigned operator()(uint64_t u) const { return mk_mix((unsigned)u, (unsigned)(u >> 32ull), 0); } };
+
+struct u64_eq { bool operator()(uint64_t u1, uint64_t u2) const { return u1 == u2; } };
+
 struct size_t_eq { bool operator()(size_t u1, size_t u2) const { return u1 == u2; } };
 
 struct int_eq { bool operator()(int u1, int u2) const { return u1 == u2; } };
@@ -287,4 +292,7 @@ class u_map : public map<unsigned, Value, u_hash, u_eq> {};
 template<typename Value>
 class size_t_map : public map<size_t, Value, size_t_hash, size_t_eq> {};
 
+template<typename Value> 
+class u64_map : public map<uint64_t, Value, u64_hash, u64_eq> {};
+
 #endif