14 #ifndef OR_TOOLS_SAT_INTERVALS_H_
15 #define OR_TOOLS_SAT_INTERVALS_H_
20 #include "absl/types/span.h"
61 IntervalVariable
CreateInterval(IntegerVariable start, IntegerVariable end,
62 IntegerVariable size, IntegerValue fixed_size,
63 LiteralIndex is_present);
66 LiteralIndex is_present,
67 bool add_linear_relation);
97 IntegerVariable
SizeVar(IntervalVariable i)
const {
102 return sizes_[i].var;
104 IntegerVariable
StartVar(IntervalVariable i)
const {
109 return starts_[i].var;
111 IntegerVariable
EndVar(IntervalVariable i)
const {
120 IntegerValue
MinSize(IntervalVariable i)
const {
125 IntegerValue
MaxSize(IntervalVariable i)
const {
131 std::vector<IntervalVariable> result;
199 absl::Span<const int> tasks);
223 IntegerValue
SizeMin(
int t)
const {
return cached_duration_min_[t]; }
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]; }
248 return cached_shifted_start_min_[t];
297 return &integer_reason_;
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);
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_; }
330 bool watch_start_max =
true,
331 bool watch_end_max =
true)
const;
339 IntegerValue event) {
340 CHECK(other_helper !=
nullptr);
341 other_helper_ = other_helper;
342 event_for_other_helper_ = event;
359 void InitSortedVectors();
360 void UpdateCachedValues(
int t);
369 void AddOtherReason(
int t);
372 void ImportOtherReasons();
379 bool current_time_direction_ =
true;
383 std::vector<AffineExpression> starts_;
384 std::vector<AffineExpression> ends_;
385 std::vector<AffineExpression> sizes_;
386 std::vector<LiteralIndex> reason_for_presence_;
390 std::vector<AffineExpression> minus_starts_;
391 std::vector<AffineExpression> minus_ends_;
394 int previous_level_ = 0;
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_;
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_;
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;
420 bool recompute_all_cache_ =
true;
421 std::vector<bool> recompute_cache_;
424 std::vector<Literal> literal_reason_;
425 std::vector<IntegerLiteral> integer_reason_;
429 IntegerValue event_for_other_helper_;
430 std::vector<bool> already_added_to_other_reasons_;
438 return integer_trail_->
IsFixed(starts_[t]);
442 return integer_trail_->
IsFixed(ends_[t]);
446 return integer_trail_->
IsFixed(sizes_[t]);
464 integer_reason_.clear();
465 literal_reason_.clear();
468 already_added_to_other_reasons_.assign(
NumTasks(),
false);
476 literal_reason_.push_back(
Literal(reason_for_presence_[t]).Negated());
484 literal_reason_.push_back(
Literal(reason_for_presence_[t]));
491 integer_reason_.push_back(
497 int t, IntegerValue lower_bound) {
505 int t, IntegerValue lower_bound) {
509 integer_reason_.push_back(starts_[t].
GreaterOrEqual(lower_bound));
514 int t, IntegerValue upper_bound) {
518 if (integer_trail_->
UpperBound(starts_[t]) <= upper_bound) {
520 integer_reason_.push_back(starts_[t].
LowerOrEqual(upper_bound));
525 integer_reason_.push_back(
529 integer_reason_.push_back(
536 int t, IntegerValue lower_bound) {
540 if (integer_trail_->
LowerBound(ends_[t]) >= lower_bound) {
547 integer_reason_.push_back(
551 integer_reason_.push_back(
558 int t, IntegerValue upper_bound) {
562 integer_reason_.push_back(ends_[t].
LowerOrEqual(upper_bound));
567 int t, IntegerValue energy_min, IntegerValue
time) {
588 IntervalVariable v) {
594 inline std::function<IntegerVariable(
const Model&)>
EndVar(IntervalVariable v) {
601 IntervalVariable v) {
626 IntervalVariable v) {
644 IntegerVariable start, IntegerVariable end, IntegerVariable size) {
668 IntegerValue(size), is_present.
Index());
672 inline std::function<IntervalVariable(Model*)>
677 const IntegerVariable start =
679 const IntegerVariable end =
683 integer_trail->MarkIntegerVariableAsOptional(end, is_present);
690 IntegerVariable start, IntegerVariable end, IntegerVariable size,
694 start, end, size, IntegerValue(0), is_present.
Index());
698 inline std::function<IntervalVariable(Model*)>
713 IntervalVariable parent,
const std::vector<IntervalVariable>& members) {
718 std::vector<Literal> presences;
719 std::vector<IntegerValue> sizes;
722 std::vector<LiteralWithCoeff> sat_ct;
723 for (
const IntervalVariable member : members) {
725 const Literal is_present = intervals->PresenceLiteral(member);
726 sat_ct.push_back({is_present, Coefficient(1)});
734 CHECK(integer_trail->IsFixed(intervals->Size(member)));
735 presences.push_back(is_present);
736 sizes.push_back(intervals->MinSize(member));
739 model->Add(
IsOneOf(intervals->SizeVar(parent), presences, sizes));
745 std::vector<IntegerVariable> starts;
746 starts.reserve(members.size());
747 for (
const IntervalVariable member : members) {
748 starts.push_back(intervals->StartVar(member));
754 std::vector<IntegerVariable> ends;
755 ends.reserve(members.size());
756 for (
const IntervalVariable member : members) {
757 ends.push_back(intervals->EndVar(member));
#define DCHECK_LE(val1, val2)
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK(condition)
An Assignment is a variable -> domains mapping, used to report solutions to the user.
bool IsFixed(IntegerVariable i) const
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool InPropagationLoop() const
IntegerValue UpperBound(IntegerVariable i) const
void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered)
IntegerValue LowerBound(IntegerVariable i) const
bool IsOptional(IntegerVariable i) const
IntegerVariable SizeVar(IntervalVariable i) const
AffineExpression End(IntervalVariable i) const
IntegerValue MaxSize(IntervalVariable i) const
AffineExpression Start(IntervalVariable i) const
Literal PresenceLiteral(IntervalVariable i) const
IntegerVariable StartVar(IntervalVariable i) const
IntegerValue MinSize(IntervalVariable i) const
IntervalsRepository(Model *model)
IntegerVariable EndVar(IntervalVariable i) const
bool IsPresent(IntervalVariable i) const
AffineExpression Size(IntervalVariable i) const
std::vector< IntervalVariable > AllIntervals() const
bool IsAbsent(IntervalVariable i) const
bool IsOptional(IntervalVariable i) const
IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end, IntegerVariable size, IntegerValue fixed_size, LiteralIndex is_present)
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
bool StartIsFixed(int t) const
IntegerValue ShiftedStartMin(int t) const
IntegerValue EndMin(int t) const
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
const std::vector< TaskTime > & TaskByDecreasingEndMax()
void SetLevel(int level) final
std::vector< Literal > * MutableLiteralReason()
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t)
SchedulingConstraintHelper(const std::vector< IntervalVariable > &tasks, Model *model)
void AddSizeMinReason(int t)
const std::vector< TaskTime > & TaskByIncreasingStartMin()
void AddStartMinReason(int t, IntegerValue lower_bound)
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
void AddPresenceReason(int t)
const std::vector< TaskTime > & TaskByIncreasingEndMin()
void ResetFromSubset(const SchedulingConstraintHelper &other, absl::Span< const int > tasks)
std::vector< IntegerLiteral > * MutableIntegerReason()
bool IsPresent(int t) const
bool SizeIsFixed(int t) const
void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time)
bool InPropagationLoop() const
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t, IntegerLiteral lit)
void RegisterWith(GenericLiteralWatcher *watcher)
std::string TaskDebugString(int t) const
void AddEndMinReason(int t, IntegerValue lower_bound)
bool EndIsFixed(int t) const
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_start_min)
void SynchronizeAndSetTimeDirection(bool is_forward)
bool IsAbsent(int t) const
IntegerValue EndMax(int t) const
ABSL_MUST_USE_RESULT bool ReportConflict()
const std::vector< AffineExpression > & Starts() const
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_start_max)
bool IsOptional(int t) const
IntegerValue StartMin(int t) const
const std::vector< TaskTime > & TaskByDecreasingStartMax()
ABSL_MUST_USE_RESULT bool PushTaskPresence(int t)
void AddAbsenceReason(int t)
Literal PresenceLiteral(int index) const
void AddEndMaxReason(int t, IntegerValue upper_bound)
void SetOtherHelper(SchedulingConstraintHelper *other_helper, IntegerValue event)
IntegerValue StartMax(int t) const
const std::vector< TaskTime > & TaskByIncreasingShiftedStartMin()
void AddReasonForBeingBefore(int before, int after)
const std::vector< AffineExpression > & Sizes() const
void AddStartMaxReason(int t, IntegerValue upper_bound)
IntegerValue SizeMax(int t) const
IntegerValue SizeMin(int t) const
const std::vector< AffineExpression > & Ends() const
const VariablesAssignment & Assignment() const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
std::function< IntegerVariable(const Model &)> SizeVar(IntervalVariable v)
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithOptionalVariables(int64 min_start, int64 max_end, int64 size, Literal is_present)
std::function< int64(const Model &)> MinSize(IntervalVariable v)
std::function< Literal(const Model &)> IsPresentLiteral(IntervalVariable v)
const LiteralIndex kNoLiteralIndex(-1)
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
std::function< void(Model *)> PartialIsOneOfVar(IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
const IntegerVariable kNoIntegerVariable(-1)
const IntervalVariable kNoIntervalVariable(-1)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
std::function< IntegerVariable(const Model &)> EndVar(IntervalVariable v)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
DEFINE_INT_TYPE(ClauseIndex, int)
std::function< bool(const Model &)> IsOptional(IntervalVariable v)
std::function< IntegerVariable(const Model &)> StartVar(IntervalVariable v)
std::function< int64(const Model &)> MaxSize(IntervalVariable v)
std::function< IntervalVariable(Model *)> NewIntervalWithVariableSize(int64 min_start, int64 max_end, int64 min_size, int64 max_size)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< void(Model *)> IntervalWithAlternatives(IntervalVariable parent, const std::vector< IntervalVariable > &members)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithVariableSize(int64 min_start, int64 max_end, int64 min_size, int64 max_size, Literal is_present)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool operator<(TaskTime other) const
bool operator>(TaskTime other) const