[SAT] preprocess tasks with 0-1 demands in cumulative as optional tasks; fix scheduling code with optional intervals

This commit is contained in:
Laurent Perron
2018-05-18 13:45:49 +02:00
parent 0bb452d5a5
commit 3e401080f9
4 changed files with 89 additions and 55 deletions

View File

@@ -537,7 +537,19 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
arg->set_capacity(capacity);
for (int i = 0; i < starts.size(); ++i) {
arg->add_intervals(intervals[i]);
arg->add_demands(demands[i]);
// Special case for a 0-1 demand, we mark the interval as optional instead
// and fix the demand to 1.
if (proto.variables(demands[i]).domain().size() == 2 &&
proto.variables(demands[i]).domain(0) == 0 &&
proto.variables(demands[i]).domain(1) == 1 &&
proto.variables(capacity).domain(1) == 1) {
proto.mutable_constraints(intervals[i])
->add_enforcement_literal(demands[i]);
arg->add_demands(LookupConstant(1));
} else {
arg->add_demands(demands[i]);
}
}
} else if (fz_ct.type == "diffn") {
const std::vector<int> x = LookupVars(fz_ct.arguments[0]);

View File

@@ -1283,10 +1283,13 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
int num_duration_one = 0;
int num_greater_half_capacity = 0;
bool has_optional_interval = false;
for (int i = 0; i < size; ++i) {
// TODO(user): adapt in the presence of optional intervals.
const IntervalConstraintProto& interval =
context->working_model->constraints(proto.intervals(i)).interval();
const ConstraintProto& ct =
context->working_model->constraints(proto.intervals(i));
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);
@@ -1294,6 +1297,11 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
context->MinOf(duration_index) == 1) {
num_duration_one++;
}
if (context->MinOf(duration_index) == 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);
if (demand_min > capacity / 2) {
@@ -1307,7 +1315,7 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
}
if (num_greater_half_capacity == size) {
if (num_duration_one == size) {
if (num_duration_one == size && !has_optional_interval) {
context->UpdateRuleStats("cumulative: convert to all_different");
ConstraintProto* new_ct = context->working_model->add_constraints();
auto* arg = new_ct->mutable_all_diff();

View File

@@ -62,38 +62,38 @@ std::function<void(Model*)> Disjunctive(
watcher->SetPropagatorPriority(id, 1);
model->TakeOwnership(overload_checker);
}
for (const bool time_direction : {true, false}) {
DisjunctiveDetectablePrecedences* detectable_precedences =
new DisjunctiveDetectablePrecedences(time_direction, helper);
const int id = detectable_precedences->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 2);
model->TakeOwnership(detectable_precedences);
}
for (const bool time_direction : {true, false}) {
DisjunctiveNotLast* not_last =
new DisjunctiveNotLast(time_direction, helper);
const int id = not_last->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 3);
model->TakeOwnership(not_last);
}
for (const bool time_direction : {true, false}) {
DisjunctiveEdgeFinding* edge_finding =
new DisjunctiveEdgeFinding(time_direction, helper);
const int id = edge_finding->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 4);
model->TakeOwnership(edge_finding);
}
if (model->GetOrCreate<SatParameters>()
->use_precedences_in_disjunctive_constraint()) {
for (const bool time_direction : {true, false}) {
DisjunctivePrecedences* precedences = new DisjunctivePrecedences(
time_direction, helper, model->GetOrCreate<IntegerTrail>(),
model->GetOrCreate<PrecedencesPropagator>());
const int id = precedences->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 5);
model->TakeOwnership(precedences);
DisjunctiveDetectablePrecedences* detectable_precedences =
new DisjunctiveDetectablePrecedences(time_direction, helper);
const int id = detectable_precedences->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 2);
model->TakeOwnership(detectable_precedences);
}
for (const bool time_direction : {true, false}) {
DisjunctiveNotLast* not_last =
new DisjunctiveNotLast(time_direction, helper);
const int id = not_last->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 3);
model->TakeOwnership(not_last);
}
for (const bool time_direction : {true, false}) {
DisjunctiveEdgeFinding* edge_finding =
new DisjunctiveEdgeFinding(time_direction, helper);
const int id = edge_finding->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 4);
model->TakeOwnership(edge_finding);
}
if (model->GetOrCreate<SatParameters>()
->use_precedences_in_disjunctive_constraint()) {
for (const bool time_direction : {true, false}) {
DisjunctivePrecedences* precedences = new DisjunctivePrecedences(
time_direction, helper, model->GetOrCreate<IntegerTrail>(),
model->GetOrCreate<PrecedencesPropagator>());
const int id = precedences->RegisterWith(watcher);
watcher->SetPropagatorPriority(id, 5);
model->TakeOwnership(precedences);
}
}
}
};
}
@@ -209,8 +209,11 @@ bool DisjunctiveOverloadChecker::Propagate() {
int num_events_ = 0;
for (const auto task_time : helper_->TaskByIncreasingStartMin()) {
const int task = task_time.task_index;
// TODO(user): Add max energy deduction for variable durations.
// Those would take into account tasks with DurationMin(task) == 0.
// TODO(user): We need to take into account task with zero duration because
// in this constraint, such a task cannot be overlapped by other. However,
// we currently use the fact that the energy min is zero to detect that a
// task is present and non-optional in the theta_tree_. Fix.
if (helper_->IsAbsent(task) || helper_->DurationMin(task) == 0) {
task_to_start_event_[task] = -1;
continue;
@@ -231,14 +234,18 @@ bool DisjunctiveOverloadChecker::Propagate() {
{
const int current_event = task_to_start_event_[current_task];
const bool is_present = helper_->IsPresent(current_task);
// TODO(user): consider reducing max available duration.
const IntegerValue energy_max = helper_->DurationMin(current_task);
const IntegerValue energy_min = is_present ? energy_max : IntegerValue(0);
theta_tree_.AddOrUpdateEvent(current_event,
start_event_time_[current_event], energy_min,
energy_max);
const IntegerValue energy_min = helper_->DurationMin(current_task);
if (helper_->IsPresent(current_task)) {
// TODO(user, stevengay): Add max energy deduction for variable
// durations by putting the energy_max here and modifying the code
// dealing with the optional enveloppe greater than current_end below.
theta_tree_.AddOrUpdateEvent(current_event,
start_event_time_[current_event],
energy_min, energy_min);
} else {
theta_tree_.AddOrUpdateOptionalEvent(
current_event, start_event_time_[current_event], energy_min);
}
}
const IntegerValue current_end = task_time.time;
@@ -250,7 +257,6 @@ bool DisjunctiveOverloadChecker::Propagate() {
const IntegerValue window_start = start_event_time_[critical_event];
const IntegerValue window_end =
theta_tree_.GetEnvelopeOf(critical_event) - 1;
for (int event = critical_event; event < num_events; event++) {
if (theta_tree_.EnergyMin(event) > 0) {
const int task = start_event_to_task_[event];
@@ -271,16 +277,15 @@ bool DisjunctiveOverloadChecker::Propagate() {
helper_->ClearReason();
int critical_event;
int optional_event;
IntegerValue unused;
IntegerValue available_energy;
theta_tree_.GetEventsWithOptionalEnvelopeGreaterThan(
current_end, &critical_event, &optional_event, &unused);
current_end, &critical_event, &optional_event, &available_energy);
const IntegerValue window_start = start_event_time_[critical_event];
const int optional_task = start_event_to_task_[optional_event];
const IntegerValue window_end =
theta_tree_.GetEnvelopeOf(critical_event) +
helper_->DurationMin(optional_task) - 1;
const IntegerValue window_start = start_event_time_[critical_event];
const IntegerValue window_end = current_end +
helper_->DurationMin(optional_task) -
available_energy - 1;
for (int event = critical_event; event < num_events; event++) {
if (theta_tree_.EnergyMin(event) > 0) {
const int task = start_event_to_task_[event];
@@ -377,7 +382,10 @@ bool DisjunctiveDetectablePrecedences::Propagate() {
return false;
}
// We need to reorder t inside task_set_.
// We need to reorder t inside task_set_. Note that if t is in the set,
// it means that the task is present and that IncreaseStartMin() did push
// its start (by opposition to an optional interval where the push might
// not happen if its start is not optional).
task_set_.NotifyEntryIsNowLastIfPresent(
{t, helper_->StartMin(t), helper_->DurationMin(t)});
}

View File

@@ -406,14 +406,20 @@ bool TimeTablingPerTask::SweepTask(int task_id) {
return false;
}
// The profile needs to be recomputed if the task has a mandatory part.
// The profile needs to be recomputed if we pushed something (because it can
// have side effects). Note that for the case where the interval is optional
// but not its start, it is possible that UpdateStartingTime() didn't change
// the start, so we need to test this in order to avoid an infinite loop.
//
// TODO(user): find an efficient way to keep the start_max < new_end_min
// condition. The problem is that ReduceProfile() assumes that by_end_min and
// by_start_max are up to date (this is not necessarily the case if we use
// the old condition). A solution is to update those vector before calling
// ReduceProfile() or to ReduceProfile() directly after BuildProfile() in the
// main loop.
profile_changed_ = true;
if (helper_->StartMin(task_id) != initial_start_min) {
profile_changed_ = true;
}
// Explain that the task should be absent or explain the resource overload.
if (overload) return OverloadOrRemove(task_id, start_max);