diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 9bc54ae74..c0a13fa77 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -96,10 +96,10 @@ struct pb2bv_rewriter::imp {
                   case l_undef: tout << "= "; break;
                   case l_false: tout << ">= "; break;
                   }
-                  tout << m_k << "\n";);
+                  tout << k << "\n";);
             if (k.is_zero()) {
                 if (is_le != l_false) {
-                    return expr_ref(m.mk_not(mk_or(m, sz, args)), m);
+                    return expr_ref(m.mk_not(::mk_or(m, sz, args)), m);
                 }
                 else {
                     return expr_ref(m.mk_true(), m);
@@ -108,6 +108,15 @@ struct pb2bv_rewriter::imp {
             if (k.is_neg()) {
                 return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
             }
+            
+            expr_ref result(m);
+            switch (is_le) {
+            case l_true:  if (mk_le(sz, args, k, result)) return result; else break;
+            case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
+            case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
+            }
+
+            // fall back to divide and conquer encoding.
             SASSERT(k.is_pos());
             expr_ref zero(m), bound(m);
             expr_ref_vector es(m), fmls(m);
@@ -139,12 +148,12 @@ struct pb2bv_rewriter::imp {
             }
             switch (is_le) {
             case l_true: 
-                return mk_and(fmls);
+                return ::mk_and(fmls);
             case l_false:
                 if (!es.empty()) {
                     fmls.push_back(bv.mk_ule(bound, es.back()));
                 }
-                return mk_or(fmls);
+                return ::mk_or(fmls);
             case l_undef:
                 if (es.empty()) {
                     fmls.push_back(m.mk_bool_val(k.is_zero()));
@@ -152,13 +161,180 @@ struct pb2bv_rewriter::imp {
                 else {
                     fmls.push_back(m.mk_eq(bound, es.back()));
                 }
-                return mk_and(fmls);
+                return ::mk_and(fmls);
             default:
                 UNREACHABLE();
                 return expr_ref(m.mk_true(), m);
             }
         }
 
+        /**
+           \brief MiniSat+ based encoding of PB constraints. 
+           The procedure is described in "Translating Pseudo-Boolean Constraints into SAT "
+           Niklas Een, Niklas Sörensson, JSAT 2006.
+         */
+
+        const unsigned primes[7] = { 2, 3, 5, 7, 11, 13, 17};
+
+        vector<rational> m_min_base;
+        rational         m_min_cost;
+        vector<rational> m_base;
+
+        void create_basis(vector<rational> const& seq, rational carry_in, rational cost) {
+            if (cost >= m_min_cost) {
+                return;
+            }
+            rational delta_cost(0);
+            for (unsigned i = 0; i < seq.size(); ++i) {
+                delta_cost += seq[i];
+            }
+            if (cost + delta_cost < m_min_cost) {
+                m_min_cost = cost + delta_cost;
+                m_min_base = m_base;             
+                m_min_base.push_back(delta_cost + rational::one());
+            }
+            
+            for (unsigned i = 0; i < sizeof(primes)/sizeof(*primes); ++i) {
+                vector<rational> seq1;
+                rational p(primes[i]);
+                rational rest = carry_in;
+                // create seq1
+                for (unsigned j = 0; j < seq.size(); ++j) {
+                    rest += seq[j] % p;
+                    if (seq[j] >= p) {
+                        seq1.push_back(div(seq[j],  p));
+                    }
+                }
+                
+                m_base.push_back(p);
+                create_basis(seq1, div(rest, p), cost + rest);
+                m_base.pop_back();
+            }
+        }
+
+        bool create_basis() {
+            m_base.reset();
+            m_min_cost = rational(INT_MAX);
+            m_min_base.reset();
+            rational cost(0);
+            create_basis(m_coeffs, rational::zero(), cost);
+            m_base = m_min_base;
+            TRACE("pb",
+                  tout << "Base: ";
+                  for (unsigned i = 0; i < m_base.size(); ++i) {
+                      tout << m_base[i] << " ";
+                  }
+                  tout << "\n";);
+            return 
+                !m_base.empty() && 
+                m_base.back().is_unsigned() &&
+                m_base.back().get_unsigned() <= 20*m_base.size();
+        }
+
+        /**
+           \brief Check if 'out mod n >= lim'. 
+         */
+        expr_ref mod_ge(ptr_vector<expr> const& out, unsigned n, unsigned lim) {
+            TRACE("pb", for (unsigned i = 0; i < out.size(); ++i) tout << mk_pp(out[i], m) << " "; tout << "\n";
+                  tout << "n:" << n << " lim: " << lim << "\n";);
+            if (lim == n) {
+                return expr_ref(m.mk_false(), m);
+            }
+            if (lim == 0) {
+                return expr_ref(m.mk_true(), m);
+            }
+            SASSERT(0 < lim && lim < n);
+            expr_ref_vector ors(m);
+            for (unsigned j = 0; j + lim - 1 < out.size(); j += n) {
+                expr_ref tmp(m);
+                tmp = out[j + lim - 1];
+                if (j + n < out.size()) {
+                    tmp = m.mk_and(tmp, m.mk_not(out[j + n]));
+                }
+                ors.push_back(tmp);
+            }
+            return ::mk_or(ors);
+        }
+
+        bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) {
+            if (!create_basis()) return false;
+            if (!bound.is_unsigned()) return false;
+            vector<rational> coeffs(m_coeffs);
+            result = m.mk_true();
+            expr_ref_vector carry(m), new_carry(m);
+            for (unsigned i = 0; i < m_base.size(); ++i) {
+                rational b_i = m_base[i];
+                unsigned B   = b_i.get_unsigned();
+                unsigned d_i = (bound % b_i).get_unsigned();
+                bound = div(bound, b_i);                
+                for (unsigned j = 0; j < coeffs.size(); ++j) {
+                    rational c = coeffs[j] % b_i;                    
+                    SASSERT(c.is_unsigned());
+                    for (unsigned k = 0; k < c.get_unsigned(); ++k) {
+                        carry.push_back(args[j]);
+                    }
+                    coeffs[j] = div(coeffs[j], b_i);
+                }
+                TRACE("pb", tout << "Carry: " << carry << "\n";
+                      for (unsigned j = 0; j < coeffs.size(); ++j) tout << coeffs[j] << " ";
+                      tout << "\n";
+                      );
+                ptr_vector<expr> out;
+                m_sort.sorting(carry.size(), carry.c_ptr(), out);
+
+                expr_ref gt = mod_ge(out, B, d_i + 1);
+                expr_ref ge = mod_ge(out, B, d_i);
+                result = mk_or(gt, mk_and(ge, result));                
+                TRACE("pb", tout << result << "\n";);
+
+                new_carry.reset();
+                for (unsigned j = B - 1; j < out.size(); j += B) {
+                    new_carry.push_back(out[j]);
+                }
+                carry.reset();
+                carry.append(new_carry);
+            }
+            TRACE("pb", tout << result << "\n";);
+            return true;
+        }
+
+        expr_ref mk_and(expr_ref& a, expr_ref& b) {
+            if (m.is_true(a)) return b;
+            if (m.is_true(b)) return a;
+            if (m.is_false(a)) return a;
+            if (m.is_false(b)) return b;
+            return expr_ref(m.mk_and(a, b), m);
+        }
+
+        expr_ref mk_or(expr_ref& a, expr_ref& b) {
+            if (m.is_true(a)) return a;
+            if (m.is_true(b)) return b;
+            if (m.is_false(a)) return b;
+            if (m.is_false(b)) return a;
+            return expr_ref(m.mk_or(a, b), m);
+        }
+
+        bool mk_le(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
+            expr_ref_vector args1(m);
+            rational bound(-k);            
+            for (unsigned i = 0; i < sz; ++i) {
+                args1.push_back(mk_not(args[i]));
+                bound += m_coeffs[i];
+            }
+            return mk_ge(sz, args1.c_ptr(), bound, result);
+        }
+
+        bool mk_eq(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
+            expr_ref r1(m), r2(m);
+            if (mk_ge(sz, args, k, r1) && mk_le(sz, args, k, r2)) {
+                result = m.mk_and(r1, r2);
+                return true;
+            }
+            else {
+                return false;
+            }
+        }
+
         expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
             decl_kind kind = f->get_decl_kind();
             rational k = pb.get_k(f);
@@ -403,7 +579,7 @@ struct pb2bv_rewriter::imp {
         }
         
         void mk_clause(unsigned n, literal const* lits) {
-            m_imp.m_lemmas.push_back(mk_or(m, n, lits));
+            m_imp.m_lemmas.push_back(::mk_or(m, n, lits));
         }        
 
         void keep_cardinality_constraints(bool f) {
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index f70ceab38..eb713ab7c 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -33,6 +33,7 @@ namespace sat {
         literal_vector  m_units;
         unsigned_vector m_units_lim;
         unsigned_vector m_learned_lim;
+        unsigned_vector m_binary;
 
 
         void init() {
@@ -44,6 +45,7 @@ namespace sat {
             m_learned_lim.push_back(s.m_learned.size());
             m_units_lim.push_back(m_units.size());
             m_trail.push_back(lit);
+            m_binary.push_back(0);
             s.push();
             assign(lit);
         }
@@ -58,27 +60,31 @@ namespace sat {
                 s.m_cls_allocator.del_clause(r);
             }
             s.m_learned.shrink(old_sz);
-            literal lits[2] = { m_trail.back(), null_literal };
             unsigned new_unit_sz = m_units_lim.back();
-            for (unsigned i = m_units.size(); i > new_unit_sz; ) {
-                --i;
-                lits[1] = m_units[i];
+            for (unsigned i = new_unit_sz; i < m_units.size(); ++i) {
+                literal lits[2] = { ~m_trail.back(), m_units[i] };
                 clause * r = s.m_cls_allocator.mk_clause(2, lits, true);
                 s.m_learned.push_back(r);
             }
             m_units.shrink(new_unit_sz);
             m_units_lim.pop_back();
             m_trail.pop_back();
+            m_binary.pop_back();
         }
         
-        unsigned diff(unsigned value0) const {
-            unsigned value1 = get_state_value();
-            SASSERT(value1 >= value0);
-            return value1 - value0;
+        unsigned diff() const { return m_binary.back() + m_units.size() - m_units_lim.back(); }
+
+        unsigned mix_diff(unsigned l, unsigned r) const { return l + r + (1 << 10) * l * r; }
+
+        clause const& get_clause(watch_list::iterator it) const {
+            clause_offset cls_off = it->get_clause_offset();
+            return *(s.m_cls_allocator.get_clause(cls_off));
         }
 
-        unsigned mix_diff(unsigned l, unsigned r) const {
-            return l + r + (1 << 10) * l * r;
+        bool is_nary_propagation(clause const& c, literal l) const {
+            bool r = c.size() > 2 && ((c[0] == l && s.value(c[1]) == l_false) || (c[1] == l && s.value(c[0]) == l_false));
+            DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
+            return r;
         }
 
         void get_resolvent_units(literal lit) {
@@ -94,34 +100,33 @@ namespace sat {
                     switch (it->get_kind()) {
                     case watched::TERNARY:
                         if (s.value(it->get_literal1()) == l_false && 
-                            s.value(it->get_literal()) == l_false) {
+                            s.value(it->get_literal2()) == l_false) {
                             m_units.push_back(l);
-                            goto done_watch_list;
+                            goto done_finding_unit;
                         }
                         break;
                     case watched::CLAUSE: {
-                        clause_offset cls_off = it->get_clause_offset();
-                        clause & c = *(s.m_cls_allocator.get_clause(cls_off));
-                        if (c.size() == 2) break;
-                        SASSERT(c.size() > 2);
-                        if (c[0] == l && s.value(c[1]) == l_false) {
-                            DEBUG_CODE(for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
+                        clause const & c = get_clause(it);
+                        SASSERT(c[0] == l || c[1] == l);
+                        if (is_nary_propagation(c, l)) {
                             m_units.push_back(l);
-                            goto done_watch_list;
-                        } 
-                        if (c[1] == l && s.value(c[0]) == l_false) {
-                            DEBUG_CODE(for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
-                            m_units.push_back(l);
-                            goto done_watch_list;
-                        } 
+                            goto done_finding_unit;
+                        }
                         break;
                     }
                     default:
                         break;
                     }
                 }
-            done_watch_list:
+            done_finding_unit:
+
+                //
+                // TBD: count binary clauses created by propagation.
+                // They used to be in the watch list of l.index(), 
+                // both new literals in watch list should be unassigned.
+                //
                 continue;
+
             }
         }
 
@@ -131,10 +136,6 @@ namespace sat {
             return l;
         }
 
-        unsigned get_state_value() const {
-            return s.m_learned.size();
-        }
-
         bool choose1(literal& l) {
             literal_vector P;
             pre_select(P);
@@ -142,28 +143,26 @@ namespace sat {
             if (P.empty()) {
                 return true;
             }
-            unsigned value0 = get_state_value();
             unsigned h = 0, count = 1;
-            literal_vector& units = m_units;;
             for (unsigned i = 0; i < P.size(); ++i) {
                 literal lit = P[i];
 
                 push(lit);
-                if (do_double(value0)) double_look();
+                if (do_double()) double_look(P);
                 if (inconsistent()) {
                     pop();
                     assign(~lit);
-                    if (do_double(value0)) double_look();
+                    if (do_double()) double_look(P);
                     if (inconsistent()) return true;
                     continue;
                 }
-                unsigned diff1 = diff(value0);
+                unsigned diff1 = diff();
                 pop();
                 
                 push(~lit);
-                if (do_double(value0)) double_look();
+                if (do_double()) double_look(P);
                 bool unsat2 = inconsistent();
-                unsigned diff2 = diff(value0);
+                unsigned diff2 = diff();
                 pop();
 
                 if (unsat2) {
@@ -173,25 +172,28 @@ namespace sat {
 
                 unsigned mixd = mix_diff(diff1, diff2);
 
+
                 if (mixd > h || (mixd == h && s.m_rand(count) == 0)) {
+                    CTRACE("sat", l != null_literal, tout << lit << " diff1: " << diff1 << " diff2: " << diff2 << "\n";);
+                    if (mixd > h) count = 1; else ++count;
                     h = mixd;
                     l = diff1 < diff2 ? lit : ~lit;
-                    ++count;
                 }
             }
             return l != null_literal;
         }
 
-        void double_look() {
-            literal_vector P;
-            pre_select(P);
+        void double_look(literal_vector const& P) {
+            bool unsat;
             for (unsigned i = 0; !inconsistent() && i < P.size(); ++i) {
                 literal lit = P[i];
+                if (s.value(lit) != l_undef) continue;
 
                 push(lit);
-                bool unsat = inconsistent();
+                unsat = inconsistent();
                 pop();
                 if (unsat) {
+                    TRACE("sat", tout << "unit: " << ~lit << "\n";);
                     assign(~lit);
                     continue;
                 }
@@ -200,6 +202,7 @@ namespace sat {
                 unsat = inconsistent();
                 pop();
                 if (unsat) {
+                    TRACE("sat", tout << "unit: " << lit << "\n";);
                     assign(lit);
                 }
 
@@ -211,6 +214,7 @@ namespace sat {
             s.assign(l, justification());
             s.propagate(false);
             get_resolvent_units(l);
+            TRACE("sat", s.display(tout << l << " @ " << s.scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
         }
 
         bool inconsistent() { return s.inconsistent(); }
@@ -220,6 +224,18 @@ namespace sat {
             order_by_implication_trees(P);            
         }
 
+        void check_binary(clause const& c, literal lit1, literal& lit2) {
+            if (c.size() == 2) {
+                if (c[0] == lit1) {
+                    lit2 = c[1];
+                }
+                else {
+                    SASSERT(c[1] == lit1);
+                    lit2 = c[0];
+                }
+            }
+        }
+
         void order_by_implication_trees(literal_vector& P) {
             literal_set roots;
             literal_vector nodes, parent;
@@ -246,28 +262,19 @@ namespace sat {
                         lit2 = it->get_literal();
                         break;
                     case watched::CLAUSE: {
-                        clause_offset cls_off = it->get_clause_offset();
-                        clause & c = *(s.m_cls_allocator.get_clause(cls_off));
-                        if (c.size() == 2) {
-                            if (c[0] == ~lit1) {
-                                lit2 = c[1];
-                            }
-                            else {
-                                SASSERT(c[1] == ~lit1);
-                                lit2 = c[0];
-                            }
-                        }
+                        clause const & c = get_clause(it);
+                        check_binary(c, lit1, lit2);
                         break;
                     }
                     default:
                         break;
                     }
                     
-                    if (lit2 != null_literal && roots.contains(lit2)) {
-                        // lit2 => lit1
+                    if (lit2 != null_literal && roots.contains(~lit2)) {
+                        // ~lit2 => lit1
                         // if lit2 is a root, put it under lit2
-                        parent.setx(lit2.index(), lit1, null_literal);
-                        roots.remove(lit2);
+                        parent.setx((~lit2).index(), lit1, null_literal);
+                        roots.remove(~lit2);
                         roots.insert(lit1);
                         goto found;
                     }
@@ -287,17 +294,8 @@ namespace sat {
                         lit2 = it->get_literal();
                         break;
                     case watched::CLAUSE: {
-                        clause_offset cls_off = it->get_clause_offset();
-                        clause & c = *(s.m_cls_allocator.get_clause(cls_off));
-                        if (c.size() == 2) {
-                            if (c[0] == lit1) {
-                                lit2 = c[1];
-                            }
-                            else {
-                                SASSERT(c[1] == lit1);
-                                lit2 = c[0];
-                            }
-                        }
+                        clause const & c = get_clause(it);
+                        check_binary(c, ~lit1, lit2);
                         break;
                     }
                     default:
@@ -311,19 +309,21 @@ namespace sat {
                         goto found;
                     }
                 }
-                std::cout << "no parents or children of literal " << lit1 << "\n";
                 nodes.push_back(lit1);
                 roots.insert(lit1);                
             found:
                 ;
-            }       
-            std::cout << "implication trees\n";
-            for (unsigned i = 0; i < parent.size(); ++i) {
-                literal p = parent[i];
-                if (p != null_literal) {
-                    std::cout << to_literal(i) << " |-> " << p << "\n";
-                }
-            }
+            }    
+            TRACE("sat", 
+                  tout << "implication trees\n";
+                  for (unsigned i = 0; i < parent.size(); ++i) {
+                      literal p = parent[i];
+                      if (p != null_literal) {
+                          tout << to_literal(i) << " |-> " << p << "\n";
+                      }
+                  });
+
+            // TBD: extract ordering.
             
         }
 
@@ -335,9 +335,8 @@ namespace sat {
             }
         }
 
-        bool do_double(unsigned value0) {
-            unsigned value1 = get_state_value();
-            return !inconsistent() && value1 - value0 > m_delta_trigger;
+        bool do_double() {
+            return !inconsistent() && diff() > m_delta_trigger;
         }
 
         void update_delta_trigger() {
@@ -368,11 +367,11 @@ namespace sat {
                 s.checkpoint();
                 BACKTRACK;
                 literal l = choose();
-                TRACE("sat", tout << l << "\n";);
                 BACKTRACK;
                 if (l == null_literal) {
                     return l_true;
                 }
+                TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
                 push(l);
                 trail.push_back(l);
             }
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index b0efbd346..33514730f 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -558,7 +558,7 @@ Notes:
             m_stats.m_num_compiled_clauses++;
             m_stats.m_num_clause_vars += n;
             literal_vector tmp(n, ls);
-            TRACE("pb", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";);
+            TRACE("pb_verbose", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";);
             ctx.mk_clause(n, tmp.c_ptr());
         }