diff --git a/ortools/base/stringprintf.cc b/ortools/base/stringprintf.cc
index 3c3ae00306..0277d533c9 100644
--- a/ortools/base/stringprintf.cc
+++ b/ortools/base/stringprintf.cc
@@ -106,4 +106,16 @@ void StringAppendF(std::string* const dst, const char* const format, ...) {
   StringAppendV(dst, format, ap);
   va_end(ap);
 }
+
 }  // namespace operations_research
+
+namespace absl {
+std::string StrFormat(const char* const format, ...) {
+  va_list ap;
+  va_start(ap, format);
+  std::string result;
+  ::operations_research::StringAppendV(&result, format, ap);
+  va_end(ap);
+  return result;
+}
+}  // namespace absl
diff --git a/ortools/base/stringprintf.h b/ortools/base/stringprintf.h
index 8b01f3888c..2430f79378 100644
--- a/ortools/base/stringprintf.h
+++ b/ortools/base/stringprintf.h
@@ -21,4 +21,8 @@ std::string StringPrintf(const char* const format, ...);
 void SStringPrintf(std::string* const dst, const char* const format, ...);
 void StringAppendF(std::string* const dst, const char* const format, ...);
 }  // namespace operations_research
+
+namespace absl {
+std::string StrFormat(const char* const format, ...);
+}  // namespace absl
 #endif  // OR_TOOLS_BASE_STRINGPRINTF_H_
diff --git a/ortools/bop/bop_ls.cc b/ortools/bop/bop_ls.cc
index af695e7103..a06b66ab33 100644
--- a/ortools/bop/bop_ls.cc
+++ b/ortools/bop/bop_ls.cc
@@ -13,6 +13,7 @@
 
 #include "ortools/bop/bop_ls.h"
 
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/stringprintf.h"
 #include "ortools/bop/bop_util.h"
 #include "ortools/sat/boolean_problem.h"
