28 std::vector<IntegerValue> deltas,
29 std::vector<Literal> presences,
int64 min_level,
32 IntegerValue min_possible(0);
33 IntegerValue max_possible(0);
34 for (
const IntegerValue d : deltas) {
41 if (max_possible > max_level) {
43 times, deltas, presences, IntegerValue(max_level),
model));
45 if (min_possible < min_level) {
46 for (IntegerValue& ref : deltas) ref = -ref;
48 times, deltas, presences, IntegerValue(-min_level),
model));
53 const std::vector<AffineExpression>& times,
54 const std::vector<IntegerValue>& deltas,
58 presences_(presences),
63 const int id = watcher->
Register(
this);
64 const int num_events = times.size();
65 for (
int e = 0; e < num_events; e++) {
67 watcher->WatchUpperBound(times_[e].
var,
id);
68 watcher->WatchLiteral(presences_[e],
id);
71 watcher->WatchLowerBound(times_[e].
var,
id);
72 watcher->WatchLiteral(presences_[e].Negated(), id);
75 watcher->NotifyThatPropagatorMayNotReachFixedPointInOnePass(
id);
79 const int num_events = times_.size();
80 if (!BuildProfile())
return false;
81 for (
int e = 0; e < num_events; e++) {
85 if (deltas_[e] > 0 && !TryToIncreaseMin(e))
return false;
88 if (deltas_[e] < 0 && !TryToDecreaseMax(e))
return false;
97bool ReservoirTimeTabling::BuildProfile() {
100 const int num_events = times_.size();
102 for (
int e = 0; e < num_events; e++) {
103 if (deltas_[e] > 0) {
106 const IntegerValue ub = integer_trail_->
UpperBound(times_[e]);
107 profile_.push_back({ub, deltas_[e]});
108 }
else if (deltas_[e] < 0) {
111 profile_.push_back({integer_trail_->
LowerBound(times_[e]), deltas_[e]});
115 std::sort(profile_.begin(), profile_.end());
119 for (
const ProfileRectangle& rect : profile_) {
120 if (rect.start == profile_[last].start) {
121 profile_[last].height += rect.height;
124 profile_[last].start = rect.start;
125 profile_[last].height = rect.height + profile_[last - 1].height;
128 profile_.resize(last + 1);
131 for (
const ProfileRectangle& rect : profile_) {
132 if (rect.height <= capacity_)
continue;
133 FillReasonForProfileAtGivenTime(rect.start);
134 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
146void ReservoirTimeTabling::FillReasonForProfileAtGivenTime(
147 IntegerValue t,
int event_to_ignore) {
148 integer_reason_.clear();
149 literal_reason_.clear();
150 const int num_events = times_.size();
151 for (
int e = 0; e < num_events; e++) {
152 if (e == event_to_ignore)
continue;
153 if (deltas_[e] > 0) {
155 if (integer_trail_->
UpperBound(times_[e]) > t)
continue;
157 literal_reason_.push_back(presences_[e].Negated());
158 }
else if (deltas_[e] < 0) {
160 literal_reason_.push_back(presences_[e]);
161 }
else if (integer_trail_->
LowerBound(times_[e]) > t) {
170bool ReservoirTimeTabling::TryToDecreaseMax(
int event) {
172 const IntegerValue start = integer_trail_->
LowerBound(times_[event]);
173 const IntegerValue end = integer_trail_->
UpperBound(times_[event]);
176 if (start == end)
return true;
180 DCHECK(std::is_sorted(profile_.begin(), profile_.end()));
182 std::upper_bound(profile_.begin(), profile_.end(), start,
183 [&](IntegerValue
value,
const ProfileRectangle& rect) {
184 return value < rect.start;
190 IntegerValue new_end = end;
191 for (; profile_[rec_id].start < end; ++rec_id) {
192 if (profile_[rec_id].height - deltas_[event] > capacity_) {
193 new_end = profile_[rec_id].start;
198 if (!push)
return true;
202 FillReasonForProfileAtGivenTime(new_end, event);
207 if (new_end < start) {
208 integer_reason_.push_back(times_[event].
GreaterOrEqual(new_end + 1));
209 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
217 integer_trail_->
EnqueueLiteral(presences_[event], literal_reason_,
223 literal_reason_, integer_reason_);
226bool ReservoirTimeTabling::TryToIncreaseMin(
int event) {
228 const IntegerValue start = integer_trail_->
LowerBound(times_[event]);
229 const IntegerValue end = integer_trail_->
UpperBound(times_[event]);
232 if (start == end)
return true;
239 DCHECK(std::is_sorted(profile_.begin(), profile_.end()));
241 std::upper_bound(profile_.begin(), profile_.end(), end,
242 [&](IntegerValue
value,
const ProfileRectangle& rect) {
243 return value < rect.start;
249 IntegerValue new_start = start;
250 if (profile_[rec_id].height + deltas_[event] > capacity_) {
255 }
else if (profile_[rec_id].start < end) {
262 for (; profile_[rec_id].start > start; --rec_id) {
263 if (profile_[rec_id - 1].height + deltas_[event] > capacity_) {
265 new_start = profile_[rec_id].start;
270 if (!push)
return true;
273 FillReasonForProfileAtGivenTime(new_start - 1, event);
276 &literal_reason_, &integer_reason_);
282 : num_tasks_(helper->NumTasks()),
285 integer_trail_(integer_trail),
290 profile_.reserve(2 * num_tasks_ + 4);
293 forward_num_tasks_to_sweep_ = num_tasks_;
294 forward_tasks_to_sweep_.resize(num_tasks_);
295 backward_num_tasks_to_sweep_ = num_tasks_;
296 backward_tasks_to_sweep_.resize(num_tasks_);
298 num_profile_tasks_ = 0;
299 profile_tasks_.resize(num_tasks_);
300 positions_in_profile_tasks_.resize(num_tasks_);
303 starting_profile_height_ = IntegerValue(0);
305 for (
int t = 0; t < num_tasks_; ++t) {
306 forward_tasks_to_sweep_[t] = t;
307 backward_tasks_to_sweep_[t] = t;
308 profile_tasks_[t] = t;
309 positions_in_profile_tasks_[t] = t;
314 const int id = watcher->
Register(
this);
317 for (
int t = 0; t < num_tasks_; t++) {
332 if (!BuildProfile())
return false;
335 if (!SweepAllTasks(
true))
return false;
341 if (!SweepAllTasks(
false))
return false;
346bool TimeTablingPerTask::BuildProfile() {
352 for (
int i = num_profile_tasks_; i < num_tasks_; ++i) {
353 const int t1 = profile_tasks_[i];
356 const int t2 = profile_tasks_[num_profile_tasks_];
357 profile_tasks_[i] = t2;
358 profile_tasks_[num_profile_tasks_] = t1;
359 positions_in_profile_tasks_[t1] = num_profile_tasks_;
360 positions_in_profile_tasks_[t2] = i;
361 num_profile_tasks_++;
381 IntegerValue current_height = starting_profile_height_;
385 int next_start = num_tasks_ - 1;
387 while (next_end < num_tasks_) {
388 const IntegerValue old_height = current_height;
390 IntegerValue t = by_end_min[next_end].time;
391 if (next_start >= 0) {
392 t =
std::min(t, by_decreasing_start_max[next_start].
time);
396 while (next_start >= 0 && by_decreasing_start_max[next_start].
time == t) {
397 const int task_index = by_decreasing_start_max[next_start].task_index;
398 if (IsInProfile(task_index)) current_height += DemandMin(task_index);
403 while (next_end < num_tasks_ && by_end_min[next_end].
time == t) {
404 const int task_index = by_end_min[next_end].task_index;
405 if (IsInProfile(task_index)) current_height -= DemandMin(task_index);
410 if (current_height != old_height) {
411 profile_.emplace_back(current_start, old_height);
412 if (current_height > profile_max_height_) {
413 profile_max_height_ = current_height;
414 max_height_start = t;
422 profile_.emplace_back(current_start, IntegerValue(0));
428 return IncreaseCapacity(max_height_start, profile_max_height_);
431void TimeTablingPerTask::ReverseProfile() {
435 for (
int i = 1; i + 1 < profile_.size(); ++i) {
436 profile_[i].start = -profile_[i + 1].start;
438 std::reverse(profile_.begin() + 1, profile_.end() - 1);
441bool TimeTablingPerTask::SweepAllTasks(
bool is_forward) {
443 const IntegerValue demand_threshold(
444 CapSub(CapacityMax().
value(), profile_max_height_.value()));
448 is_forward ? forward_num_tasks_to_sweep_ : backward_num_tasks_to_sweep_;
449 std::vector<int>& tasks =
450 is_forward ? forward_tasks_to_sweep_ : backward_tasks_to_sweep_;
455 for (
int i = num_tasks - 1; i >= 0; --i) {
456 const int t = tasks[i];
462 std::swap(tasks[i], tasks[--num_tasks]);
467 if (DemandMin(t) <= demand_threshold) {
468 if (DemandMax(t) == 0) {
470 std::swap(tasks[i], tasks[--num_tasks]);
479 if (helper_->
SizeMin(t) == 0) {
480 if (helper_->
SizeMax(t) == 0) {
481 std::swap(tasks[i], tasks[--num_tasks]);
486 if (!SweepTask(t))
return false;
492bool TimeTablingPerTask::SweepTask(
int task_id) {
494 const IntegerValue size_min = helper_->
SizeMin(task_id);
495 const IntegerValue initial_start_min = helper_->
StartMin(task_id);
496 const IntegerValue initial_end_min = helper_->
EndMin(task_id);
498 IntegerValue new_start_min = initial_start_min;
499 IntegerValue new_end_min = initial_end_min;
503 DCHECK(std::is_sorted(profile_.begin(), profile_.end()));
505 std::upper_bound(profile_.begin(), profile_.end(), new_start_min,
506 [&](IntegerValue
value,
const ProfileRectangle& rect) {
507 return value < rect.start;
514 const IntegerValue conflict_height = CapacityMax() - DemandMin(task_id);
517 bool conflict_found =
false;
530 for (; profile_[rec_id].start < limit; ++rec_id) {
532 if (profile_[rec_id].height <= conflict_height)
continue;
534 conflict_found =
true;
538 new_start_min = profile_[rec_id + 1].start;
540 if (IsInProfile(task_id)) {
550 new_end_min =
std::max(new_end_min, new_start_min + size_min);
553 if (profile_[rec_id].start < initial_end_min) {
554 last_initial_conflict =
std::min(new_start_min, initial_end_min) - 1;
558 if (!conflict_found)
return true;
560 if (initial_start_min != new_start_min &&
561 !UpdateStartingTime(task_id, last_initial_conflict, new_start_min)) {
568bool TimeTablingPerTask::UpdateStartingTime(
int task_id, IntegerValue left,
569 IntegerValue right) {
572 AddProfileReason(left, right);
590void TimeTablingPerTask::AddProfileReason(IntegerValue left,
591 IntegerValue right) {
592 for (
int i = 0; i < num_profile_tasks_; ++i) {
593 const int t = profile_tasks_[i];
611bool TimeTablingPerTask::IncreaseCapacity(IntegerValue
time,
612 IntegerValue new_min) {
613 if (new_min <= CapacityMin())
return true;
#define CHECK_LT(val1, val2)
#define CHECK_GT(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK(condition)
An Assignment is a variable -> domains mapping, used to report solutions to the user.
void RegisterReversibleInt(int id, int *rev)
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
int Register(PropagatorInterface *propagator)
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue LowerBound(IntegerVariable i) const
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
ABSL_MUST_USE_RESULT bool ConditionalEnqueue(Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
Class that owns everything related to a particular optimization model.
ReservoirTimeTabling(const std::vector< AffineExpression > ×, const std::vector< IntegerValue > &deltas, const std::vector< Literal > &presences, IntegerValue capacity, Model *model)
bool StartIsFixed(int t) const
IntegerValue EndMin(int t) const
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
std::vector< IntegerLiteral > * MutableIntegerReason()
void AddSizeMinReason(int t)
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
void AddPresenceReason(int t)
const std::vector< TaskTime > & TaskByIncreasingEndMin()
bool IsPresent(int t) const
void AddEndMinReason(int t, IntegerValue lower_bound)
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_start_min)
void SynchronizeAndSetTimeDirection(bool is_forward)
bool IsAbsent(int t) const
ABSL_MUST_USE_RESULT bool ReportConflict()
IntegerValue StartMin(int t) const
const std::vector< TaskTime > & TaskByDecreasingStartMax()
IntegerValue StartMax(int t) const
void AddStartMaxReason(int t, IntegerValue upper_bound)
IntegerValue SizeMax(int t) const
IntegerValue SizeMin(int t) const
void RegisterWith(GenericLiteralWatcher *watcher)
TimeTablingPerTask(const std::vector< AffineExpression > &demands, AffineExpression capacity, IntegerTrail *integer_trail, SchedulingConstraintHelper *helper)
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< IntegerValue > deltas, std::vector< Literal > presences, int64 min_level, int64 max_level, Model *model)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapSub(int64 x, int64 y)
IntegerLiteral GreaterOrEqual(IntegerValue bound) const