diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel
index ecb69b34b4..808a16d57d 100644
--- a/ortools/sat/BUILD.bazel
+++ b/ortools/sat/BUILD.bazel
@@ -904,23 +904,16 @@ cc_test(
         ":cp_model_cc_proto",
         ":cp_model_checker",
         ":cp_model_solver",
-        ":cp_model_solver_helpers",
         ":cp_model_test_utils",
-        ":cp_model_utils",
-        ":drat_checker",
         ":lp_utils",
         ":model",
-        ":sat_base",
         ":sat_parameters_cc_proto",
-        ":sat_solver",
-        ":synchronization",
         "//ortools/base:gmock_main",
         "//ortools/base:parse_test_proto",
         "//ortools/linear_solver:linear_solver_cc_proto",
         "//ortools/port:os",
         "//ortools/util:logging",
         "@abseil-cpp//absl/container:flat_hash_set",
-        "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/strings",
     ],
@@ -4274,6 +4267,7 @@ cc_library(
         ":model",
         ":sat_base",
         "//ortools/base:file",
+        "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/strings",
diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc
index f396b1089c..32f0952718 100644
--- a/ortools/sat/clause.cc
+++ b/ortools/sat/clause.cc
@@ -103,6 +103,8 @@ bool LiteralsAreFixedAtRoot(const Trail& trail,
 ClauseManager::ClauseManager(Model* model)
     : SatPropagator("ClauseManager"),
       clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
+      parameters_(*model->GetOrCreate<SatParameters>()),
+      assignment_(model->GetOrCreate<Trail>()->Assignment()),
       implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
       trail_(model->GetOrCreate<Trail>()),
       num_inspected_clauses_(0),
@@ -327,6 +329,9 @@ SatClause* ClauseManager::AddRemovableClause(ClauseId id,
   }
   if (add_clause_callback_ != nullptr) add_clause_callback_(lbd, literals);
   CHECK(AttachAndPropagate(clause, trail));
+
+  // Create an entry in clauses_info_ to mark that clause as removable.
+  clauses_info_[clause].lbd = lbd;
   return clause;
 }
 
@@ -484,6 +489,35 @@ bool ClauseManager::InprocessingFixLiteral(
   return implication_graph_->Propagate(trail_);
 }
 
+void ClauseManager::ChangeLbdIfBetter(SatClause* clause, int new_lbd) {
+  auto it = clauses_info_.find(clause);
+  if (it == clauses_info_.end()) return;
+
+  // Always take the min.
+  if (new_lbd > it->second.lbd) return;
+
+  ++num_lbd_promotions_;
+  if (new_lbd <= parameters_.clause_cleanup_lbd_bound()) {
+    // We keep the clause forever.
+    clauses_info_.erase(it);
+  } else {
+    it->second.lbd = new_lbd;
+  }
+}
+
+bool ClauseManager::RemoveFixedLiteralsAndTestIfTrue(SatClause* clause) {
+  if (clause->RemoveFixedLiteralsAndTestIfTrue(assignment_)) {
+    // The clause is always true, detach it.
+    LazyDelete(clause, DeletionSourceForStat::FIXED_AT_TRUE);
+    return true;
+  }
+
+  // We should have dealt with unit and unsat clause before this.
+  CHECK_GE(clause->size(), 2);
+  ChangeLbdIfBetter(clause, clause->size());
+  return false;
+}
+
 bool ClauseManager::InprocessingRewriteClause(
     SatClause* clause, absl::Span<const Literal> new_clause,
     absl::Span<const ClauseId> clause_ids) {
@@ -543,6 +577,7 @@ bool ClauseManager::InprocessingRewriteClause(
   }
 
   clause->Rewrite(new_clause);
+  ChangeLbdIfBetter(clause, new_clause.size());
 
   // And we reattach it.
   if (all_clauses_are_attached_) {
diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h
index aa9736d856..43294089c6 100644
--- a/ortools/sat/clause.h
+++ b/ortools/sat/clause.h
@@ -107,14 +107,6 @@ class SatClause {
     return absl::Span<const Literal>(&(literals_[0]), size_);
   }
 
-  // Removes literals that are fixed. This should only be called at level 0
-  // where a literal is fixed iff it is assigned. Aborts and returns true if
-  // they are not all false.
-  //
-  // Note that the removed literal can still be accessed in the portion [size,
-  // old_size) of literals().
-  bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment);
-
   // 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.
@@ -134,6 +126,14 @@ class SatClause {
   // never be used afterwards.
   void Clear() { size_ = 0; }
 
+  // Removes literals that are fixed. This should only be called at level 0
+  // where a literal is fixed iff it is assigned. Aborts and returns true if
+  // they are not all false.
+  //
+  // Note that the removed literal can still be accessed in the portion [size,
+  // 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<const Literal> new_clause) {
@@ -154,7 +154,7 @@ class SatClause {
 struct ClauseInfo {
   double activity = 0.0;
   int32_t lbd = 0;
-  bool protected_during_next_cleanup = false;
+  int32_t num_cleanup_rounds_since_last_bumped = 0;
 };
 
 class BinaryImplicationGraph;
@@ -267,6 +267,18 @@ class ClauseManager : public SatPropagator {
     if (it == clauses_info_.end()) return 0;
     return it->second.lbd;
   }
+  void KeepClauseForever(SatClause* const clause) {
+    clauses_info_.erase(clause);
+  }
+  void RescaleClauseActivities(double scaling_factor) {
+    for (auto& entry : clauses_info_) {
+      entry.second.activity *= scaling_factor;
+    }
+  }
+
+  // If the new lbd is better than the stored one, update it.
+  // And return the result of IsRemovable() (this save one hash lookup).
+  void ChangeLbdIfBetter(SatClause* clause, int new_lbd);
 
   // Total number of clauses inspected during calls to Propagate().
   int64_t num_inspected_clauses() const { return num_inspected_clauses_; }
@@ -280,6 +292,10 @@ class ClauseManager : public SatPropagator {
   // Number of clauses currently watched.
   int64_t num_watched_clauses() const { return num_watched_clauses_; }
 
+  // Number of time an existing clause lbd was reduced (due to inprocessing or
+  // recomputation of lbd in different branches).
+  int64_t num_lbd_promotions() const { return num_lbd_promotions_; }
+
   ClauseId GetClauseId(const SatClause* clause) const {
     const auto it = clause_id_.find(clause);
     return it != clause_id_.end() ? it->second : kNoClauseId;
@@ -343,6 +359,8 @@ class ClauseManager : public SatPropagator {
       SatClause* clause, absl::Span<const Literal> new_clause,
       absl::Span<const ClauseId> clause_ids = {});
 
+  bool RemoveFixedLiteralsAndTestIfTrue(SatClause* clause);
+
   // Fix a literal either with an existing LRAT `unit_clause_id`, or with a new
   // inferred unit clause, using `clause_ids` as proof.
   // This do NOT need to be between [Detach/Attach]AllClauses() calls.
@@ -427,14 +445,17 @@ class ClauseManager : public SatPropagator {
   SparseBitset<LiteralIndex> needs_cleaning_;
   bool is_clean_ = true;
 
+  const SatParameters& parameters_;
+  const VariablesAssignment& assignment_;
   BinaryImplicationGraph* implication_graph_;
   Trail* trail_;
 
   // For statistic reporting.
   std::vector<int64_t> deletion_counters_;
-  int64_t num_inspected_clauses_;
-  int64_t num_inspected_clause_literals_;
-  int64_t num_watched_clauses_;
+  int64_t num_inspected_clauses_ = 0;
+  int64_t num_inspected_clause_literals_ = 0;
+  int64_t num_watched_clauses_ = 0;
+  int64_t num_lbd_promotions_ = 0;
   mutable StatsGroup stats_;
 
   // For DetachAllClauses()/AttachAllClauses().
diff --git a/ortools/sat/cp_model_presolve_test.cc b/ortools/sat/cp_model_presolve_test.cc
index 31e7ee1815..f086e60cc5 100644
--- a/ortools/sat/cp_model_presolve_test.cc
+++ b/ortools/sat/cp_model_presolve_test.cc
@@ -8155,10 +8155,10 @@ TEST(PresolveCpModelTest, SolveDiophantine) {
 
   SatParameters params;
   params.set_cp_model_presolve(true);
+  params.set_num_workers(1);
   // Should solve in < .01 second. Note that deterministic time is not
   // completely accurate.
   params.set_max_deterministic_time(.001);
-  params.set_num_workers(1);
   const CpSolverResponse response_with =
       SolveWithParameters(model_proto, params);
 
diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc
index ca2c41950a..b54b1667d3 100644
--- a/ortools/sat/cp_model_search.cc
+++ b/ortools/sat/cp_model_search.cc
@@ -934,6 +934,13 @@ std::vector<SatParameters> GetFullWorkerParameters(
         params.search_branching() == SatParameters::FIXED_SEARCH) {
       continue;
     }
+    // As of November 2025, we don't support any LP reasoning when producing an
+    // UNSAT proof.
+    if ((params.check_lrat_proof() || params.check_drat_proof() ||
+         params.output_drat_proof()) &&
+        params.linearization_level() > 1) {
+      continue;
+    }
 
     // TODO(user): Enable probing_search in deterministic mode.
     // Currently it timeouts on small problems as the deterministic time limit
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 7453ee558f..74ca39db91 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -49,7 +49,6 @@
 #include "absl/types/span.h"
 #include "google/protobuf/arena.h"
 #include "google/protobuf/text_format.h"
-#include "ortools/base/file.h"
 #include "ortools/base/helpers.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/options.h"
@@ -132,32 +131,6 @@ ABSL_FLAG(bool, cp_model_use_hint_for_debug_only, false,
           "complete, validate that no buggy propagator make it infeasible.");
 ABSL_FLAG(bool, cp_model_fingerprint_model, true, "Fingerprint the model.");
 
-ABSL_FLAG(std::string, cp_model_drat_output, "",
-          "If non-empty, a proof in DRAT format will be written to this file. "
-          "This only works in the same conditions as the --cp_model_lrat_check "
-          "flag, and only for pure SAT models.");
-
-ABSL_FLAG(bool, cp_model_drat_check, false,
-          "If true, a proof in DRAT format will be stored in memory and "
-          "checked if the problem is UNSAT. This only works in the same "
-          "conditions as the --cp_model_lrat_check flag, and only for pure SAT "
-          "models.");
-
-ABSL_FLAG(bool, cp_model_lrat_check, false,
-          "If true, inferred clauses are checked with an LRAT checker as they "
-          "are learned. As of November 2025, this only works with a single "
-          "worker and symmetry level 0 or 1. This also works with presolve, if "
-          "find_clauses_that_are_exactly_one is false and "
-          "merge_at_most_one_work_limit is 0. However, in this case, the "
-          "presolved problem is assumed to be correct, without proof. If the "
-          "model is not pure SAT, the checks are only partial (some clauses "
-          "can be assumed without proof).");
-
-ABSL_FLAG(double, cp_model_max_drat_time_in_seconds,
-          std::numeric_limits<double>::infinity(),
-          "Maximum time in seconds to check the DRAT proof. This will only "
-          "be used is the cp_model_drat_check flag is enabled.");
-
 ABSL_FLAG(bool, cp_model_check_intermediate_solutions, false,
           "When true, all intermediate solutions found by the solver will be "
           "checked. This can be expensive, therefore it is off by default.");
@@ -1035,26 +1008,6 @@ bool SolutionHintIsCompleteAndFeasible(
   }
 }
 
-std::unique_ptr<LratProofHandler> MaybeCreateLratProofHandler(Model* model) {
-  const bool check_lrat = absl::GetFlag(FLAGS_cp_model_lrat_check);
-  const bool check_drat = absl::GetFlag(FLAGS_cp_model_drat_check);
-  File* drat_output = nullptr;
-  if (!absl::GetFlag(FLAGS_cp_model_drat_output).empty()) {
-    CHECK_OK(file::Open(absl::GetFlag(FLAGS_cp_model_drat_output), "w",
-                        &drat_output, file::Defaults()));
-  }
-  if (!check_lrat && !check_drat && drat_output == nullptr) return nullptr;
-
-  // TODO(user): pass the [presolved] model proto to the handler, so that
-  // it can map internal problem clause IDs to constraint indices in the
-  // original model. This will be needed to write the LRAT proof in a file that
-  // can be checked with an external LRAT checker, expecting the standard LRAT
-  // ASCII file format (which requires problem clauses IDs between 1 and n).
-  return std::make_unique<LratProofHandler>(model, check_lrat, check_drat,
-                                            drat_output,
-                                            /*in_binary_drat_format=*/false);
-}
-
 // Encapsulate a full CP-SAT solve without presolve in the SubSolver API.
 class FullProblemSolver : public SubSolver {
  public:
@@ -1082,7 +1035,7 @@ class FullProblemSolver : public SubSolver {
     shared_->RegisterSharedClassesInLocalModel(&local_model_);
 
     std::unique_ptr<LratProofHandler> lrat_proof_handler =
-        MaybeCreateLratProofHandler(&local_model_);
+        LratProofHandler::MaybeCreate(&local_model_);
     if (lrat_proof_handler != nullptr) {
       local_model_.Register<LratProofHandler>(lrat_proof_handler.get());
       local_model_.TakeOwnership(lrat_proof_handler.release());
@@ -1111,8 +1064,7 @@ class FullProblemSolver : public SubSolver {
       WallTimer timer;
       timer.Start();
       const bool valid = local_model_.GetOrCreate<SatSolver>()->ModelIsUnsat()
-                             ? lrat_proof_handler->Check(absl::GetFlag(
-                                   FLAGS_cp_model_max_drat_time_in_seconds))
+                             ? lrat_proof_handler->Check()
                              : lrat_proof_handler->Valid();
       shared_->lrat_proof_status->NewSubsolverProofStatus(
           valid ? DratChecker::Status::VALID : DratChecker::Status::INVALID,
@@ -1801,12 +1753,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
   const SatParameters& params = *global_model->GetOrCreate<SatParameters>();
   if (global_model->GetOrCreate<TimeLimit>()->LimitReached()) return;
 
-  if (absl::GetFlag(FLAGS_cp_model_drat_check) ||
-      !absl::GetFlag(FLAGS_cp_model_drat_output).empty()) {
-    LOG(WARNING)
-        << "DRAT check and output are skipped when using several workers";
-    absl::SetFlag(&FLAGS_cp_model_drat_check, false);
-    absl::SetFlag(&FLAGS_cp_model_drat_output, "");
+  if (params.check_drat_proof() || params.output_drat_proof()) {
+    LOG(FATAL) << "DRAT proofs are not supported with several workers";
   }
 
   // If specified by the user, we might disable some parameters based on their
diff --git a/ortools/sat/cp_model_solver.h b/ortools/sat/cp_model_solver.h
index 3dc66e9751..aaafcaa2aa 100644
--- a/ortools/sat/cp_model_solver.h
+++ b/ortools/sat/cp_model_solver.h
@@ -26,9 +26,6 @@
 
 #ifndef SWIG
 OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_dump_response);
-OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_drat_check);
-OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_lrat_check);
-OR_DLL ABSL_DECLARE_FLAG(double, cp_model_max_drat_time_in_seconds);
 #endif
 
 namespace operations_research {
diff --git a/ortools/sat/cp_model_solver_test.cc b/ortools/sat/cp_model_solver_test.cc
index e5a223885e..d5a45c6eaf 100644
--- a/ortools/sat/cp_model_solver_test.cc
+++ b/ortools/sat/cp_model_solver_test.cc
@@ -14,12 +14,10 @@
 #include "ortools/sat/cp_model_solver.h"
 
 #include <cstdint>
-#include <memory>
 #include <string>
 #include <vector>
 
 #include "absl/container/flat_hash_set.h"
-#include "absl/flags/flag.h"
 #include "absl/log/log.h"
 #include "absl/strings/str_join.h"
 #include "gtest/gtest.h"
@@ -29,15 +27,10 @@
 #include "ortools/port/os.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_checker.h"
-#include "ortools/sat/cp_model_solver_helpers.h"
 #include "ortools/sat/cp_model_test_utils.h"
-#include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/lp_utils.h"
 #include "ortools/sat/model.h"
-#include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
-#include "ortools/sat/sat_solver.h"
-#include "ortools/sat/synchronization.h"
 #include "ortools/util/logging.h"
 
 namespace operations_research {
@@ -5462,11 +5455,11 @@ TEST(CpModelSolverTest, DratProofIsValidForRandom3Sat) {
   SatParameters params;
   params.set_num_workers(1);
   params.set_cp_model_presolve(false);
-  params.set_symmetry_level(0);
-  params.set_linearization_level(0);
+  params.set_symmetry_level(1);
+  params.set_linearization_level(1);
+  params.set_check_drat_proof(true);
+  params.set_max_drat_time_in_seconds(60);
   params.set_debug_crash_if_lrat_check_fails(true);
-  absl::SetFlag(&FLAGS_cp_model_drat_check, true);
-  absl::SetFlag(&FLAGS_cp_model_max_drat_time_in_seconds, 60);
 
   int num_infeasible = 0;
   for (int i = 0; i < 100; ++i) {
@@ -5484,12 +5477,12 @@ TEST(CpModelSolverTest, DratProofIsValidForRandom3Sat) {
 
 TEST(CpModelSolverTest, LratProofIsValidForRandom3Sat) {
   SatParameters params;
-  params.set_num_workers(1);
+  params.set_num_workers(8);
   params.set_cp_model_presolve(false);
-  params.set_symmetry_level(0);
-  params.set_linearization_level(0);
+  params.set_symmetry_level(1);
+  params.set_linearization_level(1);
+  params.set_check_lrat_proof(true);
   params.set_debug_crash_if_lrat_check_fails(true);
-  absl::SetFlag(&FLAGS_cp_model_lrat_check, true);
 
   int num_infeasible = 0;
   for (int i = 0; i < 100; ++i) {
diff --git a/ortools/sat/csharp/CpSolver.cs b/ortools/sat/csharp/CpSolver.cs
index ab9bc8b336..c2a1449ee0 100644
--- a/ortools/sat/csharp/CpSolver.cs
+++ b/ortools/sat/csharp/CpSolver.cs
@@ -201,6 +201,8 @@ public sealed class CpSolver : IDisposable
 
     public double WallTime() => Response!.WallTime;
 
+    public string SolveLog() => Response!.SolveLog;
+
     public IList<int> SufficientAssumptionsForInfeasibility() => Response!.SufficientAssumptionsForInfeasibility;
 
     public string SolutionInfo() => Response!.SolutionInfo;
diff --git a/ortools/sat/java/CpSolverTest.java b/ortools/sat/java/CpSolverTest.java
index 743436f783..e3c15e9bd0 100644
--- a/ortools/sat/java/CpSolverTest.java
+++ b/ortools/sat/java/CpSolverTest.java
@@ -109,7 +109,7 @@ public final class CpSolverTest {
     final CpSolverStatus status = solver.solve(model);
 
     assertThat(status).isEqualTo(CpSolverStatus.MODEL_INVALID);
-    assertEquals("var #0 has no domain(): name: \"x\"", solver.getSolutionInfo());
+    assertEquals("var #0 has no domain(): name: \"x\"", solver.solutionInfo());
   }
 
   @Test
@@ -309,6 +309,32 @@ public final class CpSolverTest {
     assertThat(log).contains("OPTIMAL");
   }
 
+  @Test
+  public void testCpSolver_logToResponse() throws Exception {
+    System.out.println("testCpSolver_logToResponse");
+    final CpModel model = new CpModel();
+    assertNotNull(model);
+    // Creates the variables.
+    final int numVals = 3;
+    final IntVar x = model.newIntVar(0, numVals - 1, "x");
+    final IntVar y = model.newIntVar(0, numVals - 1, "y");
+    // Creates the constraints.
+    model.addDifferent(x, y);
+
+    // Creates a solver and solves the model.
+    final CpSolver solver = new CpSolver();
+    assertNotNull(solver);
+    solver.getParameters().setLogToStdout(false).setLogSearchProgress(true).setLogToResponse(true);
+    final CpSolverStatus status = solver.solve(model);
+
+    assertThat(status).isEqualTo(CpSolverStatus.OPTIMAL);
+    String log = solver.solveLog();
+    assertThat(log).isNotEmpty();
+    assertThat(log).contains("Parameters");
+    assertThat(log).contains("log_to_stdout: false");
+    assertThat(log).contains("OPTIMAL");
+  }
+
   @Test
   public void testCpSolver_customLogMultiThread() {
     System.out.println("testCpSolver_customLogMultiThread");
diff --git a/ortools/sat/lrat_proof_handler.cc b/ortools/sat/lrat_proof_handler.cc
index 0eb1e4f6ec..0fb196165b 100644
--- a/ortools/sat/lrat_proof_handler.cc
+++ b/ortools/sat/lrat_proof_handler.cc
@@ -16,19 +16,30 @@
 #include <algorithm>
 #include <cstdlib>
 #include <memory>
+#include <string>
 #include <vector>
 
+#include "absl/flags/flag.h"
 #include "absl/log/check.h"
 #include "absl/log/log.h"
 #include "absl/strings/str_join.h"
 #include "absl/types/span.h"
 #include "ortools/base/file.h"
+#include "ortools/base/options.h"
 #include "ortools/sat/drat_checker.h"
 #include "ortools/sat/drat_writer.h"
 #include "ortools/sat/lrat_checker.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 
+#if defined(_MSC_VER)
+ABSL_FLAG(std::string, cp_model_drat_output, ".\\drat.txt",
+          "File name for the generated DRAT proof, if DRAT output is enabled.");
+#else
+ABSL_FLAG(std::string, cp_model_drat_output, "/tmp/drat.txt",
+          "File name for the generated DRAT proof, if DRAT output is enabled.");
+#endif
+
 namespace operations_research {
 namespace sat {
 
@@ -46,18 +57,33 @@ std::vector<Literal> SortClauseForDrat(absl::Span<const Literal> clause) {
 }
 }  // namespace
 
-LratProofHandler::LratProofHandler(Model* model, bool check_lrat,
-                                   bool check_drat, File* drat_output,
-                                   bool in_binary_drat_format)
-    : lrat_checker_(check_lrat ? std::make_unique<LratChecker>(model)
-                               : nullptr),
-      drat_checker_(check_drat ? std::make_unique<DratChecker>() : nullptr),
-      drat_writer_(
-          drat_output != nullptr
-              ? std::make_unique<DratWriter>(in_binary_drat_format, drat_output)
-              : nullptr),
-      debug_crash_on_error_(model->GetOrCreate<SatParameters>()
-                                ->debug_crash_if_lrat_check_fails()) {}
+std::unique_ptr<LratProofHandler> LratProofHandler::MaybeCreate(Model* model) {
+  const SatParameters& params = *model->GetOrCreate<SatParameters>();
+  if (!params.check_lrat_proof() && !params.check_drat_proof() &&
+      !params.output_drat_proof()) {
+    return nullptr;
+  }
+  return std::unique_ptr<LratProofHandler>(new LratProofHandler(model));
+}
+
+LratProofHandler::LratProofHandler(Model* model) {
+  const SatParameters& params = *model->GetOrCreate<SatParameters>();
+  if (params.check_lrat_proof()) {
+    lrat_checker_ = std::make_unique<LratChecker>(model);
+  }
+  if (params.check_drat_proof()) {
+    drat_checker_ = std::make_unique<DratChecker>();
+  }
+  if (params.output_drat_proof()) {
+    File* drat_output = nullptr;
+    CHECK_OK(file::Open(absl::GetFlag(FLAGS_cp_model_drat_output), "w",
+                        &drat_output, file::Defaults()));
+    drat_writer_ = std::make_unique<DratWriter>(
+        /*in_binary_drat_format=*/false, drat_output);
+  }
+  max_drat_time_in_seconds_ = params.max_drat_time_in_seconds();
+  debug_crash_on_error_ = params.debug_crash_if_lrat_check_fails();
+}
 
 bool LratProofHandler::AddProblemClause(ClauseId id,
                                         absl::Span<const Literal> clause) {
@@ -193,15 +219,14 @@ DratChecker::Status LratProofHandler::Valid() const {
   return DratChecker::Status::UNKNOWN;
 }
 
-DratChecker::Status LratProofHandler::Check(
-    double max_drat_check_time_in_seconds) {
+DratChecker::Status LratProofHandler::Check() {
   DratChecker::Status status = DratChecker::Status::UNKNOWN;
   if (lrat_checker_ != nullptr) {
     status = CheckResult(lrat_checker_->Check()) ? DratChecker::Status::VALID
                                                  : DratChecker::Status::INVALID;
   }
   if (status != DratChecker::Status::INVALID && drat_checker_ != nullptr) {
-    drat_checker_->Check(max_drat_check_time_in_seconds);
+    drat_checker_->Check(max_drat_time_in_seconds_);
     if (status == DratChecker::Status::INVALID && debug_crash_on_error_) {
       LOG(FATAL) << "DRAT check failed";
     }
diff --git a/ortools/sat/lrat_proof_handler.h b/ortools/sat/lrat_proof_handler.h
index 8006804cb8..be5d1c7649 100644
--- a/ortools/sat/lrat_proof_handler.h
+++ b/ortools/sat/lrat_proof_handler.h
@@ -20,7 +20,6 @@
 #include <vector>
 
 #include "absl/types/span.h"
-#include "ortools/base/file.h"
 #include "ortools/sat/drat_checker.h"
 #include "ortools/sat/drat_writer.h"
 #include "ortools/sat/lrat_checker.h"
@@ -34,8 +33,12 @@ namespace sat {
 // and/or by saving it to a file.
 class LratProofHandler {
  public:
-  explicit LratProofHandler(Model* model, bool check_lrat, bool check_drat,
-                            File* drat_output, bool in_binary_drat_format);
+  // TODO(user): pass the [presolved] model proto to the handler, so that
+  // it can map internal problem clause IDs to constraint indices in the
+  // original model. This will be needed to write the LRAT proof in a file that
+  // can be checked with an external LRAT checker, expecting the standard LRAT
+  // ASCII file format (which requires problem clauses IDs between 1 and n).
+  static std::unique_ptr<LratProofHandler> MaybeCreate(Model* model);
 
   bool lrat_check_enabled() const { return lrat_checker_ != nullptr; }
   bool drat_check_enabled() const { return drat_checker_ != nullptr; }
@@ -84,23 +87,25 @@ class LratProofHandler {
   // whether the empty clause has been successfully inferred. Returns INVALID if
   // it is not. Returns UNKNOWN if the check timed out (this can only occur
   // with DRAT checks), or if neither LRAT nor DRAT checks were enabled.
-  DratChecker::Status Check(double max_drat_check_time_in_seconds =
-                                std::numeric_limits<double>::infinity());
+  DratChecker::Status Check();
 
   void AddStats() const;
 
   int64_t num_assumed_clauses() const { return num_assumed_clauses_; }
 
  private:
+  explicit LratProofHandler(Model* model);
+
   bool CheckResult(bool result) const;
 
   std::unique_ptr<LratChecker> lrat_checker_;
   std::unique_ptr<DratChecker> drat_checker_;
   std::unique_ptr<DratWriter> drat_writer_;
+  double max_drat_time_in_seconds_ = std::numeric_limits<double>::infinity();
+  bool debug_crash_on_error_ = false;
 
   bool all_problem_clauses_loaded_ = false;
   int64_t num_assumed_clauses_ = 0;
-  bool debug_crash_on_error_ = false;
 
   ClauseId pinned_clause_id_ = kNoClauseId;
   std::vector<Literal> pinned_clause_;
diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc
index 1e7f52e628..598d536d21 100644
--- a/ortools/sat/parameters_validation.cc
+++ b/ortools/sat/parameters_validation.cc
@@ -106,6 +106,7 @@ std::string ValidateParameters(const SatParameters& params) {
 
   TEST_NOT_NAN(max_time_in_seconds);
   TEST_NOT_NAN(max_deterministic_time);
+  TEST_NOT_NAN(max_drat_time_in_seconds);
 
   // Parallelism.
   const int kMaxReasonableParallelism = 10'000;
diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc
index 4a048e3923..49cecc4f94 100644
--- a/ortools/sat/probing.cc
+++ b/ortools/sat/probing.cc
@@ -1353,7 +1353,12 @@ void FailedLiteralProbing::MaybeSubsumeWithBinaryClause(
       break;
     }
   }
-  if (!subsumed) return;
+  if (!subsumed) {
+    // The clause is not subsumed but its lbd is 2 when last_decision is
+    // propagated. This is a "glue" clause.
+    clause_manager_->ChangeLbdIfBetter(clause, 2);
+    return;
+  }
 
   // Since we will remove the clause, we need to make sure we do have the
   // implication in our repository.
diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py
index d6a0094666..dfc01b3432 100644
--- a/ortools/sat/python/cp_model.py
+++ b/ortools/sat/python/cp_model.py
@@ -1869,6 +1869,19 @@ class CpSolver:
         """Returns the user time in seconds since the creation of the solver."""
         return self._checked_response.user_time
 
+    @property
+    def solve_log(self) -> str:
+        """Returns the solve log.
+
+        To enable this, the parameter log_to_response must be set to True.
+        """
+        return self._checked_response.solve_log
+
+    @property
+    def solve_info(self) -> str:
+        """Returns the information about the solve."""
+        return self._checked_response.solve_info
+
     @property
     def response_proto(self) -> cmh.CpSolverResponse:
         """Returns the response object."""
@@ -1948,17 +1961,6 @@ class CpSolver:
     def WallTime(self) -> float:
         return self.wall_time
 
-    def SolveWithSolutionCallback(
-        self, model: CpModel, callback: "CpSolverSolutionCallback"
-    ) -> cmh.CpSolverStatus:
-        """DEPRECATED Use solve() with the callback argument."""
-        warnings.warn(
-            "solve_with_solution_callback is deprecated; use solve() with"
-            + "the callback argument.",
-            DeprecationWarning,
-        )
-        return self.solve(model, callback)
-
     def SearchForAllSolutions(
         self, model: CpModel, callback: "CpSolverSolutionCallback"
     ) -> cmh.CpSolverStatus:
diff --git a/ortools/sat/python/cp_model_test.py b/ortools/sat/python/cp_model_test.py
index 28d182ef17..92505d347c 100644
--- a/ortools/sat/python/cp_model_test.py
+++ b/ortools/sat/python/cp_model_test.py
@@ -2080,7 +2080,26 @@ class CpModelTest(absltest.TestCase):
         self.assertEqual(10, solver.value(x))
         self.assertEqual(-5, solver.value(y))
 
-        self.assertRegex(log_callback.log, ".*log_to_stdout.*")
+        self.assertRegex(log_callback.log, "Starting CP-SAT solver")
+
+    def test_log_to_response(self) -> None:
+        model = cp_model.CpModel()
+        x = model.new_int_var(-10, 10, "x")
+        y = model.new_int_var(-10, 10, "y")
+        model.add_linear_constraint(x + 2 * y, 0, 10)
+        model.minimize(y)
+        solver = cp_model.CpSolver()
+        solver.parameters.log_search_progress = True
+        solver.parameters.log_to_stdout = False
+        solver.parameters.log_to_response = True
+
+        self.assertEqual(cp_model.OPTIMAL, solver.solve(model))
+        self.assertEqual(10, solver.value(x))
+        self.assertEqual(-5, solver.value(y))
+
+        self.assertRegex(solver.solve_log, "Starting CP-SAT solver")
+        print(solver.solution_info)
+        print(solver.solve_log)
 
     def test_issue2762(self) -> None:
         model = cp_model.CpModel()
diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto
index 74604a1924..90871777e3 100644
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -24,7 +24,7 @@ option java_multiple_files = true;
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 344
+// NEXT TAG: 351
 message SatParameters {
   // In some context, like in a portfolio of search, it makes sense to name a
   // given parameters set for logging purpose.
@@ -176,23 +176,25 @@ message SatParameters {
   // target of clauses to keep.
   optional double clause_cleanup_ratio = 190 [default = 0.5];
 
-  // Each time a clause activity is bumped, the clause has a chance to be
-  // protected during the next cleanup phase. Note that clauses used as a reason
-  // are always protected.
-  enum ClauseProtection {
-    PROTECTION_NONE = 0;    // No protection.
-    PROTECTION_ALWAYS = 1;  // Protect all clauses whose activity is bumped.
-    PROTECTION_LBD = 2;     // Only protect clause with a better LBD.
-  }
-  optional ClauseProtection clause_cleanup_protection = 58
-      [default = PROTECTION_NONE];
-
   // All the clauses with a LBD (literal blocks distance) lower or equal to this
   // parameters will always be kept.
+  //
+  // Note that the LBD of a clause that just propagated is 1 + number of
+  // different decision levels of its literals. So that the "classic" LBD of a
+  // learned conflict is the same as its LBD when we backjump and then propagate
+  // it.
   optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
 
-  // Only protect clauses up to this maximum LBD.
-  optional int32 clause_protection_lbd_bound = 338 [default = 8];
+  // All the clause with a LBD lower or equal to this will be kept except if
+  // its activity hasn't been bumped in the last 32 cleanup phase. Note that
+  // this has no effect if it is <= clause_cleanup_lbd_bound.
+  optional int32 clause_cleanup_lbd_tier1 = 349 [default = 0];
+
+  // All the clause with a LBD lower or equal to this will be kept except if its
+  // activity hasn't been bumped since the previous cleanup phase. Note that
+  // this has no effect if it is <= clause_cleanup_lbd_bound or <=
+  // clause_cleanup_lbd_tier1.
+  optional int32 clause_cleanup_lbd_tier2 = 350 [default = 0];
 
   // The clauses that will be kept during a cleanup are the ones that come
   // first under this order. We always keep or exclude ties together.
@@ -778,6 +780,43 @@ message SatParameters {
   // The amount of dtime between each export of shared glue clauses.
   optional double share_glue_clauses_dtime = 322 [default = 1.0];
 
+  // ==========================================================================
+  // Proofs
+  // ==========================================================================
+
+  // If true, inferred clauses are checked with an LRAT checker as they are
+  // learned. As of November 2025, this only works with pure SAT problems, with
+  //  - cp_model_presolve = false,
+  //  - linearization_level <= 1,
+  //  - symmetry_level <= 1,
+  //  - shared_tree_num_workers = 0.
+  optional bool check_lrat_proof = 344 [default = false];
+
+  // TODO(user): add and implement an output_lrat_proof field.
+  reserved 345;
+
+  // If true, and if the problem is UNSAT, a DRAT proof of this UNSAT property
+  // is checked after the solver has finished. As of November 2025, this only
+  // works for pure SAT problems, with
+  //  - num_workers = 1,
+  //  - cp_model_presolve = false,
+  //  - linearization_level <= 1,
+  //  - symmetry_level <= 1.
+  optional bool check_drat_proof = 346 [default = false];
+
+  // If true, a DRAT proof that all the clauses inferred by the solver are valid
+  // is output to a file. As of November 2025, this only works for pure SAT
+  // problems, with
+  //  - num_workers = 1,
+  //  - cp_model_presolve = false,
+  //  - linearization_level <= 1,
+  //  - symmetry_level <= 1.
+  optional bool output_drat_proof = 347 [default = false];
+
+  // The maximum time allowed to check the DRAT proof (this can take more time
+  // than the solve itself). Only used if check_drat_proof is true.
+  optional double max_drat_time_in_seconds = 348 [default = inf];
+
   // ==========================================================================
   // Debugging parameters
   // ==========================================================================
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index 7a89d68b30..08e2d8f2e5 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -492,10 +492,6 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
 
     SatClause* clause = clauses_propagator_->AddRemovableClause(
         clause_id, literals, trail_, lbd);
-
-    // BumpClauseActivity() must be called after clauses_info_[clause] has
-    // been created or it will have no effect.
-    (*clauses_propagator_->mutable_clauses_info())[clause].lbd = lbd;
     BumpClauseActivity(clause);
   } else {
     CHECK(clauses_propagator_->AddClause(clause_id, literals, trail_, lbd));
@@ -831,16 +827,17 @@ void SatSolver::ProcessCurrentConflict(
   }
 
   // Bump the clause activities.
-  // Note that the activity of the learned clause will be bumped too
-  // by AddLearnedClauseAndEnqueueUnitPropagation().
+  //
+  // Note that the activity of the learned clause will be bumped too by
+  // AddLearnedClauseAndEnqueueUnitPropagation() after we update the increment.
   if (trail_->FailingSatClause() != nullptr) {
     BumpClauseActivity(trail_->FailingSatClause());
   }
   BumpReasonActivities(reason_used_to_infer_the_conflict_);
+  UpdateClauseActivityIncrement();
 
   // Decay the activities.
   decision_policy_->UpdateVariableActivityIncrement();
-  UpdateClauseActivityIncrement();
   pb_constraints_->UpdateActivityIncrement();
 
   // Hack from Glucose that seems to perform well.
@@ -1385,8 +1382,7 @@ void SatSolver::KeepAllClausesUsedToInfer(BooleanVariable variable) {
     const BooleanVariable var = (*trail_)[trail_index].Variable();
     SatClause* clause = ReasonClauseOrNull(var);
     if (clause != nullptr) {
-      // Keep this clause.
-      clauses_propagator_->mutable_clauses_info()->erase(clause);
+      clauses_propagator_->KeepClauseForever(clause);
     }
     if (trail_->AssignmentType(var) == AssignmentType::kSearchDecision) {
       continue;
@@ -2044,43 +2040,26 @@ void SatSolver::BumpClauseActivity(SatClause* clause) {
   auto it = clauses_propagator_->mutable_clauses_info()->find(clause);
   if (it == clauses_propagator_->mutable_clauses_info()->end()) return;
 
-  // Check if the new clause LBD is below our threshold to keep this clause
-  // indefinitely.
-  const int new_lbd = ComputeLbd(clause->AsSpan());
-  if (new_lbd <= parameters_->clause_cleanup_lbd_bound()) {
-    clauses_propagator_->mutable_clauses_info()->erase(clause);
-    return;
-  }
-
-  // Potentially protect this clause for the next cleanup phase.
-  if (new_lbd <= parameters_->clause_protection_lbd_bound()) {
-    switch (parameters_->clause_cleanup_protection()) {
-      case SatParameters::PROTECTION_NONE:
-        break;
-      case SatParameters::PROTECTION_ALWAYS:
-        it->second.protected_during_next_cleanup = true;
-        break;
-      case SatParameters::PROTECTION_LBD:
-        if (new_lbd < it->second.lbd) {
-          it->second.protected_during_next_cleanup = true;
-          it->second.lbd = new_lbd;
-        }
-    }
-  }
+  it->second.num_cleanup_rounds_since_last_bumped = 0;
 
   // Increase the activity.
   const double activity = it->second.activity += clause_activity_increment_;
   if (activity > parameters_->max_clause_activity_value()) {
     RescaleClauseActivities(1.0 / parameters_->max_clause_activity_value());
   }
+
+  // Update this clause LBD using the new decision orders.
+  // Note that this can keep the clause forever depending on the parameters.
+  //
+  // TODO(user): This cause one more hash lookup, probably not a big deal, but
+  // could be optimized away.
+  clauses_propagator_->ChangeLbdIfBetter(clause, ComputeLbd(clause->AsSpan()));
 }
 
 void SatSolver::RescaleClauseActivities(double scaling_factor) {
   SCOPED_TIME_STAT(&stats_);
   clause_activity_increment_ *= scaling_factor;
-  for (auto& entry : *clauses_propagator_->mutable_clauses_info()) {
-    entry.second.activity *= scaling_factor;
-  }
+  clauses_propagator_->RescaleClauseActivities(scaling_factor);
 }
 
 void SatSolver::UpdateClauseActivityIncrement() {
@@ -2157,9 +2136,7 @@ int SatSolver::ComputeLbd(absl::Span<const Literal> literals) {
     const SatDecisionLevel level(AssignmentLevel(literal.Variable()));
     DCHECK_GE(level, 0);
     num_at_max_level += (level == max_level) ? 1 : 0;
-    if (level > limit && !is_level_marked_[level]) {
-      is_level_marked_.Set(level);
-    }
+    if (level > limit) is_level_marked_.Set(level);
   }
 
   return is_level_marked_.NumberOfSetCallsWithDifferentArguments() +
@@ -2258,10 +2235,7 @@ void SatSolver::ProcessNewlyFixedVariables() {
     if (clause->IsRemoved()) continue;
 
     const size_t old_size = clause->size();
-    if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->Assignment())) {
-      // The clause is always true, detach it.
-      clauses_propagator_->LazyDelete(clause,
-                                      DeletionSourceForStat::FIXED_AT_TRUE);
+    if (clauses_propagator_->RemoveFixedLiteralsAndTestIfTrue(clause)) {
       ++num_detached_clauses;
       continue;
     }
@@ -3253,14 +3227,25 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
   std::vector<Entry> entries;
   auto& clauses_info = *(clauses_propagator_->mutable_clauses_info());
   for (auto& entry : clauses_info) {
+    entry.second.num_cleanup_rounds_since_last_bumped++;
     if (clauses_propagator_->ClauseIsUsedAsReason(entry.first)) continue;
-    if (entry.second.protected_during_next_cleanup) {
-      entry.second.protected_during_next_cleanup = false;
+
+    if (entry.second.lbd <= parameters_->clause_cleanup_lbd_tier1() &&
+        entry.second.num_cleanup_rounds_since_last_bumped <= 32) {
       continue;
     }
+
+    if (entry.second.lbd <= parameters_->clause_cleanup_lbd_tier2() &&
+        entry.second.num_cleanup_rounds_since_last_bumped <= 1) {
+      continue;
+    }
+
+    // The LBD should always have been updated to be <= size.
+    DCHECK_LE(entry.second.lbd, entry.first->size());
     entries.push_back(entry);
   }
-  const int num_protected_clauses = clauses_info.size() - entries.size();
+  const int num_protected_clauses =
+      clauses_propagator_->num_removable_clauses() - entries.size();
 
   if (parameters_->clause_cleanup_ordering() == SatParameters::CLAUSE_LBD) {
     // Order the clauses by decreasing LBD and then increasing activity.
diff --git a/ortools/sat/stat_tables.cc b/ortools/sat/stat_tables.cc
index 1853d7498c..35c79c8280 100644
--- a/ortools/sat/stat_tables.cc
+++ b/ortools/sat/stat_tables.cc
@@ -115,16 +115,17 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
   // Track reductions of Boolean variables.
   if (bool_var_table_.empty()) {
     bool_var_table_.push_back(
-        {"Boolean variables", "Fixed", "Equiv", "Total", "Left"});
+        {"Boolean variables", "Fixed", "Equiv", "Total", "Left", "Binary"});
   }
+  auto* binary = model->GetOrCreate<BinaryImplicationGraph>();
   const int64_t num_fixed = sat_solver->NumFixedVariables();
-  const int64_t num_equiv =
-      model->GetOrCreate<BinaryImplicationGraph>()->num_redundant_literals() /
-      2;
+  const int64_t num_equiv = binary->num_redundant_literals() / 2;
   const int64_t num_bools = sat_solver->NumVariables();
-  bool_var_table_.push_back({FormatName(name), FormatCounter(num_fixed),
-                             FormatCounter(num_equiv), FormatCounter(num_bools),
-                             FormatCounter(num_bools - num_equiv - num_fixed)});
+  bool_var_table_.push_back(
+      {FormatName(name), FormatCounter(num_fixed), FormatCounter(num_equiv),
+       FormatCounter(num_bools),
+       FormatCounter(num_bools - num_equiv - num_fixed),
+       FormatCounter(binary->ComputeNumImplicationsForLog())});
 
   // Track the "life of a non-binary clause".
   CpSolverResponse r;
@@ -134,7 +135,7 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
     clauses_deletion_table_.push_back(
         {"Clause deletion", "at_true", "l_and_not(l)", "to_binary",
          "sub_conflict", "sub_eager", "sub_vivify", "sub_probing", "sub_inpro",
-         "blocked", "eliminated", "forgotten", "#conflicts"});
+         "blocked", "eliminated", "forgotten", "promoted", "conflicts"});
   }
   absl::Span<const int64_t> deletion_by_source =
       model->GetOrCreate<ClauseManager>()->DeletionCounters();
@@ -162,6 +163,7 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
            DeletionSourceForStat::ELIMINATED)]),
        FormatCounter(deletion_by_source[static_cast<int>(
            DeletionSourceForStat::GARBAGE_COLLECTED)]),
+       FormatCounter(model->GetOrCreate<ClauseManager>()->num_lbd_promotions()),
        FormatCounter(r.num_conflicts())});
 }