@@ -384,10 +385,11 @@ std::string AssignmentAndConstraintFeasibilityMaintainer::DebugString() const {
   str += "\nmin  curr  max\n";
   for (ConstraintIndex ct(0); ct < constraint_values_.size(); ++ct) {
     if (constraint_lower_bounds_[ct] == kint64min) {
-      str += StringPrintf("-  %lld  %lld\n", constraint_values_[ct],
-                          constraint_upper_bounds_[ct]);
+      str += absl::StrFormat("-  %d  %d\n", constraint_values_[ct],
+                             constraint_upper_bounds_[ct]);
     } else {
-      str += StringPrintf("%lld  %lld  %lld\n", constraint_lower_bounds_[ct],
+      str +=
+          absl::StrFormat("%d  %d  %d\n", constraint_lower_bounds_[ct],
                           constraint_values_[ct], constraint_upper_bounds_[ct]);
     }
   }
diff --git a/ortools/bop/bop_portfolio.cc b/ortools/bop/bop_portfolio.cc
index a71fc11205..3c0b447f58 100644
--- a/ortools/bop/bop_portfolio.cc
+++ b/ortools/bop/bop_portfolio.cc
@@ -13,6 +13,7 @@
 
 #include "ortools/bop/bop_portfolio.h"
 
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/bop/bop_fs.h"
@@ -411,10 +412,10 @@ void OptimizerSelector::SetOptimizerRunnability(OptimizerIndex optimizer_index,
 
 std::string OptimizerSelector::PrintStats(OptimizerIndex optimizer_index) const {
   const RunInfo& info = run_infos_[info_positions_[optimizer_index]];
-  return StringPrintf(
-      "    %40s : %3d/%-3d  (%6.2f%%)  Total gain: %6lld  Total Dtime: %0.3f "
+  return absl::StrFormat(
+      "    %40s : %3d/%-3d  (%6.2f%%)  Total gain: %6d  Total Dtime: %0.3f "
       "score: %f\n",
-      info.name.c_str(), info.num_successes, info.num_calls,
+      info.name, info.num_successes, info.num_calls,
       100.0 * info.num_successes / info.num_calls, info.total_gain,
       info.time_spent, info.score);
 }
diff --git a/ortools/bop/integral_solver.cc b/ortools/bop/integral_solver.cc
index 23cb5e3938..8b2d4e44df 100644
--- a/ortools/bop/integral_solver.cc
+++ b/ortools/bop/integral_solver.cc
@@ -289,9 +289,9 @@ std::string IntegralVariable::DebugString() const {
   std::string str;
   CHECK_EQ(bits_.size(), weights_.size());
   for (int i = 0; i < bits_.size(); ++i) {
-    str += StringPrintf("%lld [%d] ", weights_[i], bits_[i].value());
+    str += absl::StrFormat("%lld [%lld] ", weights_[i], bits_[i].value());
   }
-  str += StringPrintf(" Offset: %lld", offset_);
+  str += absl::StrFormat(" Offset: %lld", offset_);
   return str;
 }
 
diff --git a/ortools/flatzinc/flatzinc_constraints.cc b/ortools/flatzinc/flatzinc_constraints.cc
index 8e7545dea3..3030c0372d 100644
--- a/ortools/flatzinc/flatzinc_constraints.cc
+++ b/ortools/flatzinc/flatzinc_constraints.cc
@@ -17,6 +17,7 @@
 
 #include "ortools/base/commandlineflags.h"
 #include "ortools/base/stringprintf.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/constraint_solver/constraint_solveri.h"
 #include "ortools/flatzinc/logging.h"
 #include "ortools/util/string_array.h"
@@ -153,9 +154,8 @@ class FixedModulo : public Constraint {
   }
 
   std::string DebugString() const override {
-    return StringPrintf("(%s %% %s == %" GG_LL_FORMAT "d)",
-                        var_->DebugString().c_str(),
-                        mod_->DebugString().c_str(), residual_);
+    return absl::StrFormat("(%s %% %s == %" GG_LL_FORMAT "d)",
+                           var_->DebugString(), mod_->DebugString(), residual_);
   }
 
  private:
@@ -305,10 +305,10 @@ class IsBooleanSumInRange : public Constraint {
   }
 
   std::string DebugString() const override {
-    return StringPrintf("Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT
-                        "d] == %s",
-                        JoinDebugStringPtr(vars_, ", ").c_str(), range_min_,
-                        range_max_, target_->DebugString().c_str());
+    return absl::StrFormat("Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT
+                           "d] == %s",
+                           JoinDebugStringPtr(vars_, ", "), range_min_,
+                           range_max_, target_->DebugString());
   }
 
   void Accept(ModelVisitor* const visitor) const override {
@@ -424,9 +424,9 @@ class BooleanSumInRange : public Constraint {
   }
 
   std::string DebugString() const override {
-    return StringPrintf("Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d]",
-                        JoinDebugStringPtr(vars_, ", ").c_str(), range_min_,
-                        range_max_);
+    return absl::StrFormat(
+        "Sum([%s]) in [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d]",
+        JoinDebugStringPtr(vars_, ", "), range_min_, range_max_);
   }
 
   void Accept(ModelVisitor* const visitor) const override {
diff --git a/ortools/flatzinc/model.cc b/ortools/flatzinc/model.cc
index 17a634f860..9f510d76ed 100644
--- a/ortools/flatzinc/model.cc
+++ b/ortools/flatzinc/model.cc
@@ -20,6 +20,7 @@
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
 #include "ortools/base/join.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
 #include "ortools/base/map_util.h"
 #include "ortools/base/stl_util.h"
@@ -373,8 +374,8 @@ std::string Domain::DebugString() const {
     if (values.empty()) {
       return "int";
     } else {
-      return StringPrintf("[%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d]", values[0],
-                          values[1]);
+      return absl::StrFormat("[%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d]",
+                             values[0], values[1]);
     }
   } else if (values.size() == 1) {
     return StrCat(values.back());
@@ -449,10 +450,10 @@ Argument Argument::FromDomain(const Domain& domain) {
 std::string Argument::DebugString() const {
   switch (type) {
     case INT_VALUE:
-      return StringPrintf("% " GG_LL_FORMAT "d", values[0]);
+      return absl::StrFormat("% " GG_LL_FORMAT "d", values[0]);
     case INT_INTERVAL:
-      return StringPrintf("[%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d]", values[0],
-                          values[1]);
+      return absl::StrFormat("[%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d]",
+                             values[0], values[1]);
     case INT_LIST:
       return StringPrintf("[%s]", absl::StrJoin(values, ", ").c_str());
     case DOMAIN_LIST:
@@ -620,7 +621,7 @@ bool IntegerVariable::Merge(const std::string& other_name,
 
 std::string IntegerVariable::DebugString() const {
   if (!domain.is_interval && domain.values.size() == 1) {
-    return StringPrintf("% " GG_LL_FORMAT "d", domain.values.back());
+    return absl::StrFormat("% " GG_LL_FORMAT "d", domain.values.back());
   } else {
     return StringPrintf(
         "%s(%s%s%s)%s", name.c_str(), domain.DebugString().c_str(),
@@ -788,8 +789,8 @@ std::string Annotation::DebugString() const {
                           JoinDebugString(annotations, ", ").c_str());
     }
     case INTERVAL: {
-      return StringPrintf("%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d",
-                          interval_min, interval_max);
+      return absl::StrFormat("%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d",
+                             interval_min, interval_max);
     }
     case INT_VALUE: {
       return StrCat(interval_min);
@@ -816,8 +817,8 @@ std::string Annotation::DebugString() const {
 // ----- SolutionOutputSpecs -----
 
 std::string SolutionOutputSpecs::Bounds::DebugString() const {
-  return StringPrintf("%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d", min_value,
-                      max_value);
+  return absl::StrFormat("%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d", min_value,
+                         max_value);
 }
 
 SolutionOutputSpecs SolutionOutputSpecs::SingleVariable(
diff --git a/ortools/flatzinc/presolve.cc b/ortools/flatzinc/presolve.cc
index 054d93f04c..1a5d562edd 100644
--- a/ortools/flatzinc/presolve.cc
+++ b/ortools/flatzinc/presolve.cc
@@ -20,6 +20,7 @@
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
 #include "ortools/base/stringpiece_utils.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/string_view.h"
 #include "ortools/base/stringpiece_utils.h"
 #include "ortools/base/strutil.h"
@@ -1251,9 +1252,11 @@ Presolver::RuleStatus Presolver::PresolveArrayIntElement(Constraint* ct,
 
       if (last_index < ct->arguments[0].Var()->domain.Max() ||
           first_index > ct->arguments[0].Var()->domain.Min()) {
-        StringAppendF(log, "filter index to [%" GG_LL_FORMAT "d..%" GG_LL_FORMAT
-                           "d] and reduce array to size %" GG_LL_FORMAT "d",
-                      first_index, last_index, last_index);
+        StringAppendF(log,
+                              "filter index to [%" GG_LL_FORMAT
+                              "d..%" GG_LL_FORMAT
+                              "d] and reduce array to size %" GG_LL_FORMAT "d",
+                              first_index, last_index, last_index);
         IntersectVarWithInterval(ct->arguments[0].Var(), first_index,
                                  last_index);
         ct->arguments[1].values.resize(last_index);
@@ -1537,8 +1540,9 @@ Presolver::RuleStatus Presolver::PropagatePositiveLinear(Constraint* ct,
         IntegerVariable* const var = ct->arguments[1].variables[i];
         const int64 bound = rhs / coef;
         if (bound < var->domain.Max()) {
-          StringAppendF(log, ", intersect %s with [0..%" GG_LL_FORMAT "d]",
-                        var->DebugString().c_str(), bound);
+          StringAppendF(log,
+                                ", intersect %s with [0..%" GG_LL_FORMAT "d]",
+                                var->DebugString(), bound);
           IntersectVarWithInterval(var, 0, bound);
         }
       }
@@ -1550,8 +1554,9 @@ Presolver::RuleStatus Presolver::PropagatePositiveLinear(Constraint* ct,
     IntegerVariable* const var = ct->arguments[1].variables[0];
     const int64 bound = (rhs + coef - 1) / coef;
     if (bound > var->domain.Min()) {
-      StringAppendF(log, ", intersect %s with [%" GG_LL_FORMAT "d .. INT_MAX]",
-                    var->DebugString().c_str(), bound);
+      StringAppendF(
+          log, ", intersect %s with [%" GG_LL_FORMAT "d .. INT_MAX]",
+          var->DebugString(), bound);
       IntersectVarWithInterval(var, bound, kint64max);
       return CONSTRAINT_ALWAYS_TRUE;
     }
diff --git a/ortools/flatzinc/reporting.cc b/ortools/flatzinc/reporting.cc
index 49ad1d9e3b..990d54d463 100644
--- a/ortools/flatzinc/reporting.cc
+++ b/ortools/flatzinc/reporting.cc
@@ -19,6 +19,7 @@
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/constraint_solver/constraint_solver.h"
 #include "ortools/constraint_solver/constraint_solveri.h"
 #include "ortools/flatzinc/logging.h"
@@ -131,8 +132,8 @@ class MtOptimizeVar : public OptimizeVar {
       if (verbose_) {
         report_->Log(
             thread_id_,
-            StringPrintf("Polling improved objective %" GG_LL_FORMAT "d",
-                         polled_best));
+            absl::StrFormat("Polling improved objective %" GG_LL_FORMAT "d",
+                            polled_best));
       }
       best_ = polled_best;
     }
@@ -236,8 +237,8 @@ void MultiThreadReporting::OnOptimizeSolution(int thread_id, int64 value,
           if (verbose_) {
             LogNoLock(
                 thread_id,
-                StringPrintf("solution found with value %" GG_LL_FORMAT "d",
-                             value));
+                absl::StrFormat("solution found with value %" GG_LL_FORMAT "d",
+                                value));
           }
           if (ShouldPrintAllSolutions() || MaxNumSolutions() > 1) {
             Print(thread_id, solution_string);
@@ -255,8 +256,8 @@ void MultiThreadReporting::OnOptimizeSolution(int thread_id, int64 value,
           if (verbose_) {
             LogNoLock(
                 thread_id,
-                StringPrintf("solution found with value %" GG_LL_FORMAT "d",
-                             value));
+                absl::StrFormat("solution found with value %" GG_LL_FORMAT "d",
+                                value));
           }
           if (ShouldPrintAllSolutions() || MaxNumSolutions() > 1) {
             Print(thread_id, solution_string);
@@ -294,8 +295,8 @@ void MultiThreadReporting::OnSearchEnd(int thread_id, bool interrupted) {
   if (!last_solution_.empty()) {
     if (verbose_) {
       LogNoLock(last_thread_,
-                StringPrintf("solution found with value %" GG_LL_FORMAT "d",
-                             best_objective_));
+                absl::StrFormat("solution found with value %" GG_LL_FORMAT "d",
+                                best_objective_));
     }
     Print(thread_id, last_solution_);
     last_solution_.clear();
diff --git a/ortools/flatzinc/solver.cc b/ortools/flatzinc/solver.cc
index 41ac414327..8ca4a7afb4 100644
--- a/ortools/flatzinc/solver.cc
+++ b/ortools/flatzinc/solver.cc
@@ -20,6 +20,7 @@
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/map_util.h"
 #include "ortools/base/hash.h"
 #include "ortools/constraint_solver/constraint_solver.h"
@@ -96,8 +97,7 @@ std::string Solver::SolutionString(const SolutionOutputSpecs& output) const {
       return StringPrintf("%s = %s;", output.name.c_str(),
                           value == 1 ? "true" : "false");
     } else {
-      return StringPrintf("%s = %" GG_LL_FORMAT "d;", output.name.c_str(),
-                          value);
+      return absl::StrFormat("%s = %" GG_LL_FORMAT "d;", output.name, value);
     }
   } else {
     const int bound_size = output.bounds.size();
@@ -105,9 +105,9 @@ std::string Solver::SolutionString(const SolutionOutputSpecs& output) const {
         StringPrintf("%s = array%dd(", output.name.c_str(), bound_size);
     for (int i = 0; i < bound_size; ++i) {
       if (output.bounds[i].max_value != 0) {
-        result.append(StringPrintf("%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d, ",
-                                   output.bounds[i].min_value,
-                                   output.bounds[i].max_value));
+        result.append(absl::StrFormat(
+            "%" GG_LL_FORMAT "d..%" GG_LL_FORMAT "d, ",
+            output.bounds[i].min_value, output.bounds[i].max_value));
       } else {
         result.append("{},");
       }
@@ -859,40 +859,40 @@ void Solver::Solve(FlatzincParameters p, SearchReportingInterface* report) {
       proven = true;
     }
     solver_status.append(
-        StringPrintf("%%%%  total runtime:        %" GG_LL_FORMAT "d ms\n",
-                     solve_time + build_time));
-    solver_status.append(StringPrintf(
+        absl::StrFormat("%%%%  total runtime:        %" GG_LL_FORMAT "d ms\n",
+                        solve_time + build_time));
+    solver_status.append(absl::StrFormat(
         "%%%%  build time:           %" GG_LL_FORMAT "d ms\n", build_time));
-    solver_status.append(StringPrintf(
+    solver_status.append(absl::StrFormat(
         "%%%%  solve time:           %" GG_LL_FORMAT "d ms\n", solve_time));
     solver_status.append(
         StringPrintf("%%%%  solutions:            %d\n", num_solutions));
     solver_status.append(StringPrintf("%%%%  constraints:          %d\n",
                                       solver_->constraints()));
-    solver_status.append(StringPrintf(
+    solver_status.append(absl::StrFormat(
         "%%%%  normal propagations:  %" GG_LL_FORMAT "d\n",
         solver_->demon_runs(operations_research::Solver::NORMAL_PRIORITY)));
-    solver_status.append(StringPrintf(
+    solver_status.append(absl::StrFormat(
         "%%%%  delayed propagations: %" GG_LL_FORMAT "d\n",
         solver_->demon_runs(operations_research::Solver::DELAYED_PRIORITY)));
     solver_status.append(
-        StringPrintf("%%%%  branches:             %" GG_LL_FORMAT "d\n",
-                     solver_->branches()));
+        absl::StrFormat("%%%%  branches:             %" GG_LL_FORMAT "d\n",
+                        solver_->branches()));
     solver_status.append(
-        StringPrintf("%%%%  failures:             %" GG_LL_FORMAT "d\n",
-                     solver_->failures()));
+        absl::StrFormat("%%%%  failures:             %" GG_LL_FORMAT "d\n",
+                        solver_->failures()));
     solver_status.append(StringPrintf("%%%%  memory:               %s\n",
                                       MemoryUsage().c_str()));
     const int64 best = report->BestSolution();
     if (model_.objective() != nullptr) {
       if (!model_.maximize() && num_solutions > 0) {
-        solver_status.append(
-            StringPrintf("%%%%  min objective:        %" GG_LL_FORMAT "d%s\n",
-                         best, (proven ? " (proven)" : "")));
+        solver_status.append(absl::StrFormat(
+            "%%%%  min objective:        %" GG_LL_FORMAT "d%s\n", best,
+            (proven ? " (proven)" : "")));
       } else if (num_solutions > 0) {
-        solver_status.append(
-            StringPrintf("%%%%  max objective:        %" GG_LL_FORMAT "d%s\n",
-                         best, (proven ? " (proven)" : "")));
+        solver_status.append(absl::StrFormat(
+            "%%%%  max objective:        %" GG_LL_FORMAT "d%s\n", best,
+            (proven ? " (proven)" : "")));
       }
     }
 
@@ -916,16 +916,16 @@ void Solver::Solve(FlatzincParameters p, SearchReportingInterface* report) {
     solver_status.append(
         "%%  name, status, obj, solns, s_time, b_time, br, "
         "fails, cts, demon, delayed, mem, search\n");
-    solver_status.append(StringPrintf(
+    solver_status.append(absl::StrFormat(
         "%%%%  csv: %s, %s, %s, %d, %" GG_LL_FORMAT "d ms, %" GG_LL_FORMAT
         "d ms, %" GG_LL_FORMAT "d, %" GG_LL_FORMAT "d, %d, %" GG_LL_FORMAT
         "d, %" GG_LL_FORMAT "d, %s, %s",
-        model_.name().c_str(), status_string.c_str(), obj_string.c_str(),
-        num_solutions, solve_time, build_time, solver_->branches(),
-        solver_->failures(), solver_->constraints(),
+        model_.name(), status_string, obj_string, num_solutions, solve_time,
+        build_time, solver_->branches(), solver_->failures(),
+        solver_->constraints(),
         solver_->demon_runs(operations_research::Solver::NORMAL_PRIORITY),
         solver_->demon_runs(operations_research::Solver::DELAYED_PRIORITY),
-        MemoryUsage().c_str(), search_name_.c_str()));
+        MemoryUsage(), search_name_));
     report->Print(p.thread_id, search_status);
     if (p.statistics) {
       report->Print(p.thread_id, solver_status);
diff --git a/ortools/glop/revised_simplex.cc b/ortools/glop/revised_simplex.cc
index 984bf9781c..a22eabf046 100644
--- a/ortools/glop/revised_simplex.cc
+++ b/ortools/glop/revised_simplex.cc
@@ -27,6 +27,7 @@
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/glop/initial_basis.h"
 #include "ortools/glop/parameters.pb.h"
 #include "ortools/lp_data/lp_data.h"
@@ -439,7 +440,7 @@ const BasisFactorization& RevisedSimplex::GetBasisFactorization() const {
 }
 
 std::string RevisedSimplex::GetPrettySolverStats() const {
-  return StringPrintf(
+  return absl::StrFormat(
       "Problem status                               : %s\n"
       "Solving time                                 : %-6.4g\n"
       "Number of iterations                         : %llu\n"
diff --git a/ortools/graph/io.h b/ortools/graph/io.h
index efe582e617..fe9a473007 100644
--- a/ortools/graph/io.h
+++ b/ortools/graph/io.h
@@ -27,6 +27,7 @@
 #include "ortools/base/numbers.h"
 #include "ortools/base/split.h"
 #include "ortools/base/join.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
 #include "ortools/graph/graph.h"
 #include "ortools/base/status.h"
diff --git a/ortools/linear_solver/linear_solver.cc b/ortools/linear_solver/linear_solver.cc
index f1441861b9..fea05cde07 100644
--- a/ortools/linear_solver/linear_solver.cc
+++ b/ortools/linear_solver/linear_solver.cc
@@ -39,6 +39,7 @@
 #include "ortools/base/hash.h"
 #include "ortools/base/accurate_sum.h"
 #include "ortools/linear_solver/linear_solver.pb.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/linear_solver/model_exporter.h"
 #include "ortools/linear_solver/model_validator.h"
 #include "ortools/util/fp_utils.h"
@@ -311,6 +312,10 @@ bool MPSolver::SetSolverSpecificParametersAsString(const std::string& parameters
   return interface_->SetSolverSpecificParametersAsString(parameters);
 }
 
+void MPSolver::SetHint(const PartialVariableAssignment& hint) {
+  interface_->SetHint(hint);
+}
+
 // ----- Solver -----
 
 #if defined(USE_CLP) || defined(USE_CBC)
@@ -1025,9 +1030,9 @@ std::string PrettyPrintVar(const MPVariable& var) {
     if (lb > ub) {
       return prefix + "∅";
     } else if (lb == ub) {
-      return StringPrintf("%s{ %lld }", prefix.c_str(), lb);
+      return absl::StrFormat("%s{ %lld }", prefix.c_str(), lb);
     } else {
-      return StringPrintf("%s{ %lld, %lld }", prefix.c_str(), lb, ub);
+      return absl::StrFormat("%s{ %lld, %lld }", prefix.c_str(), lb, ub);
     }
   }
   // Special case: single (non-infinite) real value.
@@ -1672,4 +1677,3 @@ int MPSolverParameters::GetIntegerParam(MPSolverParameters::IntegerParam param)
 
 
 }  // namespace operations_research
-
diff --git a/ortools/linear_solver/linear_solver.h b/ortools/linear_solver/linear_solver.h
index 23fcc4ba94..1fd7d2be1b 100644
--- a/ortools/linear_solver/linear_solver.h
+++ b/ortools/linear_solver/linear_solver.h
@@ -464,6 +464,11 @@ class MPSolver {
     return solver_specific_parameter_string_;
   }
 
+  // Advanced usage: starting hint. This instructs the solver to first pin some
+  // variables to particular values and use that to quickly get an upper bound
+  // on the solution quality. Currently, only GLIP supports this.
+  void SetHint(const PartialVariableAssignment& hint);
+
   // Advanced usage: possible basis status values for a variable and the
   // slack variable of a linear constraint.
   enum BasisStatus {
@@ -1289,6 +1294,10 @@ class MPSolverInterface {
     LOG(FATAL) << "Not supported by this solver.";
   }
 
+  virtual void SetHint(const PartialVariableAssignment& hint) {
+    LOG(FATAL) << "Not supported by this solver.";
+  }
+
   virtual bool InterruptSolve() { return false; }
 
   friend class MPSolver;
diff --git a/ortools/lp_data/lp_data.cc b/ortools/lp_data/lp_data.cc
index 1be4c1ce3c..b654b0cd14 100644
--- a/ortools/lp_data/lp_data.cc
+++ b/ortools/lp_data/lp_data.cc
@@ -24,6 +24,7 @@
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/join.h"
 #include "ortools/base/join.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/lp_data/lp_print_utils.h"
 #include "ortools/lp_data/lp_utils.h"
 #include "ortools/lp_data/matrix_utils.h"
@@ -416,7 +417,7 @@ Fractional LinearProgram::GetObjectiveCoefficientForMinimizationVersion(
 }
 
 std::string LinearProgram::GetDimensionString() const {
-  return StringPrintf(
+  return absl::StrFormat(
       "%d rows, %d columns, %lld entries", num_constraints().value(),
       num_variables().value(),
       // static_cast<int64> is needed because the Android port uses int32.
@@ -437,8 +438,8 @@ std::string LinearProgram::GetObjectiveStatsString() const {
   if (num_non_zeros == 0) {
     return "No objective term. This is a pure feasibility problem.";
   } else {
-    return StringPrintf("%lld non-zeros, range [%e, %e]", num_non_zeros,
-                        min_value, max_value);
+    return absl::StrFormat("%lld non-zeros, range [%e, %e]", num_non_zeros,
+                           min_value, max_value);
   }
 }
 
diff --git a/ortools/sat/boolean_problem.cc b/ortools/sat/boolean_problem.cc
index 2791d89d38..05f429a6dd 100644
--- a/ortools/sat/boolean_problem.cc
+++ b/ortools/sat/boolean_problem.cc
@@ -24,6 +24,7 @@
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
+#include "ortools/base/stringprintf.h"
 #if !defined(__PORTABLE_PLATFORM__)
 #include "ortools/graph/io.h"
 #endif  // __PORTABLE_PLATFORM__
@@ -424,10 +425,10 @@ std::string LinearBooleanProblemToCnfString(const LinearBooleanProblem& problem)
       hard_weight += weight;
       ++i;
     }
-    output += StringPrintf("p wcnf %d %d %lld\n", first_slack_variable,
-                           static_cast<int>(problem.constraints_size() +
-                                            non_slack_objective.size()),
-                           hard_weight);
+    output += absl::StrFormat("p wcnf %d %d %lld\n", first_slack_variable,
+                              static_cast<int>(problem.constraints_size() +
+                                               non_slack_objective.size()),
+                              hard_weight);
   } else {
     output += StringPrintf("p cnf %d %d\n", problem.num_variables(),
                            problem.constraints_size());
@@ -448,7 +449,7 @@ std::string LinearBooleanProblemToCnfString(const LinearBooleanProblem& problem)
       }
     }
     if (is_wcnf) {
-      output += StringPrintf("%lld ", weight);
+      output += absl::StrFormat("%lld ", weight);
     }
     output += constraint_output + " 0\n";
   }
@@ -459,8 +460,7 @@ std::string LinearBooleanProblemToCnfString(const LinearBooleanProblem& problem)
       // Since it is falsifying this clause that cost "weigtht", we need to take
       // its negation.
       const Literal literal(-p.first);
-      output +=
-          StringPrintf("%lld %s 0\n", p.second, literal.DebugString().c_str());
+      output += absl::StrFormat("%lld %s 0\n", p.second, literal.DebugString().c_str());
     }
   }
 
diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc
index 5ec6523d19..c546642d87 100644
--- a/ortools/sat/clause.cc
+++ b/ortools/sat/clause.cc
@@ -43,12 +43,6 @@ void RemoveIf(Container c, Predicate p) {
   c->erase(std::remove_if(c->begin(), c->end(), p), c->end());
 }
 
-// Removes dettached clauses from a watcher list.
-template <typename Watcher>
-bool CleanUpPredicate(const Watcher& watcher) {
-  return !watcher.clause->IsAttached();
-}
-
 }  // namespace
 
 // ----- LiteralWatchers -----
@@ -204,7 +198,6 @@ SatClause* LiteralWatchers::AddRemovableClause(
 // is not already assigned.
 bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) {
   SCOPED_TIME_STAT(&stats_);
-  ++num_watched_clauses_;
 
   const int size = clause->Size();
   Literal* literals = clause->literals();
@@ -246,33 +239,56 @@ bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) {
     }
   }
 
-  // Attach the watchers.
+  ++num_watched_clauses_;
   AttachOnFalse(literals[0], literals[1], clause);
   AttachOnFalse(literals[1], literals[0], clause);
   return true;
 }
 
-void LiteralWatchers::LazyDetach(SatClause* clause) {
-  SCOPED_TIME_STAT(&stats_);
-  --num_watched_clauses_;
+void LiteralWatchers::Attach(SatClause* clause, Trail* trail) {
+  Literal* literals = clause->literals();
+  CHECK(!trail->Assignment().LiteralIsAssigned(literals[0]));
+  CHECK(!trail->Assignment().LiteralIsAssigned(literals[1]));
 
+  ++num_watched_clauses_;
+  AttachOnFalse(literals[0], literals[1], clause);
+  AttachOnFalse(literals[1], literals[0], clause);
+}
+
+void LiteralWatchers::InternalDetach(SatClause* clause) {
+  --num_watched_clauses_;
   const size_t size = clause->Size();
   if (drat_writer_ != nullptr && size > 2) {
     drat_writer_->DeleteClause({clause->begin(), size});
   }
-
   clauses_info_.erase(clause);
   clause->LazyDetach();
+}
+
+void LiteralWatchers::LazyDetach(SatClause* clause) {
+  InternalDetach(clause);
   is_clean_ = false;
   needs_cleaning_.Set(clause->FirstLiteral().Index());
   needs_cleaning_.Set(clause->SecondLiteral().Index());
 }
 
+void LiteralWatchers::Detach(SatClause* clause) {
+  InternalDetach(clause);
+  for (const Literal l : {clause->FirstLiteral(), clause->SecondLiteral()}) {
+    needs_cleaning_.Clear(l.Index());
+    RemoveIf(&(watchers_on_false_[l.Index()]), [](const Watcher& watcher) {
+      return !watcher.clause->IsAttached();
+    });
+  }
+}
+
 void LiteralWatchers::CleanUpWatchers() {
   SCOPED_TIME_STAT(&stats_);
   for (LiteralIndex index : needs_cleaning_.PositionsSetAtLeastOnce()) {
     DCHECK(needs_cleaning_[index]);
-    RemoveIf(&(watchers_on_false_[index]), CleanUpPredicate<Watcher>);
+    RemoveIf(&(watchers_on_false_[index]), [](const Watcher& watcher) {
+      return !watcher.clause->IsAttached();
+    });
     needs_cleaning_.Clear(index);
   }
   needs_cleaning_.NotifyAllClear();
@@ -281,6 +297,18 @@ void LiteralWatchers::CleanUpWatchers() {
 
 void LiteralWatchers::DeleteDetachedClauses() {
   DCHECK(is_clean_);
+
+  // Update to_minimize_index_.
+  if (to_minimize_index_ >= clauses_.size()) {
+    to_minimize_index_ = clauses_.size();
+  }
+  to_minimize_index_ =
+      std::stable_partition(clauses_.begin(),
+                            clauses_.begin() + to_minimize_index_,
+                            [](SatClause* a) { return a->IsAttached(); }) -
+      clauses_.begin();
+
+  // Do the proper deletion.
   std::vector<SatClause*>::iterator iter =
       std::stable_partition(clauses_.begin(), clauses_.end(),
                             [](SatClause* a) { return a->IsAttached(); });
diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h
index 0379759f1a..1a09c25454 100644
--- a/ortools/sat/clause.h
+++ b/ortools/sat/clause.h
@@ -95,6 +95,13 @@ class SatClause {
   // old_size) of literals().
   bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment);
 
+  // Rewrites a clause with another shorter one. Note that the clause shouldn't
+  // be attached when this is called.
+  void Rewrite(absl::Span<Literal> new_clause) {
+    size_ = 0;
+    for (const Literal l : new_clause) literals_[size_++] = l;
+  }
+
   // Returns true if the clause is satisfied for the given assignment. Note that
   // the assignment may be partial, so false does not mean that the clause can't
   // be satisfied by completing the assignment.
@@ -175,6 +182,13 @@ class LiteralWatchers : public SatPropagator {
   void LazyDetach(SatClause* clause);
   void CleanUpWatchers();
 
+  // Detaches the given clause right away.
+  void Detach(SatClause* clause);
+
+  // Attaches the given clause. The first two literal of the clause must
+  // be unassigned and the clause must not be already attached.
+  void Attach(SatClause* clause, Trail* trail);
+
   // Reclaims the memory of the detached clauses and remove them from
   // AllClausesInCreationOrder() this work in O(num_clauses()).
   void DeleteDetachedClauses();
@@ -206,6 +220,22 @@ class LiteralWatchers : public SatPropagator {
 
   void SetDratWriter(DratWriter* drat_writer) { drat_writer_ = drat_writer; }
 
+  // Really basic algorithm to return a clause to try to minimize. We simply
+  // loop over the clause that we keep forever, in creation order. This starts
+  // by the problem clauses and then the learned one that we keep forever.
+  SatClause* NextClauseToMinimize() {
+    for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
+      if (!clauses_[to_minimize_index_]->IsAttached()) continue;
+      if (!IsRemovable(clauses_[to_minimize_index_])) {
+        return clauses_[to_minimize_index_++];
+      }
+    }
+    return nullptr;
+  }
+
+  // Restart the scan in NextClauseToMinimize() from the first problem clause.
+  void ResetToMinimizeIndex() { to_minimize_index_ = 0; }
+
  private:
   // Attaches the given clause. This eventually propagates a literal which is
   // enqueued on the trail. Returns false if a contradiction was encountered.
@@ -221,6 +251,9 @@ class LiteralWatchers : public SatPropagator {
   void AttachOnFalse(Literal literal, Literal blocking_literal,
                      SatClause* clause);
 
+  // Common code between LazyDetach() and Detach().
+  void InternalDetach(SatClause* clause);
+
   // Contains, for each literal, the list of clauses that need to be inspected
   // when the corresponding literal becomes false.
   struct Watcher {
@@ -253,6 +286,8 @@ class LiteralWatchers : public SatPropagator {
   // here either.
   std::vector<SatClause*> clauses_;
 
+  int to_minimize_index_ = 0;
+
   // Only contains removable clause.
   std::unordered_map<SatClause*, ClauseInfo> clauses_info_;
 
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index ba7f884902..8f2dea852d 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -360,11 +360,8 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
     const LiteralIndex decision = decision_policies[policy_index]();
     if (decision == kNoLiteralIndex) return SatSolver::MODEL_SAT;
 
-    // TODO(user): move the time limit update inside this function?
-    const double saved_deterministic_time = solver->deterministic_time();
     solver->EnqueueDecisionAndBackjumpOnConflict(Literal(decision));
-    time_limit->AdvanceDeterministicTime(solver->deterministic_time() -
-                                         saved_deterministic_time);
+    solver->AdvanceDeterministicTime(time_limit);
     if (solver->IsModelUnsat()) return SatSolver::MODEL_UNSAT;
   }
   return SatSolver::Status::LIMIT_REACHED;
diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc
index 2ccc9aaf31..b6b4576f74 100644
--- a/ortools/sat/optimization.cc
+++ b/ortools/sat/optimization.cc
@@ -30,6 +30,7 @@
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/timer.h"
 #include "ortools/base/join.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/int_type.h"
 #include "ortools/base/map_util.h"
 #if !defined(__PORTABLE_PLATFORM__)
@@ -75,7 +76,7 @@ std::string CnfObjectiveLine(const LinearBooleanProblem& problem,
                         Coefficient objective) {
   const double scaled_objective =
       AddOffsetAndScaleObjectiveValue(problem, objective);
-  return StringPrintf("o %lld", static_cast<int64>(scaled_objective));
+  return absl::StrFormat("o %lld", static_cast<int64>(scaled_objective));
 }
 
 struct LiteralWithCoreIndex {
@@ -248,51 +249,42 @@ void MinimizeCore(SatSolver* solver, std::vector<Literal>* core) {
 void MinimizeCoreWithPropagation(SatSolver* solver,
                                  std::vector<Literal>* core) {
   std::set<LiteralIndex> moved_last;
-  std::deque<Literal> candidate(core->begin(), core->end());
-  while (true) {
-    {
-      // Cyclic shift. We stop as soon as we are back in the original core
-      // order. Because we always preserve the order in the candidate reduction
-      // below, we can abort the first time we see someone we moved back.
-      CHECK(!candidate.empty());
-      const Literal temp = candidate[0];
-      if (ContainsKey(moved_last, temp.Index())) break;
-      moved_last.insert(temp.Index());
-      candidate.erase(candidate.begin());
-      candidate.push_back(temp);
-    }
+  std::vector<Literal> candidate(core->begin(), core->end());
 
-    solver->Backtrack(0);
-    solver->SetAssumptionLevel(0);
+  solver->Backtrack(0);
+  solver->SetAssumptionLevel(0);
+  while (true) {
+    // We want each literal in candidate to appear last once in our propagation
+    // order. We want to do that while maximizing the reutilization of the
+    // current assignment prefix, that is minimizing the number of
+    // decision/progagation we need to perform.
+    const int target_level = MoveOneUnprocessedLiteralLast(
+        moved_last, solver->CurrentDecisionLevel(), &candidate);
+    if (target_level == -1) break;
+    solver->Backtrack(target_level);
     while (solver->CurrentDecisionLevel() < candidate.size()) {
       const Literal decision = candidate[solver->CurrentDecisionLevel()];
       if (solver->Assignment().LiteralIsTrue(decision)) {
         candidate.erase(candidate.begin() + solver->CurrentDecisionLevel());
         continue;
       } else if (solver->Assignment().LiteralIsFalse(decision)) {
-        const int level =
-            solver->LiteralTrail().Info(decision.Variable()).level;
-        if (level + 1 != candidate.size()) {
-          candidate.resize(level);
-          candidate.push_back(decision);
-        }
+        // This is a "weird" API to get the subset of decisions that caused
+        // this literal to be false with reason analysis.
+        solver->EnqueueDecisionAndBacktrackOnConflict(decision);
+        candidate = solver->GetLastIncompatibleDecisions();
         break;
       } else {
         solver->EnqueueDecisionAndBackjumpOnConflict(decision);
       }
     }
+    if (candidate.empty() || solver->IsModelUnsat()) return;
+    moved_last.insert(candidate.back().Index());
   }
 
+  solver->Backtrack(0);
+  solver->SetAssumptionLevel(0);
   if (candidate.size() < core->size()) {
     VLOG(1) << "minimization " << core->size() << " -> " << candidate.size();
-
-    // Check that the order is indeed preserved.
-    int index = 0;
-    for (const Literal l : *core) {
-      if (index < candidate.size() && l == candidate[index]) ++index;
-    }
-    CHECK_EQ(index, candidate.size());
-
     core->assign(candidate.begin(), candidate.end());
   }
 }
@@ -570,9 +562,9 @@ SatSolver::Status SolveWithWPM1(LogBehavior log,
       }
     }
     if (!to_delete.empty()) {
-      logger.Log(StringPrintf("c fixed %zu assumptions, %d with cost > %lld",
-                              to_delete.size(), num_above_threshold,
-                              hardening_threshold.value()));
+      logger.Log(absl::StrFormat("c fixed %zu assumptions, %d with cost > %lld",
+                                 to_delete.size(), num_above_threshold,
+                                 hardening_threshold.value()));
       DeleteVectorIndices(to_delete, &assumptions);
       DeleteVectorIndices(to_delete, &costs);
       DeleteVectorIndices(to_delete, &reference);
@@ -647,10 +639,9 @@ SatSolver::Status SolveWithWPM1(LogBehavior log,
     lower_bound += min_cost;
 
     // Print the search progress.
-    logger.Log(
-        StringPrintf("c iter:%d core:%zu lb:%lld min_cost:%lld strat:%lld",
-                     iter, core.size(), lower_bound.value(), min_cost.value(),
-                     stratified_lower_bound.value()));
+    logger.Log(absl::StrFormat(
+        "c iter:%d core:%zu lb:%lld min_cost:%lld strat:%lld", iter, core.size(),
+        lower_bound.value(), min_cost.value(), stratified_lower_bound.value()));
 
     // This simple line helps a lot on the packup-wpms instances!
     //
@@ -1039,13 +1030,13 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore(
     const std::string gap_string =
         (upper_bound == kCoefficientMax)
             ? ""
-            : StringPrintf(" gap:%lld", (upper_bound - lower_bound).value());
+            : absl::StrFormat(" gap:%lld", (upper_bound - lower_bound).value());
     logger.Log(
-        StringPrintf("c iter:%d [%s] lb:%lld%s assumptions:%zu depth:%d",
-                     iter, previous_core_info.c_str(),
-                     lower_bound.value() - offset.value() +
-                         static_cast<int64>(problem.objective().offset()),
-                     gap_string.c_str(), nodes.size(), max_depth));
+        absl::StrFormat("c iter:%d [%s] lb:%lld%s assumptions:%zu depth:%d", iter,
+                        previous_core_info.c_str(),
+                        lower_bound.value() - offset.value() +
+                            static_cast<int64>(problem.objective().offset()),
+                        gap_string.c_str(), nodes.size(), max_depth));
 
     // Solve under the assumptions.
     const SatSolver::Status result =
@@ -1079,7 +1070,7 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore(
     // The lower bound will be increased by that much.
     const Coefficient min_weight = ComputeCoreMinWeight(nodes, core);
     previous_core_info =
-        StringPrintf("core:%zu mw:%lld", core.size(), min_weight.value());
+        absl::StrFormat("core:%zu mw:%lld", core.size(), min_weight.value());
 
     // Increase stratified_lower_bound according to the parameters.
     if (stratified_lower_bound < min_weight &&
@@ -1555,10 +1546,10 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
 
       max_depth = std::max(max_depth, new_depth);
       if (log_info) {
-        LOG(INFO) << StringPrintf(
-            "core:%zu weight:[%lld,%lld] domain:[%lld,%lld] depth:%d",
-            core.size(), min_weight.value(), max_weight.value(),
-            new_var_lb.value(), new_var_ub.value(), new_depth);
+        LOG(INFO) << absl::StrFormat(
+            "core:%zu weight:[%lld,%lld] domain:[%lld,%lld] depth:%d", core.size(),
+            min_weight.value(), max_weight.value(), new_var_lb.value(),
+            new_var_ub.value(), new_depth);
       }
 
       // We will "transfer" min_weight from all the variables of the core
diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h
index db5621e425..1a25416590 100644
--- a/ortools/sat/optimization.h
+++ b/ortools/sat/optimization.h
@@ -46,6 +46,8 @@ void MinimizeCore(SatSolver* solver, std::vector<Literal>* core);
 // each literal of the initial core "last" at least once, so if such literal can
 // be infered by propagation by any subset of the other literal, it will be
 // removed.
+//
+// Note that this function doest NOT preserve the order of Literal in the core.
 void MinimizeCoreWithPropagation(SatSolver* solver, std::vector<Literal>* core);
 
 // Because the Solve*() functions below are also used in scripts that requires a
diff --git a/ortools/sat/pb_constraint.cc b/ortools/sat/pb_constraint.cc
index 43b5b7b255..2547136777 100644
--- a/ortools/sat/pb_constraint.cc
+++ b/ortools/sat/pb_constraint.cc
@@ -15,6 +15,7 @@
 
 #include <utility>
 
+#include "ortools/base/stringprintf.h"
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/thorough_hash.h"
 #include "ortools/util/saturated_arithmetic.h"
@@ -276,10 +277,10 @@ std::string MutableUpperBoundedLinearConstraint::DebugString() {
   std::string result;
   for (BooleanVariable var : PossibleNonZeros()) {
     if (!result.empty()) result += " + ";
-    result += StringPrintf("%lld[%s]", GetCoefficient(var).value(),
-                           GetLiteral(var).DebugString().c_str());
+    result += absl::StrFormat("%lld[%s]", GetCoefficient(var).value(),
+                              GetLiteral(var).DebugString().c_str());
   }
-  result += StringPrintf(" <= %lld", rhs_.value());
+  result += absl::StrFormat(" <= %lld", rhs_.value());
   return result;
 }
 
diff --git a/ortools/sat/sat_base.h b/ortools/sat/sat_base.h
index 86a93b685c..ba3f7f6f69 100644
--- a/ortools/sat/sat_base.h
+++ b/ortools/sat/sat_base.h
@@ -291,6 +291,10 @@ class Trail {
   }
 
   // Returns the reason why this variable was assigned.
+  //
+  // Note that this shouldn't be called on a variable at level zero, because we
+  // don't cleanup the reason data for these variables but the underlying
+  // clauses may have been deleted.
   absl::Span<Literal> Reason(BooleanVariable var) const;
 
   // Returns the "type" of an assignment (see AssignmentType). Note that this
diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto
index 8cd413306b..d085520463 100644
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -18,7 +18,7 @@ package operations_research.sat;
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 96
+// NEXT TAG: 98
 message SatParameters {
   // ==========================================================================
   // Branching and polarity
@@ -534,4 +534,20 @@ message SatParameters {
   // present. This is usually useful to have but can be slow on model with a lot
   // of precedence.
   optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true];
+
+  // Parameters for an heuristic similar to the one descibed in "An effective
+  // learnt clause minimization approach for CDCL Sat Solvers",
+  // https://www.ijcai.org/proceedings/2017/0098.pdf
+  //
+  // For now, we have a somewhat simpler implementation where every x restart we
+  // spend y decisions on clause minimization. The minimization technique is the
+  // same as the one used to minimize core in max-sat. We also minimize problem
+  // clauses and not just the learned clause that we keep forever like in the
+  // paper.
+  //
+  // Changing these parameters or the kind of clause we minimize seems to have
+  // a big impact on the overall perf on our benchmarks. So this technique seems
+  // definitely useful, but it is hard to tune properly.
+  optional int32 minimize_with_propagation_restart_period = 96 [default = 10];
+  optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000];
 }
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index 772bfa7282..03cb6049b9 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -29,6 +29,7 @@
 #include "ortools/base/stl_util.h"
 #include "ortools/port/proto_utils.h"
 #include "ortools/port/sysinfo.h"
+#include "ortools/sat/util.h"
 #include "ortools/util/saturated_arithmetic.h"
 
 namespace operations_research {
@@ -57,7 +58,6 @@ SatSolver::SatSolver(Model* model)
       num_learned_clause_before_cleanup_(0),
       same_reason_identifier_(*trail_),
       is_relevant_for_core_computation_(true),
-      deterministic_time_at_last_advanced_time_limit_(0.0),
       problem_is_pure_sat_(true),
       drat_writer_(nullptr),
       stats_("SatSolver") {
@@ -98,8 +98,9 @@ int64 SatSolver::num_propagations() const {
 }
 
 double SatSolver::deterministic_time() const {
-  // Each of these counters mesure really basic operations.
-  // The weight are just an estimate of the operation complexity.
+  // Each of these counters mesure really basic operations. The weight are just
+  // an estimate of the operation complexity. Note that these counters are never
+  // reset to zero once a SatSolver is created.
   //
   // TODO(user): Find a better procedure to fix the weight than just educated
   // guess.
@@ -129,7 +130,6 @@ void SatSolver::SetParameters(const SatParameters& parameters) {
 
   restart_->Reset();
   time_limit_->ResetLimitFromParameters(parameters);
-  deterministic_time_at_last_advanced_time_limit_ = deterministic_time();
 }
 
 std::string SatSolver::Indent() const {
@@ -608,7 +608,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
       CHECK(pb_constraints_.AddLearnedConstraint(cst, pb_conflict_.Rhs(),
                                                  trail_));
       CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_);
-      counters_.num_learned_pb_literals_ += cst.size();
+      counters_.num_learned_pb_literals += cst.size();
       return false;
     }
 
@@ -879,12 +879,141 @@ void SatSolver::SetAssumptionLevel(int assumption_level) {
 }
 
 SatSolver::Status SatSolver::SolveWithTimeLimit(TimeLimit* time_limit) {
-  deterministic_time_at_last_advanced_time_limit_ = deterministic_time();
   return SolveInternal(time_limit == nullptr ? time_limit_ : time_limit);
 }
 
 SatSolver::Status SatSolver::Solve() { return SolveInternal(time_limit_); }
 
+void SatSolver::KeepAllClauseUsedToInfer(BooleanVariable variable) {
+  CHECK(Assignment().VariableIsAssigned(variable));
+  if (trail_->Info(variable).level == 0) return;
+  int trail_index = trail_->Info(variable).trail_index;
+  std::vector<bool> is_marked(trail_index + 1, false);  // move to local member.
+  is_marked[trail_index] = true;
+  int num = 1;
+  for (; num > 0 && trail_index >= 0; --trail_index) {
+    if (!is_marked[trail_index]) continue;
+    is_marked[trail_index] = false;
+    --num;
+
+    const BooleanVariable var = (*trail_)[trail_index].Variable();
+    SatClause* clause = ReasonClauseOrNull(var);
+    if (clause != nullptr) {
+      clauses_propagator_.mutable_clauses_info()->erase(clause);
+    }
+    for (const Literal l : trail_->Reason(var)) {
+      const AssignmentInfo& info = trail_->Info(l.Variable());
+      if (info.level == 0) continue;
+      if (!is_marked[info.trail_index]) {
+        is_marked[info.trail_index] = true;
+        ++num;
+      }
+    }
+  }
+}
+
+void SatSolver::TryToMinimizeClause(SatClause* clause) {
+  CHECK_EQ(CurrentDecisionLevel(), 0);
+  ++counters_.minimization_num_clauses;
+
+  std::set<LiteralIndex> moved_last;
+  std::vector<Literal> candidate(clause->begin(), clause->end());
+  while (!is_model_unsat_) {
+    // We want each literal in candidate to appear last once in our propagation
+    // order. We want to do that while maximizing the reutilization of the
+    // current assignment prefix, that is minimizing the number of
+    // decision/progagation we need to perform.
+    const int target_level = MoveOneUnprocessedLiteralLast(
+        moved_last, CurrentDecisionLevel(), &candidate);
+    if (target_level == -1) break;
+    Backtrack(target_level);
+    while (CurrentDecisionLevel() < candidate.size()) {
+      const int level = CurrentDecisionLevel();
+      const Literal literal = candidate[level];
+      if (Assignment().LiteralIsFalse(literal)) {
+        candidate.erase(candidate.begin() + level);
+        continue;
+      } else if (Assignment().LiteralIsTrue(literal)) {
+        const int variable_level =
+            LiteralTrail().Info(literal.Variable()).level;
+        if (variable_level == 0) {
+          counters_.minimization_num_true++;
+          counters_.minimization_num_removed_literals += clause->Size();
+          Backtrack(0);
+          clauses_propagator_.Detach(clause);
+          return;
+        }
+
+        // If literal (at true) wasn't propagated by this clause, then we
+        // know that this clause is subsumed by other clauses in the database,
+        // so we can remove it. Note however that we need to make sure we will
+        // never remove the clauses that subsumes it later.
+        if (ReasonClauseOrNull(literal.Variable()) != clause) {
+          counters_.minimization_num_subsumed++;
+          counters_.minimization_num_removed_literals += clause->Size();
+
+          // TODO(user): do not do that if it make us keep too many clauses?
+          KeepAllClauseUsedToInfer(literal.Variable());
+          Backtrack(0);
+          clauses_propagator_.Detach(clause);
+          return;
+        } else {
+          // Simplify. Note(user): we could only keep in clause the literals
+          // responsible for the propagation, but because of the subsumption
+          // above, this is not needed.
+          if (variable_level + 1 < candidate.size()) {
+            candidate.resize(variable_level);
+            candidate.push_back(literal);
+          }
+        }
+        break;
+      } else {
+        ++counters_.minimization_num_decisions;
+        EnqueueDecisionAndBackjumpOnConflict(literal.Negated());
+        if (!clause->IsAttached()) {
+          Backtrack(0);
+          return;
+        }
+        if (is_model_unsat_) return;
+      }
+    }
+    if (candidate.empty()) {
+      is_model_unsat_ = true;
+      return;
+    }
+    moved_last.insert(candidate.back().Index());
+  }
+
+  Backtrack(0);
+  if (candidate.size() == 1) {
+    if (!Assignment().VariableIsAssigned(candidate[0].Variable())) {
+      counters_.minimization_num_removed_literals += clause->Size();
+      trail_->EnqueueWithUnitReason(candidate[0]);
+    }
+    return;
+  }
+
+  if (parameters_->treat_binary_clauses_separately() && candidate.size() == 2) {
+    counters_.minimization_num_removed_literals += clause->Size() - 2;
+    AddBinaryClauseInternal(candidate[0], candidate[1]);
+    clauses_propagator_.Detach(clause);
+    if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
+    return;
+  }
+
+  if (candidate.size() < clause->Size()) {
+    counters_.minimization_num_removed_literals +=
+        clause->Size() - candidate.size();
+
+    // TODO(user): If the watched literal didn't change, we could just rewrite
+    // the clause while keeping the two watched literals at the beginning.
+    clauses_propagator_.Detach(clause);
+    clause->Rewrite(candidate);
+    clauses_propagator_.Attach(clause, trail_);
+    if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
+  }
+}
+
 SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
   SCOPED_TIME_STAT(&stats_);
   if (is_model_unsat_) return MODEL_UNSAT;
@@ -910,6 +1039,11 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
     LOG(INFO) << "Parameters: " << ProtobufShortDebugString(*parameters_);
   }
 
+  // Used to trigger clause minimization via propagation.
+  int64 next_minimization_num_restart =
+      restart_->NumRestarts() +
+      parameters_->minimize_with_propagation_restart_period();
+
   // Variables used to show the search progress.
   const int kDisplayFrequency = 10000;
   int next_display = parameters_->log_search_progress()
@@ -932,12 +1066,7 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
   for (;;) {
     // Test if a limit is reached.
     if (time_limit != nullptr) {
-      const double current_deterministic_time = deterministic_time();
-      time_limit->AdvanceDeterministicTime(
-          current_deterministic_time -
-          deterministic_time_at_last_advanced_time_limit_);
-      deterministic_time_at_last_advanced_time_limit_ =
-          current_deterministic_time;
+      AdvanceDeterministicTime(time_limit);
       if (time_limit->LimitReached()) {
         if (parameters_->log_search_progress()) {
           LOG(INFO) << "The time limit has been reached. Aborting.";
@@ -999,12 +1128,48 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
         Backtrack(assumption_level_);
       }
 
+      // Clause minimization using propagation.
+      if (CurrentDecisionLevel() == 0 &&
+          restart_->NumRestarts() >= next_minimization_num_restart) {
+        next_minimization_num_restart =
+            restart_->NumRestarts() +
+            parameters_->minimize_with_propagation_restart_period();
+        MinimizeSomeClauses(
+            parameters_->minimize_with_propagation_num_decisions());
+        if (is_model_unsat_) return MODEL_UNSAT;
+      }
+
       DCHECK_GE(CurrentDecisionLevel(), assumption_level_);
       EnqueueNewDecision(decision_policy_->NextBranch());
     }
   }
 }
 
+void SatSolver::MinimizeSomeClauses(int decisions_budget) {
+  // Tricky: we don't want TryToMinimizeClause() to delete to_minimize
+  // while we are processing it.
+  block_clause_deletion_ = true;
+
+  const int64 target_num_branches = counters_.num_branches + decisions_budget;
+  while (counters_.num_branches < target_num_branches &&
+         (time_limit_ == nullptr || !time_limit_->LimitReached())) {
+    SatClause* to_minimize = clauses_propagator_.NextClauseToMinimize();
+    if (to_minimize != nullptr) {
+      TryToMinimizeClause(to_minimize);
+      if (is_model_unsat_) return;
+    } else {
+      if (to_minimize == nullptr) {
+        VLOG(1) << "Minimized all clauses, restarting from first one.";
+        clauses_propagator_.ResetToMinimizeIndex();
+      }
+      break;
+    }
+  }
+
+  block_clause_deletion_ = false;
+  clauses_propagator_.DeleteDetachedClauses();
+}
+
 std::vector<Literal> SatSolver::GetLastIncompatibleDecisions() {
   SCOPED_TIME_STAT(&stats_);
   const Literal false_assumption = decisions_[CurrentDecisionLevel()].literal;
@@ -1134,7 +1299,7 @@ void SatSolver::BumpClauseActivity(SatClause* clause) {
 void SatSolver::RescaleClauseActivities(double scaling_factor) {
   SCOPED_TIME_STAT(&stats_);
   clause_activity_increment_ *= scaling_factor;
-  for (auto& entry : *(clauses_propagator_.mutable_clauses_info())) {
+  for (auto& entry : *clauses_propagator_.mutable_clauses_info()) {
     entry.second.activity *= scaling_factor;
   }
 }
@@ -1204,64 +1369,77 @@ std::string SatSolver::StatusString(Status status) const {
   return StringPrintf("\n  status: %s\n", SatStatusString(status).c_str()) +
          StringPrintf("  time: %fs\n", time_in_s) +
          StringPrintf("  memory: %s\n", MemoryUsage().c_str()) +
-         StringPrintf("  num failures: %" GG_LL_FORMAT "d  (%.0f /sec)\n",
-                      counters_.num_failures,
-                      static_cast<double>(counters_.num_failures) / time_in_s) +
-         StringPrintf("  num branches: %" GG_LL_FORMAT "d (%.0f /sec)\n",
-                      counters_.num_branches,
-                      static_cast<double>(counters_.num_branches) / time_in_s) +
-         StringPrintf("  num propagations: %" GG_LL_FORMAT "d  (%.0f /sec)\n",
-                      num_propagations(),
-                      static_cast<double>(num_propagations()) / time_in_s) +
-         StringPrintf("  num binary propagations: %" GG_LL_FORMAT "d\n",
-                      binary_implication_graph_.num_propagations()) +
-         StringPrintf("  num binary inspections: %" GG_LL_FORMAT "d\n",
-                      binary_implication_graph_.num_inspections()) +
-         StringPrintf("  num binary redundant implications: %" GG_LL_FORMAT
-                      "d\n",
-                      binary_implication_graph_.num_redundant_implications()) +
-         StringPrintf("  num classic minimizations: %" GG_LL_FORMAT
-                      "d"
-                      "  (literals removed: %" GG_LL_FORMAT "d)\n",
-                      counters_.num_minimizations,
-                      counters_.num_literals_removed) +
-         StringPrintf("  num binary minimizations: %" GG_LL_FORMAT
-                      "d"
-                      "  (literals removed: %" GG_LL_FORMAT "d)\n",
-                      binary_implication_graph_.num_minimization(),
-                      binary_implication_graph_.num_literals_removed()) +
-         StringPrintf("  num inspected clauses: %" GG_LL_FORMAT "d\n",
-                      clauses_propagator_.num_inspected_clauses()) +
-         StringPrintf("  num inspected clause_literals: %" GG_LL_FORMAT "d\n",
-                      clauses_propagator_.num_inspected_clause_literals()) +
-         StringPrintf(
-             "  num learned literals: %lld  (avg: %.1f /clause)\n",
+         absl::StrFormat(
+             "  num failures: %" GG_LL_FORMAT "d  (%.0f /sec)\n",
+             counters_.num_failures,
+             static_cast<double>(counters_.num_failures) / time_in_s) +
+         absl::StrFormat(
+             "  num branches: %" GG_LL_FORMAT "d (%.0f /sec)\n",
+             counters_.num_branches,
+             static_cast<double>(counters_.num_branches) / time_in_s) +
+         absl::StrFormat("  num propagations: %" GG_LL_FORMAT
+                         "d  (%.0f /sec)\n",
+                         num_propagations(),
+                         static_cast<double>(num_propagations()) / time_in_s) +
+         absl::StrFormat("  num binary propagations: %" GG_LL_FORMAT "d\n",
+                         binary_implication_graph_.num_propagations()) +
+         absl::StrFormat("  num binary inspections: %" GG_LL_FORMAT "d\n",
+                         binary_implication_graph_.num_inspections()) +
+         absl::StrFormat(
+             "  num binary redundant implications: %" GG_LL_FORMAT "d\n",
+             binary_implication_graph_.num_redundant_implications()) +
+         absl::StrFormat("  num classic minimizations: %" GG_LL_FORMAT
+                         "d"
+                         "  (literals removed: %" GG_LL_FORMAT "d)\n",
+                         counters_.num_minimizations,
+                         counters_.num_literals_removed) +
+         absl::StrFormat("  num binary minimizations: %" GG_LL_FORMAT
+                         "d"
+                         "  (literals removed: %" GG_LL_FORMAT "d)\n",
+                         binary_implication_graph_.num_minimization(),
+                         binary_implication_graph_.num_literals_removed()) +
+         absl::StrFormat("  num inspected clauses: %" GG_LL_FORMAT "d\n",
+                         clauses_propagator_.num_inspected_clauses()) +
+         absl::StrFormat("  num inspected clause_literals: %" GG_LL_FORMAT
+                         "d\n",
+                         clauses_propagator_.num_inspected_clause_literals()) +
+         absl::StrFormat(
+             "  num learned literals: %d  (avg: %.1f /clause)\n",
              counters_.num_literals_learned,
              1.0 * counters_.num_literals_learned / counters_.num_failures) +
-         StringPrintf("  num learned PB literals: %lld  (avg: %.1f /clause)\n",
-                      counters_.num_learned_pb_literals_,
-                      1.0 * counters_.num_learned_pb_literals_ /
-                          counters_.num_failures) +
-         StringPrintf("  num subsumed clauses: %lld\n",
-                      counters_.num_subsumed_clauses) +
-         StringPrintf("  pb num threshold updates: %lld\n",
-                      pb_constraints_.num_threshold_updates()) +
-         StringPrintf("  pb num constraint lookups: %lld\n",
-                      pb_constraints_.num_constraint_lookups()) +
-         StringPrintf("  pb num inspected constraint literals: %lld\n",
-                      pb_constraints_.num_inspected_constraint_literals()) +
+         absl::StrFormat(
+             "  num learned PB literals: %d  (avg: %.1f /clause)\n",
+             counters_.num_learned_pb_literals,
+             1.0 * counters_.num_learned_pb_literals / counters_.num_failures) +
+         absl::StrFormat("  num subsumed clauses: %d\n",
+                         counters_.num_subsumed_clauses) +
+         absl::StrFormat("  minimization_num_clauses: %d\n",
+                         counters_.minimization_num_clauses) +
+         absl::StrFormat("  minimization_num_decisions: %d\n",
+                         counters_.minimization_num_decisions) +
+         absl::StrFormat("  minimization_num_true: %d\n",
+                         counters_.minimization_num_true) +
+         absl::StrFormat("  minimization_num_subsumed: %d\n",
+                         counters_.minimization_num_subsumed) +
+         absl::StrFormat("  minimization_num_removed_literals: %d\n",
+                         counters_.minimization_num_removed_literals) +
+         absl::StrFormat("  pb num threshold updates: %d\n",
+                         pb_constraints_.num_threshold_updates()) +
+         absl::StrFormat("  pb num constraint lookups: %d\n",
+                         pb_constraints_.num_constraint_lookups()) +
+         absl::StrFormat("  pb num inspected constraint literals: %d\n",
+                         pb_constraints_.num_inspected_constraint_literals()) +
          restart_->InfoString() +
          StringPrintf("  deterministic time: %f\n", deterministic_time());
 }
 
 std::string SatSolver::RunningStatisticsString() const {
   const double time_in_s = timer_.Get();
-  return StringPrintf(
-      "%6.2lfs, mem:%s, fails:%" GG_LL_FORMAT
+  return absl::StrFormat(
+      "%6.2fs, mem:%s, fails:%" GG_LL_FORMAT
       "d, "
       "depth:%d, clauses:%lld, tmp:%lld, bin:%llu, restarts:%d, vars:%d",
-      time_in_s, MemoryUsage().c_str(), counters_.num_failures,
-      CurrentDecisionLevel(),
+      time_in_s, MemoryUsage().c_str(), counters_.num_failures, CurrentDecisionLevel(),
       clauses_propagator_.num_clauses() -
           clauses_propagator_.num_removable_clauses(),
       clauses_propagator_.num_removable_clauses(),
@@ -2165,7 +2343,7 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
   // that appear in clauses_info can potentially be removed.
   typedef std::pair<SatClause*, ClauseInfo> Entry;
   std::vector<Entry> entries;
-  auto& clauses_info = *(clauses_propagator_.mutable_clauses_info());
+  auto& clauses_info = *clauses_propagator_.mutable_clauses_info();
   for (auto& entry : clauses_info) {
     if (ClauseIsUsedAsReason(entry.first)) continue;
     if (entry.second.protected_during_next_cleanup) {
@@ -2222,7 +2400,9 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
 
     // TODO(user): If the need arise, we could avoid this linear scan on the
     // full list of clauses by not keeping the clauses from clauses_info there.
-    clauses_propagator_.DeleteDetachedClauses();
+    if (!block_clause_deletion_) {
+      clauses_propagator_.DeleteDetachedClauses();
+    }
   }
 
   num_learned_clause_before_cleanup_ = parameters_->clause_cleanup_period();
diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h
index 448cf2ab9f..0791669fc2 100644
--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -379,6 +379,19 @@ class SatSolver {
   // Mainly visible for testing.
   bool Propagate();
 
+  // This must be called at level zero. It will spend the given num decision and
+  // use propagation to try to minimize some clauses from the database.
+  void MinimizeSomeClauses(int decisions_budget);
+
+  // Advance the given time limit with all the deterministic time that was
+  // elapsed since last call.
+  void AdvanceDeterministicTime(TimeLimit* limit) {
+    const double current = deterministic_time();
+    limit->AdvanceDeterministicTime(
+        current - deterministic_time_at_last_advanced_time_limit_);
+    deterministic_time_at_last_advanced_time_limit_ = current;
+  }
+
  private:
   // Calls Propagate() and returns true if no conflict occurred. Otherwise,
   // learns the conflict, backtracks, enqueues the consequence of the learned
@@ -473,8 +486,8 @@ class SatSolver {
            ReasonClauseOrNull(var) == clause;
   }
 
-  // Add a problem clause. Not that the clause is assumed to be "cleaned", that
-  // is no duplicate variables (not strictly required) and not empty.
+  // Add a problem clause. The clause is assumed to be "cleaned", that is no
+  // duplicate variables (not strictly required) and not empty.
   bool AddProblemClauseInternal(const std::vector<Literal>& literals);
 
   // This is used by all the Add*LinearConstraint() functions. It detects
@@ -615,6 +628,16 @@ class SatSolver {
   std::string StatusString(Status status) const;
   std::string RunningStatisticsString() const;
 
+  // Marks as "non-deletable" all clauses that were used to infer the given
+  // variable. The variable must be currently assigned.
+  void KeepAllClauseUsedToInfer(BooleanVariable variable);
+
+  // Use propagation to try to minimize the given clause. This is really similar
+  // to MinimizeCoreWithPropagation(). It must be called when the current
+  // decision level is zero. Note that because this do a small tree search, it
+  // will impact the variable/clauses activities and may add new conflicts.
+  void TryToMinimizeClause(SatClause* clause);
+
   // This is used by the old non-model constructor.
   Model* model_;
   std::unique_ptr<Model> owned_model_;
@@ -673,30 +696,27 @@ class SatSolver {
 
   // Tracks various information about the solver progress.
   struct Counters {
-    int64 num_branches;
-    int64 num_failures;
+    int64 num_branches = 0;
+    int64 num_failures = 0;
 
     // Minimization stats.
-    int64 num_minimizations;
-    int64 num_literals_removed;
+    int64 num_minimizations = 0;
+    int64 num_literals_removed = 0;
 
     // PB constraints.
-    int64 num_learned_pb_literals_;
+    int64 num_learned_pb_literals = 0;
 
     // Clause learning /deletion stats.
-    int64 num_literals_learned;
-    int64 num_literals_forgotten;
-    int64 num_subsumed_clauses;
+    int64 num_literals_learned = 0;
+    int64 num_literals_forgotten = 0;
+    int64 num_subsumed_clauses = 0;
 
-    Counters()
-        : num_branches(0),
-          num_failures(0),
-          num_minimizations(0),
-          num_literals_removed(0),
-          num_learned_pb_literals_(0),
-          num_literals_learned(0),
-          num_literals_forgotten(0),
-          num_subsumed_clauses(0) {}
+    // TryToMinimizeClause() stats.
+    int64 minimization_num_clauses = 0;
+    int64 minimization_num_decisions = 0;
+    int64 minimization_num_true = 0;
+    int64 minimization_num_subsumed = 0;
+    int64 minimization_num_removed_literals = 0;
   };
   Counters counters_;
 
@@ -737,6 +757,13 @@ class SatSolver {
   std::vector<Literal> extra_reason_literals_;
   std::vector<SatClause*> subsumed_clauses_;
 
+  // When true, temporarily disable the deletion of clauses that are not needed
+  // anymore. This is a hack for TryToMinimizeClause() because we use
+  // propagation in this function which might trigger a clause database
+  // deletion, but we still want the pointer to the clause we wants to minimize
+  // to be valid until the end of that function.
+  bool block_clause_deletion_ = false;
+
   // "cache" to avoid inspecting many times the same reason during conflict
   // analysis.
   VariableWithSameReasonIdentifier same_reason_identifier_;
@@ -756,7 +783,7 @@ class SatSolver {
   // The deterministic time when the time limit was updated.
   // As the deterministic time in the time limit has to be advanced manually,
   // it is necessary to keep track of the last time the time was advanced.
-  double deterministic_time_at_last_advanced_time_limit_;
+  double deterministic_time_at_last_advanced_time_limit_ = 0;
 
   // This is true iff the loaded problem only contains clauses.
   bool problem_is_pure_sat_;
diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc
index 99ff48c46c..d9b7a1f2e4 100644
--- a/ortools/sat/simplification.cc
+++ b/ortools/sat/simplification.cc
@@ -1207,6 +1207,7 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr<SatSolver>* solver,
     presolver.SetDratWriter(drat_writer);
     presolver.SetEquivalentLiteralMapping(equiv_map);
     (*solver)->ExtractClauses(&presolver);
+    (*solver)->AdvanceDeterministicTime(time_limit);
     (*solver).reset(nullptr);
     if (!presolver.Presolve()) {
       VLOG(1) << "UNSAT during presolve.";
diff --git a/ortools/sat/util.cc b/ortools/sat/util.cc
index bba7c15aa7..eda521ed76 100644
--- a/ortools/sat/util.cc
+++ b/ortools/sat/util.cc
@@ -41,5 +41,43 @@ void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters) {
   parameters->set_random_branches_ratio(random->OneIn(2) ? 0.01 : 0.0);
 }
 
+int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
+                                  int relevant_prefix_size,
+                                  std::vector<Literal>* literals) {
+  if (literals->empty()) return -1;
+  if (!ContainsKey(processed, literals->back().Index())) {
+    return std::min<int>(relevant_prefix_size, literals->size());
+  }
+
+  // To get O(n log n) size of suffixes, we will first process the last n/2
+  // literals, we then move all of them first and process the n/2 literals left.
+  // We use the same algorithm recursively. The sum of the suffixes' size S(n)
+  // is thus S(n/2) + n + S(n/2). That gives us the correct complexity. The code
+  // below simulates one step of this algorithm and is made to be "robust" when
+  // from one call to the next, some literals have been removed (but the order
+  // of literals is preserved).
+  int num_processed = 0;
+  int num_not_processed = 0;
+  int target_prefix_size = literals->size() - 1;
+  for (int i = literals->size() - 1; i >= 0; i--) {
+    if (ContainsKey(processed, (*literals)[i].Index())) {
+      ++num_processed;
+    } else {
+      ++num_not_processed;
+      target_prefix_size = i;
+    }
+    if (num_not_processed >= num_processed) break;
+  }
+  if (num_not_processed == 0) return -1;
+  target_prefix_size = std::min(target_prefix_size, relevant_prefix_size);
+
+  // Once a prefix size has been decided, it is always better to
+  // enqueue the literal already processed first.
+  std::stable_partition(
+      literals->begin() + target_prefix_size, literals->end(),
+      [&processed](Literal l) { return ContainsKey(processed, l.Index()); });
+  return target_prefix_size;
+}
+
 }  // namespace sat
 }  // namespace operations_research
diff --git a/ortools/sat/util.h b/ortools/sat/util.h
index 681f2826aa..04fcea186a 100644
--- a/ortools/sat/util.h
+++ b/ortools/sat/util.h
@@ -14,6 +14,7 @@
 #ifndef OR_TOOLS_SAT_UTIL_H_
 #define OR_TOOLS_SAT_UTIL_H_
 
+#include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/base/random.h"
 
@@ -23,6 +24,30 @@ namespace sat {
 // Randomizes the decision heuristic of the given SatParameters.
 void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters);
 
+// Context: this function is not really generic, but required to be unit-tested.
+// It is used in a clause minimization algorithm when we try to detect if any of
+// the clause literals can be propagated by a subset of the other literal being
+// false. For that, we want to enqueue in the solver all the subset of size n-1.
+//
+// This moves one of the unprocessed literal from literals to the last position.
+// The function tries to do that while preserving the longest possible prefix of
+// literals "amortized" through the calls assuming that we want to move each
+// literal to the last position once.
+//
+// For a vector of size n, if we want to call this n times so that each literal
+// is last at least once, the sum of the size of the changed suffixes will be
+// O(n log n). If we where to use a simpler algorithm (like moving the last
+// unprocessed literal to the last position), this sum would be O(n^2).
+//
+// Returns the size of the common prefix of literals before and after the move,
+// or -1 if all the literals are already processed. The argument
+// relevant_prefix_size is used as a hint when keeping more that this prefix
+// size do not matter. The returned value will always be lower or equal to
+// relevant_prefix_size.
+int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
+                                  int relevant_prefix_size,
+                                  std::vector<Literal>* literals);
+
 }  // namespace sat
 }  // namespace operations_research
 
diff --git a/ortools/util/piecewise_linear_function.cc b/ortools/util/piecewise_linear_function.cc
index 18796ce8f9..48c4f441e2 100644
--- a/ortools/util/piecewise_linear_function.cc
+++ b/ortools/util/piecewise_linear_function.cc
@@ -20,6 +20,7 @@
 
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
+#include "ortools/base/stringprintf.h"
 
 namespace operations_research {
 namespace {
@@ -256,16 +257,16 @@ void PiecewiseSegment::AddConstantToY(int64 constant) {
 }
 
 std::string PiecewiseSegment::DebugString() const {
-  std::string result = StringPrintf("PiecewiseSegment(<start: (%" GG_LL_FORMAT
-                               "d, %" GG_LL_FORMAT
-                               "d), "
-                               "end: (%" GG_LL_FORMAT "d, %" GG_LL_FORMAT
-                               "d), "
-                               "reference: (%" GG_LL_FORMAT "d, %" GG_LL_FORMAT
-                               "d), "
-                               "slope = %" GG_LL_FORMAT "d>)",
-                               start_x_, Value(start_x_), end_x_, Value(end_x_),
-                               reference_x_, reference_y_, slope_);
+  std::string result = absl::StrFormat(
+      "PiecewiseSegment(<start: (%" GG_LL_FORMAT "d, %" GG_LL_FORMAT
+      "d), "
+      "end: (%" GG_LL_FORMAT "d, %" GG_LL_FORMAT
+      "d), "
+      "reference: (%" GG_LL_FORMAT "d, %" GG_LL_FORMAT
+      "d), "
+      "slope = %" GG_LL_FORMAT "d>)",
+      start_x_, Value(start_x_), end_x_, Value(end_x_), reference_x_,
+      reference_y_, slope_);
   return result;
 }
 
diff --git a/ortools/util/sorted_interval_list.cc b/ortools/util/sorted_interval_list.cc
index aa28148359..87f8bdae61 100644
--- a/ortools/util/sorted_interval_list.cc
+++ b/ortools/util/sorted_interval_list.cc
@@ -17,13 +17,14 @@
 
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
+#include "ortools/base/stringprintf.h"
 #include "ortools/util/saturated_arithmetic.h"
 
 namespace operations_research {
 
 std::string ClosedInterval::DebugString() const {
-  if (start == end) return StringPrintf("[%" GG_LL_FORMAT "d]", start);
-  return StringPrintf("[%" GG_LL_FORMAT "d,%" GG_LL_FORMAT "d]", start, end);
+  if (start == end) return absl::StrFormat("[%" GG_LL_FORMAT "d]", start);
+  return absl::StrFormat("[%" GG_LL_FORMAT "d,%" GG_LL_FORMAT "d]", start, end);
 }
 
 std::string IntervalsAsString(const std::vector<ClosedInterval>& intervals) {