[CP-SAT] use precedences in completion time cuts; improve glue clause sharing

Author: lperron

ortools/sat/BUILD.bazel

@@ -2893,6 +2893,7 @@ cc_library(
         ":linear_constraint",
         ":linear_constraint_manager",
         ":model",
+        ":precedences",
         ":sat_base",
         ":sat_solver",
         ":scheduling_helpers",
@@ -3548,6 +3549,7 @@ cc_library(
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
         "@abseil-cpp//absl/container:flat_hash_set",
+        "@abseil-cpp//absl/container:inlined_vector",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/log:vlog_is_on",

ortools/sat/cp_model_solver.cc

@@ -1127,7 +1127,9 @@ class FullProblemSolver : public SubSolver {
         // Note that this is done after the loading, so we will never export
         // problem clauses.
         if (shared_->clauses != nullptr) {
-          const int id = shared_->clauses->RegisterNewId();
+          const int id = shared_->clauses->RegisterNewId(
+              /*may_terminate_early=*/stop_at_first_solution_ &&
+              local_model_.GetOrCreate<CpModelProto>()->has_objective());
           shared_->clauses->SetWorkerNameForId(id, local_model_.Name());
 
           RegisterClausesLevelZeroImport(id, shared_->clauses.get(),

ortools/sat/cp_model_solver_helpers.cc

@@ -953,27 +953,31 @@ void RegisterClausesExport(int id, SharedClausesManager* shared_clauses_manager,
   if (!model->GetOrCreate<SatParameters>()->share_glue_clauses()) {
     return;
   }
-  auto* clause_stream = shared_clauses_manager->GetClauseStream(id);
-  const int max_lbd =
-      model->GetOrCreate<SatParameters>()->clause_cleanup_lbd_bound();
-  // Note that this callback takes no global locks, everything operates on this
-  // worker's own clause stream, whose lock is only used by this worker, and
-  // briefly when generating a batch in SharedClausesManager::Synchronize().
-  auto share_clause = [mapping, clause_stream, max_lbd,
-                       clause = std::vector<int>()](
+  const double share_interval =
+      model->GetOrCreate<SatParameters>()->share_glue_clauses_dtime();
+  auto* clause_stream = model->GetOrCreate<UniqueClauseStream>();
+  auto* time_limit = model->GetOrCreate<TimeLimit>();
+  auto share_clause = [mapping, clause_stream, time_limit, id,
+                       shared_clauses_manager, share_interval,
+                       next_batch_dtime = -1.0, clause = std::vector<int>()](
                           int lbd, absl::Span<const Literal> literals) mutable {
-    if (lbd <= 0 || lbd > max_lbd ||
-        !clause_stream->CanAccept(literals.size(), lbd)) {
-      return;
+    if (literals.size() >= UniqueClauseStream::kMinClauseSize &&
+        literals.size() <= UniqueClauseStream::kMaxClauseSize) {
+      clause.clear();
+      for (const Literal& lit : literals) {
+        const int var =
+            mapping->GetProtoVariableFromBooleanVariable(lit.Variable());
+        if (var == -1) return;
+        clause.push_back(lit.IsPositive() ? var : NegatedRef(var));
+      }
+      clause_stream->Add(clause, lbd);
     }
-    clause.clear();
-    for (const Literal& lit : literals) {
-      const int var =
-          mapping->GetProtoVariableFromBooleanVariable(lit.Variable());
-      if (var == -1) return;
-      clause.push_back(lit.IsPositive() ? var : NegatedRef(var));
+    const double elapsed_dtime = time_limit->GetElapsedDeterministicTime();
+    if (next_batch_dtime < 0) next_batch_dtime = elapsed_dtime + share_interval;
+    if (elapsed_dtime >= next_batch_dtime) {
+      shared_clauses_manager->AddBatch(id, clause_stream->NextBatch());
+      next_batch_dtime = elapsed_dtime + share_interval;
     }
-    clause_stream->Add(clause);
   };
   model->GetOrCreate<ClauseManager>()->SetAddClauseCallback(
       std::move(share_clause));
@@ -994,16 +998,16 @@ int RegisterClausesLevelZeroImport(int id,
   auto* implications = model->GetOrCreate<BinaryImplicationGraph>();
   const bool share_glue_clauses =
       model->GetOrCreate<SatParameters>()->share_glue_clauses();
+  auto* clause_stream =
+      share_glue_clauses ? model->GetOrCreate<UniqueClauseStream>() : nullptr;
   const bool minimize_shared_clauses =
       model->GetOrCreate<SatParameters>()->minimize_shared_clauses();
-  auto* clause_stream = share_glue_clauses
-                            ? shared_clauses_manager->GetClauseStream(id)
-                            : nullptr;
   auto* clause_manager = model->GetOrCreate<ClauseManager>();
   const auto& import_level_zero_clauses = [shared_clauses_manager, id, mapping,
                                            sat_solver, implications,
-                                           clause_stream, clause_manager,
-                                           minimize_shared_clauses]() {
+                                           minimize_shared_clauses,
+                                           clause_stream,
+                                           clause_manager]() mutable {
     std::vector<std::pair<int, int>> new_binary_clauses;
     shared_clauses_manager->GetUnseenBinaryClauses(id, &new_binary_clauses);
     implications->EnableSharing(false);
@@ -1020,28 +1024,27 @@ int RegisterClausesLevelZeroImport(int id,
     int new_clauses = 0;
     std::array<Literal, UniqueClauseStream::kMaxClauseSize> local_clause;
     sat_solver->EnsureNewClauseIndexInitialized();
-    // Temporarily disable clause sharing so we don't immediately re-export the
-    // clauses we just imported.
+    // Temporarily disable clause sharing.
     auto callback = clause_manager->TakeAddClauseCallback();
-    for (const absl::Span<const int> shared_clause :
-         shared_clauses_manager->GetUnseenClauses(id)) {
-      // Check this clause was not already learned by this worker.
-      // We can delete the fingerprint because we should not learn an identical
-      // clause, and the global stream will not emit the same clause while any
-      // worker hasn't consumed this clause (and thus also shouldn't relearn the
-      // clause).
-      if (clause_stream->Delete(shared_clause)) continue;
-      for (int i = 0; i < shared_clause.size(); ++i) {
-        local_clause[i] = mapping->Literal(shared_clause[i]);
-      }
-      if (!sat_solver->AddProblemClause(
-              absl::MakeSpan(local_clause).subspan(0, shared_clause.size()))) {
-        return false;
+    while (true) {
+      auto batch = shared_clauses_manager->GetUnseenClauses(id);
+      if (batch.empty()) break;
+      for (int clause_index = 0; clause_index < batch.size(); ++clause_index) {
+        const absl::Span<const int>& shared_clause = batch[clause_index];
+        // Check this clause was not already learned by this worker.
+        if (!clause_stream->BlockClause(shared_clause)) continue;
+        ++new_clauses;
+        for (int i = 0; i < shared_clause.size(); ++i) {
+          local_clause[i] = mapping->Literal(shared_clause[i]);
+        }
+        if (!sat_solver->AddProblemClause(
+                absl::MakeSpan(local_clause)
+                    .subspan(0, shared_clause.size()))) {
+          return false;
+        }
       }
-      ++new_clauses;
     }
     clause_manager->SetAddClauseCallback(std::move(callback));
-    clause_stream->RemoveWorstClauses();
     if (minimize_shared_clauses && new_clauses > 0) {
       // The new clauses may be subsumed, so try to minimize them to reduce
       // overhead of sharing.
@@ -2110,8 +2113,7 @@ SharedClasses::SharedClasses(const CpModelProto* proto, Model* global_model)
       !params.interleave_search() || params.num_workers() <= 1;
   response->SetSynchronizationMode(always_synchronize);
   if (params.share_binary_clauses() && params.num_workers() > 1) {
-    clauses = std::make_unique<SharedClausesManager>(always_synchronize,
-                                                     absl::Seconds(1));
+    clauses = std::make_unique<SharedClausesManager>(always_synchronize);
   }
 }
 

ortools/sat/cp_model_solver_test.cc

@@ -87,9 +87,9 @@ TEST(LoadCpModelTest, PureSatProblem) {
 TEST(LoadCpModelTest, PureSatProblemWithLimit) {
   const CpModelProto model_proto = Random3SatProblem(500);
   LOG(INFO) << CpModelStats(model_proto);
-  Model model;
-  model.Add(NewSatParameters("max_deterministic_time:0.00001"));
-  const CpSolverResponse response = SolveCpModel(model_proto, &model);
+  SatParameters params;
+  params.set_max_deterministic_time(0.00001);
+  const CpSolverResponse response = SolveWithParameters(model_proto, params);
   EXPECT_EQ(response.status(), CpSolverStatus::UNKNOWN);
   LOG(INFO) << CpSolverResponseStats(response);
 }
@@ -193,7 +193,8 @@ TEST(LoadCpModelTest, SimpleCumulative) {
 }
 
 TEST(SolverCpModelTest, EmptyModel) {
-  const CpModelProto cp_model = ParseTestProto("solution_hint {}");
+  CpModelProto cp_model;
+  cp_model.mutable_solution_hint();
 
   SatParameters params;
   params.set_debug_crash_if_presolve_breaks_hint(true);
@@ -329,6 +330,7 @@ TEST(SolveCpModelTest, TrivialModelWithCore) {
                                         response.solution().end())));
 }
 
+#if !defined(__EMBEDDED_PLATFORM__)
 TEST(SolveCpModelTest, TrivialLinearTranslatedModel) {
   const CpModelProto model_proto = ParseTestProto(R"pb(
     variables { domain: -10 domain: 10 }
@@ -4803,6 +4805,7 @@ TEST(PresolveCpModelTest, CumulativeBug4) {
   response = SolveWithParameters(cp_model, params);
   EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
 }
+#endif  // !defined(__EMBEDDED_PLATFORM__)
 
 }  // namespace
 }  // namespace sat

ortools/sat/diffn.cc

@@ -32,7 +32,7 @@
 #include "absl/log/vlog_is_on.h"
 #include "absl/numeric/bits.h"
 #include "absl/types/span.h"
-#include "ortools/base/stl_util.h"
+// #include "ortools/base/stl_util.h"
 #include "ortools/sat/2d_mandatory_overlap_propagator.h"
 #include "ortools/sat/2d_orthogonal_packing.h"
 #include "ortools/sat/2d_try_edge_propagator.h"

ortools/sat/parameters_validation.cc

@@ -87,6 +87,7 @@ std::string ValidateParameters(const SatParameters& params) {
   TEST_IS_FINITE(relative_gap_limit);
   TEST_IS_FINITE(restart_dl_average_ratio);
   TEST_IS_FINITE(restart_lbd_average_ratio);
+  TEST_IS_FINITE(share_glue_clauses_dtime);
   TEST_IS_FINITE(shared_tree_open_leaves_per_worker);
   TEST_IS_FINITE(shaving_deterministic_time_in_probing_search);
   TEST_IS_FINITE(shaving_search_deterministic_time);
@@ -156,6 +157,7 @@ std::string ValidateParameters(const SatParameters& params) {
   TEST_NON_NEGATIVE(presolve_probing_deterministic_time_limit);
   TEST_NON_NEGATIVE(probing_deterministic_time_limit);
   TEST_NON_NEGATIVE(symmetry_detection_deterministic_time_limit);
+  TEST_POSITIVE(share_glue_clauses_dtime);
 
   if (params.enumerate_all_solutions() &&
       (params.num_search_workers() > 1 || params.num_workers() > 1)) {

ortools/sat/sat_parameters.proto

@@ -24,7 +24,7 @@ option java_multiple_files = true;
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 322
+// NEXT TAG: 323
 message SatParameters {
   // In some context, like in a portfolio of search, it makes sense to name a
   // given parameters set for logging purpose.
@@ -705,6 +705,9 @@ message SatParameters {
   // are imported.
   optional bool minimize_shared_clauses = 300 [default = true];
 
+  // The amount of dtime between each export of shared glue clauses.
+  optional double share_glue_clauses_dtime = 322 [default = 1.0];
+
   // ==========================================================================
   // Debugging parameters
   // ==========================================================================