diff --git a/makefiles/Makefile.gen.mk b/makefiles/Makefile.gen.mk
index 9d753f8de4..99eebaf33a 100644
--- a/makefiles/Makefile.gen.mk
+++ b/makefiles/Makefile.gen.mk
@@ -1829,8 +1829,10 @@ $(SRC_DIR)/ortools/sat/integer.h: \
     $(SRC_DIR)/ortools/util/sorted_interval_list.h
 
 $(SRC_DIR)/ortools/sat/integer_search.h: \
+    $(SRC_DIR)/ortools/base/random.h \
     $(SRC_DIR)/ortools/sat/integer.h \
-    $(SRC_DIR)/ortools/sat/sat_solver.h
+    $(SRC_DIR)/ortools/sat/sat_solver.h \
+    $(SRC_DIR)/ortools/util/random_engine.h
 
 $(SRC_DIR)/ortools/sat/intervals.h: \
     $(SRC_DIR)/ortools/base/integral_types.h \
@@ -2133,8 +2135,7 @@ $(OBJ_DIR)/sat/cp_model_presolve.$O: \
 $(OBJ_DIR)/sat/cp_model_search.$O: \
     $(SRC_DIR)/ortools/sat/cp_model_search.cc \
     $(SRC_DIR)/ortools/sat/cp_model_search.h \
-    $(SRC_DIR)/ortools/sat/cp_model_utils.h \
-    $(SRC_DIR)/ortools/util/random_engine.h
+    $(SRC_DIR)/ortools/sat/cp_model_utils.h
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Scp_model_search.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Scp_model_search.$O
 
 $(OBJ_DIR)/sat/cp_model_solver.$O: \
@@ -2267,7 +2268,8 @@ $(OBJ_DIR)/sat/integer_search.$O: \
     $(SRC_DIR)/ortools/sat/integer_search.cc \
     $(SRC_DIR)/ortools/sat/integer_search.h \
     $(SRC_DIR)/ortools/sat/linear_programming_constraint.h \
-    $(SRC_DIR)/ortools/sat/sat_decision.h
+    $(SRC_DIR)/ortools/sat/sat_decision.h \
+    $(SRC_DIR)/ortools/sat/util.h
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sinteger_search.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sinteger_search.$O
 
 $(OBJ_DIR)/sat/intervals.$O: \
diff --git a/ortools/bop/bop_fs.cc b/ortools/bop/bop_fs.cc
index 304f56ecb3..36381d8644 100644
--- a/ortools/bop/bop_fs.cc
+++ b/ortools/bop/bop_fs.cc
@@ -212,8 +212,7 @@ BopRandomFirstSolutionGenerator::BopRandomFirstSolutionGenerator(
     sat::SatSolver* sat_propagator, MTRandom* random)
     : BopOptimizerBase(name),
       random_(random),
-      sat_propagator_(sat_propagator),
-      sat_seed_(parameters.random_seed()) {}
+      sat_propagator_(sat_propagator) {}
 
 BopRandomFirstSolutionGenerator::~BopRandomFirstSolutionGenerator() {}
 
