Google OR-Tools v9.12
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
intervals.h
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
14#ifndef OR_TOOLS_SAT_INTERVALS_H_
15#define OR_TOOLS_SAT_INTERVALS_H_
16
17#include <cstdint>
18#include <functional>
19#include <optional>
20#include <utility>
21#include <vector>
22
23#include "absl/container/flat_hash_map.h"
24#include "absl/log/check.h"
25#include "absl/types/span.h"
27#include "ortools/sat/clause.h"
28#include "ortools/sat/integer.h"
30#include "ortools/sat/model.h"
36
37namespace operations_research {
38namespace sat {
39
40// This class maintains a set of intervals which correspond to three integer
41// variables (start, end and size). It automatically registers with the
42// PrecedencesPropagator the relation between the bounds of each interval and
43// provides many helper functions to add precedences relation between intervals.
45 public:
46 explicit IntervalsRepository(Model* model)
47 : model_(model),
48 assignment_(model->GetOrCreate<Trail>()->Assignment()),
49 sat_solver_(model->GetOrCreate<SatSolver>()),
50 implications_(model->GetOrCreate<BinaryImplicationGraph>()),
51 integer_trail_(model->GetOrCreate<IntegerTrail>()) {}
52
53 // This type is neither copyable nor movable.
56
57 // Returns the current number of intervals in the repository.
58 // The interval will always be identified by an integer in [0, num_intervals).
59 int NumIntervals() const { return starts_.size(); }
60
61 // Functions to add a new interval to the repository.
62 // If add_linear_relation is true, then we also link start, size and end.
63 //
64 // - If size == kNoIntegerVariable, then the size is fixed to fixed_size.
65 // - If is_present != kNoLiteralIndex, then this is an optional interval.
66 IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end,
67 IntegerVariable size, IntegerValue fixed_size,
68 LiteralIndex is_present);
69 IntervalVariable CreateInterval(AffineExpression start, AffineExpression end,
71 LiteralIndex is_present = kNoLiteralIndex,
72 bool add_linear_relation = false);
73
74 // Returns whether or not a interval is optional and the associated literal.
75 bool IsOptional(IntervalVariable i) const {
76 return is_present_[i] != kNoLiteralIndex;
77 }
78 Literal PresenceLiteral(IntervalVariable i) const {
79 return Literal(is_present_[i]);
80 }
81 bool IsPresent(IntervalVariable i) const {
82 if (!IsOptional(i)) return true;
83 return assignment_.LiteralIsTrue(PresenceLiteral(i));
84 }
85 bool IsAbsent(IntervalVariable i) const {
86 if (!IsOptional(i)) return false;
87 return assignment_.LiteralIsFalse(PresenceLiteral(i));
88 }
89
90 // The 3 integer variables associated to a interval.
91 // Fixed size intervals will have a kNoIntegerVariable as size.
92 //
93 // Note: For an optional interval, the start/end variables are propagated
94 // assuming the interval is present. Because of that, these variables can
95 // cross each other or have an empty domain. If any of this happen, then the
96 // PresenceLiteral() of this interval will be propagated to false.
97 AffineExpression Size(IntervalVariable i) const { return sizes_[i]; }
98 AffineExpression Start(IntervalVariable i) const { return starts_[i]; }
99 AffineExpression End(IntervalVariable i) const { return ends_[i]; }
100
101 // Return the minimum size of the given IntervalVariable.
102 IntegerValue MinSize(IntervalVariable i) const {
103 return integer_trail_->LowerBound(sizes_[i]);
104 }
105
106 // Return the maximum size of the given IntervalVariable.
107 IntegerValue MaxSize(IntervalVariable i) const {
108 return integer_trail_->UpperBound(sizes_[i]);
109 }
110
111 // Utility function that returns a vector will all intervals.
112 std::vector<IntervalVariable> AllIntervals() const {
113 std::vector<IntervalVariable> result;
114 for (IntervalVariable i(0); i < NumIntervals(); ++i) {
115 result.push_back(i);
116 }
117 return result;
118 }
119
120 // Returns a SchedulingConstraintHelper corresponding to the given variables.
121 // Note that the order of interval in the helper will be the same.
122 //
123 // It is possible to indicate that this correspond to a disjunctive constraint
124 // by setting the Boolean to true. This is used by our scheduling heuristic
125 // based on precedences.
127 const std::vector<IntervalVariable>& variables,
128 bool register_as_disjunctive_helper = false);
129
131 const std::vector<IntervalVariable>& x_variables,
132 const std::vector<IntervalVariable>& y_variables);
133
134 // Returns a SchedulingDemandHelper corresponding to the given helper and
135 // demands. Note that the order of interval in the helper and the order of
136 // demands must be the compatible.
139 absl::Span<const AffineExpression> demands);
140
141 // Calls InitDecomposedEnergies on all SchedulingDemandHelper created.
143
144 // Assuming a and b cannot overlap if they are present, this create a new
145 // literal such that:
146 // - literal & presences => a is before b.
147 // - not(literal) & presences => b is before a.
148 // - not present => literal @ true for disallowing multiple solutions.
149 //
150 // If such literal already exists this returns it.
151 void CreateDisjunctivePrecedenceLiteral(IntervalVariable a,
152 IntervalVariable b);
154 const IntervalDefinition& a, const IntervalDefinition& b);
155
156 // Creates a literal l <=> y >= x.
157 // Returns true if such literal is "non-trivial" and was created.
159
160 // Returns a literal l <=> y >= x if it exist or kNoLiteralIndex
161 // otherwise. This could be the one created by
162 // CreateDisjunctivePrecedenceLiteral() or CreatePrecedenceLiteral().
164 AffineExpression y) const;
165
166 const std::vector<SchedulingConstraintHelper*>& AllDisjunctiveHelpers()
167 const {
168 return disjunctive_helpers_;
169 }
170
171 // We register cumulative at load time so that our search heuristic can loop
172 // over all cumulative constraints easily.
179 cumulative_helpers_.push_back(helper);
180 }
181 const std::vector<CumulativeHelper>& AllCumulativeHelpers() const {
182 return cumulative_helpers_;
183 }
184
185 private:
186 // External classes needed.
187 Model* model_;
188 const VariablesAssignment& assignment_;
189 SatSolver* sat_solver_;
190 BinaryImplicationGraph* implications_;
191 IntegerTrail* integer_trail_;
192
193 // Literal indicating if the tasks is executed. Tasks that are always executed
194 // will have a kNoLiteralIndex entry in this vector.
196
197 // The integer variables for each tasks.
201
202 // We can share the helper for all the propagators that work on the same set
203 // of intervals.
204 absl::flat_hash_map<std::vector<IntervalVariable>,
206 helper_repository_;
207 absl::flat_hash_map<
208 std::pair<std::vector<IntervalVariable>, std::vector<IntervalVariable>>,
210 no_overlap_2d_helper_repository_;
211 absl::flat_hash_map<
212 std::pair<SchedulingConstraintHelper*, std::vector<AffineExpression>>,
214 demand_helper_repository_;
215
216 // Disjunctive and normal precedences.
217 //
218 // Note that for normal precedences, we use directly the affine expression so
219 // that if many intervals share the same start, we don't re-create Booleans
220 // for no reason.
221 absl::flat_hash_map<std::pair<IntervalDefinition, IntervalDefinition>,
222 Literal>
223 disjunctive_precedences_;
224 absl::flat_hash_map<std::pair<AffineExpression, AffineExpression>, Literal>
225 precedences_;
226
227 // Disjunctive/Cumulative helpers_.
228 std::vector<SchedulingConstraintHelper*> disjunctive_helpers_;
229 std::vector<CumulativeHelper> cumulative_helpers_;
230};
231
232// =============================================================================
233// Model based functions.
234// =============================================================================
235
236inline std::function<int64_t(const Model&)> MinSize(IntervalVariable v) {
237 return [=](const Model& model) {
238 return model.Get<IntervalsRepository>()->MinSize(v).value();
239 };
240}
241
242inline std::function<int64_t(const Model&)> MaxSize(IntervalVariable v) {
243 return [=](const Model& model) {
244 return model.Get<IntervalsRepository>()->MaxSize(v).value();
245 };
246}
247
248inline std::function<bool(const Model&)> IsOptional(IntervalVariable v) {
249 return [=](const Model& model) {
250 return model.Get<IntervalsRepository>()->IsOptional(v);
251 };
252}
253
254inline std::function<Literal(const Model&)> IsPresentLiteral(
255 IntervalVariable v) {
256 return [=](const Model& model) {
257 return model.Get<IntervalsRepository>()->PresenceLiteral(v);
258 };
259}
260
261inline std::function<IntervalVariable(Model*)> NewInterval(int64_t min_start,
262 int64_t max_end,
263 int64_t size) {
264 return [=](Model* model) {
265 CHECK_LE(min_start + size, max_end);
266 const IntegerVariable start =
267 model->Add(NewIntegerVariable(min_start, max_end - size));
268 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
269 AffineExpression(start),
270 AffineExpression(start, IntegerValue(1), IntegerValue(size)),
271 AffineExpression(IntegerValue(size)), kNoLiteralIndex,
272 /*add_linear_relation=*/false);
273 };
274}
275
276inline std::function<IntervalVariable(Model*)> NewInterval(
277 IntegerVariable start, IntegerVariable end, IntegerVariable size) {
278 return [=](Model* model) {
279 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
280 start, end, size, IntegerValue(0), kNoLiteralIndex);
281 };
282}
283
284inline std::function<IntervalVariable(Model*)> NewIntervalWithVariableSize(
285 int64_t min_start, int64_t max_end, int64_t min_size, int64_t max_size) {
286 return [=](Model* model) {
287 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
288 model->Add(NewIntegerVariable(min_start, max_end)),
289 model->Add(NewIntegerVariable(min_start, max_end)),
290 model->Add(NewIntegerVariable(min_size, max_size)), IntegerValue(0),
292 };
293}
294
295// Note that this should only be used in tests.
296inline std::function<IntervalVariable(Model*)> NewOptionalInterval(
297 int64_t min_start, int64_t max_end, int64_t size, Literal is_present) {
298 return [=](Model* model) {
299 CHECK_LE(min_start + size, max_end);
300 const IntegerVariable start =
301 model->Add(NewIntegerVariable(min_start, max_end - size));
302 const IntervalVariable interval =
303 model->GetOrCreate<IntervalsRepository>()->CreateInterval(
304 AffineExpression(start),
305 AffineExpression(start, IntegerValue(1), IntegerValue(size)),
306 AffineExpression(IntegerValue(size)), is_present.Index(),
307 /*add_linear_relation=*/false);
308
309 // To not have too many solutions during enumeration, we force the
310 // start at its min value for absent interval.
311 model->Add(Implication({is_present.Negated()},
312 IntegerLiteral::LowerOrEqual(start, min_start)));
313 return interval;
314 };
315}
316
317inline std::function<IntervalVariable(Model*)> NewOptionalInterval(
318 IntegerVariable start, IntegerVariable end, IntegerVariable size,
319 Literal is_present) {
320 return [=](Model* model) {
321 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
322 start, end, size, IntegerValue(0), is_present.Index());
323 };
324}
325
326inline std::function<IntervalVariable(Model*)>
327NewOptionalIntervalWithVariableSize(int64_t min_start, int64_t max_end,
328 int64_t min_size, int64_t max_size,
329 Literal is_present) {
330 return [=](Model* model) {
331 return model->GetOrCreate<IntervalsRepository>()->CreateInterval(
332 model->Add(NewIntegerVariable(min_start, max_end)),
333 model->Add(NewIntegerVariable(min_start, max_end)),
334 model->Add(NewIntegerVariable(min_size, max_size)), IntegerValue(0),
335 is_present.Index());
336 };
337}
338
340 const AffineExpression& capacity, SchedulingDemandHelper* demands_helper,
341 Model* model, std::vector<IntegerVariable>* vars);
342
343} // namespace sat
344} // namespace operations_research
345
346#endif // OR_TOOLS_SAT_INTERVALS_H_
Definition model.h:341
IntervalsRepository(const IntervalsRepository &)=delete
This type is neither copyable nor movable.
SchedulingDemandHelper * GetOrCreateDemandHelper(SchedulingConstraintHelper *helper, absl::Span< const AffineExpression > demands)
Definition intervals.cc:305
AffineExpression Start(IntervalVariable i) const
Definition intervals.h:98
AffineExpression Size(IntervalVariable i) const
Definition intervals.h:97
AffineExpression End(IntervalVariable i) const
Definition intervals.h:99
LiteralIndex GetPrecedenceLiteral(AffineExpression x, AffineExpression y) const
Definition intervals.cc:209
LiteralIndex GetOrCreateDisjunctivePrecedenceLiteral(const IntervalDefinition &a, const IntervalDefinition &b)
Definition intervals.cc:96
bool IsAbsent(IntervalVariable i) const
Definition intervals.h:85
const std::vector< CumulativeHelper > & AllCumulativeHelpers() const
Definition intervals.h:181
void InitAllDecomposedEnergies()
Calls InitDecomposedEnergies on all SchedulingDemandHelper created.
Definition intervals.cc:321
Literal PresenceLiteral(IntervalVariable i) const
Definition intervals.h:78
void CreateDisjunctivePrecedenceLiteral(IntervalVariable a, IntervalVariable b)
Definition intervals.cc:79
const std::vector< SchedulingConstraintHelper * > & AllDisjunctiveHelpers() const
Definition intervals.h:166
bool IsOptional(IntervalVariable i) const
Returns whether or not a interval is optional and the associated literal.
Definition intervals.h:75
void RegisterCumulative(CumulativeHelper helper)
Definition intervals.h:178
IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end, IntegerVariable size, IntegerValue fixed_size, LiteralIndex is_present)
Definition intervals.cc:38
IntegerValue MaxSize(IntervalVariable i) const
Return the maximum size of the given IntervalVariable.
Definition intervals.h:107
IntegerValue MinSize(IntervalVariable i) const
Return the minimum size of the given IntervalVariable.
Definition intervals.h:102
SchedulingConstraintHelper * GetOrCreateHelper(const std::vector< IntervalVariable > &variables, bool register_as_disjunctive_helper=false)
Definition intervals.cc:219
IntervalsRepository & operator=(const IntervalsRepository &)=delete
NoOverlap2DConstraintHelper * GetOrCreate2DHelper(const std::vector< IntervalVariable > &x_variables, const std::vector< IntervalVariable > &y_variables)
Definition intervals.cc:258
std::vector< IntervalVariable > AllIntervals() const
Utility function that returns a vector will all intervals.
Definition intervals.h:112
bool CreatePrecedenceLiteral(AffineExpression x, AffineExpression y)
Definition intervals.cc:182
bool IsPresent(IntervalVariable i) const
Definition intervals.h:81
LiteralIndex Index() const
Definition sat_base.h:91
std::function< int64_t(const Model &)> MaxSize(IntervalVariable v)
Definition intervals.h:244
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithVariableSize(int64_t min_start, int64_t max_end, int64_t min_size, int64_t max_size, Literal is_present)
Definition intervals.h:329
std::function< Literal(const Model &)> IsPresentLiteral(IntervalVariable v)
Definition intervals.h:256
const LiteralIndex kNoLiteralIndex(-1)
std::function< IntervalVariable(Model *)> NewIntervalWithVariableSize(int64_t min_start, int64_t max_end, int64_t min_size, int64_t max_size)
Definition intervals.h:286
std::function< IntervalVariable(Model *)> NewInterval(int64_t min_start, int64_t max_end, int64_t size)
Definition intervals.h:263
std::function< void(Model *)> Implication(absl::Span< const Literal > enforcement_literals, IntegerLiteral i)
Definition integer.h:1609
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64_t min_start, int64_t max_end, int64_t size, Literal is_present)
Definition intervals.h:298
void AppendVariablesFromCapacityAndDemands(const AffineExpression &capacity, SchedulingDemandHelper *demands_helper, Model *model, std::vector< IntegerVariable > *vars)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64_t lb, int64_t ub)
Definition integer.h:1491
std::function< int64_t(const Model &)> MinSize(IntervalVariable v)
Definition intervals.h:238
std::function< bool(const Model &)> IsOptional(IntervalVariable v)
Definition intervals.h:250
In SWIG mode, we don't want anything besides these top-level includes.
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)