[CP-SAT] experimental routing cuts; new cumulative cuts; improve no_overlap_2d code all around

Author: lperron

ortools/sat/BUILD.bazel

@@ -1790,7 +1790,6 @@ cc_library(
         "//ortools/util:sort",
         "//ortools/util:strong_integers",
         "@com_google_absl//absl/base:core_headers",
-        "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/log:check",
         "@com_google_absl//absl/meta:type_traits",
         "@com_google_absl//absl/strings",
@@ -2368,12 +2367,14 @@ cc_library(
         ":cp_model_utils",
         ":cuts",
         ":diffn_cuts",
+        ":diffn_util",
         ":implied_bounds",
         ":integer",
         ":integer_base",
         ":integer_expr",
         ":intervals",
         ":linear_constraint",
+        ":linear_constraint_manager",
         ":model",
         ":no_overlap_2d_helper",
         ":precedences",
@@ -2653,16 +2654,19 @@ cc_library(
         ":linear_constraint",
         ":linear_constraint_manager",
         ":model",
+        ":precedences",
         ":sat_base",
         "//ortools/base",
         "//ortools/base:mathutil",
         "//ortools/base:strong_vector",
-        "//ortools/graph",
         "//ortools/graph:max_flow",
         "//ortools/util:strong_integers",
+        "@com_google_absl//absl/algorithm:container",
         "@com_google_absl//absl/cleanup",
+        "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/container:flat_hash_set",
         "@com_google_absl//absl/log:check",
+        "@com_google_absl//absl/random:distributions",
         "@com_google_absl//absl/strings",
         "@com_google_absl//absl/types:span",
     ],
@@ -2678,12 +2682,14 @@ cc_test(
         ":linear_constraint",
         ":linear_constraint_manager",
         ":model",
+        ":precedences",
         ":routing_cuts",
         ":sat_base",
         "//ortools/base:gmock_main",
         "//ortools/base:strong_vector",
         "//ortools/graph:max_flow",
         "//ortools/util:strong_integers",
+        "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/log",
         "@com_google_absl//absl/random",
         "@com_google_absl//absl/random:distributions",
@@ -2704,6 +2710,7 @@ cc_library(
         ":linear_constraint_manager",
         ":model",
         ":sat_base",
+        ":scheduling_helpers",
         ":util",
         "//ortools/base",
         "//ortools/base:stl_util",
@@ -3094,6 +3101,7 @@ cc_library(
         "//ortools/graph:strongly_connected_components",
         "//ortools/util:fixed_shape_binary_tree",
         "//ortools/util:integer_pq",
+        "//ortools/util:saturated_arithmetic",
         "//ortools/util:strong_integers",
         "@com_google_absl//absl/algorithm:container",
         "@com_google_absl//absl/container:btree",

ortools/sat/cp_model_expand.cc

@@ -892,7 +892,9 @@ void LinkLiteralsAndValues(const std::vector<int>& literals,
   for (const auto& [encoding_lit, support] : encoding_lit_to_support) {
     CHECK(!support.empty());
     if (support.size() == 1) {
-      context->StoreBooleanEqualityRelation(encoding_lit, support[0]);
+      if (!context->StoreBooleanEqualityRelation(encoding_lit, support[0])) {
+        return;
+      }
     } else {
       BoolArgumentProto* bool_or =
           context->working_model->add_constraints()->mutable_bool_or();
@@ -979,6 +981,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
     std::vector<int64_t> in_states;
     std::vector<int64_t> labels;
     std::vector<int64_t> out_states;
+    absl::flat_hash_set<int64_t> still_reachable_after_domain_change;
     for (int i = 0; i < proto.transition_label_size(); ++i) {
       const int64_t tail = proto.transition_tail(i);
       const int64_t label = proto.transition_label(i);
@@ -988,6 +991,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
       if (!reachable_states[time + 1].contains(head)) continue;
       if (!context->DomainContains(proto.exprs(time), label)) continue;
 
+      still_reachable_after_domain_change.insert(head);
       // TODO(user): if this transition correspond to just one in-state or
       // one-out state or one variable value, we could reuse the corresponding
       // Boolean variable instead of creating a new one!
@@ -999,6 +1003,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
       out_states.push_back(time + 1 == n ? 0 : head);
     }
 
+    reachable_states[time + 1] = still_reachable_after_domain_change;
+
     // Deal with single tuple.
     const int num_tuples = in_states.size();
     if (num_tuples == 1) {
@@ -1013,10 +1019,9 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
       // at false.
       std::vector<int> at_false;
       for (const auto [value, literal] : in_encoding) {
-        if (value != in_states[0]) at_false.push_back(literal);
-      }
-      for (const int literal : at_false) {
-        if (!context->SetLiteralToFalse(literal)) return;
+        if (value != in_states[0]) {
+          if (!context->SetLiteralToFalse(literal)) return;
+        }
       }
 
       in_encoding.clear();

ortools/sat/cp_model_lns.cc

@@ -951,22 +951,23 @@ NeighborhoodGeneratorHelper::GetSchedulingPrecedences(
 }
 
 std::vector<std::vector<int>>
-NeighborhoodGeneratorHelper::GetRoutingPathLiterals(
+NeighborhoodGeneratorHelper::GetRoutingPathBooleanVariables(
     const CpSolverResponse& initial_solution) const {
-  struct HeadAndArcLiteral {
+  struct HeadAndArcBooleanVariable {
     int head;
-    int literal;
+    int bool_var;
   };
 
   std::vector<std::vector<int>> result;
-  absl::flat_hash_map<int, HeadAndArcLiteral> tail_to_head_and_arc_literal;
+  absl::flat_hash_map<int, HeadAndArcBooleanVariable>
+      tail_to_head_and_arc_bool_var;
 
   for (const int i : TypeToConstraints(ConstraintProto::kCircuit)) {
     const CircuitConstraintProto& ct = ModelProto().constraints(i).circuit();
 
     // Collect arcs.
     int min_node = std::numeric_limits<int>::max();
-    tail_to_head_and_arc_literal.clear();
+    tail_to_head_and_arc_bool_var.clear();
     for (int i = 0; i < ct.literals_size(); ++i) {
       const int literal = ct.literals(i);
       const int head = ct.heads(i);
@@ -977,27 +978,27 @@ NeighborhoodGeneratorHelper::GetRoutingPathLiterals(
       if (RefIsPositive(literal) == (value == 0)) continue;
       // Ignore self loops.
       if (head == tail) continue;
-      tail_to_head_and_arc_literal[tail] = {head, bool_var};
+      tail_to_head_and_arc_bool_var[tail] = {head, bool_var};
       min_node = std::min(tail, min_node);
     }
-    if (tail_to_head_and_arc_literal.empty()) continue;
+    if (tail_to_head_and_arc_bool_var.empty()) continue;
 
     // Unroll the path.
     int current_node = min_node;
     std::vector<int> path;
     do {
-      auto it = tail_to_head_and_arc_literal.find(current_node);
-      CHECK(it != tail_to_head_and_arc_literal.end());
+      auto it = tail_to_head_and_arc_bool_var.find(current_node);
+      CHECK(it != tail_to_head_and_arc_bool_var.end());
       current_node = it->second.head;
-      path.push_back(it->second.literal);
+      path.push_back(it->second.bool_var);
     } while (current_node != min_node);
     result.push_back(std::move(path));
   }
 
-  std::vector<HeadAndArcLiteral> route_starts;
+  std::vector<HeadAndArcBooleanVariable> route_starts;
   for (const int i : TypeToConstraints(ConstraintProto::kRoutes)) {
     const RoutesConstraintProto& ct = ModelProto().constraints(i).routes();
-    tail_to_head_and_arc_literal.clear();
+    tail_to_head_and_arc_bool_var.clear();
     route_starts.clear();
 
     // Collect route starts and arcs.
@@ -1014,20 +1015,20 @@ NeighborhoodGeneratorHelper::GetRoutingPathLiterals(
       if (tail == 0) {
         route_starts.push_back({head, bool_var});
       } else {
-        tail_to_head_and_arc_literal[tail] = {head, bool_var};
+        tail_to_head_and_arc_bool_var[tail] = {head, bool_var};
       }
     }
 
     // Unroll all routes.
-    for (const HeadAndArcLiteral& head_var : route_starts) {
+    for (const HeadAndArcBooleanVariable& head_var : route_starts) {
       std::vector<int> path;
       int current_node = head_var.head;
-      path.push_back(head_var.literal);
+      path.push_back(head_var.bool_var);
       do {
-        auto it = tail_to_head_and_arc_literal.find(current_node);
-        CHECK(it != tail_to_head_and_arc_literal.end());
+        auto it = tail_to_head_and_arc_bool_var.find(current_node);
+        CHECK(it != tail_to_head_and_arc_bool_var.end());
         current_node = it->second.head;
-        path.push_back(it->second.literal);
+        path.push_back(it->second.bool_var);
       } while (current_node != 0);
       result.push_back(std::move(path));
     }
@@ -2598,39 +2599,50 @@ Neighborhood RoutingRandomNeighborhoodGenerator::Generate(
     const CpSolverResponse& initial_solution, SolveData& data,
     absl::BitGenRef random) {
   const std::vector<std::vector<int>> all_paths =
-      helper_.GetRoutingPathLiterals(initial_solution);
+      helper_.GetRoutingPathBooleanVariables(initial_solution);
 
   // Collect all unique variables.
-  absl::flat_hash_set<int> all_path_variables;
-  for (auto& path : all_paths) {
-    all_path_variables.insert(path.begin(), path.end());
+  std::vector<int> variables_to_fix;
+  for (const auto& path : all_paths) {
+    variables_to_fix.insert(variables_to_fix.end(), path.begin(), path.end());
   }
-  std::vector<int> fixed_variables(all_path_variables.begin(),
-                                   all_path_variables.end());
-  std::sort(fixed_variables.begin(), fixed_variables.end());
-  GetRandomSubset(1.0 - data.difficulty, &fixed_variables, random);
+  gtl::STLSortAndRemoveDuplicates(&variables_to_fix);
+  GetRandomSubset(1.0 - data.difficulty, &variables_to_fix, random);
 
   Bitset64<int> to_fix(helper_.NumVariables());
-  for (const int var : fixed_variables) to_fix.Set(var);
+  for (const int var : variables_to_fix) to_fix.Set(var);
   return helper_.FixGivenVariables(initial_solution, to_fix);
 }
 
 Neighborhood RoutingPathNeighborhoodGenerator::Generate(
     const CpSolverResponse& initial_solution, SolveData& data,
     absl::BitGenRef random) {
   std::vector<std::vector<int>> all_paths =
-      helper_.GetRoutingPathLiterals(initial_solution);
+      helper_.GetRoutingPathBooleanVariables(initial_solution);
+
+  // Remove a corner case where all paths are empty.
+  if (all_paths.empty()) {
+    return helper_.NoNeighborhood();
+  }
 
   // Collect all unique variables.
-  absl::flat_hash_set<int> all_path_variables;
+  std::vector<int> all_path_variables;
+  int sum_of_path_sizes = 0;
+  for (const auto& path : all_paths) {
+    sum_of_path_sizes += path.size();
+  }
+  all_path_variables.reserve(sum_of_path_sizes);
   for (const auto& path : all_paths) {
-    all_path_variables.insert(path.begin(), path.end());
+    all_path_variables.insert(all_path_variables.end(), path.begin(),
+                              path.end());
   }
+  gtl::STLSortAndRemoveDuplicates(&all_path_variables);
 
-  // Select variables to relax.
+  // Select target number of variables to relax.
   const int num_variables_to_relax =
       static_cast<int>(all_path_variables.size() * data.difficulty);
   absl::flat_hash_set<int> relaxed_variables;
+
   while (relaxed_variables.size() < num_variables_to_relax) {
     DCHECK(!all_paths.empty());
     const int path_index = absl::Uniform<int>(random, 0, all_paths.size());
@@ -2665,57 +2677,54 @@ Neighborhood RoutingFullPathNeighborhoodGenerator::Generate(
     const CpSolverResponse& initial_solution, SolveData& data,
     absl::BitGenRef random) {
   std::vector<std::vector<int>> all_paths =
-      helper_.GetRoutingPathLiterals(initial_solution);
+      helper_.GetRoutingPathBooleanVariables(initial_solution);
+
   // Remove a corner case where all paths are empty.
   if (all_paths.empty()) {
     return helper_.NoNeighborhood();
   }
 
   // Collect all unique variables.
-  absl::flat_hash_set<int> all_path_variables;
+  std::vector<int> all_path_variables;
+  int sum_of_path_sizes = 0;
   for (const auto& path : all_paths) {
-    all_path_variables.insert(path.begin(), path.end());
+    sum_of_path_sizes += path.size();
   }
+  all_path_variables.reserve(sum_of_path_sizes);
+  for (const auto& path : all_paths) {
+    all_path_variables.insert(all_path_variables.end(), path.begin(),
+                              path.end());
+  }
+  gtl::STLSortAndRemoveDuplicates(&all_path_variables);
 
-  // Select variables to relax.
+  // Select target number of variables to relax.
   const int num_variables_to_relax =
       static_cast<int>(all_path_variables.size() * data.difficulty);
   absl::flat_hash_set<int> relaxed_variables;
 
   // Relax the start and end of each path to ease relocation.
+  // TODO(user): Restrict this if the difficulty is very low.
   for (const auto& path : all_paths) {
     relaxed_variables.insert(path.front());
     relaxed_variables.insert(path.back());
   }
 
-  // Randomize paths.
-  for (auto& path : all_paths) {
-    std::shuffle(path.begin(), path.end(), random);
-  }
-
-  // Relax all variables (if possible) in one random path.
-  const int path_to_clean = absl::Uniform<int>(random, 0, all_paths.size());
+  // Relax all variables, if possible, of one random path.
+  const int path_index = absl::Uniform<int>(random, 0, all_paths.size());
+  std::shuffle(all_paths[path_index].begin(), all_paths[path_index].end(),
+               random);
   while (relaxed_variables.size() < num_variables_to_relax &&
-         !all_paths[path_to_clean].empty()) {
-    relaxed_variables.insert(all_paths[path_to_clean].back());
-    all_paths[path_to_clean].pop_back();
-  }
-  if (all_paths[path_to_clean].empty()) {
-    std::swap(all_paths[path_to_clean], all_paths.back());
-    all_paths.pop_back();
+         !all_paths[path_index].empty()) {
+    relaxed_variables.insert(all_paths[path_index].back());
+    all_paths[path_index].pop_back();
   }
 
   // Relax more variables until the target is reached.
-  while (relaxed_variables.size() < num_variables_to_relax) {
-    DCHECK(!all_paths.empty());
-    const int path_index = absl::Uniform<int>(random, 0, all_paths.size());
-    relaxed_variables.insert(all_paths[path_index].back());
-
-    // Remove variable and clean up empty paths.
-    all_paths[path_index].pop_back();
-    if (all_paths[path_index].empty()) {
-      std::swap(all_paths[path_index], all_paths.back());
-      all_paths.pop_back();
+  if (relaxed_variables.size() < num_variables_to_relax) {
+    std::shuffle(all_path_variables.begin(), all_path_variables.end(), random);
+    while (relaxed_variables.size() < num_variables_to_relax) {
+      relaxed_variables.insert(all_path_variables.back());
+      all_path_variables.pop_back();
     }
   }
 

ortools/sat/cp_model_lns.h

@@ -247,12 +247,13 @@ class NeighborhoodGeneratorHelper : public SubSolver {
   // cumulative, or as a dimension of a no_overlap_2d constraint.
   std::vector<std::vector<int>> GetUniqueIntervalSets() const;
 
-  // Returns one sub-vector per circuit or per single vehicle circuit in a
+  // Returns one sub-vector per circuit or per individual vehicle circuit in a
   // routes constraints. Each circuit is non empty, and does not contain any
   // self-looping arcs. Path are sorted, starting from the arc with the lowest
   // tail index, and going in sequence up to the last arc before the circuit is
-  // closed. Each entry correspond to the arc literal on the circuit.
-  std::vector<std::vector<int>> GetRoutingPathLiterals(
+  // closed. Each entry correspond to the Boolean variable of the arc literal on
+  // the circuit.
+  std::vector<std::vector<int>> GetRoutingPathBooleanVariables(
       const CpSolverResponse& initial_solution) const;
 
   // Returns all precedences extracted from the scheduling constraint and the
@@ -818,7 +819,7 @@ class RoutingPathNeighborhoodGenerator : public NeighborhoodGenerator {
                         SolveData& data, absl::BitGenRef random) final;
 };
 
-// This routing based LNS generator aims are relaxing one full path, and make
+// This routing based LNS generator aims at relaxing one full path, and make
 // some room on the other paths to absorb the nodes of the relaxed path.
 //
 // In order to do so, it will relax the first and the last arc of each path in