@@ -249,14 +248,12 @@ BopOptimizerBase::Status BopRandomFirstSolutionGenerator::Optimize(
 
   bool solution_found = false;
   while (remaining_num_conflicts > 0 && !time_limit->LimitReached()) {
-    ++sat_seed_;
     sat_propagator_->Backtrack(0);
     old_num_failures = sat_propagator_->num_failures();
 
     sat::SatParameters sat_params = saved_params;
     sat::RandomizeDecisionHeuristic(random_, &sat_params);
     sat_params.set_max_number_of_conflicts(kMaxNumConflicts);
-    sat_params.set_random_seed(sat_seed_);
     sat_propagator_->SetParameters(sat_params);
     sat_propagator_->ResetDecisionHeuristic();
 
diff --git a/ortools/bop/bop_fs.h b/ortools/bop/bop_fs.h
index 794a5f88e5..ca429d8189 100644
--- a/ortools/bop/bop_fs.h
+++ b/ortools/bop/bop_fs.h
@@ -100,7 +100,6 @@ class BopRandomFirstSolutionGenerator : public BopOptimizerBase {
   int random_seed_;
   MTRandom* random_;
   sat::SatSolver* sat_propagator_;
-  uint32 sat_seed_;
 };
 
 // This class computes the linear relaxation of the state problem.
diff --git a/ortools/bop/bop_parameters.proto b/ortools/bop/bop_parameters.proto
index 154a89f583..a3d051d583 100644
--- a/ortools/bop/bop_parameters.proto
+++ b/ortools/bop/bop_parameters.proto
@@ -108,7 +108,11 @@ message BopParameters {
   optional bool use_random_lns = 6 [default = true];
 
   // The seed used to initialize the random generator.
-  optional int32 random_seed = 7 [default = 0];
+  //
+  // TODO(user): Some of our client test fail depending on this value! we need
+  // to fix them and ideally randomize our behavior from on test to the next so
+  // that this doesn't happen in the future.
+  optional int32 random_seed = 7 [default = 8];
 
   // Number of variables to relax in the exhaustive Large Neighborhood Search.
   optional int32 num_relaxed_vars = 8 [default = 10];
diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc
index d0cd54aefb..599fcc5587 100644
--- a/ortools/flatzinc/cp_model_fz_solver.cc
+++ b/ortools/flatzinc/cp_model_fz_solver.cc
@@ -26,6 +26,7 @@
 #include "ortools/base/timer.h"
 #include "ortools/flatzinc/checker.h"
 #include "ortools/flatzinc/logging.h"
+#include "ortools/port/proto_utils.h"
 #include "ortools/sat/cp_constraints.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
@@ -926,6 +927,74 @@ CpSolverResponse WorkerSearch(
   return response;
 }
 
+bool MergeOptimizationSolution(const CpSolverResponse& response, bool maximize,
+                               CpSolverResponse* best) {
+  switch (response.status()) {
+    case CpSolverStatus::MODEL_SAT: {
+      const bool is_improving =
+          maximize ? response.objective_value() > best->objective_value()
+                   : response.objective_value() < best->objective_value();
+      const double current_best_bound = response.best_objective_bound();
+      const double previous_best_bound = best->best_objective_bound();
+      const double new_best_objective_bound =
+          maximize ? std::min(previous_best_bound, current_best_bound)
+                   : std::max(previous_best_bound, current_best_bound);
+      // TODO(user): return OPTIMAL if objective is tight.
+      if (is_improving) {
+        // Overwrite solution and fix best_objective_bound.
+        *best = response;
+        best->set_best_objective_bound(new_best_objective_bound);
+        return true;
+      }
+      // Maybe we can always improve best_objective_bound.
+      best->set_best_objective_bound(new_best_objective_bound);
+      return false;
+    }
+    case CpSolverStatus::MODEL_UNSAT: {
+      if (best->status() == CpSolverStatus::UNKNOWN ||
+          best->status() == CpSolverStatus::MODEL_UNSAT) {
+        // Stores the unsat solution.
+        *best = response;
+        return true;
+      } else {
+        // It can happen that the LNS finds the best solution, but does
+        // not prove it. Then another worker pulls in the best solution,
+        // does not improve upon it, returns UNSAT if it has not found a
+        // previous solution, or OPTIMAL with a bad objective value, and
+        // stops all other workers. In that case, if the last solution
+        // found has a MODEL_SAT status, it is indeed optimal, and
+        // should be marked as thus.
+        FZVLOG << "Fixing best known solution to optimal." << FZENDL;
+        best->set_status(CpSolverStatus::OPTIMAL);
+        best->set_best_objective_bound(best->objective_value());
+        return false;
+      }
+      break;
+    }
+    case CpSolverStatus::OPTIMAL: {
+      const double previous = best->objective_value();
+      const double current = response.objective_value();
+      if ((maximize && current >= previous) ||
+          (!maximize && current <= previous)) {
+        // We always overwrite the best solution with an at-least as good
+        // optimal solution.
+        *best = response;
+        return true;
+      } else {
+        // We are in the same case as the MODEL_UNSAT above.  Solution
+        // synchronization has forced the solver to exit with a sub-optimal
+        // solution, believing it was optimal.
+        FZVLOG << "Fixing best known solution to optimal." << FZENDL;
+        best->set_status(CpSolverStatus::OPTIMAL);
+        best->set_best_objective_bound(best->objective_value());
+        return false;
+      }
+      break;
+    }
+    default: { return false; }
+  }
+}
+
 }  // namespace
 
 void SolveFzWithCpModelProto(const fz::Model& fz_model,
@@ -1035,8 +1104,18 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
   const int num_search_workers = std::max(1, p.threads);
 
   bool stopped = false;
-  std::vector<CpSolverResponse> responses(num_search_workers);
-  int last_worker_id = -1;
+  CpSolverResponse best_response;
+  if (fz_model.objective() != nullptr) {
+    const double kInfinity = std::numeric_limits<double>::infinity();
+    if (fz_model.maximize()) {
+      best_response.set_objective_value(-kInfinity);
+      best_response.set_best_objective_bound(kInfinity);
+    } else {
+      best_response.set_objective_value(kInfinity);
+      best_response.set_best_objective_bound(-kInfinity);
+    }
+  }
+
   int solution_count = 1;  // Start at 1 as in the sat solver output.
 
   // Solve the problem.
@@ -1052,18 +1131,17 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
       const SatParameters local_params =
           DiversifySearchParameters(worker_id, m.parameters, m.proto, 0);
       pool.Schedule([&fz_model, &m, &p, &stopped, local_params, worker_id,
-                     &responses, &last_worker_id, &mutex]() {
-        responses[worker_id] =
+                     &best_response, &mutex]() {
+        const CpSolverResponse local_response =
             WorkerSearch(m.proto, local_params, p, nullptr, nullptr, nullptr,
                          worker_id, &stopped);
         absl::MutexLock lock(&mutex);
-        if (responses[worker_id].status() == CpSolverStatus::MODEL_SAT ||
-            responses[worker_id].status() == CpSolverStatus::MODEL_UNSAT) {
-          last_worker_id = worker_id;
+        if (best_response.status() == CpSolverStatus::UNKNOWN) {
+          best_response = local_response;
+        }
+        if (local_response.status() != CpSolverStatus::UNKNOWN) {
+          CHECK_EQ(local_response.status(), best_response.status());
           stopped = true;
-        } else if (last_worker_id == -1) {
-          // Puts a default value.
-          last_worker_id = worker_id;
         }
       });
     }
@@ -1083,24 +1161,11 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
       FZLOG << "Starting parallel search with " << num_search_workers
             << " workers" << FZENDL;
     }
-    CpSolverResponse best_response;
-    bool suspicious_termination = false;
     {
       ThreadPool pool("Parallel_FlatZinc_sat", num_active_threads);
       pool.StartWorkers();
 
       for (int worker_id = 0; worker_id < num_active_threads; ++worker_id) {
-        const auto is_improving = [&best_response,
-                                   maximize](const CpSolverResponse& r) {
-          return (best_response.status() == CpSolverStatus::MODEL_SAT ||
-                  best_response.status() == CpSolverStatus::OPTIMAL)
-                     ? (maximize ? r.objective_value() >
-                                       best_response.objective_value()
-                                 : r.objective_value() <
-                                       best_response.objective_value())
-                     : true;
-        };
-
         const auto solution_synchronization = [&mutex, &best_response]() {
           absl::MutexLock lock(&mutex);
           return best_response;
@@ -1116,25 +1181,28 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
         };
 
         const auto solution_observer = [maximize, &solution_count, worker_id,
-                                        &mutex, &p, &fz_model, &last_worker_id,
-                                        &m, &best_response, is_improving,
+                                        &mutex, &p, &fz_model, &m,
+                                        &best_response,
                                         &timer](const CpSolverResponse& r) {
           absl::MutexLock lock(&mutex);
 
           // Check is the new solution is actually improving upon the best
           // solution found so far.
-          if (is_improving(r)) {
-            best_response = r;
-            last_worker_id = worker_id;
-            FZLOG << "worker #" << worker_id << ", solution #"
-                  << solution_count++ << ", objective = " << r.objective_value()
-                  << ", time = " << timer.Get() << "s" << FZENDL;
-            if (FLAGS_use_flatzinc_format && p.all_solutions) {
-              const std::string solution_string =
-                  SolutionString(fz_model, [&m, &r](fz::IntegerVariable* v) {
-                    return r.solution(gtl::FindOrDie(m.fz_var_to_index, v));
-                  });
-              std::cout << solution_string << std::endl;
+          if (MergeOptimizationSolution(r, maximize, &best_response)) {
+            if (p.all_solutions) {
+              FZLOG << "worker #" << worker_id << ", solution #"
+                    << solution_count++
+                    << ", objective = " << best_response.objective_value()
+                    << ", objective " << (maximize ? "upper" : "lower")
+                    << " bound = " << best_response.best_objective_bound()
+                    << ", time = " << timer.Get() << "s" << FZENDL;
+              if (FLAGS_use_flatzinc_format) {
+                const std::string solution_string =
+                    SolutionString(fz_model, [&m, &r](fz::IntegerVariable* v) {
+                      return r.solution(gtl::FindOrDie(m.fz_var_to_index, v));
+                    });
+                std::cout << solution_string << std::endl;
+              }
             }
           }
         };
@@ -1145,10 +1213,9 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
 
         pool.Schedule([&fz_model, &m, &p, solution_observer,
                        solution_synchronization, objective_synchronization,
-                       &stopped, local_params, worker_id, &mutex, &responses,
-                       &last_worker_id, is_improving, &best_response, maximize,
-                       &suspicious_termination]() {
-          responses[worker_id] =
+                       &stopped, local_params, worker_id, &mutex,
+                       &best_response, maximize]() {
+          const CpSolverResponse local_response =
               WorkerSearch(m.proto, local_params, p, solution_observer,
                            solution_synchronization, objective_synchronization,
                            worker_id, &stopped);
@@ -1156,88 +1223,36 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
           // Process final solution. Decide which worker has the 'best'
           // solution. Note that the solution observer may or may not have been
           // called.
+          //
+          // TODO(user): If the solution is SAT, we can pull the best lower
+          // bound.
           absl::MutexLock lock(&mutex);
           FZVLOG << "Worker " << worker_id << " terminates with status "
-                 << responses[worker_id].status()
+                 << ProtoEnumToString<CpSolverStatus>(local_response.status())
                  << " and an objective value of "
-                 << responses[worker_id].objective_value() << FZENDL;
-          switch (responses[worker_id].status()) {
-            case CpSolverStatus::MODEL_SAT: {
-              if (is_improving(responses[worker_id])) {
-                last_worker_id = worker_id;
-                best_response = responses[worker_id];
-              }
-              break;
-            }
-            case CpSolverStatus::MODEL_UNSAT: {
-              if (best_response.status() != CpSolverStatus::MODEL_SAT &&
-                  best_response.status() != CpSolverStatus::OPTIMAL) {
-                // Overwrite any previous worker.
-                last_worker_id = worker_id;
-                // Stores the unsat solution.
-                best_response = responses[worker_id];
-              } else {
-                suspicious_termination = true;
-              }
-              // Stops all other workers.
-              stopped = true;
-              break;
-            }
-            case CpSolverStatus::OPTIMAL: {
-              const double previous =
-                  (best_response.status() == CpSolverStatus::MODEL_SAT ||
-                   best_response.status() == CpSolverStatus::OPTIMAL)
-                      ? best_response.objective_value()
-                      : (maximize ? kint64min : kint64max);
-              const double current = responses[worker_id].objective_value();
-              if ((maximize && current >= previous) ||
-                  (!maximize && current <= previous)) {
-                // Overwrite any previous worker.
-                last_worker_id = worker_id;
-                // Stops all other workers.
-                stopped = true;
-                // Stores the best solution.
-                best_response = responses[worker_id];
-              } else {
-                suspicious_termination = true;
-                // Stops all other workers.
-                stopped = true;
-              }
-              break;
-            }
-            default: {
-              if (last_worker_id == -1) {
-                last_worker_id = worker_id;
-              }
-            }
+                 << local_response.objective_value() << FZENDL;
+          MergeOptimizationSolution(local_response, maximize, &best_response);
+          if (best_response.status() == CpSolverStatus::OPTIMAL ||
+              best_response.status() == CpSolverStatus::MODEL_UNSAT) {
+            stopped = true;
           }
         });
       }
     }
-    // It can happen that the LNS finds the best solution, but does not prove
-    // it. Then another worker pulls in the best solution, does not improve
-    // upon it, returns UNSAT if it has not found a previous solution, or
-    // OPTIMAL with a bad objective value, and stops all other workers. In that
-    // case, if the last solution found has a MODEL_SAT status, it is indeed
-    // optimal, and should be marked as thus.
-    if (last_worker_id != -1 &&
-        responses[last_worker_id].status() == CpSolverStatus::MODEL_SAT &&
-        suspicious_termination) {
-      FZVLOG << "Fixing best known solution to optimal." << FZENDL;
-      responses[last_worker_id].set_status(CpSolverStatus::OPTIMAL);
-      responses[last_worker_id].set_best_objective_bound(
-          responses[last_worker_id].objective_value());
-    }
-    // TODO(user): If the solution is SAT, we can pull the best lower bound.
+    // Fix wall time.
+    best_response.set_wall_time(timer.Get());
   } else if (p.all_solutions) {  // Sequential case with observer.
-    auto solution_observer = [&fz_model, &solution_count, &m,
+    const bool maximize = fz_model.maximize();
+    auto solution_observer = [&fz_model, &solution_count, &m, maximize,
                               &timer](const CpSolverResponse& r) {
       if (fz_model.objective() == nullptr) {
         FZLOG << "solution #" << solution_count++ << ", time = " << timer.Get()
               << " s" << FZENDL;
       } else {
         FZLOG << "solution #" << solution_count++
-              << ", objective = " << r.objective_value()
+              << ", objective = " << r.objective_value() << ", objective "
+              << (maximize ? "upper" : "lower")
+              << " bound = " << r.best_objective_bound()
               << ", time = " << timer.Get() << " s" << FZENDL;
       }
       if (FLAGS_use_flatzinc_format) {
@@ -1248,60 +1263,47 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
         std::cout << solution_string << std::endl;
       }
     };
-    responses[0] = WorkerSearch(m.proto, m.parameters, p, solution_observer,
-                                nullptr, nullptr, 0, &stopped);
-    last_worker_id = 0;
+    best_response = WorkerSearch(m.proto, m.parameters, p, solution_observer,
+                                 nullptr, nullptr, 0, &stopped);
   } else {  // Sequential case, no observer.
-    responses[0] = WorkerSearch(m.proto, m.parameters, p, nullptr, nullptr,
-                                nullptr, 0, &stopped);
-    last_worker_id = 0;
-  }
-
-  for (int i = 0; i < num_search_workers; ++i) {
-    if (responses[i].status() != CpSolverStatus::UNKNOWN) {
-      FZLOG << "Worker " << i << ": " << responses[i].status() << FZENDL;
-    }
-  }
-
-  CHECK_NE(last_worker_id, -1);
-  if (num_search_workers > 1) {
-    FZLOG << "Final solution found by worker " << last_worker_id << FZENDL;
+    best_response = WorkerSearch(m.proto, m.parameters, p, nullptr, nullptr,
+                                 nullptr, 0, &stopped);
   }
 
   // Check the returned solution with the fz model checker.
-  const CpSolverResponse& response = responses[last_worker_id];
-  if (response.status() == CpSolverStatus::MODEL_SAT ||
-      response.status() == CpSolverStatus::OPTIMAL) {
-    CHECK(CheckSolution(fz_model, [&response, &m](fz::IntegerVariable* v) {
-      return response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
+  if (best_response.status() == CpSolverStatus::MODEL_SAT ||
+      best_response.status() == CpSolverStatus::OPTIMAL) {
+    CHECK(CheckSolution(fz_model, [&best_response, &m](fz::IntegerVariable* v) {
+      return best_response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
     }));
   }
 
   // Output the solution if the flatzinc official format.
   if (FLAGS_use_flatzinc_format) {
-    if (response.status() == CpSolverStatus::MODEL_SAT ||
-        response.status() == CpSolverStatus::OPTIMAL) {
+    if (best_response.status() == CpSolverStatus::MODEL_SAT ||
+        best_response.status() == CpSolverStatus::OPTIMAL) {
       if (!p.all_solutions) {  // Already printed otherwise.
-        const std::string solution_string =
-            SolutionString(fz_model, [&response, &m](fz::IntegerVariable* v) {
-              return response.solution(gtl::FindOrDie(m.fz_var_to_index, v));
+        const std::string solution_string = SolutionString(
+            fz_model, [&best_response, &m](fz::IntegerVariable* v) {
+              return best_response.solution(
+                  gtl::FindOrDie(m.fz_var_to_index, v));
             });
         std::cout << solution_string << std::endl;
       }
-      if (response.status() == CpSolverStatus::OPTIMAL ||
-          response.all_solutions_were_found()) {
+      if (best_response.status() == CpSolverStatus::OPTIMAL ||
+          best_response.all_solutions_were_found()) {
         std::cout << "==========" << std::endl;
       }
-    } else if (response.status() == CpSolverStatus::MODEL_UNSAT) {
+    } else if (best_response.status() == CpSolverStatus::MODEL_UNSAT) {
       std::cout << "=====UNSATISFIABLE=====" << std::endl;
     } else {
       std::cout << "%% TIMEOUT" << std::endl;
     }
     if (p.statistics) {
-      LogInFlatzincFormat(CpSolverResponseStats(response));
+      LogInFlatzincFormat(CpSolverResponseStats(best_response));
     }
   } else {
-    LOG(INFO) << CpSolverResponseStats(response);
+    LOG(INFO) << CpSolverResponseStats(best_response);
   }
 }
 
diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc
index 6648fea50c..b2580e8810 100644
--- a/ortools/sat/cp_model_search.cc
+++ b/ortools/sat/cp_model_search.cc
@@ -17,7 +17,7 @@
 #include <unordered_map>
 
 #include "ortools/sat/cp_model_utils.h"
-#include "ortools/util/random_engine.h"
+#include "ortools/sat/util.h"
 
 namespace operations_research {
 namespace sat {
@@ -38,12 +38,6 @@ struct VarValue {
   IntegerValue value;
 };
 
-// Thin wrapper around a random_engine. This helps store a random engine
-// inside a Model as template programming messes up compilation.
-struct SearchStrategyRandomGenerator {
-  random_engine_t rand;
-};
-
 const std::function<LiteralIndex()> ConstructSearchStrategyInternal(
     const std::unordered_map<int, std::pair<int64, int64>>&
         var_to_coeff_offset_pair,
@@ -134,16 +128,9 @@ const std::function<LiteralIndex()> ConstructSearchStrategyInternal(
         active_vars.erase(std::remove_if(active_vars.begin(), active_vars.end(),
                                          is_above_tolerance),
                           active_vars.end());
-        // TODO(user): Move this to its own method.
-        const bool seeded =
-            model->Get<SearchStrategyRandomGenerator>() != nullptr;
-        SearchStrategyRandomGenerator* const rw =
-            model->GetOrCreate<SearchStrategyRandomGenerator>();
-        if (!seeded) {
-          rw->rand.seed(parameters->random_seed());
-        }
-        const int winner = std::uniform_int_distribution<int>(
-            0, active_vars.size() - 1)(rw->rand);
+        const int winner =
+            std::uniform_int_distribution<int>(0, active_vars.size() - 1)(
+                *model->GetOrCreate<ModelRandomGenerator>());
         candidate = active_vars[winner].var;
         candidate_lb = integer_trail->LowerBound(candidate);
         candidate_ub = integer_trail->UpperBound(candidate);
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 1beb9bdd49..0f0bd2cc6a 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -2243,6 +2243,10 @@ std::function<SatParameters(Model*)> NewSatParameters(
 std::function<SatParameters(Model*)> NewSatParameters(
     const sat::SatParameters& parameters) {
   return [=](Model* model) {
+    // Tricky: It is important to initialize the model parameters before any
+    // of the solver object are created, so that by default they use the given
+    // parameters.
+    *model->GetOrCreate<SatParameters>() = parameters;
     model->GetOrCreate<SatSolver>()->SetParameters(parameters);
     return parameters;
   };
@@ -2536,6 +2540,9 @@ CpSolverResponse SolveCpModelInternal(
                                m.Integer(model_proto.objective().vars(i))));
       }
       response.set_objective_value(ScaleObjectiveValue(obj, objective_value));
+      const IntegerTrail* integer_trail = sat_model.Get<IntegerTrail>();
+      response.set_best_objective_bound(ScaleObjectiveValue(
+          obj, integer_trail->LevelZeroBound(objective_var).value()));
       external_solution_observer(response);
       VLOG(1) << "Solution #" << num_solutions
               << " obj:" << response.objective_value()
diff --git a/ortools/sat/cp_model_solver.h b/ortools/sat/cp_model_solver.h
index 0e188d56a8..728016a30f 100644
--- a/ortools/sat/cp_model_solver.h
+++ b/ortools/sat/cp_model_solver.h
@@ -62,8 +62,8 @@ std::function<void(Model*)> NewFeasibleSolutionObserver(
 void SetSynchronizationFunction(std::function<CpSolverResponse()> f,
                                 Model* model);
 
-// wait until this function returns with the current "best" information about
-// the objective value of the current best solution.
+// Wait until this function returns with the objective value of the current
+// best solution.
 void SetObjectiveSynchronizationFunction(std::function<double()> f,
                                          Model* model);
 
diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h
index cf243319ee..670577b5c7 100644
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -609,6 +609,13 @@ class IntegerTrail : public SatPropagator {
     return false;
   }
 
+  // Returns a lower bound on the given var that will always be valid.
+  IntegerValue LevelZeroBound(IntegerVariable var) const {
+    // The level zero bounds are stored at the beginning of the trail and they
+    // also serves as sentinels. Their index match the variables index.
+    return integer_trail_[var.value()].bound;
+  }
+
   // Returns true if the variable lower bound is still the one from level zero.
   bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const {
     return vars_[var].current_trail_index < vars_.size();
@@ -638,13 +645,6 @@ class IntegerTrail : public SatPropagator {
                                 absl::Span<IntegerLiteral> integer_reason,
                                 BooleanVariable* variable_with_same_reason);
 
-  // Returns a lower bound on the given var that will always be valid.
-  IntegerValue LevelZeroBound(IntegerVariable var) const {
-    // The level zero bounds are stored at the beginning of the trail and they
-    // also serves as sentinels. Their index match the variables index.
-    return integer_trail_[var.value()].bound;
-  }
-
   // Returns the lowest trail index of a TrailEntry that can be used to explain
   // the given IntegerLiteral. The literal must be currently true (CHECKed).
   // Returns -1 if the explanation is trivial.
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index fa594ad2c2..21b4fcc5bd 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -17,6 +17,7 @@
 
 #include "ortools/sat/linear_programming_constraint.h"
 #include "ortools/sat/sat_decision.h"
+#include "ortools/sat/util.h"
 
 namespace operations_research {
 namespace sat {
@@ -91,6 +92,23 @@ std::function<LiteralIndex()> SatSolverHeuristic(Model* model) {
   };
 }
 
+std::function<LiteralIndex()> RandomizeOnRestartSatSolverHeuristic(
+    Model* model) {
+  SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
+  Trail* trail = model->GetOrCreate<Trail>();
+  SatDecisionPolicy* decision_policy = model->GetOrCreate<SatDecisionPolicy>();
+  return [sat_solver, trail, decision_policy, model] {
+    if (sat_solver->CurrentDecisionLevel() == 0) {
+      RandomizeDecisionHeuristic(model->GetOrCreate<ModelRandomGenerator>(),
+                                 model->GetOrCreate<SatParameters>());
+      decision_policy->ResetDecisionHeuristic();
+    }
+    const bool all_assigned = trail->Index() == sat_solver->NumVariables();
+    return all_assigned ? kNoLiteralIndex
+                        : decision_policy->NextBranch().Index();
+  };
+}
+
 std::function<LiteralIndex()> FollowHint(
     const std::vector<BooleanOrIntegerVariable>& vars,
     const std::vector<IntegerValue>& values, Model* model) {
@@ -270,16 +288,18 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(
   const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
   switch (parameters.search_branching()) {
     case SatParameters::AUTOMATIC_SEARCH: {
+      std::function<LiteralIndex()> search;
+      if (parameters.randomize_search()) {
+        search = SequentialSearch(
+            {RandomizeOnRestartSatSolverHeuristic(model), next_decision});
+      } else {
+        search = SequentialSearch({SatSolverHeuristic(model), next_decision});
+      }
       if (parameters.exploit_integer_lp_solution()) {
-        return SolveProblemWithPortfolioSearch(
-            {ExploitIntegerLpSolution(
-                SequentialSearch({SatSolverHeuristic(model), next_decision}),
-                model)},
-            {SatSolverRestartPolicy(model)}, model);
+        search = ExploitIntegerLpSolution(search, model);
       }
       return SolveProblemWithPortfolioSearch(
-          {SequentialSearch({SatSolverHeuristic(model), next_decision})},
-          {SatSolverRestartPolicy(model)}, model);
+          {search}, {SatSolverRestartPolicy(model)}, model);
     }
     case SatParameters::FIXED_SEARCH: {
       // Not all Boolean might appear in next_decision(), so once there is no
@@ -361,6 +381,13 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
   if (num_policies == 0) return SatSolver::MODEL_SAT;
   CHECK_EQ(num_policies, restart_policies.size());
   SatSolver* const solver = model->GetOrCreate<SatSolver>();
+  const SatParameters* const params = model->Get<SatParameters>();
+  const bool use_core = params != nullptr && params->optimize_with_core();
+  const ObjectiveSynchronizationHelper* helper =
+      model->Get<ObjectiveSynchronizationHelper>();
+  const bool synchronize_objective =
+      !use_core && helper != nullptr && helper->get_external_bound != nullptr &&
+      helper->objective_var != kNoIntegerVariable;
 
   // Note that it is important to do the level-zero propagation if it wasn't
   // already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
@@ -385,10 +412,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
 
     // Check external objective, and restart if a better one is supplied.
     // TODO(user): Maybe do not check this at each decision.
-    const ObjectiveSynchronizationHelper* helper =
-        model->Get<ObjectiveSynchronizationHelper>();
-    if (helper != nullptr && helper->get_external_bound != nullptr &&
-        helper->objective_var != kNoIntegerVariable) {
+    if (synchronize_objective) {
       const double external_bound = helper->get_external_bound();
       if (std::isfinite(external_bound)) {
         IntegerValue best_bound(helper->UnscaledObjective(external_bound));
diff --git a/ortools/sat/sat_decision.cc b/ortools/sat/sat_decision.cc
index 7827e29f61..a211678722 100644
--- a/ortools/sat/sat_decision.cc
+++ b/ortools/sat/sat_decision.cc
@@ -13,14 +13,15 @@
 
 #include "ortools/sat/sat_decision.h"
 
+#include "ortools/sat/util.h"
+
 namespace operations_research {
 namespace sat {
 
 SatDecisionPolicy::SatDecisionPolicy(Model* model)
     : parameters_(*(model->GetOrCreate<SatParameters>())),
-      trail_(model->GetOrCreate<Trail>()) {
-  random_.seed(parameters_.random_seed());
-}
+      trail_(model->GetOrCreate<Trail>()),
+      random_(model->GetOrCreate<ModelRandomGenerator>()) {}
 
 void SatDecisionPolicy::IncreaseNumVariables(int num_variables) {
   const int old_num_variables = activities_.size();
@@ -47,8 +48,6 @@ void SatDecisionPolicy::IncreaseNumVariables(int num_variables) {
 }
 
 void SatDecisionPolicy::ResetDecisionHeuristic() {
-  random_.seed(parameters_.random_seed());
-
   const int num_variables = activities_.size();
   variable_activity_increment_ = 1.0;
   activities_.assign(num_variables, parameters_.initial_variables_activity());
@@ -83,7 +82,7 @@ void SatDecisionPolicy::ResetInitialPolarity(int from) {
         var_polarity_[var] = false;
         break;
       case SatParameters::POLARITY_RANDOM:
-        var_polarity_[var] = std::uniform_int_distribution<int>(0, 1)(random_);
+        var_polarity_[var] = std::uniform_int_distribution<int>(0, 1)(*random_);
         break;
       case SatParameters::POLARITY_WEIGHTED_SIGN:
         var_polarity_[var] = weighted_sign_[var] > 0;
@@ -130,7 +129,7 @@ void SatDecisionPolicy::InitializeVariableOrdering() {
       std::reverse(variables.begin(), variables.end());
       break;
     case SatParameters::IN_RANDOM_ORDER:
-      std::shuffle(variables.begin(), variables.end(), random_);
+      std::shuffle(variables.begin(), variables.end(), *random_);
       break;
   }
 
@@ -243,7 +242,7 @@ Literal SatDecisionPolicy::NextBranch() {
   BooleanVariable var;
   const double ratio = parameters_.random_branches_ratio();
   auto zero_to_one = [this]() {
-    return std::uniform_real_distribution<double>()(random_);
+    return std::uniform_real_distribution<double>()(*random_);
   };
   if (ratio != 0.0 && zero_to_one() < ratio) {
     while (true) {
@@ -251,7 +250,7 @@ Literal SatDecisionPolicy::NextBranch() {
       // variables are assigned.
       std::uniform_int_distribution<int> index_dist(0,
                                                     var_ordering_.Size() - 1);
-      var = var_ordering_.QueueElement(index_dist(random_)).var;
+      var = var_ordering_.QueueElement(index_dist(*random_)).var;
       if (!trail_->Assignment().VariableIsAssigned(var)) break;
       pq_need_update_for_var_at_trail_index_.Set(trail_->Info(var).trail_index);
       var_ordering_.Remove(var.value());
@@ -271,7 +270,7 @@ Literal SatDecisionPolicy::NextBranch() {
   // Choose its polarity (i.e. True of False).
   const double random_ratio = parameters_.random_polarity_ratio();
   if (random_ratio != 0.0 && zero_to_one() < random_ratio) {
-    return Literal(var, std::uniform_int_distribution<int>(0, 1)(random_));
+    return Literal(var, std::uniform_int_distribution<int>(0, 1)(*random_));
   }
   return Literal(var, var_use_phase_saving_[var]
                           ? trail_->Info(var).last_polarity
diff --git a/ortools/sat/sat_decision.h b/ortools/sat/sat_decision.h
index 836c2cb309..c5a3bf1228 100644
--- a/ortools/sat/sat_decision.h
+++ b/ortools/sat/sat_decision.h
@@ -109,9 +109,7 @@ class SatDecisionPolicy {
   // Singleton model objects.
   const SatParameters& parameters_;
   Trail* trail_;
-
-  // TODO(user): make this part of the Model so it can be shared?
-  random_engine_t random_;
+  random_engine_t* random_;
 
   // Variable ordering (priority will be adjusted dynamically). queue_elements_
   // holds the elements used by var_ordering_ (it uses pointers).
diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto
index d7846a6b89..9e4390e7e9 100644
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -18,7 +18,7 @@ package operations_research.sat;
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 105
+// NEXT TAG: 106
 message SatParameters {
   // ==========================================================================
   // Branching and polarity
@@ -568,13 +568,14 @@ message SatParameters {
   // Specify the number of parallel workers to use during search.
   // A number <= 1 means no parallelism.
   optional int32 num_search_workers = 100 [default = 0];
+  optional bool deterministic_search = 101 [default = true];
 
   // LNS parameters.
-  optional bool use_lns = 101 [default = false];
-  optional int32 lns_num_threads = 102 [default = 1];
+  optional bool use_lns = 102 [default = false];
+  optional int32 lns_num_threads = 103 [default = 1];
 
   // Randomize fixed search.
-  optional bool randomize_search = 103 [default = false];
+  optional bool randomize_search = 104 [default = false];
 
   // Search randomization will collect equivalent 'max valued' variables, and
   // pick one randomly. For instance, if the variable strategy is CHOOSE_FIRST,
@@ -583,5 +584,5 @@ message SatParameters {
   // variables, then the set of max valued variables will be all unassigned
   // variables where
   //    lm <= variable min <= lm + search_randomization_tolerance
-  optional int64 search_randomization_tolerance = 104 [default = 0];
+  optional int64 search_randomization_tolerance = 105 [default = 0];
 }
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index ffa47b35bf..f0890ed044 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -123,9 +123,6 @@ void SatSolver::SetParameters(const SatParameters& parameters) {
   *parameters_ = parameters;
 
   pb_constraints_.SetParameters(parameters);
-
-  random_.seed(parameters.random_seed());
-
   restart_->Reset();
   time_limit_->ResetLimitFromParameters(parameters);
 }
@@ -681,7 +678,8 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
                SatParameters::
                    BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION) {
       binary_implication_graph_.MinimizeConflictFirstWithTransitiveReduction(
-          *trail_, &learned_conflict_, &is_marked_, &random_);
+          *trail_, &learned_conflict_, &is_marked_,
+          model_->GetOrCreate<ModelRandomGenerator>());
     }
     DCHECK(IsConflictValid(learned_conflict_));
   }
diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h
index 5f9fb3afbd..c3a80e42e3 100644
--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -43,7 +43,6 @@
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_decision.h"
 #include "ortools/sat/sat_parameters.pb.h"
-#include "ortools/util/random_engine.h"
 #include "ortools/util/stats.h"
 #include "ortools/util/time_limit.h"
 
@@ -796,9 +795,6 @@ class SatSolver {
   // analysis.
   VariableWithSameReasonIdentifier same_reason_identifier_;
 
-  // A random number generator.
-  mutable random_engine_t random_;
-
   // Temporary vector used by AddProblemClause().
   std::vector<LiteralWithCoeff> tmp_pb_constraint_;
 
diff --git a/ortools/sat/util.cc b/ortools/sat/util.cc
index 02d581a688..d9372e8a82 100644
--- a/ortools/sat/util.cc
+++ b/ortools/sat/util.cc
@@ -13,34 +13,9 @@
 
 #include "ortools/sat/util.h"
 
-#if !defined(__PORTABLE_PLATFORM__)
-#include "google/protobuf/descriptor.h"
-#endif  // __PORTABLE_PLATFORM__
-
 namespace operations_research {
 namespace sat {
 
-void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters) {
-#if !defined(__PORTABLE_PLATFORM__)
-  // Random preferred variable order.
-  const google::protobuf::EnumDescriptor* order_d =
-      SatParameters::VariableOrder_descriptor();
-  parameters->set_preferred_variable_order(
-      static_cast<SatParameters::VariableOrder>(
-          order_d->value(random->Uniform(order_d->value_count()))->number()));
-
-  // Random polarity initial value.
-  const google::protobuf::EnumDescriptor* polarity_d =
-      SatParameters::Polarity_descriptor();
-  parameters->set_initial_polarity(static_cast<SatParameters::Polarity>(
-      polarity_d->value(random->Uniform(polarity_d->value_count()))->number()));
-#endif  // __PORTABLE_PLATFORM__
-  // Other random parameters.
-  parameters->set_use_phase_saving(random->OneIn(2));
-  parameters->set_random_polarity_ratio(random->OneIn(2) ? 0.01 : 0.0);
-  parameters->set_random_branches_ratio(random->OneIn(2) ? 0.01 : 0.0);
-}
-
 int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
                                   int relevant_prefix_size,
                                   std::vector<Literal>* literals) {
diff --git a/ortools/sat/util.h b/ortools/sat/util.h
index 637d8bbd2c..3bb8e9c3fa 100644
--- a/ortools/sat/util.h
+++ b/ortools/sat/util.h
@@ -15,14 +15,32 @@
 #define OR_TOOLS_SAT_UTIL_H_
 
 #include "ortools/base/random.h"
+#include "ortools/sat/model.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
+#include "ortools/util/random_engine.h"
+
+#if !defined(__PORTABLE_PLATFORM__)
+#include "google/protobuf/descriptor.h"
+#endif  // __PORTABLE_PLATFORM__
 
 namespace operations_research {
 namespace sat {
 
+// The model "singleton" random engine used in the solver.
+struct ModelRandomGenerator : public random_engine_t {
+  // We seed the strategy at creation only. This should be enough for our use
+  // case since the SatParameters is set first before the solver is created. We
+  // also never really need to change the seed afterwards, it is just used to
+  // diversify solves with identical parameters on different Model objects.
+  explicit ModelRandomGenerator(Model* model) : random_engine_t() {
+    seed(model->GetOrCreate<SatParameters>()->random_seed());
+  }
+};
+
 // Randomizes the decision heuristic of the given SatParameters.
-void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters);
+template <typename URBG>
+void RandomizeDecisionHeuristic(URBG* random, SatParameters* parameters);
 
 // Context: this function is not really generic, but required to be unit-tested.
 // It is used in a clause minimization algorithm when we try to detect if any of
@@ -48,6 +66,37 @@ int MoveOneUnprocessedLiteralLast(const std::set<LiteralIndex>& processed,
                                   int relevant_prefix_size,
                                   std::vector<Literal>* literals);
 
+// ============================================================================
+// Implementation.
+// ============================================================================
+
+template <typename URBG>
+inline void RandomizeDecisionHeuristic(URBG* random,
+                                       SatParameters* parameters) {
+#if !defined(__PORTABLE_PLATFORM__)
+  // Random preferred variable order.
+  const google::protobuf::EnumDescriptor* order_d =
+      SatParameters::VariableOrder_descriptor();
+  parameters->set_preferred_variable_order(
+      static_cast<SatParameters::VariableOrder>(
+          order_d->value(absl::Uniform(*random, 0, order_d->value_count()))
+              ->number()));
+
+  // Random polarity initial value.
+  const google::protobuf::EnumDescriptor* polarity_d =
+      SatParameters::Polarity_descriptor();
+  parameters->set_initial_polarity(static_cast<SatParameters::Polarity>(
+      polarity_d->value(absl::Uniform(*random, 0, polarity_d->value_count()))
+          ->number()));
+#endif  // __PORTABLE_PLATFORM__
+  // Other random parameters.
+  parameters->set_use_phase_saving(absl::Bernoulli(*random, 0.5));
+  parameters->set_random_polarity_ratio(absl::Bernoulli(*random, 0.5) ? 0.01
+                                                                      : 0.0);
+  parameters->set_random_branches_ratio(absl::Bernoulli(*random, 0.5) ? 0.01
+                                                                      : 0.0);
+}
+
 }  // namespace sat
 }  // namespace operations_research
 
diff --git a/ortools/util/time_limit.h b/ortools/util/time_limit.h
index 249540a113..5a2e449b73 100644
--- a/ortools/util/time_limit.h
+++ b/ortools/util/time_limit.h
@@ -244,7 +244,7 @@ class TimeLimit {
     external_boolean_as_limit_ = external_boolean_as_limit;
   }
 
-  // Returns the external boolean limit set by the previous call.
+  // Returns the current external Boolean limit.
   bool* ExternalBooleanAsLimit() const { return external_boolean_as_limit_; }
 
   // Sets new time limits. Note that this do not reset the running max nor