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