diff --git a/src/sat/intervals.h b/src/sat/intervals.h index 8984e6128e..1b3a95e4c9 100644 --- a/src/sat/intervals.h +++ b/src/sat/intervals.h @@ -137,6 +137,7 @@ class SchedulingConstraintHelper { // Note that for tasks with variable durations, we don't necessarily have // duration-min between the the XXX-min and XXX-max value. IntegerValue DurationMin(int t) const; + IntegerValue DurationMax(int t) const; IntegerValue StartMin(int t) const; IntegerValue StartMax(int t) const; IntegerValue EndMin(int t) const; @@ -240,6 +241,12 @@ inline IntegerValue SchedulingConstraintHelper::DurationMin(int t) const { : integer_trail_->LowerBound(duration_vars_[t]); } +inline IntegerValue SchedulingConstraintHelper::DurationMax(int t) const { + return duration_vars_[t] == kNoIntegerVariable + ? fixed_durations_[t] + : integer_trail_->UpperBound(duration_vars_[t]); +} + inline IntegerValue SchedulingConstraintHelper::StartMin(int t) const { return integer_trail_->LowerBound(start_vars_[t]); } @@ -340,6 +347,19 @@ inline std::function SizeVar( }; } +inline std::function IsOptional(IntervalVariable v) { + return [=](const Model& model) { + return model.Get()->IsOptional(v); + }; +} + +inline std::function IsPresentLiteral( + IntervalVariable v) { + return [=](const Model& model) { + return model.Get()->IsPresentLiteral(v); + }; +} + inline std::function NewInterval(int64 min_start, int64 max_end, int64 size) { diff --git a/src/sat/timetable.cc b/src/sat/timetable.cc index 3295e95168..7cb74e8636 100644 --- a/src/sat/timetable.cc +++ b/src/sat/timetable.cc @@ -35,9 +35,16 @@ TimeTablingPerTask::TimeTablingPerTask( // the profile is shaped like the Hanoi tower. The additional space is for // both extremities and the sentinels. profile_.reserve(2 * num_tasks_ + 4); - in_profile_.resize(num_tasks_); scp_.reserve(num_tasks_); ecp_.reserve(num_tasks_); + is_in_profile_.resize(num_tasks_); + in_profile_.reserve(num_tasks_); + // Reversible set of tasks to consider for propagation. + num_tasks_to_sweep_ = num_tasks_; + tasks_to_sweep_.resize(num_tasks_); + for (int t = 0; t < num_tasks_; ++t) { + tasks_to_sweep_[t] = t; + } } void TimeTablingPerTask::RegisterWith(GenericLiteralWatcher* watcher) { @@ -47,6 +54,8 @@ void TimeTablingPerTask::RegisterWith(GenericLiteralWatcher* watcher) { for (int t = 0; t < num_tasks_; t++) { watcher->WatchLowerBound(demand_vars_[t], id); } + // Reversible number of tasks to consider for propagation. + watcher->RegisterReversibleInt(id, &num_tasks_to_sweep_); } bool TimeTablingPerTask::Propagate() { @@ -75,19 +84,23 @@ bool TimeTablingPerTask::BuildProfile() { scp_.clear(); ecp_.clear(); + in_profile_.clear(); // Build start of compulsory part events. for (int i = num_tasks_ - 1; i >= 0; --i) { const auto task_time = by_decreasing_start_max[i]; const int t = task_time.task_index; - in_profile_[t] = + is_in_profile_[t] = helper_->IsPresent(t) && task_time.time < helper_->EndMin(t); - if (in_profile_[t]) scp_.push_back(task_time); + if (is_in_profile_[t]) { + in_profile_.push_back(t); + scp_.push_back(task_time); + } } // Build end of compulsory part events. for (int i = 0; i < num_tasks_; ++i) { - if (in_profile_[by_increasing_end_min[i].task_index]) { + if (is_in_profile_[by_increasing_end_min[i].task_index]) { ecp_.push_back(by_increasing_end_min[i]); } } @@ -189,17 +202,38 @@ void TimeTablingPerTask::ReverseProfile() { bool TimeTablingPerTask::SweepAllTasks() { // Tasks with a lower or equal demand will not be pushed. const IntegerValue min_demand = CapacityMax() - profile_max_height_; - for (int t = 0; t < num_tasks_; ++t) { - // Note: We still push the optional task that may be present. It is OK to - // propagate the bounds of such tasks. They should become unperformed if - // the bounds are no longer consistent. - if (DemandMin(t) <= min_demand || helper_->DurationMin(t) == 0) continue; - if (helper_->IsAbsent(t)) continue; - if (helper_->StartMin(t) != helper_->StartMax(t) && !SweepTask(t)) { - return false; + for (int i = num_tasks_to_sweep_ - 1; i >= 0; --i) { + const int t = tasks_to_sweep_[i]; + const bool fixed_start = helper_->StartMin(t) == helper_->StartMax(t); + const bool fixed_end = helper_->EndMin(t) == helper_->EndMax(t); + // A task does not have to be considered for propagation in the rest of the + // sub-tree if it respects one of these conditions: + // - its start and end variables are fixed; + // - it has a maximum duration of 0; + // - it has a maximum demand of 0; + // - it is absent. + if ((fixed_start && fixed_end) || helper_->DurationMax(t) == 0 || + DemandMax(t) == 0 || helper_->IsAbsent(t)) { + // Remove the task from the set of tasks to sweep. + num_tasks_to_sweep_--; + tasks_to_sweep_[i] = tasks_to_sweep_[num_tasks_to_sweep_]; + tasks_to_sweep_[num_tasks_to_sweep_] = t; + continue; } + // A task does not have to be considered for propagation in this particular + // iteration if it respects one of these conditions: + // - its start variable is fixed; + // - its minimum demand cannot lead to a resource overload; + // - its minimum duration is 0. + if (fixed_start || DemandMin(t) <= min_demand || + helper_->DurationMin(t) == 0) { + continue; + } + + if (!SweepTask(t)) return false; } + return true; } @@ -249,7 +283,7 @@ bool TimeTablingPerTask::SweepTask(int task_id) { new_start_min = profile_[rec_id].end; if (start_max < new_start_min) { new_start_min = start_max; - overload = !in_profile_[task_id]; + overload = !is_in_profile_[task_id]; } new_end_min = std::max(new_end_min, new_start_min + duration_min); @@ -294,13 +328,12 @@ bool TimeTablingPerTask::UpdateStartingTime(int task_id, IntegerValue left, void TimeTablingPerTask::AddProfileReason(IntegerValue left, IntegerValue right) { - for (int t = 0; t < num_tasks_; ++t) { + for (const int t : in_profile_) { const IntegerValue start_max = helper_->StartMax(t); const IntegerValue end_min = helper_->EndMin(t); - // Do not consider the task if it does not overlap [left, right), if it is - // absent, or if it does not have a mandatory part. - if (end_min <= left || right <= start_max || !in_profile_[t]) continue; + // Do not consider the task if it does not overlap [left, right). + if (end_min <= left || right <= start_max) continue; helper_->AddPresenceReason(t); helper_->AddStartMaxReason(t, std::max(left, start_max)); diff --git a/src/sat/timetable.h b/src/sat/timetable.h index 7c6abab82e..a25cf8d612 100644 --- a/src/sat/timetable.h +++ b/src/sat/timetable.h @@ -88,6 +88,10 @@ class TimeTablingPerTask : public PropagatorInterface { return integer_trail_->LowerBound(demand_vars_[task_id]); } + IntegerValue DemandMax(int task_id) const { + return integer_trail_->UpperBound(demand_vars_[task_id]); + } + // Number of tasks. const int num_tasks_; @@ -110,12 +114,21 @@ class TimeTablingPerTask : public PropagatorInterface { // True if the corresponding task is part of the profile, i.e., it has a // mandatory part and is not optional. - std::vector in_profile_; + std::vector is_in_profile_; + + // Tasks that are part of the profile. In other words, this vector contains + // all the tasks for which is_in_profile_ is true. + std::vector in_profile_; // True if the last call of the propagator has filtered the domain of a task // and changed the shape of the profile. bool profile_changed_; + // Reversible set of tasks to consider for propagation. The set contains the + // tasks in the [0, num_tasks_to_sweep_) prefix of tasks_to_sweep_. + std::vector tasks_to_sweep_; + int num_tasks_to_sweep_; + DISALLOW_COPY_AND_ASSIGN(TimeTablingPerTask); };