diff --git a/clasp/cli/clasp_cli_options.inl b/clasp/cli/clasp_cli_options.inl
index 3c5e2a7..eac162a 100644
--- a/clasp/cli/clasp_cli_options.inl
+++ b/clasp/cli/clasp_cli_options.inl
@@ -104,9 +104,9 @@ OPTION(share, "!,@1", ARG_EXT(defaultsTo("auto")->state(Value::value_defaulted),
        "      %A: {auto|problem|learnt|all}", FUN(arg) {ContextParams::ShareMode x; return arg>>x && SET(SELF.shareMode, (uint32)x);}, GET((ContextParams::ShareMode)SELF.shareMode))
 OPTION(learn_explicit, ",@2" , ARG(flag()), "Do not use Short Implication Graph for learning", STORE_FLAG(SELF.shortMode), GET(SELF.shortMode))
 OPTION(short_simp_mode, ",@2" , ARG_EXT(arg("<mode>")->defaultsTo("no")->state(Value::value_defaulted), DEFINE_ENUM_MAPPING(ContextParams::ShortSimpMode, \
-       MAP("no"  , ContextParams::simp_no)  , MAP("learnt", ContextParams::simp_learnt))),\
+       MAP("no"  , ContextParams::simp_no), MAP("learnt", ContextParams::simp_learnt), MAP("all", ContextParams::simp_all))),\
        "Remove duplicate short constraints [%D]\n"\
