[CP-SAT] improve diffn clustering; more work on hints

Author: lperron

ortools/sat/BUILD.bazel

@@ -1231,6 +1231,7 @@ cc_library(
         ":pb_constraint",
         ":sat_base",
         ":sat_parameters_cc_proto",
+        ":synchronization",
         ":util",
         "//ortools/base",
         "//ortools/base:strong_vector",
@@ -2601,16 +2602,10 @@ cc_library(
         ":model",
         ":sat_base",
         ":util",
-        "//ortools/base",
         "//ortools/base:stl_util",
         "//ortools/base:strong_vector",
-        "//ortools/util:saturated_arithmetic",
-        "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
-        "//ortools/util:time_limit",
         "@com_google_absl//absl/base:core_headers",
-        "@com_google_absl//absl/container:btree",
-        "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/log:check",
         "@com_google_absl//absl/strings",
         "@com_google_absl//absl/types:span",
@@ -3160,6 +3155,7 @@ cc_library(
         ":util",
         "//ortools/util:saturated_arithmetic",
         "//ortools/util:strong_integers",
+        "//ortools/util:time_limit",
         "@com_google_absl//absl/container:flat_hash_set",
         "@com_google_absl//absl/container:inlined_vector",
         "@com_google_absl//absl/log",

ortools/sat/cp_model_presolve.cc

@@ -5882,14 +5882,14 @@ bool CpModelPresolver::PresolveNoOverlap2D(int /*c*/, ConstraintProto* ct) {
       indexed_intervals.push_back({x, IntegerValue(context_->StartMin(y)),
                                    IntegerValue(context_->EndMax(y))});
     }
-    std::vector<std::vector<int>> no_overlaps;
-    ConstructOverlappingSets(/*already_sorted=*/false, &indexed_intervals,
-                             &no_overlaps);
-    for (const std::vector<int>& no_overlap : no_overlaps) {
+    CompactVectorVector<int> no_overlaps;
+    absl::c_sort(indexed_intervals, IndexedInterval::ComparatorByStart());
+    ConstructOverlappingSets(absl::MakeSpan(indexed_intervals), &no_overlaps);
+    for (int i = 0; i < no_overlaps.size(); ++i) {
       ConstraintProto* new_ct = context_->working_model->add_constraints();
       // Unfortunately, the Assign() method does not work in or-tools as the
       // protobuf int32_t type is not the int type.
-      for (const int i : no_overlap) {
+      for (const int i : no_overlaps[i]) {
         new_ct->mutable_no_overlap()->add_intervals(i);
       }
     }

ortools/sat/cp_model_search.cc

@@ -704,6 +704,13 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
     new_params.set_optimize_with_lb_tree_search(false);
     new_params.set_optimize_with_max_hs(false);
 
+    // Given that each workers work on a different part of the subtree, it might
+    // not be a good idea to try to work on a global shared solution.
+    //
+    // TODO(user): Experiments more here, in particular we could follow it if
+    // it falls into the current subtree.
+    new_params.set_polarity_exploit_ls_hints(false);
+
     strategies["shared_tree"] = new_params;
   }
 

ortools/sat/cp_model_solver.cc

@@ -682,12 +682,13 @@ void LogFinalStatistics(SharedClasses* shared) {
   shared->logger->FlushPendingThrottledLogs(/*ignore_rates=*/true);
   SOLVER_LOG(shared->logger, "");
 
-  shared->stat_tables.Display(shared->logger);
+  shared->stat_tables->Display(shared->logger);
   shared->response->DisplayImprovementStatistics();
 
   std::vector<std::vector<std::string>> table;
   table.push_back({"Solution repositories", "Added", "Queried", "Synchro"});
   table.push_back(shared->response->SolutionsRepository().TableLineStats());
+  table.push_back(shared->ls_hints->TableLineStats());
   if (shared->lp_solutions != nullptr) {
     table.push_back(shared->lp_solutions->TableLineStats());
   }
@@ -914,35 +915,9 @@ class FullProblemSolver : public SubSolver {
               shared_->response->first_solution_solvers_should_stop());
     }
 
-    if (shared->response != nullptr) {
-      local_model_.Register<SharedResponseManager>(shared->response);
-    }
-
-    if (shared->lp_solutions != nullptr) {
-      local_model_.Register<SharedLPSolutionRepository>(
-          shared->lp_solutions.get());
-    }
-
-    if (shared->incomplete_solutions != nullptr) {
-      local_model_.Register<SharedIncompleteSolutionManager>(
-          shared->incomplete_solutions.get());
-    }
-
-    if (shared->bounds != nullptr) {
-      local_model_.Register<SharedBoundsManager>(shared->bounds.get());
-    }
-
-    if (shared->clauses != nullptr) {
-      local_model_.Register<SharedClausesManager>(shared->clauses.get());
-    }
-
-    if (local_parameters.use_shared_tree_search()) {
-      local_model_.Register<SharedTreeManager>(shared->shared_tree_manager);
-    }
-
     // TODO(user): For now we do not count LNS statistics. We could easily
     // by registering the SharedStatistics class with LNS local model.
-    local_model_.Register<SharedStatistics>(shared_->stats);
+    shared_->RegisterSharedClassesInLocalModel(&local_model_);
 
     // Setup the local logger, in multi-thread log_search_progress should be
     // false by default, but we might turn it on for debugging. It is on by
@@ -956,10 +931,10 @@ class FullProblemSolver : public SubSolver {
     CpSolverResponse response;
     shared_->response->FillSolveStatsInResponse(&local_model_, &response);
     shared_->response->AppendResponseToBeMerged(response);
-    shared_->stat_tables.AddTimingStat(*this);
-    shared_->stat_tables.AddLpStat(name(), &local_model_);
-    shared_->stat_tables.AddSearchStat(name(), &local_model_);
-    shared_->stat_tables.AddClausesStat(name(), &local_model_);
+    shared_->stat_tables->AddTimingStat(*this);
+    shared_->stat_tables->AddLpStat(name(), &local_model_);
+    shared_->stat_tables->AddSearchStat(name(), &local_model_);
+    shared_->stat_tables->AddClausesStat(name(), &local_model_);
   }
 
   bool IsDone() override {
@@ -1104,30 +1079,11 @@ class FeasibilityPumpSolver : public SubSolver {
     *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
     shared_->time_limit->UpdateLocalLimit(
         local_model_->GetOrCreate<TimeLimit>());
-
-    if (shared->response != nullptr) {
-      local_model_->Register<SharedResponseManager>(shared->response);
-    }
-
-    if (shared->lp_solutions != nullptr) {
-      local_model_->Register<SharedLPSolutionRepository>(
-          shared->lp_solutions.get());
-    }
-
-    if (shared->incomplete_solutions != nullptr) {
-      local_model_->Register<SharedIncompleteSolutionManager>(
-          shared->incomplete_solutions.get());
-    }
-
-    // Level zero variable bounds sharing.
-    if (shared_->bounds != nullptr) {
-      RegisterVariableBoundsLevelZeroImport(
-          shared_->model_proto, shared_->bounds.get(), local_model_.get());
-    }
+    shared_->RegisterSharedClassesInLocalModel(local_model_.get());
   }
 
   ~FeasibilityPumpSolver() override {
-    shared_->stat_tables.AddTimingStat(*this);
+    shared_->stat_tables->AddTimingStat(*this);
   }
 
   bool IsDone() override { return shared_->SearchIsDone(); }
@@ -1216,8 +1172,8 @@ class LnsSolver : public SubSolver {
         shared_(shared) {}
 
   ~LnsSolver() override {
-    shared_->stat_tables.AddTimingStat(*this);
-    shared_->stat_tables.AddLnsStat(
+    shared_->stat_tables->AddTimingStat(*this);
+    shared_->stat_tables->AddLnsStat(
         name(),
         /*num_fully_solved_calls=*/generator_->num_fully_solved_calls(),
         /*num_calls=*/generator_->num_calls(),
@@ -1654,6 +1610,7 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
       "synchronization_agent", [shared]() {
         shared->response->Synchronize();
         shared->response->MutableSolutionsRepository()->Synchronize();
+        shared->ls_hints->Synchronize();
         if (shared->bounds != nullptr) {
           shared->bounds->Synchronize();
         }
@@ -1946,7 +1903,7 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
 
     if (num_ls_default > 0) {
       std::shared_ptr<SharedLsStates> states = std::make_shared<SharedLsStates>(
-          ls_name, params, &shared->stat_tables);
+          ls_name, params, shared->stat_tables);
       for (int i = 0; i < num_ls_default; ++i) {
         SatParameters local_params = params;
         local_params.set_random_seed(
@@ -1956,14 +1913,15 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
             std::make_unique<FeasibilityJumpSolver>(
                 ls_name, SubSolver::INCOMPLETE, get_linear_model(),
                 local_params, states, shared->time_limit, shared->response,
-                shared->bounds.get(), shared->stats, &shared->stat_tables));
+                shared->bounds.get(), shared->ls_hints, shared->stats,
+                shared->stat_tables));
       }
     }
 
     if (num_ls_lin > 0) {
       std::shared_ptr<SharedLsStates> lin_states =
           std::make_shared<SharedLsStates>(lin_ls_name, params,
-                                           &shared->stat_tables);
+                                           shared->stat_tables);
       for (int i = 0; i < num_ls_lin; ++i) {
         SatParameters local_params = params;
         local_params.set_random_seed(
@@ -1973,7 +1931,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
             std::make_unique<FeasibilityJumpSolver>(
                 lin_ls_name, SubSolver::INCOMPLETE, get_linear_model(),
                 local_params, lin_states, shared->time_limit, shared->response,
-                shared->bounds.get(), shared->stats, &shared->stat_tables));
+                shared->bounds.get(), shared->ls_hints, shared->stats,
+                shared->stat_tables));
       }
     }
   }
@@ -2011,13 +1970,13 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
         if (local_params.feasibility_jump_linearization_level() == 0) {
           if (fj_states == nullptr) {
             fj_states = std::make_shared<SharedLsStates>(
-                local_params.name(), params, &shared->stat_tables);
+                local_params.name(), params, shared->stat_tables);
           }
           states = fj_states;
         } else {
           if (fj_lin_states == nullptr) {
             fj_lin_states = std::make_shared<SharedLsStates>(
-                local_params.name(), params, &shared->stat_tables);
+                local_params.name(), params, shared->stat_tables);
           }
           states = fj_lin_states;
         }
@@ -2026,8 +1985,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
             std::make_unique<FeasibilityJumpSolver>(
                 local_params.name(), SubSolver::FIRST_SOLUTION,
                 get_linear_model(), local_params, states, shared->time_limit,
-                shared->response, shared->bounds.get(), shared->stats,
-                &shared->stat_tables));
+                shared->response, shared->bounds.get(), shared->ls_hints,
+                shared->stats, shared->stat_tables));
       } else {
         first_solution_full_subsolvers.push_back(
             std::make_unique<FullProblemSolver>(

ortools/sat/cp_model_solver_helpers.cc

@@ -1971,8 +1971,10 @@ SharedClasses::SharedClasses(const CpModelProto* proto, Model* global_model)
       time_limit(global_model->GetOrCreate<ModelSharedTimeLimit>()),
       logger(global_model->GetOrCreate<SolverLogger>()),
       stats(global_model->GetOrCreate<SharedStatistics>()),
+      stat_tables(global_model->GetOrCreate<SharedStatTables>()),
       response(global_model->GetOrCreate<SharedResponseManager>()),
-      shared_tree_manager(global_model->GetOrCreate<SharedTreeManager>()) {
+      shared_tree_manager(global_model->GetOrCreate<SharedTreeManager>()),
+      ls_hints(global_model->GetOrCreate<SharedLsSolutionRepository>()) {
   const SatParameters& params = *global_model->GetOrCreate<SatParameters>();
 
   if (params.share_level_zero_bounds()) {
@@ -2007,6 +2009,31 @@ SharedClasses::SharedClasses(const CpModelProto* proto, Model* global_model)
   }
 }
 
+void SharedClasses::RegisterSharedClassesInLocalModel(Model* local_model) {
+  // Note that we do not register the logger which is not a shared class.
+  local_model->Register<SharedResponseManager>(response);
+  local_model->Register<SharedLsSolutionRepository>(ls_hints);
+  local_model->Register<SharedTreeManager>(shared_tree_manager);
+  local_model->Register<SharedStatistics>(stats);
+  local_model->Register<SharedStatTables>(stat_tables);
+
+  // TODO(user): Use parameters and not the presence/absence of these class
+  // to decide when to use them.
+  if (lp_solutions != nullptr) {
+    local_model->Register<SharedLPSolutionRepository>(lp_solutions.get());
+  }
+  if (incomplete_solutions != nullptr) {
+    local_model->Register<SharedIncompleteSolutionManager>(
+        incomplete_solutions.get());
+  }
+  if (bounds != nullptr) {
+    local_model->Register<SharedBoundsManager>(bounds.get());
+  }
+  if (clauses != nullptr) {
+    local_model->Register<SharedClausesManager>(clauses.get());
+  }
+}
+
 bool SharedClasses::SearchIsDone() {
   if (response->ProblemIsSolved()) {
     // This is for cases where the time limit is checked more often.

ortools/sat/cp_model_solver_helpers.h

@@ -56,17 +56,20 @@ struct SharedClasses {
   ModelSharedTimeLimit* const time_limit;
   SolverLogger* const logger;
   SharedStatistics* const stats;
+  SharedStatTables* const stat_tables;
   SharedResponseManager* const response;
   SharedTreeManager* const shared_tree_manager;
+  SharedLsSolutionRepository* const ls_hints;
 
   // These can be nullptr depending on the options.
   std::unique_ptr<SharedBoundsManager> bounds;
   std::unique_ptr<SharedLPSolutionRepository> lp_solutions;
   std::unique_ptr<SharedIncompleteSolutionManager> incomplete_solutions;
   std::unique_ptr<SharedClausesManager> clauses;
 
-  // For displaying summary at the end.
-  SharedStatTables stat_tables;
+  // call local_model->Register() on most of the class here, this allow to
+  // more easily depends on one of the shared class deep within the solver.
+  void RegisterSharedClassesInLocalModel(Model* local_model);
 
   bool SearchIsDone();
 };