OR-Tools  8.2
intervals.h
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
14#ifndef OR_TOOLS_SAT_INTERVALS_H_
15#define OR_TOOLS_SAT_INTERVALS_H_
16
17#include <functional>
18#include <vector>
19
20#include "absl/types/span.h"
24#include "ortools/base/macros.h"
27#include "ortools/sat/integer.h"
29#include "ortools/sat/model.h"
34
35namespace operations_research {
36namespace sat {
37
38DEFINE_INT_TYPE(IntervalVariable, int32);
39const IntervalVariable kNoIntervalVariable(-1);
40
41// This class maintains a set of intervals which correspond to three integer
42// variables (start, end and size). It automatically registers with the
43// PrecedencesPropagator the relation between the bounds of each interval and
44// provides many helper functions to add precedences relation between intervals.
46 public:
48 : model_(model),
49 assignment_(model->GetOrCreate<Trail>()->Assignment()),
50 integer_trail_(model->GetOrCreate<IntegerTrail>()) {}
51
52 // Returns the current number of intervals in the repository.
53 // The interval will always be identified by an integer in [0, num_intervals).
54 int NumIntervals() const { return starts_.size(); }
55
56 // Functions to add a new interval to the repository.
57 // If add_linear_relation is true, then we also link start, size and end.
58 //
59 // - If size == kNoIntegerVariable, then the size is fixed to fixed_size.
60 // - If is_present != kNoLiteralIndex, then this is an optional interval.
61 IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end,
62 IntegerVariable size, IntegerValue fixed_size,
63 LiteralIndex is_present);
64 IntervalVariable CreateInterval(AffineExpression start, AffineExpression end,
66 LiteralIndex is_present,
67 bool add_linear_relation);
68
69 // Returns whether or not a interval is optional and the associated literal.
70 bool IsOptional(IntervalVariable i) const {
71 return is_present_[i] != kNoLiteralIndex;
72 }
73 Literal PresenceLiteral(IntervalVariable i) const {
74 return Literal(is_present_[i]);
75 }
76 bool IsPresent(IntervalVariable i) const {
77 if (!IsOptional(i)) return true;
78 return assignment_.LiteralIsTrue(PresenceLiteral(i));
79 }
80 bool IsAbsent(IntervalVariable i) const {
81 if (!IsOptional(i)) return false;
82 return assignment_.LiteralIsFalse(PresenceLiteral(i));
83 }
84
85 // The 3 integer variables associated to a interval.
86 // Fixed size intervals will have a kNoIntegerVariable as size.
87 //
88 // Note: For an optional interval, the start/end variables are propagated
89 // asssuming the interval is present. Because of that, these variables can
90 // cross each other or have an empty domain. If any of this happen, then the
91 // PresenceLiteral() of this interval will be propagated to false.
92 AffineExpression Size(IntervalVariable i) const { return sizes_[i]; }
93 AffineExpression Start(IntervalVariable i) const { return starts_[i]; }
94 AffineExpression End(IntervalVariable i) const { return ends_[i]; }
95
96 // Deprecated.
97 IntegerVariable SizeVar(IntervalVariable i) const {
98 if (sizes_[i].var != kNoIntegerVariable) {
99 CHECK_EQ(sizes_[i].coeff, 1);
100 CHECK_EQ(sizes_[i].constant, 0);
101 }
102 return sizes_[i].var;
103 }
104 IntegerVariable StartVar(IntervalVariable i) const {
105 if (starts_[i].var != kNoIntegerVariable) {
106 CHECK_EQ(starts_[i].coeff, 1);
107 CHECK_EQ(starts_[i].constant, 0);
108 }
109 return starts_[i].var;
110 }
111 IntegerVariable EndVar(IntervalVariable i) const {
112 if (ends_[i].var != kNoIntegerVariable) {
113 CHECK_EQ(ends_[i].coeff, 1);
114 CHECK_EQ(ends_[i].constant, 0);
115 }
116 return ends_[i].var;
117 }
118
119 // Return the minimum size of the given IntervalVariable.
120 IntegerValue MinSize(IntervalVariable i) const {
121 return integer_trail_->LowerBound(sizes_[i]);
122 }
123
124 // Return the maximum size of the given IntervalVariable.
125 IntegerValue MaxSize(IntervalVariable i) const {
126 return integer_trail_->UpperBound(sizes_[i]);
127 }
128
129 // Utility function that returns a vector will all intervals.
130 std::vector<IntervalVariable> AllIntervals() const {
131 std::vector<IntervalVariable> result;
132 for (IntervalVariable i(0); i < NumIntervals(); ++i) {
133 result.push_back(i);
134 }
135 return result;
136 }
137
138 private:
139 // External classes needed.
140 Model* model_;
141 const VariablesAssignment& assignment_;
142 IntegerTrail* integer_trail_;
143
144 // Literal indicating if the tasks is executed. Tasks that are always executed
145 // will have a kNoLiteralIndex entry in this vector.
147
148 // The integer variables for each tasks.
152
153 DISALLOW_COPY_AND_ASSIGN(IntervalsRepository);
154};
155
156// An helper struct to sort task by time. This is used by the
157// SchedulingConstraintHelper but also by many scheduling propagators to sort
158// tasks.
159struct TaskTime {
161 IntegerValue time;
162 bool operator<(TaskTime other) const { return time < other.time; }
163 bool operator>(TaskTime other) const { return time > other.time; }
164};
165
166// Helper class shared by the propagators that manage a given list of tasks.
167//
168// One of the main advantage of this class is that it allows to share the
169// vectors of tasks sorted by various criteria between propagator for a faster
170// code.
173 public:
174 // All the functions below refer to a task by its index t in the tasks
175 // vector given at construction.
176 SchedulingConstraintHelper(const std::vector<IntervalVariable>& tasks,
177 Model* model);
178
179 // Temporary constructor.
180 // The class will not be usable until ResetFromSubset() is called.
181 //
182 // TODO(user): Remove this. It is a hack because the disjunctive class needs
183 // to fetch the maximum possible number of task at construction.
184 SchedulingConstraintHelper(int num_tasks, Model* model);
185
186 // This is a propagator so we can "cache" all the intervals relevant
187 // information. This gives good speedup. Note however that the info is stale
188 // except if a bound was pushed by this helper or if this was called. We run
189 // it at the highest priority, so that will mostly be the case at the
190 // beginning of each Propagate() call of the classes using this.
191 bool Propagate() final;
192 bool IncrementalPropagate(const std::vector<int>& watch_indices) final;
193 void RegisterWith(GenericLiteralWatcher* watcher);
194 void SetLevel(int level) final;
195
196 // Resets the class to the same state as if it was constructed with
197 // the given subset of tasks from other.
199 absl::Span<const int> tasks);
200
201 // Returns the number of task.
202 int NumTasks() const { return starts_.size(); }
203
204 // Make sure the cached values are up to date. Also sets the time direction to
205 // either forward/backward. This will impact all the functions below. This
206 // MUST be called at the beginning of all Propagate() call that uses this
207 // helper.
208 void SynchronizeAndSetTimeDirection(bool is_forward);
209
210 // Helpers for the current bounds on the current task time window.
211 // [ (size-min) ... (size-min) ]
212 // ^ ^ ^ ^
213 // start-min end-min start-max end-max
214 //
215 // Note that for tasks with variable durations, we don't necessarily have
216 // duration-min between the XXX-min and XXX-max value.
217 //
218 // Remark: We use cached values for most of these function as this is faster.
219 // In practice, the cache will almost always be up to date, but not in corner
220 // cases where pushing the start of one task will change values for many
221 // others. This is fine as the new values will be picked up as we reach the
222 // propagation fixed point.
223 IntegerValue SizeMin(int t) const { return cached_duration_min_[t]; }
224 IntegerValue SizeMax(int t) const {
225 // This one is "rare" so we don't cache it.
226 return integer_trail_->UpperBound(sizes_[t]);
227 }
228 IntegerValue StartMin(int t) const { return cached_start_min_[t]; }
229 IntegerValue EndMin(int t) const { return cached_end_min_[t]; }
230 IntegerValue StartMax(int t) const { return -cached_negated_start_max_[t]; }
231 IntegerValue EndMax(int t) const { return -cached_negated_end_max_[t]; }
232
233 // In the presence of tasks with a variable size, we do not necessarily
234 // have start_min + size_min = end_min, we can instead have a situation
235 // like:
236 // | |<--- size-min --->|
237 // ^ ^ ^
238 // start-min | end-min
239 // |
240 // We define the "shifted start min" to be the right most time such that
241 // we known that we must have min-size "energy" to the right of it if the
242 // task is present. Using it in our scheduling propagators allows to propagate
243 // more in the presence of tasks with variable size (or optional task
244 // where we also do not necessarily have start_min + size_min = end_min.
245 //
246 // To explain this shifted start min, one must use the AddEnergyAfterReason().
247 IntegerValue ShiftedStartMin(int t) const {
248 return cached_shifted_start_min_[t];
249 }
250
251 bool StartIsFixed(int t) const;
252 bool EndIsFixed(int t) const;
253 bool SizeIsFixed(int t) const;
254
255 // Returns true if the corresponding fact is known for sure. A normal task is
256 // always present. For optional task for which the presence is still unknown,
257 // both of these function will return false.
258 bool IsOptional(int t) const;
259 bool IsPresent(int t) const;
260 bool IsAbsent(int t) const;
261
262 // Returns a string with the current task bounds.
263 std::string TaskDebugString(int t) const;
264
265 // Sorts and returns the tasks in corresponding order at the time of the call.
266 // Note that we do not mean strictly-increasing/strictly-decreasing, there
267 // will be duplicate time values in these vectors.
268 //
269 // TODO(user): we could merge the first loop of IncrementalSort() with the
270 // loop that fill TaskTime.time at each call.
271 const std::vector<TaskTime>& TaskByIncreasingStartMin();
272 const std::vector<TaskTime>& TaskByIncreasingEndMin();
273 const std::vector<TaskTime>& TaskByDecreasingStartMax();
274 const std::vector<TaskTime>& TaskByDecreasingEndMax();
275 const std::vector<TaskTime>& TaskByIncreasingShiftedStartMin();
276
277 // Functions to clear and then set the current reason.
278 void ClearReason();
279 void AddPresenceReason(int t);
280 void AddAbsenceReason(int t);
281 void AddSizeMinReason(int t);
282 void AddSizeMinReason(int t, IntegerValue lower_bound);
283 void AddStartMinReason(int t, IntegerValue lower_bound);
284 void AddStartMaxReason(int t, IntegerValue upper_bound);
285 void AddEndMinReason(int t, IntegerValue lower_bound);
286 void AddEndMaxReason(int t, IntegerValue upper_bound);
287 void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time);
288
289 // Adds the reason why task "before" must be before task "after".
290 // That is StartMax(before) < EndMin(after).
291 void AddReasonForBeingBefore(int before, int after);
292
293 // It is also possible to directly manipulates the underlying reason vectors
294 // that will be used when pushing something.
295 std::vector<Literal>* MutableLiteralReason() { return &literal_reason_; }
296 std::vector<IntegerLiteral>* MutableIntegerReason() {
297 return &integer_reason_;
298 }
299
300 // Push something using the current reason. Note that IncreaseStartMin() will
301 // also increase the end-min, and DecreaseEndMax() will also decrease the
302 // start-max.
303 //
304 // Important: IncreaseStartMin() and DecreaseEndMax() can be called on an
305 // optional interval whose presence is still unknown and push a bound
306 // conditionned on its presence. The functions will do the correct thing
307 // depending on whether or not the start_min/end_max are optional variables
308 // whose presence implies the interval presence.
309 ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_start_min);
310 ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_start_max);
311 ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t);
312 ABSL_MUST_USE_RESULT bool PushTaskPresence(int t);
313 ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit);
314 ABSL_MUST_USE_RESULT bool ReportConflict();
315 ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t,
316 IntegerLiteral lit);
317
318 // Returns the underlying affine expressions.
319 const std::vector<AffineExpression>& Starts() const { return starts_; }
320 const std::vector<AffineExpression>& Ends() const { return ends_; }
321 const std::vector<AffineExpression>& Sizes() const { return sizes_; }
324 return Literal(reason_for_presence_[index]);
325 }
326
327 // Registers the given propagator id to be called if any of the tasks
328 // in this class change. Note that we do not watch size max though.
329 void WatchAllTasks(int id, GenericLiteralWatcher* watcher,
330 bool watch_start_max = true,
331 bool watch_end_max = true) const;
332
333 // Manages the other helper (used by the diffn constraint).
334 //
335 // For each interval appearing in a reason on this helper, another reason
336 // will be added. This other reason specifies that on the other helper, the
337 // corresponding interval overlaps 'event'.
339 IntegerValue event) {
340 CHECK(other_helper != nullptr);
341 other_helper_ = other_helper;
342 event_for_other_helper_ = event;
343 }
344
345 void ClearOtherHelper() { other_helper_ = nullptr; }
346
347 // Adds to this helper reason all the explanation of the other helper.
348 // This checks that other_helper_ is null.
349 //
350 // This is used in the 2D energetic reasoning in the diffn constraint.
351 void ImportOtherReasons(const SchedulingConstraintHelper& other_helper);
352
353 // TODO(user): Change the propagation loop code so that we don't stop
354 // pushing in the middle of the propagation as more advanced propagator do
355 // not handle this correctly.
356 bool InPropagationLoop() const { return integer_trail_->InPropagationLoop(); }
357
358 private:
359 void InitSortedVectors();
360 void UpdateCachedValues(int t);
361
362 // Internal function for IncreaseStartMin()/DecreaseEndMax().
363 bool PushIntervalBound(int t, IntegerLiteral lit);
364
365 // This will be called on any interval that is part of a reason or
366 // a bound push. Since the last call to ClearReason(), for each unique
367 // t, we will add once to other_helper_ the reason for t containing
368 // the point event_for_other_helper_.
369 void AddOtherReason(int t);
370
371 // Import the reasons on the other helper into this helper.
372 void ImportOtherReasons();
373
374 Trail* trail_;
375 IntegerTrail* integer_trail_;
376 PrecedencesPropagator* precedences_;
377
378 // The current direction of time, true for forward, false for backward.
379 bool current_time_direction_ = true;
380
381 // All the underlying variables of the tasks.
382 // The vectors are indexed by the task index t.
383 std::vector<AffineExpression> starts_;
384 std::vector<AffineExpression> ends_;
385 std::vector<AffineExpression> sizes_;
386 std::vector<LiteralIndex> reason_for_presence_;
387
388 // The negation of the start/end variable so that SetTimeDirection()
389 // can do its job in O(1) instead of calling NegationOf() on each entry.
390 std::vector<AffineExpression> minus_starts_;
391 std::vector<AffineExpression> minus_ends_;
392
393 // This is used by SetLevel() to dected untrail.
394 int previous_level_ = 0;
395
396 // The caches of all relevant interval values.
397 std::vector<IntegerValue> cached_duration_min_;
398 std::vector<IntegerValue> cached_start_min_;
399 std::vector<IntegerValue> cached_end_min_;
400 std::vector<IntegerValue> cached_negated_start_max_;
401 std::vector<IntegerValue> cached_negated_end_max_;
402 std::vector<IntegerValue> cached_shifted_start_min_;
403 std::vector<IntegerValue> cached_negated_shifted_end_max_;
404
405 // Sorted vectors returned by the TasksBy*() functions.
406 std::vector<TaskTime> task_by_increasing_start_min_;
407 std::vector<TaskTime> task_by_increasing_end_min_;
408 std::vector<TaskTime> task_by_decreasing_start_max_;
409 std::vector<TaskTime> task_by_decreasing_end_max_;
410
411 // This one is the most commonly used, so we optimized a bit more its
412 // computation by detecting when there is nothing to do.
413 std::vector<TaskTime> task_by_increasing_shifted_start_min_;
414 std::vector<TaskTime> task_by_negated_shifted_end_max_;
415 bool recompute_shifted_start_min_ = true;
416 bool recompute_negated_shifted_end_max_ = true;
417
418 // If recompute_cache_[t] is true, then we need to update all the cached
419 // value for the task t in SynchronizeAndSetTimeDirection().
420 bool recompute_all_cache_ = true;
421 std::vector<bool> recompute_cache_;
422
423 // Reason vectors.
424 std::vector<Literal> literal_reason_;
425 std::vector<IntegerLiteral> integer_reason_;
426
427 // Optional 'proxy' helper used in the diffn constraint.
428 SchedulingConstraintHelper* other_helper_ = nullptr;
429 IntegerValue event_for_other_helper_;
430 std::vector<bool> already_added_to_other_reasons_;
431};
432
433// =============================================================================
434// SchedulingConstraintHelper inlined functions.
435// =============================================================================
436
438 return integer_trail_->IsFixed(starts_[t]);
439}
440
442 return integer_trail_->IsFixed(ends_[t]);
443}
444
446 return integer_trail_->IsFixed(sizes_[t]);
447}
448
450 return reason_for_presence_[t] != kNoLiteralIndex;
451}
452
454 if (reason_for_presence_[t] == kNoLiteralIndex) return true;
455 return trail_->Assignment().LiteralIsTrue(Literal(reason_for_presence_[t]));
456}
457
458inline bool SchedulingConstraintHelper::IsAbsent(int t) const {
459 if (reason_for_presence_[t] == kNoLiteralIndex) return false;
460 return trail_->Assignment().LiteralIsFalse(Literal(reason_for_presence_[t]));
461}
462
464 integer_reason_.clear();
465 literal_reason_.clear();
466 if (other_helper_) {
467 other_helper_->ClearReason();
468 already_added_to_other_reasons_.assign(NumTasks(), false);
469 }
470}
471
473 DCHECK(IsPresent(t));
474 AddOtherReason(t);
475 if (reason_for_presence_[t] != kNoLiteralIndex) {
476 literal_reason_.push_back(Literal(reason_for_presence_[t]).Negated());
477 }
478}
479
481 DCHECK(IsAbsent(t));
482 AddOtherReason(t);
483 if (reason_for_presence_[t] != kNoLiteralIndex) {
484 literal_reason_.push_back(Literal(reason_for_presence_[t]));
485 }
486}
487
489 AddOtherReason(t);
490 if (sizes_[t].var != kNoIntegerVariable) {
491 integer_reason_.push_back(
492 integer_trail_->LowerBoundAsLiteral(sizes_[t].var));
493 }
494}
495
497 int t, IntegerValue lower_bound) {
498 AddOtherReason(t);
499 if (sizes_[t].var != kNoIntegerVariable) {
500 integer_reason_.push_back(sizes_[t].GreaterOrEqual(lower_bound));
501 }
502}
503
505 int t, IntegerValue lower_bound) {
506 DCHECK_GE(StartMin(t), lower_bound);
507 AddOtherReason(t);
508 if (starts_[t].var != kNoIntegerVariable) {
509 integer_reason_.push_back(starts_[t].GreaterOrEqual(lower_bound));
510 }
511}
512
514 int t, IntegerValue upper_bound) {
515 AddOtherReason(t);
516
517 // Note that we cannot use the cache here!
518 if (integer_trail_->UpperBound(starts_[t]) <= upper_bound) {
519 if (starts_[t].var != kNoIntegerVariable) {
520 integer_reason_.push_back(starts_[t].LowerOrEqual(upper_bound));
521 }
522 } else {
523 // This might happen if we used StartMax() <= EndMax() - SizeMin().
524 if (sizes_[t].var != kNoIntegerVariable) {
525 integer_reason_.push_back(
526 integer_trail_->LowerBoundAsLiteral(sizes_[t].var));
527 }
528 if (ends_[t].var != kNoIntegerVariable) {
529 integer_reason_.push_back(
530 ends_[t].LowerOrEqual(upper_bound + SizeMin(t)));
531 }
532 }
533}
534
536 int t, IntegerValue lower_bound) {
537 AddOtherReason(t);
538
539 // Note that we cannot use the cache here!
540 if (integer_trail_->LowerBound(ends_[t]) >= lower_bound) {
541 if (ends_[t].var != kNoIntegerVariable) {
542 integer_reason_.push_back(ends_[t].GreaterOrEqual(lower_bound));
543 }
544 } else {
545 // This might happen if we used EndMin() >= StartMin() + SizeMin().
546 if (sizes_[t].var != kNoIntegerVariable) {
547 integer_reason_.push_back(
548 integer_trail_->LowerBoundAsLiteral(sizes_[t].var));
549 }
550 if (starts_[t].var != kNoIntegerVariable) {
551 integer_reason_.push_back(
552 starts_[t].GreaterOrEqual(lower_bound - SizeMin(t)));
553 }
554 }
555}
556
558 int t, IntegerValue upper_bound) {
559 DCHECK_LE(EndMax(t), upper_bound);
560 AddOtherReason(t);
561 if (ends_[t].var != kNoIntegerVariable) {
562 integer_reason_.push_back(ends_[t].LowerOrEqual(upper_bound));
563 }
564}
565
567 int t, IntegerValue energy_min, IntegerValue time) {
568 AddOtherReason(t);
569 if (StartMin(t) >= time) {
570 if (starts_[t].var != kNoIntegerVariable) {
571 integer_reason_.push_back(starts_[t].GreaterOrEqual(time));
572 }
573 } else {
574 if (ends_[t].var != kNoIntegerVariable) {
575 integer_reason_.push_back(ends_[t].GreaterOrEqual(time + energy_min));
576 }
577 }
578 if (sizes_[t].var != kNoIntegerVariable) {
579 integer_reason_.push_back(sizes_[t].GreaterOrEqual(energy_min));
580 }
581}
582
583// =============================================================================
584// Model based functions.
585// =============================================================================
586
587inline std::function<IntegerVariable(const Model&)> StartVar(
588 IntervalVariable v) {
589 return [=](const Model& model) {
590 return model.Get<IntervalsRepository>()->StartVar(v);
591 };
592}
593
594inline std::function<IntegerVariable(const Model&)> EndVar(IntervalVariable v) {
595 return [=](const Model& model) {
596 return model.Get<IntervalsRepository>()->EndVar(v);
597 };
598}
599
600inline std::function<IntegerVariable(const Model&)> SizeVar(
601 IntervalVariable v) {
602 return [=](const Model& model) {
603 return model.Get<IntervalsRepository>()->SizeVar(v);
604 };
605}
606
607inline std::function<int64(const Model&)> MinSize(IntervalVariable v) {
608 return [=](const Model& model) {
609 return model.Get<IntervalsRepository>()->MinSize(v).value();
610 };
611}
612
613inline std::function<int64(const Model&)> MaxSize(IntervalVariable v) {
614 return [=](const Model& model) {
615 return model.Get<IntervalsRepository>()->MaxSize(v).value();
616 };
617}
618
619inline std::function<bool(const Model&)> IsOptional(IntervalVariable v) {
620 return [=](const Model& model) {
621 return model.Get<IntervalsRepository>()->IsOptional(v);
622 };
623}
624
625inline std::function<Literal(const Model&)> IsPresentLiteral(
626 IntervalVariable v) {
627 return [=](const Model& model) {
628 return model.Get<IntervalsRepository>()->PresenceLiteral(v);
629 };
630}
631
632inline std::function<IntervalVariable(Model*)> NewInterval(int64 min_start,
633 int64 max_end,
634 int64 size) {
635 return [=](Model* model) {
636 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
637 model->Add(NewIntegerVariable(min_start, max_end)),
638 model->Add(NewIntegerVariable(min_start, max_end)), kNoIntegerVariable,
639 IntegerValue(size), kNoLiteralIndex);
640 };
641}
642
643inline std::function<IntervalVariable(Model*)> NewInterval(
644 IntegerVariable start, IntegerVariable end, IntegerVariable size) {
645 return [=](Model* model) {
646 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
647 start, end, size, IntegerValue(0), kNoLiteralIndex);
648 };
649}
650
651inline std::function<IntervalVariable(Model*)> NewIntervalWithVariableSize(
652 int64 min_start, int64 max_end, int64 min_size, int64 max_size) {
653 return [=](Model* model) {
654 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
655 model->Add(NewIntegerVariable(min_start, max_end)),
656 model->Add(NewIntegerVariable(min_start, max_end)),
657 model->Add(NewIntegerVariable(min_size, max_size)), IntegerValue(0),
659 };
660}
661
662inline std::function<IntervalVariable(Model*)> NewOptionalInterval(
663 int64 min_start, int64 max_end, int64 size, Literal is_present) {
664 return [=](Model* model) {
665 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
666 model->Add(NewIntegerVariable(min_start, max_end)),
667 model->Add(NewIntegerVariable(min_start, max_end)), kNoIntegerVariable,
668 IntegerValue(size), is_present.Index());
669 };
670}
671
672inline std::function<IntervalVariable(Model*)>
674 int64 size, Literal is_present) {
675 return [=](Model* model) {
676 // Note that we need to mark the optionality first.
677 const IntegerVariable start =
678 model->Add(NewIntegerVariable(min_start, max_end));
679 const IntegerVariable end =
680 model->Add(NewIntegerVariable(min_start, max_end));
681 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
682 integer_trail->MarkIntegerVariableAsOptional(start, is_present);
683 integer_trail->MarkIntegerVariableAsOptional(end, is_present);
684 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
685 start, end, kNoIntegerVariable, IntegerValue(size), is_present.Index());
686 };
687}
688
689inline std::function<IntervalVariable(Model*)> NewOptionalInterval(
690 IntegerVariable start, IntegerVariable end, IntegerVariable size,
691 Literal is_present) {
692 return [=](Model* model) {
693 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
694 start, end, size, IntegerValue(0), is_present.Index());
695 };
696}
697
698inline std::function<IntervalVariable(Model*)>
700 int64 min_size, int64 max_size,
701 Literal is_present) {
702 return [=](Model* model) {
703 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
704 model->Add(NewIntegerVariable(min_start, max_end)),
705 model->Add(NewIntegerVariable(min_start, max_end)),
706 model->Add(NewIntegerVariable(min_size, max_size)), IntegerValue(0),
707 is_present.Index());
708 };
709}
710
711// This requires that all the alternatives are optional tasks.
712inline std::function<void(Model*)> IntervalWithAlternatives(
713 IntervalVariable parent, const std::vector<IntervalVariable>& members) {
714 return [=](Model* model) {
715 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
716 auto* intervals = model->GetOrCreate<IntervalsRepository>();
717
718 std::vector<Literal> presences;
719 std::vector<IntegerValue> sizes;
720
721 // Create an "exactly one executed" constraint on the alternatives.
722 std::vector<LiteralWithCoeff> sat_ct;
723 for (const IntervalVariable member : members) {
724 CHECK(intervals->IsOptional(member));
725 const Literal is_present = intervals->PresenceLiteral(member);
726 sat_ct.push_back({is_present, Coefficient(1)});
727 model->Add(
728 Equality(model->Get(StartVar(parent)), model->Get(StartVar(member))));
729 model->Add(
730 Equality(model->Get(EndVar(parent)), model->Get(EndVar(member))));
731
732 // TODO(user): IsOneOf() only work for members with fixed size.
733 // Generalize to an "int_var_element" constraint.
734 CHECK(integer_trail->IsFixed(intervals->Size(member)));
735 presences.push_back(is_present);
736 sizes.push_back(intervals->MinSize(member));
737 }
738 if (intervals->SizeVar(parent) != kNoIntegerVariable) {
739 model->Add(IsOneOf(intervals->SizeVar(parent), presences, sizes));
740 }
741 model->Add(BooleanLinearConstraint(1, 1, &sat_ct));
742
743 // Propagate from the candidate bounds to the parent interval ones.
744 {
745 std::vector<IntegerVariable> starts;
746 starts.reserve(members.size());
747 for (const IntervalVariable member : members) {
748 starts.push_back(intervals->StartVar(member));
749 }
750 model->Add(
751 PartialIsOneOfVar(intervals->StartVar(parent), starts, presences));
752 }
753 {
754 std::vector<IntegerVariable> ends;
755 ends.reserve(members.size());
756 for (const IntervalVariable member : members) {
757 ends.push_back(intervals->EndVar(member));
758 }
759 model->Add(PartialIsOneOfVar(intervals->EndVar(parent), ends, presences));
760 }
761 };
762}
763
764} // namespace sat
765} // namespace operations_research
766
767#endif // OR_TOOLS_SAT_INTERVALS_H_
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK(condition)
Definition: base/logging.h:884
An Assignment is a variable -> domains mapping, used to report solutions to the user.
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1330
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered)
Definition: integer.h:639
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
bool IsOptional(IntegerVariable i) const
Definition: integer.h:622
IntegerVariable SizeVar(IntervalVariable i) const
Definition: intervals.h:97
AffineExpression End(IntervalVariable i) const
Definition: intervals.h:94
IntegerValue MaxSize(IntervalVariable i) const
Definition: intervals.h:125
AffineExpression Start(IntervalVariable i) const
Definition: intervals.h:93
Literal PresenceLiteral(IntervalVariable i) const
Definition: intervals.h:73
std::vector< IntervalVariable > AllIntervals() const
Definition: intervals.h:130
IntegerVariable StartVar(IntervalVariable i) const
Definition: intervals.h:104
IntegerValue MinSize(IntervalVariable i) const
Definition: intervals.h:120
IntegerVariable EndVar(IntervalVariable i) const
Definition: intervals.h:111
bool IsPresent(IntervalVariable i) const
Definition: intervals.h:76
AffineExpression Size(IntervalVariable i) const
Definition: intervals.h:92
bool IsAbsent(IntervalVariable i) const
Definition: intervals.h:80
bool IsOptional(IntervalVariable i) const
Definition: intervals.h:70
IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end, IntegerVariable size, IntegerValue fixed_size, LiteralIndex is_present)
Definition: intervals.cc:24
LiteralIndex Index() const
Definition: sat_base.h:84
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
Definition: intervals.cc:378
const std::vector< AffineExpression > & Starts() const
Definition: intervals.h:319
const std::vector< TaskTime > & TaskByDecreasingEndMax()
Definition: intervals.cc:302
std::vector< IntegerLiteral > * MutableIntegerReason()
Definition: intervals.h:296
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t)
Definition: intervals.cc:423
SchedulingConstraintHelper(const std::vector< IntervalVariable > &tasks, Model *model)
Definition: intervals.cc:65
const std::vector< TaskTime > & TaskByIncreasingStartMin()
Definition: intervals.cc:265
void AddStartMinReason(int t, IntegerValue lower_bound)
Definition: intervals.h:504
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
Definition: intervals.cc:460
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: intervals.cc:110
const std::vector< TaskTime > & TaskByIncreasingEndMin()
Definition: intervals.cc:277
void ResetFromSubset(const SchedulingConstraintHelper &other, absl::Span< const int > tasks)
Definition: intervals.cc:176
void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time)
Definition: intervals.h:566
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t, IntegerLiteral lit)
Definition: intervals.cc:383
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: intervals.cc:129
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
const std::vector< AffineExpression > & Sizes() const
Definition: intervals.h:321
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
ABSL_MUST_USE_RESULT bool PushTaskPresence(int t)
Definition: intervals.cc:439
void AddEndMaxReason(int t, IntegerValue upper_bound)
Definition: intervals.h:557
void SetOtherHelper(SchedulingConstraintHelper *other_helper, IntegerValue event)
Definition: intervals.h:338
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
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
int64_t int64
std::function< IntegerVariable(const Model &)> SizeVar(IntervalVariable v)
Definition: intervals.h:600
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
Definition: intervals.h:662
std::function< IntegerVariable(const Model &)> EndVar(IntervalVariable v)
Definition: intervals.h:594
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
Definition: sat_solver.h:852
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
std::function< IntegerVariable(const Model &)> StartVar(IntervalVariable v)
Definition: intervals.h:587
std::function< void(Model *)> PartialIsOneOfVar(IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
DEFINE_INT_TYPE(ClauseIndex, int)
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithOptionalVariables(int64 min_start, int64 max_end, int64 size, Literal is_present)
Definition: intervals.h:673
const IntegerVariable kNoIntegerVariable(-1)
const IntervalVariable kNoIntervalVariable(-1)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
Definition: integer.h:1495
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1426
std::function< IntervalVariable(Model *)> NewIntervalWithVariableSize(int64 min_start, int64 max_end, int64 min_size, int64 max_size)
Definition: intervals.h:651
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
Definition: intervals.h:632
std::function< bool(const Model &)> IsOptional(IntervalVariable v)
Definition: intervals.h:619
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithVariableSize(int64 min_start, int64 max_end, int64 min_size, int64 max_size, Literal is_present)
Definition: intervals.h:699
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1509
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
Definition: integer.h:1524
std::function< int64(const Model &)> MinSize(IntervalVariable v)
Definition: intervals.h:607
std::function< int64(const Model &)> MaxSize(IntervalVariable v)
Definition: intervals.h:613
std::function< Literal(const Model &)> IsPresentLiteral(IntervalVariable v)
Definition: intervals.h:625
std::function< void(Model *)> IntervalWithAlternatives(IntervalVariable parent, const std::vector< IntervalVariable > &members)
Definition: intervals.h:712
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
bool operator<(TaskTime other) const
Definition: intervals.h:162
bool operator>(TaskTime other) const
Definition: intervals.h:163