fix bug in the sat scheduling code found by the rcpsp

examples/python/rcpsp_sat.py

@@ -24,7 +24,7 @@ from google.protobuf import text_format
 from ortools.data import pywraprcpsp
 from ortools.sat.python import cp_model
 
-Parser = argparse.ArgumentParser()
+Parser=argparse.ArgumentParser()
 Parser.add_argument('--input', default = "",
                     help = 'Input file to parse and solve.')
 Parser.add_argument('--output_proto', default = "",

makefiles/Makefile.gen.mk

@@ -1561,6 +1561,7 @@ $(OBJ_DIR)/graph/max_flow.$O: \
  $(SRC_DIR)/ortools/base/integral_types.h \
  $(SRC_DIR)/ortools/base/logging.h \
  $(SRC_DIR)/ortools/base/macros.h \
+ $(SRC_DIR)/ortools/base/memory.h \
  $(SRC_DIR)/ortools/base/stringprintf.h \
  $(SRC_DIR)/ortools/graph/ebert_graph.h \
  $(GEN_DIR)/ortools/graph/flow_problem.pb.h \

ortools/sat/cp_model_presolve.cc

@@ -1362,26 +1362,42 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
     if (!ct.enforcement_literal().empty()) has_optional_interval = true;
     const IntervalConstraintProto& interval = ct.interval();
     start_indices[i] = interval.start();
-    const int duration_index = interval.size();
-    const int demand_index = proto.demands(i);
-    if (context->IsFixed(duration_index) &&
-        context->MinOf(duration_index) == 1) {
+    const int duration_ref = interval.size();
+    const int demand_ref = proto.demands(i);
+    if (context->IsFixed(duration_ref) && context->MinOf(duration_ref) == 1) {
       num_duration_one++;
     }
-    if (context->MinOf(duration_index) == 0) {
+    if (context->MinOf(duration_ref) == 0) {
       // The behavior for zero-duration interval is currently not the same in
       // the no-overlap and the cumulative constraint.
       return false;
     }
-    const int64 demand_min = context->MinOf(demand_index);
-    const int64 demand_max = context->MaxOf(demand_index);
+    const int64 demand_min = context->MinOf(demand_ref);
+    const int64 demand_max = context->MaxOf(demand_ref);
     if (demand_min > capacity / 2) {
       num_greater_half_capacity++;
     }
     if (demand_min > capacity) {
-      context->UpdateRuleStats("TODO cumulative: demand_min exceeds capacity");
+      context->UpdateRuleStats("cumulative: demand_min exceeds capacity");
+      if (ct.enforcement_literal().empty()) {
+        context->is_unsat = true;
+        return false;
+      } else {
+        CHECK_EQ(ct.enforcement_literal().size(), 1);
+        context->SetLiteralToFalse(ct.enforcement_literal(0));
+      }
+      return false;
     } else if (demand_max > capacity) {
-      context->UpdateRuleStats("TODO cumulative: demand_max exceeds capacity");
+      if (ct.enforcement_literal().empty()) {
+        context->UpdateRuleStats("cumulative: demand_max exceeds capacity.");
+        context->IntersectDomainWith(demand_ref, {{kint64min, capacity}});
+      } else {
+        // TODO(user): we abort because we cannot convert this to a no_overlap
+        // for instance.
+        context->UpdateRuleStats(
+            "cumulative: demand_max of optional interval exceeds capacity.");
+        return false;
+      }
     }
   }
 

ortools/sat/disjunctive.cc

@@ -369,7 +369,7 @@ bool DisjunctiveOverloadChecker::Propagate() {
       // If tasks shares the same presence literal, it is possible that we
       // already pushed this task absence.
       if (!helper_->IsAbsent(optional_task)) {
-        helper_->PushTaskAbsence(optional_task);  // This never fails.
+        if (!helper_->PushTaskAbsence(optional_task)) return false;
       }
       theta_tree_.RemoveEvent(optional_event);
     }

ortools/sat/integer.cc

@@ -784,11 +784,37 @@ bool IntegerTrail::Enqueue(IntegerLiteral i_lit,
   return Enqueue(i_lit, literal_reason, integer_reason, integer_trail_.size());
 }
 
+bool IntegerTrail::ReasonIsValid(absl::Span<Literal> literal_reason,
+                                 absl::Span<IntegerLiteral> integer_reason) {
+  const VariablesAssignment& assignment = trail_->Assignment();
+  for (const Literal lit : literal_reason) {
+    if (!assignment.LiteralIsFalse(lit)) return false;
+  }
+  for (const IntegerLiteral i_lit : integer_reason) {
+    if (i_lit.bound > vars_[i_lit.var].current_bound) {
+      if (IsOptional(i_lit.var)) {
+        const Literal is_ignored = IsIgnoredLiteral(i_lit.var);
+        LOG(INFO) << "Reason " << i_lit << " is not true!"
+                  << " optional variable:" << i_lit.var
+                  << " present:" << assignment.LiteralIsFalse(is_ignored)
+                  << " absent:" << assignment.LiteralIsTrue(is_ignored)
+                  << " current_lb:" << vars_[i_lit.var].current_bound;
+      } else {
+        LOG(INFO) << "Reason " << i_lit << " is not true!"
+                  << " non-optional variable:" << i_lit.var
+                  << " current_lb:" << vars_[i_lit.var].current_bound;
+      }
+      return false;
+    }
+  }
+  return true;
+}
+
 bool IntegerTrail::Enqueue(IntegerLiteral i_lit,
                            absl::Span<Literal> literal_reason,
                            absl::Span<IntegerLiteral> integer_reason,
                            int trail_index_with_same_reason) {
-  DCHECK(AllLiteralsAreFalse(literal_reason));
+  DCHECK(ReasonIsValid(literal_reason, integer_reason));
 
   // No point doing work if the variable is already ignored.
   if (IsCurrentlyIgnored(i_lit.var)) return true;
@@ -1003,13 +1029,6 @@ std::vector<Literal> IntegerTrail::ReasonFor(IntegerLiteral literal) const {
   return reason;
 }
 
-bool IntegerTrail::AllLiteralsAreFalse(absl::Span<Literal> literals) const {
-  for (const Literal lit : literals) {
-    if (!trail_->Assignment().LiteralIsFalse(lit)) return false;
-  }
-  return true;
-}
-
 // TODO(user): If this is called many time on the same variables, it could be
 // made faster by using some caching mecanism.
 void IntegerTrail::MergeReasonInto(absl::Span<IntegerLiteral> literals,
@@ -1157,7 +1176,8 @@ absl::Span<Literal> IntegerTrail::Reason(const Trail& trail,
 void IntegerTrail::EnqueueLiteral(Literal literal,
                                   absl::Span<Literal> literal_reason,
                                   absl::Span<IntegerLiteral> integer_reason) {
-  DCHECK(AllLiteralsAreFalse(literal_reason));
+  DCHECK(!trail_->Assignment().LiteralIsAssigned(literal));
+  DCHECK(ReasonIsValid(literal_reason, integer_reason));
   if (integer_search_levels_.empty()) {
     // Level zero. We don't keep any reason.
     trail_->EnqueueWithUnitReason(literal);

ortools/sat/integer.h

@@ -598,12 +598,14 @@ class IntegerTrail : public SatPropagator {
   // simply do: return integer_trail_->ReportConflict(...);
   bool ReportConflict(absl::Span<Literal> literal_reason,
                       absl::Span<IntegerLiteral> integer_reason) {
+    DCHECK(ReasonIsValid(literal_reason, integer_reason));
     std::vector<Literal>* conflict = trail_->MutableConflict();
     conflict->assign(literal_reason.begin(), literal_reason.end());
     MergeReasonInto(integer_reason, conflict);
     return false;
   }
   bool ReportConflict(absl::Span<IntegerLiteral> integer_reason) {
+    DCHECK(ReasonIsValid({}, integer_reason));
     std::vector<Literal>* conflict = trail_->MutableConflict();
     conflict->clear();
     MergeReasonInto(integer_reason, conflict);
@@ -631,9 +633,10 @@ class IntegerTrail : public SatPropagator {
   int Index() const { return integer_trail_.size(); }
 
  private:
-  // Tests that all the literals in the given reason are assigned to false.
-  // This is used to DCHECK the given reasons to the Enqueue*() functions.
-  bool AllLiteralsAreFalse(absl::Span<Literal> literals) const;
+  // Used for DHECKs to validate the reason given to the public functions above.
+  // Tests that all Literal are false. Tests that all IntegerLiteral are true.
+  bool ReasonIsValid(absl::Span<Literal> literal_reason,
+                     absl::Span<IntegerLiteral> integer_reason);
 
   // Does the work of MergeReasonInto() when queue_ is already initialized.
   void MergeReasonIntoInternal(std::vector<Literal>* output) const;

ortools/sat/intervals.cc

@@ -174,7 +174,7 @@ bool SchedulingConstraintHelper::PushIntervalBound(int t, IntegerLiteral lit) {
       if (lit.bound > integer_trail_->UpperBound(lit.var)) {
         integer_reason_.push_back(
             IntegerLiteral::LowerOrEqual(lit.var, lit.bound - 1));
-        PushTaskAbsence(t);
+        if (!PushTaskAbsence(t)) return false;
       }
       return true;
     }
@@ -200,12 +200,16 @@ bool SchedulingConstraintHelper::DecreaseEndMax(int t,
       t, IntegerLiteral::LowerOrEqual(end_vars_[t], new_max_end));
 }
 
-void SchedulingConstraintHelper::PushTaskAbsence(int t) {
+bool SchedulingConstraintHelper::PushTaskAbsence(int t) {
   DCHECK_NE(reason_for_presence_[t], kNoLiteralIndex);
-  DCHECK(!IsPresent(t));
   DCHECK(!IsAbsent(t));
+  if (IsPresent(t)) {
+    literal_reason_.push_back(Literal(reason_for_presence_[t]).Negated());
+    return ReportConflict();
+  }
   integer_trail_->EnqueueLiteral(Literal(reason_for_presence_[t]).Negated(),
                                  literal_reason_, integer_reason_);
+  return true;
 }
 
 bool SchedulingConstraintHelper::ReportConflict() {

ortools/sat/intervals.h

@@ -195,11 +195,11 @@ class SchedulingConstraintHelper {
   // conditionned on its presence. The functions will do the correct thing
   // depending on whether or not the start_min/end_max are optional variables
   // whose presence implies the interval presence.
-  bool IncreaseStartMin(int t, IntegerValue new_min_start);
-  bool DecreaseEndMax(int t, IntegerValue new_max_end);
-  void PushTaskAbsence(int t);
-  bool PushIntegerLiteral(IntegerLiteral bound);
-  bool ReportConflict();
+  MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_min_start);
+  MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_max_end);
+  MUST_USE_RESULT bool PushTaskAbsence(int t);
+  MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral bound);
+  MUST_USE_RESULT bool ReportConflict();
 
   // Returns the underlying integer variables.
   const std::vector<IntegerVariable>& StartVars() const { return start_vars_; }

ortools/sat/swig_helper.h

@@ -101,6 +101,7 @@ class SatHelper {
     model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
     model.GetOrCreate<SigintHandler>()->Register(
         [&stopped]() { stopped = true; });
+
     return operations_research::sat::SolveCpModel(model_proto, &model);
   }
 

ortools/sat/timetable.cc

@@ -366,11 +366,6 @@ bool TimeTablingPerTask::SweepTask(int task_id) {
   // rectangle before being pushed.
   IntegerValue last_initial_conflict = kMinIntegerValue;
 
-  // True if the task has been scheduled during a conflicting profile rectangle.
-  // This means that the task is either part of the profile rectangle or that we
-  // have an overload in which case we remove the case if it is optional.
-  bool overload = false;
-
   // Push the task from left to right until it does not overlap any conflicting
   // rectangle. Pushing the task may push the end of its compulsory part on the
   // right but will not change its start. The main loop of the propagator will
@@ -388,9 +383,16 @@ bool TimeTablingPerTask::SweepTask(int task_id) {
     // are not updated yet.
     new_start_min = profile_[rec_id + 1].start;  // i.e. profile_[rec_id].end
     if (start_max < new_start_min) {
-      new_start_min = start_max;
-      overload = !IsInProfile(task_id);
+      if (IsInProfile(task_id)) {
+        // Because the task is part of the profile, we cannot push it further.
+        new_start_min = start_max;
+      } else {
+        // We have a conflict or we can push the task absence. In both cases
+        // we don't need more than start_max + 1 in the explanation below.
+        new_start_min = start_max + 1;
+      }
     }
+
     new_end_min = std::max(new_end_min, new_start_min + duration_min);
     limit = std::min(start_max, new_end_min);
 
@@ -421,9 +423,6 @@ bool TimeTablingPerTask::SweepTask(int task_id) {
     profile_changed_ = true;
   }
 
-  // Explain that the task should be absent or explain the resource overload.
-  if (overload) return OverloadOrRemove(task_id, start_max);
-
   return true;
 }
 
@@ -475,33 +474,5 @@ bool TimeTablingPerTask::IncreaseCapacity(IntegerValue time,
       IntegerLiteral::GreaterOrEqual(capacity_var_, new_min));
 }
 
-bool TimeTablingPerTask::OverloadOrRemove(int task_id, IntegerValue time) {
-  helper_->ClearReason();
-
-  helper_->MutableIntegerReason()->push_back(
-      integer_trail_->UpperBoundAsLiteral(capacity_var_));
-
-  AddProfileReason(time, time + 1);
-
-  // We know that task_id was not part of the profile when it was built. We thus
-  // have to add it manualy since it will not be added by AddProfileReason.
-  helper_->AddStartMaxReason(task_id, time);
-  helper_->AddEndMinReason(task_id, time + 1);
-  helper_->MutableIntegerReason()->push_back(
-      integer_trail_->LowerBoundAsLiteral(demand_vars_[task_id]));
-
-  // Explain the resource overload if the task cannot be removed.
-  if (helper_->IsPresent(task_id)) {
-    helper_->AddPresenceReason(task_id);
-    return helper_->PushIntegerLiteral(
-        IntegerLiteral::GreaterOrEqual(capacity_var_, CapacityMax() + 1));
-  }
-
-  // Remove the task to prevent the overload.
-  helper_->PushTaskAbsence(task_id);
-
-  return true;
-}
-
 }  // namespace sat
 }  // namespace operations_research

ortools/sat/timetable.h

@@ -83,10 +83,6 @@ class TimeTablingPerTask : public PropagatorInterface {
   // the mandatory parts that overlap time.
   bool IncreaseCapacity(IntegerValue time, IntegerValue new_min);
 
-  // Explains the resource overload at time or removes task_id if it is
-  // optional.
-  bool OverloadOrRemove(int task_id, IntegerValue time);
-
   // Explains the state of the profile in the time interval [left, right). The
   // reason is all the mandatory parts that overlap the interval. The current
   // reason is not cleared when this method is called.