[CP-SAT] experiment with prefered linearization_level in lns; fuzzer bugs fixed

Author: lperron

ortools/sat/cp_model_copy.cc

@@ -119,7 +119,9 @@ bool ModelCopy::ImportAndSimplifyConstraints(
         }
         break;
       case ConstraintProto::kLinear:
-        if (!CopyLinear(ct)) return CreateUnsatModel(c, ct);
+        if (!CopyLinear(ct, /*canonicalize=*/first_copy)) {
+          return CreateUnsatModel(c, ct);
+        }
         break;
       case ConstraintProto::kIntProd:
         if (!CopyIntProd(ct, ignore_names)) return CreateUnsatModel(c, ct);
@@ -407,8 +409,9 @@ bool ModelCopy::CopyBoolAndWithDupSupport(const ConstraintProto& ct) {
   return true;
 }
 
-bool ModelCopy::CopyLinearExpression(const LinearExpressionProto& expr,
-                                     LinearExpressionProto* dst) {
+bool ModelCopy::CopyLinearExpression(
+    const LinearExpressionProto& expr, LinearExpressionProto* dst,
+    absl::Span<const int> enforcement_literals) {
   non_fixed_variables_.clear();
   non_fixed_coefficients_.clear();
   int64_t offset = expr.offset();
@@ -436,10 +439,13 @@ bool ModelCopy::CopyLinearExpression(const LinearExpressionProto& expr,
                            non_fixed_variables_.end());
   dst->mutable_coeffs()->Add(non_fixed_coefficients_.begin(),
                              non_fixed_coefficients_.end());
+  // TODO(user): We could save work by only doing this if this is the first
+  // copy.
+  context_->CanonicalizeLinearExpression(enforcement_literals, dst);
   return true;
 }
 
-bool ModelCopy::CopyLinear(const ConstraintProto& ct) {
+bool ModelCopy::CopyLinear(const ConstraintProto& ct, bool canonicalize) {
   non_fixed_variables_.clear();
   non_fixed_coefficients_.clear();
   int64_t offset = 0;
@@ -516,6 +522,9 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) {
   linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(),
                                 non_fixed_coefficients_.end());
   FillDomainInProto(tight_domain, linear);
+  if (canonicalize) {
+    context_->CanonicalizeLinearConstraint(new_ct);
+  }
   return true;
 }
 
@@ -708,11 +717,14 @@ bool ModelCopy::CopyInterval(const ConstraintProto& ct, int c,
   }
   *new_ct->mutable_enforcement_literal() = ct.enforcement_literal();
   CopyLinearExpression(ct.interval().start(),
-                       new_ct->mutable_interval()->mutable_start());
+                       new_ct->mutable_interval()->mutable_start(),
+                       ct.enforcement_literal());
   CopyLinearExpression(ct.interval().size(),
-                       new_ct->mutable_interval()->mutable_size());
+                       new_ct->mutable_interval()->mutable_size(),
+                       ct.enforcement_literal());
   CopyLinearExpression(ct.interval().end(),
-                       new_ct->mutable_interval()->mutable_end());
+                       new_ct->mutable_interval()->mutable_end(),
+                       ct.enforcement_literal());
   return true;
 }
 
@@ -778,10 +790,10 @@ bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) {
     AddLinearExpressionToLinearConstraint(itv.start(), 1, mutable_linear);
     AddLinearExpressionToLinearConstraint(itv.size(), 1, mutable_linear);
     AddLinearExpressionToLinearConstraint(itv.end(), -1, mutable_linear);
-    if (!CopyLinear(tmp_constraint_)) return false;
+    if (!CopyLinear(tmp_constraint_, true)) return false;
   }
 
-  // An enforced interval must have is size non-negative.
+  // An enforced interval must have its size non-negative.
   const LinearExpressionProto& size_expr = itv.size();
   if (context_->MinOf(size_expr) < 0) {
     tmp_constraint_.Clear();
@@ -791,7 +803,7 @@ bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) {
     tmp_constraint_.mutable_linear()->add_domain(-size_expr.offset());
     tmp_constraint_.mutable_linear()->add_domain(
         std::numeric_limits<int64_t>::max());
-    if (!CopyLinear(tmp_constraint_)) return false;
+    if (!CopyLinear(tmp_constraint_, true)) return false;
   }
 
   return true;

ortools/sat/cp_model_copy.h

@@ -90,9 +90,10 @@ class ModelCopy {
   bool CopyIntProd(const ConstraintProto& ct, bool ignore_names);
   bool CopyIntDiv(const ConstraintProto& ct, bool ignore_names);
   bool CopyIntMod(const ConstraintProto& ct, bool ignore_names);
-  bool CopyLinear(const ConstraintProto& ct);
+  bool CopyLinear(const ConstraintProto& ct, bool canonicalize);
   bool CopyLinearExpression(const LinearExpressionProto& expr,
-                            LinearExpressionProto* dst);
+                            LinearExpressionProto* dst,
+                            absl::Span<const int> enforcement_literals = {});
   bool CopyAutomaton(const ConstraintProto& ct);
   bool CopyTable(const ConstraintProto& ct);
   bool CopyAllDiff(const ConstraintProto& ct);

