update sat runner for pbo competition

Author: lperron

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

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