new heuristics to minimize clauses in SAT; base library changes

2018-03-06 18:17:36 +01:00
parent 79f01620e0
commit 9044de9355
31 changed files with 636 additions and 247 deletions
--- 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
--- 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_
--- 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]);
    }
  }
--- 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);
 }
--- 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;
 }

--- 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 {
--- 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(
--- 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;
    }
--- 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();
--- 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);
--- 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"
--- 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"
--- 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
-
--- 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;
--- 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);
  }
 }

--- 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());
    }
  }

--- 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(); });
--- 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_;

--- 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;
--- 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
--- 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
--- 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;
 }

--- 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
--- 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];
 }
--- 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();
--- 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_;
--- 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.";
--- 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
--- 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

--- 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;
 }

--- 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) {