Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
intervals.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 <optional>
17#include <utility>
18#include <vector>
19
20#include "absl/container/flat_hash_map.h"
21#include "absl/log/check.h"
22#include "absl/types/span.h"
24#include "ortools/sat/clause.h"
25#include "ortools/sat/integer.h"
29#include "ortools/sat/model.h"
36
37namespace operations_research {
38namespace sat {
39
41 : model_(model),
42 assignment_(model->GetOrCreate<Trail>()->Assignment()),
43 sat_solver_(model->GetOrCreate<SatSolver>()),
44 implications_(model->GetOrCreate<BinaryImplicationGraph>()),
45 integer_trail_(model->GetOrCreate<IntegerTrail>()),
46 relations_maps_(model->GetOrCreate<BinaryRelationsMaps>()) {}
47
48IntervalVariable IntervalsRepository::CreateInterval(IntegerVariable start,
49 IntegerVariable end,
50 IntegerVariable size,
51 IntegerValue fixed_size,
52 LiteralIndex is_present) {
54 size == kNoIntegerVariable
55 ? AffineExpression(fixed_size)
56 : AffineExpression(size),
57 is_present, /*add_linear_relation=*/true);
58}
59
63 LiteralIndex is_present,
64 bool add_linear_relation) {
65 // Create the interval.
66 const IntervalVariable i(starts_.size());
67 starts_.push_back(start);
68 ends_.push_back(end);
69 sizes_.push_back(size);
70 is_present_.push_back(is_present);
71
72 std::vector<Literal> enforcement_literals;
73 if (is_present != kNoLiteralIndex) {
74 enforcement_literals.push_back(Literal(is_present));
75 }
76
77 if (add_linear_relation) {
78 LinearConstraintBuilder builder(model_, IntegerValue(0), IntegerValue(0));
79 builder.AddTerm(Start(i), IntegerValue(1));
80 builder.AddTerm(Size(i), IntegerValue(1));
81 builder.AddTerm(End(i), IntegerValue(-1));
82 LoadConditionalLinearConstraint(enforcement_literals, builder.Build(),
83 model_);
84 }
85
86 return i;
87}
88
90 IntervalVariable a, IntervalVariable b) {
92 IntervalDefinition{.start = Start(a),
93 .end = End(a),
94 .size = Size(a),
95 .is_present = IsOptional(a)
96 ? std::optional(PresenceLiteral(a))
97 : std::nullopt},
98 IntervalDefinition{.start = Start(b),
99 .end = End(b),
100 .size = Size(b),
101 .is_present = IsOptional(b)
102 ? std::optional(PresenceLiteral(b))
103 : std::nullopt});
104}
105
106LiteralIndex
108 const IntervalDefinition& a, const IntervalDefinition& b) {
109 auto it = disjunctive_precedences_.find({a, b});
110 if (it != disjunctive_precedences_.end()) return it->second.Index();
111
112 std::vector<Literal> enforcement_literals;
113 if (a.is_present.has_value()) {
114 enforcement_literals.push_back(a.is_present.value());
115 }
116 if (b.is_present.has_value()) {
117 enforcement_literals.push_back(b.is_present.value());
118 }
119
120 auto remove_fixed = [assignment =
121 &assignment_](std::vector<Literal>& literals) {
122 int new_size = 0;
123 for (const Literal l : literals) {
124 // We can ignore always absent interval, and skip the literal of the
125 // interval that are now always present.
126 if (assignment->LiteralIsTrue(l)) continue;
127 if (assignment->LiteralIsFalse(l)) return false;
128 literals[new_size++] = l;
129 }
130 literals.resize(new_size);
131 return true;
132 };
133
134 if (sat_solver_->CurrentDecisionLevel() == 0) {
135 if (!remove_fixed(enforcement_literals)) return kNoLiteralIndex;
136 }
137
138 // task_a is currently before task_b ?
139 // Lets not create a literal that will be propagated right away.
140 if (integer_trail_->UpperBound(a.start) < integer_trail_->LowerBound(b.end)) {
141 if (sat_solver_->CurrentDecisionLevel() == 0) {
142 AddConditionalAffinePrecedence(enforcement_literals, a.end, b.start,
143 model_);
144 }
145 return kNoLiteralIndex;
146 }
147
148 // task_b is before task_a ?
149 if (integer_trail_->UpperBound(b.start) < integer_trail_->LowerBound(a.end)) {
150 if (sat_solver_->CurrentDecisionLevel() == 0) {
151 AddConditionalAffinePrecedence(enforcement_literals, b.end, a.start,
152 model_);
153 }
154 return kNoLiteralIndex;
155 }
156
157 // Abort if the relation is already known.
158 if (relations_maps_->GetLevelZeroPrecedenceStatus(a.end, b.start) ==
160 relations_maps_->GetLevelZeroPrecedenceStatus(b.end, a.start) ==
162 return kNoLiteralIndex;
163 }
164
165 // Create a new literal.
166 //
167 // TODO(user): If there are no enforcement and we already have at one of:
168 // - s <=> a.end <= b.start
169 // - t <=> b.end <= a.start
170 // We could use (s, not(s)) or (not(t), t) and make sure s = not(t) if both
171 // exists.
172 //
173 // TODO(user): Otherwise, an alternative solution is to create s and t (can be
174 // one more Boolean though), and have enforcement => s + t == 1. The later
175 // might not even be needed though, since interval equation should already
176 // enforce it.
177 const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
178 const Literal a_before_b = Literal(boolean_var, true);
179 disjunctive_precedences_.insert({{a, b}, a_before_b});
180 disjunctive_precedences_.insert({{b, a}, a_before_b.Negated()});
181
182 // Also insert it in precedences.
183 if (enforcement_literals.empty()) {
184 relations_maps_->AddReifiedPrecedenceIfNonTrivial(a_before_b, a.end,
185 b.start);
186 relations_maps_->AddReifiedPrecedenceIfNonTrivial(a_before_b.Negated(),
187 b.end, a.start);
188 }
189
190 enforcement_literals.push_back(a_before_b);
191 AddConditionalAffinePrecedence(enforcement_literals, a.end, b.start, model_);
192 enforcement_literals.pop_back();
193
194 enforcement_literals.push_back(a_before_b.Negated());
195 AddConditionalAffinePrecedence(enforcement_literals, b.end, a.start, model_);
196 enforcement_literals.pop_back();
197
198 // The calls to AddConditionalAffinePrecedence() might have fixed some of the
199 // enforcement literals. Remove them if we are at level zero.
200 if (sat_solver_->CurrentDecisionLevel() == 0) {
201 if (!remove_fixed(enforcement_literals)) return kNoLiteralIndex;
202 }
203
204 // Force the value of boolean_var in case the precedence is not active. This
205 // avoids duplicate solutions when enumerating all possible solutions.
206 for (const Literal l : enforcement_literals) {
207 implications_->AddBinaryClause(l, a_before_b);
208 }
209
210 return a_before_b;
211}
212
215 const LiteralIndex index = relations_maps_->GetReifiedPrecedence(x, y);
216 if (index != kNoLiteralIndex) return false;
217
218 // We want l => x <= y and not(l) => x > y <=> y + 1 <= x
219 // Do not create l if the relation is always true or false.
220 if (relations_maps_->GetLevelZeroPrecedenceStatus(x, y) !=
222 return false;
223 }
224
225 // Create a new literal.
226 const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
227 const Literal x_before_y = Literal(boolean_var, true);
228 relations_maps_->AddReifiedPrecedenceIfNonTrivial(x_before_y, x, y);
229
230 AffineExpression y_plus_one = y;
231 y_plus_one.constant += 1;
232 AddConditionalAffinePrecedence({x_before_y}, x, y, model_);
233 AddConditionalAffinePrecedence({x_before_y.Negated()}, y_plus_one, x, model_);
234 return true;
235}
236
239 return relations_maps_->GetReifiedPrecedence(x, y);
240}
241
244 {
245 const LiteralIndex index = GetPrecedenceLiteral(x, y);
246 if (index != kNoLiteralIndex) return Literal(index);
247 }
248
250 const LiteralIndex index = relations_maps_->GetReifiedPrecedence(x, y);
251 CHECK_NE(index, kNoLiteralIndex);
252 return Literal(index);
253}
254
255// TODO(user): Ideally we should sort the vector of variables, but right now
256// we cannot since we often use this with a parallel vector of demands. So this
257// "sorting" should happen in the presolver so we can share as much as possible.
259 const std::vector<IntervalVariable>& variables,
260 bool register_as_disjunctive_helper) {
261 const auto it = helper_repository_.find(variables);
262 if (it != helper_repository_.end()) return it->second;
263 std::vector<AffineExpression> starts;
264 std::vector<AffineExpression> ends;
265 std::vector<AffineExpression> sizes;
266 std::vector<LiteralIndex> reason_for_presence;
267
268 const int num_variables = variables.size();
269 starts.reserve(num_variables);
270 ends.reserve(num_variables);
271 sizes.reserve(num_variables);
272 reason_for_presence.reserve(num_variables);
273
274 for (const IntervalVariable i : variables) {
275 if (IsOptional(i)) {
276 reason_for_presence.push_back(PresenceLiteral(i).Index());
277 } else {
278 reason_for_presence.push_back(kNoLiteralIndex);
279 }
280 sizes.push_back(Size(i));
281 starts.push_back(Start(i));
282 ends.push_back(End(i));
283 }
284
286 std::move(starts), std::move(ends), std::move(sizes),
287 std::move(reason_for_presence), model_);
288 helper->RegisterWith(model_->GetOrCreate<GenericLiteralWatcher>());
289 helper_repository_[variables] = helper;
290 model_->TakeOwnership(helper);
291 if (register_as_disjunctive_helper) {
292 disjunctive_helpers_.push_back(helper);
293 }
294 return helper;
295}
296
298 const std::vector<IntervalVariable>& x_variables,
299 const std::vector<IntervalVariable>& y_variables) {
300 const auto it =
301 no_overlap_2d_helper_repository_.find({x_variables, y_variables});
302 if (it != no_overlap_2d_helper_repository_.end()) return it->second;
303
304 std::vector<AffineExpression> x_starts;
305 std::vector<AffineExpression> x_ends;
306 std::vector<AffineExpression> x_sizes;
307 std::vector<LiteralIndex> x_reason_for_presence;
308
309 for (const IntervalVariable i : x_variables) {
310 if (IsOptional(i)) {
311 x_reason_for_presence.push_back(PresenceLiteral(i).Index());
312 } else {
313 x_reason_for_presence.push_back(kNoLiteralIndex);
314 }
315 x_sizes.push_back(Size(i));
316 x_starts.push_back(Start(i));
317 x_ends.push_back(End(i));
318 }
319 std::vector<AffineExpression> y_starts;
320 std::vector<AffineExpression> y_ends;
321 std::vector<AffineExpression> y_sizes;
322 std::vector<LiteralIndex> y_reason_for_presence;
323
324 for (const IntervalVariable i : y_variables) {
325 if (IsOptional(i)) {
326 y_reason_for_presence.push_back(PresenceLiteral(i).Index());
327 } else {
328 y_reason_for_presence.push_back(kNoLiteralIndex);
329 }
330 y_sizes.push_back(Size(i));
331 y_starts.push_back(Start(i));
332 y_ends.push_back(End(i));
333 }
335 std::move(x_starts), std::move(x_ends), std::move(x_sizes),
336 std::move(x_reason_for_presence), std::move(y_starts), std::move(y_ends),
337 std::move(y_sizes), std::move(y_reason_for_presence), model_);
338 helper->RegisterWith(model_->GetOrCreate<GenericLiteralWatcher>());
339 no_overlap_2d_helper_repository_[{x_variables, y_variables}] = helper;
340 model_->TakeOwnership(helper);
341 return helper;
342}
343
346 absl::Span<const AffineExpression> demands) {
347 const std::pair<SchedulingConstraintHelper*, std::vector<AffineExpression>>
348 key = {helper,
349 std::vector<AffineExpression>(demands.begin(), demands.end())};
350 const auto it = demand_helper_repository_.find(key);
351 if (it != demand_helper_repository_.end()) return it->second;
352
353 SchedulingDemandHelper* demand_helper =
354 new SchedulingDemandHelper(demands, helper, model_);
355 model_->TakeOwnership(demand_helper);
356 demand_helper_repository_[key] = demand_helper;
357 return demand_helper;
358}
359
361 for (const auto& it : demand_helper_repository_) {
362 it.second->InitDecomposedEnergies();
363 }
364}
365
366} // namespace sat
367} // namespace operations_research
SchedulingDemandHelper * GetOrCreateDemandHelper(SchedulingConstraintHelper *helper, absl::Span< const AffineExpression > demands)
Definition intervals.cc:344
AffineExpression Start(IntervalVariable i) const
Definition intervals.h:92
AffineExpression Size(IntervalVariable i) const
Definition intervals.h:91
AffineExpression End(IntervalVariable i) const
Definition intervals.h:93
Literal GetOrCreatePrecedenceLiteral(AffineExpression x, AffineExpression y)
Definition intervals.cc:242
LiteralIndex GetPrecedenceLiteral(AffineExpression x, AffineExpression y) const
Definition intervals.cc:237
void InitAllDecomposedEnergies()
Calls InitDecomposedEnergies on all SchedulingDemandHelper created.
Definition intervals.cc:360
Literal PresenceLiteral(IntervalVariable i) const
Definition intervals.h:72
void CreateDisjunctivePrecedenceLiteral(IntervalVariable a, IntervalVariable b)
Definition intervals.cc:89
bool CreatePrecedenceLiteralIfNonTrivial(AffineExpression x, AffineExpression y)
Definition intervals.cc:213
LiteralIndex GetOrCreateDisjunctivePrecedenceLiteralIfNonTrivial(const IntervalDefinition &a, const IntervalDefinition &b)
Definition intervals.cc:107
bool IsOptional(IntervalVariable i) const
Returns whether or not a interval is optional and the associated literal.
Definition intervals.h:69
IntervalVariable CreateInterval(IntegerVariable start, IntegerVariable end, IntegerVariable size, IntegerValue fixed_size, LiteralIndex is_present)
Definition intervals.cc:48
SchedulingConstraintHelper * GetOrCreateHelper(const std::vector< IntervalVariable > &variables, bool register_as_disjunctive_helper=false)
Definition intervals.cc:258
NoOverlap2DConstraintHelper * GetOrCreate2DHelper(const std::vector< IntervalVariable > &x_variables, const std::vector< IntervalVariable > &y_variables)
Definition intervals.cc:297
void AddTerm(IntegerVariable var, IntegerValue coeff)
const LiteralIndex kNoLiteralIndex(-1)
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
LinearConstraint version.
const IntegerVariable kNoIntegerVariable(-1)
void AddConditionalAffinePrecedence(const absl::Span< const Literal > enforcement_literals, AffineExpression left, AffineExpression right, Model *model)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)