[CP-SAT] fix more corner cases in checker and presolve

ortools/sat/cp_model_checker.cc

@@ -187,6 +187,51 @@ bool PossibleIntegerOverflow(const CpModelProto& model,
   return false;
 }
 
+int64_t MinOfRef(const CpModelProto& model, int ref) {
+  const IntegerVariableProto& var_proto = model.variables(PositiveRef(ref));
+  if (RefIsPositive(ref)) {
+    return var_proto.domain(0);
+  } else {
+    return -var_proto.domain(var_proto.domain_size() - 1);
+  }
+}
+
+int64_t MaxOfRef(const CpModelProto& model, int ref) {
+  const IntegerVariableProto& var_proto = model.variables(PositiveRef(ref));
+  if (RefIsPositive(ref)) {
+    return var_proto.domain(var_proto.domain_size() - 1);
+  } else {
+    return -var_proto.domain(0);
+  }
+}
+
+template <class LinearExpressionProto>
+int64_t MaxOfExpression(const CpModelProto& model,
+                        const LinearExpressionProto& proto) {
+  int64_t sum_max = 0;
+  for (int i = 0; i < proto.vars_size(); ++i) {
+    const int ref = proto.vars(i);
+    const int64_t coeff = proto.coeffs(i);
+    sum_max =
+        CapAdd(sum_max, coeff >= 0 ? CapProd(MaxOfRef(model, ref), coeff)
+                                   : CapProd(MinOfRef(model, ref), coeff));
+  }
+
+  return sum_max;
+}
+
+int64_t IntervalSizeMax(const CpModelProto& model, int interval_index) {
+  DCHECK_EQ(ConstraintProto::ConstraintCase::kInterval,
+            model.constraints(interval_index).constraint_case());
+  const IntervalConstraintProto& proto =
+      model.constraints(interval_index).interval();
+  if (proto.has_size_view()) {
+    return MaxOfExpression(model, proto.size_view());
+  } else {
+    return MaxOfRef(model, proto.size());
+  }
+}
+
 std::string ValidateLinearExpression(const CpModelProto& model,
                                      const LinearExpressionProto& expr) {
   if (expr.coeffs_size() != expr.vars_size()) {
@@ -445,6 +490,17 @@ std::string ValidateCumulativeConstraint(const CpModelProto& model,
     }
   }
 
+  int64_t sum_max_demands = 0;
+  for (const int demand_ref : ct.cumulative().demands()) {
+    const int64_t demand_max = MaxOfRef(model, demand_ref);
+    DCHECK_GE(demand_max, 0);
+    sum_max_demands = CapAdd(sum_max_demands, demand_max);
+    if (sum_max_demands == std::numeric_limits<int64_t>::max()) {
+      return "The sum of max demands do not fit on an int64_t in constraint: " +
+             ProtobufDebugString(ct);
+    }
+  }
+
   for (const LinearExpressionProto& expr : ct.cumulative().energies()) {
     const std::string error = ValidateLinearExpression(model, expr);
     if (!error.empty()) {
@@ -464,6 +520,21 @@ std::string ValidateNoOverlap2DConstraint(const CpModelProto& model,
     return absl::StrCat("The two lists of intervals must have the same size: ",
                         ProtobufShortDebugString(ct));
   }
+
+  // Checks if the sum of max areas of each rectangle can overflow.
+  int64_t sum_max_areas = 0;
+  for (int i = 0; i < ct.no_overlap_2d().x_intervals().size(); ++i) {
+    const int64_t max_size_x =
+        IntervalSizeMax(model, ct.no_overlap_2d().x_intervals(i));
+    const int64_t max_size_y =
+        IntervalSizeMax(model, ct.no_overlap_2d().y_intervals(i));
+    sum_max_areas = CapAdd(sum_max_areas, CapProd(max_size_x, max_size_y));
+    if (sum_max_areas == std::numeric_limits<int64_t>::max()) {
+      return "Integer overflow when summing all areas in "
+             "constraint: " +
+             ProtobufDebugString(ct);
+    }
+  }
   return "";
 }
 

ortools/sat/cp_model_expand.cc

@@ -979,12 +979,9 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
 
     std::vector<int> tuple_literals;
     if (transition_values.size() == 1) {
-      bool tmp_removed_values = false;
       tuple_literals.push_back(context->GetOrCreateConstantVar(1));
-      CHECK_EQ(reachable_states[time + 1].size(), 1);
       if (!context->IntersectDomainWith(vars[time],
-                                        Domain(transition_values.front()),
-                                        &tmp_removed_values)) {
+                                        Domain(transition_values.front()))) {
         VLOG(1) << "Infeasible automaton.";
         return;
       }

ortools/sat/cp_model_postsolve.cc

@@ -190,6 +190,10 @@ void PostsolveLinear(const ConstraintProto& ct,
 
 // We assign any non fixed lhs variables to their minimum value. Then we assign
 // the target to the max. This should always be feasible.
+//
+// Note(user): Our heuristic is not feasible if x = max(-x, ...) but we made
+// sure we don't output such int_max here. Alternatively we could probably fix
+// the code here.
 void PostsolveIntMax(const ConstraintProto& ct, std::vector<Domain>* domains) {
   int64_t m = std::numeric_limits<int64_t>::min();
   for (const int ref : ct.int_max().vars()) {

ortools/sat/cp_model_presolve.cc

@@ -530,6 +530,7 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) {
   int64_t infered_min = std::numeric_limits<int64_t>::min();
   int64_t infered_max = std::numeric_limits<int64_t>::min();
   bool contains_target_ref = false;
+  bool contains_negated_target_ref = false;
   std::set<int> used_ref;
   int new_size = 0;
   for (const int ref : ct->int_max().vars()) {
@@ -539,6 +540,17 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) {
         ref == NegatedRef(target_ref)) {
       infered_min = std::max(infered_min, int64_t{0});
     }
+    if (ref == NegatedRef(target_ref)) {
+      // x must be non-negative.
+      // It can be positive if they are other terms, otherwise it must be zero.
+      // TODO(user): more presolve in this case?
+      contains_negated_target_ref = true;
+      context_->UpdateRuleStats("int_max: x = max(-x, ...)");
+      if (!context_->IntersectDomainWith(
+              target_ref, {0, std::numeric_limits<int64_t>::max()})) {
+        return false;
+      }
+    }
     used_ref.insert(ref);
     ct->mutable_int_max()->set_vars(new_size++, ref);
     infered_min = std::max(infered_min, context_->MinOf(ref));
@@ -548,6 +560,7 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) {
     context_->UpdateRuleStats("int_max: removed dup");
   }
   ct->mutable_int_max()->mutable_vars()->Truncate(new_size);
+
   if (contains_target_ref) {
     context_->UpdateRuleStats("int_max: x = max(x, ...)");
     for (const int ref : ct->int_max().vars()) {
@@ -584,7 +597,10 @@ bool CpModelPresolver::PresolveIntMax(ConstraintProto* ct) {
   // If the target is only used here and if
   // infered_domain ∩ [kint64min, target_ub] ⊂ target_domain
   // then the constraint is really max(...) <= target_ub and we can simplify it.
-  if (context_->VariableIsUniqueAndRemovable(target_ref)) {
+  //
+  // This is not as easy if x = max(-x, ...) so we skip this case.
+  if (context_->VariableIsUniqueAndRemovable(target_ref) &&
+      !contains_negated_target_ref) {
     const Domain& target_domain = context_->DomainOf(target_ref);
     if (infered_domain
             .IntersectionWith(Domain(std::numeric_limits<int64_t>::min(),

ortools/sat/intervals.cc

@@ -151,12 +151,23 @@ bool SchedulingConstraintHelper::UpdateCachedValues(int t) {
 
   IntegerValue smin = integer_trail_->LowerBound(starts_[t]);
   IntegerValue smax = integer_trail_->UpperBound(starts_[t]);
-  IntegerValue dmin = integer_trail_->LowerBound(sizes_[t]);
-  IntegerValue dmax = integer_trail_->UpperBound(sizes_[t]);
   IntegerValue emin = integer_trail_->LowerBound(ends_[t]);
   IntegerValue emax = integer_trail_->UpperBound(ends_[t]);
 
+  // We take the max for the corner case where the size of an optional interval
+  // is used elsewhere and has a domain with negative value.
+  //
+  // TODO(user): maybe we should just disallow size with a negative domain, but
+  // is is harder to enforce if we have a linear expression for size.
+  IntegerValue dmin =
+      std::max(IntegerValue(0), integer_trail_->LowerBound(sizes_[t]));
+  IntegerValue dmax = integer_trail_->UpperBound(sizes_[t]);
+
   // Detect first if we have a conflict using the relation start + size = end.
+  if (dmax < 0) {
+    AddSizeMaxReason(t, dmax);
+    return PushTaskAbsence(t);
+  }
   if (smin + dmin - emax > 0) {
     ClearReason();
     AddStartMinReason(t, smin);

ortools/sat/intervals.h

@@ -546,6 +546,7 @@ inline void SchedulingConstraintHelper::AddSizeMinReason(
     int t, IntegerValue lower_bound) {
   AddOtherReason(t);
   DCHECK(!IsAbsent(t));
+  if (lower_bound <= 0) return;
   AddGenericReason(sizes_[t].Negated(), -lower_bound, minus_ends_[t],
                    starts_[t]);
 }

ortools/sat/java/sat.i

@@ -91,7 +91,7 @@ PROTO2_RETURN(operations_research::sat::CpSolverResponse,
     $input_object_class, "accept", "(Ljava/lang/Object;)V");
   assert($input_method_id != nullptr);
 
-  // When the lambda will be destroyed, input_guard's destructor will be call.
+  // When the lambda will be destroyed, input_guard's destructor will be called.
   $1 = [jvm, $input_object, $input_method_id, $input_guard](
       const std::string& message) -> void {
         JNIEnv *jenv = NULL;

ortools/sat/sat_parameters.proto

@@ -17,6 +17,7 @@ package operations_research.sat;
 
 option java_package = "com.google.ortools.sat";
 option java_multiple_files = true;
+
 option csharp_namespace = "Google.OrTools.Sat";