binspr

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

src/sat/CMakeLists.txt

@@ -5,6 +5,7 @@ z3_add_component(sat
     sat_asymm_branch.cpp
     sat_bdd.cpp
     sat_big.cpp
+    sat_binspr.cpp
     sat_clause.cpp
     sat_clause_set.cpp
     sat_clause_use_list.cpp

src/sat/sat_binspr.cpp

@@ -0,0 +1,463 @@
+/*++
+  Copyright (c) 2019 Microsoft Corporation
+
+  Module Name:
+
+   sat_binspr.cpp
+
+  Abstract:
+   
+    Inprocessing step for creating SPR binary clauses.
+
+  Author:
+
+    Nikolaj Bjorner, Marijn Heule 2019-4-29
+
+  Notes:
+
+
+  L = { lit1, lit2 }
+  G := { touched_L(C) |  C in F and C intersects with L, and not F|L |-_unit untouch_L(C) }
+  G & ~L is satisfiable
+  ------------
+  Learn ~lit1 or ~lit2
+
+
+Marijn's version:
+
+  L = { lit1, lit2 }
+  alpha = L + units in F|L
+  G := { touched_alpha(C) |  C in F and C intersects with L, and not F|L |-_unit untouch_alpha(C) }
+  G & ~L is satisfiable
+  ---------------------
+  Learn ~L
+
+    
+
+
+  Alternative:   
+
+  for p in literals:
+      push(1)
+      propagate(p)
+      candidates = literals \ units
+      for (C or p) in use(p) and candidates != empty:
+          push(1)
+          propagate(~C)
+          if inconsistent():
+             learn C (subsumes C or p)
+          else:
+             candidates' := C union ~(consequencs of propagate(~C))
+             candidates  := candidates' intersect candidates
+          pop(1)
+      for q in candidates:
+          add (~q or ~p)
+      pop(1) 
+
+  The idea is that all clauses using p must satisfy 
+      q in C or F|pq |-1 untouched(C)
+  The clauses that contain q are not restricted: We directly create G := (~p or ~q) & q, which is satisfiable
+  Let pqM |= F, we claim then that ~pqM |= F 
+  
+  - every clause (C or q) that contains q is satisfied by ~pqM
+  - every clause (C or p) that does not contain q positively, but contains p satisfies F|pq |-1 untouched(C)
+    Therefore pqM |= untouched(C) and therefore already M |= untouched(C)
+  - all other clauses are satisfied by pqM, but contain neither p, nor q, 
+    so it is already the case that M satisfies the clause.
+
+  Alternative:
+
+  for p in literals:
+      push(1)
+      propagate(p)
+      candidates = {}
+      for (C or p) in use(p):
+          push(1)
+          propagate(~C)
+          if inconsistent():
+             learn C (subsumes C or p)
+          else:
+             candidates := candicates union C union ~(consequencs of propagate(~C))
+          pop(1)
+      for q in candidates:
+          push(1)
+          propagate(q)
+          incons := true
+          for (C or p) in use(p) and incons:
+              push(1)
+              propagate(~C)
+              incons := inconsistent()
+              pop(1)
+          pop(1)
+          if incons:
+             add (~p or ~q)
+      pop(1) 
+
+  The idea is similar to the previous alternative, but it allows a candidate to
+  not be directly unit derivable in all clauses C or p, but could be a failed literal
+  under the assumption ~C. 
+  The motivation for this variant is that it is unlikely that we need failed literals to
+  close both (C_1 or p),..., (C_n or p) for all clauses containing p.
+
+  Alternative:
+
+
+  1. extract BIG
+     Use BIG to limit cone enumeration
+  2. for each literal lit:
+        enumerate k1 in cone of lit
+           enumerate lit2 in use(~k1)
+              check if cone of lit2 contains k2 such that lit1 in use(~k2)
+
+  --*/
+
+#include "sat/sat_binspr.h"
+#include "sat/sat_solver.h"
+#include "sat/sat_big.h"
+
+namespace sat {
+
+    struct binspr::report {
+        binspr& m_binspr;
+        stopwatch m_watch;
+        report(binspr& b): 
+            m_binspr(b) {
+            m_watch.start();
+        }
+        ~report() {
+            m_watch.stop();
+            unsigned nb = m_binspr.m_bin_clauses;
+            IF_VERBOSE(2, verbose_stream() << " (sat-binspr :binary " << nb << m_watch << ")\n");
+        }            
+    };
+
+    void binspr::operator()() {
+        unsigned num = s.num_vars();
+        m_bin_clauses = 0;
+
+        report _rep(*this);
+        m_use_list.reset();
+        m_use_list.reserve(num*2);
+        for (clause* c : s.m_clauses) {
+            if (!c->frozen() && !c->was_removed()) { 
+                for (literal lit : *c) {
+                    m_use_list[lit.index()].push_back(c);
+                }
+            }
+        }
+        TRACE("sat", s.display(tout););
+        algorithm2();
+    }
+
+
+    /**
+       F, p |- ~u, 
+       F, p, q |- ~v, 
+       { p, v } u C in F
+       { q, u } u D in F
+  
+       Then use { p, ~u, q, ~v } as alpha, L = { p, q }
+
+      for u in ~consequences of p:
+          for (u u D) in use(u):
+              for q in D, unassigned:              
+                  for v in ~consequences(q) | ({p, v} u C) in use(v):
+                   check_spr(p, q, u, v)                
+    */
+
+    void binspr::algorithm2() {
+        mk_masks();
+        unsigned num_lits = 2 * s.num_vars();
+        for (unsigned l_idx = 0; l_idx < num_lits && !s.inconsistent(); ++l_idx) {
+            s.checkpoint();
+            literal p = to_literal(l_idx);
+            TRACE("sat", tout << "p " << p << " " << s.value(p) << "\n";);
+            if (is_used(p) && s.value(p) == l_undef) {
+                s.push();
+                s.assign_scoped(p);
+                unsigned sz_p = s.m_trail.size();
+                s.propagate(false);
+                if (s.inconsistent()) {
+                    s.pop(1);
+                    s.assign_unit(~p);
+                    s.propagate(false);
+                    TRACE("sat", s.display(tout << "unit\n"););
+                    IF_VERBOSE(0, verbose_stream() << "unit " << (~p) << "\n");
+                    continue;
+                }
+                for (unsigned i = sz_p; !s.inconsistent() && i < s.m_trail.size(); ++i) {
+                    literal u = ~s.m_trail[i];
+                    TRACE("sat", tout << "p " << p << " u " << u << "\n";);
+                    for (clause* cp : m_use_list[u.index()]) {
+                        for (literal q : *cp) {
+                            if (s.inconsistent()) 
+                                break;
+                            if (s.value(q) != l_undef) 
+                                continue;
+
+                            s.push();
+                            s.assign_scoped(q);
+                            unsigned sz_q = s.m_trail.size();
+                            s.propagate(false);
+                            if (s.inconsistent()) {
+                                // learn ~p or ~q
+                                s.pop(1);
+                                block_binary(p, q, true);
+                                s.propagate(false);
+                                continue;
+                            }
+                            bool found = false;
+                            for (unsigned j = sz_q; !found && j < s.m_trail.size(); ++j) {
+                                literal v = ~s.m_trail[j];
+                                for (clause* cp2 : m_use_list[v.index()]) {                                    
+                                    if (cp2->contains(p)) {
+                                        if (check_spr(p, q, u, v)) {
+                                            found = true;
+                                            break;
+                                        }
+                                    }
+                                }
+                            }
+                            s.pop(1);
+                            if (found) {
+                                block_binary(p, q, false);
+                                s.propagate(false);
+                                TRACE("sat", s.display(tout););
+                            }
+                        }
+                    }
+                }
+                s.pop(1);
+            }
+        }               
+    }
+
+    bool binspr::is_used(literal lit) const {
+        return !m_use_list[lit.index()].empty() || !s.get_wlist(~lit).empty();
+    }
+    
+    bool binspr::check_spr(literal p, literal q, literal u, literal v) {
+        SASSERT(s.value(p) == l_true);
+        SASSERT(s.value(q) == l_true);
+        SASSERT(s.value(u) == l_false);
+        SASSERT(s.value(v) == l_false);
+        init_g(p, q, u, v);
+        literal lits[4] = { p, q, ~u, ~v };
+        for (unsigned i = 0; g_is_sat() && i < 4; ++i) {
+            binary_are_unit_implied(lits[i]);
+            clauses_are_unit_implied(lits[i]);
+        }
+        TRACE("sat", tout << p << " " << q << " " << u << " " << v << " " << g_is_sat() << "\n";);
+        return g_is_sat();
+    }
+
+    void binspr::binary_are_unit_implied(literal p) {
+        for (watched const& w : s.get_wlist(~p)) {
+            if (!g_is_sat()) {
+                break;
+            }
+            if (!w.is_binary_non_learned_clause()) {
+                continue;
+            }            
+
+            clear_alpha();
+            VERIFY(touch(p));
+            literal lit = w.get_literal();
+            SASSERT(lit != p);
+            
+            if (touch(lit)) {
+                add_touched();
+                continue;
+            }
+
+            bool inconsistent = (s.value(lit) == l_true);
+            if (s.value(lit) == l_undef) {
+                s.push();
+                s.assign_scoped(~lit);
+                s.propagate(false);
+                inconsistent = s.inconsistent();
+                s.pop(1);
+            }
+
+            if (!inconsistent) {            
+                TRACE("sat", tout << "not implied: " << p << " " << lit << "\n";);
+                m_state = 0;
+                add_touched();
+            }
+        }
+    }
+
+    void binspr::clauses_are_unit_implied(literal p) {
+        for (clause* cp : m_use_list[p.index()]) {
+            if (!g_is_sat()) break;
+            clause_is_unit_implied(*cp);
+        }
+    }
+
+    void binspr::clause_is_unit_implied(clause const& c) {
+        s.push();
+        clear_alpha();
+        for (literal lit : c) {
+            if (touch(lit)) {
+                continue;
+            }
+            else if (s.value(lit) == l_true) {
+                s.pop(1);
+                return;
+            }
+            else if (s.value(lit) != l_false) {
+                s.assign_scoped(~lit);
+            }
+        }
+        s.propagate(false);
+        bool inconsistent = s.inconsistent();
+        s.pop(1);
+        if (!inconsistent) {
+            add_touched();
+        }
+    }
+
+
+    void binspr::block_binary(literal lit1, literal lit2, bool learned) {
+        IF_VERBOSE(2, verbose_stream() << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n");
+        TRACE("sat", tout << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n";);
+        s.mk_clause(~lit1, ~lit2, learned);
+        ++m_bin_clauses;
+    }
+
+    void binspr::g_add_unit(literal lit1, literal lit2) {
+        if (lit1.var() < lit2.var()) {
+            m_state &= 0x2;
+        }
+        else {
+            m_state &= 0x4;
+        }
+    }
+
+    void binspr::g_add_binary(literal lit1, literal lit2, bool flip2) {
+        bool flip1 = false;
+        if (lit1.var() > lit2.var()) { std::swap(flip1, flip2); }
+        m_state &= ((flip1?0x5:0xA) | (flip2?0x3:0xC)); 
+    }
+
+    // 0 -> 10
+    // 1 -> 01
+    // * -> 11
+    // 00 -> 1000
+    // 10 -> 0100
+    // 01 -> 0010
+    // 11 -> 0001
+    // *1 -> 00110011
+    // *0 -> 11001100
+    // 0* -> 10101010
+    // 1* -> 01010101
+    // **1 -> 00001111
+    // **0 -> 11110000
+
+    /**
+       \brief create masks (lsb is left)
+       i = 0: 1010101010101010
+       i = 1: 1100110011001100
+       i = 2: 1111000011110000
+     */
+    unsigned binspr::mk_mask(unsigned i) {
+        // variable number i is false.
+        unsigned mask0 = (1 << (1 << i)) - 1;  // 2^i bits of ones
+        unsigned pos = 1 << (i+1);                  // how many bits in mask 
+
+        unsigned mask = mask0;
+        while (pos < 32) {
+            mask |= (mask0 << pos);
+            pos += 1 << (i + 1);
+        }
+        return mask;
+    }
+
+    void binspr::mk_masks() {
+        for (unsigned i = 0; i < max_lits; ++i) {
+            m_false[i] = mk_mask(i);
+            m_true[i]  = m_false[i] << (1 << i);
+        }
+    }
+
+    /**
+       \brief create Boolean function table
+       corresponding to disjunction of literals
+    */
+    
+    void binspr::add_touched() {
+
+        unsigned mask = 0;
+        for (unsigned i = 0; i < 4; ++i) {
+            switch (m_vals[i]) {
+            case l_true:
+                mask |= m_true[i];
+                break;
+            case l_false:
+                mask |= m_false[i];
+                break;
+            default:
+                break;
+            }
+        }
+        bool first = m_state == ~0;
+        m_state &= mask;
+        TRACE("sat", 
+              {
+                  bool_var vars[4];
+                  vars[0] = m_p; vars[1] = m_q; vars[2] = m_u; vars[3] = m_v;
+                  tout << "touched: ";
+                  for (unsigned i = 0; i < 4; ++i) {
+                      switch (m_vals[i]) {
+                      case l_true:
+                          tout << literal(vars[i], false) << " ";
+                          break;
+                      case l_false:
+                          tout << literal(vars[i], true) << " ";
+                          break;
+                      default:
+                          break;
+                      }
+                  }
+                  display_mask(tout << "  ", m_state);
+              });
+    }
+
+    void binspr::init_g(literal p, literal q, literal u, literal v) {
+        m_p = p.var();
+        m_q = q.var();
+        m_u = u.var();
+        m_v = v.var();
+        m_state = ~0;
+        clear_alpha();
+        VERIFY(touch(~p));
+        VERIFY(touch(~q));
+        add_touched();
+    }
+
+    void binspr::clear_alpha() {
+        m_vals[0] = m_vals[1] = m_vals[2] = m_vals[3] = l_undef;
+    }
+
+    bool binspr::touch(literal p) {
+        bool_var v = p.var();
+        if (v == m_p) m_vals[0] = to_lbool(!p.sign());
+        else if (v == m_q) m_vals[1] = to_lbool(!p.sign());
+        else if (v == m_u) m_vals[2] = to_lbool(!p.sign());
+        else if (v == m_v) m_vals[3] = to_lbool(!p.sign());
+        else return false;
+        return true;
+    }
+
+    std::ostream& binspr::display_mask(std::ostream& out, unsigned mask) const {
+        for (unsigned i = 0; i < 4; ++i) {
+            out << m_vals[i] << " ";
+        }
+        out << " - ";
+        for (unsigned i = 0; i < 32; ++i) {
+            out << (0 != (mask & (1 << i)) ? 1 : 0);           
+        }
+        return out << "\n";
+    }
+}
+

src/sat/sat_binspr.h

@@ -0,0 +1,108 @@
+/*++
+  Copyright (c) 2019 Microsoft Corporation
+
+  Module Name:
+
+   sat_binspr.h
+
+  Abstract:
+   
+    Inprocessing step for creating SPR binary clauses.
+
+  Author:
+
+    Nikolaj Bjorner, Marijn Heule 2019-4-29
+
+  Notes:
+  
+
+  --*/
+#ifndef _SAT_BINSPR_
+#define _SAT_BINSPR_
+
+#include "util/params.h"
+#include "util/statistics.h"
+#include "sat/sat_clause.h"
+#include "sat/sat_types.h"
+
+namespace sat {
+    class solver;
+
+    class binspr {
+        enum states {
+            unit                = 0xA,  // 1010 
+            unit_or_other_nunit = 0xB,  // 1011
+            either              = 0xE,  // 1110    
+            nand                = 0x7,  // 0111
+            not_pr              = 0x0
+        };
+
+        solver& s;
+        unsigned                             m_bin_clauses;
+        unsigned                             m_stopped_at;
+        vector<clause_vector>                m_use_list;
+        unsigned                             m_limit1, m_limit2;
+        svector<bool>                        m_mark, m_mark2;
+        literal_vector                       m_must_candidates, m_may_candidates;
+        unsigned                             m_state;
+
+        void init_g() { m_state = 0x7; }
+        void g_add_binary(literal l1, literal l2, bool flip2);
+        void g_add_unit(literal l1, literal l2);      // l1 is a unit
+        bool g_is_sat() { return m_state != 0; }
+
+        void init_g(literal p, literal q, literal u, literal v);
+
+
+        struct report;
+
+        void block_binary(literal lit1, literal lit2, bool learned);
+        void double_lookahead();
+        
+        void check_spr_single_lookahead(literal lit);
+        void check_spr(literal lit1);
+        void check_spr(literal lit1, literal lit2);
+        bool check_spr(literal p, literal q, literal s, literal r);
+        void binary_are_unit_implied(literal lit1, literal lit2);
+        void clauses_are_unit_implied(literal lit1, literal lit2);
+        void clause_is_unit_implied(literal lit1, literal lit2, clause& c);
+        bool is_used(literal lit) const;
+        void update_candidates(bool& first, unsigned sz1);
+        void collect_candidates(literal lit, literal const* begin, literal const* end);
+        void strengthen_clause(literal lit, literal const* begin, literal const* end);
+
+        bool_var m_p, m_q, m_u, m_v; 
+        lbool m_vals[4];
+
+        void algorithm2();
+        void algorithm2(literal lit, clause const& c);
+        void clear_alpha();
+        void add_touched();
+        bool touch(literal p);
+        void binary_are_unit_implied(literal p);
+        void clauses_are_unit_implied(literal p);
+        void clause_is_unit_implied(clause const& c);
+        static const unsigned max_lits = 5; // = log(32)
+        unsigned m_true[max_lits], m_false[max_lits];
+        unsigned mk_function(svector<lbool> const& lits);
+        void mk_masks();
+        unsigned mk_mask(unsigned i);
+
+        std::ostream& display_mask(std::ostream& out, unsigned mask) const;
+
+    public:
+
+        binspr(solver& s, params_ref const& p): s(s), m_stopped_at(0), m_limit1(1000), m_limit2(300) {}
+
+        ~binspr() {}
+
+        void operator()();
+
+        void updt_params(params_ref const& p) {}
+
+        void collect_statistics(statistics& st) const {} 
+
+    };
+}
+
+#endif