speed up timetabling in sat

This commit is contained in:
Laurent Perron
2017-04-07 13:50:29 +02:00
parent b9e9031b9b
commit 3736072d20
3 changed files with 84 additions and 18 deletions

View File

@@ -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<IntegerVariable(const Model&)> SizeVar(
};
}
inline std::function<bool(const Model&)> IsOptional(IntervalVariable v) {
return [=](const Model& model) {
return model.Get<IntervalsRepository>()->IsOptional(v);
};
}
inline std::function<Literal(const Model&)> IsPresentLiteral(
IntervalVariable v) {
return [=](const Model& model) {
return model.Get<IntervalsRepository>()->IsPresentLiteral(v);
};
}
inline std::function<IntervalVariable(Model*)> NewInterval(int64 min_start,
int64 max_end,
int64 size) {

View File

@@ -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));

View File

@@ -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<bool> in_profile_;
std::vector<bool> 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<int> 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<int> tasks_to_sweep_;
int num_tasks_to_sweep_;
DISALLOW_COPY_AND_ASSIGN(TimeTablingPerTask);
};