Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
scheduling_helpers.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <algorithm>
17#include <cstdint>
18#include <functional>
19#include <string>
20#include <utility>
21#include <vector>
22
23#include "absl/log/check.h"
24#include "absl/strings/str_cat.h"
25#include "absl/types/span.h"
28#include "ortools/sat/integer.h"
32#include "ortools/sat/model.h"
36#include "ortools/util/sort.h"
38
39namespace operations_research {
40namespace sat {
41
43 std::vector<AffineExpression> starts, std::vector<AffineExpression> ends,
44 std::vector<AffineExpression> sizes,
45 std::vector<LiteralIndex> reason_for_presence, Model* model)
46 : model_(model),
47 sat_solver_(model->GetOrCreate<SatSolver>()),
48 assignment_(sat_solver_->Assignment()),
49 integer_trail_(model->GetOrCreate<IntegerTrail>()),
50 watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
51 precedence_relations_(model->GetOrCreate<PrecedenceRelations>()),
52 starts_(std::move(starts)),
53 ends_(std::move(ends)),
54 sizes_(std::move(sizes)),
55 reason_for_presence_(std::move(reason_for_presence)),
56 capacity_(starts_.size()),
57 cached_size_min_(new IntegerValue[capacity_]),
58 cached_start_min_(new IntegerValue[capacity_]),
59 cached_end_min_(new IntegerValue[capacity_]),
60 cached_negated_start_max_(new IntegerValue[capacity_]),
61 cached_negated_end_max_(new IntegerValue[capacity_]),
62 cached_shifted_start_min_(new IntegerValue[capacity_]),
63 cached_negated_shifted_end_max_(new IntegerValue[capacity_]) {
64 DCHECK_EQ(starts_.size(), ends_.size());
65 DCHECK_EQ(starts_.size(), sizes_.size());
66 DCHECK_EQ(starts_.size(), reason_for_presence_.size());
67
68 minus_starts_.clear();
69 minus_starts_.reserve(starts_.size());
70 minus_ends_.clear();
71 minus_ends_.reserve(starts_.size());
72 for (int i = 0; i < starts_.size(); ++i) {
73 minus_starts_.push_back(starts_[i].Negated());
74 minus_ends_.push_back(ends_[i].Negated());
75 }
76
77 InitSortedVectors();
79 model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
80 }
81}
82
84 Model* model)
85 : model_(model),
86 sat_solver_(model->GetOrCreate<SatSolver>()),
87 assignment_(sat_solver_->Assignment()),
88 integer_trail_(model->GetOrCreate<IntegerTrail>()),
89 precedence_relations_(model->GetOrCreate<PrecedenceRelations>()),
90 capacity_(num_tasks),
91 cached_size_min_(new IntegerValue[capacity_]),
92 cached_start_min_(new IntegerValue[capacity_]),
93 cached_end_min_(new IntegerValue[capacity_]),
94 cached_negated_start_max_(new IntegerValue[capacity_]),
95 cached_negated_end_max_(new IntegerValue[capacity_]),
96 cached_shifted_start_min_(new IntegerValue[capacity_]),
97 cached_negated_shifted_end_max_(new IntegerValue[capacity_]) {
98 starts_.resize(num_tasks);
99 CHECK_EQ(NumTasks(), num_tasks);
100}
101
103 recompute_all_cache_ = true;
104 for (const int id : propagator_ids_) watcher_->CallOnNextPropagate(id);
105 return true;
106}
107
109 const std::vector<int>& watch_indices) {
110 for (const int t : watch_indices) recompute_cache_.Set(t);
111 for (const int id : propagator_ids_) watcher_->CallOnNextPropagate(id);
112 return true;
113}
114
116 const int id = watcher->Register(this);
117 const int num_tasks = starts_.size();
118 for (int t = 0; t < num_tasks; ++t) {
119 watcher->WatchIntegerVariable(sizes_[t].var, id, t);
120 watcher->WatchIntegerVariable(starts_[t].var, id, t);
121 watcher->WatchIntegerVariable(ends_[t].var, id, t);
122
123 // This class do not need to be waked up on presence change, since this is
124 // not cached. However given that we can have many propagators that use the
125 // same helper, it is nicer to only register this one, and wake up all
126 // propagator through it rather than registering all of them individually.
127 // Note that IncrementalPropagate() will do nothing if this is the only
128 // change except waking up registered propagators.
129 if (!IsPresent(t) && !IsAbsent(t)) {
130 watcher_->WatchLiteral(Literal(reason_for_presence_[t]), id);
131 }
132 }
133 watcher->SetPropagatorPriority(id, 0);
134}
135
136bool SchedulingConstraintHelper::UpdateCachedValues(int t) {
137 if (IsAbsent(t)) return true;
138
139 IntegerValue smin = integer_trail_->LowerBound(starts_[t]);
140 IntegerValue smax = integer_trail_->UpperBound(starts_[t]);
141 IntegerValue emin = integer_trail_->LowerBound(ends_[t]);
142 IntegerValue emax = integer_trail_->UpperBound(ends_[t]);
143
144 // We take the max for the corner case where the size of an optional interval
145 // is used elsewhere and has a domain with negative value.
146 //
147 // TODO(user): maybe we should just disallow size with a negative domain, but
148 // is is harder to enforce if we have a linear expression for size.
149 IntegerValue dmin =
150 std::max(IntegerValue(0), integer_trail_->LowerBound(sizes_[t]));
151 IntegerValue dmax = integer_trail_->UpperBound(sizes_[t]);
152
153 // Detect first if we have a conflict using the relation start + size = end.
154 if (dmax < 0) {
155 ClearReason();
156 AddSizeMaxReason(t, dmax);
157 return PushTaskAbsence(t);
158 }
159 if (smin + dmin - emax > 0) {
160 ClearReason();
161 AddStartMinReason(t, smin);
162 AddSizeMinReason(t, dmin);
163 AddEndMaxReason(t, emax);
164 return PushTaskAbsence(t);
165 }
166 if (smax + dmax - emin < 0) {
167 ClearReason();
168 AddStartMaxReason(t, smax);
169 AddSizeMaxReason(t, dmax);
170 AddEndMinReason(t, emin);
171 return PushTaskAbsence(t);
172 }
173
174 // Sometimes, for optional interval with non-optional bounds, this propagation
175 // give tighter bounds. We always consider the value assuming
176 // the interval is present.
177 //
178 // Note that this is also useful in case not everything was propagated. Note
179 // also that since there is no conflict, we reach the fix point in one pass.
180 smin = std::max(smin, emin - dmax);
181 smax = std::min(smax, emax - dmin);
182 dmin = std::max(dmin, emin - smax);
183 emin = std::max(emin, smin + dmin);
184 emax = std::min(emax, smax + dmax);
185
186 if (emin != cached_end_min_[t]) {
187 recompute_energy_profile_ = true;
188 }
189
190 // We might only want to do that if the value changed, but I am not sure it
191 // is worth the test.
192 recompute_by_start_max_ = true;
193 recompute_by_end_min_ = true;
194
195 cached_start_min_[t] = smin;
196 cached_end_min_[t] = emin;
197 cached_negated_start_max_[t] = -smax;
198 cached_negated_end_max_[t] = -emax;
199 cached_size_min_[t] = dmin;
200
201 // Note that we use the cached value here for EndMin()/StartMax().
202 const IntegerValue new_shifted_start_min = emin - dmin;
203 if (new_shifted_start_min != cached_shifted_start_min_[t]) {
204 recompute_energy_profile_ = true;
205 recompute_shifted_start_min_ = true;
206 cached_shifted_start_min_[t] = new_shifted_start_min;
207 }
208 const IntegerValue new_negated_shifted_end_max = -(smax + dmin);
209 if (new_negated_shifted_end_max != cached_negated_shifted_end_max_[t]) {
210 recompute_negated_shifted_end_max_ = true;
211 cached_negated_shifted_end_max_[t] = new_negated_shifted_end_max;
212 }
213 return true;
214}
215
217 const SchedulingConstraintHelper& other, absl::Span<const int> tasks) {
218 current_time_direction_ = other.current_time_direction_;
219
220 const int num_tasks = tasks.size();
221 CHECK_LE(num_tasks, capacity_);
222 starts_.resize(num_tasks);
223 ends_.resize(num_tasks);
224 minus_ends_.resize(num_tasks);
225 minus_starts_.resize(num_tasks);
226 sizes_.resize(num_tasks);
227 reason_for_presence_.resize(num_tasks);
228 for (int i = 0; i < num_tasks; ++i) {
229 const int t = tasks[i];
230 starts_[i] = other.starts_[t];
231 ends_[i] = other.ends_[t];
232 minus_ends_[i] = other.minus_ends_[t];
233 minus_starts_[i] = other.minus_starts_[t];
234 sizes_[i] = other.sizes_[t];
235 reason_for_presence_[i] = other.reason_for_presence_[t];
236 }
237
238 InitSortedVectors();
240}
241
242void SchedulingConstraintHelper::InitSortedVectors() {
243 const int num_tasks = starts_.size();
244
245 recompute_all_cache_ = true;
246 recompute_cache_.Resize(num_tasks);
247 non_fixed_intervals_.resize(num_tasks);
248 for (int t = 0; t < num_tasks; ++t) {
249 non_fixed_intervals_[t] = t;
250 recompute_cache_.Set(t);
251 }
252
253 // Make sure all the cached_* arrays can hold enough data.
254 CHECK_LE(num_tasks, capacity_);
255
256 task_by_increasing_start_min_.resize(num_tasks);
257 task_by_increasing_end_min_.resize(num_tasks);
258 task_by_increasing_negated_start_max_.resize(num_tasks);
259 task_by_decreasing_end_max_.resize(num_tasks);
260 task_by_increasing_shifted_start_min_.resize(num_tasks);
261 task_by_negated_shifted_end_max_.resize(num_tasks);
262 for (int t = 0; t < num_tasks; ++t) {
263 task_by_increasing_start_min_[t].task_index = t;
264 task_by_increasing_end_min_[t].task_index = t;
265 task_by_increasing_negated_start_max_[t].task_index = t;
266 task_by_decreasing_end_max_[t].task_index = t;
267
268 task_by_increasing_shifted_start_min_[t].task_index = t;
269 task_by_increasing_shifted_start_min_[t].presence_lit =
270 reason_for_presence_[t];
271 task_by_negated_shifted_end_max_[t].task_index = t;
272 task_by_negated_shifted_end_max_[t].presence_lit = reason_for_presence_[t];
273 }
274
275 recompute_by_start_max_ = true;
276 recompute_by_end_min_ = true;
277 recompute_energy_profile_ = true;
278 recompute_shifted_start_min_ = true;
279 recompute_negated_shifted_end_max_ = true;
280}
281
283 if (current_time_direction_ != is_forward) {
284 current_time_direction_ = is_forward;
285
286 std::swap(starts_, minus_ends_);
287 std::swap(ends_, minus_starts_);
288
289 std::swap(task_by_increasing_start_min_, task_by_decreasing_end_max_);
290 std::swap(task_by_increasing_end_min_,
291 task_by_increasing_negated_start_max_);
292 std::swap(recompute_by_end_min_, recompute_by_start_max_);
293 std::swap(task_by_increasing_shifted_start_min_,
294 task_by_negated_shifted_end_max_);
295
296 recompute_energy_profile_ = true;
297 std::swap(cached_start_min_, cached_negated_end_max_);
298 std::swap(cached_end_min_, cached_negated_start_max_);
299 std::swap(cached_shifted_start_min_, cached_negated_shifted_end_max_);
300 std::swap(recompute_shifted_start_min_, recompute_negated_shifted_end_max_);
301 }
302}
303
305 bool is_forward) {
306 SetTimeDirection(is_forward);
307
308 // If there was any backtracks since the last time this was called, we
309 // recompute our cache.
310 if (sat_solver_->num_backtracks() != saved_num_backtracks_) {
311 recompute_all_cache_ = true;
312 saved_num_backtracks_ = sat_solver_->num_backtracks();
313 }
314
315 if (recompute_all_cache_) {
316 for (const int t : non_fixed_intervals_) {
317 if (!UpdateCachedValues(t)) return false;
318 }
319
320 // We also update non_fixed_intervals_ at level zero so that we will never
321 // scan them again.
322 if (sat_solver_->CurrentDecisionLevel() == 0) {
323 int new_size = 0;
324 for (const int t : non_fixed_intervals_) {
325 if (IsPresent(t) && StartIsFixed(t) && EndIsFixed(t) &&
326 SizeIsFixed(t)) {
327 continue;
328 }
329 non_fixed_intervals_[new_size++] = t;
330 }
331 non_fixed_intervals_.resize(new_size);
332 }
333 } else {
334 for (const int t : recompute_cache_) {
335 if (!UpdateCachedValues(t)) return false;
336 }
337 }
338 recompute_cache_.ClearAll();
339 recompute_all_cache_ = false;
340 return true;
341}
342
343// TODO(user): be more precise when we know a and b are in disjunction.
344// we really just need start_b > start_a, or even >= if duration is non-zero.
346 int a, int b, bool add_reason_if_after) {
347 const AffineExpression before = ends_[a];
348 const AffineExpression after = starts_[b];
349 LinearExpression2 expr(before.var, after.var, before.coeff, -after.coeff);
350
351 // We take the min of the level zero (end_a - start_b) and the one coming from
352 // a conditional precedence at true.
353 const IntegerValue conditional_ub = precedence_relations_->UpperBound(expr);
354 const IntegerValue level_zero_ub = integer_trail_->LevelZeroUpperBound(expr);
355 const IntegerValue expr_ub = std::min(conditional_ub, level_zero_ub);
356
357 const IntegerValue needed_offset = before.constant - after.constant;
358 const IntegerValue ub_of_end_minus_start = expr_ub + needed_offset;
359 const IntegerValue distance = -ub_of_end_minus_start;
360 if (add_reason_if_after && distance >= 0 && level_zero_ub > conditional_ub) {
361 precedence_relations_->AddReasonForUpperBoundLowerThan(
362 expr, conditional_ub, MutableLiteralReason(), MutableIntegerReason());
363 }
364 return distance;
365}
366
367// Note that we could call this at a positive level to propagate any literal
368// associated to task a before task b. However we only call this for task that
369// are in detectable precedence, which means the normal precedence or linear
370// propagator should have already propagated that Boolean too.
372 CHECK(IsPresent(a));
373 CHECK(IsPresent(b));
374 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
375
376 const AffineExpression before = ends_[a];
377 const AffineExpression after = starts_[b];
378 if (after.coeff != 1) return true;
379 if (before.coeff != 1) return true;
380 if (after.var == kNoIntegerVariable) return true;
381 if (before.var == kNoIntegerVariable) return true;
382 if (before.var == after.var) {
383 if (before.constant <= after.constant) {
384 return true;
385 } else {
386 sat_solver_->NotifyThatModelIsUnsat();
387 return false;
388 }
389 }
390 const IntegerValue offset = before.constant - after.constant;
391 const LinearExpression2 expr =
393 if (precedence_relations_->AddUpperBound(expr, -offset)) {
394 VLOG(2) << "new relation " << TaskDebugString(a)
395 << " <= " << TaskDebugString(b);
396 if (before.var == NegationOf(after.var)) {
397 AddWeightedSumLowerOrEqual({}, {before.var}, {int64_t{2}},
398 -offset.value(), model_);
399 } else {
400 // TODO(user): Adding new constraint during propagation might not be the
401 // best idea as it can create some complication.
402 AddWeightedSumLowerOrEqual({}, {before.var, after.var},
403 {int64_t{1}, int64_t{-1}}, -offset.value(),
404 model_);
405 }
406 if (sat_solver_->ModelIsUnsat()) return false;
407 }
408 return true;
409}
410
411absl::Span<const TaskTime>
413 for (TaskTime& ref : task_by_increasing_start_min_) {
414 ref.time = StartMin(ref.task_index);
415 }
416 IncrementalSort(task_by_increasing_start_min_.begin(),
417 task_by_increasing_start_min_.end());
418 return task_by_increasing_start_min_;
419}
420
421absl::Span<const TaskTime>
423 if (!recompute_by_end_min_) return task_by_increasing_end_min_;
424 for (TaskTime& ref : task_by_increasing_end_min_) {
425 ref.time = EndMin(ref.task_index);
426 }
427 IncrementalSort(task_by_increasing_end_min_.begin(),
428 task_by_increasing_end_min_.end());
429 recompute_by_end_min_ = false;
430 return task_by_increasing_end_min_;
431}
432
433absl::Span<const TaskTime>
435 if (!recompute_by_start_max_) return task_by_increasing_negated_start_max_;
436 for (TaskTime& ref : task_by_increasing_negated_start_max_) {
437 ref.time = cached_negated_start_max_[ref.task_index];
438 }
439 IncrementalSort(task_by_increasing_negated_start_max_.begin(),
440 task_by_increasing_negated_start_max_.end());
441 recompute_by_start_max_ = false;
442 return task_by_increasing_negated_start_max_;
443}
444
445absl::Span<const TaskTime>
447 for (TaskTime& ref : task_by_decreasing_end_max_) {
448 ref.time = EndMax(ref.task_index);
449 }
450 IncrementalSort(task_by_decreasing_end_max_.begin(),
451 task_by_decreasing_end_max_.end(), std::greater<TaskTime>());
452 return task_by_decreasing_end_max_;
453}
454
455absl::Span<const CachedTaskBounds>
457 if (recompute_shifted_start_min_) {
458 recompute_shifted_start_min_ = false;
459 bool is_sorted = true;
460 IntegerValue previous = kMinIntegerValue;
461 for (CachedTaskBounds& ref : task_by_increasing_shifted_start_min_) {
462 ref.time = ShiftedStartMin(ref.task_index);
463 is_sorted = is_sorted && ref.time >= previous;
464 previous = ref.time;
465 }
466 if (is_sorted) return task_by_increasing_shifted_start_min_;
467 IncrementalSort(task_by_increasing_shifted_start_min_.begin(),
468 task_by_increasing_shifted_start_min_.end());
469 }
470 return task_by_increasing_shifted_start_min_;
471}
472
473// TODO(user): Avoid recomputing it if nothing changed.
474const std::vector<SchedulingConstraintHelper::ProfileEvent>&
476 if (energy_profile_.empty()) {
477 const int num_tasks = NumTasks();
478 for (int t = 0; t < num_tasks; ++t) {
479 energy_profile_.push_back(
480 {cached_shifted_start_min_[t], t, /*is_first=*/true});
481 energy_profile_.push_back({cached_end_min_[t], t, /*is_first=*/false});
482 }
483 } else {
484 if (!recompute_energy_profile_) return energy_profile_;
485 for (ProfileEvent& ref : energy_profile_) {
486 const int t = ref.task;
487 if (ref.is_first) {
488 ref.time = cached_shifted_start_min_[t];
489 } else {
490 ref.time = cached_end_min_[t];
491 }
492 }
493 }
494 IncrementalSort(energy_profile_.begin(), energy_profile_.end());
495 recompute_energy_profile_ = false;
496 return energy_profile_;
497}
498
499// Produces a relaxed reason for StartMax(before) < EndMin(after).
501 int after) {
502 AddOtherReason(before);
503 AddOtherReason(after);
504
505 // The reason will be a linear expression greater than a value. Note that all
506 // coeff must be positive, and we will use the variable lower bound.
507 std::vector<IntegerVariable> vars;
508 std::vector<IntegerValue> coeffs;
509
510 // Reason for StartMax(before).
511 const IntegerValue smax_before = StartMax(before);
512 if (smax_before >= integer_trail_->UpperBound(starts_[before])) {
513 if (starts_[before].var != kNoIntegerVariable) {
514 vars.push_back(NegationOf(starts_[before].var));
515 coeffs.push_back(starts_[before].coeff);
516 }
517 } else {
518 if (ends_[before].var != kNoIntegerVariable) {
519 vars.push_back(NegationOf(ends_[before].var));
520 coeffs.push_back(ends_[before].coeff);
521 }
522 if (sizes_[before].var != kNoIntegerVariable) {
523 vars.push_back(sizes_[before].var);
524 coeffs.push_back(sizes_[before].coeff);
525 }
526 }
527
528 // Reason for EndMin(after);
529 const IntegerValue emin_after = EndMin(after);
530 if (emin_after <= integer_trail_->LowerBound(ends_[after])) {
531 if (ends_[after].var != kNoIntegerVariable) {
532 vars.push_back(ends_[after].var);
533 coeffs.push_back(ends_[after].coeff);
534 }
535 } else {
536 if (starts_[after].var != kNoIntegerVariable) {
537 vars.push_back(starts_[after].var);
538 coeffs.push_back(starts_[after].coeff);
539 }
540 if (sizes_[after].var != kNoIntegerVariable) {
541 vars.push_back(sizes_[after].var);
542 coeffs.push_back(sizes_[after].coeff);
543 }
544 }
545
546 DCHECK_LT(smax_before, emin_after);
547 const IntegerValue slack = emin_after - smax_before - 1;
548 integer_trail_->AppendRelaxedLinearReason(slack, coeffs, vars,
549 &integer_reason_);
550}
551
553 CHECK(other_helper_ == nullptr);
554 return integer_trail_->Enqueue(lit, literal_reason_, integer_reason_);
555}
556
558 int t, IntegerLiteral lit) {
559 if (IsAbsent(t)) return true;
560 AddOtherReason(t);
562 if (IsOptional(t)) {
563 return integer_trail_->ConditionalEnqueue(
564 PresenceLiteral(t), lit, &literal_reason_, &integer_reason_);
565 }
566 return integer_trail_->Enqueue(lit, literal_reason_, integer_reason_);
567}
568
569// We also run directly the precedence propagator for this variable so that when
570// we push an interval start for example, we have a chance to push its end.
571bool SchedulingConstraintHelper::PushIntervalBound(int t, IntegerLiteral lit) {
572 if (!PushIntegerLiteralIfTaskPresent(t, lit)) return false;
573 if (IsAbsent(t)) return true;
574 if (!UpdateCachedValues(t)) return false;
575 recompute_cache_.Clear(t);
576 return true;
577}
578
579bool SchedulingConstraintHelper::IncreaseStartMin(int t, IntegerValue value) {
580 if (starts_[t].var == kNoIntegerVariable) {
581 if (value > starts_[t].constant) return PushTaskAbsence(t);
582 return true;
583 }
584 return PushIntervalBound(t, starts_[t].GreaterOrEqual(value));
585}
586
587bool SchedulingConstraintHelper::IncreaseEndMin(int t, IntegerValue value) {
588 if (ends_[t].var == kNoIntegerVariable) {
589 if (value > ends_[t].constant) return PushTaskAbsence(t);
590 return true;
591 }
592 return PushIntervalBound(t, ends_[t].GreaterOrEqual(value));
593}
594
595bool SchedulingConstraintHelper::DecreaseEndMax(int t, IntegerValue value) {
596 if (ends_[t].var == kNoIntegerVariable) {
597 if (value < ends_[t].constant) return PushTaskAbsence(t);
598 return true;
599 }
600 return PushIntervalBound(t, ends_[t].LowerOrEqual(value));
601}
602
604 integer_trail_->EnqueueLiteral(l, literal_reason_, integer_reason_);
605 return true;
606}
607
609 if (IsAbsent(t)) return true;
610 if (!IsOptional(t)) return ReportConflict();
611
612 AddOtherReason(t);
613
614 if (IsPresent(t)) {
615 literal_reason_.push_back(Literal(reason_for_presence_[t]).Negated());
616 return ReportConflict();
617 }
619 integer_trail_->EnqueueLiteral(Literal(reason_for_presence_[t]).Negated(),
620 literal_reason_, integer_reason_);
621 return true;
622}
623
625 DCHECK_NE(reason_for_presence_[t], kNoLiteralIndex);
626 DCHECK(!IsPresent(t));
627
628 AddOtherReason(t);
629
630 if (IsAbsent(t)) {
631 literal_reason_.push_back(Literal(reason_for_presence_[t]));
632 return ReportConflict();
633 }
635 integer_trail_->EnqueueLiteral(Literal(reason_for_presence_[t]),
636 literal_reason_, integer_reason_);
637 return true;
638}
639
642 return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
643}
644
646 // It is more efficient to enqueue the propagator
647 // when the helper Propagate() is called. This result in less entries in our
648 // watched lists.
649 propagator_ids_.push_back(id);
650}
651
652void SchedulingConstraintHelper::AddOtherReason(int t) {
653 if (other_helper_ == nullptr || already_added_to_other_reasons_[t]) return;
654 already_added_to_other_reasons_[t] = true;
655 const int mapped_t = map_to_other_helper_[t];
656 other_helper_->AddStartMaxReason(mapped_t, event_for_other_helper_);
657 other_helper_->AddEndMinReason(mapped_t, event_for_other_helper_ + 1);
658}
659
661 if (other_helper_ != nullptr) ImportOtherReasons(*other_helper_);
662}
663
665 const SchedulingConstraintHelper& other_helper) {
666 literal_reason_.insert(literal_reason_.end(),
667 other_helper.literal_reason_.begin(),
668 other_helper.literal_reason_.end());
669 integer_reason_.insert(integer_reason_.end(),
670 other_helper.integer_reason_.begin(),
671 other_helper.integer_reason_.end());
672}
673
675 return absl::StrCat("t=", t, " is_present=",
676 (IsPresent(t) ? "1"
677 : IsAbsent(t) ? "0"
678 : "?"),
679 " size=[", SizeMin(t).value(), ",", SizeMax(t).value(),
680 "]", " start=[", StartMin(t).value(), ",",
681 StartMax(t).value(), "]", " end=[", EndMin(t).value(),
682 ",", EndMax(t).value(), "]");
683}
684
686 IntegerValue start,
687 IntegerValue end) const {
688 return std::min(std::min(end - start, SizeMin(t)),
689 std::min(EndMin(t) - start, end - StartMax(t)));
690}
691
693 IntegerValue start_min, IntegerValue start_max, IntegerValue end_min,
694 IntegerValue end_max, IntegerValue size_min, IntegerValue demand_min,
695 absl::Span<const LiteralValueValue> filtered_energy,
696 IntegerValue window_start, IntegerValue window_end) {
697 if (window_end <= window_start) return IntegerValue(0);
698
699 // Returns zero if the interval do not necessarily overlap.
700 if (end_min <= window_start) return IntegerValue(0);
701 if (start_max >= window_end) return IntegerValue(0);
702 const IntegerValue window_size = window_end - window_start;
703 const IntegerValue simple_energy_min =
704 demand_min * std::min({end_min - window_start, window_end - start_max,
705 size_min, window_size});
706 if (filtered_energy.empty()) return simple_energy_min;
707
708 IntegerValue result = kMaxIntegerValue;
709 for (const auto [lit, fixed_size, fixed_demand] : filtered_energy) {
710 const IntegerValue alt_end_min = std::max(end_min, start_min + fixed_size);
711 const IntegerValue alt_start_max =
712 std::min(start_max, end_max - fixed_size);
713 const IntegerValue energy_min =
714 fixed_demand *
715 std::min({alt_end_min - window_start, window_end - alt_start_max,
716 fixed_size, window_size});
717 result = std::min(result, energy_min);
718 }
719 if (result == kMaxIntegerValue) return simple_energy_min;
720 return std::max(simple_energy_min, result);
721}
722
724 absl::Span<const AffineExpression> demands,
725 SchedulingConstraintHelper* helper, Model* model)
726 : integer_trail_(model->GetOrCreate<IntegerTrail>()),
727 product_decomposer_(model->GetOrCreate<ProductDecomposer>()),
728 sat_solver_(model->GetOrCreate<SatSolver>()),
729 assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
730 demands_(demands.begin(), demands.end()),
731 helper_(helper) {
732 const int num_tasks = helper->NumTasks();
733 decomposed_energies_.resize(num_tasks);
734 cached_energies_min_.resize(num_tasks, kMinIntegerValue);
735 cached_energies_max_.resize(num_tasks, kMaxIntegerValue);
736 energy_is_quadratic_.resize(num_tasks, false);
737
738 // We try to init decomposed energies. This is needed for the cuts that are
739 // created after we call InitAllDecomposedEnergies().
741}
742
744 // For the special case were demands is empty.
745 const int num_tasks = helper_->NumTasks();
746 if (demands_.size() != num_tasks) return;
747 for (int t = 0; t < num_tasks; ++t) {
748 const AffineExpression size = helper_->Sizes()[t];
749 const AffineExpression demand = demands_[t];
750 decomposed_energies_[t] = product_decomposer_->TryToDecompose(size, demand);
751 }
752}
753
754IntegerValue SchedulingDemandHelper::SimpleEnergyMin(int t) const {
755 if (demands_.empty()) return kMinIntegerValue;
756 return CapProdI(DemandMin(t), helper_->SizeMin(t));
757}
758
759IntegerValue SchedulingDemandHelper::DecomposedEnergyMin(int t) const {
760 if (decomposed_energies_[t].empty()) return kMinIntegerValue;
761 IntegerValue result = kMaxIntegerValue;
762 for (const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
763 if (assignment_.LiteralIsTrue(lit)) {
764 return fixed_size * fixed_demand;
765 }
766 if (assignment_.LiteralIsFalse(lit)) continue;
767 result = std::min(result, fixed_size * fixed_demand);
768 }
769 DCHECK_NE(result, kMaxIntegerValue);
770 return result;
771}
772
773IntegerValue SchedulingDemandHelper::SimpleEnergyMax(int t) const {
774 if (demands_.empty()) return kMaxIntegerValue;
775 return CapProdI(DemandMax(t), helper_->SizeMax(t));
776}
777
778IntegerValue SchedulingDemandHelper::DecomposedEnergyMax(int t) const {
779 if (decomposed_energies_[t].empty()) return kMaxIntegerValue;
780 IntegerValue result = kMinIntegerValue;
781 for (const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
782 if (assignment_.LiteralIsTrue(lit)) {
783 return fixed_size * fixed_demand;
784 }
785 if (assignment_.LiteralIsFalse(lit)) continue;
786 result = std::max(result, fixed_size * fixed_demand);
787 }
788 DCHECK_NE(result, kMinIntegerValue);
789 return result;
790}
791
793 const int num_tasks = cached_energies_min_.size();
794 const bool is_at_level_zero = sat_solver_->CurrentDecisionLevel() == 0;
795 for (int t = 0; t < num_tasks; ++t) {
796 // Try to reduce the size of the decomposed energy vector.
797 if (is_at_level_zero) {
798 int new_size = 0;
799 for (int i = 0; i < decomposed_energies_[t].size(); ++i) {
800 if (assignment_.LiteralIsFalse(decomposed_energies_[t][i].literal)) {
801 continue;
802 }
803 decomposed_energies_[t][new_size++] = decomposed_energies_[t][i];
804 }
805 decomposed_energies_[t].resize(new_size);
806 }
807
808 cached_energies_min_[t] =
809 std::max(SimpleEnergyMin(t), DecomposedEnergyMin(t));
810 if (cached_energies_min_[t] <= kMinIntegerValue) return false;
811 energy_is_quadratic_[t] =
812 decomposed_energies_[t].empty() && !demands_.empty() &&
813 !integer_trail_->IsFixed(demands_[t]) && !helper_->SizeIsFixed(t);
814 cached_energies_max_[t] =
815 std::min(SimpleEnergyMax(t), DecomposedEnergyMax(t));
816 if (cached_energies_max_[t] >= kMaxIntegerValue) return false;
817 }
818
819 return true;
820}
821
822IntegerValue SchedulingDemandHelper::DemandMin(int t) const {
823 DCHECK_LT(t, demands_.size());
824 return integer_trail_->LowerBound(demands_[t]);
825}
826
827IntegerValue SchedulingDemandHelper::DemandMax(int t) const {
828 DCHECK_LT(t, demands_.size());
829 return integer_trail_->UpperBound(demands_[t]);
830}
831
833 return integer_trail_->IsFixed(demands_[t]);
834}
835
836bool SchedulingDemandHelper::DecreaseEnergyMax(int t, IntegerValue value) {
837 if (helper_->IsAbsent(t)) return true;
838 if (value < EnergyMin(t)) return helper_->PushTaskAbsence(t);
839
840 if (!decomposed_energies_[t].empty()) {
841 for (const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
842 if (fixed_size * fixed_demand > value) {
843 // `lit` encodes that the energy is higher than value. So either lit
844 // must be false or the task must be absent.
845 if (assignment_.LiteralIsFalse(lit)) continue;
846 if (assignment_.LiteralIsTrue(lit)) {
847 // Task must be absent.
848 if (helper_->PresenceLiteral(t) != lit) {
849 helper_->MutableLiteralReason()->push_back(lit.Negated());
850 }
851 return helper_->PushTaskAbsence(t);
852 }
853 if (helper_->IsPresent(t)) {
854 // Task is present, `lit` must be false.
855 DCHECK(!helper_->IsOptional(t) || helper_->PresenceLiteral(t) != lit);
856 helper_->AddPresenceReason(t);
857 if (!helper_->PushLiteral(lit.Negated())) return false;
858 }
859 }
860 }
861 } else {
862 // TODO(user): Propagate if possible.
863 VLOG(3) << "Cumulative energy missed propagation";
864 }
865 return true;
866}
867
869 DCHECK_LT(t, demands_.size());
870 if (demands_[t].var != kNoIntegerVariable) {
871 helper_->MutableIntegerReason()->push_back(
872 integer_trail_->LowerBoundAsLiteral(demands_[t].var));
873 }
874}
875
877 IntegerValue min_demand) {
878 DCHECK_LT(t, demands_.size());
879 if (demands_[t].var != kNoIntegerVariable) {
880 helper_->MutableIntegerReason()->push_back(
881 demands_[t].GreaterOrEqual(min_demand));
882 }
883}
884
886 // We prefer these reason in order.
887 const IntegerValue value = cached_energies_min_[t];
888 if (DecomposedEnergyMin(t) >= value) {
889 auto* reason = helper_->MutableLiteralReason();
890 const int old_size = reason->size();
891 for (const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
892 if (assignment_.LiteralIsTrue(lit)) {
893 reason->resize(old_size);
894 reason->push_back(lit.Negated());
895 return;
896 } else if (fixed_size * fixed_demand < value &&
897 assignment_.LiteralIsFalse(lit)) {
898 reason->push_back(lit);
899 }
900 }
901 } else if (SimpleEnergyMin(t) >= value) {
903 helper_->AddSizeMinReason(t);
904 }
905}
906
908 int t, LinearConstraintBuilder* builder) const {
909 if (helper_->IsPresent(t)) {
910 if (!decomposed_energies_[t].empty()) {
911 for (const LiteralValueValue& entry : decomposed_energies_[t]) {
912 if (!builder->AddLiteralTerm(entry.literal, entry.right_value)) {
913 return false;
914 }
915 }
916 } else {
917 builder->AddTerm(demands_[t], IntegerValue(1));
918 }
919 } else if (!helper_->IsAbsent(t)) {
920 return builder->AddLiteralTerm(helper_->PresenceLiteral(t), DemandMin(t));
921 }
922 return true;
923}
924
926 int index) {
927 if (decomposed_energies_[index].empty()) return {};
928 if (sat_solver_->CurrentDecisionLevel() == 0) {
929 // CacheAllEnergyValues has already filtered false literals.
930 return decomposed_energies_[index];
931 }
932
933 // Scan and filter false literals.
934 std::vector<LiteralValueValue> result;
935 for (const auto& e : decomposed_energies_[index]) {
936 if (assignment_.LiteralIsFalse(e.literal)) continue;
937 result.push_back(e);
938 }
939 return result;
940}
941
943 const std::vector<std::vector<LiteralValueValue>>& energies) {
944 DCHECK_EQ(energies.size(), helper_->NumTasks());
945 decomposed_energies_ = energies;
946}
947
949 int t, IntegerValue window_start, IntegerValue window_end) {
951 helper_->StartMin(t), helper_->StartMax(t), helper_->EndMin(t),
952 helper_->EndMax(t), helper_->SizeMin(t), DemandMin(t),
953 FilteredDecomposedEnergy(t), window_start, window_end);
954}
955
956// Since we usually ask way less often for the reason, we redo the computation
957// here.
959 int t, IntegerValue window_start, IntegerValue window_end) {
960 const IntegerValue actual_energy_min =
961 EnergyMinInWindow(t, window_start, window_end);
962 if (actual_energy_min == 0) return;
963
964 // Return simple reason right away if there is no decomposition or the simple
965 // energy is enough.
966 const IntegerValue start_max = helper_->StartMax(t);
967 const IntegerValue end_min = helper_->EndMin(t);
968 const IntegerValue min_overlap =
969 helper_->GetMinOverlap(t, window_start, window_end);
970 const IntegerValue simple_energy_min = DemandMin(t) * min_overlap;
971 if (simple_energy_min == actual_energy_min) {
973 helper_->AddSizeMinReason(t);
974 helper_->AddStartMaxReason(t, start_max);
975 helper_->AddEndMinReason(t, end_min);
976 return;
977 }
978
979 // TODO(user): only include the one we need?
980 const IntegerValue start_min = helper_->StartMin(t);
981 const IntegerValue end_max = helper_->EndMax(t);
982 DCHECK(!decomposed_energies_[t].empty());
983 helper_->AddStartMinReason(t, start_min);
984 helper_->AddStartMaxReason(t, start_max);
985 helper_->AddEndMinReason(t, end_min);
986 helper_->AddEndMaxReason(t, end_max);
987
988 auto* literal_reason = helper_->MutableLiteralReason();
989 const int old_size = literal_reason->size();
990
991 DCHECK(!decomposed_energies_[t].empty());
992 for (const auto [lit, fixed_size, fixed_demand] : decomposed_energies_[t]) {
993 // Should be the same in most cases.
994 if (assignment_.LiteralIsTrue(lit)) {
995 literal_reason->resize(old_size);
996 literal_reason->push_back(lit.Negated());
997 return;
998 }
999 if (assignment_.LiteralIsFalse(lit)) {
1000 const IntegerValue alt_em = std::max(end_min, start_min + fixed_size);
1001 const IntegerValue alt_sm = std::min(start_max, end_max - fixed_size);
1002 const IntegerValue energy_min =
1003 fixed_demand *
1004 std::min({alt_em - window_start, window_end - alt_sm, fixed_size});
1005 if (energy_min >= actual_energy_min) continue;
1006 literal_reason->push_back(lit);
1007 }
1008 }
1009}
1010
1012 Model* model,
1013 std::vector<IntegerVariable>* vars,
1014 int mask) {
1015 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1016 for (int t = 0; t < helper->NumTasks(); ++t) {
1017 if ((mask & IntegerVariablesToAddMask::kStart) &&
1018 helper->Starts()[t].var != kNoIntegerVariable) {
1019 vars->push_back(helper->Starts()[t].var);
1020 }
1021 if ((mask & IntegerVariablesToAddMask::kSize) &&
1022 helper->Sizes()[t].var != kNoIntegerVariable) {
1023 vars->push_back(helper->Sizes()[t].var);
1024 }
1025 if ((mask & IntegerVariablesToAddMask::kEnd) &&
1026 helper->Ends()[t].var != kNoIntegerVariable) {
1027 vars->push_back(helper->Ends()[t].var);
1028 }
1030 helper->IsOptional(t) && !helper->IsAbsent(t) &&
1031 !helper->IsPresent(t)) {
1032 const Literal l = helper->PresenceLiteral(t);
1033 IntegerVariable view = kNoIntegerVariable;
1034 if (!encoder->LiteralOrNegationHasView(l, &view)) {
1035 view = model->Add(NewIntegerVariableFromLiteral(l));
1036 }
1037 vars->push_back(view);
1038 }
1039 }
1040}
1041
1043 const AffineExpression& capacity, SchedulingDemandHelper* demands_helper,
1044 Model* model, std::vector<IntegerVariable>* vars) {
1045 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1046 for (const AffineExpression& demand_expr : demands_helper->Demands()) {
1047 if (!integer_trail->IsFixed(demand_expr)) {
1048 vars->push_back(demand_expr.var);
1049 }
1050 }
1051 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1052 for (const auto& product : demands_helper->DecomposedEnergies()) {
1053 for (const auto& lit_val_val : product) {
1054 IntegerVariable view = kNoIntegerVariable;
1055 if (!encoder->LiteralOrNegationHasView(lit_val_val.literal, &view)) {
1056 view = model->Add(NewIntegerVariableFromLiteral(lit_val_val.literal));
1057 }
1058 vars->push_back(view);
1059 }
1060 }
1061
1062 if (!integer_trail->IsFixed(capacity)) {
1063 vars->push_back(capacity.var);
1064 }
1065}
1066
1067} // namespace sat
1068} // namespace operations_research
void Clear(IndexType i)
Sets the bit at position i to 0.
Definition bitset.h:505
void Resize(IndexType size)
Definition bitset.h:474
void Set(IndexType i)
Sets the bit at position i to 1.
Definition bitset.h:543
void SetPropagatorPriority(int id, int priority)
Definition integer.cc:2352
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
Definition integer.h:1502
int Register(PropagatorInterface *propagator)
Registers a propagator and returns its unique ids.
Definition integer.cc:2326
ABSL_MUST_USE_RESULT bool LiteralOrNegationHasView(Literal lit, IntegerVariable *view=nullptr, bool *view_is_direct=nullptr) const
Definition integer.cc:575
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
Definition integer.h:1317
IntegerValue UpperBound(IntegerVariable i) const
Definition integer.h:1321
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff=IntegerValue(1))
void AddTerm(IntegerVariable var, IntegerValue coeff)
T Add(std::function< T(Model *)> f)
Definition model.h:87
Helper class to express a product as a linear constraint.
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
void AddReasonForBeingBefore(int before, int after)
Produces a relaxed reason for StartMax(before) < EndMin(after).
void AddStartMaxReason(int t, IntegerValue upper_bound)
ABSL_MUST_USE_RESULT bool IncreaseEndMin(int t, IntegerValue value)
void AddSizeMaxReason(int t, IntegerValue upper_bound)
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue value)
int NumTasks() const
Returns the number of task.
absl::Span< const AffineExpression > Sizes() const
const std::vector< ProfileEvent > & GetEnergyProfile()
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t, IntegerLiteral lit)
absl::Span< const AffineExpression > Starts() const
void AddEndMaxReason(int t, IntegerValue upper_bound)
absl::Span< const AffineExpression > Ends() const
ABSL_MUST_USE_RESULT bool ResetFromSubset(const SchedulingConstraintHelper &other, absl::Span< const int > tasks)
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue value)
void AddEndMinReason(int t, IntegerValue lower_bound)
void ClearReason()
Functions to clear and then set the current reason.
SchedulingConstraintHelper(std::vector< AffineExpression > starts, std::vector< AffineExpression > ends, std::vector< AffineExpression > sizes, std::vector< LiteralIndex > reason_for_presence, Model *model)
absl::Span< const CachedTaskBounds > TaskByIncreasingShiftedStartMin()
ABSL_MUST_USE_RESULT bool SynchronizeAndSetTimeDirection(bool is_forward)
std::string TaskDebugString(int t) const
Returns a string with the current task bounds.
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
void ImportOtherReasons(const SchedulingConstraintHelper &other_helper)
IntegerValue GetCurrentMinDistanceBetweenTasks(int a, int b, bool add_reason_if_after=false)
IntegerValue GetMinOverlap(int t, IntegerValue start, IntegerValue end) const
void AddStartMinReason(int t, IntegerValue lower_bound)
std::vector< LiteralValueValue > FilteredDecomposedEnergy(int index)
IntegerValue EnergyMinInWindow(int t, IntegerValue window_start, IntegerValue window_end)
const std::vector< std::vector< LiteralValueValue > > & DecomposedEnergies() const
void AddEnergyMinInWindowReason(int t, IntegerValue window_start, IntegerValue window_end)
SchedulingDemandHelper(absl::Span< const AffineExpression > demands, SchedulingConstraintHelper *helper, Model *model)
void OverrideDecomposedEnergies(const std::vector< std::vector< LiteralValueValue > > &energies)
Visible for testing.
const std::vector< AffineExpression > & Demands() const
ABSL_MUST_USE_RESULT bool DecreaseEnergyMax(int t, IntegerValue value)
ABSL_MUST_USE_RESULT bool AddLinearizedDemand(int t, LinearConstraintBuilder *builder) const
bool LiteralIsFalse(Literal literal) const
Definition sat_base.h:185
bool LiteralIsTrue(Literal literal) const
Definition sat_base.h:188
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
Definition integer.h:1574
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
const LiteralIndex kNoLiteralIndex(-1)
std::function< int64_t(const Model &)> LowerBound(IntegerVariable v)
Definition integer.h:1581
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64_t ub)
Definition integer.h:1624
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
void AddIntegerVariableFromIntervals(const SchedulingConstraintHelper *helper, Model *model, std::vector< IntegerVariable > *vars, int mask)
void AppendVariablesFromCapacityAndDemands(const AffineExpression &capacity, SchedulingDemandHelper *demands_helper, Model *model, std::vector< IntegerVariable > *vars)
void AddWeightedSumLowerOrEqual(absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const int64_t > coefficients, int64_t upper_bound, Model *model)
enforcement_literals => sum <= upper_bound
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64_t lb)
Definition integer.h:1609
IntegerValue CapProdI(IntegerValue a, IntegerValue b)
Overflows and saturated arithmetic.
IntegerValue ComputeEnergyMinInWindow(IntegerValue start_min, IntegerValue start_max, IntegerValue end_min, IntegerValue end_max, IntegerValue size_min, IntegerValue demand_min, absl::Span< const LiteralValueValue > filtered_energy, IntegerValue window_start, IntegerValue window_end)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
void IncrementalSort(int max_comparisons, Iterator begin, Iterator end, Compare comp=Compare{}, bool is_stable=false)
Definition sort.h:46
ClosedInterval::Iterator begin(ClosedInterval interval)
STL namespace.
IntegerLiteral Negated() const
The negation of x >= bound is x <= bound - 1.
static LinearExpression2 Difference(IntegerVariable v1, IntegerVariable v2)
Build (v1 - v2)