OR-Tools  8.1
disjunctive.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_DISJUNCTIVE_H_
15 #define OR_TOOLS_SAT_DISJUNCTIVE_H_
16 
17 #include <algorithm>
18 #include <functional>
19 #include <vector>
20 
21 #include "ortools/base/int_type.h"
22 #include "ortools/base/macros.h"
23 #include "ortools/sat/integer.h"
24 #include "ortools/sat/intervals.h"
25 #include "ortools/sat/model.h"
27 #include "ortools/sat/sat_base.h"
28 #include "ortools/sat/theta_tree.h"
29 
30 namespace operations_research {
31 namespace sat {
32 
33 // Enforces a disjunctive (or no overlap) constraint on the given interval
34 // variables. The intervals are interpreted as [start, end) and the constraint
35 // enforces that no time point belongs to two intervals.
36 //
37 // TODO(user): This is not completely true for empty intervals (start == end).
38 // Make sure such intervals are ignored by the constraint.
39 std::function<void(Model*)> Disjunctive(
40  const std::vector<IntervalVariable>& vars);
41 
42 // Creates Boolean variables for all the possible precedences of the form (task
43 // i is before task j) and forces that, for each couple of task (i,j), either i
44 // is before j or j is before i. Do not create any other propagators.
45 std::function<void(Model*)> DisjunctiveWithBooleanPrecedencesOnly(
46  const std::vector<IntervalVariable>& vars);
47 
48 // Same as Disjunctive() + DisjunctiveWithBooleanPrecedencesOnly().
49 std::function<void(Model*)> DisjunctiveWithBooleanPrecedences(
50  const std::vector<IntervalVariable>& vars);
51 
52 // Helper class to compute the end-min of a set of tasks given their start-min
53 // and size-min. In Petr Vilim's PhD "Global Constraints in Scheduling",
54 // this corresponds to his Theta-tree except that we use a O(n) implementation
55 // for most of the function here, not a O(log(n)) one.
56 class TaskSet {
57  public:
58  explicit TaskSet(int num_tasks) { sorted_tasks_.reserve(num_tasks); }
59 
60  struct Entry {
61  int task;
62  IntegerValue start_min;
63  IntegerValue size_min;
64 
65  // Note that the tie-breaking is not important here.
66  bool operator<(Entry other) const { return start_min < other.start_min; }
67  };
68 
69  // Insertion and modification. These leave sorted_tasks_ sorted.
70  void Clear() {
71  sorted_tasks_.clear();
72  optimized_restart_ = 0;
73  }
74  void AddEntry(const Entry& e);
75  void RemoveEntryWithIndex(int index);
76 
77  // Same as AddEntry({t, helper->ShiftedStartMin(t), helper->SizeMin(t)}).
78  // This is a minor optimization to not call SizeMin(t) twice.
79  void AddShiftedStartMinEntry(const SchedulingConstraintHelper& helper, int t);
80 
81  // Advanced usage, if the entry is present, this assumes that its start_min is
82  // >= the end min without it, and update the datastructure accordingly.
83  void NotifyEntryIsNowLastIfPresent(const Entry& e);
84 
85  // Advanced usage. Instead of calling many AddEntry(), it is more efficient to
86  // call AddUnsortedEntry() instead, but then Sort() MUST be called just after
87  // the insertions. Nothing is checked here, so it is up to the client to do
88  // that properly.
89  void AddUnsortedEntry(const Entry& e) { sorted_tasks_.push_back(e); }
90  void Sort() { std::sort(sorted_tasks_.begin(), sorted_tasks_.end()); }
91 
92  // Returns the end-min for the task in the set. The time profile of the tasks
93  // packed to the left will always be a set of contiguous tasks separated by
94  // empty space:
95  //
96  // [Bunch of tasks] ... [Bunch of tasks] ... [critical tasks].
97  //
98  // We call "critical tasks" the last group. These tasks will be solely
99  // responsible for for the end-min of the whole set. The returned
100  // critical_index will be the index of the first critical task in
101  // SortedTasks().
102  //
103  // A reason for the min end is:
104  // - The size-min of all the critical tasks.
105  // - The fact that all critical tasks have a start-min greater or equal to the
106  // first of them, that is SortedTasks()[critical_index].start_min.
107  //
108  // It is possible to behave like if one task was not in the set by setting
109  // task_to_ignore to the id of this task. This returns 0 if the set is empty
110  // in which case critical_index will be left unchanged.
111  IntegerValue ComputeEndMin(int task_to_ignore, int* critical_index) const;
112  IntegerValue ComputeEndMin() const;
113 
114  // Warning, this is only valid if ComputeEndMin() was just called. It is the
115  // same index as if one called ComputeEndMin(-1, &critical_index), but saves
116  // another unneeded loop.
117  int GetCriticalIndex() const { return optimized_restart_; }
118 
119  const std::vector<Entry>& SortedTasks() const { return sorted_tasks_; }
120 
121  private:
122  std::vector<Entry> sorted_tasks_;
123  mutable int optimized_restart_ = 0;
124 };
125 
126 // ============================================================================
127 // Below are many of the known propagation techniques for the disjunctive, each
128 // implemented in only one time direction and in its own propagator class. The
129 // Disjunctive() model function above will instantiate the used ones (according
130 // to the solver parameters) in both time directions.
131 //
132 // See Petr Vilim PhD "Global Constraints in Scheduling" for a description of
133 // some of the algorithm.
134 // ============================================================================
135 
137  public:
139  : helper_(helper) {
140  // Resize this once and for all.
141  task_to_event_.resize(helper_->NumTasks());
142  }
143  bool Propagate() final;
144  int RegisterWith(GenericLiteralWatcher* watcher);
145 
146  private:
147  bool PropagateSubwindow(IntegerValue global_window_end);
148 
150 
151  std::vector<TaskTime> window_;
152  std::vector<TaskTime> task_by_increasing_end_max_;
153 
154  ThetaLambdaTree<IntegerValue> theta_tree_;
155  std::vector<int> task_to_event_;
156 };
157 
159  public:
160  DisjunctiveDetectablePrecedences(bool time_direction,
162  : time_direction_(time_direction),
163  helper_(helper),
164  task_set_(helper->NumTasks()) {}
165  bool Propagate() final;
166  int RegisterWith(GenericLiteralWatcher* watcher);
167 
168  private:
169  bool PropagateSubwindow();
170 
171  std::vector<TaskTime> task_by_increasing_end_min_;
172  std::vector<TaskTime> task_by_increasing_start_max_;
173 
174  std::vector<bool> processed_;
175  std::vector<int> to_propagate_;
176 
177  const bool time_direction_;
179  TaskSet task_set_;
180 };
181 
182 // Singleton model class which is just a SchedulingConstraintHelper will all
183 // the intervals.
185  public:
188  model->GetOrCreate<IntervalsRepository>()->AllIntervals(), model) {}
189 };
190 
191 // This propagates the same things as DisjunctiveDetectablePrecedences, except
192 // that it only sort the full set of intervals once and then work on a combined
193 // set of disjunctives.
194 template <bool time_direction>
196  public:
197  explicit CombinedDisjunctive(Model* model);
198 
199  // After creation, this must be called for all the disjunctive constraints
200  // in the model.
201  void AddNoOverlap(const std::vector<IntervalVariable>& var);
202 
203  bool Propagate() final;
204 
205  private:
206  AllIntervalsHelper* helper_;
207  std::vector<std::vector<int>> task_to_disjunctives_;
208  std::vector<bool> task_is_added_;
209  std::vector<TaskSet> task_sets_;
210  std::vector<IntegerValue> end_mins_;
211 };
212 
214  public:
215  DisjunctiveNotLast(bool time_direction, SchedulingConstraintHelper* helper)
216  : time_direction_(time_direction),
217  helper_(helper),
218  task_set_(helper->NumTasks()) {}
219  bool Propagate() final;
220  int RegisterWith(GenericLiteralWatcher* watcher);
221 
222  private:
223  bool PropagateSubwindow();
224 
225  std::vector<TaskTime> start_min_window_;
226  std::vector<TaskTime> start_max_window_;
227 
228  const bool time_direction_;
230  TaskSet task_set_;
231 };
232 
234  public:
235  DisjunctiveEdgeFinding(bool time_direction,
237  : time_direction_(time_direction), helper_(helper) {}
238  bool Propagate() final;
239  int RegisterWith(GenericLiteralWatcher* watcher);
240 
241  private:
242  bool PropagateSubwindow(IntegerValue window_end_min);
243 
244  const bool time_direction_;
246 
247  // This only contains non-gray tasks.
248  std::vector<TaskTime> task_by_increasing_end_max_;
249 
250  // All these member are indexed in the same way.
251  std::vector<TaskTime> window_;
252  ThetaLambdaTree<IntegerValue> theta_tree_;
253  std::vector<IntegerValue> event_size_;
254 
255  // Task indexed.
256  std::vector<int> non_gray_task_to_event_;
257  std::vector<bool> is_gray_;
258 };
259 
260 // Exploits the precedences relations of the form "this set of disjoint
261 // IntervalVariables must be performed before a given IntegerVariable". The
262 // relations are computed with PrecedencesPropagator::ComputePrecedences().
264  public:
265  DisjunctivePrecedences(bool time_direction,
267  IntegerTrail* integer_trail,
268  PrecedencesPropagator* precedences)
269  : time_direction_(time_direction),
270  helper_(helper),
271  integer_trail_(integer_trail),
272  precedences_(precedences),
273  task_set_(helper->NumTasks()),
274  task_to_arc_index_(helper->NumTasks()) {}
275  bool Propagate() final;
276  int RegisterWith(GenericLiteralWatcher* watcher);
277 
278  private:
279  bool PropagateSubwindow();
280 
281  const bool time_direction_;
283  IntegerTrail* integer_trail_;
284  PrecedencesPropagator* precedences_;
285 
286  std::vector<TaskTime> window_;
287  std::vector<IntegerVariable> index_to_end_vars_;
288 
289  TaskSet task_set_;
290  std::vector<int> task_to_arc_index_;
291  std::vector<PrecedencesPropagator::IntegerPrecedences> before_;
292 };
293 
294 // This is an optimization for the case when we have a big number of such
295 // pairwise constraints. This should be roughtly equivalent to what the general
296 // disjunctive case is doing, but it dealt with variable size better and has a
297 // lot less overhead.
299  public:
301  : helper_(helper) {}
302  bool Propagate() final;
303  int RegisterWith(GenericLiteralWatcher* watcher);
304 
305  private:
307 };
308 
309 } // namespace sat
310 } // namespace operations_research
311 
312 #endif // OR_TOOLS_SAT_DISJUNCTIVE_H_
operations_research::sat::TaskSet::Entry::task
int task
Definition: disjunctive.h:61
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::TaskSet::Entry::start_min
IntegerValue start_min
Definition: disjunctive.h:62
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::DisjunctiveOverloadChecker::RegisterWith
int RegisterWith(GenericLiteralWatcher *watcher)
Definition: disjunctive.cc:629
operations_research::sat::DisjunctiveOverloadChecker::DisjunctiveOverloadChecker
DisjunctiveOverloadChecker(SchedulingConstraintHelper *helper)
Definition: disjunctive.h:138
operations_research::sat::TaskSet::NotifyEntryIsNowLastIfPresent
void NotifyEntryIsNowLastIfPresent(const Entry &e)
Definition: disjunctive.cc:182
operations_research::sat::TaskSet::AddUnsortedEntry
void AddUnsortedEntry(const Entry &e)
Definition: disjunctive.h:89
operations_research::sat::PropagatorInterface
Definition: integer.h:1043
operations_research::sat::DisjunctiveDetectablePrecedences
Definition: disjunctive.h:158
operations_research::sat::DisjunctiveWithTwoItems::DisjunctiveWithTwoItems
DisjunctiveWithTwoItems(SchedulingConstraintHelper *helper)
Definition: disjunctive.h:300
model.h
macros.h
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::CombinedDisjunctive
Definition: disjunctive.h:195
operations_research::sat::AllIntervalsHelper::AllIntervalsHelper
AllIntervalsHelper(Model *model)
Definition: disjunctive.h:186
index
int index
Definition: pack.cc:508
sat_base.h
operations_research::sat::DisjunctivePrecedences
Definition: disjunctive.h:263
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::AllIntervalsHelper
Definition: disjunctive.h:184
operations_research::sat::DisjunctiveOverloadChecker
Definition: disjunctive.h:136
operations_research::sat::DisjunctiveNotLast::DisjunctiveNotLast
DisjunctiveNotLast(bool time_direction, SchedulingConstraintHelper *helper)
Definition: disjunctive.h:215
operations_research::sat::DisjunctiveWithBooleanPrecedencesOnly
std::function< void(Model *)> DisjunctiveWithBooleanPrecedencesOnly(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:130
operations_research::sat::DisjunctiveEdgeFinding::DisjunctiveEdgeFinding
DisjunctiveEdgeFinding(bool time_direction, SchedulingConstraintHelper *helper)
Definition: disjunctive.h:235
operations_research::sat::TaskSet::AddShiftedStartMinEntry
void AddShiftedStartMinEntry(const SchedulingConstraintHelper &helper, int t)
Definition: disjunctive.cc:176
operations_research::sat::TaskTime
Definition: intervals.h:159
operations_research::sat::SchedulingConstraintHelper
Definition: intervals.h:172
operations_research::sat::PrecedencesPropagator
Definition: precedences.h:51
int_type.h
precedences.h
operations_research::sat::DisjunctiveEdgeFinding
Definition: disjunctive.h:233
intervals.h
operations_research::sat::DisjunctiveOverloadChecker::Propagate
bool Propagate() final
Definition: disjunctive.cc:458
operations_research::sat::DisjunctiveDetectablePrecedences::DisjunctiveDetectablePrecedences
DisjunctiveDetectablePrecedences(bool time_direction, SchedulingConstraintHelper *helper)
Definition: disjunctive.h:160
operations_research::sat::TaskSet::Entry
Definition: disjunctive.h:60
operations_research::sat::TaskSet::GetCriticalIndex
int GetCriticalIndex() const
Definition: disjunctive.h:117
operations_research::sat::DisjunctivePrecedences::DisjunctivePrecedences
DisjunctivePrecedences(bool time_direction, SchedulingConstraintHelper *helper, IntegerTrail *integer_trail, PrecedencesPropagator *precedences)
Definition: disjunctive.h:265
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::SchedulingConstraintHelper::NumTasks
int NumTasks() const
Definition: intervals.h:202
operations_research::sat::TaskSet::Sort
void Sort()
Definition: disjunctive.h:90
operations_research::sat::DisjunctiveNotLast
Definition: disjunctive.h:213
operations_research::sat::TaskSet::Clear
void Clear()
Definition: disjunctive.h:70
operations_research::sat::TaskSet::SortedTasks
const std::vector< Entry > & SortedTasks() const
Definition: disjunctive.h:119
theta_tree.h
operations_research::sat::TaskSet::ComputeEndMin
IntegerValue ComputeEndMin() const
Definition: disjunctive.cc:202
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::TaskSet::Entry::operator<
bool operator<(Entry other) const
Definition: disjunctive.h:66
operations_research::sat::TaskSet::TaskSet
TaskSet(int num_tasks)
Definition: disjunctive.h:58
operations_research::sat::Disjunctive
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:30
operations_research::sat::IntervalsRepository
Definition: intervals.h:45
operations_research::sat::TaskSet::RemoveEntryWithIndex
void RemoveEntryWithIndex(int index)
Definition: disjunctive.cc:197
operations_research::sat::TaskSet::AddEntry
void AddEntry(const Entry &e)
Definition: disjunctive.cc:161
operations_research::sat::TaskSet
Definition: disjunctive.h:56
operations_research::sat::DisjunctiveWithTwoItems
Definition: disjunctive.h:298
operations_research::sat::ThetaLambdaTree
Definition: theta_tree.h:103
operations_research::sat::DisjunctiveWithBooleanPrecedences
std::function< void(Model *)> DisjunctiveWithBooleanPrecedences(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:153
integer.h
operations_research::sat::TaskSet::Entry::size_min
IntegerValue size_min
Definition: disjunctive.h:63