ortools/sat/cp_model_presolve.cc

@@ -5866,8 +5866,8 @@ bool CpModelPresolver::PresolveNoOverlap2DFramed(
       // Something can be outside of the frame.
       return false;
     }
-    if (2 * box.bounding_area.SizeX() <= framed_region.SizeX() ||
-        2 * box.bounding_area.SizeY() <= framed_region.SizeY()) {
+    if (2 * box.x_size <= framed_region.SizeX() ||
+        2 * box.y_size <= framed_region.SizeY()) {
       // We can fit two boxes in the delimited space between the fixed boxes, so
       // we cannot replace it by an at-most-one.
       return false;

ortools/sat/cp_model_solver.cc

@@ -1192,8 +1192,10 @@ class LnsSolver : public SubSolver {
  public:
   LnsSolver(std::unique_ptr<NeighborhoodGenerator> generator,
             const SatParameters& lns_parameters,
-            NeighborhoodGeneratorHelper* helper, SharedClasses* shared)
+            NeighborhoodGeneratorHelper* helper, SharedClasses* shared,
+            int preferred_linearization_level = 0)
       : SubSolver(generator->name(), INCOMPLETE),
+        preferred_linearization_level_(preferred_linearization_level),
         generator_(std::move(generator)),
         helper_(helper),
         lns_parameters_(lns_parameters),
@@ -1274,13 +1276,13 @@ class LnsSolver : public SubSolver {
       // TODO(user): Tune these.
       // TODO(user): This could be a good candidate for bandits.
       const int64_t stall = generator_->num_consecutive_non_improving_calls();
+      std::string search_info;
       const int search_index = stall < 10 ? 0 : task_id % 2;
-      absl::string_view search_info;
       switch (search_index) {
         case 0:
           local_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
-          local_params.set_linearization_level(0);
-          search_info = "auto_l0";
+          local_params.set_linearization_level(preferred_linearization_level_);
+          search_info = absl::StrCat("auto_l", preferred_linearization_level_);
           break;
         default:
           local_params.set_search_branching(SatParameters::PORTFOLIO_SEARCH);
@@ -1616,6 +1618,7 @@ class LnsSolver : public SubSolver {
   }
 
  private:
+  int preferred_linearization_level_ = 0;
   std::unique_ptr<NeighborhoodGenerator> generator_;
   NeighborhoodGeneratorHelper* helper_;
   const SatParameters lns_parameters_;
@@ -1881,6 +1884,9 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
       }
     }
 
+    // For routing, the LP relaxation seems pretty important, so we prefer an
+    // high linearization level to solve LNS subproblems.
+    const int routing_lin_level = 2;
     const int num_circuit = static_cast<int>(
         helper->TypeToConstraints(ConstraintProto::kCircuit).size());
     const int num_routes = static_cast<int>(
@@ -1890,21 +1896,21 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
         reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
             std::make_unique<RoutingRandomNeighborhoodGenerator>(
                 helper, name_filter.LastName()),
-            lns_params, helper, shared));
+            lns_params, helper, shared, routing_lin_level));
       }
       if (name_filter.Keep("routing_path_lns")) {
         reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
             std::make_unique<RoutingPathNeighborhoodGenerator>(
                 helper, name_filter.LastName()),
-            lns_params, helper, shared));
+            lns_params, helper, shared, routing_lin_level));
       }
     }
     if (num_routes > 0 || num_circuit > 1) {
       if (name_filter.Keep("routing_full_path_lns")) {
         reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
             std::make_unique<RoutingFullPathNeighborhoodGenerator>(
                 helper, name_filter.LastName()),
-            lns_params, helper, shared));
+            lns_params, helper, shared, routing_lin_level));
       }
     }
   }

ortools/sat/linear_relaxation.cc

@@ -1056,10 +1056,12 @@ void AppendNoOverlap2dRelaxation(const ConstraintProto& ct, Model* model,
           intervals_repository->IsPresent(x_intervals[i])
               ? intervals_repository->PresenceLiteral(y_intervals[i])
               : intervals_repository->PresenceLiteral(x_intervals[i]);
-      const IntegerValue area_min =
-          integer_trail->LevelZeroLowerBound(x_sizes[i]) *
+      const IntegerValue x_size =
+          integer_trail->LevelZeroLowerBound(x_sizes[i]);
+      const IntegerValue y_size =
           integer_trail->LevelZeroLowerBound(y_sizes[i]);
-      if (area_min > 0) {
+      if (x_size > 0 && y_size > 0) {
+        const IntegerValue area_min = x_size * y_size;
         // Note that intervals that must be absent can have negative sizes.
         // Not including the term if we don't have a view is ok.
         (void)lc.AddLiteralTerm(presence_literal, area_min);