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 
19 #include "ortools/base/logging.h"
21 #include "ortools/sat/integer.h"
22 #include "ortools/sat/sat_parameters.pb.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  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);
70  TimeTablingPerTask* timetable = new TimeTablingPerTask(
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 =
87  new DisjunctiveOverloadChecker(helper);
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 
163 void 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 
204 IntegerValue 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 
220 IntegerValue 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 
320 template <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 
332 template <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 
343 template <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.
524 bool 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 
699 bool 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 
902 bool 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 
1058 bool 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 
1209 bool 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
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
std::vector< IntegerLiteral > * MutableIntegerReason()
Definition: intervals.h:296
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
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
const std::vector< Entry > & SortedTasks() const
Definition: disjunctive.h:119
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 kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
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
std::function< IntegerVariable(const Model &)> StartVar(IntervalVariable v)
Definition: intervals.h:587
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