fix bug in PB constraint init_watch handling, adding transitive reduction, HLE, ULT,

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

src/sat/ba_solver.cpp

@@ -216,12 +216,12 @@ namespace sat {
     // ----------------------------
     // card
 
-    bool ba_solver::init_watch(card& c, bool is_true) {
+    bool ba_solver::init_watch(card& c) {
         clear_watch(c);
         literal root = c.lit();
-        if (root != null_literal && root.sign() == is_true) {
+        if (root != null_literal && value(root) == l_false) {
             c.negate();
-			root.neg();
+            root.neg();
         }
         if (root != null_literal) {
             if (!is_watched(root, c)) watch_literal(root, c);
@@ -352,7 +352,7 @@ namespace sat {
             IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true););
             SASSERT(lvl(p.lit()) == 0);
             nullify_tracking_literal(p);
-            init_watch(p, true);
+            init_watch(p);
         }
 
         SASSERT(p.lit() == null_literal || value(p.lit()) != l_false);
@@ -379,7 +379,7 @@ namespace sat {
         }
         else if (true_val == 0 && num_false == 0) {
             if (p.lit() == null_literal || value(p.lit()) == l_true) {
-                init_watch(p, true);
+                init_watch(p);
             }
         }
         else if (true_val >= p.k()) {
@@ -431,7 +431,7 @@ namespace sat {
                 return;
             }
             else if (p.lit() == null_literal || value(p.lit()) == l_true) {
-                init_watch(p, true);
+                init_watch(p);
             }
             else {
                 SASSERT(value(p.lit()) == l_undef);
@@ -510,13 +510,13 @@ namespace sat {
 
 
     // watch a prefix of literals, such that the slack of these is >= k
-    bool ba_solver::init_watch(pb& p, bool is_true) {
+    bool ba_solver::init_watch(pb& p) {
         clear_watch(p);        
-        if (p.lit() != null_literal && p.lit().sign() == is_true) {
+        if (p.lit() != null_literal && value(p.lit()) == l_false) {
             p.negate();           
         }
         
-        SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
+        VERIFY(p.lit() == null_literal || value(p.lit()) == l_true);
         unsigned sz = p.size(), bound = p.k();
 
         // put the non-false literals into the head.
@@ -548,7 +548,7 @@ namespace sat {
 
         if (slack < bound) {
             literal lit = p[j].second;
-            SASSERT(value(lit) == l_false);
+            VERIFY(value(lit) == l_false);
             for (unsigned i = j + 1; i < sz; ++i) {
                 if (lvl(lit) < lvl(p[i].second)) {
                     lit = p[i].second;
@@ -826,7 +826,7 @@ namespace sat {
             SASSERT(p.well_formed());
             
             if (p.lit() == null_literal || value(p.lit()) == l_true) {
-                init_watch(p, true);
+                init_watch(p);
             }
         }
     }
@@ -909,9 +909,9 @@ namespace sat {
         return odd;
     }
 
-    bool ba_solver::init_watch(xor& x, bool is_true) {
+    bool ba_solver::init_watch(xor& x) {
         clear_watch(x);
-        if (x.lit() != null_literal && x.lit().sign() == is_true) {
+        if (x.lit() != null_literal && value(x.lit()) == l_false) {
             x.negate();
         }
         TRACE("ba", display(tout, x, true););
@@ -1566,7 +1566,7 @@ namespace sat {
             m_constraint_to_reinit.push_back(c);
         }
         else if (lit == null_literal) {
-            init_watch(*c, true);
+            init_watch(*c);
         }
         else {
             if (m_solver) m_solver->set_external(lit.var());
@@ -1577,12 +1577,12 @@ namespace sat {
     }
 
 
-    bool ba_solver::init_watch(constraint& c, bool is_true) {
+    bool ba_solver::init_watch(constraint& c) {
         if (inconsistent()) return false;
         switch (c.tag()) {
-        case card_t: return init_watch(c.to_card(), is_true); 
+        case card_t: return init_watch(c.to_card()); 
-        case pb_t: return init_watch(c.to_pb(), is_true); 
+        case pb_t: return init_watch(c.to_pb());
-        case xor_t: return init_watch(c.to_xor(), is_true); 
+        case xor_t: return init_watch(c.to_xor()); 
         }
         UNREACHABLE();
         return false;
@@ -1642,7 +1642,7 @@ namespace sat {
         constraint& c = index2constraint(idx);
         TRACE("ba", tout << l << "\n";);
         if (c.lit() != null_literal && l.var() == c.lit().var()) {
-            init_watch(c, !l.sign());
+            init_watch(c);
             return true;
         }
         else if (c.lit() != null_literal && value(c.lit()) != l_true) {
@@ -2358,7 +2358,7 @@ namespace sat {
         unsigned sz = m_constraint_to_reinit_last_sz;
         for (unsigned i = sz; i < m_constraint_to_reinit.size(); ++i) {
             constraint* c = m_constraint_to_reinit[i];
-            if (!init_watch(*c, true) && !s().at_base_lvl()) {
+            if (!init_watch(*c) && !s().at_base_lvl()) {
                 m_constraint_to_reinit[sz++] = c;
             }
         }
@@ -2677,7 +2677,7 @@ namespace sat {
         }
         else {
             if (c.lit() == null_literal || value(c.lit()) == l_true) {
-                init_watch(c, true);
+                init_watch(c);
             }
             SASSERT(c.lit() == null_literal || is_watched(c.lit(), c));
             SASSERT(c.well_formed());
@@ -2753,10 +2753,7 @@ namespace sat {
             recompile(c);
         }
         else {
-            // review for potential incompleteness: if c.lit() == l_false, do propagations happen?
+            if (c.lit() == null_literal || value(c.lit()) != l_undef) init_watch(c);            
-            if (c.lit() == null_literal || value(c.lit()) == l_true) {    
-                init_watch(c, true);
-            }
             SASSERT(c.well_formed());
         }
     }
@@ -2870,7 +2867,6 @@ namespace sat {
                 s().set_external(v);                
             }
         }
-        IF_VERBOSE(10, verbose_stream() << "non-external variables converted: " << ext << "\n";);
         return ext;
     }
 
@@ -2897,7 +2893,6 @@ namespace sat {
                 ++pure_literals;
             }
         }
-        IF_VERBOSE(10, verbose_stream() << "pure literals converted: " << pure_literals << " " << inconsistent() << "\n";);
         return pure_literals;
     }
 
@@ -3119,7 +3114,7 @@ namespace sat {
                         }
                     }
                     c2.set_size(c2.size() - 1);
-                    init_watch(c2, true);
+                    init_watch(c2);
                     m_simplify_change = true;
 #endif
                 }

src/sat/ba_solver.h

@@ -296,7 +296,7 @@ namespace sat {
         void watch_literal(wliteral w, pb& p);
         bool is_watched(literal l, constraint const& c) const;
         void add_constraint(constraint* c);
-        bool init_watch(constraint& c, bool is_true);
+        bool init_watch(constraint& c);
         void init_watch(bool_var v);
         void clear_watch(constraint& c);
         lbool add_assign(constraint& c, literal l);
@@ -320,7 +320,7 @@ namespace sat {
 
 
         // cardinality
-        bool init_watch(card& c, bool is_true);
+        bool init_watch(card& c);
         lbool add_assign(card& c, literal lit);
         void clear_watch(card& c);
         void reset_coeffs();
@@ -334,7 +334,7 @@ namespace sat {
 
         // xor specific functionality
         void clear_watch(xor& x);
-        bool init_watch(xor& x, bool is_true);
+        bool init_watch(xor& x);
         bool parity(xor const& x, unsigned offset) const;
         lbool add_assign(xor& x, literal alit);
         void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
@@ -345,7 +345,7 @@ namespace sat {
         
         // pb functionality
         unsigned m_a_max;
-        bool init_watch(pb& p, bool is_true);
+        bool init_watch(pb& p);
         lbool add_assign(pb& p, literal alit);
         void add_index(pb& p, unsigned index, literal lit);
         void clear_watch(pb& p);

src/sat/sat_asymm_branch.cpp

@@ -59,7 +59,7 @@ namespace sat {
         }
     };
 
-    void asymm_branch::process(clause_vector& clauses) {
+    void asymm_branch::process(scc& scc, clause_vector& clauses) {
         int64 limit = -m_asymm_branch_limit;
         std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
         m_counter -= clauses.size();
@@ -83,8 +83,9 @@ namespace sat {
                 }
                 s.checkpoint();
                 clause & c = *(*it);
-                if (!process(c))
+                if (m_asymm_branch_sampled ? !process_sampled(scc, c) : !process(c)) {
                     continue; // clause was removed
+                }
                 *it2 = *it;
                 ++it2;
             }
@@ -103,7 +104,7 @@ namespace sat {
     
     void asymm_branch::operator()(bool force) {
         ++m_calls;
-        if (m_calls <= 1)
+        if (m_calls <= m_asymm_branch_delay)
             return;
         if (!m_asymm_branch && !m_asymm_branch_all)
             return;
@@ -118,9 +119,27 @@ namespace sat {
         TRACE("asymm_branch_detail", s.display(tout););
         report rpt(*this);
         svector<char> saved_phase(s.m_phase);
-        m_counter  = 0; 
+        if (m_asymm_branch_sampled) {
-        process(s.m_clauses);
+            scc scc(s, m_params);
-        m_counter = -m_counter;
+            while (true) {
+                unsigned elim = m_elim_literals;
+                scc.init_big(true);
+                process(scc, s.m_clauses);
+                process(scc, s.m_learned);
+                s.propagate(false); 
+                if (s.m_inconsistent)
+                    break;
+                std::cout << m_elim_literals - elim << "\n";
+                if (m_elim_literals == elim)
+                    break;
+            }
+        }
+        else {
+            scc scc(s, m_params);
+            m_counter  = 0; 
+            process(scc, s.m_clauses);
+            m_counter = -m_counter;
+        }
         s.m_phase = saved_phase;
         m_asymm_branch_limit *= 2;
         if (m_asymm_branch_limit > UINT_MAX)
@@ -145,12 +164,6 @@ namespace sat {
         return true;
     }
 
-    void asymm_branch::setup_big() {
-        scc scc(s, m_params);
-        vector<literal_vector> const& big = scc.get_big(true); // include learned binary clauses 
-        
-    }
-
     struct asymm_branch::compare_left {
         scc& s;
         compare_left(scc& s): s(s) {}
@@ -206,19 +219,34 @@ namespace sat {
                 right = right2;
             }
         }
-        right = scc.get_right(m_neg[0]);
+        if (m_to_delete.empty()) {
-        for (unsigned i = 1; i < m_neg.size(); ++i) {
+            right = scc.get_right(m_neg[0]);
-            literal lit = m_neg[i];
+            for (unsigned i = 1; i < m_neg.size(); ++i) {
-            int right2 = scc.get_right(lit);
+                literal lit = m_neg[i];
-            if (right > right2) {
+                int right2 = scc.get_right(lit);
-                // ~first => ~lit
+                if (right > right2) {
-                m_to_delete.push_back(~lit);
+                    // ~first => ~lit
-            }
+                    m_to_delete.push_back(~lit);
-            else {
+                }
-                right = right2;
+                else {
+                    right = right2;
+                }
             }
         }
         if (!m_to_delete.empty()) {
+#if 0
+            std::cout << "delete " << m_to_delete << "\n";
+
+            std::cout << "pos\n";
+            for (literal l : m_pos) {
+                std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
+            }
+            std::cout << "neg\n";
+            for (literal l : m_neg) {
+                std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
+            }
+            std::cout << "\n";
+#endif
             unsigned j = 0;
             for (unsigned i = 0; i < c.size(); ++i) {
                 if (!m_to_delete.contains(c[i])) {
@@ -283,12 +311,12 @@ namespace sat {
             }
         }
         new_sz = j;        
-        m_elim_literals += c.size() - new_sz;
         // std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n";
         return re_attach(scoped_d, c, new_sz);
     }
 
    bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
+       m_elim_literals += c.size() - new_sz;
        switch(new_sz) {
        case 0:
             s.set_conflict(justification());
@@ -315,8 +343,9 @@ namespace sat {
         }
     }
 
-    bool asymm_branch::process2(scc& scc, clause & c) {
+    bool asymm_branch::process_sampled(scc& scc, clause & c) {
         scoped_detach scoped_d(s, c);
+        sort(scc, c);
         if (uhte(scc, c)) {
             scoped_d.del_clause();
             return false;
@@ -372,6 +401,8 @@ namespace sat {
     void asymm_branch::updt_params(params_ref const & _p) {
         sat_asymm_branch_params p(_p);
         m_asymm_branch        = p.asymm_branch();
+        m_asymm_branch_delay = p.asymm_branch_delay();
+        m_asymm_branch_sampled = p.asymm_branch_sampled();
         m_asymm_branch_limit  = p.asymm_branch_limit();
         m_asymm_branch_all    = p.asymm_branch_all();
         if (m_asymm_branch_limit > UINT_MAX)

src/sat/sat_asymm_branch.h

@@ -39,6 +39,8 @@ namespace sat {
         
         // config
         bool       m_asymm_branch;
+        unsigned   m_asymm_branch_delay;
+        bool       m_asymm_branch_sampled;
         bool       m_asymm_branch_all;
         int64      m_asymm_branch_limit;
 
@@ -60,9 +62,9 @@ namespace sat {
 
         bool process(clause & c);
 
-        bool process2(scc& scc, clause & c);
+        bool process_sampled(scc& scc, clause & c);
 
-        void process(clause_vector & c);
+        void process(scc& scc, clause_vector & c);
         
         bool process_all(clause & c);
         
@@ -72,8 +74,6 @@ namespace sat {
 
         bool propagate_literal(clause const& c, literal l);
 
-        void setup_big();
-
     public:
         asymm_branch(solver & s, params_ref const & p);
 

src/sat/sat_asymm_branch_params.pyg

@@ -2,5 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_asymm_branch_params',
                   export=True,
                   params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
+                          ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
+                          ('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'),
                           ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
                           ('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause')))

src/sat/sat_lookahead.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "sat/sat_solver.h"
 #include "sat/sat_extension.h"
 #include "sat/sat_lookahead.h"
+#include "sat/sat_scc.h"
 #include "util/union_find.h"
 
 namespace sat {
@@ -2304,15 +2305,86 @@ namespace sat {
 
     void lookahead::add_hyper_binary() {
 
+        unsigned num_lits = m_s.num_vars() * 2;
+
+#if 0
         std::cout << "binary trail size: " << m_binary_trail.size() << "\n";
         std::cout << "Are windfalls still on the trail at base level?\n";
-        unsigned num_lits = m_s.num_vars() * 2;
+#endif   
+
+        unsigned disconnected1 = 0;
+        unsigned disconnected2 = 0;
+
+#if 1
+        typedef std::pair<unsigned, unsigned> u_pair;
+        hashtable<u_pair, pair_hash<unsigned_hash, unsigned_hash>, default_eq<u_pair> > imp;
+        for (unsigned idx = 0; idx < num_lits; ++idx) {
+            literal u = get_parent(to_literal(idx));
+            if (null_literal != u) {
+                for (watched const& w : m_s.m_watches[idx]) {
+                    if (!w.is_binary_clause()) continue;
+                    literal v = get_parent(w.get_literal());
+                    if (null_literal != v) {
+                        imp.insert(std::make_pair(u.index(), v.index()));
+                    }
+                }
+            }
+        }
+
+        scc scc(m_s, m_s.m_params);
+        scc.init_big(true);
+        svector<std::pair<literal, literal>> candidates;
+
         unsigned_vector bin_size(num_lits);
         for (unsigned idx : m_binary_trail) {
             bin_size[idx]++;
         }
+        for (unsigned idx = 0; idx < num_lits; ++idx) {
+            literal u = to_literal(idx);
+            if (u != get_parent(u)) continue;
+            if (m_s.was_eliminated(u.var())) continue;
+            literal_vector const& lits = m_binary[idx];
+            for (unsigned sz = bin_size[idx]; sz > 0; --sz) {
+                literal v = lits[lits.size() - sz];
+                if (v != get_parent(v)) continue;
+                if (m_s.was_eliminated(v.var())) continue;
+                if (imp.contains(std::make_pair(u.index(), v.index()))) continue;
+                if (scc.reaches(u, v)) continue;
+                candidates.push_back(std::make_pair(u, v));
+            }
+        }
+        for (unsigned i = 0; i < 5; ++i) {
+            scc.init_big(true);
+            unsigned k = 0;
+            union_find_default_ctx ufctx;
+            union_find<union_find_default_ctx> uf(ufctx);
+            for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
+            for (unsigned j = 0; j < candidates.size(); ++j) {
+                literal u = candidates[j].first;
+                literal v = candidates[j].second;
+                if (!scc.reaches(u, v)) {
+                    if (uf.find(u.index()) != uf.find(v.index())) {
+                        ++disconnected1;
+                        uf.merge(u.index(), v.index());
+                        uf.merge((~u).index(), (~v).index());
+                        m_s.mk_clause(~u, v, true);
+                    }
+                    else {
+                        candidates[k] = candidates[j];
+                        ++k;
+                    }
+                }
+            }
+            std::cout << candidates.size() << " -> " << k << "\n";
+            if (k == candidates.size()) break;
+            candidates.shrink(k);
+        }
 
+        std::cout << "candidates: " << candidates.size() << "\n";
 
+#endif
+
+#if 0
         union_find_default_ctx ufctx;
         union_find<union_find_default_ctx> uf(ufctx);
         for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
@@ -2329,21 +2401,25 @@ namespace sat {
             }
         }
 
-        unsigned disconnected = 0;
         for (unsigned i = 0; i < m_binary.size(); ++i) {
             literal u = to_literal(i);
-            if (u == get_parent(u)) {
+            if (u == get_parent(u) && !m_s.was_eliminated(u.var())) {
                 for (literal v : m_binary[i]) {
-                    if (v == get_parent(v) && uf.find(u.index()) != uf.find(v.index())) {
+                    if (v == get_parent(v) && 
-                        ++disconnected;
+                        !m_s.was_eliminated(v.var()) && 
+                        uf.find(u.index()) != uf.find(v.index())) {
+                        ++disconnected2;
                         uf.merge(u.index(), v.index());
-                        m_s.mk_clause(~u, v, true);
+                        // m_s.mk_clause(~u, v, true);
                     }
                 }
             }
         }
-        IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";);
+#endif
-        m_stats.m_bca += disconnected;
+        
+        IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected1 << " " << disconnected2 << ")\n";);
+        //IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";);
+        //m_stats.m_bca += disconnected;
     }
 
     void lookahead::normalize_parents() {

src/sat/sat_scc.cpp

@@ -234,17 +234,7 @@ namespace sat {
         return to_elim.size();
     }
 
-    // shuffle vertices to obtain different DAG traversal each time
+    void scc::init_big(bool learned) {
-    void scc::shuffle(literal_vector& lits) {
-        unsigned sz = lits.size();
-        if (sz > 1) {
-            for (unsigned i = sz; i-- > 0; ) {
-                std::swap(lits[i], lits[m_rand(i+1)]);
-            }
-        }
-    }
-
-    vector<literal_vector> const& scc::get_big(bool learned) {
         unsigned num_lits = m_solver.num_vars() * 2;
         m_dag.reset();
         m_roots.reset();
@@ -263,53 +253,21 @@ namespace sat {
                     edges.push_back(v);
                 }
             }
-            shuffle(edges);
+            shuffle<literal>(edges.size(), edges.c_ptr(), m_rand);
         }
-        return m_dag;
+        init_dfs_num(learned);
     }
 
-    void scc::get_dfs_num(bool learned) {
+    struct scc::pframe {
-        unsigned num_lits = m_solver.num_vars() * 2;
+        literal m_parent;
-        SASSERT(m_left.size() == num_lits);
+        literal m_child;
-        SASSERT(m_right.size() == num_lits);
+        pframe(literal p, literal c):
-        literal_vector todo;
+            m_parent(p), m_child(c) {}
-        // retrieve literals that have no predecessors
+        literal child() const { return m_child; }
-        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
+        literal parent() const { return m_parent; }
-            literal u(to_literal(l_idx));
+    };
-            if (m_roots[u.index()]) todo.push_back(u);
-        }
-        shuffle(todo);
-        int dfs_num = 0;
-        while (!todo.empty()) {
-            literal u = todo.back();
-            int& d = m_left[u.index()];
-            // already visited
-            if (d > 0) {
-                if (m_right[u.index()] < 0) {
-                    m_right[u.index()] = dfs_num;
-                }
-                todo.pop_back();
-            }
-            // visited as child:
-            else if (d < 0) {
-                d = -d;
-                for (literal v : m_dag[u.index()]) {
-                    if (m_left[v.index()] == 0) {
-                        m_left[v.index()] = - d - 1;
-                        m_root[v.index()] = m_root[u.index()];
-                        m_parent[v.index()] = u;
-                        todo.push_back(v);
-                    }
-                }
-            }
-            // new root.
-            else {
-                d = --dfs_num;
-            }
-        }
-    }
 
-    unsigned scc::reduce_tr(bool learned) {        
+    void scc::init_dfs_num(bool learned) {
         unsigned num_lits = m_solver.num_vars() * 2;
         m_left.reset();
         m_right.reset();
@@ -317,11 +275,61 @@ namespace sat {
         m_parent.reset();
         m_left.resize(num_lits, 0);
         m_right.resize(num_lits, -1);
+        m_root.resize(num_lits, null_literal);
+        m_parent.resize(num_lits, null_literal);
         for (unsigned i = 0; i < num_lits; ++i) {
             m_root[i]   = to_literal(i);
             m_parent[i] = to_literal(i);            
         }
-        get_dfs_num(learned);
+        svector<pframe> todo;
+        // retrieve literals that have no predecessors
+        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
+            literal u(to_literal(l_idx));
+            if (m_roots[u.index()]) {
+                todo.push_back(pframe(null_literal, u));
+            }
+        }
+        shuffle<pframe>(todo.size(), todo.c_ptr(), m_rand);
+        int dfs_num = 0;
+        while (!todo.empty()) {
+            literal u = todo.back().child();
+            if (m_left[u.index()] > 0) {
+                // already visited
+                if (m_right[u.index()] < 0) {
+                    m_right[u.index()] = ++dfs_num;
+                }
+                todo.pop_back();
+            }
+            else {
+                SASSERT(m_left[u.index()] == 0);
+                m_left[u.index()] = ++dfs_num;
+                for (literal v : m_dag[u.index()]) {
+                    if (m_left[v.index()] == 0) {
+                        todo.push_back(pframe(u, v));
+                    }
+                }
+                literal p = todo.back().parent();
+                if (p != null_literal) {
+                    m_root[u.index()] = m_root[p.index()];
+                    m_parent[u.index()] = p;
+                }
+            }
+        }
+        for (unsigned i = 0; i < num_lits; ++i) {
+            if (m_right[i] < 0) {
+                VERIFY(m_left[i] == 0);
+                m_left[i]  = ++dfs_num;
+                m_right[i] = ++dfs_num;
+            }
+        }
+        for (unsigned i = 0; i < num_lits; ++i) {
+            VERIFY(m_left[i] < m_right[i]);
+        }
+    }
+
+    unsigned scc::reduce_tr(bool learned) {        
+        unsigned num_lits = m_solver.num_vars() * 2;
+        init_big(learned);
         unsigned idx = 0;
         unsigned elim = m_num_elim_bin;
         for (watch_list & wlist : m_solver.m_watches) {
@@ -333,7 +341,7 @@ namespace sat {
                 watched& w = *it;
                 if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) {
                     literal v = w.get_literal();
-                    if (m_left[u.index()] + 1 < m_left[v.index()]) {
+                    if (reaches(u, v) && u != get_parent(v)) {
                         ++m_num_elim_bin;
                     }
                     else {

src/sat/sat_scc.h

@@ -44,10 +44,13 @@ namespace sat {
         svector<int>           m_left, m_right;
         literal_vector         m_root, m_parent;
 
-        void shuffle(literal_vector& lits);
         void reduce_tr();
         unsigned reduce_tr(bool learned);
 
+        void init_dfs_num(bool learned);
+
+        struct pframe;
+
     public:
 
         scc(solver & s, params_ref const & p);
@@ -60,17 +63,14 @@ namespace sat {
         void reset_statistics();
 
         /*
-          \brief retrieve binary implication graph
+          \brief create binary implication graph and associated data-structures to check transitivity.
          */
-        vector<literal_vector> const& get_big(bool learned);
+        void init_big(bool learned);
-
         int get_left(literal l) const { return m_left[l.index()]; }
         int get_right(literal l) const { return m_right[l.index()]; }
         literal get_parent(literal l) const { return m_parent[l.index()]; }
         literal get_root(literal l) const { return m_root[l.index()]; }
-
+        bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
-        void get_dfs_num(bool learned);
-
     };
 };
 

src/sat/sat_simplifier_params.pyg

@@ -2,7 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_simplifier_params',
                   export=True,
                   params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
-                          ('abce', BOOL, BOOL, False, 'eliminate blocked clauses using asymmmetric literals'),
+                          ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'),
                           ('cce', BOOL, False, 'eliminate covered clauses'),
                           ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'),
                           ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),