Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
linear_relaxation.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 <algorithm>
17#include <cstdint>
18#include <limits>
19#include <numeric>
20#include <optional>
21#include <utility>
22#include <vector>
23
24#include "absl/base/attributes.h"
25#include "absl/container/btree_map.h"
26#include "absl/container/flat_hash_map.h"
27#include "absl/container/flat_hash_set.h"
28#include "absl/log/check.h"
29#include "absl/meta/type_traits.h"
30#include "absl/types/span.h"
31#include "google/protobuf/message.h"
36#include "ortools/sat/circuit.h" // for ReindexArcs.
37#include "ortools/sat/clause.h"
41#include "ortools/sat/cuts.h"
45#include "ortools/sat/integer.h"
51#include "ortools/sat/model.h"
61#include "ortools/sat/util.h"
65
66namespace operations_research {
67namespace sat {
68
69namespace {
70
71std::pair<IntegerValue, IntegerValue> GetMinAndMaxNotEncoded(
72 IntegerVariable var,
73 const absl::flat_hash_set<IntegerValue>& encoded_values,
74 const Model& model) {
75 CHECK(VariableIsPositive(var));
76 const PositiveOnlyIndex index = GetPositiveOnlyIndex(var);
77
78 const auto* domains = model.Get<IntegerDomains>();
79 if (domains == nullptr || index >= domains->size()) {
81 }
82
83 // The domain can be large, but the list of values shouldn't, so this
84 // runs in O(encoded_values.size());
85 IntegerValue min = kMaxIntegerValue;
86 for (const int64_t v : (*domains)[index].Values()) {
87 if (!encoded_values.contains(IntegerValue(v))) {
88 min = IntegerValue(v);
89 break;
90 }
91 }
92
93 IntegerValue max = kMinIntegerValue;
94 const Domain negated_domain = (*domains)[index].Negation();
95 for (const int64_t v : negated_domain.Values()) {
96 if (!encoded_values.contains(IntegerValue(-v))) {
97 max = IntegerValue(-v);
98 break;
99 }
100 }
101
102 return {min, max};
103}
104
105// Collect all the affines expressions in a LinMax constraint.
106// It checks that these are indeed affine expressions, and that they all share
107// the same variable.
108// It returns the shared variable, as well as a vector of pairs
109// (coefficient, offset) when each affine is coefficient * shared_var + offset.
110void CollectAffineExpressionWithSingleVariable(
111 const ConstraintProto& ct, CpModelMapping* mapping, IntegerVariable* var,
112 std::vector<std::pair<IntegerValue, IntegerValue>>* affines) {
113 DCHECK(ExpressionsContainsOnlyOneVar(ct.lin_max().exprs()));
114 CHECK_EQ(ct.constraint_case(), ConstraintProto::ConstraintCase::kLinMax);
115 *var = kNoIntegerVariable;
116 affines->clear();
117 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
118 if (expr.vars().empty()) {
119 affines->push_back({IntegerValue(0), IntegerValue(expr.offset())});
120 } else {
121 CHECK_EQ(expr.vars().size(), 1);
122 const IntegerVariable affine_var = mapping->Integer(expr.vars(0));
123 if (*var == kNoIntegerVariable) {
124 *var = PositiveVariable(affine_var);
125 }
126 if (VariableIsPositive(affine_var)) {
127 CHECK_EQ(affine_var, *var);
128 affines->push_back(
129 {IntegerValue(expr.coeffs(0)), IntegerValue(expr.offset())});
130 } else {
131 CHECK_EQ(NegationOf(affine_var), *var);
132 affines->push_back(
133 {IntegerValue(-expr.coeffs(0)), IntegerValue(expr.offset())});
134 }
135 }
136 }
137}
138
139} // namespace
140
141void AppendRelaxationForEqualityEncoding(IntegerVariable var,
142 const Model& model,
143 LinearRelaxation* relaxation,
144 int* num_tight, int* num_loose) {
145 const auto* encoder = model.Get<IntegerEncoder>();
146 const auto* integer_trail = model.Get<IntegerTrail>();
147 if (encoder == nullptr || integer_trail == nullptr) return;
148
149 std::vector<Literal> at_most_one_ct;
150 absl::flat_hash_set<IntegerValue> encoded_values;
151 std::vector<ValueLiteralPair> encoding;
152 {
153 const std::vector<ValueLiteralPair>& initial_encoding =
154 encoder->PartialDomainEncoding(var);
155 if (initial_encoding.empty()) return;
156 for (const auto value_literal : initial_encoding) {
157 const Literal literal = value_literal.literal;
158
159 // Note that we skip pairs that do not have an Integer view.
160 if (encoder->GetLiteralView(literal) == kNoIntegerVariable &&
161 encoder->GetLiteralView(literal.Negated()) == kNoIntegerVariable) {
162 continue;
163 }
164
165 encoding.push_back(value_literal);
166 at_most_one_ct.push_back(literal);
167 encoded_values.insert(value_literal.value);
168 }
169 }
170 if (encoded_values.empty()) return;
171
172 // TODO(user): PartialDomainEncoding() filter pair corresponding to literal
173 // set to false, however the initial variable Domain is not always updated. As
174 // a result, these min/max can be larger than in reality. Try to fix this even
175 // if in practice this is a rare occurrence, as the presolve should have
176 // propagated most of what we can.
177 const auto [min_not_encoded, max_not_encoded] =
178 GetMinAndMaxNotEncoded(var, encoded_values, model);
179
180 // This means that there are no non-encoded value and we have a full encoding.
181 // We substract the minimum value to reduce its size.
182 if (min_not_encoded == kMaxIntegerValue) {
183 const IntegerValue rhs = encoding[0].value;
184 LinearConstraintBuilder at_least_one(&model, IntegerValue(1),
186 LinearConstraintBuilder encoding_ct(&model, rhs, rhs);
187 encoding_ct.AddTerm(var, IntegerValue(1));
188 for (const auto value_literal : encoding) {
189 const Literal lit = value_literal.literal;
190 CHECK(at_least_one.AddLiteralTerm(lit, IntegerValue(1)));
191
192 const IntegerValue delta = value_literal.value - rhs;
193 if (delta != IntegerValue(0)) {
194 CHECK_GE(delta, IntegerValue(0));
195 CHECK(encoding_ct.AddLiteralTerm(lit, -delta));
196 }
197 }
198
199 // It is possible that the linear1 encoding respect our overflow
200 // precondition but not the Var = sum bool * value one. In this case, we
201 // just don't encode it this way. Hopefully, most normal model will not run
202 // into this.
203 LinearConstraint lc = encoding_ct.Build();
204 if (!PossibleOverflow(*integer_trail, lc)) {
205 relaxation->linear_constraints.push_back(at_least_one.Build());
206 relaxation->linear_constraints.push_back(std::move(lc));
207 relaxation->at_most_ones.push_back(at_most_one_ct);
208 ++*num_tight;
209 }
210 return;
211 }
212
213 // In this special case, the two constraints below can be merged into an
214 // equality: var = rhs + sum l_i * (value_i - rhs).
215 if (min_not_encoded == max_not_encoded) {
216 const IntegerValue rhs = min_not_encoded;
217 LinearConstraintBuilder encoding_ct(&model, rhs, rhs);
218 encoding_ct.AddTerm(var, IntegerValue(1));
219 for (const auto value_literal : encoding) {
220 CHECK(encoding_ct.AddLiteralTerm(value_literal.literal,
221 rhs - value_literal.value));
222 }
223
224 LinearConstraint lc = encoding_ct.Build();
225 if (!PossibleOverflow(*integer_trail, lc)) {
226 relaxation->at_most_ones.push_back(at_most_one_ct);
227 relaxation->linear_constraints.push_back(std::move(lc));
228 ++*num_tight;
229 }
230 return;
231 }
232
233 // min + sum l_i * (value_i - min) <= var.
234 // Note that this might overflow in corner cases, so we need to prevent that.
235 const IntegerValue d_min = min_not_encoded;
236 LinearConstraintBuilder lower_bound_ct(&model, d_min, kMaxIntegerValue);
237 lower_bound_ct.AddTerm(var, IntegerValue(1));
238 for (const auto value_literal : encoding) {
239 CHECK(lower_bound_ct.AddLiteralTerm(value_literal.literal,
240 d_min - value_literal.value));
241 }
242 LinearConstraint built_lb_ct = lower_bound_ct.Build();
243 if (!PossibleOverflow(*integer_trail, built_lb_ct)) {
244 relaxation->linear_constraints.push_back(std::move(built_lb_ct));
245 ++*num_loose;
246 }
247
248 // var <= max + sum l_i * (value_i - max).
249 // Note that this might overflow in corner cases, so we need to prevent that.
250 const IntegerValue d_max = max_not_encoded;
251 LinearConstraintBuilder upper_bound_ct(&model, kMinIntegerValue, d_max);
252 upper_bound_ct.AddTerm(var, IntegerValue(1));
253 for (const auto value_literal : encoding) {
254 CHECK(upper_bound_ct.AddLiteralTerm(value_literal.literal,
255 d_max - value_literal.value));
256 }
257 LinearConstraint built_ub_ct = upper_bound_ct.Build();
258 if (!PossibleOverflow(*integer_trail, built_ub_ct)) {
259 relaxation->linear_constraints.push_back(std::move(built_ub_ct));
260 ++*num_loose;
261 }
262
263 // Note that empty/trivial constraints will be filtered later.
264 relaxation->at_most_ones.push_back(at_most_one_ct);
265}
266
268 const Model& model,
269 LinearRelaxation* relaxation) {
270 const auto* integer_trail = model.Get<IntegerTrail>();
271 const auto* encoder = model.Get<IntegerEncoder>();
272 if (integer_trail == nullptr || encoder == nullptr) return;
273
274 const auto& greater_than_encoding = encoder->PartialGreaterThanEncoding(var);
275 if (greater_than_encoding.empty()) return;
276
277 // Start by the var >= side.
278 // And also add the implications between used literals.
279 {
280 IntegerValue prev_used_bound = integer_trail->LowerBound(var);
281 LinearConstraintBuilder builder(&model, prev_used_bound, kMaxIntegerValue);
282 builder.AddTerm(var, IntegerValue(1));
283 LiteralIndex prev_literal_index = kNoLiteralIndex;
284 for (const auto entry : greater_than_encoding) {
285 if (entry.value <= prev_used_bound) continue;
286
287 const LiteralIndex literal_index = entry.literal.Index();
288 const IntegerValue diff = prev_used_bound - entry.value;
289
290 // Skip the entry if the literal doesn't have a view.
291 if (!builder.AddLiteralTerm(entry.literal, diff)) continue;
292 if (prev_literal_index != kNoLiteralIndex) {
293 // Add var <= prev_var, which is the same as var + not(prev_var) <= 1
294 relaxation->at_most_ones.push_back(
295 {Literal(literal_index), Literal(prev_literal_index).Negated()});
296 }
297 prev_used_bound = entry.value;
298 prev_literal_index = literal_index;
299 }
300
301 // Note that by construction, this shouldn't be able to overflow.
302 relaxation->linear_constraints.push_back(builder.Build());
303 }
304
305 // Do the same for the var <= side by using NegationOfVar().
306 // Note that we do not need to add the implications between literals again.
307 {
308 IntegerValue prev_used_bound = integer_trail->LowerBound(NegationOf(var));
309 LinearConstraintBuilder builder(&model, prev_used_bound, kMaxIntegerValue);
310 builder.AddTerm(var, IntegerValue(-1));
311 for (const auto entry :
312 encoder->PartialGreaterThanEncoding(NegationOf(var))) {
313 if (entry.value <= prev_used_bound) continue;
314 const IntegerValue diff = prev_used_bound - entry.value;
315
316 // Skip the entry if the literal doesn't have a view.
317 if (!builder.AddLiteralTerm(entry.literal, diff)) continue;
318 prev_used_bound = entry.value;
319 }
320
321 // Note that by construction, this shouldn't be able to overflow.
322 relaxation->linear_constraints.push_back(builder.Build());
323 }
324}
325
326namespace {
327
328bool AllLiteralsHaveViews(const IntegerEncoder& encoder,
329 absl::Span<const Literal> literals) {
330 for (const Literal lit : literals) {
331 if (!encoder.LiteralOrNegationHasView(lit)) return false;
332 }
333 return true;
334}
335
336} // namespace
337
339 LinearRelaxation* relaxation) {
340 auto* mapping = model->GetOrCreate<CpModelMapping>();
341 LinearConstraintBuilder lc(model, IntegerValue(1), kMaxIntegerValue);
342 for (const int enforcement_ref : ct.enforcement_literal()) {
343 CHECK(lc.AddLiteralTerm(mapping->Literal(NegatedRef(enforcement_ref)),
344 IntegerValue(1)));
345 }
346 for (const int ref : ct.bool_or().literals()) {
347 CHECK(lc.AddLiteralTerm(mapping->Literal(ref), IntegerValue(1)));
348 }
349 relaxation->linear_constraints.push_back(lc.Build());
350}
351
353 LinearRelaxation* relaxation,
354 ActivityBoundHelper* activity_helper) {
355 if (!HasEnforcementLiteral(ct)) return;
356
357 // TODO(user): These constraints can be many, and if they are not regrouped
358 // in big at most ones, then they should probably only added lazily as cuts.
359 // Regroup this with future clique-cut separation logic.
360 //
361 // Note that for the case with only one enforcement, what we do below is
362 // already done by the clique merging code.
363 auto* mapping = model->GetOrCreate<CpModelMapping>();
364 if (ct.enforcement_literal().size() == 1) {
365 const Literal enforcement = mapping->Literal(ct.enforcement_literal(0));
366 for (const int ref : ct.bool_and().literals()) {
367 relaxation->at_most_ones.push_back(
368 {enforcement, mapping->Literal(ref).Negated()});
369 }
370 return;
371 }
372
373 // If we have many_literals => many_fixed literal, it is important to
374 // try to use a tight big-M if we can. This is important on neos-957323.pb.gz
375 // for instance.
376 //
377 // We split the literal into disjoint AMO and we encode each with
378 // sum Not(literals) <= sum Not(enforcement)
379 //
380 // Note that what we actually do is use the decomposition into at most one
381 // and add a constraint for each part rather than just adding the sum of them.
382 //
383 // TODO(user): More generally, do not miss the same structure if the bool_and
384 // was expanded into many clauses!
385 //
386 // TODO(user): It is not 100% clear that just not adding one constraint is
387 // worse. Relaxation is worse, but then we have less constraint.
388 LinearConstraintBuilder builder(model);
389 if (activity_helper != nullptr) {
390 std::vector<int> negated_lits;
391 for (const int ref : ct.bool_and().literals()) {
392 negated_lits.push_back(NegatedRef(ref));
393 }
394 for (absl::Span<const int> part :
395 activity_helper->PartitionLiteralsIntoAmo(negated_lits)) {
396 builder.Clear();
397 for (const int negated_ref : part) {
398 CHECK(builder.AddLiteralTerm(mapping->Literal(negated_ref)));
399 }
400 for (const int enforcement_ref : ct.enforcement_literal()) {
401 CHECK(builder.AddLiteralTerm(
402 mapping->Literal(NegatedRef(enforcement_ref)), IntegerValue(-1)));
403 }
404 relaxation->linear_constraints.push_back(
405 builder.BuildConstraint(kMinIntegerValue, IntegerValue(0)));
406 }
407 } else {
408 for (const int ref : ct.bool_and().literals()) {
409 builder.Clear();
410 CHECK(builder.AddLiteralTerm(mapping->Literal(NegatedRef(ref))));
411 for (const int enforcement_ref : ct.enforcement_literal()) {
412 CHECK(builder.AddLiteralTerm(
413 mapping->Literal(NegatedRef(enforcement_ref)), IntegerValue(-1)));
414 }
415 relaxation->linear_constraints.push_back(
416 builder.BuildConstraint(kMinIntegerValue, IntegerValue(0)));
417 }
418 }
419}
420
422 LinearRelaxation* relaxation) {
423 if (HasEnforcementLiteral(ct)) return;
424
425 auto* mapping = model->GetOrCreate<CpModelMapping>();
426 relaxation->at_most_ones.push_back(
427 mapping->Literals(ct.at_most_one().literals()));
428}
429
431 LinearRelaxation* relaxation) {
432 if (HasEnforcementLiteral(ct)) return;
433 auto* mapping = model->GetOrCreate<CpModelMapping>();
434 auto* encoder = model->GetOrCreate<IntegerEncoder>();
435
436 const std::vector<Literal> literals =
437 mapping->Literals(ct.exactly_one().literals());
438 if (AllLiteralsHaveViews(*encoder, literals)) {
439 LinearConstraintBuilder lc(model, IntegerValue(1), IntegerValue(1));
440 for (const Literal lit : literals) {
441 CHECK(lc.AddLiteralTerm(lit, IntegerValue(1)));
442 }
443 relaxation->linear_constraints.push_back(lc.Build());
444 } else {
445 // We just encode the at most one part that might be partially linearized
446 // later.
447 relaxation->at_most_ones.push_back(literals);
448 }
449}
450
452 int num_literals, Model* model, LinearRelaxation* relaxation) {
453 auto* encoder = model->GetOrCreate<IntegerEncoder>();
454
455 if (num_literals == 1) {
456 // This is not supposed to happen, but it is easy enough to cover, just
457 // in case. We might however want to use encoder->GetTrueLiteral().
458 const IntegerVariable var = model->Add(NewIntegerVariable(1, 1));
459 const Literal lit =
460 encoder->GetOrCreateLiteralAssociatedToEquality(var, IntegerValue(1));
461 return {lit};
462 }
463
464 if (num_literals == 2) {
465 const IntegerVariable var = model->Add(NewIntegerVariable(0, 1));
466 const Literal lit =
467 encoder->GetOrCreateLiteralAssociatedToEquality(var, IntegerValue(1));
468
469 // TODO(user): We shouldn't need to create this view ideally. Even better,
470 // we should be able to handle Literal natively in the linear relaxation,
471 // but that is a lot of work.
472 const IntegerVariable var2 = model->Add(NewIntegerVariable(0, 1));
473 encoder->AssociateToIntegerEqualValue(lit.Negated(), var2, IntegerValue(1));
474
475 return {lit, lit.Negated()};
476 }
477
478 std::vector<Literal> literals;
479 LinearConstraintBuilder lc_builder(model, IntegerValue(1), IntegerValue(1));
480 for (int i = 0; i < num_literals; ++i) {
481 const IntegerVariable var = model->Add(NewIntegerVariable(0, 1));
482 const Literal lit =
483 encoder->GetOrCreateLiteralAssociatedToEquality(var, IntegerValue(1));
484 literals.push_back(lit);
485 CHECK(lc_builder.AddLiteralTerm(lit, IntegerValue(1)));
486 }
487 model->Add(ExactlyOneConstraint(literals));
488 relaxation->linear_constraints.push_back(lc_builder.Build());
489 return literals;
490}
491
493 LinearRelaxation* relaxation) {
494 if (HasEnforcementLiteral(ct)) return;
495 auto* mapping = model->GetOrCreate<CpModelMapping>();
496 const int num_arcs = ct.circuit().literals_size();
497 CHECK_EQ(num_arcs, ct.circuit().tails_size());
498 CHECK_EQ(num_arcs, ct.circuit().heads_size());
499
500 // Each node must have exactly one incoming and one outgoing arc (note
501 // that it can be the unique self-arc of this node too).
502 absl::btree_map<int, std::vector<Literal>> incoming_arc_constraints;
503 absl::btree_map<int, std::vector<Literal>> outgoing_arc_constraints;
504 for (int i = 0; i < num_arcs; i++) {
505 const Literal arc = mapping->Literal(ct.circuit().literals(i));
506 const int tail = ct.circuit().tails(i);
507 const int head = ct.circuit().heads(i);
508 outgoing_arc_constraints[tail].push_back(arc);
509 incoming_arc_constraints[head].push_back(arc);
510 }
511 for (const auto* node_map :
512 {&outgoing_arc_constraints, &incoming_arc_constraints}) {
513 for (const auto& entry : *node_map) {
514 const std::vector<Literal>& exactly_one = entry.second;
515 if (exactly_one.size() > 1) {
516 LinearConstraintBuilder at_least_one_lc(model, IntegerValue(1),
518 for (const Literal l : exactly_one) {
519 CHECK(at_least_one_lc.AddLiteralTerm(l, IntegerValue(1)));
520 }
521
522 // We separate the two constraints.
523 relaxation->at_most_ones.push_back(exactly_one);
524 relaxation->linear_constraints.push_back(at_least_one_lc.Build());
525 }
526 }
527 }
528}
529
531 LinearRelaxation* relaxation) {
532 if (HasEnforcementLiteral(ct)) return;
533 auto* mapping = model->GetOrCreate<CpModelMapping>();
534 const int num_arcs = ct.routes().literals_size();
535 CHECK_EQ(num_arcs, ct.routes().tails_size());
536 CHECK_EQ(num_arcs, ct.routes().heads_size());
537
538 // Each node except node zero must have exactly one incoming and one outgoing
539 // arc (note that it can be the unique self-arc of this node too). For node
540 // zero, the number of incoming arcs should be the same as the number of
541 // outgoing arcs.
542 absl::btree_map<int, std::vector<Literal>> incoming_arc_constraints;
543 absl::btree_map<int, std::vector<Literal>> outgoing_arc_constraints;
544 for (int i = 0; i < num_arcs; i++) {
545 const Literal arc = mapping->Literal(ct.routes().literals(i));
546 const int tail = ct.routes().tails(i);
547 const int head = ct.routes().heads(i);
548 outgoing_arc_constraints[tail].push_back(arc);
549 incoming_arc_constraints[head].push_back(arc);
550 }
551 for (const auto* node_map :
552 {&outgoing_arc_constraints, &incoming_arc_constraints}) {
553 for (const auto& entry : *node_map) {
554 if (entry.first == 0) continue;
555 const std::vector<Literal>& exactly_one = entry.second;
556 if (exactly_one.size() > 1) {
557 LinearConstraintBuilder at_least_one_lc(model, IntegerValue(1),
559 for (const Literal l : exactly_one) {
560 CHECK(at_least_one_lc.AddLiteralTerm(l, IntegerValue(1)));
561 }
562
563 // We separate the two constraints.
564 relaxation->at_most_ones.push_back(exactly_one);
565 relaxation->linear_constraints.push_back(at_least_one_lc.Build());
566 }
567 }
568 }
569 LinearConstraintBuilder zero_node_balance_lc(model, IntegerValue(0),
570 IntegerValue(0));
571 for (const Literal& incoming_arc : incoming_arc_constraints[0]) {
572 CHECK(zero_node_balance_lc.AddLiteralTerm(incoming_arc, IntegerValue(1)));
573 }
574 for (const Literal& outgoing_arc : outgoing_arc_constraints[0]) {
575 CHECK(zero_node_balance_lc.AddLiteralTerm(outgoing_arc, IntegerValue(-1)));
576 }
577 relaxation->linear_constraints.push_back(zero_node_balance_lc.Build());
578}
579
581 LinearRelaxation* relaxation) {
582 std::vector<int> tails(ct.circuit().tails().begin(),
583 ct.circuit().tails().end());
584 std::vector<int> heads(ct.circuit().heads().begin(),
585 ct.circuit().heads().end());
586 auto* mapping = m->GetOrCreate<CpModelMapping>();
587 std::vector<Literal> literals = mapping->Literals(ct.circuit().literals());
588 const int num_nodes = ReindexArcs(&tails, &heads);
589
591 num_nodes, tails, heads, literals, m));
592}
593
595 LinearRelaxation* relaxation) {
596 std::vector<int> tails(ct.routes().tails().begin(),
597 ct.routes().tails().end());
598 std::vector<int> heads(ct.routes().heads().begin(),
599 ct.routes().heads().end());
600 auto* mapping = m->GetOrCreate<CpModelMapping>();
601 std::vector<Literal> literals = mapping->Literals(ct.routes().literals());
602
603 int num_nodes = 0;
604 for (int i = 0; i < ct.routes().tails_size(); ++i) {
605 num_nodes = std::max(num_nodes, 1 + ct.routes().tails(i));
606 num_nodes = std::max(num_nodes, 1 + ct.routes().heads(i));
607 }
608 const int num_dimensions = ct.routes().dimensions_size();
609 if (num_dimensions == 0) {
610 relaxation->cut_generators.push_back(
611 CreateStronglyConnectedGraphCutGenerator(num_nodes, tails, heads,
612 literals, m));
613 } else {
614 std::vector<AffineExpression> flat_node_dim_expressions(
615 num_dimensions * num_nodes, AffineExpression());
616 for (int d = 0; d < num_dimensions; ++d) {
617 const auto& node_exprs = ct.routes().dimensions(d).exprs();
618 for (int n = 0; n < node_exprs.size(); ++n) {
619 const LinearExpressionProto& expr = node_exprs[n];
620 AffineExpression& node_expr =
621 flat_node_dim_expressions[n * num_dimensions + d];
622 if (expr.vars().empty()) {
623 node_expr = AffineExpression(IntegerValue(expr.offset()));
624 continue;
625 }
626 DCHECK_EQ(expr.vars_size(), 1);
627 node_expr = AffineExpression(mapping->Integer(expr.vars(0)),
628 expr.coeffs(0), expr.offset());
629 }
630 }
631 relaxation->cut_generators.push_back(CreateCVRPCutGenerator(
632 num_nodes, tails, heads, literals, flat_node_dim_expressions, m));
633 }
634}
635
636// Scan the intervals of a cumulative/no_overlap constraint, and its capacity (1
637// for the no_overlap). It returns the index of the makespan interval if found,
638// or std::nullopt otherwise.
639//
640// Currently, this requires the capacity to be fixed in order to scan for a
641// makespan interval.
642//
643// The makespan interval has the following property:
644// - its end is fixed at the horizon
645// - it is always present
646// - its demand is the capacity of the cumulative/no_overlap.
647// - its size is > 0.
648//
649// These property ensures that all other intervals ends before the start of
650// the makespan interval.
651std::optional<int> DetectMakespan(absl::Span<const IntervalVariable> intervals,
652 absl::Span<const AffineExpression> demands,
653 const AffineExpression& capacity,
654 Model* model) {
655 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
657
658 // TODO(user): Supports variable capacity.
659 if (!integer_trail->IsFixed(capacity)) {
660 return std::nullopt;
661 }
662
663 // Detect the horizon (max of all end max of all intervals).
664 IntegerValue horizon = kMinIntegerValue;
665 for (int i = 0; i < intervals.size(); ++i) {
666 if (repository->IsAbsent(intervals[i])) continue;
667 horizon = std::max(
668 horizon, integer_trail->UpperBound(repository->End(intervals[i])));
669 }
670
671 const IntegerValue capacity_value = integer_trail->FixedValue(capacity);
672 for (int i = 0; i < intervals.size(); ++i) {
673 if (!repository->IsPresent(intervals[i])) continue;
674 const AffineExpression& end = repository->End(intervals[i]);
675 if (integer_trail->IsFixed(demands[i]) &&
676 integer_trail->FixedValue(demands[i]) == capacity_value &&
677 integer_trail->IsFixed(end) &&
678 integer_trail->FixedValue(end) == horizon &&
679 integer_trail->LowerBound(repository->Size(intervals[i])) > 0) {
680 return i;
681 }
682 }
683 return std::nullopt;
684}
685
686namespace {
687
688std::optional<AffineExpression> DetectMakespanFromPrecedences(
689 const SchedulingConstraintHelper& helper, Model* model) {
690 if (helper.NumTasks() == 0) return {};
691
692 const absl::Span<const AffineExpression> ends = helper.Ends();
693 std::vector<IntegerVariable> end_vars;
694 for (const AffineExpression& end : ends) {
695 // TODO(user): Deal with constant end.
696 if (end.var == kNoIntegerVariable) return {};
697 if (end.coeff != 1) return {};
698 end_vars.push_back(end.var);
699 }
700
701 std::vector<FullIntegerPrecedence> output;
702 auto* precedences = model->GetOrCreate<PrecedenceRelations>();
703 precedences->ComputeFullPrecedences(end_vars, &output);
704 for (const auto& p : output) {
705 // TODO(user): What if we have more than one candidate makespan ?
706 if (p.indices.size() != ends.size()) continue;
707
708 // We have a Makespan!
709 // We want p.var - min_delta >= max(end).
710 IntegerValue min_delta = kMaxIntegerValue;
711 for (int i = 0; i < p.indices.size(); ++i) {
712 // end_vars[indices[i]] + p.offset[i] <= p.var
713 // [interval_end - end_offset][indices[i]] + p.offset[i] <= p.var
714 //
715 // TODO(user): It is possible this min_delta becomes positive but for a
716 // real makespan, we could make sure it is <= 0. This can happen if we
717 // have an optional interval because we didn't compute the offset assuming
718 // this interval was present. We could potentially fix it if we know that
719 // presence_literal => p.var >= end.
720 min_delta =
721 std::min(min_delta, p.offsets[i] - ends[p.indices[i]].constant);
722 }
723 VLOG(2) << "Makespan detected >= ends + " << min_delta;
724 return AffineExpression(p.var, IntegerValue(1), -min_delta);
725 }
726
727 return {};
728}
729
730} // namespace
731
733 Model* model,
734 LinearRelaxation* relaxation) {
735 if (HasEnforcementLiteral(ct)) return;
736
737 auto* mapping = model->GetOrCreate<CpModelMapping>();
738 std::vector<IntervalVariable> intervals =
739 mapping->Intervals(ct.no_overlap().intervals());
740 const IntegerValue one(1);
741 std::vector<AffineExpression> demands(intervals.size(), one);
743
744 std::optional<AffineExpression> makespan;
745 const std::optional<int> makespan_index =
746 DetectMakespan(intervals, demands, /*capacity=*/one, model);
747 if (makespan_index.has_value()) {
748 makespan = repository->Start(intervals[makespan_index.value()]);
749 demands.pop_back(); // the vector is filled with ones.
750 intervals.erase(intervals.begin() + makespan_index.value());
751 }
752
753 SchedulingConstraintHelper* helper = repository->GetOrCreateHelper(intervals);
754 if (!helper->SynchronizeAndSetTimeDirection(true)) return;
755 SchedulingDemandHelper* demands_helper =
756 repository->GetOrCreateDemandHelper(helper, demands);
757
758 if (!makespan.has_value()) {
759 makespan = DetectMakespanFromPrecedences(*helper, model);
760 }
761
762 AddCumulativeRelaxation(/*capacity=*/one, helper, demands_helper, makespan,
763 model, relaxation);
764 if (model->GetOrCreate<SatParameters>()->linearization_level() > 1) {
765 AddNoOverlapCutGenerator(helper, makespan, model, relaxation);
766 }
767}
768
770 Model* model,
771 LinearRelaxation* relaxation) {
772 if (HasEnforcementLiteral(ct)) return;
773 auto* mapping = model->GetOrCreate<CpModelMapping>();
774 std::vector<IntervalVariable> intervals =
775 mapping->Intervals(ct.cumulative().intervals());
776 std::vector<AffineExpression> demands =
777 mapping->Affines(ct.cumulative().demands());
778 const AffineExpression capacity = mapping->Affine(ct.cumulative().capacity());
779 const std::optional<int> makespan_index =
780 DetectMakespan(intervals, demands, capacity, model);
781 std::optional<AffineExpression> makespan;
783 if (makespan_index.has_value()) {
784 // We remove the makespan data from the intervals the demands vector.
785 makespan = repository->Start(intervals[makespan_index.value()]);
786 demands.erase(demands.begin() + makespan_index.value());
787 intervals.erase(intervals.begin() + makespan_index.value());
788 }
789
790 // We try to linearize the energy of each task (size * demand).
791 SchedulingConstraintHelper* helper = repository->GetOrCreateHelper(intervals);
792 if (!helper->SynchronizeAndSetTimeDirection(true)) return;
793 SchedulingDemandHelper* demands_helper =
794 repository->GetOrCreateDemandHelper(helper, demands);
795
796 if (!makespan.has_value()) {
797 makespan = DetectMakespanFromPrecedences(*helper, model);
798 }
799
800 // We can now add the relaxation and the cut generators.
801 AddCumulativeRelaxation(capacity, helper, demands_helper, makespan, model,
802 relaxation);
803 if (model->GetOrCreate<SatParameters>()->linearization_level() > 1) {
804 AddCumulativeCutGenerator(capacity, helper, demands_helper, makespan, model,
805 relaxation);
806 }
807}
808
809// This relaxation will compute the bounding box of all tasks in the cumulative,
810// and add the constraint that the sum of energies of each task must fit in the
811// capacity * span area.
814 SchedulingDemandHelper* demands_helper,
815 const std::optional<AffineExpression>& makespan,
816 Model* model, LinearRelaxation* relaxation) {
817 const int num_intervals = helper->NumTasks();
818 if (!demands_helper->CacheAllEnergyValues()) return;
819
820 IntegerValue min_of_starts = kMaxIntegerValue;
821 IntegerValue max_of_ends = kMinIntegerValue;
822 int num_variable_energies = 0;
823 int num_optionals = 0;
824 int64_t sizes_gcd = 0;
825 int64_t demands_gcd = 0;
826 int64_t num_active_intervals = 0;
827 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
828 for (int index = 0; index < num_intervals; ++index) {
829 if (helper->IsAbsent(index)) continue;
830 if (helper->SizeMax(index) == 0 || demands_helper->DemandMax(index) == 0) {
831 continue;
832 }
833
834 if (helper->IsOptional(index)) {
835 if (demands_helper->EnergyMin(index) > 0) {
836 num_optionals++;
837 } else {
838 continue;
839 }
840 }
841
842 if (!helper->SizeIsFixed(index) || !demands_helper->DemandIsFixed(index)) {
843 num_variable_energies++;
844 }
845 if (sizes_gcd != 1) {
846 if (helper->SizeIsFixed(index)) {
847 sizes_gcd = std::gcd(helper->SizeMin(index).value(), sizes_gcd);
848 } else {
849 sizes_gcd = 1;
850 }
851 }
852 if (demands_gcd != 1) {
853 if (demands_helper->DemandIsFixed(index)) {
854 demands_gcd =
855 std::gcd(demands_helper->DemandMin(index).value(), demands_gcd);
856 } else {
857 demands_gcd = 1;
858 }
859 }
860 num_active_intervals++;
861 min_of_starts = std::min(min_of_starts, helper->StartMin(index));
862 max_of_ends = std::max(max_of_ends, helper->EndMax(index));
863 }
864
865 VLOG(2) << "Span [" << min_of_starts << ".." << max_of_ends << "] with "
866 << num_optionals << " optional intervals, and "
867 << num_variable_energies << " variable energy tasks out of "
868 << num_active_intervals << "/" << num_intervals << " intervals"
869 << (makespan.has_value() ? ", and 1 makespan" : "")
870 << " sizes_gcd: " << sizes_gcd << " demands_gcd: " << demands_gcd;
871
872 // There are no active intervals, no need to add the relaxation.
873 if (num_active_intervals == 0) return;
874
875 // If nothing is variable, and the coefficients cannot be reduced, the linear
876 // relaxation will already be enforced by the scheduling propagators.
877 if (num_variable_energies + num_optionals == 0 && sizes_gcd == 1 &&
878 demands_gcd == 1) {
879 return;
880 }
881
882 // Specialized case 1: sizes are fixed with a non 1 gcd and no makespan.
883 if (sizes_gcd != 1 && !makespan.has_value()) {
884 VLOG(2) << "Cumulative relaxation: sizes_gcd = " << sizes_gcd
885 << ", demands_gcd = " << demands_gcd
886 << ", no makespan, capacity is " << capacity.DebugString();
887 // We can simplify the capacity only if it is fixed.
888 // TODO(user): We could use (capacity / demands_gcd) * demands_gcd.
889 if (!integer_trail->IsFixed(capacity)) demands_gcd = 1;
890 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
891 for (int index = 0; index < num_intervals; ++index) {
892 if (helper->IsAbsent(index)) continue;
893 if (helper->SizeMax(index) == 0 ||
894 demands_helper->DemandMax(index) == 0) {
895 continue;
896 }
897
898 if (helper->IsOptional(index)) {
899 const IntegerValue energy_min = demands_helper->EnergyMin(index);
900 if (energy_min == 0) continue;
901 DCHECK_EQ(energy_min % (sizes_gcd * demands_gcd), 0);
902 if (!lc.AddLiteralTerm(helper->PresenceLiteral(index),
903 energy_min / sizes_gcd / demands_gcd)) {
904 return;
905 }
906 } else {
907 // Copy the decomposed energy.
908 std::vector<LiteralValueValue> product =
909 demands_helper->DecomposedEnergies()[index];
910 if (!product.empty()) {
911 // The energy is defined if the vector is not empty.
912 // Let's reduce the coefficients.
913 for (LiteralValueValue& entry : product) {
914 DCHECK_EQ(entry.left_value % sizes_gcd, 0);
915 entry.left_value /= sizes_gcd;
916 DCHECK_EQ(entry.right_value % demands_gcd, 0);
917 entry.right_value /= demands_gcd;
918 }
919 if (!lc.AddDecomposedProduct(product)) return;
920 } else {
921 // We know the size is fixed.
922 const IntegerValue local_size =
923 integer_trail->FixedValue(helper->Sizes()[index]);
924 DCHECK_EQ(local_size % sizes_gcd, 0);
925 if (demands_gcd == 1) {
926 lc.AddTerm(demands_helper->Demands()[index],
927 local_size / sizes_gcd);
928 } else {
929 const IntegerValue local_demand =
930 integer_trail->FixedValue(demands_helper->Demands()[index]);
931 DCHECK_EQ(local_demand % demands_gcd, 0);
932 lc.AddConstant(local_size * local_demand / sizes_gcd / demands_gcd);
933 }
934 }
935 }
936 }
937
938 // Add the available energy of the cumulative.
939 if (integer_trail->IsFixed(capacity)) {
940 const IntegerValue span = max_of_ends - min_of_starts;
941 const IntegerValue fixed_capacity = integer_trail->FixedValue(capacity);
942 lc.AddConstant(
943 -MathUtil::FloorOfRatio(fixed_capacity.value(), demands_gcd) *
944 MathUtil::FloorOfRatio(span.value(), sizes_gcd));
945 } else {
946 DCHECK_EQ(demands_gcd, 1);
947 lc.AddTerm(capacity, -(max_of_ends - min_of_starts) / sizes_gcd);
948 }
949 relaxation->linear_constraints.push_back(lc.Build());
950 return;
951 }
952
953 // TODO(user): Implement demands_gcd != 1 && capacity is fixed.
954
955 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
956 for (int index = 0; index < num_intervals; ++index) {
957 if (helper->IsAbsent(index)) continue;
958 if (helper->IsOptional(index)) {
959 const IntegerValue energy_min = demands_helper->EnergyMin(index);
960 if (energy_min == 0) continue;
961 if (!lc.AddLiteralTerm(helper->PresenceLiteral(index), energy_min)) {
962 return;
963 }
964 } else {
965 const std::vector<LiteralValueValue>& product =
966 demands_helper->DecomposedEnergies()[index];
967 if (!product.empty()) {
968 // The energy is defined if the vector is not empty.
969 if (!lc.AddDecomposedProduct(product)) return;
970 } else {
971 // The energy is not a decomposed product, but it could still be
972 // constant or linear. If not, a McCormick relaxation will be
973 // introduced. AddQuadraticLowerBound() supports all cases.
974 lc.AddQuadraticLowerBound(helper->Sizes()[index],
975 demands_helper->Demands()[index],
976 integer_trail);
977 }
978 }
979 }
980
981 // Create and link span_start and span_end to the starts and ends of the
982 // tasks.
983 //
984 // TODO(user): In some cases, we could have only one task that can be
985 // first.
986 IntegerValue max_for_overflow_check = std::max(-min_of_starts, max_of_ends);
987 if (makespan.has_value()) {
988 max_for_overflow_check = std::max(
989 max_for_overflow_check, integer_trail->UpperBound(makespan.value()));
990 }
991 if (ProdOverflow(max_for_overflow_check,
992 integer_trail->UpperBound(capacity))) {
993 return;
994 }
995 const AffineExpression span_start = min_of_starts;
996 const AffineExpression span_end =
997 makespan.has_value() ? makespan.value() : max_of_ends;
998 lc.AddTerm(span_end, -integer_trail->UpperBound(capacity));
999 lc.AddTerm(span_start, integer_trail->UpperBound(capacity));
1000 relaxation->linear_constraints.push_back(lc.Build());
1001}
1003 absl::Span<const int> component, Model* model,
1004 NoOverlap2DConstraintHelper* no_overlap_helper,
1005 LinearConstraintManager* manager, ProductDecomposer* product_decomposer) {
1006 std::optional<Rectangle> bounding_box;
1007 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1008 for (const int b : component) {
1009 const Rectangle curr_bounding_box =
1010 no_overlap_helper->GetLevelZeroBoundingRectangle(b);
1011 if (curr_bounding_box.x_min > curr_bounding_box.x_max ||
1012 curr_bounding_box.y_min > curr_bounding_box.y_max) {
1013 // This can happen if the box must be absent.
1014 continue;
1015 }
1016 if (bounding_box.has_value()) {
1017 bounding_box->GrowToInclude(
1018 no_overlap_helper->GetLevelZeroBoundingRectangle(b));
1019 } else {
1020 bounding_box = no_overlap_helper->GetLevelZeroBoundingRectangle(b);
1021 }
1022 }
1023
1024 if (!bounding_box.has_value()) {
1025 // All boxes must be absent.
1026 return;
1027 }
1028
1029 const IntegerValue max_area = bounding_box->CapArea();
1030 if (max_area == kMaxIntegerValue) return;
1031
1032 LinearConstraintBuilder lc(model, IntegerValue(0), max_area);
1033 for (const int b : component) {
1034 if (no_overlap_helper->IsPresent(b)) {
1035 const AffineExpression& x_size_affine =
1036 no_overlap_helper->x_helper().Sizes()[b];
1037 const AffineExpression& y_size_affine =
1038 no_overlap_helper->y_helper().Sizes()[b];
1039 const std::vector<LiteralValueValue> energy =
1040 product_decomposer->TryToDecompose(x_size_affine, y_size_affine);
1041 if (!energy.empty()) {
1042 if (!lc.AddDecomposedProduct(energy)) return;
1043 } else {
1044 lc.AddQuadraticLowerBound(x_size_affine, y_size_affine, integer_trail);
1045 }
1046 } else if (no_overlap_helper->x_helper().IsPresent(b) ||
1047 no_overlap_helper->y_helper().IsPresent(b) ||
1048 (no_overlap_helper->x_helper().PresenceLiteral(b) ==
1049 no_overlap_helper->y_helper().PresenceLiteral(b))) {
1050 // We have only one active literal.
1051 const Literal presence_literal =
1052 no_overlap_helper->x_helper().IsPresent(b)
1053 ? no_overlap_helper->y_helper().PresenceLiteral(b)
1054 : no_overlap_helper->x_helper().PresenceLiteral(b);
1055 const auto& [x_size, y_size] =
1056 no_overlap_helper->GetLevelZeroBoxSizesMin(b);
1057 const IntegerValue area_min = x_size * y_size;
1058 if (area_min > 0) {
1059 // Not including the term if we don't have a view is ok.
1060 (void)lc.AddLiteralTerm(presence_literal, area_min);
1061 }
1062 }
1063 }
1064 LinearConstraint ct = lc.Build();
1065 if (ct.num_terms == 0) return;
1066 manager->Add(std::move(ct));
1067}
1068
1069// Adds the energetic relaxation sum(areas) <= bounding box area.
1071 LinearRelaxation* relaxation) {
1072 CHECK(ct.has_no_overlap_2d());
1073 if (HasEnforcementLiteral(ct)) return;
1074
1075 auto* mapping = model->GetOrCreate<CpModelMapping>();
1076 std::vector<IntervalVariable> x_intervals =
1077 mapping->Intervals(ct.no_overlap_2d().x_intervals());
1078 std::vector<IntervalVariable> y_intervals =
1079 mapping->Intervals(ct.no_overlap_2d().y_intervals());
1080
1081 auto* intervals_repository = model->GetOrCreate<IntervalsRepository>();
1082 NoOverlap2DConstraintHelper* no_overlap_helper =
1083 intervals_repository->GetOrCreate2DHelper(x_intervals, y_intervals);
1084 auto* product_decomposer = model->GetOrCreate<ProductDecomposer>();
1085
1086 CutGenerator& result = relaxation->cut_generators.emplace_back();
1087 result.only_run_at_level_zero = true;
1088
1090 &no_overlap_helper->x_helper(), model, &result.vars,
1093 &no_overlap_helper->y_helper(), model, &result.vars,
1095 result.generate_cuts = [no_overlap_helper, model, product_decomposer,
1096 last_level_zero_bound_change_idx = int64_t{-1}](
1097 LinearConstraintManager* manager) mutable {
1098 if (last_level_zero_bound_change_idx ==
1099 no_overlap_helper->LastLevelZeroChangeIdx()) {
1100 return true;
1101 }
1102 last_level_zero_bound_change_idx =
1103 no_overlap_helper->LastLevelZeroChangeIdx();
1104 for (const auto& component :
1105 no_overlap_helper->connected_components().AsVectorOfSpan()) {
1107 component, model, no_overlap_helper, manager, product_decomposer);
1108 }
1109 return true;
1110 };
1111}
1112
1114 LinearRelaxation* relaxation) {
1115 auto* mapping = model->GetOrCreate<CpModelMapping>();
1116
1117 // We want to linearize target = max(exprs[1], exprs[2], ..., exprs[d]).
1118 // Part 1: Encode target >= max(exprs[1], exprs[2], ..., exprs[d])
1119 const LinearExpression negated_target =
1120 NegationOf(mapping->GetExprFromProto(ct.lin_max().target()));
1121 for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
1122 const LinearExpression expr =
1123 mapping->GetExprFromProto(ct.lin_max().exprs(i));
1124 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
1125 lc.AddLinearExpression(negated_target);
1126 lc.AddLinearExpression(expr);
1127 relaxation->linear_constraints.push_back(lc.Build());
1128 }
1129}
1130
1131// TODO(user): experiment with:
1132// 1) remove this code
1133// 2) keep this code
1134// 3) remove this code and create the cut generator at level 1.
1136 LinearRelaxation* relaxation) {
1137 IntegerVariable var;
1138 std::vector<std::pair<IntegerValue, IntegerValue>> affines;
1139 auto* mapping = model->GetOrCreate<CpModelMapping>();
1140 CollectAffineExpressionWithSingleVariable(ct, mapping, &var, &affines);
1141 if (var == kNoIntegerVariable ||
1142 model->GetOrCreate<IntegerTrail>()->IsFixed(var)) {
1143 return;
1144 }
1145
1146 CHECK(VariableIsPositive(var));
1147 const LinearExpression target_expr =
1148 PositiveVarExpr(mapping->GetExprFromProto(ct.lin_max().target()));
1149 LinearConstraintBuilder builder(model);
1150 if (BuildMaxAffineUpConstraint(target_expr, var, affines, model, &builder)) {
1151 relaxation->linear_constraints.push_back(builder.Build());
1152 }
1153}
1154
1156 LinearRelaxation* relaxation) {
1157 IntegerVariable var;
1158 std::vector<std::pair<IntegerValue, IntegerValue>> affines;
1159 auto* mapping = model->GetOrCreate<CpModelMapping>();
1160 CollectAffineExpressionWithSingleVariable(ct, mapping, &var, &affines);
1161 if (var == kNoIntegerVariable ||
1162 model->GetOrCreate<IntegerTrail>()->IsFixed(var)) {
1163 return;
1164 }
1165
1166 // If the target is constant, propagation is enough.
1167 if (ct.lin_max().target().vars().empty()) return;
1168
1169 const LinearExpression target_expr =
1170 PositiveVarExpr(mapping->GetExprFromProto(ct.lin_max().target()));
1171 relaxation->cut_generators.push_back(CreateMaxAffineCutGenerator(
1172 target_expr, var, affines, "AffineMax", model));
1173}
1174
1175// Part 2: Encode upper bound on X.
1176//
1177// Add linking constraint to the CP solver
1178// sum zi = 1 and for all i, zi => max = expr_i.
1179void AppendLinMaxRelaxationPart2(IntegerVariable target,
1180 absl::Span<const Literal> alternative_literals,
1181 absl::Span<const LinearExpression> exprs,
1182 Model* model, LinearRelaxation* relaxation) {
1183 const int num_exprs = exprs.size();
1185
1186 // First add the CP constraints.
1187 for (int i = 0; i < num_exprs; ++i) {
1188 LinearExpression local_expr;
1189 local_expr.vars = NegationOf(exprs[i].vars);
1190 local_expr.vars.push_back(target);
1191 local_expr.coeffs = exprs[i].coeffs;
1192 local_expr.coeffs.push_back(IntegerValue(1));
1193 IntegerSumLE* upper_bound =
1194 new IntegerSumLE({alternative_literals[i]}, local_expr.vars,
1195 local_expr.coeffs, exprs[i].offset, model);
1196 upper_bound->RegisterWith(watcher);
1197 model->TakeOwnership(upper_bound);
1198 }
1199
1200 // For the relaxation, we use different constraints with a stronger linear
1201 // relaxation as explained in the .h
1202 std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
1203 num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
1204
1205 // Cache coefficients.
1206 // TODO(user): Remove hash_map ?
1207 absl::flat_hash_map<std::pair<int, IntegerVariable>, IntegerValue> cache;
1208 for (int i = 0; i < num_exprs; ++i) {
1209 for (int j = 0; j < exprs[i].vars.size(); ++j) {
1210 cache[std::make_pair(i, exprs[i].vars[j])] = exprs[i].coeffs[j];
1211 }
1212 }
1213 const auto get_coeff = [&cache](IntegerVariable var, int index) {
1214 const auto it = cache.find(std::make_pair(index, var));
1215 if (it == cache.end()) return IntegerValue(0);
1216 return it->second;
1217 };
1218
1219 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
1220 std::vector<IntegerVariable> active_vars;
1221 for (int i = 0; i + 1 < num_exprs; ++i) {
1222 for (int j = i + 1; j < num_exprs; ++j) {
1223 active_vars = exprs[i].vars;
1224 active_vars.insert(active_vars.end(), exprs[j].vars.begin(),
1225 exprs[j].vars.end());
1226 gtl::STLSortAndRemoveDuplicates(&active_vars);
1227 for (const IntegerVariable x_var : active_vars) {
1228 const IntegerValue diff = get_coeff(x_var, j) - get_coeff(x_var, i);
1229 if (diff == 0) continue;
1230
1231 const IntegerValue lb = integer_trail->LevelZeroLowerBound(x_var);
1232 const IntegerValue ub = integer_trail->LevelZeroUpperBound(x_var);
1233 sum_of_max_corner_diff[i][j] += std::max(diff * lb, diff * ub);
1234 sum_of_max_corner_diff[j][i] += std::max(-diff * lb, -diff * ub);
1235 }
1236 }
1237 }
1238
1239 for (int i = 0; i < num_exprs; ++i) {
1240 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
1241 lc.AddTerm(target, IntegerValue(1));
1242 for (int j = 0; j < exprs[i].vars.size(); ++j) {
1243 lc.AddTerm(exprs[i].vars[j], -exprs[i].coeffs[j]);
1244 }
1245 for (int j = 0; j < num_exprs; ++j) {
1246 CHECK(lc.AddLiteralTerm(alternative_literals[j],
1247 -exprs[j].offset - sum_of_max_corner_diff[i][j]));
1248 }
1249 relaxation->linear_constraints.push_back(lc.Build());
1250 }
1251}
1252
1254 bool linearize_enforced_constraints,
1255 Model* model,
1256 LinearRelaxation* relaxation,
1257 ActivityBoundHelper* activity_helper) {
1258 auto* mapping = model->Get<CpModelMapping>();
1259
1260 // Note that we ignore the holes in the domain.
1261 //
1262 // TODO(user): In LoadLinearConstraint() we already created intermediate
1263 // Booleans for each disjoint interval, we should reuse them here if
1264 // possible.
1265 //
1266 // TODO(user): process the "at most one" part of a == 1 separately?
1267 const IntegerValue rhs_domain_min = IntegerValue(ct.linear().domain(0));
1268 const IntegerValue rhs_domain_max =
1269 IntegerValue(ct.linear().domain(ct.linear().domain_size() - 1));
1270 if (rhs_domain_min == std::numeric_limits<int64_t>::min() &&
1271 rhs_domain_max == std::numeric_limits<int64_t>::max())
1272 return;
1273
1274 if (!HasEnforcementLiteral(ct)) {
1275 LinearConstraintBuilder lc(model, rhs_domain_min, rhs_domain_max);
1276 for (int i = 0; i < ct.linear().vars_size(); i++) {
1277 const int ref = ct.linear().vars(i);
1278 const int64_t coeff = ct.linear().coeffs(i);
1279 lc.AddTerm(mapping->Integer(ref), IntegerValue(coeff));
1280 }
1281 relaxation->linear_constraints.push_back(lc.Build());
1282 return;
1283 }
1284
1285 // Reified version.
1286 if (!linearize_enforced_constraints) return;
1287
1288 // We linearize fully reified constraints of size 1 all together for a given
1289 // variable. But we need to process half-reified ones or constraint with
1290 // more than one enforcement.
1291 //
1292 // TODO(user): Use cleaner "already loaded" logic, and mark as such constraint
1293 // already encoded by code like AppendRelaxationForEqualityEncoding().
1294 if (!mapping->IsHalfEncodingConstraint(&ct) && ct.linear().vars_size() <= 1 &&
1295 ct.enforcement_literal().size() <= 1) {
1296 return;
1297 }
1298
1299 std::vector<Literal> enforcing_literals;
1300 enforcing_literals.reserve(ct.enforcement_literal_size());
1301 for (const int enforcement_ref : ct.enforcement_literal()) {
1302 enforcing_literals.push_back(mapping->Literal(enforcement_ref));
1303 }
1304
1305 // Compute min/max activity.
1306 std::vector<std::pair<int, int64_t>> bool_terms;
1307 IntegerValue min_activity(0);
1308 IntegerValue max_activity(0);
1309 const auto integer_trail = model->GetOrCreate<IntegerTrail>();
1310 for (int i = 0; i < ct.linear().vars_size(); i++) {
1311 const int ref = ct.linear().vars(i);
1312 const IntegerValue coeff(ct.linear().coeffs(i));
1313 const IntegerVariable int_var = mapping->Integer(ref);
1314
1315 // Everything here should have a view.
1316 CHECK_NE(int_var, kNoIntegerVariable);
1317
1318 const IntegerValue lb = integer_trail->LowerBound(int_var);
1319 const IntegerValue ub = integer_trail->UpperBound(int_var);
1320 if (lb == 0 && ub == 1 && activity_helper != nullptr) {
1321 bool_terms.push_back({ref, coeff.value()});
1322 } else {
1323 if (coeff > 0) {
1324 min_activity += coeff * lb;
1325 max_activity += coeff * ub;
1326 } else {
1327 min_activity += coeff * ub;
1328 max_activity += coeff * lb;
1329 }
1330 }
1331 }
1332 if (activity_helper != nullptr) {
1333 min_activity +=
1334 IntegerValue(activity_helper->ComputeMinActivity(bool_terms));
1335 max_activity +=
1336 IntegerValue(activity_helper->ComputeMaxActivity(bool_terms));
1337 }
1338
1339 if (rhs_domain_min > min_activity) {
1340 // And(ei) => terms >= rhs_domain_min
1341 // <=> Sum_i (~ei * (rhs_domain_min - min_activity)) + terms >=
1342 // rhs_domain_min
1343 LinearConstraintBuilder lc(model, rhs_domain_min, kMaxIntegerValue);
1344 const IntegerValue term = CapSubI(rhs_domain_min, min_activity);
1345 if (AtMinOrMaxInt64I(term) && !enforcing_literals.empty()) return;
1346 for (const Literal& literal : enforcing_literals) {
1347 CHECK(lc.AddLiteralTerm(literal.Negated(), term));
1348 }
1349 for (int i = 0; i < ct.linear().vars_size(); i++) {
1350 const int ref = ct.linear().vars(i);
1351 const IntegerValue coeff(ct.linear().coeffs(i));
1352 const IntegerVariable int_var = mapping->Integer(ref);
1353 lc.AddTerm(int_var, coeff);
1354 }
1355 LinearConstraint built_ct = lc.Build();
1356 if (!PossibleOverflow(*integer_trail, built_ct)) {
1357 relaxation->linear_constraints.push_back(std::move(built_ct));
1358 }
1359 }
1360 if (rhs_domain_max < max_activity) {
1361 // And(ei) => terms <= rhs_domain_max
1362 // <=> Sum_i (~ei * (rhs_domain_max - max_activity)) + terms <=
1363 // rhs_domain_max
1364 LinearConstraintBuilder lc(model, kMinIntegerValue, rhs_domain_max);
1365 const IntegerValue term = CapSubI(rhs_domain_max, max_activity);
1366 if (AtMinOrMaxInt64I(term) && !enforcing_literals.empty()) return;
1367 for (const Literal& literal : enforcing_literals) {
1368 CHECK(lc.AddLiteralTerm(literal.Negated(), term));
1369 }
1370 for (int i = 0; i < ct.linear().vars_size(); i++) {
1371 const int ref = ct.linear().vars(i);
1372 const IntegerValue coeff(ct.linear().coeffs(i));
1373 const IntegerVariable int_var = mapping->Integer(ref);
1374 lc.AddTerm(int_var, coeff);
1375 }
1376 LinearConstraint built_ct = lc.Build();
1377 if (!PossibleOverflow(*integer_trail, built_ct)) {
1378 relaxation->linear_constraints.push_back(std::move(built_ct));
1379 }
1380 }
1381}
1382
1383// Add a static and a dynamic linear relaxation of the CP constraint to the set
1384// of linear constraints. The highest linearization_level is, the more types of
1385// constraint we encode. This method should be called only for
1386// linearization_level > 0. The static part is just called a relaxation and is
1387// called at the root node of the search. The dynamic part is implemented
1388// through a set of linear cut generators that will be called throughout the
1389// search.
1390//
1391// TODO(user): In full generality, we could encode all the constraint as an LP.
1392// TODO(user): Add unit tests for this method.
1393// TODO(user): Remove and merge with model loading.
1394void TryToLinearizeConstraint(const CpModelProto& /*model_proto*/,
1395 const ConstraintProto& ct,
1396 int linearization_level, Model* model,
1397 LinearRelaxation* relaxation,
1398 ActivityBoundHelper* activity_helper) {
1399 CHECK_EQ(model->GetOrCreate<SatSolver>()->CurrentDecisionLevel(), 0);
1400 DCHECK_GT(linearization_level, 0);
1401
1402 const int old_index = relaxation->linear_constraints.size();
1403 switch (ct.constraint_case()) {
1405 if (linearization_level > 1) {
1406 AppendBoolOrRelaxation(ct, model, relaxation);
1407 }
1408 break;
1409 }
1411 if (linearization_level > 1) {
1412 AppendBoolAndRelaxation(ct, model, relaxation, activity_helper);
1413 }
1414 break;
1415 }
1417 AppendAtMostOneRelaxation(ct, model, relaxation);
1418 break;
1419 }
1421 AppendExactlyOneRelaxation(ct, model, relaxation);
1422 break;
1423 }
1425 const LinearArgumentProto& int_prod = ct.int_prod();
1426 if (int_prod.exprs_size() == 2 &&
1428 int_prod.exprs(1))) {
1429 AppendSquareRelaxation(ct, model, relaxation);
1430 AddSquareCutGenerator(ct, linearization_level, model, relaxation);
1431 } else {
1432 // No relaxation, just a cut generator .
1433 AddIntProdCutGenerator(ct, linearization_level, model, relaxation);
1434 }
1435 break;
1436 }
1438 AppendLinMaxRelaxationPart1(ct, model, relaxation);
1439 const bool is_affine_max =
1441 if (is_affine_max) {
1442 AppendMaxAffineRelaxation(ct, model, relaxation);
1443 }
1444
1445 // Add cut generators.
1446 if (linearization_level > 1) {
1447 if (is_affine_max) {
1448 AddMaxAffineCutGenerator(ct, model, relaxation);
1449 } else if (ct.lin_max().exprs().size() < 100) {
1450 AddLinMaxCutGenerator(ct, model, relaxation);
1451 }
1452 }
1453 break;
1454 }
1456 AddAllDiffRelaxationAndCutGenerator(ct, linearization_level, model,
1457 relaxation);
1458 break;
1459 }
1462 ct, /*linearize_enforced_constraints=*/linearization_level > 1, model,
1463 relaxation, activity_helper);
1464 break;
1465 }
1467 AppendCircuitRelaxation(ct, model, relaxation);
1468 if (linearization_level > 1) {
1469 AddCircuitCutGenerator(ct, model, relaxation);
1470 }
1471 break;
1472 }
1474 AppendRoutesRelaxation(ct, model, relaxation);
1475 if (linearization_level > 1) {
1476 AddRoutesCutGenerator(ct, model, relaxation);
1477 }
1478 break;
1479 }
1481 AppendNoOverlapRelaxationAndCutGenerator(ct, model, relaxation);
1482 break;
1483 }
1485 AppendCumulativeRelaxationAndCutGenerator(ct, model, relaxation);
1486 break;
1487 }
1489 // TODO(user): Use the same pattern as the other 2 scheduling methods:
1490 // - single function
1491 // - generate helpers once
1492 //
1493 // Adds an energetic relaxation (sum of areas fits in bounding box).
1494 AppendNoOverlap2dRelaxation(ct, model, relaxation);
1495 if (linearization_level > 1) {
1496 // Adds a completion time cut generator and an energetic cut generator.
1497 AddNoOverlap2dCutGenerator(ct, model, relaxation);
1498 }
1499 break;
1500 }
1501 default: {
1502 }
1503 }
1504
1505 if (DEBUG_MODE) {
1506 const auto& integer_trail = *model->GetOrCreate<IntegerTrail>();
1507 for (int i = old_index; i < relaxation->linear_constraints.size(); ++i) {
1508 const bool issue =
1509 PossibleOverflow(integer_trail, relaxation->linear_constraints[i]);
1510 if (issue) {
1511 LOG(INFO) << "Possible overflow in linearization of: "
1512 << google::protobuf::ShortFormat(ct);
1513 }
1514 }
1515 }
1516}
1517
1518// Cut generators.
1519
1520void AddIntProdCutGenerator(const ConstraintProto& ct, int linearization_level,
1521 Model* m, LinearRelaxation* relaxation) {
1522 if (HasEnforcementLiteral(ct)) return;
1523 if (ct.int_prod().exprs_size() != 2) return;
1524 auto* mapping = m->GetOrCreate<CpModelMapping>();
1525
1526 // Constraint is z == x * y.
1527 AffineExpression z = mapping->Affine(ct.int_prod().target());
1528 AffineExpression x = mapping->Affine(ct.int_prod().exprs(0));
1529 AffineExpression y = mapping->Affine(ct.int_prod().exprs(1));
1530
1531 IntegerTrail* const integer_trail = m->GetOrCreate<IntegerTrail>();
1532 IntegerValue x_lb = integer_trail->LowerBound(x);
1533 IntegerValue x_ub = integer_trail->UpperBound(x);
1534 IntegerValue y_lb = integer_trail->LowerBound(y);
1535 IntegerValue y_ub = integer_trail->UpperBound(y);
1536
1537 // We currently only support variables with non-negative domains.
1538 if (x_lb < 0 && x_ub > 0) return;
1539 if (y_lb < 0 && y_ub > 0) return;
1540
1541 // Change signs to return to the case where all variables are a domain
1542 // with non negative values only.
1543 if (x_ub <= 0) {
1544 x = x.Negated();
1545 z = z.Negated();
1546 }
1547 if (y_ub <= 0) {
1548 y = y.Negated();
1549 z = z.Negated();
1550 }
1551
1553 z, x, y, linearization_level, m));
1554}
1555
1557 LinearRelaxation* relaxation) {
1558 if (HasEnforcementLiteral(ct)) return;
1559 auto* mapping = m->GetOrCreate<CpModelMapping>();
1560 IntegerTrail* const integer_trail = m->GetOrCreate<IntegerTrail>();
1561
1562 // Constraint is square == x * x.
1563 AffineExpression square = mapping->Affine(ct.int_prod().target());
1564 AffineExpression x = mapping->Affine(ct.int_prod().exprs(0));
1565 IntegerValue x_lb = integer_trail->LowerBound(x);
1566 IntegerValue x_ub = integer_trail->UpperBound(x);
1567
1568 if (x_lb == x_ub) return;
1569
1570 // We currently only support variables with non-negative domains.
1571 if (x_lb < 0 && x_ub > 0) return;
1572
1573 // Change the sigh of x if its domain is non-positive.
1574 if (x_ub <= 0) {
1575 x = x.Negated();
1576 const IntegerValue tmp = x_ub;
1577 x_ub = -x_lb;
1578 x_lb = -tmp;
1579 }
1580
1581 // Check for potential overflows.
1582 if (x_ub > (int64_t{1} << 31)) return;
1583 DCHECK_GE(x_lb, 0);
1584
1585 relaxation->linear_constraints.push_back(
1586 ComputeHyperplanAboveSquare(x, square, x_lb, x_ub, m));
1587
1588 relaxation->linear_constraints.push_back(
1589 ComputeHyperplanBelowSquare(x, square, x_lb, m));
1590 // TODO(user): We could add all or some below_hyperplans.
1591 if (x_lb + 1 < x_ub) {
1592 // The hyperplan will use x_ub - 1 and x_ub.
1593 relaxation->linear_constraints.push_back(
1594 ComputeHyperplanBelowSquare(x, square, x_ub - 1, m));
1595 }
1596}
1597
1598void AddSquareCutGenerator(const ConstraintProto& ct, int linearization_level,
1599 Model* m, LinearRelaxation* relaxation) {
1600 if (HasEnforcementLiteral(ct)) return;
1601 auto* mapping = m->GetOrCreate<CpModelMapping>();
1602 IntegerTrail* const integer_trail = m->GetOrCreate<IntegerTrail>();
1603
1604 // Constraint is square == x * x.
1605 const AffineExpression square = mapping->Affine(ct.int_prod().target());
1606 AffineExpression x = mapping->Affine(ct.int_prod().exprs(0));
1607 const IntegerValue x_lb = integer_trail->LowerBound(x);
1608 const IntegerValue x_ub = integer_trail->UpperBound(x);
1609
1610 // We currently only support variables with non-negative domains.
1611 if (x_lb < 0 && x_ub > 0) return;
1612
1613 // Change the sigh of x if its domain is non-positive.
1614 if (x_ub <= 0) {
1615 x = x.Negated();
1616 }
1617
1618 relaxation->cut_generators.push_back(
1619 CreateSquareCutGenerator(square, x, linearization_level, m));
1620}
1621
1623 int linearization_level, Model* m,
1624 LinearRelaxation* relaxation) {
1625 if (HasEnforcementLiteral(ct)) return;
1626 auto* mapping = m->GetOrCreate<CpModelMapping>();
1627 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1628 const int num_exprs = ct.all_diff().exprs_size();
1629
1630 const std::vector<AffineExpression> exprs =
1631 mapping->Affines(ct.all_diff().exprs());
1632
1633 // Build union of affine expressions domains to check if this is a
1634 // permutation.
1635 Domain union_of_domains;
1636 for (const AffineExpression& expr : exprs) {
1637 if (integer_trail->IsFixed(expr)) {
1638 union_of_domains = union_of_domains.UnionWith(
1639 Domain(integer_trail->FixedValue(expr).value()));
1640 } else {
1641 union_of_domains = union_of_domains.UnionWith(
1642 integer_trail->InitialVariableDomain(expr.var)
1643 .MultiplicationBy(expr.coeff.value())
1644 .AdditionWith(Domain(expr.constant.value())));
1645 }
1646 }
1647
1648 if (union_of_domains.Size() == num_exprs) {
1649 // In case of a permutation, the linear constraint is tight.
1650 int64_t sum_of_values = 0;
1651 for (const int64_t v : union_of_domains.Values()) {
1652 sum_of_values += v;
1653 }
1654 LinearConstraintBuilder relax(m, sum_of_values, sum_of_values);
1655 for (const AffineExpression& expr : exprs) {
1656 relax.AddTerm(expr, 1);
1657 }
1658 relaxation->linear_constraints.push_back(relax.Build());
1659 } else if (num_exprs <=
1661 linearization_level > 1) {
1662 relaxation->cut_generators.push_back(
1664 }
1665}
1666
1667bool IntervalIsVariable(const IntervalVariable interval,
1668 IntervalsRepository* intervals_repository) {
1669 // Ignore absent rectangles.
1670 if (intervals_repository->IsAbsent(interval)) {
1671 return false;
1672 }
1673
1674 // Checks non-present intervals.
1675 if (!intervals_repository->IsPresent(interval)) {
1676 return true;
1677 }
1678
1679 // Checks variable sized intervals.
1680 if (intervals_repository->MinSize(interval) !=
1681 intervals_repository->MaxSize(interval)) {
1682 return true;
1683 }
1684
1685 return false;
1686}
1687
1690 SchedulingDemandHelper* demands_helper,
1691 const std::optional<AffineExpression>& makespan,
1692 Model* m, LinearRelaxation* relaxation) {
1694 helper, demands_helper, capacity, m));
1695 relaxation->cut_generators.push_back(
1696 CreateCumulativeCompletionTimeCutGenerator(helper, demands_helper,
1697 capacity, m));
1699 helper, demands_helper, capacity, m));
1700
1701 // Checks if at least one rectangle has a variable size, is optional, or if
1702 // the demand or the capacity are variable.
1703 bool has_variable_part = false;
1704 IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
1705 for (int i = 0; i < helper->NumTasks(); ++i) {
1706 if (!helper->SizeIsFixed(i)) {
1707 has_variable_part = true;
1708 break;
1709 }
1710 // Checks variable demand.
1711 if (!demands_helper->DemandIsFixed(i)) {
1712 has_variable_part = true;
1713 break;
1714 }
1715 }
1716 if (has_variable_part || !integer_trail->IsFixed(capacity)) {
1718 helper, demands_helper, capacity, makespan, m));
1719 }
1720}
1721
1723 const std::optional<AffineExpression>& makespan,
1724 Model* m, LinearRelaxation* relaxation) {
1725 relaxation->cut_generators.push_back(
1727 relaxation->cut_generators.push_back(
1729
1730 // Checks if at least one rectangle has a variable size or is optional.
1731 bool has_variable_or_optional_part = false;
1732 for (int i = 0; i < helper->NumTasks(); ++i) {
1733 if (helper->IsAbsent(i)) continue;
1734 if (!helper->SizeIsFixed(i) || !helper->IsPresent(i)) {
1735 has_variable_or_optional_part = true;
1736 break;
1737 }
1738 }
1739 if (has_variable_or_optional_part) {
1740 relaxation->cut_generators.push_back(
1741 CreateNoOverlapEnergyCutGenerator(helper, makespan, m));
1742 }
1743}
1744
1746 LinearRelaxation* relaxation) {
1747 if (HasEnforcementLiteral(ct)) return;
1748
1749 auto* mapping = m->GetOrCreate<CpModelMapping>();
1750 std::vector<IntervalVariable> x_intervals =
1751 mapping->Intervals(ct.no_overlap_2d().x_intervals());
1752 std::vector<IntervalVariable> y_intervals =
1753 mapping->Intervals(ct.no_overlap_2d().y_intervals());
1754
1755 IntervalsRepository* intervals_repository =
1757 NoOverlap2DConstraintHelper* no_overlap_helper =
1758 intervals_repository->GetOrCreate2DHelper(x_intervals, y_intervals);
1759
1760 relaxation->cut_generators.push_back(
1761 CreateNoOverlap2dCompletionTimeCutGenerator(no_overlap_helper, m));
1762
1763 // Checks if at least one rectangle has a variable dimension or is optional.
1764 bool has_variable_part = false;
1765 for (int i = 0; i < x_intervals.size(); ++i) {
1766 // Ignore absent rectangles.
1767 if (intervals_repository->IsAbsent(x_intervals[i]) ||
1768 intervals_repository->IsAbsent(y_intervals[i])) {
1769 continue;
1770 }
1771
1772 // Checks non-present intervals.
1773 if (!intervals_repository->IsPresent(x_intervals[i]) ||
1774 !intervals_repository->IsPresent(y_intervals[i])) {
1775 has_variable_part = true;
1776 break;
1777 }
1778
1779 // Checks variable sized intervals.
1780 if (intervals_repository->MinSize(x_intervals[i]) !=
1781 intervals_repository->MaxSize(x_intervals[i]) ||
1782 intervals_repository->MinSize(y_intervals[i]) !=
1783 intervals_repository->MaxSize(y_intervals[i])) {
1784 has_variable_part = true;
1785 break;
1786 }
1787 }
1788
1789 if (!has_variable_part) return;
1790
1791 relaxation->cut_generators.push_back(
1792 CreateNoOverlap2dEnergyCutGenerator(no_overlap_helper, m));
1793}
1794
1796 LinearRelaxation* relaxation) {
1797 if (!m->GetOrCreate<SatParameters>()->add_lin_max_cuts()) return;
1798 if (HasEnforcementLiteral(ct)) return;
1799
1800 // TODO(user): Support linearization of general target expression.
1801 auto* mapping = m->GetOrCreate<CpModelMapping>();
1802 if (ct.lin_max().target().vars_size() != 1) return;
1803 if (ct.lin_max().target().coeffs(0) != 1) return;
1804 if (ct.lin_max().target().offset() != 0) return;
1805
1806 const IntegerVariable target =
1807 mapping->Integer(ct.lin_max().target().vars(0));
1808 std::vector<LinearExpression> exprs;
1809 exprs.reserve(ct.lin_max().exprs_size());
1810 for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
1811 // Note: Cut generator requires all expressions to contain only positive
1812 // vars.
1813 exprs.push_back(
1814 PositiveVarExpr(mapping->GetExprFromProto(ct.lin_max().exprs(i))));
1815 }
1816
1817 const std::vector<Literal> alternative_literals =
1818 CreateAlternativeLiteralsWithView(exprs.size(), m, relaxation);
1819
1820 // TODO(user): Move this out of here.
1821 //
1822 // Add initial big-M linear relaxation.
1823 // z_vars[i] == 1 <=> target = exprs[i].
1824 AppendLinMaxRelaxationPart2(target, alternative_literals, exprs, m,
1825 relaxation);
1826
1827 std::vector<IntegerVariable> z_vars;
1828 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1829 for (const Literal lit : alternative_literals) {
1830 z_vars.push_back(encoder->GetLiteralView(lit));
1831 CHECK_NE(z_vars.back(), kNoIntegerVariable);
1832 }
1833 relaxation->cut_generators.push_back(
1834 CreateLinMaxCutGenerator(target, exprs, z_vars, m));
1835}
1836
1837// If we have an exactly one between literals l_i, and each l_i => var ==
1838// value_i, then we can add a strong linear relaxation: var = sum l_i * value_i.
1839//
1840// This codes detect this and add the corresponding linear equations.
1841//
1842// TODO(user): We can do something similar with just an at most one, however
1843// it is harder to detect that if all literal are false then none of the implied
1844// value can be taken.
1846 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1847 auto* element_encodings = m->GetOrCreate<ElementEncodings>();
1848
1849 int num_exactly_one_elements = 0;
1850 for (const IntegerVariable var :
1851 element_encodings->GetElementEncodedVariables()) {
1852 for (const auto& [index, literal_value_list] :
1853 element_encodings->Get(var)) {
1854 IntegerValue min_value = kMaxIntegerValue;
1855 for (const auto& literal_value : literal_value_list) {
1856 min_value = std::min(min_value, literal_value.value);
1857 }
1858
1859 LinearConstraintBuilder builder(m, -min_value, -min_value);
1860 builder.AddTerm(var, IntegerValue(-1));
1861 for (const auto& [value, literal] : literal_value_list) {
1862 const IntegerValue delta_min = value - min_value;
1863 if (delta_min != 0) {
1864 // If the term has no view, we abort.
1865 if (!builder.AddLiteralTerm(literal, delta_min)) {
1866 return;
1867 }
1868 }
1869 }
1870 ++num_exactly_one_elements;
1871 LinearConstraint lc = builder.Build();
1872 if (!PossibleOverflow(*integer_trail, lc)) {
1873 relaxation->linear_constraints.push_back(std::move(lc));
1874 }
1875 }
1876 }
1877
1878 if (num_exactly_one_elements != 0) {
1879 auto* logger = m->GetOrCreate<SolverLogger>();
1880 SOLVER_LOG(logger,
1881 "[ElementLinearRelaxation]"
1882 " #from_exactly_one:",
1883 num_exactly_one_elements);
1884 }
1885}
1886
1888 Model* m) {
1889 LinearRelaxation relaxation;
1890 const SatParameters& params = *m->GetOrCreate<SatParameters>();
1891
1892 // Collect AtMostOne to compute better Big-M.
1893 ActivityBoundHelper activity_bound_helper;
1894 if (params.linearization_level() > 1) {
1895 activity_bound_helper.AddAllAtMostOnes(model_proto);
1896 }
1897
1898 // Linearize the constraints.
1899 for (const auto& ct : model_proto.constraints()) {
1900 TryToLinearizeConstraint(model_proto, ct, params.linearization_level(), m,
1901 &relaxation, &activity_bound_helper);
1902 }
1903
1904 // Linearize the encoding of variable that are fully encoded.
1905 int num_loose_equality_encoding_relaxations = 0;
1906 int num_tight_equality_encoding_relaxations = 0;
1907 int num_inequality_encoding_relaxations = 0;
1908 auto* mapping = m->GetOrCreate<CpModelMapping>();
1909 for (int i = 0; i < model_proto.variables_size(); ++i) {
1910 if (mapping->IsBoolean(i)) continue;
1911
1912 const IntegerVariable var = mapping->Integer(i);
1913 if (m->Get(IsFixed(var))) continue;
1914
1915 // We first try to linearize the values encoding.
1917 var, *m, &relaxation, &num_tight_equality_encoding_relaxations,
1918 &num_loose_equality_encoding_relaxations);
1919
1920 // Then we try to linearize the inequality encoding. Note that on some
1921 // problem like pizza27i.mps.gz, adding both equality and inequality
1922 // encoding is a must.
1923 //
1924 // Even if the variable is fully encoded, sometimes not all its associated
1925 // literal have a view (if they are not part of the original model for
1926 // instance).
1927 //
1928 // TODO(user): Should we add them to the LP anyway? this isn't clear as
1929 // we can sometimes create a lot of Booleans like this.
1930 const int old = relaxation.linear_constraints.size();
1931 AppendPartialGreaterThanEncodingRelaxation(var, *m, &relaxation);
1932 if (relaxation.linear_constraints.size() > old) {
1933 ++num_inequality_encoding_relaxations;
1934 }
1935 }
1936
1937 // TODO(user): This is similar to AppendRelaxationForEqualityEncoding() above.
1938 // Investigate if we can merge the code.
1939 if (params.linearization_level() >= 2) {
1940 AppendElementEncodingRelaxation(m, &relaxation);
1941 }
1942
1943 // TODO(user): I am not sure this is still needed. Investigate and explain why
1944 // or remove.
1945 if (!m->GetOrCreate<SatSolver>()->FinishPropagation()) {
1946 return relaxation;
1947 }
1948
1949 // We display the stats before linearizing the at most ones.
1950 auto* logger = m->GetOrCreate<SolverLogger>();
1951 if (num_tight_equality_encoding_relaxations != 0 ||
1952 num_loose_equality_encoding_relaxations != 0 ||
1953 num_inequality_encoding_relaxations != 0) {
1954 SOLVER_LOG(logger,
1955 "[EncodingLinearRelaxation]"
1956 " #tight_equality:",
1957 num_tight_equality_encoding_relaxations,
1958 " #loose_equality:", num_loose_equality_encoding_relaxations,
1959 " #inequality:", num_inequality_encoding_relaxations);
1960 }
1961 if (!relaxation.linear_constraints.empty() ||
1962 !relaxation.at_most_ones.empty()) {
1963 SOLVER_LOG(logger,
1964 "[LinearRelaxationBeforeCliqueExpansion]"
1965 " #linear:",
1966 relaxation.linear_constraints.size(),
1967 " #at_most_ones:", relaxation.at_most_ones.size());
1968 }
1969
1970 // Linearize the at most one constraints. Note that we transform them
1971 // into maximum "at most one" first and we removes redundant ones.
1972 m->GetOrCreate<BinaryImplicationGraph>()->TransformIntoMaxCliques(
1973 &relaxation.at_most_ones,
1975 for (const std::vector<Literal>& at_most_one : relaxation.at_most_ones) {
1976 if (at_most_one.empty()) continue;
1977
1978 LinearConstraintBuilder lc(m, kMinIntegerValue, IntegerValue(1));
1979 for (const Literal literal : at_most_one) {
1980 // Note that it is okay to simply ignore the literal if it has no
1981 // integer view.
1982 const bool unused ABSL_ATTRIBUTE_UNUSED =
1983 lc.AddLiteralTerm(literal, IntegerValue(1));
1984 }
1985 relaxation.linear_constraints.push_back(lc.Build());
1986 }
1987
1988 // We converted all at_most_one to LP constraints, so we need to clear them
1989 // so that we don't do extra work in the connected component computation.
1990 relaxation.at_most_ones.clear();
1991
1992 // Propagate unary constraints.
1993 {
1994 SatSolver* sat_solver = m->GetOrCreate<SatSolver>();
1995 CHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
1996 IntegerTrail* integer_trail = m->GetOrCreate<IntegerTrail>();
1997 for (const LinearConstraint& lc : relaxation.linear_constraints) {
1998 if (lc.num_terms == 0) {
1999 if (lc.lb > 0 || lc.ub < 0) {
2000 sat_solver->NotifyThatModelIsUnsat();
2001 return relaxation;
2002 }
2003 } else if (lc.num_terms == 1) {
2004 const AffineExpression expr(lc.vars[0], lc.coeffs[0]);
2005 if (lc.lb > integer_trail->LevelZeroLowerBound(expr)) {
2006 if (!integer_trail->Enqueue(expr.GreaterOrEqual(lc.lb), {}, {})) {
2007 sat_solver->NotifyThatModelIsUnsat();
2008 return relaxation;
2009 }
2010 }
2011 if (lc.ub < integer_trail->LevelZeroUpperBound(expr)) {
2012 if (!integer_trail->Enqueue(expr.LowerOrEqual(lc.ub), {}, {})) {
2013 sat_solver->NotifyThatModelIsUnsat();
2014 return relaxation;
2015 }
2016 }
2017 }
2018 }
2019 if (!sat_solver->FinishPropagation()) return relaxation;
2020 }
2021
2022 // Remove size one LP constraints from the main algorithms, they are not
2023 // useful.
2024 relaxation.linear_constraints.erase(
2025 std::remove_if(
2026 relaxation.linear_constraints.begin(),
2027 relaxation.linear_constraints.end(),
2028 [](const LinearConstraint& lc) { return lc.num_terms <= 1; }),
2029 relaxation.linear_constraints.end());
2030
2031 if (!relaxation.linear_constraints.empty() ||
2032 !relaxation.cut_generators.empty()) {
2033 SOLVER_LOG(logger,
2034 "[FinalLinearRelaxation]"
2035 " #linear:",
2036 relaxation.linear_constraints.size(),
2037 " #cut_generators:", relaxation.cut_generators.size());
2038 }
2039
2040 return relaxation;
2041}
2042
2043} // namespace sat
2044} // namespace operations_research
Definition model.h:341
DomainIteratorBeginEnd Values() const &
Domain UnionWith(const Domain &domain) const
static IntegralType FloorOfRatio(IntegralType numerator, IntegralType denominator)
Definition mathutil.h:53
int64_t ComputeMaxActivity(absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > *conditional=nullptr)
int64_t ComputeMinActivity(absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > *conditional=nullptr)
std::vector< absl::Span< const int > > PartitionLiteralsIntoAmo(absl::Span< const int > literals)
Similar algo as above for this simpler case.
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 1;
int heads_size() const
repeated int32 heads = 4;
int tails_size() const
repeated int32 tails = 3;
int literals_size() const
repeated int32 literals = 5;
::int32_t enforcement_literal(int index) const
const ::operations_research::sat::BoolArgumentProto & exactly_one() const
const ::operations_research::sat::NoOverlapConstraintProto & no_overlap() const
const ::operations_research::sat::AllDifferentConstraintProto & all_diff() const
const ::operations_research::sat::LinearConstraintProto & linear() const
const ::operations_research::sat::BoolArgumentProto & at_most_one() const
const ::operations_research::sat::RoutesConstraintProto & routes() const
const ::operations_research::sat::LinearArgumentProto & lin_max() const
const ::operations_research::sat::BoolArgumentProto & bool_and() const
const ::operations_research::sat::BoolArgumentProto & bool_or() const
const ::operations_research::sat::LinearArgumentProto & int_prod() const
const ::operations_research::sat::CircuitConstraintProto & circuit() const
const ::operations_research::sat::CumulativeConstraintProto & cumulative() const
int enforcement_literal_size() const
repeated int32 enforcement_literal = 2;
bool has_no_overlap_2d() const
.operations_research.sat.NoOverlap2DConstraintProto no_overlap_2d = 21;
const ::operations_research::sat::NoOverlap2DConstraintProto & no_overlap_2d() const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
std::vector< sat::Literal > Literals(const ProtoIndices &indices) const
IntegerVariable Integer(int ref) const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
const ::operations_research::sat::LinearExpressionProto & demands(int index) const
const ::operations_research::sat::LinearExpressionProto & capacity() const
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
Definition integer.h:1317
IntegerValue UpperBound(IntegerVariable i) const
Definition integer.h:1321
IntegerValue FixedValue(IntegerVariable i) const
Checks that the variable is fixed and returns its value.
Definition integer.h:1329
bool IsFixed(IntegerVariable i) const
Checks if the variable is fixed.
Definition integer.h:1325
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition integer.h:1419
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
Definition integer.h:1412
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit)
Definition integer.h:609
SchedulingDemandHelper * GetOrCreateDemandHelper(SchedulingConstraintHelper *helper, absl::Span< const AffineExpression > demands)
Definition intervals.cc:344
AffineExpression Start(IntervalVariable i) const
Definition intervals.h:92
bool IsAbsent(IntervalVariable i) const
Definition intervals.h:79
IntegerValue MaxSize(IntervalVariable i) const
Return the maximum size of the given IntervalVariable.
Definition intervals.h:101
IntegerValue MinSize(IntervalVariable i) const
Return the minimum size of the given IntervalVariable.
Definition intervals.h:96
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
bool IsPresent(IntervalVariable i) const
Definition intervals.h:75
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 2;
const ::operations_research::sat::LinearExpressionProto & target() const
void AddQuadraticLowerBound(AffineExpression left, AffineExpression right, IntegerTrail *integer_trail, bool *is_quadratic=nullptr)
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff=IntegerValue(1))
void AddTerm(IntegerVariable var, IntegerValue coeff)
void AddLinearExpression(const LinearExpression &expr)
void AddConstant(IntegerValue value)
Adds the corresponding term to the current linear expression.
void Clear()
Clears all added terms and constants. Keeps the original bounds.
LinearConstraint BuildConstraint(IntegerValue lb, IntegerValue ub)
ABSL_MUST_USE_RESULT bool AddDecomposedProduct(absl::Span< const LiteralValueValue > product)
ConstraintIndex Add(LinearConstraint ct, bool *added=nullptr, bool *folded=nullptr)
void RegisterWith(GenericLiteralWatcher *watcher)
int vars_size() const
repeated int32 vars = 1;
int domain_size() const
repeated int64 domain = 3;
int vars_size() const
repeated int32 vars = 1;
T Add(std::function< T(Model *)> f)
Definition model.h:87
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Definition model.h:93
std::pair< IntegerValue, IntegerValue > GetLevelZeroBoxSizesMin(int index) const
void ComputeFullPrecedences(absl::Span< const IntegerVariable > vars, std::vector< FullIntegerPrecedence > *output)
Helper class to express a product as a linear constraint.
std::vector< LiteralValueValue > TryToDecompose(const AffineExpression &left, const AffineExpression &right)
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::RoutesConstraintProto_NodeExpressions & dimensions(int index) const
int literals_size() const
repeated int32 literals = 3;
int dimensions_size() const
repeated .operations_research.sat.RoutesConstraintProto.NodeExpressions dimensions = 6;
int heads_size() const
repeated int32 heads = 2;
int tails_size() const
repeated int32 tails = 1;
ABSL_MUST_USE_RESULT bool FinishPropagation()
int NumTasks() const
Returns the number of task.
absl::Span< const AffineExpression > Sizes() const
ABSL_MUST_USE_RESULT bool SynchronizeAndSetTimeDirection(bool is_forward)
const std::vector< std::vector< LiteralValueValue > > & DecomposedEnergies() const
const std::vector< AffineExpression > & Demands() const
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:55
std::vector< typename Map::mapped_type > Values(const Map &map, const Keys &keys)
Definition key_types.h:137
void AppendNoOverlapRelaxationAndCutGenerator(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AppendCumulativeRelaxationAndCutGenerator(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
CutGenerator CreateCumulativeCompletionTimeCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
void AddSquareCutGenerator(const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
void AppendExactlyOneRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
bool BuildMaxAffineUpConstraint(const LinearExpression &target, IntegerVariable var, absl::Span< const std::pair< IntegerValue, IntegerValue > > affines, Model *model, LinearConstraintBuilder *builder)
Definition cuts.cc:2668
std::optional< int > DetectMakespan(absl::Span< const IntervalVariable > intervals, absl::Span< const AffineExpression > demands, const AffineExpression &capacity, Model *model)
void AddCumulativeCutGenerator(const AffineExpression &capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const std::optional< AffineExpression > &makespan, Model *m, LinearRelaxation *relaxation)
void AppendLinMaxRelaxationPart2(IntegerVariable target, absl::Span< const Literal > alternative_literals, absl::Span< const LinearExpression > exprs, Model *model, LinearRelaxation *relaxation)
void AppendRoutesRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
CutGenerator CreatePositiveMultiplicationCutGenerator(AffineExpression z, AffineExpression x, AffineExpression y, int linearization_level, Model *model)
A cut generator for z = x * y (x and y >= 0).
Definition cuts.cc:1876
CutGenerator CreateStronglyConnectedGraphCutGenerator(int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, Model *model)
bool ProdOverflow(IntegerValue t, IntegerValue value)
CutGenerator CreateNoOverlap2dEnergyCutGenerator(NoOverlap2DConstraintHelper *helper, Model *model)
const LiteralIndex kNoLiteralIndex(-1)
void AddMaxAffineCutGenerator(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AddCircuitCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x, AffineExpression square, IntegerValue x_value, Model *model)
Definition cuts.cc:1983
CutGenerator CreateCumulativePrecedenceCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
LinearRelaxation ComputeLinearRelaxation(const CpModelProto &model_proto, Model *m)
Builds the linear relaxation of a CpModelProto.
bool HasEnforcementLiteral(const ConstraintProto &ct)
Small utility functions to deal with half-reified constraints.
void AppendLinearConstraintRelaxation(const ConstraintProto &ct, bool linearize_enforced_constraints, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition integer.h:1593
void AddIntProdCutGenerator(const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
Cut generators.
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
void AddRoutesCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
CutGenerator CreateCumulativeEnergyCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, const std::optional< AffineExpression > &makespan, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
bool PossibleOverflow(const IntegerTrail &integer_trail, const LinearConstraint &constraint)
CutGenerator CreateLinMaxCutGenerator(const IntegerVariable target, absl::Span< const LinearExpression > exprs, absl::Span< const IntegerVariable > z_vars, Model *model)
Definition cuts.cc:2579
void AddIntegerVariableFromIntervals(const SchedulingConstraintHelper *helper, Model *model, std::vector< IntegerVariable > *vars, int mask)
CutGenerator CreateAllDifferentCutGenerator(absl::Span< const AffineExpression > exprs, Model *model)
Definition cuts.cc:2467
void AddCumulativeRelaxation(const AffineExpression &capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const std::optional< AffineExpression > &makespan, Model *model, LinearRelaxation *relaxation)
Scheduling relaxations and cut generators.
CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x, int linearization_level, Model *model)
Definition cuts.cc:1995
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
void TryToLinearizeConstraint(const CpModelProto &, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
Adds linearization of different types of constraints.
IntegerVariable PositiveVariable(IntegerVariable i)
CutGenerator CreateCumulativeTimeTableCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
int64_t SafeDoubleToInt64(double value)
Definition util.h:737
void AppendLinMaxRelaxationPart1(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
CutGenerator CreateNoOverlapCompletionTimeCutGenerator(SchedulingConstraintHelper *helper, Model *model)
CutGenerator CreateMaxAffineCutGenerator(LinearExpression target, IntegerVariable var, std::vector< std::pair< IntegerValue, IntegerValue > > affines, const std::string cut_name, Model *model)
Definition cuts.cc:2722
int ReindexArcs(IntContainer *tails, IntContainer *heads, absl::flat_hash_map< int, int > *mapping_output=nullptr)
Definition circuit.h:208
void AppendCircuitRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
Routing relaxation and cut generators.
CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator(NoOverlap2DConstraintHelper *helper, Model *model)
void AppendElementEncodingRelaxation(Model *m, LinearRelaxation *relaxation)
LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x, AffineExpression square, IntegerValue x_lb, IntegerValue x_ub, Model *model)
Definition cuts.cc:1971
void AppendMaxAffineRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AppendNoOverlap2dRelaxationForComponent(absl::Span< const int > component, Model *model, NoOverlap2DConstraintHelper *no_overlap_helper, LinearConstraintManager *manager, ProductDecomposer *product_decomposer)
bool ExpressionsContainsOnlyOneVar(const ExpressionList &exprs)
Returns true if there exactly one variable appearing in all the expressions.
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64_t lb, int64_t ub)
Definition integer.h:1533
CutGenerator CreateNoOverlapEnergyCutGenerator(SchedulingConstraintHelper *helper, const std::optional< AffineExpression > &makespan, Model *model)
CutGenerator CreateCVRPCutGenerator(int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, absl::Span< const AffineExpression > flat_node_dim_expressions, Model *model)
bool IntervalIsVariable(const IntervalVariable interval, IntervalsRepository *intervals_repository)
void AppendSquareRelaxation(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
CutGenerator CreateNoOverlapPrecedenceCutGenerator(SchedulingConstraintHelper *helper, Model *model)
void AddLinMaxCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
std::function< void(Model *)> ExactlyOneConstraint(absl::Span< const Literal > literals)
Definition sat_solver.h:914
LinearExpression PositiveVarExpr(const LinearExpression &expr)
Returns the same expression with positive variables.
void AppendBoolAndRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
void AddAllDiffRelaxationAndCutGenerator(const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
void AppendNoOverlap2dRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
Adds the energetic relaxation sum(areas) <= bounding box area.
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
void AppendAtMostOneRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AddNoOverlapCutGenerator(SchedulingConstraintHelper *helper, const std::optional< AffineExpression > &makespan, Model *m, LinearRelaxation *relaxation)
void AddNoOverlap2dCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
bool VariableIsPositive(IntegerVariable i)
std::vector< Literal > CreateAlternativeLiteralsWithView(int num_literals, Model *model, LinearRelaxation *relaxation)
IntegerValue CapSubI(IntegerValue a, IntegerValue b)
bool LinearExpressionProtosAreEqual(const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
Returns true iff a == b * b_scaling.
bool AtMinOrMaxInt64I(IntegerValue t)
LinearConstraintPropagator< false > IntegerSumLE
void AppendBoolOrRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AppendRelaxationForEqualityEncoding(IntegerVariable var, const Model &model, LinearRelaxation *relaxation, int *num_tight, int *num_loose)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
const bool DEBUG_MODE
Definition radix_sort.h:266
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
var * coeff + constant >= bound.
IntegerLiteral LowerOrEqual(IntegerValue bound) const
var * coeff + constant <= bound.
std::unique_ptr< IntegerValue[]> coeffs
std::unique_ptr< IntegerVariable[]> vars
std::vector< std::vector< Literal > > at_most_ones
std::vector< LinearConstraint > linear_constraints
#define SOLVER_LOG(logger,...)
Definition logging.h:110