diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel
index 1edd2c32eb..4b2bb11f07 100644
--- a/ortools/sat/BUILD.bazel
+++ b/ortools/sat/BUILD.bazel
@@ -1370,6 +1370,7 @@ cc_library(
         "//ortools/util:time_limit",
         "@com_google_absl//absl/container:btree",
         "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/log:log_streamer",
         "@com_google_absl//absl/numeric:int128",
         "@com_google_absl//absl/random",
         "@com_google_absl//absl/random:bit_gen_ref",
diff --git a/ortools/sat/all_different.cc b/ortools/sat/all_different.cc
index 10c28b6901..f75367ec8a 100644
--- a/ortools/sat/all_different.cc
+++ b/ortools/sat/all_different.cc
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "absl/container/btree_map.h"
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/graph/strongly_connected_components.h"
diff --git a/ortools/sat/all_different.h b/ortools/sat/all_different.h
index fcba62b584..6216f1a769 100644
--- a/ortools/sat/all_different.h
+++ b/ortools/sat/all_different.h
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/boolean_problem.cc b/ortools/sat/boolean_problem.cc
index f2f7fba38c..3030e47ae2 100644
--- a/ortools/sat/boolean_problem.cc
+++ b/ortools/sat/boolean_problem.cc
@@ -14,7 +14,6 @@
 #include "ortools/sat/boolean_problem.h"
 
 #include <algorithm>
-#include <cmath>
 #include <cstdint>
 #include <cstdlib>
 #include <limits>
@@ -26,6 +25,8 @@
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/flags/flag.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/status/status.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/string_view.h"
@@ -512,7 +513,7 @@ namespace {
 // GenerateGraphForSymmetryDetection().
 class IdGenerator {
  public:
-  IdGenerator() {}
+  IdGenerator() = default;
 
   // If the pair (type, coefficient) was never seen before, then generate
   // a new id, otherwise return the previously generated id.
@@ -716,10 +717,8 @@ void FindLinearBooleanProblemSymmetries(
                                       /*is_undirected=*/true);
   std::vector<int> factorized_automorphism_group_size;
   // TODO(user): inject the appropriate time limit here.
-  CHECK(symmetry_finder
-            .FindSymmetries(&equivalence_classes, generators,
-                            &factorized_automorphism_group_size)
-            .ok());
+  CHECK_OK(symmetry_finder.FindSymmetries(&equivalence_classes, generators,
+                                          &factorized_automorphism_group_size));
 
   // Remove from the permutations the part not concerning the literals.
   // Note that some permutation may becomes empty, which means that we had
diff --git a/ortools/sat/circuit.cc b/ortools/sat/circuit.cc
index 692dc8c929..56d70bd0ce 100644
--- a/ortools/sat/circuit.cc
+++ b/ortools/sat/circuit.cc
@@ -13,14 +13,16 @@
 
 #include "ortools/sat/circuit.h"
 
-#include <algorithm>
 #include <functional>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "ortools/base/logging.h"
+#include "ortools/graph/strongly_connected_components.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc
index 7c10402c27..6cdbae8c58 100644
--- a/ortools/sat/clause.cc
+++ b/ortools/sat/clause.cc
@@ -25,10 +25,10 @@
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/random/distributions.h"
 #include "absl/types/span.h"
-#include "ortools/base/hash.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/base/strong_vector.h"
diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h
index cac00a3382..15ad05988f 100644
--- a/ortools/sat/clause.h
+++ b/ortools/sat/clause.h
@@ -27,6 +27,7 @@
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/types/span.h"
 #include "ortools/base/hash.h"
@@ -69,8 +70,8 @@ class SatClause {
   int empty() const { return size_ == 0; }
 
   // Allows for range based iteration: for (Literal literal : clause) {}.
-  const Literal* const begin() const { return &(literals_[0]); }
-  const Literal* const end() const { return &(literals_[size_]); }
+  const Literal* begin() const { return &(literals_[0]); }
+  const Literal* end() const { return &(literals_[size_]); }
 
   // Returns the first and second literals. These are always the watched
   // literals if the clause is attached in the LiteralWatchers.
@@ -288,7 +289,7 @@ class LiteralWatchers : public SatPropagator {
   // Contains, for each literal, the list of clauses that need to be inspected
   // when the corresponding literal becomes false.
   struct Watcher {
-    Watcher() {}
+    Watcher() = default;
     Watcher(SatClause* c, Literal b, int i = 2)
         : blocking_literal(b), start_index(i), clause(c) {}
 
@@ -384,7 +385,7 @@ struct BinaryClause {
 // A simple class to manage a set of binary clauses.
 class BinaryClauseManager {
  public:
-  BinaryClauseManager() {}
+  BinaryClauseManager() = default;
   int NumClauses() const { return set_.size(); }
 
   // Adds a new binary clause to the manager and returns true if it wasn't
@@ -726,7 +727,7 @@ class BinaryImplicationGraph : public SatPropagator {
   // Same as ExpandAtMostOne() but try to maximize the weight in the clique.
   template <bool use_weight = true>
   std::vector<Literal> ExpandAtMostOneWithWeight(
-      const absl::Span<const Literal> at_most_one,
+      absl::Span<const Literal> at_most_one,
       const absl::StrongVector<LiteralIndex, bool>& can_be_included,
       const absl::StrongVector<LiteralIndex, double>& expanded_lp_values);
 
@@ -752,15 +753,14 @@ class BinaryImplicationGraph : public SatPropagator {
   // the underlying incompatibility graph. Note that there is no guarantee that
   // if this is called with any sub-clique of the result we will get the same
   // maximal clique.
-  std::vector<Literal> ExpandAtMostOne(
-      const absl::Span<const Literal> at_most_one,
-      int64_t max_num_explored_nodes);
+  std::vector<Literal> ExpandAtMostOne(absl::Span<const Literal> at_most_one,
+                                       int64_t max_num_explored_nodes);
 
   // Process all at most one constraints starting at or after base_index in
   // at_most_one_buffer_. This replace literal by their representative, remove
   // fixed literals and deal with duplicates. Return false iff the model is
   // UNSAT.
-  bool CleanUpAndAddAtMostOnes(const int base_index);
+  bool CleanUpAndAddAtMostOnes(int base_index);
 
   mutable StatsGroup stats_;
   TimeLimit* time_limit_;
diff --git a/ortools/sat/constraint_violation.cc b/ortools/sat/constraint_violation.cc
index 002af85a83..bb8f217115 100644
--- a/ortools/sat/constraint_violation.cc
+++ b/ortools/sat/constraint_violation.cc
@@ -17,6 +17,7 @@
 #include <cstdint>
 #include <cstdlib>
 #include <limits>
+#include <memory>
 #include <utility>
 #include <vector>
 
diff --git a/ortools/sat/cp_constraints.h b/ortools/sat/cp_constraints.h
index 114fd8da71..b9e21763ab 100644
--- a/ortools/sat/cp_constraints.h
+++ b/ortools/sat/cp_constraints.h
@@ -19,6 +19,7 @@
 #include <memory>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
@@ -71,11 +72,12 @@ class BooleanXorPropagator : public PropagatorInterface {
 // This constraint support duplicate selectors.
 class GreaterThanAtLeastOneOfPropagator : public PropagatorInterface {
  public:
-  GreaterThanAtLeastOneOfPropagator(
-      IntegerVariable target_var, const absl::Span<const IntegerVariable> vars,
-      const absl::Span<const IntegerValue> offsets,
-      const absl::Span<const Literal> selectors,
-      const absl::Span<const Literal> enforcements, Model* model);
+  GreaterThanAtLeastOneOfPropagator(IntegerVariable target_var,
+                                    absl::Span<const IntegerVariable> vars,
+                                    absl::Span<const IntegerValue> offsets,
+                                    absl::Span<const Literal> selectors,
+                                    absl::Span<const Literal> enforcements,
+                                    Model* model);
 
   bool Propagate() final;
   void RegisterWith(GenericLiteralWatcher* watcher);
diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc
index de16c62d61..d9a9646bb7 100644
--- a/ortools/sat/cp_model.cc
+++ b/ortools/sat/cp_model.cc
@@ -21,10 +21,10 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
 #include "absl/types/span.h"
-#include "ortools/base/logging.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/util/sorted_interval_list.h"
@@ -319,7 +319,7 @@ std::ostream& operator<<(std::ostream& os, const LinearExpr& e) {
   return os;
 }
 
-DoubleLinearExpr::DoubleLinearExpr() {}
+DoubleLinearExpr::DoubleLinearExpr() = default;
 
 DoubleLinearExpr::DoubleLinearExpr(BoolVar var) { AddTerm(var, 1); }
 
diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h
index d19e58f6aa..871a5d1540 100644
--- a/ortools/sat/cp_model.h
+++ b/ortools/sat/cp_model.h
@@ -292,7 +292,7 @@ class LinearExpr {
   const std::vector<int64_t>& coefficients() const { return coefficients_; }
 
   /// Returns true if the expression has no variables.
-  const bool IsConstant() const { return variables_.empty(); }
+  bool IsConstant() const { return variables_.empty(); }
 
   /// Returns the constant term.
   int64_t constant() const { return constant_; }
@@ -406,7 +406,7 @@ class DoubleLinearExpr {
   const std::vector<double>& coefficients() const { return coefficients_; }
 
   // Returns true if the expression has no variable.
-  const bool IsConstant() const { return variables_.empty(); }
+  bool IsConstant() const { return variables_.empty(); }
 
   /// Returns the constant term.
   double constant() const { return constant_; }
diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
index b758ac39ba..47fa3828d2 100644
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -16,7 +16,6 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <limits>
 #include <string>
 #include <utility>
@@ -25,8 +24,10 @@
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
+#include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/port/proto_utils.h"
 #include "ortools/sat/cp_model.pb.h"
diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc
index 8bdc8e8615..e689408def 100644
--- a/ortools/sat/cp_model_expand.cc
+++ b/ortools/sat/cp_model_expand.cc
@@ -23,8 +23,10 @@
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
-#include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stl_util.h"
diff --git a/ortools/sat/cp_model_expand.h b/ortools/sat/cp_model_expand.h
index f4c5d6e8ea..41bf286885 100644
--- a/ortools/sat/cp_model_expand.h
+++ b/ortools/sat/cp_model_expand.h
@@ -14,8 +14,11 @@
 #ifndef OR_TOOLS_SAT_CP_MODEL_EXPAND_H_
 #define OR_TOOLS_SAT_CP_MODEL_EXPAND_H_
 
+#include <stdint.h>
+
 #include <vector>
 
+#include "absl/container/flat_hash_set.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/presolve_context.h"
 
diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc
index 133137f094..2ccefd108c 100644
--- a/ortools/sat/cp_model_lns.cc
+++ b/ortools/sat/cp_model_lns.cc
@@ -16,10 +16,9 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <deque>
+#include <functional>
 #include <limits>
-#include <numeric>
 #include <random>
 #include <string>
 #include <tuple>
@@ -55,7 +54,6 @@
 #include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
-#include "ortools/util/time_limit.h"
 
 namespace operations_research {
 namespace sat {
diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h
index 11d89c20d1..dcc06f5b06 100644
--- a/ortools/sat/cp_model_lns.h
+++ b/ortools/sat/cp_model_lns.h
@@ -25,6 +25,7 @@
 #include "absl/base/thread_annotations.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/synchronization/mutex.h"
 #include "absl/time/time.h"
@@ -193,7 +194,7 @@ class NeighborhoodGeneratorHelper : public SubSolver {
   }
 
   // Returns all the constraints indices of a given type.
-  const absl::Span<const int> TypeToConstraints(
+  absl::Span<const int> TypeToConstraints(
       ConstraintProto::ConstraintCase type) const {
     if (type >= type_to_constraints_.size()) return {};
     return absl::MakeSpan(type_to_constraints_[type]);
@@ -324,7 +325,7 @@ class NeighborhoodGenerator {
   NeighborhoodGenerator(const std::string& name,
                         NeighborhoodGeneratorHelper const* helper)
       : name_(name), helper_(*helper), difficulty_(0.5) {}
-  virtual ~NeighborhoodGenerator() {}
+  virtual ~NeighborhoodGenerator() = default;
 
   // Generates a "local" subproblem for the given seed.
   //
@@ -529,7 +530,7 @@ class RelaxObjectiveVariablesGenerator : public NeighborhoodGenerator {
 // scheduling constraint, it adds strict relation order between the non-relaxed
 // intervals.
 Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals(
-    const absl::Span<const int> intervals_to_relax,
+    absl::Span<const int> intervals_to_relax,
     const CpSolverResponse& initial_solution, absl::BitGenRef random,
     const NeighborhoodGeneratorHelper& helper);
 
@@ -537,7 +538,7 @@ Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals(
 // full neighborhood enriched with the set or precedences passed to the generate
 // method.
 Neighborhood GenerateSchedulingNeighborhoodFromIntervalPrecedences(
-    const absl::Span<const std::pair<int, int>> precedences,
+    absl::Span<const std::pair<int, int>> precedences,
     const CpSolverResponse& initial_solution,
     const NeighborhoodGeneratorHelper& helper);
 
diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc
index 6043f86462..20ca8cfd12 100644
--- a/ortools/sat/cp_model_loader.cc
+++ b/ortools/sat/cp_model_loader.cc
@@ -16,7 +16,6 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <limits>
 #include <memory>
 #include <numeric>
@@ -28,6 +27,7 @@
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/sparse_permutation.h"
diff --git a/ortools/sat/cp_model_mapping.h b/ortools/sat/cp_model_mapping.h
index e92865f746..c26bfd363a 100644
--- a/ortools/sat/cp_model_mapping.h
+++ b/ortools/sat/cp_model_mapping.h
@@ -20,6 +20,7 @@
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/cp_model_objective.cc b/ortools/sat/cp_model_objective.cc
index f44c65b504..63151a3b30 100644
--- a/ortools/sat/cp_model_objective.cc
+++ b/ortools/sat/cp_model_objective.cc
@@ -17,7 +17,7 @@
 #include <cstdint>
 #include <cstdlib>
 
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/util/sorted_interval_list.h"
diff --git a/ortools/sat/cp_model_postsolve.cc b/ortools/sat/cp_model_postsolve.cc
index c8a962d45f..971fb4ebf9 100644
--- a/ortools/sat/cp_model_postsolve.cc
+++ b/ortools/sat/cp_model_postsolve.cc
@@ -18,6 +18,7 @@
 #include <limits>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
diff --git a/ortools/sat/cp_model_postsolve.h b/ortools/sat/cp_model_postsolve.h
index 1da224c39d..3089eeaed3 100644
--- a/ortools/sat/cp_model_postsolve.h
+++ b/ortools/sat/cp_model_postsolve.h
@@ -41,7 +41,7 @@ namespace sat {
 //
 // TODO(user): We could use the search strategy to fix free variables to some
 // chosen values? The feature might never be needed though.
-void PostsolveResponse(const int64_t num_variables_in_original_model,
+void PostsolveResponse(int64_t num_variables_in_original_model,
                        const CpModelProto& mapping_proto,
                        const std::vector<int>& postsolve_mapping,
                        std::vector<int64_t>* solution);
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index 340890d4c6..767c2bb54e 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -14,9 +14,11 @@
 #include "ortools/sat/cp_model_presolve.h"
 
 #include <algorithm>
+#include <array>
 #include <cstdint>
 #include <cstdlib>
 #include <deque>
+#include <functional>
 #include <limits>
 #include <numeric>
 #include <string>
@@ -31,14 +33,17 @@
 #include "absl/container/flat_hash_set.h"
 #include "absl/hash/hash.h"
 #include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/numeric/int128.h"
+#include "absl/status/statusor.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
+#include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/mathutil.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/base/timer.h"
-#include "ortools/base/vlog_is_on.h"
+#include "ortools/graph/strongly_connected_components.h"
 #include "ortools/graph/topologicalsorter.h"
 #include "ortools/sat/circuit.h"
 #include "ortools/sat/clause.h"
@@ -67,6 +72,7 @@
 #include "ortools/util/logging.h"
 #include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/sorted_interval_list.h"
+#include "ortools/util/strong_integers.h"
 #include "ortools/util/time_limit.h"
 
 namespace operations_research {
@@ -8773,6 +8779,17 @@ void CpModelPresolver::RemoveCommonPart(
   }
 }
 
+namespace {
+
+int64_t ComputeNonZeroReduction(size_t block_size, size_t common_part_size) {
+  // We replace the block by a column of new variable.
+  // But we also need to define this new variable.
+  return static_cast<int64_t>(block_size * (common_part_size - 1) -
+                              common_part_size - 1);
+}
+
+}  // namespace
+
 // This helps on neos-5045105-creuse.pb.gz for instance.
 void CpModelPresolver::FindBigVerticalLinearOverlap() {
   if (context_->time_limit()->LimitReached()) return;
@@ -8899,10 +8916,8 @@ void CpModelPresolver::FindBigVerticalLinearOverlap() {
     }
 
     // We have a candidate.
-    const int64_t saved_nz = block.size() * common_part.size()  // removed
-                             - block.size()  // replaced by new_var
-                             -
-                             (1 + common_part.size());  // new_var = common_part
+    const int64_t saved_nz =
+        ComputeNonZeroReduction(block.size(), common_part.size());
     if (saved_nz < 20) continue;
 
     // Fix multiples, currently this contain the coeff of x for each constraint.
@@ -8986,6 +9001,7 @@ void CpModelPresolver::FindBigHorizontalLinearOverlap() {
     std::vector<int> used_sorted_linear = {i};
     std::vector<std::pair<int, int64_t>> block = {{c, 1}};
     std::vector<std::pair<int, int64_t>> common_part;
+    std::vector<std::pair<int, int>> old_matches;
 
     for (int j = 0; j < sorted_linear.size(); ++j) {
       if (i == j) continue;
@@ -8995,7 +9011,8 @@ void CpModelPresolver::FindBigHorizontalLinearOverlap() {
 
       // No need to continue if linear is not large enough.
       const int num_terms = ct.linear().vars().size();
-      const int best_saved_nz = block.size() * (num_terms - 1) - 2;
+      const int best_saved_nz =
+          ComputeNonZeroReduction(block.size() + 1, num_terms);
       if (best_saved_nz <= saved_nz) break;
 
       work_done += num_terms;
@@ -9012,7 +9029,8 @@ void CpModelPresolver::FindBigHorizontalLinearOverlap() {
       // 2/ new_block_size variable
       // So new_block_size * common_size - common_size - 1 - new_block_size
       // which is (new_block_size - 1) * (common_size - 1) - 2;
-      const int64_t new_saved_nz = block.size() * (common_part.size() - 1) - 2;
+      const int64_t new_saved_nz =
+          ComputeNonZeroReduction(block.size() + 1, common_part.size());
       if (new_saved_nz > saved_nz) {
         saved_nz = new_saved_nz;
         used_sorted_linear.push_back(j);
@@ -9021,18 +9039,43 @@ void CpModelPresolver::FindBigHorizontalLinearOverlap() {
         for (const auto [var, coeff] : common_part) {
           coeff_map[var] = coeff;
         }
+      } else {
+        if (common_part.size() > 1) {
+          old_matches.push_back({j, common_part.size()});
+        }
       }
     }
 
     // Introduce a new variable = common_part.
     // Use it in all linear constraint.
-    //
-    // TODO(user): Given our heuristic above, it is maybe possible to extend
-    // this block vertically.
     if (block.size() > 1) {
       context_->UpdateRuleStats("linear matrix: common horizontal rectangle");
+
+      // Try to extend with exact matches that were skipped.
+      for (const auto [index, old_match_size] : old_matches) {
+        if (old_match_size < coeff_map.size()) continue;
+
+        int new_match_size = 0;
+        const int other_c = sorted_linear[index];
+        const ConstraintProto& ct =
+            context_->working_model->constraints(other_c);
+        const int num_terms = ct.linear().vars().size();
+        for (int k = 0; k < num_terms; ++k) {
+          const auto it = coeff_map.find(ct.linear().vars(k));
+          if (it != coeff_map.end() && it->second == ct.linear().coeffs(k)) {
+            ++new_match_size;
+          }
+        }
+        if (new_match_size == coeff_map.size()) {
+          context_->UpdateRuleStats(
+              "linear matrix: common horizontal rectangle extension");
+          used_sorted_linear.push_back(index);
+          block.push_back({other_c, 1});
+        }
+      }
+
       ++num_blocks;
-      nz_reduction += saved_nz;
+      nz_reduction += ComputeNonZeroReduction(block.size(), coeff_map.size());
       RemoveCommonPart(coeff_map, block);
       for (const int i : used_sorted_linear) sorted_linear[i] = -1;
     }
@@ -10957,8 +11000,8 @@ CpSolverStatus CpModelPresolver::Presolve() {
     DetectDominatedLinearConstraints();
     ProcessSetPPC();
     if (context_->params().find_big_linear_overlap()) {
-      FindBigVerticalLinearOverlap();
       FindBigHorizontalLinearOverlap();
+      FindBigVerticalLinearOverlap();
     }
     if (context_->ModelIsUnsat()) return InfeasibleStatus();
 
diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h
index 2f501693cc..c91130a9ba 100644
--- a/ortools/sat/cp_model_presolve.h
+++ b/ortools/sat/cp_model_presolve.h
@@ -27,6 +27,7 @@
 #include "ortools/sat/presolve_context.h"
 #include "ortools/sat/presolve_util.h"
 #include "ortools/sat/sat_parameters.pb.h"
+#include "ortools/sat/util.h"
 #include "ortools/util/affine_relation.h"
 #include "ortools/util/bitset.h"
 #include "ortools/util/logging.h"
@@ -220,7 +221,7 @@ class CpModelPresolver {
   void ExtractEnforcementLiteralFromLinearConstraint(int ct_index,
                                                      ConstraintProto* ct);
   void LowerThanCoeffStrengthening(bool from_lower_bound, int64_t min_magnitude,
-                                   int64_t threshold, ConstraintProto* ct);
+                                   int64_t rhs, ConstraintProto* ct);
 
   // Extracts cliques from bool_and and small at_most_one constraints and
   // transforms them into maximal cliques.
diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc
index 4c2b25c615..e5f9036aba 100644
--- a/ortools/sat/cp_model_search.cc
+++ b/ortools/sat/cp_model_search.cc
@@ -24,6 +24,7 @@
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/flags/flag.h"
+#include "absl/log/check.h"
 #include "absl/random/distributions.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/string_view.h"
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 06ea389abb..bd33c7a968 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -14,13 +14,14 @@
 #include "ortools/sat/cp_model_solver.h"
 
 #include <algorithm>
-#include <cmath>
+#include <atomic>
 #include <cstdint>
 #include <cstdlib>
 #include <deque>
 #include <functional>
 #include <limits>
 #include <memory>
+#include <new>
 #include <random>
 #include <string>
 #include <thread>
@@ -28,10 +29,8 @@
 #include <utility>
 #include <vector>
 
-#include "absl/log/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/timer.h"
-#include "ortools/sat/linear_model.h"
 #if !defined(__PORTABLE_PLATFORM__)
 #include "ortools/base/file.h"
 #include "ortools/base/helpers.h"
@@ -42,6 +41,9 @@
 #include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/flags/flag.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
+#include "absl/strings/escaping.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/str_join.h"
@@ -49,7 +51,10 @@
 #include "absl/strings/string_view.h"
 #include "absl/synchronization/mutex.h"
 #include "absl/types/span.h"
+#include "google/protobuf/text_format.h"
 #include "ortools/base/cleanup.h"
+#include "ortools/base/logging.h"
+#include "ortools/base/strong_vector.h"
 #include "ortools/graph/connected_components.h"
 #include "ortools/port/proto_utils.h"
 #include "ortools/sat/clause.h"
@@ -74,6 +79,7 @@
 #include "ortools/sat/integer_search.h"
 #include "ortools/sat/lb_tree_search.h"
 #include "ortools/sat/linear_constraint.h"
+#include "ortools/sat/linear_model.h"
 #include "ortools/sat/linear_programming_constraint.h"
 #include "ortools/sat/linear_relaxation.h"
 #include "ortools/sat/lp_utils.h"
diff --git a/ortools/sat/cp_model_symmetries.cc b/ortools/sat/cp_model_symmetries.cc
index cdfaf1cef3..edd11a9c11 100644
--- a/ortools/sat/cp_model_symmetries.cc
+++ b/ortools/sat/cp_model_symmetries.cc
@@ -17,6 +17,7 @@
 
 #include <algorithm>
 #include <cstdint>
+#include <functional>
 #include <limits>
 #include <memory>
 #include <utility>
@@ -24,6 +25,7 @@
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "absl/status/status.h"
 #include "absl/strings/str_cat.h"
@@ -65,7 +67,7 @@ struct VectorHash {
 // GenerateGraphForSymmetryDetection().
 class IdGenerator {
  public:
-  IdGenerator() {}
+  IdGenerator() = default;
 
   // If the color was never seen before, then generate a new id, otherwise
   // return the previously generated id.
diff --git a/ortools/sat/cp_model_utils.cc b/ortools/sat/cp_model_utils.cc
index deca2a6b44..d8ca28f27d 100644
--- a/ortools/sat/cp_model_utils.cc
+++ b/ortools/sat/cp_model_utils.cc
@@ -17,10 +17,15 @@
 #include <cstdlib>
 #include <functional>
 #include <string>
+#include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
+#include "absl/types/span.h"
+#include "google/protobuf/message.h"
+#include "google/protobuf/text_format.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/util/sorted_interval_list.h"
diff --git a/ortools/sat/cp_model_utils.h b/ortools/sat/cp_model_utils.h
index ff5dcd260f..3240ea1c8a 100644
--- a/ortools/sat/cp_model_utils.h
+++ b/ortools/sat/cp_model_utils.h
@@ -21,16 +21,18 @@
 #include <string>
 #include <vector>
 
-#include "absl/log/check.h"
-#include "absl/strings/match.h"
-#include "absl/types/span.h"
-#include "google/protobuf/text_format.h"
-#include "ortools/base/options.h"
 #if !defined(__PORTABLE_PLATFORM__)
 #include "ortools/base/helpers.h"
 #endif  // !defined(__PORTABLE_PLATFORM__)
+#include "absl/log/check.h"
+#include "absl/status/status.h"
+#include "absl/strings/match.h"
 #include "absl/strings/string_view.h"
+#include "absl/types/span.h"
+#include "google/protobuf/message.h"
+#include "google/protobuf/text_format.h"
 #include "ortools/base/hash.h"
+#include "ortools/base/options.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/util/sorted_interval_list.h"
 
diff --git a/ortools/sat/cumulative.cc b/ortools/sat/cumulative.cc
index 06adcdd061..14b30c79f8 100644
--- a/ortools/sat/cumulative.cc
+++ b/ortools/sat/cumulative.cc
@@ -17,6 +17,7 @@
 #include <functional>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/strings/str_join.h"
 #include "ortools/base/logging.h"
 #include "ortools/sat/cumulative_energy.h"
diff --git a/ortools/sat/cumulative_energy.cc b/ortools/sat/cumulative_energy.cc
index 9cb5a2206b..a90b72b49d 100644
--- a/ortools/sat/cumulative_energy.cc
+++ b/ortools/sat/cumulative_energy.cc
@@ -17,13 +17,13 @@
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/iterator_adaptors.h"
-#include "ortools/base/logging.h"
-#include "ortools/sat/implied_bounds.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/theta_tree.h"
+#include "ortools/sat/util.h"
 #include "ortools/util/strong_integers.h"
 
 namespace operations_research {
diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc
index 5456ddd447..faf39162c2 100644
--- a/ortools/sat/cuts.cc
+++ b/ortools/sat/cuts.cc
@@ -14,20 +14,23 @@
 #include "ortools/sat/cuts.h"
 
 #include <algorithm>
+#include <array>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <functional>
 #include <limits>
-#include <memory>
-#include <sstream>      // std::ostringstream
 #include <string>
 #include <utility>
 #include <vector>
 
+#include "absl/container/btree_map.h"
 #include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
+#include "absl/numeric/int128.h"
+#include "absl/strings/str_cat.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/base/strong_vector.h"
@@ -38,10 +41,10 @@
 #include "ortools/sat/linear_constraint_manager.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
+#include "ortools/sat/synchronization.h"
 #include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
-#include "ortools/util/time_limit.h"
 
 namespace absl {
 template <typename Sink>
diff --git a/ortools/sat/cuts.h b/ortools/sat/cuts.h
index fb8d32cc71..e03549e480 100644
--- a/ortools/sat/cuts.h
+++ b/ortools/sat/cuts.h
@@ -14,6 +14,8 @@
 #ifndef OR_TOOLS_SAT_CUTS_H_
 #define OR_TOOLS_SAT_CUTS_H_
 
+#include <stdint.h>
+
 #include <array>
 #include <functional>
 #include <limits>
@@ -21,8 +23,11 @@
 #include <utility>
 #include <vector>
 
+#include "absl/container/btree_map.h"
+#include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/numeric/int128.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/base/strong_vector.h"
diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc
index bdf0e4a4a7..0a451eae06 100644
--- a/ortools/sat/diffn.cc
+++ b/ortools/sat/diffn.cc
@@ -13,6 +13,8 @@
 
 #include "ortools/sat/diffn.h"
 
+#include <stddef.h>
+
 #include <algorithm>
 #include <cstdint>
 #include <limits>
@@ -20,6 +22,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/sat/cumulative_energy.h"
 #include "ortools/sat/diffn_util.h"
diff --git a/ortools/sat/diffn.h b/ortools/sat/diffn.h
index 3cbf847a25..6859da4ab1 100644
--- a/ortools/sat/diffn.h
+++ b/ortools/sat/diffn.h
@@ -25,6 +25,7 @@
 #include "ortools/sat/intervals.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
diff --git a/ortools/sat/diffn_util.cc b/ortools/sat/diffn_util.cc
index 8a8dd7e9d3..a3cb86922f 100644
--- a/ortools/sat/diffn_util.cc
+++ b/ortools/sat/diffn_util.cc
@@ -16,11 +16,11 @@
 #include <stddef.h>
 
 #include <algorithm>
-#include <ostream>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/diffn_util.h b/ortools/sat/diffn_util.h
index 8fe2367ddf..ad0bfba408 100644
--- a/ortools/sat/diffn_util.h
+++ b/ortools/sat/diffn_util.h
@@ -225,15 +225,13 @@ class CapacityProfile {
     EventType type;
     int index;
 
-    const bool operator<(const Event& other) const { return time < other.time; }
+    bool operator<(const Event& other) const { return time < other.time; }
   };
 
   // Element of the integer_pq heap.
   struct QueueElement {
     int Index() const { return index; }
-    const bool operator<(const QueueElement& o) const {
-      return value < o.value;
-    }
+    bool operator<(const QueueElement& o) const { return value < o.value; }
 
     int index;
     IntegerValue value;
diff --git a/ortools/sat/diophantine.cc b/ortools/sat/diophantine.cc
index fe0dca4828..78f8adc2bc 100644
--- a/ortools/sat/diophantine.cc
+++ b/ortools/sat/diophantine.cc
@@ -14,14 +14,15 @@
 #include "ortools/sat/diophantine.h"
 
 #include <algorithm>
-#include <cstddef>
 #include <cstdint>
 #include <cstdlib>
 #include <limits>
 #include <numeric>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/numeric/int128.h"
+#include "absl/types/span.h"
 #include "ortools/sat/util.h"
 
 namespace operations_research::sat {
diff --git a/ortools/sat/diophantine.h b/ortools/sat/diophantine.h
index 5841719a66..37f316db24 100644
--- a/ortools/sat/diophantine.h
+++ b/ortools/sat/diophantine.h
@@ -34,8 +34,7 @@ namespace operations_research::sat {
 // the end of the reduction, we have
 //     -floor(|P|/2) <= v < ceil(|P|/2).
 void ReduceModuloBasis(const std::vector<std::vector<absl::int128>>& basis,
-                       const int elements_to_consider,
-                       std::vector<absl::int128>& v);
+                       int elements_to_consider, std::vector<absl::int128>& v);
 
 // Returns an ordering of the indices of coefficients such that the GCD of its
 // initial segments decreases fast. As the product of the 15 smallest prime
diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc
index a8e9f71574..45c103863c 100644
--- a/ortools/sat/disjunctive.cc
+++ b/ortools/sat/disjunctive.cc
@@ -15,10 +15,9 @@
 
 #include <algorithm>
 #include <functional>
-#include <utility>
 #include <vector>
 
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
 #include "ortools/sat/all_different.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/integer_expr.h"
diff --git a/ortools/sat/drat_checker.cc b/ortools/sat/drat_checker.cc
index 6a1aae6393..3e3fc22ea4 100644
--- a/ortools/sat/drat_checker.cc
+++ b/ortools/sat/drat_checker.cc
@@ -16,16 +16,15 @@
 #include <stddef.h>
 
 #include <algorithm>
-#include <cmath>
 #include <cstdint>
 #include <cstdlib>
-#include <fstream>
+#include <fstream>  // NOLINT
 #include <limits>
 #include <string>
-#include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/strings/numbers.h"
 #include "absl/strings/str_split.h"
 #include "absl/strings/string_view.h"
diff --git a/ortools/sat/drat_checker.h b/ortools/sat/drat_checker.h
index 8f5f5e2ff4..4265adca97 100644
--- a/ortools/sat/drat_checker.h
+++ b/ortools/sat/drat_checker.h
@@ -14,6 +14,8 @@
 #ifndef OR_TOOLS_SAT_DRAT_CHECKER_H_
 #define OR_TOOLS_SAT_DRAT_CHECKER_H_
 
+#include <stddef.h>
+
 #include <cstdint>
 #include <limits>
 #include <memory>
@@ -44,7 +46,7 @@ const ClauseIndex kNoClauseIndex(-1);
 class DratChecker {
  public:
   DratChecker();
-  ~DratChecker() {}
+  ~DratChecker() = default;
 
   // Returns the number of Boolean variables used in the problem and infered
   // clauses.
@@ -162,15 +164,14 @@ class DratChecker {
   struct ClauseHash {
     DratChecker* checker;
     explicit ClauseHash(DratChecker* checker) : checker(checker) {}
-    std::size_t operator()(const ClauseIndex clause_index) const;
+    std::size_t operator()(ClauseIndex clause_index) const;
   };
 
   // Equality function for clauses.
   struct ClauseEquiv {
     DratChecker* checker;
     explicit ClauseEquiv(DratChecker* checker) : checker(checker) {}
-    bool operator()(const ClauseIndex clause_index1,
-                    const ClauseIndex clause_index2) const;
+    bool operator()(ClauseIndex clause_index1, ClauseIndex clause_index2) const;
   };
 
   // Adds a clause and returns its index.
diff --git a/ortools/sat/drat_proof_handler.cc b/ortools/sat/drat_proof_handler.cc
index bf0fb82847..935ad26b39 100644
--- a/ortools/sat/drat_proof_handler.cc
+++ b/ortools/sat/drat_proof_handler.cc
@@ -14,16 +14,13 @@
 #include "ortools/sat/drat_proof_handler.h"
 
 #include <algorithm>
-#include <cmath>
 #include <cstdlib>
 #include <memory>
-#include <utility>
 #include <vector>
-
-#include "ortools/base/logging.h"
 #if !defined(__PORTABLE_PLATFORM__)
 #include "ortools/base/file.h"
 #endif  // !defined(__PORTABLE_PLATFORM__)
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/drat_checker.h"
diff --git a/ortools/sat/drat_proof_handler.h b/ortools/sat/drat_proof_handler.h
index 7b05d821d2..4c3032aff5 100644
--- a/ortools/sat/drat_proof_handler.h
+++ b/ortools/sat/drat_proof_handler.h
@@ -49,7 +49,7 @@ class DratProofHandler {
   // store it in memory as well (in which case the proof can be checked with
   // Check() when it is complete).
   DratProofHandler(bool in_binary_format, File* output, bool check = false);
-  ~DratProofHandler() {}
+  ~DratProofHandler() = default;
 
   // During the presolve step, variable get deleted and the set of non-deleted
   // variable is remaped in a dense set. This allows to keep track of that and
diff --git a/ortools/sat/drat_writer.cc b/ortools/sat/drat_writer.cc
index 1d35261b11..43bfd55989 100644
--- a/ortools/sat/drat_writer.cc
+++ b/ortools/sat/drat_writer.cc
@@ -14,14 +14,12 @@
 #include "ortools/sat/drat_writer.h"
 
 #include <string>
-
-#include "ortools/base/logging.h"
 #if !defined(__PORTABLE_PLATFORM__)
 #include "ortools/base/file.h"
 #include "ortools/base/helpers.h"
 #include "ortools/base/options.h"
 #endif  // !__PORTABLE_PLATFORM__
-#include "absl/status/status.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_format.h"
 #include "absl/types/span.h"
 #include "ortools/sat/sat_base.h"
diff --git a/ortools/sat/encoding.cc b/ortools/sat/encoding.cc
index 28feb2e8c8..a8305973c3 100644
--- a/ortools/sat/encoding.cc
+++ b/ortools/sat/encoding.cc
@@ -13,15 +13,17 @@
 
 #include "ortools/sat/encoding.h"
 
+#include <stddef.h>
+
 #include <algorithm>
-#include <cstdint>
 #include <deque>
 #include <functional>
 #include <queue>
 #include <string>
 #include <vector>
 
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
+#include "absl/strings/str_cat.h"
 #include "ortools/sat/boolean_problem.pb.h"
 #include "ortools/sat/pb_constraint.h"
 #include "ortools/sat/sat_base.h"
diff --git a/ortools/sat/encoding.h b/ortools/sat/encoding.h
index 3126f6e76f..3501de150e 100644
--- a/ortools/sat/encoding.h
+++ b/ortools/sat/encoding.h
@@ -26,6 +26,7 @@
 #include <string>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/macros.h"
@@ -57,7 +58,7 @@ namespace sat {
 // Constraints", In Proc. of CP 2003, pages 108-122, 2003.
 class EncodingNode {
  public:
-  EncodingNode() {}
+  EncodingNode() = default;
 
   // Constructs a EncodingNode of size one, just formed by the given literal.
   explicit EncodingNode(Literal l);
diff --git a/ortools/sat/feasibility_jump.cc b/ortools/sat/feasibility_jump.cc
index c9b8917e8b..0612c72711 100644
--- a/ortools/sat/feasibility_jump.cc
+++ b/ortools/sat/feasibility_jump.cc
@@ -14,9 +14,9 @@
 #include "ortools/sat/feasibility_jump.h"
 
 #include <algorithm>
+#include <atomic>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <functional>
 #include <limits>
 #include <memory>
@@ -27,7 +27,6 @@
 #include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/random/distributions.h"
-#include "absl/random/random.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/binary_search.h"
@@ -37,11 +36,14 @@
 #include "ortools/sat/cp_model_checker.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/integer.h"
+#include "ortools/sat/linear_model.h"
 #include "ortools/sat/restart.h"
+#include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/subsolver.h"
 #include "ortools/sat/synchronization.h"
 #include "ortools/sat/util.h"
 #include "ortools/util/sorted_interval_list.h"
+#include "ortools/util/strong_integers.h"
 
 namespace operations_research::sat {
 
diff --git a/ortools/sat/feasibility_pump.cc b/ortools/sat/feasibility_pump.cc
index 9e336c36bc..11e7956ec1 100644
--- a/ortools/sat/feasibility_pump.cc
+++ b/ortools/sat/feasibility_pump.cc
@@ -16,12 +16,12 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <limits>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc
index f5d61bc077..52754402a1 100644
--- a/ortools/sat/implied_bounds.cc
+++ b/ortools/sat/implied_bounds.cc
@@ -13,27 +13,32 @@
 
 #include "ortools/sat/implied_bounds.h"
 
+#include <stddef.h>
 #include <stdint.h>
 
 #include <algorithm>
 #include <array>
 #include <bitset>
-#include <limits>
-#include <optional>
 #include <string>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
+#include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
+#include "ortools/sat/clause.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_constraint.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/bitset.h"
 #include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
diff --git a/ortools/sat/implied_bounds.h b/ortools/sat/implied_bounds.h
index 6c6ff9e63a..468adfdc2a 100644
--- a/ortools/sat/implied_bounds.h
+++ b/ortools/sat/implied_bounds.h
@@ -22,9 +22,12 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
+#include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
+#include "ortools/sat/clause.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_constraint.h"
 #include "ortools/sat/model.h"
diff --git a/ortools/sat/inclusion.h b/ortools/sat/inclusion.h
index ab3207156e..dca046534e 100644
--- a/ortools/sat/inclusion.h
+++ b/ortools/sat/inclusion.h
@@ -25,6 +25,7 @@
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
 
@@ -151,7 +152,7 @@ class InclusionDetector {
   // Function that should only be used from within "process()".
   // Returns the bitset corresponsing to the elements of the current superset
   // passed to the process() function.
-  const std::vector<bool> IsInSuperset() const { return is_in_superset_; }
+  std::vector<bool> IsInSuperset() const { return is_in_superset_; }
 
   // Function that should only be used from within "process()".
   // Stop will abort the current search. The other two will cause the
diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc
index add259b512..239cd2d852 100644
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -18,13 +18,16 @@
 #include <deque>
 #include <functional>
 #include <limits>
-#include <ostream>
 #include <string>
 #include <utility>
 #include <vector>
 
+#include "absl/base/attributes.h"
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h
index f9b02eb0ac..12c67f9615 100644
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -31,6 +31,7 @@
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/string_view.h"
 #include "absl/types/span.h"
@@ -250,7 +251,7 @@ using InlinedIntegerValueVector =
 // related constraints.
 struct AffineExpression {
   // Helper to construct an AffineExpression.
-  AffineExpression() {}
+  AffineExpression() = default;
   AffineExpression(IntegerValue cst)  // NOLINT(runtime/explicit)
       : constant(cst) {}
   AffineExpression(IntegerVariable v)  // NOLINT(runtime/explicit)
@@ -301,7 +302,7 @@ struct AffineExpression {
 
   bool IsConstant() const { return var == kNoIntegerVariable; }
 
-  const std::string DebugString() const {
+  std::string DebugString() const {
     if (var == kNoIntegerVariable) return absl::StrCat(constant.value());
     if (constant == 0) {
       return absl::StrCat("(", coeff.value(), " * X", var.value(), ")");
@@ -555,7 +556,7 @@ class IntegerEncoder {
   // given literal is true. Returns kNoIntegerVariable if such variable does not
   // exist. Note that one can create one by creating a new IntegerVariable and
   // calling AssociateToIntegerEqualValue().
-  const IntegerVariable GetLiteralView(Literal lit) const {
+  IntegerVariable GetLiteralView(Literal lit) const {
     if (lit.Index() >= literal_view_.size()) return kNoIntegerVariable;
     return literal_view_[lit.Index()];
   }
@@ -1274,8 +1275,8 @@ class IntegerTrail : public SatPropagator {
 // Base class for CP like propagators.
 class PropagatorInterface {
  public:
-  PropagatorInterface() {}
-  virtual ~PropagatorInterface() {}
+  PropagatorInterface() = default;
+  virtual ~PropagatorInterface() = default;
 
   // This will be called after one or more literals that are watched by this
   // propagator changed. It will also always be called on the first propagation
@@ -1323,7 +1324,7 @@ class RevIntegerValueRepository : public RevRepository<IntegerValue> {
 class GenericLiteralWatcher : public SatPropagator {
  public:
   explicit GenericLiteralWatcher(Model* model);
-  ~GenericLiteralWatcher() final {}
+  ~GenericLiteralWatcher() final = default;
 
   // Memory optimization: you can call this before registering watchers.
   void ReserveSpaceForNumVariables(int num_vars);
diff --git a/ortools/sat/integer_expr.cc b/ortools/sat/integer_expr.cc
index a54824dad0..9aa1e3234a 100644
--- a/ortools/sat/integer_expr.cc
+++ b/ortools/sat/integer_expr.cc
@@ -18,11 +18,12 @@
 #include <cstdlib>
 #include <functional>
 #include <limits>
-#include <type_traits>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
+#include "absl/numeric/int128.h"
 #include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
@@ -823,7 +824,7 @@ bool ProductPropagator::CanonicalizeCases() {
         p_.GreaterOrEqual(0), {a_.GreaterOrEqual(0), b_.GreaterOrEqual(0)});
   }
 
-  // Otherwise, make sure p is non-negative or across zero.
+  // Otherwise, make sure p is non-negative or accros zero.
   if (integer_trail_->UpperBound(p_) <= 0) {
     if (integer_trail_->LowerBound(a_) < 0) {
       DCHECK_GT(integer_trail_->UpperBound(a_), 0);
diff --git a/ortools/sat/integer_expr.h b/ortools/sat/integer_expr.h
index 022ef0eda7..c059a787ab 100644
--- a/ortools/sat/integer_expr.h
+++ b/ortools/sat/integer_expr.h
@@ -22,6 +22,7 @@
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
 #include "ortools/base/logging.h"
@@ -33,6 +34,7 @@
 #include "ortools/sat/model.h"
 #include "ortools/sat/precedences.h"
 #include "ortools/sat/sat_base.h"
+#include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/sat_solver.h"
 #include "ortools/util/rev.h"
 #include "ortools/util/strong_integers.h"
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index 7873546ff8..40802b833b 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -22,6 +22,8 @@
 
 #include "absl/container/flat_hash_set.h"
 #include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
+#include "absl/random/distributions.h"
 #include "absl/strings/str_cat.h"
 #include "absl/time/clock.h"
 #include "absl/time/time.h"
diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h
index e89dcce681..fb5d35bf7e 100644
--- a/ortools/sat/integer_search.h
+++ b/ortools/sat/integer_search.h
@@ -53,7 +53,7 @@ namespace sat {
 //
 // At most one of the two options should be set.
 struct BooleanOrIntegerLiteral {
-  BooleanOrIntegerLiteral() {}
+  BooleanOrIntegerLiteral() = default;
   explicit BooleanOrIntegerLiteral(LiteralIndex index)
       : boolean_literal_index(index) {}
   explicit BooleanOrIntegerLiteral(IntegerLiteral i_lit)
@@ -301,7 +301,7 @@ class ContinuousProber {
  private:
   bool ImportFromSharedClasses();
   SatSolver::Status ShaveLiteral(Literal literal);
-  bool ReportStatus(const SatSolver::Status status);
+  bool ReportStatus(SatSolver::Status status);
   void LogStatistics();
 
   // Variables to probe.
diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc
index 7dd6e4d784..e0a9b99a12 100644
--- a/ortools/sat/intervals.cc
+++ b/ortools/sat/intervals.cc
@@ -14,10 +14,15 @@
 #include "ortools/sat/intervals.h"
 
 #include <algorithm>
+#include <functional>
+#include <optional>
 #include <string>
 #include <utility>
 #include <vector>
 
+#include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h
index f52c25cd7d..befb92a0e5 100644
--- a/ortools/sat/intervals.h
+++ b/ortools/sat/intervals.h
@@ -21,11 +21,16 @@
 #include <vector>
 
 #include "absl/base/attributes.h"
+#include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
+#include "absl/strings/string_view.h"
+#include "absl/types/span.h"
 #include "ortools/base/macros.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/cp_constraints.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/integer_expr.h"
+#include "ortools/sat/linear_constraint.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/pb_constraint.h"
 #include "ortools/sat/precedences.h"
diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc
index 81bc68ba0e..2aa7886fb3 100644
--- a/ortools/sat/lb_tree_search.cc
+++ b/ortools/sat/lb_tree_search.cc
@@ -21,7 +21,7 @@
 #include <utility>
 #include <vector>
 
-#include "absl/random/distributions.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_cat.h"
 #include "absl/time/clock.h"
 #include "absl/time/time.h"
diff --git a/ortools/sat/linear_constraint.cc b/ortools/sat/linear_constraint.cc
index ba7e5bd428..e63ab4c5e0 100644
--- a/ortools/sat/linear_constraint.cc
+++ b/ortools/sat/linear_constraint.cc
@@ -16,7 +16,6 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <limits>
 #include <string>
 #include <utility>
@@ -24,8 +23,8 @@
 
 #include "absl/base/attributes.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_cat.h"
-#include "ortools/base/logging.h"
 #include "ortools/base/mathutil.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/integer.h"
diff --git a/ortools/sat/linear_constraint.h b/ortools/sat/linear_constraint.h
index 17cc412bd0..f135b95a47 100644
--- a/ortools/sat/linear_constraint.h
+++ b/ortools/sat/linear_constraint.h
@@ -44,7 +44,7 @@ struct LinearConstraint {
   std::vector<IntegerVariable> vars;
   std::vector<IntegerValue> coeffs;
 
-  LinearConstraint() {}
+  LinearConstraint() = default;
   LinearConstraint(IntegerValue _lb, IntegerValue _ub) : lb(_lb), ub(_ub) {}
 
   void AddTerm(IntegerVariable var, IntegerValue coeff) {
@@ -141,9 +141,8 @@ LinearExpression PositiveVarExpr(const LinearExpression& expr);
 // Returns the coefficient of the variable in the expression. Works in linear
 // time.
 // Note: GetCoefficient(NegationOf(var, expr)) == -GetCoefficient(var, expr).
-IntegerValue GetCoefficient(const IntegerVariable var,
-                            const LinearExpression& expr);
-IntegerValue GetCoefficientOfPositiveVar(const IntegerVariable var,
+IntegerValue GetCoefficient(IntegerVariable var, const LinearExpression& expr);
+IntegerValue GetCoefficientOfPositiveVar(IntegerVariable var,
                                          const LinearExpression& expr);
 
 // Allow to build a LinearConstraint while making sure there is no duplicate
diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc
index 3ff17185b2..87546fdd5a 100644
--- a/ortools/sat/linear_constraint_manager.cc
+++ b/ortools/sat/linear_constraint_manager.cc
@@ -13,27 +13,33 @@
 
 #include "ortools/sat/linear_constraint_manager.h"
 
+#include <stdint.h>
+
 #include <algorithm>
 #include <cmath>
 #include <cstddef>
-#include <cstdlib>
 #include <limits>
 #include <string>
 #include <utility>
 #include <vector>
 
+#include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
 #include "ortools/base/hash.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
+#include "ortools/glop/variables_info.h"
 #include "ortools/lp_data/lp_types.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_constraint.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/synchronization.h"
+#include "ortools/sat/util.h"
+#include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/strong_integers.h"
 #include "ortools/util/time_limit.h"
 
diff --git a/ortools/sat/linear_constraint_manager.h b/ortools/sat/linear_constraint_manager.h
index 61e89a6f9c..bac16a27f6 100644
--- a/ortools/sat/linear_constraint_manager.h
+++ b/ortools/sat/linear_constraint_manager.h
@@ -27,6 +27,8 @@
 #include "absl/strings/string_view.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/glop/revised_simplex.h"
+#include "ortools/glop/variables_info.h"
+#include "ortools/lp_data/lp_types.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_constraint.h"
 #include "ortools/sat/model.h"
diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc
index e600c51b6c..c86b4ebaa4 100644
--- a/ortools/sat/linear_programming_constraint.cc
+++ b/ortools/sat/linear_programming_constraint.cc
@@ -14,9 +14,9 @@
 #include "ortools/sat/linear_programming_constraint.h"
 
 #include <algorithm>
+#include <array>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <functional>
 #include <limits>
 #include <memory>
@@ -27,10 +27,8 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
-#include "absl/container/inlined_vector.h"
-#include "absl/meta/type_traits.h"
+#include "absl/log/check.h"
 #include "absl/numeric/int128.h"
-#include "absl/random/distributions.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/binary_search.h"
@@ -40,6 +38,7 @@
 #include "ortools/glop/parameters.pb.h"
 #include "ortools/glop/revised_simplex.h"
 #include "ortools/glop/status.h"
+#include "ortools/glop/variables_info.h"
 #include "ortools/lp_data/lp_data.h"
 #include "ortools/lp_data/lp_data_utils.h"
 #include "ortools/lp_data/lp_types.h"
@@ -55,6 +54,7 @@
 #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/sat/util.h"
 #include "ortools/sat/zero_half_cuts.h"
 #include "ortools/util/bitset.h"
diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h
index 54a4af875e..5aeb51eebb 100644
--- a/ortools/sat/linear_programming_constraint.h
+++ b/ortools/sat/linear_programming_constraint.h
@@ -23,11 +23,16 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/numeric/int128.h"
+#include "absl/types/span.h"
 #include "ortools/base/strong_vector.h"
+#include "ortools/glop/parameters.pb.h"
 #include "ortools/glop/revised_simplex.h"
+#include "ortools/glop/variables_info.h"
 #include "ortools/lp_data/lp_data.h"
 #include "ortools/lp_data/lp_data_utils.h"
 #include "ortools/lp_data/lp_types.h"
+#include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cuts.h"
 #include "ortools/sat/implied_bounds.h"
 #include "ortools/sat/integer.h"
diff --git a/ortools/sat/linear_propagation.cc b/ortools/sat/linear_propagation.cc
index 6836c391c5..c5154c0af1 100644
--- a/ortools/sat/linear_propagation.cc
+++ b/ortools/sat/linear_propagation.cc
@@ -13,6 +13,8 @@
 
 #include "ortools/sat/linear_propagation.h"
 
+#include <stdint.h>
+
 #include <algorithm>
 #include <functional>
 #include <limits>
@@ -21,6 +23,24 @@
 #include <utility>
 #include <vector>
 
+#include "absl/container/flat_hash_map.h"
+#include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
+#include "absl/numeric/int128.h"
+#include "absl/strings/str_cat.h"
+#include "absl/types/span.h"
+#include "ortools/base/logging.h"
+#include "ortools/base/stl_util.h"
+#include "ortools/base/strong_vector.h"
+#include "ortools/sat/integer.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_base.h"
+#include "ortools/sat/sat_solver.h"
+#include "ortools/sat/synchronization.h"
+#include "ortools/util/bitset.h"
+#include "ortools/util/strong_integers.h"
+#include "ortools/util/time_limit.h"
+
 namespace operations_research {
 namespace sat {
 
diff --git a/ortools/sat/linear_propagation.h b/ortools/sat/linear_propagation.h
index 2fccdce83e..447151bff1 100644
--- a/ortools/sat/linear_propagation.h
+++ b/ortools/sat/linear_propagation.h
@@ -14,6 +14,8 @@
 #ifndef OR_TOOLS_SAT_LINEAR_PROPAGATION_H_
 #define OR_TOOLS_SAT_LINEAR_PROPAGATION_H_
 
+#include <stdint.h>
+
 #include <deque>
 #include <functional>
 #include <ostream>
@@ -21,13 +23,20 @@
 #include <utility>
 #include <vector>
 
+#include "absl/base/attributes.h"
 #include "absl/container/inlined_vector.h"
+#include "absl/strings/string_view.h"
 #include "absl/types/span.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/integer.h"
+#include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"
 #include "ortools/sat/synchronization.h"
+#include "ortools/util/bitset.h"
+#include "ortools/util/rev.h"
+#include "ortools/util/strong_integers.h"
+#include "ortools/util/time_limit.h"
 
 namespace operations_research {
 namespace sat {
@@ -37,7 +46,7 @@ DEFINE_STRONG_INDEX_TYPE(EnforcementId);
 // A FIFO queue that allows some form of reordering of its element.
 class CustomFifoQueue {
  public:
-  CustomFifoQueue() {}
+  CustomFifoQueue() = default;
 
   // Note that this requires the queue to be empty or to never have been poped
   // before.
diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc
index ed5992332c..514718d3ec 100644
--- a/ortools/sat/linear_relaxation.cc
+++ b/ortools/sat/linear_relaxation.cc
@@ -25,6 +25,8 @@
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
+#include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/base/strong_vector.h"
@@ -1492,12 +1494,18 @@ void AddNoOverlap2dCutGenerator(const ConstraintProto& ct, Model* m,
       mapping->Intervals(ct.no_overlap_2d().x_intervals());
   std::vector<IntervalVariable> y_intervals =
       mapping->Intervals(ct.no_overlap_2d().y_intervals());
-  relaxation->cut_generators.push_back(
-      CreateNoOverlap2dCompletionTimeCutGenerator(x_intervals, y_intervals, m));
 
-  // Checks if at least one rectangle has a variable dimension or is optional.
   IntervalsRepository* intervals_repository =
       m->GetOrCreate<IntervalsRepository>();
+  SchedulingConstraintHelper* x_helper =
+      intervals_repository->GetOrCreateHelper(x_intervals);
+  SchedulingConstraintHelper* y_helper =
+      intervals_repository->GetOrCreateHelper(y_intervals);
+
+  relaxation->cut_generators.push_back(
+      CreateNoOverlap2dCompletionTimeCutGenerator(x_helper, y_helper, m));
+
+  // Checks if at least one rectangle has a variable dimension or is optional.
   bool has_variable_part = false;
   for (int i = 0; i < x_intervals.size(); ++i) {
     // Ignore absent rectangles.
@@ -1522,10 +1530,25 @@ void AddNoOverlap2dCutGenerator(const ConstraintProto& ct, Model* m,
       break;
     }
   }
-  if (has_variable_part) {
-    relaxation->cut_generators.push_back(
-        CreateNoOverlap2dEnergyCutGenerator(x_intervals, y_intervals, m));
+
+  if (!has_variable_part) return;
+
+  SchedulingDemandHelper* x_demands_helper =
+      new SchedulingDemandHelper(x_helper->Sizes(), y_helper, m);
+  m->TakeOwnership(x_demands_helper);
+  SchedulingDemandHelper* y_demands_helper =
+      new SchedulingDemandHelper(y_helper->Sizes(), x_helper, m);
+  m->TakeOwnership(y_demands_helper);
+
+  std::vector<std::vector<LiteralValueValue>> energies;
+  const int num_rectangles = x_helper->NumTasks();
+  for (int i = 0; i < num_rectangles; ++i) {
+    energies.push_back(
+        TryToDecomposeProduct(x_helper->Sizes()[i], y_helper->Sizes()[i], m));
   }
+
+  relaxation->cut_generators.push_back(CreateNoOverlap2dEnergyCutGenerator(
+      x_helper, y_helper, x_demands_helper, y_demands_helper, energies, m));
 }
 
 void AddLinMaxCutGenerator(const ConstraintProto& ct, Model* m,
diff --git a/ortools/sat/linear_relaxation.h b/ortools/sat/linear_relaxation.h
index ffdb256a83..d2e8e84fba 100644
--- a/ortools/sat/linear_relaxation.h
+++ b/ortools/sat/linear_relaxation.h
@@ -21,8 +21,10 @@
 #include "ortools/sat/cuts.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
+#include "ortools/sat/linear_constraint.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/presolve_util.h"
+#include "ortools/sat/sat_base.h"
 
 namespace operations_research {
 namespace sat {
diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc
index 4d828fcad1..8cd03dd842 100644
--- a/ortools/sat/lp_utils.cc
+++ b/ortools/sat/lp_utils.cc
@@ -16,13 +16,14 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <limits>
 #include <string>
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/strings/str_cat.h"
+#include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/glop/lp_solver.h"
@@ -38,6 +39,7 @@
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/util/fp_utils.h"
 #include "ortools/util/logging.h"
+#include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/strong_integers.h"
 
 namespace operations_research {
diff --git a/ortools/sat/lp_utils.h b/ortools/sat/lp_utils.h
index 8a072e8507..a1d8e3119d 100644
--- a/ortools/sat/lp_utils.h
+++ b/ortools/sat/lp_utils.h
@@ -166,7 +166,7 @@ bool ScaleAndSetObjective(const SatParameters& params,
 double ComputeTrueObjectiveLowerBound(
     const CpModelProto& model_proto_with_floating_point_objective,
     const CpObjectiveProto& integer_objective,
-    const int64_t inner_integer_objective_lower_bound);
+    int64_t inner_integer_objective_lower_bound);
 
 // Converts an integer program with only binary variables to a Boolean
 // optimization problem. Returns false if the problem didn't contains only
diff --git a/ortools/sat/max_hs.cc b/ortools/sat/max_hs.cc
index 5d3f0cc725..1821dba743 100644
--- a/ortools/sat/max_hs.cc
+++ b/ortools/sat/max_hs.cc
@@ -24,12 +24,14 @@
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
 #include "absl/flags/flag.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "absl/random/random.h"
 #include "absl/strings/string_view.h"
 #include "ortools/base/cleanup.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
+#include "ortools/sat/presolve_util.h"
 #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
 #include "ortools/linear_solver/linear_solver.h"
 #endif  // __PORTABLE_PLATFORM__
diff --git a/ortools/sat/model.h b/ortools/sat/model.h
index 1b3462b709..1b0c1bc310 100644
--- a/ortools/sat/model.h
+++ b/ortools/sat/model.h
@@ -25,6 +25,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/macros.h"
@@ -41,7 +42,7 @@ namespace sat {
  */
 class Model {
  public:
-  Model() {}
+  Model() = default;
 
   ~Model() {
     // The order of deletion seems to be platform dependent.
diff --git a/ortools/sat/opb_reader.h b/ortools/sat/opb_reader.h
index 0d35be3f22..f0afc604c6 100644
--- a/ortools/sat/opb_reader.h
+++ b/ortools/sat/opb_reader.h
@@ -20,6 +20,7 @@
 #include <string>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/strings/numbers.h"
 #include "absl/strings/str_split.h"
 #include "ortools/base/logging.h"
@@ -35,7 +36,7 @@ namespace sat {
 //   http://www.cril.univ-artois.fr/PB12/format.pdf
 class OpbReader {
  public:
-  OpbReader() {}
+  OpbReader() = default;
 
   // Loads the given opb filename into the given problem.
   bool Load(const std::string& filename, LinearBooleanProblem* problem) {
diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc
index 53edd0486c..eb454bd99c 100644
--- a/ortools/sat/optimization.cc
+++ b/ortools/sat/optimization.cc
@@ -16,7 +16,6 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <deque>
 #include <functional>
 #include <limits>
@@ -27,17 +26,21 @@
 #include "absl/container/btree_map.h"
 #include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/random/random.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
+#include "absl/types/span.h"
 #include "ortools/base/cleanup.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/macros.h"
 #include "ortools/base/stl_util.h"
+#include "ortools/base/strong_vector.h"
 #include "ortools/port/proto_utils.h"
 #include "ortools/sat/boolean_problem.h"
 #include "ortools/sat/boolean_problem.pb.h"
+#include "ortools/sat/clause.h"
 #include "ortools/sat/encoding.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/integer_expr.h"
@@ -49,6 +52,7 @@
 #include "ortools/sat/sat_solver.h"
 #include "ortools/sat/synchronization.h"
 #include "ortools/sat/util.h"
+#include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
 #include "ortools/util/time_limit.h"
 
@@ -138,7 +142,7 @@ void DeleteVectorIndices(const std::vector<int>& indices, Vector* v) {
 // Artificial Intelligence, 2013 - Elsevier.
 class FuMalikSymmetryBreaker {
  public:
-  FuMalikSymmetryBreaker() {}
+  FuMalikSymmetryBreaker() = default;
 
   // Must be called before a new core is processed.
   void StartResolvingNewCore(int new_core_index) {
diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h
index 5dfdbf2ca1..847a9a7fe0 100644
--- a/ortools/sat/optimization.h
+++ b/ortools/sat/optimization.h
@@ -19,6 +19,7 @@
 
 #include "absl/random/bit_gen_ref.h"
 #include "ortools/sat/boolean_problem.pb.h"
+#include "ortools/sat/clause.h"
 #include "ortools/sat/cp_model_mapping.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/integer_search.h"
diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc
index 84e28e7b95..04d2a78c1f 100644
--- a/ortools/sat/parameters_validation.cc
+++ b/ortools/sat/parameters_validation.cc
@@ -13,10 +13,11 @@
 
 #include "ortools/sat/parameters_validation.h"
 
+#include <stdint.h>
+
 #include <cmath>
 #include <limits>
 #include <string>
-#include <vector>
 
 #include "absl/container/flat_hash_set.h"
 #include "absl/strings/str_cat.h"
diff --git a/ortools/sat/pb_constraint.cc b/ortools/sat/pb_constraint.cc
index b14c9a574f..7d88265e0c 100644
--- a/ortools/sat/pb_constraint.cc
+++ b/ortools/sat/pb_constraint.cc
@@ -21,6 +21,7 @@
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/hash/hash.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_format.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/pb_constraint.h b/ortools/sat/pb_constraint.h
index 3a9a77eb66..100d14fd5e 100644
--- a/ortools/sat/pb_constraint.h
+++ b/ortools/sat/pb_constraint.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/strings/string_view.h"
 #include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
@@ -50,7 +51,7 @@ const Coefficient kCoefficientMax(
 
 // Represents a term in a pseudo-Boolean formula.
 struct LiteralWithCoeff {
-  LiteralWithCoeff() {}
+  LiteralWithCoeff() = default;
   LiteralWithCoeff(Literal l, Coefficient c) : literal(l), coefficient(c) {}
   LiteralWithCoeff(Literal l, int64_t c) : literal(l), coefficient(c) {}
   Literal literal;
@@ -150,7 +151,7 @@ void SimplifyCanonicalBooleanLinearConstraint(
 // symmetries of the associated graph that are not useful.
 class CanonicalBooleanLinearProblem {
  public:
-  CanonicalBooleanLinearProblem() {}
+  CanonicalBooleanLinearProblem() = default;
 
   // Adds a new constraint to the problem. The bounds are inclusive.
   // Returns false in case of a possible overflow or if the constraint is
@@ -163,7 +164,7 @@ class CanonicalBooleanLinearProblem {
 
   // Getters. All the constraints are guaranteed to be in canonical form.
   int NumConstraints() const { return constraints_.size(); }
-  const Coefficient Rhs(int i) const { return rhs_[i]; }
+  Coefficient Rhs(int i) const { return rhs_[i]; }
   const std::vector<LiteralWithCoeff>& Constraint(int i) const {
     return constraints_[i];
   }
@@ -638,7 +639,7 @@ class PbConstraints : public SatPropagator {
   // probably that the thresholds_ vector is a lot more efficient cache-wise.
   DEFINE_STRONG_INDEX_TYPE(ConstraintIndex);
   struct ConstraintIndexWithCoeff {
-    ConstraintIndexWithCoeff() {}  // Needed for vector.resize()
+    ConstraintIndexWithCoeff() = default;  // Needed for vector.resize()
     ConstraintIndexWithCoeff(bool n, ConstraintIndex i, Coefficient c)
         : need_untrail_inspection(n), index(i), coefficient(c) {}
     bool need_untrail_inspection;
diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc
index e64b2f1757..bbf8405269 100644
--- a/ortools/sat/precedences.cc
+++ b/ortools/sat/precedences.cc
@@ -13,6 +13,8 @@
 
 #include "ortools/sat/precedences.h"
 
+#include <stdint.h>
+
 #include <algorithm>
 #include <deque>
 #include <string>
@@ -20,7 +22,11 @@
 #include <vector>
 
 #include "absl/container/btree_set.h"
+#include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/types/span.h"
 #include "ortools/base/cleanup.h"
 #include "ortools/base/logging.h"
@@ -33,6 +39,7 @@
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"
+#include "ortools/sat/synchronization.h"
 #include "ortools/util/bitset.h"
 #include "ortools/util/strong_integers.h"
 #include "ortools/util/time_limit.h"
diff --git a/ortools/sat/precedences.h b/ortools/sat/precedences.h
index 1976e7f101..a05dc05c4d 100644
--- a/ortools/sat/precedences.h
+++ b/ortools/sat/precedences.h
@@ -174,7 +174,7 @@ class PrecedencesPropagator : public SatPropagator, PropagatorInterface {
   // least one of" type of constraints. Returns the number of such constraint
   // added.
   int AddGreaterThanAtLeastOneOfConstraintsFromClause(
-      const absl::Span<const Literal> clause, Model* model);
+      absl::Span<const Literal> clause, Model* model);
 
   // Another approach for AddGreaterThanAtLeastOneOfConstraints(), this one
   // might be a bit slow as it relies on the propagation engine to detect
diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc
index 819b29ff7b..4881c99de3 100644
--- a/ortools/sat/presolve_context.cc
+++ b/ortools/sat/presolve_context.cc
@@ -27,7 +27,9 @@
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
+#include "absl/numeric/int128.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/presolve_util.cc b/ortools/sat/presolve_util.cc
index c00ce5d743..6bf604b128 100644
--- a/ortools/sat/presolve_util.cc
+++ b/ortools/sat/presolve_util.cc
@@ -17,14 +17,16 @@
 #include <array>
 #include <cstdint>
 #include <cstdlib>
+#include <functional>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
-#include "absl/strings/str_join.h"
+#include "absl/random/distributions.h"
 #include "absl/types/span.h"
-#include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
diff --git a/ortools/sat/presolve_util.h b/ortools/sat/presolve_util.h
index 386a0cc08d..1bf1812b82 100644
--- a/ortools/sat/presolve_util.h
+++ b/ortools/sat/presolve_util.h
@@ -110,7 +110,7 @@ bool SubstituteVariable(int var, int64_t var_coeff_in_definition,
 // graph.
 class ActivityBoundHelper {
  public:
-  ActivityBoundHelper() {}
+  ActivityBoundHelper() = default;
 
   // The at most one constraint must be added before linear constraint are
   // processed. The functions below will still works, but do nothing more than
diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc
index 6acb66cda9..ea296254eb 100644
--- a/ortools/sat/probing.cc
+++ b/ortools/sat/probing.cc
@@ -15,10 +15,12 @@
 
 #include <algorithm>
 #include <cstdint>
+#include <functional>
 #include <utility>
 #include <vector>
 
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
diff --git a/ortools/sat/pseudo_costs.cc b/ortools/sat/pseudo_costs.cc
index 99fc4f1c22..0d17650d6d 100644
--- a/ortools/sat/pseudo_costs.cc
+++ b/ortools/sat/pseudo_costs.cc
@@ -15,9 +15,10 @@
 
 #include <algorithm>
 #include <limits>
+#include <tuple>
 #include <vector>
 
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/model.h"
diff --git a/ortools/sat/pseudo_costs.h b/ortools/sat/pseudo_costs.h
index ae951cffad..24ae7fd09d 100644
--- a/ortools/sat/pseudo_costs.h
+++ b/ortools/sat/pseudo_costs.h
@@ -16,6 +16,7 @@
 
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/integer.h"
diff --git a/ortools/sat/restart.h b/ortools/sat/restart.h
index bc74d23928..f4ae9af3d8 100644
--- a/ortools/sat/restart.h
+++ b/ortools/sat/restart.h
@@ -17,6 +17,7 @@
 #include <string>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_decision.h"
diff --git a/ortools/sat/rins.cc b/ortools/sat/rins.cc
index 89897bbc37..75f6240992 100644
--- a/ortools/sat/rins.cc
+++ b/ortools/sat/rins.cc
@@ -15,13 +15,12 @@
 
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <limits>
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/random/bit_gen_ref.h"
-#include "ortools/base/logging.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_programming_constraint.h"
 #include "ortools/sat/model.h"
diff --git a/ortools/sat/routing_cuts.cc b/ortools/sat/routing_cuts.cc
index 284f1b5b44..a2f62b87c6 100644
--- a/ortools/sat/routing_cuts.cc
+++ b/ortools/sat/routing_cuts.cc
@@ -20,10 +20,20 @@
 #include <utility>
 #include <vector>
 
+#include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
+#include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/mathutil.h"
+#include "ortools/base/strong_vector.h"
+#include "ortools/sat/cuts.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_constraint.h"
+#include "ortools/sat/linear_constraint_manager.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_base.h"
+#include "ortools/sat/util.h"
+#include "ortools/util/strong_integers.h"
 
 namespace operations_research {
 namespace sat {
diff --git a/ortools/sat/routing_cuts.h b/ortools/sat/routing_cuts.h
index d5bc8fff4b..812703e345 100644
--- a/ortools/sat/routing_cuts.h
+++ b/ortools/sat/routing_cuts.h
@@ -14,15 +14,19 @@
 #ifndef OR_TOOLS_SAT_ROUTING_CUTS_H_
 #define OR_TOOLS_SAT_ROUTING_CUTS_H_
 
+#include <stdint.h>
+
 #include <functional>
 #include <optional>
 #include <utility>
 #include <vector>
 
+#include "absl/types/span.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cuts.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/model.h"
+#include "ortools/sat/sat_base.h"
 
 namespace operations_research {
 namespace sat {
diff --git a/ortools/sat/sat_base.h b/ortools/sat/sat_base.h
index 11b70ce963..e28028025c 100644
--- a/ortools/sat/sat_base.h
+++ b/ortools/sat/sat_base.h
@@ -27,6 +27,7 @@
 #include <vector>
 
 #include "absl/base/attributes.h"
+#include "absl/log/check.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/string_view.h"
 #include "absl/types/span.h"
@@ -77,7 +78,7 @@ class Literal {
     CHECK_NE(signed_value, 0);
   }
 
-  Literal() {}
+  Literal() = default;
   explicit Literal(LiteralIndex index) : index_(index.value()) {}
   Literal(BooleanVariable variable, bool is_positive)
       : index_(is_positive ? (variable.value() << 1)
@@ -135,7 +136,7 @@ inline std::ostream& operator<<(std::ostream& os,
 // Each variable can be unassigned or be assigned to true or false.
 class VariablesAssignment {
  public:
-  VariablesAssignment() {}
+  VariablesAssignment() = default;
   explicit VariablesAssignment(int num_variables) { Resize(num_variables); }
   void Resize(int num_variables) {
     assignment_.Resize(LiteralIndex(num_variables << 1));
@@ -395,7 +396,7 @@ class Trail {
   int Index() const { return current_info_.trail_index; }
   // This accessor can return trail_.end(). operator[] cannot. This allows
   // normal std:vector operations, such as assign(begin, end).
-  const std::vector<Literal>::const_iterator IteratorAt(int index) const {
+  std::vector<Literal>::const_iterator IteratorAt(int index) const {
     return trail_.begin() + index;
   }
   const Literal& operator[](int index) const { return trail_[index]; }
@@ -476,7 +477,7 @@ class SatPropagator {
  public:
   explicit SatPropagator(const std::string& name)
       : name_(name), propagator_id_(-1), propagation_trail_index_(0) {}
-  virtual ~SatPropagator() {}
+  virtual ~SatPropagator() = default;
 
   // Sets/Gets this propagator unique id.
   void SetPropagatorId(int id) { propagator_id_ = id; }
diff --git a/ortools/sat/sat_cnf_reader.h b/ortools/sat/sat_cnf_reader.h
index a2e0302310..9db7fe88be 100644
--- a/ortools/sat/sat_cnf_reader.h
+++ b/ortools/sat/sat_cnf_reader.h
@@ -22,6 +22,7 @@
 
 #include "absl/container/btree_map.h"
 #include "absl/flags/flag.h"
+#include "absl/log/check.h"
 #include "absl/strings/numbers.h"
 #include "absl/strings/str_split.h"
 #include "absl/strings/string_view.h"
diff --git a/ortools/sat/sat_decision.cc b/ortools/sat/sat_decision.cc
index f7cb2a9b91..767b10ef3c 100644
--- a/ortools/sat/sat_decision.cc
+++ b/ortools/sat/sat_decision.cc
@@ -19,6 +19,7 @@
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/model.h"
@@ -301,7 +302,7 @@ void SatDecisionPolicy::UpdateWeightedSign(
 }
 
 void SatDecisionPolicy::BumpVariableActivities(
-    const std::vector<Literal>& literals) {
+    absl::Span<const Literal> literals) {
   if (parameters_.use_erwa_heuristic()) {
     if (num_bumps_.size() != activities_.size()) {
       num_bumps_.resize(activities_.size(), 0);
diff --git a/ortools/sat/sat_decision.h b/ortools/sat/sat_decision.h
index dd5abeab1c..9324b4dd7c 100644
--- a/ortools/sat/sat_decision.h
+++ b/ortools/sat/sat_decision.h
@@ -27,6 +27,7 @@
 #include "ortools/sat/util.h"
 #include "ortools/util/bitset.h"
 #include "ortools/util/integer_pq.h"
+#include "ortools/util/strong_integers.h"
 
 namespace operations_research {
 namespace sat {
@@ -62,7 +63,7 @@ class SatDecisionPolicy {
   // must be currently assigned. See VSIDS decision heuristic: Chaff:
   // Engineering an Efficient SAT Solver. M.W. Moskewicz et al. ANNUAL ACM IEEE
   // DESIGN AUTOMATION CONFERENCE 2001.
-  void BumpVariableActivities(const std::vector<Literal>& literals);
+  void BumpVariableActivities(absl::Span<const Literal> literals);
 
   // Updates the increment used for activity bumps. This is basically the same
   // as decaying all the variable activities, but it is a lot more efficient.
diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc
index 5ac578be4c..00f1c2a9f8 100644
--- a/ortools/sat/sat_inprocessing.cc
+++ b/ortools/sat/sat_inprocessing.cc
@@ -18,10 +18,10 @@
 #include <cstdint>
 #include <deque>
 #include <limits>
-#include <utility>
 #include <vector>
 
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
 #include "absl/random/distributions.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/sat_runner.cc b/ortools/sat/sat_runner.cc
index 1e87bda43a..7179253350 100644
--- a/ortools/sat/sat_runner.cc
+++ b/ortools/sat/sat_runner.cc
@@ -20,6 +20,7 @@
 
 #include "absl/flags/flag.h"
 #include "absl/flags/usage.h"
+#include "absl/log/check.h"
 #include "absl/log/flags.h"
 #include "absl/log/initialize.h"
 #include "absl/random/random.h"
@@ -29,8 +30,10 @@
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/string_view.h"
+#include "google/protobuf/text_format.h"
 #include "ortools/algorithms/sparse_permutation.h"
 #include "ortools/base/helpers.h"
+#include "ortools/base/logging.h"
 #include "ortools/base/options.h"
 #include "ortools/base/timer.h"
 #include "ortools/linear_solver/linear_solver.pb.h"
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index d3ecf95e42..3363dff82a 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -26,6 +26,7 @@
 #include "absl/base/attributes.h"
 #include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h
index b7ec7e17d0..330e3a01d8 100644
--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -29,6 +29,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/log/check.h"
 #include "absl/strings/string_view.h"
 #include "absl/types/span.h"
 #include "ortools/base/hash.h"
@@ -374,7 +375,7 @@ class SatSolver {
   void ClearNewlyAddedBinaryClauses();
 
   struct Decision {
-    Decision() {}
+    Decision() = default;
     Decision(int i, Literal l) : trail_index(i), literal(l) {}
     int trail_index = 0;
     Literal literal;
@@ -492,7 +493,7 @@ class SatSolver {
   bool ClauseIsValidUnderDebugAssignment(
       const std::vector<Literal>& clause) const;
   bool PBConstraintIsValidUnderDebugAssignment(
-      const std::vector<LiteralWithCoeff>& cst, const Coefficient rhs) const;
+      const std::vector<LiteralWithCoeff>& cst, Coefficient rhs) const;
 
   // Logs the given status if parameters_.log_search_progress() is true.
   // Also returns it.
diff --git a/ortools/sat/scheduling_cuts.cc b/ortools/sat/scheduling_cuts.cc
index eb436d5110..4d89f31d0f 100644
--- a/ortools/sat/scheduling_cuts.cc
+++ b/ortools/sat/scheduling_cuts.cc
@@ -13,21 +13,23 @@
 
 #include "ortools/sat/scheduling_cuts.h"
 
+#include <stdint.h>
+
 #include <algorithm>
 #include <cmath>
-#include <cstdlib>
 #include <functional>
 #include <limits>
-#include <numeric>
 #include <optional>
 #include <string>
 #include <tuple>
 #include <utility>
 #include <vector>
 
+#include "absl/base/attributes.h"
+#include "absl/container/btree_set.h"
+#include "absl/container/flat_hash_map.h"
 #include "absl/log/check.h"
 #include "absl/strings/str_cat.h"
-#include "absl/strings/str_join.h"
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/stl_util.h"
@@ -42,7 +44,10 @@
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/util.h"
+#include "ortools/util/saturated_arithmetic.h"
+#include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
+#include "ortools/util/time_limit.h"
 
 namespace operations_research {
 namespace sat {
@@ -912,33 +917,16 @@ void GenerateNoOverlap2dEnergyCut(
 }
 
 CutGenerator CreateNoOverlap2dEnergyCutGenerator(
-    const std::vector<IntervalVariable>& x_intervals,
-    const std::vector<IntervalVariable>& y_intervals, Model* model) {
-  SchedulingConstraintHelper* x_helper =
-      model->GetOrCreate<IntervalsRepository>()->GetOrCreateHelper(x_intervals);
-  SchedulingConstraintHelper* y_helper =
-      model->GetOrCreate<IntervalsRepository>()->GetOrCreateHelper(y_intervals);
-
+    SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper,
+    SchedulingDemandHelper* x_demands_helper,
+    SchedulingDemandHelper* y_demands_helper,
+    const std::vector<std::vector<LiteralValueValue>>& energies, Model* model) {
   CutGenerator result;
   result.only_run_at_level_zero = true;
   AddIntegerVariableFromIntervals(x_helper, model, &result.vars);
   AddIntegerVariableFromIntervals(y_helper, model, &result.vars);
   gtl::STLSortAndRemoveDuplicates(&result.vars);
 
-  SchedulingDemandHelper* x_demands_helper =
-      new SchedulingDemandHelper(x_helper->Sizes(), y_helper, model);
-  model->TakeOwnership(x_demands_helper);
-  SchedulingDemandHelper* y_demands_helper =
-      new SchedulingDemandHelper(y_helper->Sizes(), x_helper, model);
-  model->TakeOwnership(y_demands_helper);
-
-  std::vector<std::vector<LiteralValueValue>> energies;
-  const int num_rectangles = x_intervals.size();
-  for (int i = 0; i < num_rectangles; ++i) {
-    energies.push_back(TryToDecomposeProduct(x_helper->Sizes()[i],
-                                             y_helper->Sizes()[i], model));
-  }
-
   result.generate_cuts =
       [x_helper, y_helper, x_demands_helper, y_demands_helper, model, energies](
           const absl::StrongVector<IntegerVariable, double>& lp_values,
@@ -1016,9 +1004,8 @@ CutGenerator CreateCumulativeTimeTableCutGenerator(
     bool is_optional = false;
   };
 
-  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
   result.generate_cuts =
-      [helper, capacity, demands_helper, integer_trail, model](
+      [helper, capacity, demands_helper, model](
           const absl::StrongVector<IntegerVariable, double>& lp_values,
           LinearConstraintManager* manager) {
         if (!helper->SynchronizeAndSetTimeDirection(true)) return false;
@@ -1578,7 +1565,7 @@ void GenerateShortCompletionTimeCutsWithExactBound(
 // The original cut is:
 //    sum(end_min_i * duration_min_i) >=
 //        (sum(duration_min_i^2) + sum(duration_min_i)^2) / 2
-// We strenghten this cuts by noticing that if all tasks starts after S,
+// We strengthen this cuts by noticing that if all tasks starts after S,
 // then replacing end_min_i by (end_min_i - S) is still valid.
 //
 // A second difference is that we look at a set of intervals starting
@@ -1849,13 +1836,8 @@ CutGenerator CreateCumulativeCompletionTimeCutGenerator(
 
 // TODO(user): Use demands_helper and decomposed energy.
 CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator(
-    const std::vector<IntervalVariable>& x_intervals,
-    const std::vector<IntervalVariable>& y_intervals, Model* model) {
-  SchedulingConstraintHelper* x_helper =
-      model->GetOrCreate<IntervalsRepository>()->GetOrCreateHelper(x_intervals);
-  SchedulingConstraintHelper* y_helper =
-      model->GetOrCreate<IntervalsRepository>()->GetOrCreateHelper(y_intervals);
-
+    SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper,
+    Model* model) {
   CutGenerator result;
   result.only_run_at_level_zero = true;
   AddIntegerVariableFromIntervals(x_helper, model, &result.vars);
@@ -1902,8 +1884,7 @@ CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator(
         for (absl::Span<int> rectangles : components) {
           if (rectangles.size() <= 1) continue;
 
-          auto generate_cuts = [&lp_values, model, manager, &rectangles,
-                                &cached_areas](
+          auto generate_cuts = [&lp_values, model, manager, &rectangles](
                                    const std::string& cut_name,
                                    SchedulingConstraintHelper* x_helper,
                                    SchedulingConstraintHelper* y_helper) {
diff --git a/ortools/sat/scheduling_cuts.h b/ortools/sat/scheduling_cuts.h
index ba9528c999..f181fe6a68 100644
--- a/ortools/sat/scheduling_cuts.h
+++ b/ortools/sat/scheduling_cuts.h
@@ -23,6 +23,7 @@
 #include "ortools/sat/cuts.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
+#include "ortools/sat/model.h"
 
 namespace operations_research {
 namespace sat {
@@ -76,8 +77,8 @@ CutGenerator CreateCumulativePrecedenceCutGenerator(
 // Completion time cuts for the no_overlap_2d constraint. It actually generates
 // the completion time cumulative cuts in both axis.
 CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator(
-    const std::vector<IntervalVariable>& x_intervals,
-    const std::vector<IntervalVariable>& y_intervals, Model* model);
+    SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper,
+    Model* model);
 
 // Energetic cuts for the no_overlap_2d constraint.
 //
@@ -94,8 +95,10 @@ CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator(
 // The maximum area is the area of the bounding rectangle of each intervals
 // at level 0.
 CutGenerator CreateNoOverlap2dEnergyCutGenerator(
-    const std::vector<IntervalVariable>& x_intervals,
-    const std::vector<IntervalVariable>& y_intervals, Model* model);
+    SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper,
+    SchedulingDemandHelper* x_demands_helper,
+    SchedulingDemandHelper* y_demands_helper,
+    const std::vector<std::vector<LiteralValueValue>>& energies, Model* model);
 
 // For a given set of intervals, we first compute the min and max of all
 // intervals. Then we create a cut that indicates that all intervals must fit
diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc
index e1e4d7b1ca..36e9c1e1c6 100644
--- a/ortools/sat/simplification.cc
+++ b/ortools/sat/simplification.cc
@@ -21,6 +21,8 @@
 #include <utility>
 #include <vector>
 
+#include "absl/container/btree_set.h"
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/dynamic_partition.h"
 #include "ortools/base/adjustable_priority_queue-inl.h"
diff --git a/ortools/sat/simplification.h b/ortools/sat/simplification.h
index 37171f1316..fdce601688 100644
--- a/ortools/sat/simplification.h
+++ b/ortools/sat/simplification.h
@@ -54,7 +54,7 @@ class SatPostsolver {
   // The postsolver will process the Add() calls in reverse order. If the given
   // clause has all its literals at false, it simply sets the literal x to true.
   // Note that x must be a literal of the given clause.
-  void Add(Literal x, const absl::Span<const Literal> clause);
+  void Add(Literal x, absl::Span<const Literal> clause);
 
   // Tells the postsolver that the given literal must be true in any solution.
   // We currently check that the variable is not already fixed.
diff --git a/ortools/sat/subsolver.cc b/ortools/sat/subsolver.cc
index 3bc1eba85d..d46f02e235 100644
--- a/ortools/sat/subsolver.cc
+++ b/ortools/sat/subsolver.cc
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "absl/flags/flag.h"
+#include "absl/log/check.h"
 #include "absl/strings/string_view.h"
 #include "absl/synchronization/blocking_counter.h"
 #include "absl/synchronization/mutex.h"
diff --git a/ortools/sat/subsolver.h b/ortools/sat/subsolver.h
index 945b54fa51..0f0fb5892d 100644
--- a/ortools/sat/subsolver.h
+++ b/ortools/sat/subsolver.h
@@ -46,7 +46,7 @@ class SubSolver {
 
   SubSolver(const std::string& name, SubsolverType type)
       : name_(name), type_(type) {}
-  virtual ~SubSolver() {}
+  virtual ~SubSolver() = default;
 
   // Synchronizes with the external world from this SubSolver point of view.
   // Also incorporate the results of the latest completed tasks if any.
diff --git a/ortools/sat/swig_helper.cc b/ortools/sat/swig_helper.cc
index 3d4bbb0691..faa6f66506 100644
--- a/ortools/sat/swig_helper.cc
+++ b/ortools/sat/swig_helper.cc
@@ -13,16 +13,27 @@
 
 #include "ortools/sat/swig_helper.h"
 
+#include <stdint.h>
+
 #include <atomic>
 #include <functional>
 #include <string>
 
 #include "ortools/base/logging.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_checker.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+#include "ortools/util/logging.h"
+#include "ortools/util/sorted_interval_list.h"
+#include "ortools/util/time_limit.h"
 
 namespace operations_research {
 namespace sat {
 
-SolutionCallback::~SolutionCallback() {}
+SolutionCallback::~SolutionCallback() = default;
 
 void SolutionCallback::Run(
     const operations_research::sat::CpSolverResponse& response) const {
diff --git a/ortools/sat/swig_helper.h b/ortools/sat/swig_helper.h
index c0e50f171c..fb154bd407 100644
--- a/ortools/sat/swig_helper.h
+++ b/ortools/sat/swig_helper.h
@@ -85,7 +85,7 @@ class SolutionCallback {
 // Simple director class for C#.
 class LogCallback {
  public:
-  virtual ~LogCallback() {}
+  virtual ~LogCallback() = default;
   virtual void NewMessage(const std::string& message) = 0;
 };
 
diff --git a/ortools/sat/symmetry.cc b/ortools/sat/symmetry.cc
index 71543ee2ff..fb7a6eac52 100644
--- a/ortools/sat/symmetry.cc
+++ b/ortools/sat/symmetry.cc
@@ -16,9 +16,9 @@
 #include <memory>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/sparse_permutation.h"
-#include "ortools/base/logging.h"
 #include "ortools/base/strong_vector.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/util/stats.h"
diff --git a/ortools/sat/symmetry_util.cc b/ortools/sat/symmetry_util.cc
index 86b26dea6a..1803ecd222 100644
--- a/ortools/sat/symmetry_util.cc
+++ b/ortools/sat/symmetry_util.cc
@@ -18,6 +18,7 @@
 #include <memory>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/algorithms/dynamic_partition.h"
 #include "ortools/algorithms/sparse_permutation.h"
 #include "ortools/base/logging.h"
diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc
index cceb2f0bd4..49163b504c 100644
--- a/ortools/sat/synchronization.cc
+++ b/ortools/sat/synchronization.cc
@@ -14,10 +14,10 @@
 #include "ortools/sat/synchronization.h"
 
 #include <algorithm>
+#include <atomic>
 #include <cctype>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <deque>
 #include <functional>
 #include <limits>
diff --git a/ortools/sat/table.cc b/ortools/sat/table.cc
index 43ed8a8708..f0d8721d07 100644
--- a/ortools/sat/table.cc
+++ b/ortools/sat/table.cc
@@ -18,7 +18,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"
diff --git a/ortools/sat/theta_tree.cc b/ortools/sat/theta_tree.cc
index 87bb756daa..65243b77a0 100644
--- a/ortools/sat/theta_tree.cc
+++ b/ortools/sat/theta_tree.cc
@@ -16,14 +16,14 @@
 #include <algorithm>
 #include <cstdint>
 
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
 #include "ortools/sat/integer.h"
 
 namespace operations_research {
 namespace sat {
 
 template <typename IntegerType>
-ThetaLambdaTree<IntegerType>::ThetaLambdaTree() {}
+ThetaLambdaTree<IntegerType>::ThetaLambdaTree() = default;
 
 template <typename IntegerType>
 typename ThetaLambdaTree<IntegerType>::TreeNode
diff --git a/ortools/sat/timetable.cc b/ortools/sat/timetable.cc
index 71e198bddd..4d88a6ec62 100644
--- a/ortools/sat/timetable.cc
+++ b/ortools/sat/timetable.cc
@@ -15,15 +15,13 @@
 
 #include <algorithm>
 #include <cstdint>
-#include <utility>
 #include <vector>
 
-#include "ortools/base/logging.h"
+#include "absl/log/check.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
-#include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/strong_integers.h"
 
 namespace operations_research {
diff --git a/ortools/sat/timetable.h b/ortools/sat/timetable.h
index 54b2175085..cf1008578c 100644
--- a/ortools/sat/timetable.h
+++ b/ortools/sat/timetable.h
@@ -60,7 +60,7 @@ class ReservoirTimeTabling : public PropagatorInterface {
   // will be equal to the start of the next one. The height correspond to the
   // one from start (inclusive) until the next one (exclusive).
   struct ProfileRectangle {
-    ProfileRectangle() {}
+    ProfileRectangle() = default;
     ProfileRectangle(IntegerValue start, IntegerValue height)
         : start(start), height(height) {}
 
diff --git a/ortools/sat/timetable_edgefinding.cc b/ortools/sat/timetable_edgefinding.cc
index 11eda56ac3..49f70e87a2 100644
--- a/ortools/sat/timetable_edgefinding.cc
+++ b/ortools/sat/timetable_edgefinding.cc
@@ -14,14 +14,13 @@
 #include "ortools/sat/timetable_edgefinding.h"
 
 #include <algorithm>
-#include <cstdint>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/iterator_adaptors.h"
-#include "ortools/base/logging.h"
-#include "ortools/sat/implied_bounds.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
+#include "ortools/sat/model.h"
 #include "ortools/util/strong_integers.h"
 
 namespace operations_research {
diff --git a/ortools/sat/timetable_edgefinding.h b/ortools/sat/timetable_edgefinding.h
index 244e14f183..7e2a497848 100644
--- a/ortools/sat/timetable_edgefinding.h
+++ b/ortools/sat/timetable_edgefinding.h
@@ -19,6 +19,7 @@
 #include "ortools/base/macros.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
+#include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/util/strong_integers.h"
 
diff --git a/ortools/sat/util.cc b/ortools/sat/util.cc
index 8d35a30ef2..023edefc49 100644
--- a/ortools/sat/util.cc
+++ b/ortools/sat/util.cc
@@ -16,30 +16,31 @@
 #include <algorithm>
 #include <cmath>
 #include <cstdint>
-#include <cstdlib>
 #include <deque>
+#include <functional>
 #include <limits>
 #include <numeric>
 #include <string>
 #include <utility>
 #include <vector>
 
-#include "ortools/base/integral_types.h"
-#include "ortools/base/logging.h"
-#if !defined(__PORTABLE_PLATFORM__)
-#include "google/protobuf/descriptor.h"
-#endif  // __PORTABLE_PLATFORM__
 #include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
 #include "absl/numeric/int128.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/random/distributions.h"
+#include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
+#include "google/protobuf/descriptor.h"
+#include "ortools/base/logging.h"
 #include "ortools/base/mathutil.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/util/saturated_arithmetic.h"
+#include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
 
 namespace operations_research {
diff --git a/ortools/sat/util.h b/ortools/sat/util.h
index bdf0abe192..7ff5195ae1 100644
--- a/ortools/sat/util.h
+++ b/ortools/sat/util.h
@@ -14,22 +14,25 @@
 #ifndef OR_TOOLS_SAT_UTIL_H_
 #define OR_TOOLS_SAT_UTIL_H_
 
+#include <algorithm>
+#include <array>
 #include <cmath>
 #include <cstdint>
 #include <deque>
 #include <limits>
 #include <string>
+#include <utility>
 #include <vector>
 
-#include "ortools/base/logging.h"
-#if !defined(__PORTABLE_PLATFORM__)
-#include "google/protobuf/descriptor.h"
-#endif  // __PORTABLE_PLATFORM__
 #include "absl/container/btree_set.h"
 #include "absl/container/inlined_vector.h"
+#include "absl/log/check.h"
+#include "absl/log/log_streamer.h"
+#include "absl/numeric/int128.h"
 #include "absl/random/bit_gen_ref.h"
 #include "absl/random/random.h"
 #include "absl/types/span.h"
+#include "ortools/base/logging.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
@@ -343,7 +346,7 @@ class IncrementalAverage {
   // Initializes the average with 'initial_average' and number of records to 0.
   explicit IncrementalAverage(double initial_average)
       : average_(initial_average) {}
-  IncrementalAverage() {}
+  IncrementalAverage() = default;
 
   // Sets the number of records to 0 and average to 'reset_value'.
   void Reset(double reset_value);
diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc
index 05a0d939d0..692908367d 100644
--- a/ortools/sat/var_domination.cc
+++ b/ortools/sat/var_domination.cc
@@ -24,6 +24,10 @@
 #include <utility>
 #include <vector>
 
+#include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
+#include "absl/log/check.h"
+#include "absl/meta/type_traits.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/dynamic_partition.h"
@@ -35,6 +39,7 @@
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/presolve_context.h"
+#include "ortools/sat/presolve_util.h"
 #include "ortools/util/affine_relation.h"
 #include "ortools/util/sorted_interval_list.h"
 #include "ortools/util/strong_integers.h"
@@ -1380,13 +1385,24 @@ bool ExploitDominanceRelations(const VarDomination& var_domination,
     // implies one of its dominant to zero, then it can be set to zero. It seems
     // adding the implication below should have the same effect? but currently
     // it requires a lot of presolve rounds.
+    const auto add_implications = [&implications](absl::Span<const int> lits) {
+      if (lits.size() > 3) return;
+      for (int i = 0; i < lits.size(); ++i) {
+        for (int j = 0; j < lits.size(); ++j) {
+          if (i == j) continue;
+          implications.insert({lits[i], NegatedRef(lits[j])});
+        }
+      }
+    };
     if (ct.constraint_case() == ConstraintProto::kAtMostOne) {
+      add_implications(ct.at_most_one().literals());
       if (!ProcessAtMostOne(ct.at_most_one().literals(),
                             "domination: in at most one", var_domination,
                             &in_constraints, context)) {
         return false;
       }
     } else if (ct.constraint_case() == ConstraintProto::kExactlyOne) {
+      add_implications(ct.exactly_one().literals());
       if (!ProcessAtMostOne(ct.exactly_one().literals(),
                             "domination: in exactly one", var_domination,
                             &in_constraints, context)) {
@@ -1555,8 +1571,6 @@ bool ExploitDominanceRelations(const VarDomination& var_domination,
   // implications?
   //
   // TODO(user): generalize to non Booleans?
-  // TODO(user): We always keep adding the same relations. Investigate?
-  // it seems pure SAT presolve remove them.
   int num_added = 0;
   absl::StrongVector<IntegerVariable, bool> increase_is_forbidden(2 * num_vars,
                                                                   false);
diff --git a/ortools/sat/var_domination.h b/ortools/sat/var_domination.h
index 9903085ebb..660bf81130 100644
--- a/ortools/sat/var_domination.h
+++ b/ortools/sat/var_domination.h
@@ -51,7 +51,7 @@ namespace sat {
 // any. Try to improve the situation.
 class VarDomination {
  public:
-  VarDomination() {}
+  VarDomination() = default;
 
   // This is the translation used from "ref" to IntegerVariable. The API
   // understand the cp_model.proto ref, but internally we only store
diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc
index e6adda3a80..cf942c03ce 100644
--- a/ortools/sat/work_assignment.cc
+++ b/ortools/sat/work_assignment.cc
@@ -13,11 +13,11 @@
 
 #include "ortools/sat/work_assignment.h"
 
-#include <math.h>
-
 #include <algorithm>
+#include <array>
 #include <cmath>
 #include <cstdint>
+#include <deque>
 #include <functional>
 #include <limits>
 #include <optional>
@@ -28,7 +28,6 @@
 
 #include "absl/log/check.h"
 #include "absl/random/distributions.h"
-#include "absl/random/random.h"
 #include "absl/strings/str_cat.h"
 #include "absl/synchronization/mutex.h"
 #include "absl/types/span.h"
@@ -42,6 +41,8 @@
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/sat_solver.h"
 #include "ortools/sat/synchronization.h"
+#include "ortools/sat/util.h"
+#include "ortools/util/strong_integers.h"
 #include "ortools/util/time_limit.h"
 
 namespace operations_research::sat {
diff --git a/ortools/sat/work_assignment.h b/ortools/sat/work_assignment.h
index 035beb6cc2..d31f7c3155 100644
--- a/ortools/sat/work_assignment.h
+++ b/ortools/sat/work_assignment.h
@@ -14,6 +14,8 @@
 #ifndef OR_TOOLS_SAT_WORK_ASSIGNMENT_H_
 #define OR_TOOLS_SAT_WORK_ASSIGNMENT_H_
 
+#include <stdint.h>
+
 #include <array>
 #include <deque>
 #include <functional>
@@ -25,16 +27,20 @@
 #include <vector>
 
 #include "absl/base/thread_annotations.h"
+#include "absl/log/check.h"
 #include "absl/synchronization/mutex.h"
 #include "absl/types/span.h"
 #include "ortools/sat/cp_model_mapping.h"
+#include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/integer_search.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/sat/util.h"
+#include "ortools/util/strong_integers.h"
 #include "ortools/util/time_limit.h"
 
 namespace operations_research::sat {
diff --git a/ortools/sat/zero_half_cuts.cc b/ortools/sat/zero_half_cuts.cc
index 183c99a5b8..e4f6754120 100644
--- a/ortools/sat/zero_half_cuts.cc
+++ b/ortools/sat/zero_half_cuts.cc
@@ -14,10 +14,10 @@
 #include "ortools/sat/zero_half_cuts.h"
 
 #include <algorithm>
-#include <functional>
 #include <utility>
 #include <vector>
 
+#include "absl/log/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/lp_data/lp_types.h"
 #include "ortools/sat/integer.h"