OR-Tools  8.2
disjunctive.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <memory>
17
21#include "ortools/sat/integer.h"
22#include "ortools/sat/sat_parameters.pb.h"
25#include "ortools/util/sort.h"
26
27namespace operations_research {
28namespace sat {
29
30std::function<void(Model*)> Disjunctive(
31 const std::vector<IntervalVariable>& vars) {
32 return [=](Model* model) {
33 bool is_all_different = true;
34 IntervalsRepository* repository = model->GetOrCreate<IntervalsRepository>();
35 for (const IntervalVariable var : vars) {
36 if (repository->IsOptional(var) || repository->MinSize(var) != 1 ||
37 repository->MaxSize(var) != 1 ||
38 repository->Start(var).constant != 0 ||
39 repository->Start(var).coeff != 1) {
40 is_all_different = false;
41 break;
42 }
43 }
44 if (is_all_different) {
45 std::vector<IntegerVariable> starts;
46 starts.reserve(vars.size());
47 for (const IntervalVariable var : vars) {
48 starts.push_back(model->Get(StartVar(var)));
49 }
50 model->Add(AllDifferentOnBounds(starts));
51 return;
52 }
53
54 auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
55 const auto& sat_parameters = *model->GetOrCreate<SatParameters>();
56 if (vars.size() > 2 && sat_parameters.use_combined_no_overlap()) {
57 model->GetOrCreate<CombinedDisjunctive<true>>()->AddNoOverlap(vars);
58 model->GetOrCreate<CombinedDisjunctive<false>>()->AddNoOverlap(vars);
59 return;
60 }
61
64 model->TakeOwnership(helper);
65
66 // Experiments to use the timetable only to propagate the disjunctive.
67 if (/*DISABLES_CODE*/ (false)) {
68 const AffineExpression one(IntegerValue(1));
69 std::vector<AffineExpression> demands(vars.size(), one);
71 demands, one, model->GetOrCreate<IntegerTrail>(), helper);
72 timetable->RegisterWith(watcher);
73 model->TakeOwnership(timetable);
74 return;
75 }
76
77 if (vars.size() == 2) {
78 DisjunctiveWithTwoItems* propagator = new DisjunctiveWithTwoItems(helper);
79 propagator->RegisterWith(watcher);
80 model->TakeOwnership(propagator);
81 } else {
82 // We decided to create the propagators in this particular order, but it
83 // shouldn't matter much because of the different priorities used.
84 {
85 // Only one direction is needed by this one.
86 DisjunctiveOverloadChecker* overload_checker =
88 const int id = overload_checker->RegisterWith(watcher);
89 watcher->SetPropagatorPriority(id, 1);
90 model->TakeOwnership(overload_checker);
91 }
92 for (const bool time_direction : {true, false}) {
93 DisjunctiveDetectablePrecedences* detectable_precedences =
94 new DisjunctiveDetectablePrecedences(time_direction, helper);
95 const int id = detectable_precedences->RegisterWith(watcher);
96 watcher->SetPropagatorPriority(id, 2);
97 model->TakeOwnership(detectable_precedences);
98 }
99 for (const bool time_direction : {true, false}) {
100 DisjunctiveNotLast* not_last =
101 new DisjunctiveNotLast(time_direction, helper);
102 const int id = not_last->RegisterWith(watcher);
103 watcher->SetPropagatorPriority(id, 3);
104 model->TakeOwnership(not_last);
105 }
106 for (const bool time_direction : {true, false}) {
107 DisjunctiveEdgeFinding* edge_finding =
108 new DisjunctiveEdgeFinding(time_direction, helper);
109 const int id = edge_finding->RegisterWith(watcher);
110 watcher->SetPropagatorPriority(id, 4);
111 model->TakeOwnership(edge_finding);
112 }
113 }
114
115 // Note that we keep this one even when there is just two intervals. This is
116 // because it might push a variable that is after both of the intervals
117 // using the fact that they are in disjunction.
118 if (sat_parameters.use_precedences_in_disjunctive_constraint() &&
119 !sat_parameters.use_combined_no_overlap()) {
120 for (const bool time_direction : {true, false}) {
122 time_direction, helper, model->GetOrCreate<IntegerTrail>(),
123 model->GetOrCreate<PrecedencesPropagator>());
124 const int id = precedences->RegisterWith(watcher);
125 watcher->SetPropagatorPriority(id, 5);
126 model->TakeOwnership(precedences);
127 }
128 }
129 };
130}
131
133 const std::vector<IntervalVariable>& vars) {
134 return [=](Model* model) {
135 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
136 IntervalsRepository* repository = model->GetOrCreate<IntervalsRepository>();
137 PrecedencesPropagator* precedences =
138 model->GetOrCreate<PrecedencesPropagator>();
139 for (int i = 0; i < vars.size(); ++i) {
140 for (int j = 0; j < i; ++j) {
141 const BooleanVariable boolean_var = sat_solver->NewBooleanVariable();
142 const Literal i_before_j = Literal(boolean_var, true);
143 const Literal j_before_i = i_before_j.Negated();
144 precedences->AddConditionalPrecedence(repository->EndVar(vars[i]),
145 repository->StartVar(vars[j]),
146 i_before_j);
147 precedences->AddConditionalPrecedence(repository->EndVar(vars[j]),
148 repository->StartVar(vars[i]),
149 j_before_i);
150 }
151 }
152 };
153}
154
156 const std::vector<IntervalVariable>& vars) {
157 return [=](Model* model) {
159 model->Add(Disjunctive(vars));
160 };
161}
162
163void TaskSet::AddEntry(const Entry& e) {
164 int j = sorted_tasks_.size();
165 sorted_tasks_.push_back(e);
166 while (j > 0 && sorted_tasks_[j - 1].start_min > e.start_min) {
167 sorted_tasks_[j] = sorted_tasks_[j - 1];
168 --j;
169 }
170 sorted_tasks_[j] = e;
171 DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
172
173 // If the task is added after optimized_restart_, we know that we don't need
174 // to scan the task before optimized_restart_ in the next ComputeEndMin().
175 if (j <= optimized_restart_) optimized_restart_ = 0;
176}
177
179 int t) {
180 const IntegerValue dmin = helper.SizeMin(t);
181 AddEntry({t, std::max(helper.StartMin(t), helper.EndMin(t) - dmin), dmin});
182}
183
185 const int size = sorted_tasks_.size();
186 for (int i = 0;; ++i) {
187 if (i == size) return;
188 if (sorted_tasks_[i].task == e.task) {
189 sorted_tasks_.erase(sorted_tasks_.begin() + i);
190 break;
191 }
192 }
193
194 optimized_restart_ = sorted_tasks_.size();
195 sorted_tasks_.push_back(e);
196 DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
197}
198
200 sorted_tasks_.erase(sorted_tasks_.begin() + index);
201 optimized_restart_ = 0;
202}
203
204IntegerValue TaskSet::ComputeEndMin() const {
205 DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
206 const int size = sorted_tasks_.size();
207 IntegerValue end_min = kMinIntegerValue;
208 for (int i = optimized_restart_; i < size; ++i) {
209 const Entry& e = sorted_tasks_[i];
210 if (e.start_min >= end_min) {
211 optimized_restart_ = i;
212 end_min = e.start_min + e.size_min;
213 } else {
214 end_min += e.size_min;
215 }
216 }
217 return end_min;
218}
219
220IntegerValue TaskSet::ComputeEndMin(int task_to_ignore,
221 int* critical_index) const {
222 // The order in which we process tasks with the same start-min doesn't matter.
223 DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
224 bool ignored = false;
225 const int size = sorted_tasks_.size();
226 IntegerValue end_min = kMinIntegerValue;
227
228 // If the ignored task is last and was the start of the critical block, then
229 // we need to reset optimized_restart_.
230 if (optimized_restart_ + 1 == size &&
231 sorted_tasks_[optimized_restart_].task == task_to_ignore) {
232 optimized_restart_ = 0;
233 }
234
235 for (int i = optimized_restart_; i < size; ++i) {
236 const Entry& e = sorted_tasks_[i];
237 if (e.task == task_to_ignore) {
238 ignored = true;
239 continue;
240 }
241 if (e.start_min >= end_min) {
242 *critical_index = i;
243 if (!ignored) optimized_restart_ = i;
244 end_min = e.start_min + e.size_min;
245 } else {
246 end_min += e.size_min;
247 }
248 }
249 return end_min;
250}
251
253 DCHECK_EQ(helper_->NumTasks(), 2);
254 helper_->SynchronizeAndSetTimeDirection(true);
255
256 // We can't propagate anything if one of the interval is absent for sure.
257 if (helper_->IsAbsent(0) || helper_->IsAbsent(1)) return true;
258
259 // Note that this propagation also take care of the "overload checker" part.
260 // It also propagates as much as possible, even in the presence of task with
261 // variable sizes.
262 //
263 // TODO(user): For optional interval whose presence in unknown and without
264 // optional variable, the end-min may not be propagated to at least (start_min
265 // + size_min). Consider that into the computation so we may decide the
266 // interval forced absence? Same for the start-max.
267 int task_before = 0;
268 int task_after = 1;
269 if (helper_->StartMax(0) < helper_->EndMin(1)) {
270 // Task 0 must be before task 1.
271 } else if (helper_->StartMax(1) < helper_->EndMin(0)) {
272 // Task 1 must be before task 0.
273 std::swap(task_before, task_after);
274 } else {
275 return true;
276 }
277
278 if (helper_->IsPresent(task_before)) {
279 const IntegerValue end_min_before = helper_->EndMin(task_before);
280 if (helper_->StartMin(task_after) < end_min_before) {
281 // Reason for precedences if both present.
282 helper_->ClearReason();
283 helper_->AddReasonForBeingBefore(task_before, task_after);
284
285 // Reason for the bound push.
286 helper_->AddPresenceReason(task_before);
287 helper_->AddEndMinReason(task_before, end_min_before);
288 if (!helper_->IncreaseStartMin(task_after, end_min_before)) {
289 return false;
290 }
291 }
292 }
293
294 if (helper_->IsPresent(task_after)) {
295 const IntegerValue start_max_after = helper_->StartMax(task_after);
296 if (helper_->EndMax(task_before) > start_max_after) {
297 // Reason for precedences if both present.
298 helper_->ClearReason();
299 helper_->AddReasonForBeingBefore(task_before, task_after);
300
301 // Reason for the bound push.
302 helper_->AddPresenceReason(task_after);
303 helper_->AddStartMaxReason(task_after, start_max_after);
304 if (!helper_->DecreaseEndMax(task_before, start_max_after)) {
305 return false;
306 }
307 }
308 }
309
310 return true;
311}
312
314 // This propagator reach the fix point in one pass.
315 const int id = watcher->Register(this);
316 helper_->WatchAllTasks(id, watcher);
317 return id;
318}
319
320template <bool time_direction>
322 : helper_(model->GetOrCreate<AllIntervalsHelper>()) {
323 task_to_disjunctives_.resize(helper_->NumTasks());
324
325 auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
326 const int id = watcher->Register(this);
327 helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/true,
328 /*watch_end_max=*/false);
329 watcher->NotifyThatPropagatorMayNotReachFixedPointInOnePass(id);
330}
331
332template <bool time_direction>
334 const std::vector<IntervalVariable>& vars) {
335 const int index = task_sets_.size();
336 task_sets_.emplace_back(vars.size());
337 end_mins_.push_back(kMinIntegerValue);
338 for (const IntervalVariable var : vars) {
339 task_to_disjunctives_[var.value()].push_back(index);
340 }
341}
342
343template <bool time_direction>
345 helper_->SynchronizeAndSetTimeDirection(time_direction);
346 const auto& task_by_increasing_end_min = helper_->TaskByIncreasingEndMin();
347 const auto& task_by_decreasing_start_max =
348 helper_->TaskByDecreasingStartMax();
349
350 for (auto& task_set : task_sets_) task_set.Clear();
351 end_mins_.assign(end_mins_.size(), kMinIntegerValue);
352 IntegerValue max_of_end_min = kMinIntegerValue;
353
354 const int num_tasks = helper_->NumTasks();
355 task_is_added_.assign(num_tasks, false);
356 int queue_index = num_tasks - 1;
357 for (const auto task_time : task_by_increasing_end_min) {
358 const int t = task_time.task_index;
359 const IntegerValue end_min = task_time.time;
360 if (helper_->IsAbsent(t)) continue;
361
362 // Update all task sets.
363 while (queue_index >= 0) {
364 const auto to_insert = task_by_decreasing_start_max[queue_index];
365 const int task_index = to_insert.task_index;
366 const IntegerValue start_max = to_insert.time;
367 if (end_min <= start_max) break;
368 if (helper_->IsPresent(task_index)) {
369 task_is_added_[task_index] = true;
370 const IntegerValue shifted_smin = helper_->ShiftedStartMin(task_index);
371 const IntegerValue size_min = helper_->SizeMin(task_index);
372 for (const int d_index : task_to_disjunctives_[task_index]) {
373 // TODO(user): AddEntry() and ComputeEndMin() could be combined.
374 task_sets_[d_index].AddEntry({task_index, shifted_smin, size_min});
375 end_mins_[d_index] = task_sets_[d_index].ComputeEndMin();
376 max_of_end_min = std::max(max_of_end_min, end_mins_[d_index]);
377 }
378 }
379 --queue_index;
380 }
381
382 // Find out amongst the disjunctives in which t appear, the one with the
383 // largest end_min, ignoring t itself. This will be the new start min for t.
384 IntegerValue new_start_min = helper_->StartMin(t);
385 if (new_start_min >= max_of_end_min) continue;
386 int best_critical_index = 0;
387 int best_d_index = -1;
388 if (task_is_added_[t]) {
389 for (const int d_index : task_to_disjunctives_[t]) {
390 if (new_start_min >= end_mins_[d_index]) continue;
391 int critical_index = 0;
392 const IntegerValue end_min_of_critical_tasks =
393 task_sets_[d_index].ComputeEndMin(/*task_to_ignore=*/t,
394 &critical_index);
395 DCHECK_LE(end_min_of_critical_tasks, max_of_end_min);
396 if (end_min_of_critical_tasks > new_start_min) {
397 new_start_min = end_min_of_critical_tasks;
398 best_d_index = d_index;
399 best_critical_index = critical_index;
400 }
401 }
402 } else {
403 // If the task t was not added, then there is no task to ignore and
404 // end_mins_[d_index] is up to date.
405 for (const int d_index : task_to_disjunctives_[t]) {
406 if (end_mins_[d_index] > new_start_min) {
407 new_start_min = end_mins_[d_index];
408 best_d_index = d_index;
409 }
410 }
411 if (best_d_index != -1) {
412 const IntegerValue end_min_of_critical_tasks =
413 task_sets_[best_d_index].ComputeEndMin(/*task_to_ignore=*/t,
414 &best_critical_index);
415 CHECK_EQ(end_min_of_critical_tasks, new_start_min);
416 }
417 }
418
419 // Do we push something?
420 if (best_d_index == -1) continue;
421
422 // Same reason as DisjunctiveDetectablePrecedences.
423 // TODO(user): Maybe factor out the code? It does require a function with a
424 // lot of arguments though.
425 helper_->ClearReason();
426 const std::vector<TaskSet::Entry>& sorted_tasks =
427 task_sets_[best_d_index].SortedTasks();
428 const IntegerValue window_start =
429 sorted_tasks[best_critical_index].start_min;
430 for (int i = best_critical_index; i < sorted_tasks.size(); ++i) {
431 const int ct = sorted_tasks[i].task;
432 if (ct == t) continue;
433 helper_->AddPresenceReason(ct);
434 helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min, window_start);
435 helper_->AddStartMaxReason(ct, end_min - 1);
436 }
437 helper_->AddEndMinReason(t, end_min);
438 if (!helper_->IncreaseStartMin(t, new_start_min)) {
439 return false;
440 }
441
442 // We need to reorder t inside task_set_. Note that if t is in the set,
443 // it means that the task is present and that IncreaseStartMin() did push
444 // its start (by opposition to an optional interval where the push might
445 // not happen if its start is not optional).
446 if (task_is_added_[t]) {
447 const IntegerValue shifted_smin = helper_->ShiftedStartMin(t);
448 const IntegerValue size_min = helper_->SizeMin(t);
449 for (const int d_index : task_to_disjunctives_[t]) {
450 task_sets_[d_index].NotifyEntryIsNowLastIfPresent(
451 {t, shifted_smin, size_min});
452 end_mins_[d_index] = task_sets_[d_index].ComputeEndMin();
453 max_of_end_min = std::max(max_of_end_min, end_mins_[d_index]);
454 }
455 }
456 }
457 return true;
458}
459
461 helper_->SynchronizeAndSetTimeDirection(/*is_forward=*/true);
462
463 // Split problem into independent part.
464 //
465 // Many propagators in this file use the same approach, we start by processing
466 // the task by increasing start-min, packing everything to the left. We then
467 // process each "independent" set of task separately. A task is independent
468 // from the one before it, if its start-min wasn't pushed.
469 //
470 // This way, we get one or more window [window_start, window_end] so that for
471 // all task in the window, [start_min, end_min] is inside the window, and the
472 // end min of any set of task to the left is <= window_start, and the
473 // start_min of any task to the right is >= end_min.
474 window_.clear();
475 IntegerValue window_end = kMinIntegerValue;
476 IntegerValue relevant_end;
477 int relevant_size = 0;
478 for (const TaskTime task_time : helper_->TaskByIncreasingShiftedStartMin()) {
479 const int task = task_time.task_index;
480 if (helper_->IsAbsent(task)) continue;
481
482 const IntegerValue start_min = task_time.time;
483 if (start_min < window_end) {
484 window_.push_back(task_time);
485 window_end += helper_->SizeMin(task);
486 if (window_end > helper_->EndMax(task)) {
487 relevant_size = window_.size();
488 relevant_end = window_end;
489 }
490 continue;
491 }
492
493 // Process current window.
494 // We don't need to process the end of the window (after relevant_size)
495 // because these interval can be greedily assembled in a feasible solution.
496 window_.resize(relevant_size);
497 if (relevant_size > 0 && !PropagateSubwindow(relevant_end)) {
498 return false;
499 }
500
501 // Start of the next window.
502 window_.clear();
503 window_.push_back(task_time);
504 window_end = start_min + helper_->SizeMin(task);
505 relevant_size = 0;
506 }
507
508 // Process last window.
509 window_.resize(relevant_size);
510 if (relevant_size > 0 && !PropagateSubwindow(relevant_end)) {
511 return false;
512 }
513
514 return true;
515}
516
517// TODO(user): Improve the Overload Checker using delayed insertion.
518// We insert events at the cost of O(log n) per insertion, and this is where
519// the algorithm spends most of its time, thus it is worth improving.
520// We can insert an arbitrary set of tasks at the cost of O(n) for the whole
521// set. This is useless for the overload checker as is since we need to check
522// overload after every insertion, but we could use an upper bound of the
523// theta envelope to save us from checking the actual value.
524bool DisjunctiveOverloadChecker::PropagateSubwindow(
525 IntegerValue global_window_end) {
526 // Set up theta tree and task_by_increasing_end_max_.
527 const int window_size = window_.size();
528 theta_tree_.Reset(window_size);
529 task_by_increasing_end_max_.clear();
530 for (int i = 0; i < window_size; ++i) {
531 // No point adding a task if its end_max is too large.
532 const int task = window_[i].task_index;
533 const IntegerValue end_max = helper_->EndMax(task);
534 if (end_max < global_window_end) {
535 task_to_event_[task] = i;
536 task_by_increasing_end_max_.push_back({task, end_max});
537 }
538 }
539
540 // Introduce events by increasing end_max, check for overloads.
541 std::sort(task_by_increasing_end_max_.begin(),
542 task_by_increasing_end_max_.end());
543 for (const auto task_time : task_by_increasing_end_max_) {
544 const int current_task = task_time.task_index;
545
546 // We filtered absent task while constructing the subwindow, but it is
547 // possible that as we propagate task absence below, other task also become
548 // absent (if they share the same presence Boolean).
549 if (helper_->IsAbsent(current_task)) continue;
550
551 DCHECK_NE(task_to_event_[current_task], -1);
552 {
553 const int current_event = task_to_event_[current_task];
554 const IntegerValue energy_min = helper_->SizeMin(current_task);
555 if (helper_->IsPresent(current_task)) {
556 // TODO(user,user): Add max energy deduction for variable
557 // sizes by putting the energy_max here and modifying the code
558 // dealing with the optional envelope greater than current_end below.
559 theta_tree_.AddOrUpdateEvent(current_event, window_[current_event].time,
560 energy_min, energy_min);
561 } else {
562 theta_tree_.AddOrUpdateOptionalEvent(
563 current_event, window_[current_event].time, energy_min);
564 }
565 }
566
567 const IntegerValue current_end = task_time.time;
568 if (theta_tree_.GetEnvelope() > current_end) {
569 // Explain failure with tasks in critical interval.
570 helper_->ClearReason();
571 const int critical_event =
572 theta_tree_.GetMaxEventWithEnvelopeGreaterThan(current_end);
573 const IntegerValue window_start = window_[critical_event].time;
574 const IntegerValue window_end =
575 theta_tree_.GetEnvelopeOf(critical_event) - 1;
576 for (int event = critical_event; event < window_size; event++) {
577 const IntegerValue energy_min = theta_tree_.EnergyMin(event);
578 if (energy_min > 0) {
579 const int task = window_[event].task_index;
580 helper_->AddPresenceReason(task);
581 helper_->AddEnergyAfterReason(task, energy_min, window_start);
582 helper_->AddEndMaxReason(task, window_end);
583 }
584 }
585 return helper_->ReportConflict();
586 }
587
588 // Exclude all optional tasks that would overload an interval ending here.
589 while (theta_tree_.GetOptionalEnvelope() > current_end) {
590 // Explain exclusion with tasks present in the critical interval.
591 // TODO(user): This could be done lazily, like most of the loop to
592 // compute the reasons in this file.
593 helper_->ClearReason();
594 int critical_event;
595 int optional_event;
596 IntegerValue available_energy;
598 current_end, &critical_event, &optional_event, &available_energy);
599
600 const int optional_task = window_[optional_event].task_index;
601 const IntegerValue optional_size_min = helper_->SizeMin(optional_task);
602 const IntegerValue window_start = window_[critical_event].time;
603 const IntegerValue window_end =
604 current_end + optional_size_min - available_energy - 1;
605 for (int event = critical_event; event < window_size; event++) {
606 const IntegerValue energy_min = theta_tree_.EnergyMin(event);
607 if (energy_min > 0) {
608 const int task = window_[event].task_index;
609 helper_->AddPresenceReason(task);
610 helper_->AddEnergyAfterReason(task, energy_min, window_start);
611 helper_->AddEndMaxReason(task, window_end);
612 }
613 }
614
615 helper_->AddEnergyAfterReason(optional_task, optional_size_min,
616 window_start);
617 helper_->AddEndMaxReason(optional_task, window_end);
618
619 // If tasks shares the same presence literal, it is possible that we
620 // already pushed this task absence.
621 if (!helper_->IsAbsent(optional_task)) {
622 if (!helper_->PushTaskAbsence(optional_task)) return false;
623 }
624 theta_tree_.RemoveEvent(optional_event);
625 }
626 }
627
628 return true;
629}
630
632 // This propagator reach the fix point in one pass.
633 const int id = watcher->Register(this);
634 helper_->SynchronizeAndSetTimeDirection(/*is_forward=*/true);
635 helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/false,
636 /*watch_end_max=*/true);
637 return id;
638}
639
641 helper_->SynchronizeAndSetTimeDirection(time_direction_);
642
643 to_propagate_.clear();
644 processed_.assign(helper_->NumTasks(), false);
645
646 // Split problem into independent part.
647 //
648 // The "independent" window can be processed separately because for each of
649 // them, a task [start-min, end-min] is in the window [window_start,
650 // window_end]. So any task to the left of the window cannot push such
651 // task start_min, and any task to the right of the window will have a
652 // start_max >= end_min, so wouldn't be in detectable precedence.
653 task_by_increasing_end_min_.clear();
654 IntegerValue window_end = kMinIntegerValue;
655 for (const TaskTime task_time : helper_->TaskByIncreasingShiftedStartMin()) {
656 const int task = task_time.task_index;
657 if (helper_->IsAbsent(task)) continue;
658
659 const IntegerValue shifted_smin = task_time.time;
660 const IntegerValue size_min = helper_->SizeMin(task);
661
662 // Tricky: Because we use the up to date version of size_min (that might
663 // have increased in one of the PropagateSubwindow() call) and the cached
664 // shifted_smin which didn't change, we cannot do shifted_smin +
665 // size_min which might be higher than the actual end_min_if_present.
666 // So we use the updated value instead.
667 //
668 // Note that we have the same problem below when window_end might be higher
669 // that it is actually, but that is fine since we will just decompose less.
670 const IntegerValue end_min_if_present =
671 std::max(helper_->EndMin(task), helper_->StartMin(task) + size_min);
672
673 // Note that we use the real StartMin() here, as this is the one we will
674 // push.
675 if (helper_->StartMin(task) < window_end) {
676 task_by_increasing_end_min_.push_back({task, end_min_if_present});
677 window_end = std::max(window_end, shifted_smin) + size_min;
678 continue;
679 }
680
681 // Process current window.
682 if (task_by_increasing_end_min_.size() > 1 && !PropagateSubwindow()) {
683 return false;
684 }
685
686 // Start of the next window.
687 task_by_increasing_end_min_.clear();
688 task_by_increasing_end_min_.push_back({task, end_min_if_present});
689 window_end = end_min_if_present;
690 }
691
692 if (task_by_increasing_end_min_.size() > 1 && !PropagateSubwindow()) {
693 return false;
694 }
695
696 return true;
697}
698
699bool DisjunctiveDetectablePrecedences::PropagateSubwindow() {
700 DCHECK(!task_by_increasing_end_min_.empty());
701
702 // The vector is already sorted by shifted_start_min, so there is likely a
703 // good correlation, hence the incremental sort.
704 IncrementalSort(task_by_increasing_end_min_.begin(),
705 task_by_increasing_end_min_.end());
706 const IntegerValue max_end_min = task_by_increasing_end_min_.back().time;
707
708 // Fill and sort task_by_increasing_start_max_.
709 //
710 // TODO(user): we should use start max if present, but more generally, all
711 // helper function should probably return values "if present".
712 task_by_increasing_start_max_.clear();
713 for (const TaskTime entry : task_by_increasing_end_min_) {
714 const int task = entry.task_index;
715 const IntegerValue start_max = helper_->StartMax(task);
716 if (start_max < max_end_min && helper_->IsPresent(task)) {
717 task_by_increasing_start_max_.push_back({task, start_max});
718 }
719 }
720 if (task_by_increasing_start_max_.empty()) return true;
721 std::sort(task_by_increasing_start_max_.begin(),
722 task_by_increasing_start_max_.end());
723
724 // Invariant: need_update is false implies that task_set_end_min is equal to
725 // task_set_.ComputeEndMin().
726 //
727 // TODO(user): Maybe it is just faster to merge ComputeEndMin() with
728 // AddEntry().
729 task_set_.Clear();
730 bool need_update = false;
731 IntegerValue task_set_end_min = kMinIntegerValue;
732
733 int queue_index = 0;
734 int blocking_task = -1;
735 const int queue_size = task_by_increasing_start_max_.size();
736 for (const auto task_time : task_by_increasing_end_min_) {
737 // Note that we didn't put absent task in task_by_increasing_end_min_, but
738 // the absence might have been pushed while looping here. This is fine since
739 // any push we do on this task should handle this case correctly.
740 //
741 // TODO(user): Still test and continue the status even if in most cases the
742 // task will not be absent?
743 const int current_task = task_time.task_index;
744 const IntegerValue current_end_min = task_time.time;
745
746 for (; queue_index < queue_size; ++queue_index) {
747 const auto to_insert = task_by_increasing_start_max_[queue_index];
748 const IntegerValue start_max = to_insert.time;
749 if (current_end_min <= start_max) break;
750
751 const int t = to_insert.task_index;
752 DCHECK(helper_->IsPresent(t));
753
754 // If t has not been processed yet, it has a mandatory part, and rather
755 // than adding it right away to task_set, we will delay all propagation
756 // until current_task is equal to this "blocking task".
757 //
758 // This idea is introduced in "Linear-Time Filtering Algorithms for the
759 // Disjunctive Constraints" Hamed Fahimi, Claude-Guy Quimper.
760 //
761 // Experiments seems to indicate that it is slighlty faster rather than
762 // having to ignore one of the task already inserted into task_set_ when
763 // we have tasks with mandatory parts. It also open-up more option for the
764 // data structure used in task_set_.
765 if (!processed_[t]) {
766 if (blocking_task != -1) {
767 // We have two blocking tasks, which means they are in conflict.
768 helper_->ClearReason();
769 helper_->AddPresenceReason(blocking_task);
770 helper_->AddPresenceReason(t);
771 helper_->AddReasonForBeingBefore(blocking_task, t);
772 helper_->AddReasonForBeingBefore(t, blocking_task);
773 return helper_->ReportConflict();
774 }
775 DCHECK_LT(start_max, helper_->ShiftedStartMin(t) + helper_->SizeMin(t))
776 << " task should have mandatory part: "
777 << helper_->TaskDebugString(t);
778 DCHECK(to_propagate_.empty());
779 blocking_task = t;
780 to_propagate_.push_back(t);
781 } else {
782 need_update = true;
783 task_set_.AddShiftedStartMinEntry(*helper_, t);
784 }
785 }
786
787 // If we have a blocking task, we delay the propagation until current_task
788 // is the blocking task.
789 if (blocking_task != current_task) {
790 to_propagate_.push_back(current_task);
791 if (blocking_task != -1) continue;
792 }
793 for (const int t : to_propagate_) {
794 DCHECK(!processed_[t]);
795 processed_[t] = true;
796 if (need_update) {
797 need_update = false;
798 task_set_end_min = task_set_.ComputeEndMin();
799 }
800
801 // task_set_ contains all the tasks that must be executed before t. They
802 // are in "detectable precedence" because their start_max is smaller than
803 // the end-min of t like so:
804 // [(the task t)
805 // (a task in task_set_)]
806 // From there, we deduce that the start-min of t is greater or equal to
807 // the end-min of the critical tasks.
808 //
809 // Note that this works as well when IsPresent(t) is false.
810 if (task_set_end_min > helper_->StartMin(t)) {
811 const int critical_index = task_set_.GetCriticalIndex();
812 const std::vector<TaskSet::Entry>& sorted_tasks =
813 task_set_.SortedTasks();
814 helper_->ClearReason();
815
816 // We need:
817 // - StartMax(ct) < EndMin(t) for the detectable precedence.
818 // - StartMin(ct) >= window_start for the value of task_set_end_min.
819 const IntegerValue end_min_if_present =
820 helper_->ShiftedStartMin(t) + helper_->SizeMin(t);
821 const IntegerValue window_start =
822 sorted_tasks[critical_index].start_min;
823 for (int i = critical_index; i < sorted_tasks.size(); ++i) {
824 const int ct = sorted_tasks[i].task;
825 DCHECK_NE(ct, t);
826 helper_->AddPresenceReason(ct);
827 helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
828 window_start);
829 helper_->AddStartMaxReason(ct, end_min_if_present - 1);
830 }
831
832 // Add the reason for t (we only need the end-min).
833 helper_->AddEndMinReason(t, end_min_if_present);
834
835 // This augment the start-min of t. Note that t is not in task set
836 // yet, so we will use this updated start if we ever add it there.
837 if (!helper_->IncreaseStartMin(t, task_set_end_min)) {
838 return false;
839 }
840
841 // This propagators assumes that every push is reflected for its
842 // correctness.
843 if (helper_->InPropagationLoop()) return true;
844 }
845
846 if (t == blocking_task) {
847 // Insert the blocking_task. Note that because we just pushed it,
848 // it will be last in task_set_ and also the only reason used to push
849 // any of the subsequent tasks. In particular, the reason will be valid
850 // even though task_set might contains tasks with a start_max greater or
851 // equal to the end_min of the task we push.
852 need_update = true;
853 blocking_task = -1;
854 task_set_.AddShiftedStartMinEntry(*helper_, t);
855 }
856 }
857 to_propagate_.clear();
858 }
859 return true;
860}
861
863 GenericLiteralWatcher* watcher) {
864 const int id = watcher->Register(this);
865 helper_->SynchronizeAndSetTimeDirection(time_direction_);
866 helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/true,
867 /*watch_end_max=*/false);
869 return id;
870}
871
873 helper_->SynchronizeAndSetTimeDirection(time_direction_);
874 window_.clear();
875 IntegerValue window_end = kMinIntegerValue;
876 for (const TaskTime task_time : helper_->TaskByIncreasingShiftedStartMin()) {
877 const int task = task_time.task_index;
878 if (!helper_->IsPresent(task)) continue;
879
880 const IntegerValue start_min = task_time.time;
881 if (start_min < window_end) {
882 window_.push_back(task_time);
883 window_end += helper_->SizeMin(task);
884 continue;
885 }
886
887 if (window_.size() > 1 && !PropagateSubwindow()) {
888 return false;
889 }
890
891 // Start of the next window.
892 window_.clear();
893 window_.push_back(task_time);
894 window_end = start_min + helper_->SizeMin(task);
895 }
896 if (window_.size() > 1 && !PropagateSubwindow()) {
897 return false;
898 }
899 return true;
900}
901
902bool DisjunctivePrecedences::PropagateSubwindow() {
903 // TODO(user): We shouldn't consider ends for fixed intervals here. But
904 // then we should do a better job of computing the min-end of a subset of
905 // intervals from this disjunctive (like using fixed intervals even if there
906 // is no "before that variable" relationship). Ex: If a variable is after two
907 // intervals that cannot be both before a fixed one, we could propagate more.
908 index_to_end_vars_.clear();
909 for (const auto task_time : window_) {
910 const int task = task_time.task_index;
911 const AffineExpression& end_exp = helper_->Ends()[task];
912
913 // TODO(user): Handle generic affine relation?
914 if (end_exp.var == kNoIntegerVariable || end_exp.coeff != 1) continue;
915 index_to_end_vars_.push_back(end_exp.var);
916 }
917 precedences_->ComputePrecedences(index_to_end_vars_, &before_);
918
919 const int size = before_.size();
920 for (int i = 0; i < size;) {
921 const IntegerVariable var = before_[i].var;
923 task_set_.Clear();
924
925 const int initial_i = i;
926 IntegerValue min_offset = kMaxIntegerValue;
927 for (; i < size && before_[i].var == var; ++i) {
928 const TaskTime task_time = window_[before_[i].index];
929
930 // We have var >= end_exp.var + offset, so
931 // var >= (end_exp.var + end_exp.constant) + (offset - end_exp.constant)
932 // var >= task end + new_offset.
933 const AffineExpression& end_exp = helper_->Ends()[task_time.task_index];
934 min_offset = std::min(min_offset, before_[i].offset - end_exp.constant);
935
936 // The task are actually in sorted order, so we do not need to call
937 // task_set_.Sort(). This property is DCHECKed.
938 task_set_.AddUnsortedEntry({task_time.task_index, task_time.time,
939 helper_->SizeMin(task_time.task_index)});
940 }
941 DCHECK_GE(task_set_.SortedTasks().size(), 2);
942 if (integer_trail_->IsCurrentlyIgnored(var)) continue;
943
944 // TODO(user): Only use the min_offset of the critical task? Or maybe do a
945 // more general computation to find by how much we can push var?
946 const IntegerValue new_lb = task_set_.ComputeEndMin() + min_offset;
947 if (new_lb > integer_trail_->LowerBound(var)) {
948 const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
949 helper_->ClearReason();
950
951 // Fill task_to_arc_index_ since we need it for the reason.
952 // Note that we do not care about the initial content of this vector.
953 for (int j = initial_i; j < i; ++j) {
954 const int task = window_[before_[j].index].task_index;
955 task_to_arc_index_[task] = before_[j].arc_index;
956 }
957
958 const int critical_index = task_set_.GetCriticalIndex();
959 const IntegerValue window_start = sorted_tasks[critical_index].start_min;
960 for (int i = critical_index; i < sorted_tasks.size(); ++i) {
961 const int ct = sorted_tasks[i].task;
962 helper_->AddPresenceReason(ct);
963 helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
964 window_start);
965
966 const AffineExpression& end_exp = helper_->Ends()[ct];
967 precedences_->AddPrecedenceReason(
968 task_to_arc_index_[ct], min_offset + end_exp.constant,
969 helper_->MutableLiteralReason(), helper_->MutableIntegerReason());
970 }
971
972 // TODO(user): If var is actually a start-min of an interval, we
973 // could push the end-min and check the interval consistency right away.
974 if (!helper_->PushIntegerLiteral(
976 return false;
977 }
978 }
979 }
980 return true;
981}
982
984 // This propagator reach the fixed point in one go.
985 const int id = watcher->Register(this);
986 helper_->SynchronizeAndSetTimeDirection(time_direction_);
987 helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/false,
988 /*watch_end_max=*/false);
989 return id;
990}
991
993 helper_->SynchronizeAndSetTimeDirection(time_direction_);
994
995 const auto& task_by_decreasing_start_max =
996 helper_->TaskByDecreasingStartMax();
997 const auto& task_by_increasing_shifted_start_min =
999
1000 // Split problem into independent part.
1001 //
1002 // The situation is trickier here, and we use two windows:
1003 // - The classical "start_min_window_" as in the other propagator.
1004 // - A second window, that includes all the task with a start_max inside
1005 // [window_start, window_end].
1006 //
1007 // Now, a task from the second window can be detected to be "not last" by only
1008 // looking at the task in the first window. Tasks to the left do not cause
1009 // issue for the task to be last, and tasks to the right will not lower the
1010 // end-min of the task under consideration.
1011 int queue_index = task_by_decreasing_start_max.size() - 1;
1012 const int num_tasks = task_by_increasing_shifted_start_min.size();
1013 for (int i = 0; i < num_tasks;) {
1014 start_min_window_.clear();
1015 IntegerValue window_end = kMinIntegerValue;
1016 for (; i < num_tasks; ++i) {
1017 const TaskTime task_time = task_by_increasing_shifted_start_min[i];
1018 const int task = task_time.task_index;
1019 if (!helper_->IsPresent(task)) continue;
1020
1021 const IntegerValue start_min = task_time.time;
1022 if (start_min_window_.empty()) {
1023 start_min_window_.push_back(task_time);
1024 window_end = start_min + helper_->SizeMin(task);
1025 } else if (start_min < window_end) {
1026 start_min_window_.push_back(task_time);
1027 window_end += helper_->SizeMin(task);
1028 } else {
1029 break;
1030 }
1031 }
1032
1033 // Add to start_max_window_ all the task whose start_max
1034 // fall into [window_start, window_end).
1035 start_max_window_.clear();
1036 for (; queue_index >= 0; queue_index--) {
1037 const auto task_time = task_by_decreasing_start_max[queue_index];
1038
1039 // Note that we add task whose presence is still unknown here.
1040 if (task_time.time >= window_end) break;
1041 if (helper_->IsAbsent(task_time.task_index)) continue;
1042 start_max_window_.push_back(task_time);
1043 }
1044
1045 // If this is the case, we cannot propagate more than the detectable
1046 // precedence propagator. Note that this continue must happen after we
1047 // computed start_max_window_ though.
1048 if (start_min_window_.size() <= 1) continue;
1049
1050 // Process current window.
1051 if (!start_max_window_.empty() && !PropagateSubwindow()) {
1052 return false;
1053 }
1054 }
1055 return true;
1056}
1057
1058bool DisjunctiveNotLast::PropagateSubwindow() {
1059 auto& task_by_increasing_end_max = start_max_window_;
1060 for (TaskTime& entry : task_by_increasing_end_max) {
1061 entry.time = helper_->EndMax(entry.task_index);
1062 }
1063 IncrementalSort(task_by_increasing_end_max.begin(),
1064 task_by_increasing_end_max.end());
1065
1066 const IntegerValue threshold = task_by_increasing_end_max.back().time;
1067 auto& task_by_increasing_start_max = start_min_window_;
1068 int queue_size = 0;
1069 for (const TaskTime entry : task_by_increasing_start_max) {
1070 const int task = entry.task_index;
1071 const IntegerValue start_max = helper_->StartMax(task);
1072 DCHECK(helper_->IsPresent(task));
1073 if (start_max < threshold) {
1074 task_by_increasing_start_max[queue_size++] = {task, start_max};
1075 }
1076 }
1077
1078 // If the size is one, we cannot propagate more than the detectable precedence
1079 // propagator.
1080 if (queue_size <= 1) return true;
1081
1082 task_by_increasing_start_max.resize(queue_size);
1083 std::sort(task_by_increasing_start_max.begin(),
1084 task_by_increasing_start_max.end());
1085
1086 task_set_.Clear();
1087 int queue_index = 0;
1088 for (const auto task_time : task_by_increasing_end_max) {
1089 const int t = task_time.task_index;
1090 const IntegerValue end_max = task_time.time;
1091 DCHECK(!helper_->IsAbsent(t));
1092
1093 // task_set_ contains all the tasks that must start before the end-max of t.
1094 // These are the only candidates that have a chance to decrease the end-max
1095 // of t.
1096 while (queue_index < queue_size) {
1097 const auto to_insert = task_by_increasing_start_max[queue_index];
1098 const IntegerValue start_max = to_insert.time;
1099 if (end_max <= start_max) break;
1100
1101 const int task_index = to_insert.task_index;
1102 DCHECK(helper_->IsPresent(task_index));
1103 task_set_.AddEntry({task_index, helper_->ShiftedStartMin(task_index),
1104 helper_->SizeMin(task_index)});
1105 ++queue_index;
1106 }
1107
1108 // In the following case, task t cannot be after all the critical tasks
1109 // (i.e. it cannot be last):
1110 //
1111 // [(critical tasks)
1112 // | <- t start-max
1113 //
1114 // So we can deduce that the end-max of t is smaller than or equal to the
1115 // largest start-max of the critical tasks.
1116 //
1117 // Note that this works as well when the presence of t is still unknown.
1118 int critical_index = 0;
1119 const IntegerValue end_min_of_critical_tasks =
1120 task_set_.ComputeEndMin(/*task_to_ignore=*/t, &critical_index);
1121 if (end_min_of_critical_tasks <= helper_->StartMax(t)) continue;
1122
1123 // Find the largest start-max of the critical tasks (excluding t). The
1124 // end-max for t need to be smaller than or equal to this.
1125 IntegerValue largest_ct_start_max = kMinIntegerValue;
1126 const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
1127 const int sorted_tasks_size = sorted_tasks.size();
1128 for (int i = critical_index; i < sorted_tasks_size; ++i) {
1129 const int ct = sorted_tasks[i].task;
1130 if (t == ct) continue;
1131 const IntegerValue start_max = helper_->StartMax(ct);
1132 if (start_max > largest_ct_start_max) {
1133 largest_ct_start_max = start_max;
1134 }
1135 }
1136
1137 // If we have any critical task, the test will always be true because
1138 // of the tasks we put in task_set_.
1139 DCHECK(largest_ct_start_max == kMinIntegerValue ||
1140 end_max > largest_ct_start_max);
1141 if (end_max > largest_ct_start_max) {
1142 helper_->ClearReason();
1143
1144 const IntegerValue window_start = sorted_tasks[critical_index].start_min;
1145 for (int i = critical_index; i < sorted_tasks_size; ++i) {
1146 const int ct = sorted_tasks[i].task;
1147 if (ct == t) continue;
1148 helper_->AddPresenceReason(ct);
1149 helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
1150 window_start);
1151 helper_->AddStartMaxReason(ct, largest_ct_start_max);
1152 }
1153
1154 // Add the reason for t, we only need the start-max.
1155 helper_->AddStartMaxReason(t, end_min_of_critical_tasks - 1);
1156
1157 // Enqueue the new end-max for t.
1158 // Note that changing it will not influence the rest of the loop.
1159 if (!helper_->DecreaseEndMax(t, largest_ct_start_max)) return false;
1160 }
1161 }
1162 return true;
1163}
1164
1166 const int id = watcher->Register(this);
1167 helper_->WatchAllTasks(id, watcher);
1169 return id;
1170}
1171
1173 const int num_tasks = helper_->NumTasks();
1174 helper_->SynchronizeAndSetTimeDirection(time_direction_);
1175 is_gray_.resize(num_tasks, false);
1176 non_gray_task_to_event_.resize(num_tasks);
1177
1178 window_.clear();
1179 IntegerValue window_end = kMinIntegerValue;
1180 for (const TaskTime task_time : helper_->TaskByIncreasingShiftedStartMin()) {
1181 const int task = task_time.task_index;
1182 if (helper_->IsAbsent(task)) continue;
1183
1184 // Note that we use the real start min here not the shifted one. This is
1185 // because we might be able to push it if it is smaller than window end.
1186 if (helper_->StartMin(task) < window_end) {
1187 window_.push_back(task_time);
1188 window_end += helper_->SizeMin(task);
1189 continue;
1190 }
1191
1192 // We need at least 3 tasks for the edge-finding to be different from
1193 // detectable precedences.
1194 if (window_.size() > 2 && !PropagateSubwindow(window_end)) {
1195 return false;
1196 }
1197
1198 // Start of the next window.
1199 window_.clear();
1200 window_.push_back(task_time);
1201 window_end = task_time.time + helper_->SizeMin(task);
1202 }
1203 if (window_.size() > 2 && !PropagateSubwindow(window_end)) {
1204 return false;
1205 }
1206 return true;
1207}
1208
1209bool DisjunctiveEdgeFinding::PropagateSubwindow(IntegerValue window_end_min) {
1210 // Cache the task end-max and abort early if possible.
1211 task_by_increasing_end_max_.clear();
1212 for (const auto task_time : window_) {
1213 const int task = task_time.task_index;
1214 DCHECK(!helper_->IsAbsent(task));
1215
1216 // We already mark all the non-present task as gray.
1217 //
1218 // Same for task with an end-max that is too large: Tasks that are not
1219 // present can never trigger propagation or an overload checking failure.
1220 // theta_tree_.GetOptionalEnvelope() is always <= window_end, so tasks whose
1221 // end_max is >= window_end can never trigger propagation or failure either.
1222 // Thus, those tasks can be marked as gray, which removes their contribution
1223 // to theta right away.
1224 const IntegerValue end_max = helper_->EndMax(task);
1225 if (helper_->IsPresent(task) && end_max < window_end_min) {
1226 is_gray_[task] = false;
1227 task_by_increasing_end_max_.push_back({task, end_max});
1228 } else {
1229 is_gray_[task] = true;
1230 }
1231 }
1232
1233 // If we have just 1 non-gray task, then this propagator does not propagate
1234 // more than the detectable precedences, so we abort early.
1235 if (task_by_increasing_end_max_.size() < 2) return true;
1236 std::sort(task_by_increasing_end_max_.begin(),
1237 task_by_increasing_end_max_.end());
1238
1239 // Set up theta tree.
1240 //
1241 // Some task in the theta tree will be considered "gray".
1242 // When computing the end-min of the sorted task, we will compute it for:
1243 // - All the non-gray task
1244 // - All the non-gray task + at most one gray task.
1245 //
1246 // TODO(user): it should be faster to initialize it all at once rather
1247 // than calling AddOrUpdate() n times.
1248 const int window_size = window_.size();
1249 event_size_.clear();
1250 theta_tree_.Reset(window_size);
1251 for (int event = 0; event < window_size; ++event) {
1252 const TaskTime task_time = window_[event];
1253 const int task = task_time.task_index;
1254 const IntegerValue energy_min = helper_->SizeMin(task);
1255 event_size_.push_back(energy_min);
1256 if (is_gray_[task]) {
1257 theta_tree_.AddOrUpdateOptionalEvent(event, task_time.time, energy_min);
1258 } else {
1259 non_gray_task_to_event_[task] = event;
1260 theta_tree_.AddOrUpdateEvent(event, task_time.time, energy_min,
1261 energy_min);
1262 }
1263 }
1264
1265 // At each iteration we either transform a non-gray task into a gray one or
1266 // remove a gray task, so this loop is linear in complexity.
1267 while (true) {
1268 DCHECK(!is_gray_[task_by_increasing_end_max_.back().task_index]);
1269 const IntegerValue non_gray_end_max =
1270 task_by_increasing_end_max_.back().time;
1271
1272 // Overload checking.
1273 const IntegerValue non_gray_end_min = theta_tree_.GetEnvelope();
1274 if (non_gray_end_min > non_gray_end_max) {
1275 helper_->ClearReason();
1276
1277 // We need the reasons for the critical tasks to fall in:
1278 const int critical_event =
1279 theta_tree_.GetMaxEventWithEnvelopeGreaterThan(non_gray_end_max);
1280 const IntegerValue window_start = window_[critical_event].time;
1281 const IntegerValue window_end =
1282 theta_tree_.GetEnvelopeOf(critical_event) - 1;
1283 for (int event = critical_event; event < window_size; event++) {
1284 const int task = window_[event].task_index;
1285 if (is_gray_[task]) continue;
1286 helper_->AddPresenceReason(task);
1287 helper_->AddEnergyAfterReason(task, event_size_[event], window_start);
1288 helper_->AddEndMaxReason(task, window_end);
1289 }
1290 return helper_->ReportConflict();
1291 }
1292
1293 // Edge-finding.
1294 // If we have a situation like:
1295 // [(critical_task_with_gray_task)
1296 // ]
1297 // ^ end-max without the gray task.
1298 //
1299 // Then the gray task must be after all the critical tasks (all the non-gray
1300 // tasks in the tree actually), otherwise there will be no way to schedule
1301 // the critical_tasks inside their time window.
1302 while (theta_tree_.GetOptionalEnvelope() > non_gray_end_max) {
1303 int critical_event_with_gray;
1304 int gray_event;
1305 IntegerValue available_energy;
1307 non_gray_end_max, &critical_event_with_gray, &gray_event,
1308 &available_energy);
1309 const int gray_task = window_[gray_event].task_index;
1310
1311 // Since the gray task is after all the other, we have a new lower bound.
1312 DCHECK(is_gray_[gray_task]);
1313 if (helper_->StartMin(gray_task) < non_gray_end_min) {
1314 // The API is not ideal here. We just want the start of the critical
1315 // tasks that explain the non_gray_end_min computed above.
1316 const int critical_event =
1317 theta_tree_.GetMaxEventWithEnvelopeGreaterThan(non_gray_end_min -
1318 1);
1319 const int first_event =
1320 std::min(critical_event, critical_event_with_gray);
1321 const int second_event =
1322 std::max(critical_event, critical_event_with_gray);
1323 const IntegerValue first_start = window_[first_event].time;
1324 const IntegerValue second_start = window_[second_event].time;
1325
1326 // window_end is chosen to be has big as possible and still have an
1327 // overload if the gray task is not last.
1328 const IntegerValue window_end =
1329 non_gray_end_max + event_size_[gray_event] - available_energy - 1;
1330 CHECK_GE(window_end, non_gray_end_max);
1331
1332 // The non-gray part of the explanation as detailed above.
1333 helper_->ClearReason();
1334 for (int event = first_event; event < window_size; event++) {
1335 const int task = window_[event].task_index;
1336 if (is_gray_[task]) continue;
1337 helper_->AddPresenceReason(task);
1338 helper_->AddEnergyAfterReason(
1339 task, event_size_[event],
1340 event >= second_event ? second_start : first_start);
1341 helper_->AddEndMaxReason(task, window_end);
1342 }
1343
1344 // Add the reason for the gray_task (we don't need the end-max or
1345 // presence reason).
1346 helper_->AddEnergyAfterReason(gray_task, event_size_[gray_event],
1347 window_[critical_event_with_gray].time);
1348
1349 // Enqueue the new start-min for gray_task.
1350 //
1351 // TODO(user): propagate the precedence Boolean here too? I think it
1352 // will be more powerful. Even if eventually all these precedence will
1353 // become detectable (see Petr Villim PhD).
1354 if (!helper_->IncreaseStartMin(gray_task, non_gray_end_min)) {
1355 return false;
1356 }
1357 }
1358
1359 // Remove the gray_task.
1360 theta_tree_.RemoveEvent(gray_event);
1361 }
1362
1363 // Stop before we get just one non-gray task.
1364 if (task_by_increasing_end_max_.size() <= 2) break;
1365
1366 // Stop if the min of end_max is too big.
1367 if (task_by_increasing_end_max_[0].time >=
1368 theta_tree_.GetOptionalEnvelope()) {
1369 break;
1370 }
1371
1372 // Make the non-gray task with larger end-max gray.
1373 const int new_gray_task = task_by_increasing_end_max_.back().task_index;
1374 task_by_increasing_end_max_.pop_back();
1375 const int new_gray_event = non_gray_task_to_event_[new_gray_task];
1376 DCHECK(!is_gray_[new_gray_task]);
1377 is_gray_[new_gray_task] = true;
1378 theta_tree_.AddOrUpdateOptionalEvent(new_gray_event,
1379 window_[new_gray_event].time,
1380 event_size_[new_gray_event]);
1381 }
1382
1383 return true;
1384}
1385
1387 const int id = watcher->Register(this);
1388 helper_->SynchronizeAndSetTimeDirection(time_direction_);
1389 helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/false,
1390 /*watch_end_max=*/true);
1392 return id;
1393}
1394
1395} // namespace sat
1396} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
void AddNoOverlap(const std::vector< IntervalVariable > &var)
Definition: disjunctive.cc:333
int RegisterWith(GenericLiteralWatcher *watcher)
Definition: disjunctive.cc:862
int RegisterWith(GenericLiteralWatcher *watcher)
int RegisterWith(GenericLiteralWatcher *watcher)
int RegisterWith(GenericLiteralWatcher *watcher)
Definition: disjunctive.cc:631
int RegisterWith(GenericLiteralWatcher *watcher)
Definition: disjunctive.cc:983
int RegisterWith(GenericLiteralWatcher *watcher)
Definition: disjunctive.cc:313
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
bool IsCurrentlyIgnored(IntegerVariable i) const
Definition: integer.h:625
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
IntegerValue MaxSize(IntervalVariable i) const
Definition: intervals.h:125
AffineExpression Start(IntervalVariable i) const
Definition: intervals.h:93
IntegerValue MinSize(IntervalVariable i) const
Definition: intervals.h:120
bool IsOptional(IntervalVariable i) const
Definition: intervals.h:70
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
void AddPrecedenceReason(int arc_index, IntegerValue min_offset, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
Definition: precedences.cc:212
void ComputePrecedences(const std::vector< IntegerVariable > &vars, std::vector< IntegerPrecedences > *output)
Definition: precedences.cc:135
BooleanVariable NewBooleanVariable()
Definition: sat_solver.h:83
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
Definition: intervals.cc:378
std::vector< IntegerLiteral > * MutableIntegerReason()
Definition: intervals.h:296
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t)
Definition: intervals.cc:423
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
Definition: intervals.cc:460
void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time)
Definition: intervals.h:566
void AddEndMinReason(int t, IntegerValue lower_bound)
Definition: intervals.h:535
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_start_min)
Definition: intervals.cc:405
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_start_max)
Definition: intervals.cc:414
const std::vector< TaskTime > & TaskByDecreasingStartMax()
Definition: intervals.cc:289
void AddEndMaxReason(int t, IntegerValue upper_bound)
Definition: intervals.h:557
const std::vector< TaskTime > & TaskByIncreasingShiftedStartMin()
Definition: intervals.cc:314
void AddReasonForBeingBefore(int before, int after)
Definition: intervals.cc:334
void AddStartMaxReason(int t, IntegerValue upper_bound)
Definition: intervals.h:513
const std::vector< AffineExpression > & Ends() const
Definition: intervals.h:320
void AddUnsortedEntry(const Entry &e)
Definition: disjunctive.h:89
void NotifyEntryIsNowLastIfPresent(const Entry &e)
Definition: disjunctive.cc:184
const std::vector< Entry > & SortedTasks() const
Definition: disjunctive.h:119
void AddShiftedStartMinEntry(const SchedulingConstraintHelper &helper, int t)
Definition: disjunctive.cc:178
IntegerValue ComputeEndMin() const
Definition: disjunctive.cc:204
void AddEntry(const Entry &e)
Definition: disjunctive.cc:163
IntegerValue ComputeEndMin(int task_to_ignore, int *critical_index) const
Definition: disjunctive.cc:220
IntegerType GetEnvelopeOf(int event) const
Definition: theta_tree.cc:202
void GetEventsWithOptionalEnvelopeGreaterThan(IntegerType target_envelope, int *critical_event, int *optional_event, IntegerType *available_energy) const
Definition: theta_tree.cc:189
int GetMaxEventWithEnvelopeGreaterThan(IntegerType target_envelope) const
Definition: theta_tree.cc:179
void AddOrUpdateOptionalEvent(int event, IntegerType initial_envelope_opt, IntegerType energy_max)
Definition: theta_tree.cc:124
IntegerType EnergyMin(int event) const
Definition: theta_tree.h:197
void AddOrUpdateEvent(int event, IntegerType initial_envelope, IntegerType energy_min, IntegerType energy_max)
Definition: theta_tree.cc:111
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: timetable.cc:313
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< IntegerVariable(const Model &)> StartVar(IntervalVariable v)
Definition: intervals.h:587
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< IntegerVariable > &vars)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> DisjunctiveWithBooleanPrecedencesOnly(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:132
std::function< void(Model *)> DisjunctiveWithBooleanPrecedences(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:155
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:30
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
void IncrementalSort(int max_comparisons, Iterator begin, Iterator end, Compare comp=Compare{}, bool is_stable=false)
Definition: sort.h:46
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
Rev< int64 > end_min
Rev< int64 > end_max
Rev< int64 > start_max
Rev< int64 > start_min
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
Definition: disjunctive.h:60
int task
Definition: disjunctive.h:61
IntegerValue size_min
Definition: disjunctive.h:63
IntegerValue start_min
Definition: disjunctive.h:62