From 89b85436fd670288eb39d7a19c49510a3828945d Mon Sep 17 00:00:00 2001
From: Laurent Perron <lperron@google.com>
Date: Thu, 17 Apr 2025 16:23:03 +0200
Subject: [PATCH] update sat runner for pbo competition

---
 ortools/sat/cp_model_solver.cc |  7 +++++++
 ortools/sat/sat_runner.cc      | 25 +++++++++++++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 1c064451ae..d22edce2b4 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -2140,6 +2140,13 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
       --num_thread_available;
     }
     num_thread_available = std::max(num_thread_available, 0);
+    // If we are in interleaved mode with one worker, num_thread_available is
+    // always negative. We force it to 1 so that we at least have a
+    // feasibility_jump subsolver.
+    if (params.interleave_search() && params.num_workers() == 1) {
+      // TODO(user): the 1 should be a parameter.
+      num_thread_available = 1;
+    }
 
     const std::vector<SatParameters> all_params =
         RepeatParameters(name_filter.Filter(GetFirstSolutionBaseParams(params)),
diff --git a/ortools/sat/sat_runner.cc b/ortools/sat/sat_runner.cc
index 24625b05eb..1fd4b5f0c3 100644
--- a/ortools/sat/sat_runner.cc
+++ b/ortools/sat/sat_runner.cc
@@ -77,6 +77,8 @@ ABSL_FLAG(bool, fingerprint_intermediate_solutions, false,
           "Attach the fingerprint of intermediate solutions to the output.");
 ABSL_FLAG(bool, competition_mode, false,
           "If true, output the log in a competition format.");
+ABSL_FLAG(bool, force_interleave_search, false,
+          "If true, enable interleaved workers when num_workers is 1.");
 
 namespace operations_research {
 namespace sat {
@@ -169,6 +171,26 @@ void LogInPbCompetitionFormat(int num_variables, bool has_objective,
       final_response_callback);
 }
 
+void SetInterleavedWorkers(bool has_objective, SatParameters* parameters) {
+  // Enable interleaved workers when num_workers is 1.
+  if (parameters->num_workers() == 1) {
+    parameters->set_interleave_search(true);
+    parameters->set_use_rins_lns(false);
+    if (has_objective) {
+      parameters->add_subsolvers("default_lp");
+      parameters->add_subsolvers("quick_restart");
+      parameters->add_subsolvers("core_or_no_lp");
+      parameters->add_subsolvers("max_lp");
+      parameters->set_num_violation_ls(1);
+    } else {
+      parameters->add_subsolvers("default_lp");
+      parameters->add_subsolvers("no_lp");
+      parameters->add_subsolvers("max_lp");
+      parameters->add_subsolvers("quick_restart");
+    }
+  }
+}
+
 bool LoadProblem(const std::string& filename, absl::string_view hint_file,
                  absl::string_view domain_file, CpModelProto* cp_model,
                  Model* model, SatParameters* parameters) {
@@ -204,6 +226,9 @@ bool LoadProblem(const std::string& filename, absl::string_view hint_file,
       LogInPbCompetitionFormat(num_variables, cp_model->has_objective(), model,
                                parameters);
     }
+    if (absl::GetFlag(FLAGS_force_interleave_search)) {
+      SetInterleavedWorkers(cp_model->has_objective(), parameters);
+    }
   } else if (absl::EndsWith(filename, ".cnf") ||
              absl::EndsWith(filename, ".cnf.xz") ||
              absl::EndsWith(filename, ".cnf.gz") ||