diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 135e0f80ee8..d316f936058 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -649,6 +649,7 @@ class maxres : public maxsmt_solver_base {
         }
     }
 
+
     void max_resolve(exprs const& core, rational const& w) {
         SASSERT(!core.empty());
         expr_ref fml(m), asum(m);
@@ -699,6 +700,88 @@ class maxres : public maxsmt_solver_base {
         }
     }
 
+#if 0
+
+    void bin_max_resolve(exprs const& _core, rational const& w) {
+        expr_ref_vector core(m, _core.size(), _core.data());
+        expr_ref fml(m), cls(m);
+        for (unsigned i = 0; i + 1 < core.size(); ++i) {
+            expr* a = core.get(i);
+            expr* b = core.get(i + 1);
+            expr_ref u = mk_fresh_bool("u");
+            expr_ref v = mk_fresh_bool("v");
+            // u = a or b
+            // v = a and b
+            cls = m.mk_or(a, b);
+            fml = m.mk_implies(u, cls);
+            add(fml);
+            update_model(u, cls);
+            m_defs.push_back(fml);
+            cls = m.mk_and(a, b);
+            fml = m.mk_implies(v, cls);
+            add(fml);
+            update_model(v, cls);
+            m_defs.push_back(fml);
+            new_assumption(u, w);
+            core.push_back(v);
+        }
+    }
+
+    struct unfold_record {
+        ptr_vector<expr> ws;
+        rational weight;
+    };
+
+    void bin_delay_max_resolve(exprs const& _core, rational const& w) {
+        expr_ref_vector core(m, _core.size(), _core.data()), us(m), partial(m);
+        expr_ref fml(m), cls(m);
+        for (expr* c : core) {
+            unfold_record ws;
+            if (!m_unfold.find(c, ws))
+                continue;
+            for (expr* f : ws.ws)
+                new_assumption(f, ws.weight);
+        }
+        if (core.size() <= 1)
+            return;
+        
+        for (expr* core)
+            partial.push_back(nullptr);
+            
+        for (unsigned i = 0; i + 1 < core.size(); ++i) {
+            expr* a = core.get(i);
+            expr* b = core.get(i + 1);
+            expr_ref u = mk_fresh_bool("u");
+            expr_ref v = mk_fresh_bool("v");
+            // u = a or b
+            // v = a and b
+            cls = m.mk_or(a, b);
+            fml = m.mk_implies(u, cls);
+            add(fml);
+            update_model(u, cls);
+            m_defs.push_back(fml);
+            cls = m.mk_and(a, b);
+            fml = m.mk_implies(v, cls);
+            add(fml);
+            update_model(v, cls);
+            m_defs.push_back(fml);
+            us.push_back(u);
+            core.push_back(v);
+
+            unfold_record r;
+            r.ws.push_back(u);
+            if (partial.get(i))
+                r.ws.push_back(partia.get(i));
+            if (partial.get(i + 1))
+                r.ws.push_back(partia.get(i + 1));            
+            partial.push_back(m.mk_and(r.ws));            
+            m_unfold.insert(partial.back(), r);
+        }
+        expr_ref u = mk_and(us);
+        new_assumption(u, w);
+    }
+#endif
+
     // cs is a correction set (a complement of a (maximal) satisfying assignment).
     void cs_max_resolve(exprs const& cs, rational const& w) {
         if (cs.empty()) return;
diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp
index 6cbc8b1b937..bbf11926692 100644
--- a/src/opt/opt_preprocess.cpp
+++ b/src/opt/opt_preprocess.cpp
@@ -20,9 +20,93 @@ Module Name:
 #pragma once
 
 #include "opt/opt_preprocess.h"
+#include "util/max_cliques.h"
 
 namespace opt {
 
+    expr_ref_vector preprocess::propagate(expr* f, lbool& is_sat) {
+        expr_ref_vector asms(m);
+        asms.push_back(f);
+        is_sat = s.check_sat(asms);
+        return s.get_trail(1);
+    }
+
+    bool preprocess::prop_mutexes(vector<soft>& softs, rational& lower) {
+        expr_ref_vector fmls(m);
+        obj_map<expr, rational> new_soft = soft2map(softs, fmls);
+
+        params_ref p;
+        p.set_uint("max_conflicts", 1);
+        s.updt_params(p);
+
+        obj_hashtable<expr> pfmls, nfmls;
+        for (expr* f : fmls)
+            if (m.is_not(f, f))
+                nfmls.insert(f);
+            else
+                pfmls.insert(f);
+        
+        u_map<expr*> ids;
+        unsigned_vector ps;
+        for (expr* f : fmls) {
+            ids.insert(f->get_id(), f);
+            ps.push_back(f->get_id());
+        }
+
+        u_map<uint_set> conns;
+
+        for (expr* f : fmls) {
+            lbool is_sat;
+            expr_ref_vector trail = propagate(f, is_sat);
+            if (is_sat == l_false) {
+                rational w = new_soft[f];
+                lower += w;
+                s.assert_expr(m.mk_not(f));
+                new_soft.remove(f);
+                continue;
+            }
+                
+            expr_ref_vector mux(m);
+            for (expr* g : trail) {
+                if (m.is_not(g, g)) {
+                    if (pfmls.contains(g))
+                        mux.push_back(g);
+                }
+                else if (nfmls.contains(g))
+                    mux.push_back(m.mk_not(g));
+            }
+            uint_set reach;
+            for (expr* g : mux)
+                reach.insert(g->get_id());
+            conns.insert(f->get_id(), reach);
+        }
+        
+        p.set_uint("max_conflicts", UINT_MAX);
+        s.updt_params(p);
+
+        struct neg_literal {
+            unsigned negate(unsigned id) {
+                throw default_exception("unexpected call");
+            }
+        };
+        max_cliques<neg_literal> mc;
+        vector<unsigned_vector> mutexes;
+        mc.cliques(ps, conns, mutexes);
+
+        for (auto& mux : mutexes) {
+            expr_ref_vector _mux(m);
+            for (auto p : mux)
+                _mux.push_back(ids[p]);
+            process_mutex(_mux, new_soft, lower);
+        }
+
+        softs.reset();
+        for (auto const& [k, v] : new_soft)
+            softs.push_back(soft(expr_ref(k, m), v, false));
+        m_trail.reset();
+        return true;        
+    }
+
     obj_map<expr, rational> preprocess::soft2map(vector<soft> const& softs, expr_ref_vector& fmls) {
         obj_map<expr, rational> new_soft;
         for (soft const& sf : softs) {
@@ -104,6 +188,8 @@ namespace opt {
     bool preprocess::operator()(vector<soft>& soft, rational& lower) {
         if (!find_mutexes(soft, lower))
             return false;
+        if (false && !prop_mutexes(soft, lower))
+            return false;
         return true;
     }
 };
diff --git a/src/opt/opt_preprocess.h b/src/opt/opt_preprocess.h
index f5f1c9db6e9..567a750eda2 100644
--- a/src/opt/opt_preprocess.h
+++ b/src/opt/opt_preprocess.h
@@ -28,8 +28,10 @@ namespace opt {
         solver&          s;
         expr_ref_vector  m_trail;
 
+        expr_ref_vector propagate(expr* f, lbool& is_sat);
         obj_map<expr, rational> soft2map(vector<soft> const& softs, expr_ref_vector& fmls);
         bool find_mutexes(vector<soft>& softs, rational& lower);
+        bool prop_mutexes(vector<soft>& softs, rational& lower);
         void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);
 
     public:
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index b54e92a704c..657e222dadf 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -612,7 +612,7 @@ namespace smt {
             }
         }
         vector<unsigned_vector> _mutexes;
-        mc.cliques(ps, _mutexes);
+        mc.cliques2(ps, _mutexes);
         for (auto const& mux : _mutexes) {
             expr_ref_vector lits(m);
             for (unsigned idx : mux) {
diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h
index 4dd91b366d9..979a5b79595 100644
--- a/src/util/max_cliques.h
+++ b/src/util/max_cliques.h
@@ -83,6 +83,29 @@ class max_cliques : public T {
         m_next.reserve(max);
         m_tc.reserve(m_next.size());
     }
+
+    struct compare_degree {
+        u_map<uint_set>& conns;
+        compare_degree(u_map<uint_set>& conns): conns(conns) {}
+        bool operator()(unsigned x, unsigned y) const {
+            return conns[x].num_elems() < conns[y].num_elems();
+        }
+    };
+
+
+    void init(unsigned_vector const& ps, u_map<uint_set>& conns) {
+
+        uint_set vars;
+        
+        for (unsigned p : ps) 
+            vars.insert(p);
+        
+        for (unsigned v : ps) {
+            uint_set reach;
+            get_reachable(v, vars, reach);
+            conns.insert(v, reach);
+        }
+    }
     
 public:
     void add_edge(unsigned src, unsigned dst) {
@@ -92,7 +115,7 @@ class max_cliques : public T {
         m_next[dst].push_back(src);
     }
 
-    void cliques(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {     
+    void cliques1(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {     
         init(ps);
         unsigned_vector clique;
         uint_set vars;
@@ -124,35 +147,29 @@ class max_cliques : public T {
         }        
     }
 
-
     // better quality cliques
-    void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {     
-
-        uint_set all_vars, todo;
+    void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cs) {     
         u_map<uint_set> conns;
-
         init(ps);
+        // compute connections using TC of implication graph
+        init(ps, conns);
+        cliques(ps, conns, cs);
+    }
 
-        struct compare_degree {
-            u_map<uint_set>& conns;
-            compare_degree(u_map<uint_set>& conns): conns(conns) {}
-            bool operator()(unsigned x, unsigned y) const {
-                return conns[x].num_elems() < conns[y].num_elems();
-            }
-        };
+    // cliques after connections are computed.
+    void cliques(unsigned_vector const& ps, u_map<uint_set>& conns, vector<unsigned_vector>& cliques) {
+
+        unsigned maxp = 1;
+        for (unsigned p : ps)
+            maxp = std::max(p, maxp);
+        
+        uint_set todo;
         compare_degree lt(conns);
-        heap<compare_degree> heap(m_next.size(), lt);
+        heap<compare_degree> heap(maxp + 1, lt);
 
-        for (unsigned p : ps) {
-            all_vars.insert(p);
+        for (unsigned p : ps) {           
             todo.insert(p);
-        }
-
-        for (unsigned v : ps) {
-            uint_set reach;
-            get_reachable(v, all_vars, reach);
-            conns.insert(v, reach);
-            heap.insert(v);
+            heap.insert(p);
         }
 
         while (!todo.empty()) {