-       "      %A: {no|learnt}", FUN(arg) {ContextParams::ShortSimpMode x; return arg>>x && SET(SELF.shortSimp, (uint32)x);}\
+       "      %A: {no|learnt|all}", FUN(arg) {ContextParams::ShortSimpMode x; return arg>>x && SET(SELF.shortSimp, (uint32)x);}\
        , GET((ContextParams::ShortSimpMode)SELF.shortSimp))\
 OPTION(sat_prepro    , "!,@1", ARG(arg("<arg>")->implicit("2")),                     \
        "Run SatELite-like preprocessing (Implicit: %I)\n"                            \
diff --git a/clasp/shared_context.h b/clasp/shared_context.h
index 9060a7c..a4c1a4d 100644
--- a/clasp/shared_context.h
+++ b/clasp/shared_context.h
@@ -326,6 +326,11 @@ class ShortImplicationsGraph {
      * \return true iff a new implication was added.
      */
     bool add(LitView lits, bool learnt);
+    //! Removes the given constraint from the implication graph.
+    /*!
+     * \pre The object is currently not shared.
+     */
+    void remove(LitView lits, bool learnt);
 
     //! Removes p and its implications.
     /*!
@@ -972,6 +977,7 @@ class SharedContext {
     [[nodiscard]] MinPtr       minimizeNoCreate() const;
     //@}
 private:
+    bool    preprocessShort();
     bool    unfreezeStep();
     Literal addStepLit();
     using VarVec = PodVector_t<VarInfo>;
diff --git a/clasp/solver_strategies.h b/clasp/solver_strategies.h
index ae390ac..76310ce 100644
--- a/clasp/solver_strategies.h
+++ b/clasp/solver_strategies.h
@@ -581,6 +581,7 @@ struct ContextParams {
     enum ShortSimpMode {
         simp_no     = 0, /*!< No additional simplifications. */
         simp_learnt = 1, /*!< Drop duplicate learnt short clauses. */
+        simp_all    = 2, /*!< Drop all duplicate short clauses. */
     };
     //! How to handle physical sharing of (explicit) constraints.
     enum ShareMode {
diff --git a/src/shared_context.cpp b/src/shared_context.cpp
index d61d503..27b60e9 100644
--- a/src/shared_context.cpp
+++ b/src/shared_context.cpp
@@ -206,7 +206,7 @@ bool ShortImplicationsGraph::add(LitView lits, bool learnt) {
     Literal p = lits[0], q = lits[1], r = (tern ? lits[2] : lit_false);
     p.unflag(), q.unflag(), r.unflag();
     if (not shared_) {
-        bool simp = learnt && simp_ == ContextParams::simp_learnt;
+        bool simp = simp_ == ContextParams::simp_all || (learnt && simp_ == ContextParams::simp_learnt);
         if (simp && contains(getList(~p).left_view(), q)) {
             return true;
         }
@@ -241,6 +241,31 @@ bool ShortImplicationsGraph::add(LitView lits, bool learnt) {
 #endif
     return false;
 }
+void ShortImplicationsGraph::remove(LitView lits, bool learnt) {
+    assert(not shared_);
+    bool     tern  = lits.size() == 3u;
+    uint32&  stats = (tern ? tern_ : bin_)[learnt];
+    unsigned i = 0, rem = 0;
+    for (auto x : lits) {
+        auto& w  = getList(~x);
+        auto  sz = w.left_size() + w.right_size();
+        if (not tern) {
+            w.erase_left_unordered(std::find(w.left_begin(), w.left_end(), lits[1 - i]));
+        }
+        else {
+            Tern t = {lits[(i + 1) % 3], lits[(i + 2) % 3]};
+            w.erase_right_unordered(std::find_if(w.right_begin(), w.right_end(), [&t](const Tern& e) {
+                return contains(t, e[0]) && contains(t, e[1]);
+            }));
+        }
+        rem += sz != (w.left_size() + w.right_size());
+        w.try_shrink();
+        ++i;
+    }
+    if (rem) {
+        --stats;
+    }
+}
 
 void ShortImplicationsGraph::removeBin(Literal other, Literal sat) {
     --bin_[other.flagged()];
@@ -1022,8 +1047,11 @@ bool SharedContext::endInit(bool attachAll) {
     initStats(*master());
     heuristic.simplify();
     SatPrePtr temp = std::move(satPrepro);
-    bool      ok   = not master()->hasConflict() && master()->preparePost() && (not temp || temp->preprocess(*this)) &&
-              master()->endInit();
+    bool      ok   = not master()->hasConflict() && master()->preparePost() && (not temp || temp->preprocess(*this));
+    if (ok && not temp && btig_.simpMode() == ContextParams::simp_all) {
+        ok = preprocessShort();
+    }
+    ok                         = ok && master()->endInit();
     satPrepro                  = std::move(temp);
     master()->dbIdx_           = sizeVec(master()->constraints_);
     lastTopLevel_              = master()->assign_.front;
@@ -1206,6 +1234,90 @@ uint32 SharedContext::problemComplexity() const {
     }
     return numConstraints();
 }
+bool SharedContext::preprocessShort() {
+    auto&  s      = *master();
+    auto&  assign = s.assign_;
+    LitVec lits;
+    LitVec tern;
+    for (Var v = 1; v < assign.numVars() && not s.hasConflict(); ++v) {
+        if (assign.value(v) != value_free) {
+            continue;
+        }
+        for (Literal lit : {posLit(v), negLit(v)}) {
+            if (marked(lit)) {
+                continue;
+            }
+            tern.clear();
+            bool ok     = true;
+            auto qFront = assign.assigned();
+            assign.assign(lit, 0, lit_true);
+            do {
+                ok = btig_.forEach(assign.trail[qFront++], [&](Literal p, Literal q, Literal r = lit_false) {
+                    if (r == lit_false) {
+                        return assign.assign(q, 0, p);
+                    }
+                    auto vq   = assign.value(q.var());
+                    auto vr   = assign.value(r.var());
+                    auto ante = Antecedent(p);
+                    if (vr == trueValue(r) || vq == trueValue(q)) {
+                        if (assign.reason(r.var()).asUint() == ante.asUint() ||
+                            assign.reason(q.var()).asUint() == ante.asUint()) {
+                            tern.push_back(~p);
+                            tern.push_back(q);
+                            tern.push_back(r);
+                        }
+                        return true;
+                    }
+                    if (vr == vq) {
+                        return vr == value_free;
+                    }
+                    if (vq) {
+                        if (assign.reason(q.var()).asUint() == ante.asUint()) {
+                            tern.push_back(q.flag());
+                            tern.push_back(~p);
+                            tern.push_back(r);
+                        }
+                        return assign.assign(r, 0, Antecedent(p, ~q));
+                    }
+                    if (assign.reason(r.var()).asUint() == ante.asUint()) {
+                        tern.push_back(r.flag());
+                        tern.push_back(~p);
+                        tern.push_back(q);
+                    }
+                    return assign.assign(q, 0, Antecedent(p, ~r));
+                });
+            } while (ok && qFront < assign.assigned());
+            if (ok) {
+                for (auto i = 0u; i < sizeVec(tern); i += 3) {
+                    bool sat    = not tern[i].flagged();
+                    bool learnt = tern[i + 1].flagged() || tern[i + 2].flagged();
+                    tern[i].unflag();
+                    btig_.remove(std::span(tern.data() + i, 3), learnt);
+                    if (not sat) {
+                        btig_.add(std::span(tern.data() + i + 1, 2), learnt);
+                    }
+                }
+            }
+            while (assign.trail.back() != lit) {
+                if (not marked(assign.trail.back())) {
+                    mark(assign.trail.back());
+                    lits.push_back(assign.trail.back());
+                }
+                assign.undoLast();
+            }
+            assign.undoLast();
+            if (not ok) {
+                master()->force(~lit) && master()->propagate();
+                break;
+            }
+        }
+    }
+    while (not lits.empty()) {
+        unmark(lits.back().var());
+        lits.pop_back();
+    }
+    return master()->simplify();
+}
 /////////////////////////////////////////////////////////////////////////////////////////
 // Distributor
 /////////////////////////////////////////////////////////////////////////////////////////
diff --git a/tests/cli_test.cpp b/tests/cli_test.cpp
index db7f5b4..f6c9e36 100644
--- a/tests/cli_test.cpp
+++ b/tests/cli_test.cpp
@@ -458,7 +458,8 @@ TEST_CASE("Cli options", "[cli]") {
         REQUIRE(config.getValue(key, val) == 2);
         REQUIRE(val == "no");
 
-        for (auto [x, y] : {std::pair{ContextParams::simp_learnt, "learnt"}, std::pair{ContextParams::simp_no, "no"}}) {
+        for (auto [x, y] : {std::pair{ContextParams::simp_learnt, "learnt"}, std::pair{ContextParams::simp_all, "all"},
+                            std::pair{ContextParams::simp_no, "no"}}) {
             CAPTURE(y);
             REQUIRE(1 == config.setValue(key, y));
             REQUIRE(config.shortSimp == x);