[CP-SAT] stronger no_overlap_2d variation

Author: lperron

ortools/sat/BUILD.bazel

@@ -3570,6 +3570,7 @@ cc_library(
         ":synchronization",
         ":timetable",
         ":util",
+        "//ortools/base:stl_util",
         "//ortools/util:bitset",
         "//ortools/util:saturated_arithmetic",
         "//ortools/util:strong_integers",

ortools/sat/cp_model_search.cc

@@ -188,6 +188,7 @@ void AddExtraSchedulingPropagators(SatParameters& new_params) {
   new_params.set_use_energetic_reasoning_in_no_overlap_2d(true);
   new_params.set_use_area_energetic_reasoning_in_no_overlap_2d(true);
   new_params.set_use_try_edge_reasoning_in_no_overlap_2d(true);
+  new_params.set_no_overlap_2d_boolean_relations_limit(100);
 }
 
 // We want a random tie breaking among variables with equivalent values.

ortools/sat/diffn.cc

@@ -32,6 +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/sat/2d_distances_propagator.h"
 #include "ortools/sat/2d_mandatory_overlap_propagator.h"
 #include "ortools/sat/2d_orthogonal_packing.h"
@@ -276,11 +277,11 @@ void AddNonOverlappingRectangles(const std::vector<IntervalVariable>& x,
     DCHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
 
     for (int i = 0; i < num_boxes; ++i) {
-      if (repository->IsOptional(x[i])) continue;
-      if (repository->IsOptional(y[i])) continue;
+      if (repository->IsAbsent(x[i])) continue;
+      if (repository->IsAbsent(y[i])) continue;
       for (int j = i + 1; j < num_boxes; ++j) {
-        if (repository->IsOptional(x[j])) continue;
-        if (repository->IsOptional(y[j])) continue;
+        if (repository->IsAbsent(x[j])) continue;
+        if (repository->IsAbsent(y[j])) continue;
 
         // At most one of these two x options is true.
         const Literal x_ij = repository->GetOrCreatePrecedenceLiteral(
@@ -307,7 +308,21 @@ void AddNonOverlappingRectangles(const std::vector<IntervalVariable>& x,
         }
 
         // At least one of the 4 options is true.
-        if (!sat_solver->AddProblemClause({x_ij, x_ji, y_ij, y_ji})) {
+        std::vector<Literal> clause = {x_ij, x_ji, y_ij, y_ji};
+        if (repository->IsOptional(x[i])) {
+          clause.push_back(repository->PresenceLiteral(x[i]).Negated());
+        }
+        if (repository->IsOptional(y[i])) {
+          clause.push_back(repository->PresenceLiteral(y[i]).Negated());
+        }
+        if (repository->IsOptional(x[j])) {
+          clause.push_back(repository->PresenceLiteral(x[j]).Negated());
+        }
+        if (repository->IsOptional(y[j])) {
+          clause.push_back(repository->PresenceLiteral(y[j]).Negated());
+        }
+        gtl::STLSortAndRemoveDuplicates(&clause);
+        if (!sat_solver->AddProblemClause(clause)) {
           return;
         }
       }