OR-Tools  8.2
linear_relaxation.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <vector>
17
18#include "absl/container/flat_hash_set.h"
21#include "ortools/sat/cp_model.pb.h"
23#include "ortools/sat/integer.h"
29
30namespace operations_research {
31namespace sat {
32
33bool AppendFullEncodingRelaxation(IntegerVariable var, const Model& model,
34 LinearRelaxation* relaxation) {
35 const auto* encoder = model.Get<IntegerEncoder>();
36 if (encoder == nullptr) return false;
37 if (!encoder->VariableIsFullyEncoded(var)) return false;
38
39 const auto& encoding = encoder->FullDomainEncoding(var);
40 const IntegerValue var_min = model.Get<IntegerTrail>()->LowerBound(var);
41
42 LinearConstraintBuilder at_least_one(&model, IntegerValue(1),
44 LinearConstraintBuilder encoding_ct(&model, var_min, var_min);
45 encoding_ct.AddTerm(var, IntegerValue(1));
46
47 // Create the constraint if all literal have a view.
48 std::vector<Literal> at_most_one;
49
50 for (const auto value_literal : encoding) {
51 const Literal lit = value_literal.literal;
52 const IntegerValue delta = value_literal.value - var_min;
53 DCHECK_GE(delta, IntegerValue(0));
54 at_most_one.push_back(lit);
55 if (!at_least_one.AddLiteralTerm(lit, IntegerValue(1))) return false;
56 if (delta != IntegerValue(0)) {
57 if (!encoding_ct.AddLiteralTerm(lit, -delta)) return false;
58 }
59 }
60
61 relaxation->linear_constraints.push_back(at_least_one.Build());
62 relaxation->linear_constraints.push_back(encoding_ct.Build());
63 relaxation->at_most_ones.push_back(at_most_one);
64 return true;
65}
66
67namespace {
68
69// TODO(user): Not super efficient.
70std::pair<IntegerValue, IntegerValue> GetMinAndMaxNotEncoded(
71 IntegerVariable var,
72 const absl::flat_hash_set<IntegerValue>& encoded_values,
73 const Model& model) {
74 const auto* domains = model.Get<IntegerDomains>();
75 if (domains == nullptr || var >= domains->size()) {
77 }
78
79 // The domain can be large, but the list of values shouldn't, so this
80 // runs in O(encoded_values.size());
81 IntegerValue min = kMaxIntegerValue;
82 for (const ClosedInterval interval : (*domains)[var]) {
83 for (IntegerValue v(interval.start); v <= interval.end; ++v) {
84 if (!gtl::ContainsKey(encoded_values, v)) {
85 min = v;
86 break;
87 }
88 }
89 if (min != kMaxIntegerValue) break;
90 }
91
92 IntegerValue max = kMinIntegerValue;
93 const auto& domain = (*domains)[var];
94 for (int i = domain.NumIntervals() - 1; i >= 0; --i) {
95 const ClosedInterval interval = domain[i];
96 for (IntegerValue v(interval.end); v >= interval.start; --v) {
97 if (!gtl::ContainsKey(encoded_values, v)) {
98 max = v;
99 break;
100 }
101 }
102 if (max != kMinIntegerValue) break;
103 }
104
105 return {min, max};
106}
107
108} // namespace
109
110void AppendPartialEncodingRelaxation(IntegerVariable var, const Model& model,
111 LinearRelaxation* relaxation) {
112 const auto* encoder = model.Get<IntegerEncoder>();
113 const auto* integer_trail = model.Get<IntegerTrail>();
114 if (encoder == nullptr || integer_trail == nullptr) return;
115
116 const std::vector<IntegerEncoder::ValueLiteralPair>& encoding =
117 encoder->PartialDomainEncoding(var);
118 if (encoding.empty()) return;
119
120 std::vector<Literal> at_most_one_ct;
121 absl::flat_hash_set<IntegerValue> encoded_values;
122 for (const auto value_literal : encoding) {
123 const Literal literal = value_literal.literal;
124
125 // Note that we skip pairs that do not have an Integer view.
126 if (encoder->GetLiteralView(literal) == kNoIntegerVariable &&
127 encoder->GetLiteralView(literal.Negated()) == kNoIntegerVariable) {
128 continue;
129 }
130
131 at_most_one_ct.push_back(literal);
132 encoded_values.insert(value_literal.value);
133 }
134 if (encoded_values.empty()) return;
135
136 // TODO(user): The PartialDomainEncoding() function automatically exclude
137 // values that are no longer in the initial domain, so we could be a bit
138 // tighter here. That said, this is supposed to be called just after the
139 // presolve, so it shouldn't really matter.
140 const auto pair = GetMinAndMaxNotEncoded(var, encoded_values, model);
141 if (pair.first == kMaxIntegerValue) {
142 // TODO(user): try to remove the duplication with
143 // AppendFullEncodingRelaxation()? actually I am not sure we need the other
144 // function since this one is just more general.
145 LinearConstraintBuilder exactly_one_ct(&model, IntegerValue(1),
146 IntegerValue(1));
147 LinearConstraintBuilder encoding_ct(&model, IntegerValue(0),
148 IntegerValue(0));
149 encoding_ct.AddTerm(var, IntegerValue(1));
150 for (const auto value_literal : encoding) {
151 const Literal lit = value_literal.literal;
152 CHECK(exactly_one_ct.AddLiteralTerm(lit, IntegerValue(1)));
153 CHECK(
154 encoding_ct.AddLiteralTerm(lit, IntegerValue(-value_literal.value)));
155 }
156 relaxation->linear_constraints.push_back(exactly_one_ct.Build());
157 relaxation->linear_constraints.push_back(encoding_ct.Build());
158 return;
159 }
160
161 // min + sum li * (xi - min) <= var.
162 const IntegerValue d_min = pair.first;
163 LinearConstraintBuilder lower_bound_ct(&model, d_min, kMaxIntegerValue);
164 lower_bound_ct.AddTerm(var, IntegerValue(1));
165 for (const auto value_literal : encoding) {
166 CHECK(lower_bound_ct.AddLiteralTerm(value_literal.literal,
167 d_min - value_literal.value));
168 }
169
170 // var <= max + sum li * (xi - max).
171 const IntegerValue d_max = pair.second;
172 LinearConstraintBuilder upper_bound_ct(&model, kMinIntegerValue, d_max);
173 upper_bound_ct.AddTerm(var, IntegerValue(1));
174 for (const auto value_literal : encoding) {
175 CHECK(upper_bound_ct.AddLiteralTerm(value_literal.literal,
176 d_max - value_literal.value));
177 }
178
179 // Note that empty/trivial constraints will be filtered later.
180 relaxation->at_most_ones.push_back(at_most_one_ct);
181 relaxation->linear_constraints.push_back(lower_bound_ct.Build());
182 relaxation->linear_constraints.push_back(upper_bound_ct.Build());
183}
184
186 const Model& model,
187 LinearRelaxation* relaxation) {
188 const auto* integer_trail = model.Get<IntegerTrail>();
189 const auto* encoder = model.Get<IntegerEncoder>();
190 if (integer_trail == nullptr || encoder == nullptr) return;
191
192 const std::map<IntegerValue, Literal>& greater_than_encoding =
193 encoder->PartialGreaterThanEncoding(var);
194 if (greater_than_encoding.empty()) return;
195
196 // Start by the var >= side.
197 // And also add the implications between used literals.
198 {
199 IntegerValue prev_used_bound = integer_trail->LowerBound(var);
200 LinearConstraintBuilder lb_constraint(&model, prev_used_bound,
202 lb_constraint.AddTerm(var, IntegerValue(1));
203 LiteralIndex prev_literal_index = kNoLiteralIndex;
204 for (const auto entry : greater_than_encoding) {
205 if (entry.first <= prev_used_bound) continue;
206
207 const LiteralIndex literal_index = entry.second.Index();
208 const IntegerValue diff = prev_used_bound - entry.first;
209
210 // Skip the entry if the literal doesn't have a view.
211 if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue;
212 if (prev_literal_index != kNoLiteralIndex) {
213 // Add var <= prev_var, which is the same as var + not(prev_var) <= 1
214 relaxation->at_most_ones.push_back(
215 {Literal(literal_index), Literal(prev_literal_index).Negated()});
216 }
217 prev_used_bound = entry.first;
218 prev_literal_index = literal_index;
219 }
220 relaxation->linear_constraints.push_back(lb_constraint.Build());
221 }
222
223 // Do the same for the var <= side by using NegationOfVar().
224 // Note that we do not need to add the implications between literals again.
225 {
226 IntegerValue prev_used_bound = integer_trail->LowerBound(NegationOf(var));
227 LinearConstraintBuilder lb_constraint(&model, prev_used_bound,
229 lb_constraint.AddTerm(var, IntegerValue(-1));
230 for (const auto entry :
231 encoder->PartialGreaterThanEncoding(NegationOf(var))) {
232 if (entry.first <= prev_used_bound) continue;
233 const IntegerValue diff = prev_used_bound - entry.first;
234
235 // Skip the entry if the literal doesn't have a view.
236 if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue;
237 prev_used_bound = entry.first;
238 }
239 relaxation->linear_constraints.push_back(lb_constraint.Build());
240 }
241}
242
243namespace {
244// Adds enforcing_lit => target <= bounding_var to relaxation.
245void AppendEnforcedUpperBound(const Literal enforcing_lit,
246 const IntegerVariable target,
247 const IntegerVariable bounding_var, Model* model,
248 LinearRelaxation* relaxation) {
249 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
250 const IntegerValue max_target_value = integer_trail->UpperBound(target);
251 const IntegerValue min_var_value = integer_trail->LowerBound(bounding_var);
252 const IntegerValue max_term_value = max_target_value - min_var_value;
253 LinearConstraintBuilder lc(model, kMinIntegerValue, max_term_value);
254 lc.AddTerm(target, IntegerValue(1));
255 lc.AddTerm(bounding_var, IntegerValue(-1));
256 CHECK(lc.AddLiteralTerm(enforcing_lit, max_term_value));
257 relaxation->linear_constraints.push_back(lc.Build());
258}
259
260// Adds {enforcing_lits} => rhs_domain_min <= expr <= rhs_domain_max.
261// Requires expr offset to be 0.
262void AppendEnforcedLinearExpression(
263 const std::vector<Literal>& enforcing_literals,
264 const LinearExpression& expr, const IntegerValue rhs_domain_min,
265 const IntegerValue rhs_domain_max, const Model& model,
266 LinearRelaxation* relaxation) {
267 CHECK_EQ(expr.offset, IntegerValue(0));
268 const LinearExpression canonical_expr = CanonicalizeExpr(expr);
269 const IntegerTrail* integer_trail = model.Get<IntegerTrail>();
270 const IntegerValue min_expr_value =
271 LinExprLowerBound(canonical_expr, *integer_trail);
272
273 if (rhs_domain_min > min_expr_value) {
274 // And(ei) => terms >= rhs_domain_min
275 // <=> Sum_i (~ei * (rhs_domain_min - min_expr_value)) + terms >=
276 // rhs_domain_min
277 LinearConstraintBuilder lc(&model, rhs_domain_min, kMaxIntegerValue);
278 for (const Literal& literal : enforcing_literals) {
279 CHECK(lc.AddLiteralTerm(literal.Negated(),
280 rhs_domain_min - min_expr_value));
281 }
282 for (int i = 0; i < canonical_expr.vars.size(); i++) {
283 lc.AddTerm(canonical_expr.vars[i], canonical_expr.coeffs[i]);
284 }
285 relaxation->linear_constraints.push_back(lc.Build());
286 }
287 const IntegerValue max_expr_value =
288 LinExprUpperBound(canonical_expr, *integer_trail);
289 if (rhs_domain_max < max_expr_value) {
290 // And(ei) => terms <= rhs_domain_max
291 // <=> Sum_i (~ei * (rhs_domain_max - max_expr_value)) + terms <=
292 // rhs_domain_max
293 LinearConstraintBuilder lc(&model, kMinIntegerValue, rhs_domain_max);
294 for (const Literal& literal : enforcing_literals) {
295 CHECK(lc.AddLiteralTerm(literal.Negated(),
296 rhs_domain_max - max_expr_value));
297 }
298 for (int i = 0; i < canonical_expr.vars.size(); i++) {
299 lc.AddTerm(canonical_expr.vars[i], canonical_expr.coeffs[i]);
300 }
301 relaxation->linear_constraints.push_back(lc.Build());
302 }
303}
304
305bool AllLiteralsHaveViews(const IntegerEncoder& encoder,
306 const std::vector<Literal>& literals) {
307 for (const Literal lit : literals) {
308 if (!encoder.LiteralOrNegationHasView(lit)) return false;
309 }
310 return true;
311}
312
313} // namespace
314
315// Add a linear relaxation of the CP constraint to the set of linear
316// constraints. The highest linearization_level is, the more types of constraint
317// we encode. This method should be called only for linearization_level > 0.
318//
319// Note: IntProd is linearized dynamically using the cut generators.
320//
321// TODO(user): In full generality, we could encode all the constraint as an LP.
322// TODO(user,user): Add unit tests for this method.
323void TryToLinearizeConstraint(const CpModelProto& model_proto,
324 const ConstraintProto& ct, Model* model,
325 int linearization_level,
326 LinearRelaxation* relaxation) {
327 CHECK_EQ(model->GetOrCreate<SatSolver>()->CurrentDecisionLevel(), 0);
328 DCHECK_GT(linearization_level, 0);
329 auto* mapping = model->GetOrCreate<CpModelMapping>();
330 const auto& encoder = *model->GetOrCreate<IntegerEncoder>();
331 if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
332 if (linearization_level < 2) return;
333 LinearConstraintBuilder lc(model, IntegerValue(1), kMaxIntegerValue);
334 for (const int enforcement_ref : ct.enforcement_literal()) {
335 CHECK(lc.AddLiteralTerm(mapping->Literal(NegatedRef(enforcement_ref)),
336 IntegerValue(1)));
337 }
338 for (const int ref : ct.bool_or().literals()) {
339 CHECK(lc.AddLiteralTerm(mapping->Literal(ref), IntegerValue(1)));
340 }
341 relaxation->linear_constraints.push_back(lc.Build());
342 } else if (ct.constraint_case() ==
343 ConstraintProto::ConstraintCase::kBoolAnd) {
344 // TODO(user): These constraints can be many, and if they are not regrouped
345 // in big at most ones, then they should probably only added lazily as cuts.
346 // Regroup this with future clique-cut separation logic.
347 if (linearization_level < 2) return;
348 if (!HasEnforcementLiteral(ct)) return;
349 if (ct.enforcement_literal().size() == 1) {
350 const Literal enforcement = mapping->Literal(ct.enforcement_literal(0));
351 for (const int ref : ct.bool_and().literals()) {
352 relaxation->at_most_ones.push_back(
353 {enforcement, mapping->Literal(ref).Negated()});
354 }
355 return;
356 }
357
358 // Andi(e_i) => Andj(x_j)
359 // <=> num_rhs_terms <= Sum_j(x_j) + num_rhs_terms * Sum_i(~e_i)
360 int num_literals = ct.bool_and().literals_size();
361 LinearConstraintBuilder lc(model, IntegerValue(num_literals),
363 for (const int ref : ct.bool_and().literals()) {
364 CHECK(lc.AddLiteralTerm(mapping->Literal(ref), IntegerValue(1)));
365 }
366 for (const int enforcement_ref : ct.enforcement_literal()) {
367 CHECK(lc.AddLiteralTerm(mapping->Literal(NegatedRef(enforcement_ref)),
368 IntegerValue(num_literals)));
369 }
370 relaxation->linear_constraints.push_back(lc.Build());
371 } else if (ct.constraint_case() ==
372 ConstraintProto::ConstraintCase::kAtMostOne) {
373 if (HasEnforcementLiteral(ct)) return;
374 relaxation->at_most_ones.push_back(
375 mapping->Literals(ct.at_most_one().literals()));
376 } else if (ct.constraint_case() ==
377 ConstraintProto::ConstraintCase::kExactlyOne) {
378 if (HasEnforcementLiteral(ct)) return;
379 const std::vector<Literal> literals =
380 mapping->Literals(ct.exactly_one().literals());
381 if (linearization_level >= 2 || AllLiteralsHaveViews(encoder, literals)) {
382 LinearConstraintBuilder lc(model, IntegerValue(1), IntegerValue(1));
383 for (const Literal lit : literals) {
384 CHECK(lc.AddLiteralTerm(lit, IntegerValue(1)));
385 }
386 relaxation->linear_constraints.push_back(lc.Build());
387 } else if (linearization_level == 1) {
388 // We just encode the at most one part that might be partially linearized
389 // later.
390 relaxation->at_most_ones.push_back(literals);
391 }
392 } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMax) {
393 if (HasEnforcementLiteral(ct)) return;
394 const IntegerVariable target = mapping->Integer(ct.int_max().target());
395 const std::vector<IntegerVariable> vars =
396 mapping->Integers(ct.int_max().vars());
397 AppendMaxRelaxation(target, vars, linearization_level, model, relaxation);
398
399 } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMin) {
400 if (HasEnforcementLiteral(ct)) return;
401 const IntegerVariable negative_target =
402 NegationOf(mapping->Integer(ct.int_min().target()));
403 const std::vector<IntegerVariable> negative_vars =
404 NegationOf(mapping->Integers(ct.int_min().vars()));
405 AppendMaxRelaxation(negative_target, negative_vars, linearization_level,
406 model, relaxation);
407 } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
408 AppendLinearConstraintRelaxation(ct, linearization_level, *model,
409 relaxation);
410 } else if (ct.constraint_case() ==
411 ConstraintProto::ConstraintCase::kCircuit) {
412 if (HasEnforcementLiteral(ct)) return;
413 const int num_arcs = ct.circuit().literals_size();
414 CHECK_EQ(num_arcs, ct.circuit().tails_size());
415 CHECK_EQ(num_arcs, ct.circuit().heads_size());
416
417 // Each node must have exactly one incoming and one outgoing arc (note that
418 // it can be the unique self-arc of this node too).
419 std::map<int, std::vector<Literal>> incoming_arc_constraints;
420 std::map<int, std::vector<Literal>> outgoing_arc_constraints;
421 for (int i = 0; i < num_arcs; i++) {
422 const Literal arc = mapping->Literal(ct.circuit().literals(i));
423 const int tail = ct.circuit().tails(i);
424 const int head = ct.circuit().heads(i);
425
426 // Make sure this literal has a view.
428 outgoing_arc_constraints[tail].push_back(arc);
429 incoming_arc_constraints[head].push_back(arc);
430 }
431 for (const auto* node_map :
432 {&outgoing_arc_constraints, &incoming_arc_constraints}) {
433 for (const auto& entry : *node_map) {
434 const std::vector<Literal>& exactly_one = entry.second;
435 if (exactly_one.size() > 1) {
436 LinearConstraintBuilder at_least_one_lc(model, IntegerValue(1),
438 for (const Literal l : exactly_one) {
439 CHECK(at_least_one_lc.AddLiteralTerm(l, IntegerValue(1)));
440 }
441
442 // We separate the two constraints.
443 relaxation->at_most_ones.push_back(exactly_one);
444 relaxation->linear_constraints.push_back(at_least_one_lc.Build());
445 }
446 }
447 }
448 } else if (ct.constraint_case() ==
449 ConstraintProto::ConstraintCase::kElement) {
450 const IntegerVariable index = mapping->Integer(ct.element().index());
451 const IntegerVariable target = mapping->Integer(ct.element().target());
452 const std::vector<IntegerVariable> vars =
453 mapping->Integers(ct.element().vars());
454
455 // We only relax the case where all the vars are constant.
456 // target = sum (index == i) * fixed_vars[i].
457 LinearConstraintBuilder constraint(model, IntegerValue(0), IntegerValue(0));
458 constraint.AddTerm(target, IntegerValue(-1));
459 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
460 for (const auto literal_value : model->Add(FullyEncodeVariable((index)))) {
461 const IntegerVariable var = vars[literal_value.value.value()];
462 if (!model->Get(IsFixed(var))) return;
463
464 // Make sure this literal has a view.
465 model->Add(NewIntegerVariableFromLiteral(literal_value.literal));
466 CHECK(constraint.AddLiteralTerm(literal_value.literal,
467 integer_trail->LowerBound(var)));
468 }
469
470 relaxation->linear_constraints.push_back(constraint.Build());
471 } else if (ct.constraint_case() ==
472 ConstraintProto::ConstraintCase::kInterval) {
473 // If the interval is using views, then the linear equation is already
474 // present in the model.
475 if (linearization_level < 2) return;
476 if (ct.interval().has_start_view()) return;
477 const IntegerVariable start = mapping->Integer(ct.interval().start());
478 const IntegerVariable size = mapping->Integer(ct.interval().size());
479 const IntegerVariable end = mapping->Integer(ct.interval().end());
480 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
481 const bool size_is_fixed = integer_trail->IsFixed(size);
482 const IntegerValue rhs =
483 size_is_fixed ? -integer_trail->LowerBound(size) : IntegerValue(0);
484 LinearConstraintBuilder lc(model, rhs, rhs);
485 lc.AddTerm(start, IntegerValue(1));
486 if (!size_is_fixed) {
487 lc.AddTerm(size, IntegerValue(1));
488 }
489 lc.AddTerm(end, IntegerValue(-1));
491 LinearConstraint tmp_lc = lc.Build();
492 LinearExpression expr;
493 expr.coeffs = tmp_lc.coeffs;
494 expr.vars = tmp_lc.vars;
495 AppendEnforcedLinearExpression(
496 mapping->Literals(ct.enforcement_literal()), expr, tmp_lc.ub,
497 tmp_lc.ub, *model, relaxation);
498 } else {
499 relaxation->linear_constraints.push_back(lc.Build());
500 }
501 } else if (ct.constraint_case() ==
502 ConstraintProto::ConstraintCase::kNoOverlap) {
503 AppendNoOverlapRelaxation(model_proto, ct, linearization_level, model,
504 relaxation);
505 } else if (ct.constraint_case() ==
506 ConstraintProto::ConstraintCase::kCumulative) {
507 AppendCumulativeRelaxation(model_proto, ct, linearization_level, model,
508 relaxation);
509 }
510}
511
512// TODO(user): Use affine demand.
513void AddCumulativeCut(const std::vector<IntervalVariable>& intervals,
514 const std::vector<IntegerVariable>& demands,
515 IntegerValue capacity_upper_bound, Model* model,
516 LinearRelaxation* relaxation) {
517 // TODO(user): Keep a map intervals -> helper, or ct_index->helper to avoid
518 // creating many helpers for the same constraint.
519 auto* helper = new SchedulingConstraintHelper(intervals, model);
520 model->TakeOwnership(helper);
521 const int num_intervals = helper->NumTasks();
522
523 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
524
525 IntegerValue min_of_starts = kMaxIntegerValue;
526 IntegerValue max_of_ends = kMinIntegerValue;
527
528 int num_variable_sizes = 0;
529 int num_optionals = 0;
530
531 for (int index = 0; index < num_intervals; ++index) {
532 min_of_starts = std::min(min_of_starts, helper->StartMin(index));
533 max_of_ends = std::max(max_of_ends, helper->EndMax(index));
534
535 if (helper->IsOptional(index)) {
536 num_optionals++;
537 }
538
539 if (!helper->SizeIsFixed(index) ||
540 (!demands.empty() && !integer_trail->IsFixed(demands[index]))) {
541 num_variable_sizes++;
542 }
543 }
544
545 VLOG(2) << "Span [" << min_of_starts << ".." << max_of_ends << "] with "
546 << num_optionals << " optional intervals, and " << num_variable_sizes
547 << " variable size intervals out of " << num_intervals
548 << " intervals";
549
550 if (num_variable_sizes + num_optionals == 0) return;
551
552 const IntegerVariable span_start =
553 integer_trail->AddIntegerVariable(min_of_starts, max_of_ends);
554 const IntegerVariable span_size = integer_trail->AddIntegerVariable(
555 IntegerValue(0), max_of_ends - min_of_starts);
556 const IntegerVariable span_end =
557 integer_trail->AddIntegerVariable(min_of_starts, max_of_ends);
558
559 IntervalVariable span_var;
560 if (num_optionals < num_intervals) {
561 span_var = model->Add(NewInterval(span_start, span_end, span_size));
562 } else {
563 const Literal span_lit = Literal(model->Add(NewBooleanVariable()), true);
564 span_var = model->Add(
565 NewOptionalInterval(span_start, span_end, span_size, span_lit));
566 }
567
568 model->Add(SpanOfIntervals(span_var, intervals));
569
570 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
571 lc.AddTerm(span_size, -capacity_upper_bound);
572 for (int i = 0; i < num_intervals; ++i) {
573 const IntegerValue demand_lower_bound =
574 demands.empty() ? IntegerValue(1)
575 : integer_trail->LowerBound(demands[i]);
576 const bool demand_is_fixed =
577 demands.empty() || integer_trail->IsFixed(demands[i]);
578 if (!helper->IsOptional(i)) {
579 if (helper->SizeIsFixed(i) && !demands.empty()) {
580 lc.AddTerm(demands[i], helper->SizeMin(i));
581 } else if (demand_is_fixed) {
582 lc.AddTerm(helper->Sizes()[i], demand_lower_bound);
583 } else { // demand and size are not fixed.
584 DCHECK(!demands.empty());
585 // We use McCormick equation.
586 // demand * size = (demand_min + delta_d) * (size_min + delta_s) =
587 // demand_min * size_min + delta_d * size_min +
588 // delta_s * demand_min + delta_s * delta_d
589 // which is >= (by ignoring the quatratic term)
590 // demand_min * size + size_min * demand - demand_min * size_min
591 lc.AddTerm(helper->Sizes()[i], demand_lower_bound);
592 lc.AddTerm(demands[i], helper->SizeMin(i));
593 lc.AddConstant(-helper->SizeMin(i) * demand_lower_bound);
594 }
595 } else {
596 if (!lc.AddLiteralTerm(helper->PresenceLiteral(i),
597 helper->SizeMin(i) * demand_lower_bound)) {
598 return;
599 }
600 }
601 }
602 relaxation->linear_constraints.push_back(lc.Build());
603}
604
606 const ConstraintProto& ct,
607 int linearization_level, Model* model,
608 LinearRelaxation* relaxation) {
609 CHECK(ct.has_cumulative());
610 if (linearization_level < 2) return;
611 if (HasEnforcementLiteral(ct)) return;
612
613 auto* mapping = model->GetOrCreate<CpModelMapping>();
614 const std::vector<IntegerVariable> demands =
615 mapping->Integers(ct.cumulative().demands());
616 std::vector<IntervalVariable> intervals =
617 mapping->Intervals(ct.cumulative().intervals());
618 const IntegerValue capacity_upper_bound =
619 model->GetOrCreate<IntegerTrail>()->UpperBound(
620 mapping->Integer(ct.cumulative().capacity()));
621 AddCumulativeCut(intervals, demands, capacity_upper_bound, model, relaxation);
622}
623
624void AppendNoOverlapRelaxation(const CpModelProto& model_proto,
625 const ConstraintProto& ct,
626 int linearization_level, Model* model,
627 LinearRelaxation* relaxation) {
628 CHECK(ct.has_no_overlap());
629 if (linearization_level < 2) return;
630 if (HasEnforcementLiteral(ct)) return;
631
632 auto* mapping = model->GetOrCreate<CpModelMapping>();
633 std::vector<IntervalVariable> intervals =
634 mapping->Intervals(ct.no_overlap().intervals());
635 AddCumulativeCut(intervals, /*demands=*/{},
636 /*capacity_upper_bound=*/IntegerValue(1), model, relaxation);
637}
638
639void AppendMaxRelaxation(IntegerVariable target,
640 const std::vector<IntegerVariable>& vars,
641 int linearization_level, Model* model,
642 LinearRelaxation* relaxation) {
643 // Case X = max(X_1, X_2, ..., X_N)
644 // Part 1: Encode X >= max(X_1, X_2, ..., X_N)
645 for (const IntegerVariable var : vars) {
646 // This deal with the corner case X = max(X, Y, Z, ..) !
647 // Note that this can be presolved into X >= Y, X >= Z, ...
648 if (target == var) continue;
649 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
650 lc.AddTerm(var, IntegerValue(1));
651 lc.AddTerm(target, IntegerValue(-1));
652 relaxation->linear_constraints.push_back(lc.Build());
653 }
654
655 // Part 2: Encode upper bound on X.
656 if (linearization_level < 2) return;
657 GenericLiteralWatcher* watcher = model->GetOrCreate<GenericLiteralWatcher>();
658 // For size = 2, we do this with 1 less variable.
659 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
660 if (vars.size() == 2) {
661 IntegerVariable y = model->Add(NewIntegerVariable(0, 1));
662 const Literal y_lit =
663 encoder->GetOrCreateLiteralAssociatedToEquality(y, IntegerValue(1));
664 AppendEnforcedUpperBound(y_lit, target, vars[0], model, relaxation);
665
666 // TODO(user,user): It makes more sense to use ConditionalLowerOrEqual()
667 // here, but that degrades perf on the road*.fzn problem. Understand why.
668 IntegerSumLE* upper_bound1 = new IntegerSumLE(
669 {y_lit}, {target, vars[0]}, {IntegerValue(1), IntegerValue(-1)},
670 IntegerValue(0), model);
671 upper_bound1->RegisterWith(watcher);
672 model->TakeOwnership(upper_bound1);
673 AppendEnforcedUpperBound(y_lit.Negated(), target, vars[1], model,
674 relaxation);
675 IntegerSumLE* upper_bound2 = new IntegerSumLE(
676 {y_lit.Negated()}, {target, vars[1]},
677 {IntegerValue(1), IntegerValue(-1)}, IntegerValue(0), model);
678 upper_bound2->RegisterWith(watcher);
679 model->TakeOwnership(upper_bound2);
680 return;
681 }
682 // For each X_i, we encode y_i => X <= X_i. And at least one of the y_i is
683 // true. Note that the correct y_i will be chosen because of the first part in
684 // linearlization (X >= X_i).
685 // TODO(user): Only lower bound is needed, experiment.
686 LinearConstraintBuilder lc_exactly_one(model, IntegerValue(1),
687 IntegerValue(1));
688 std::vector<Literal> exactly_one_literals;
689 exactly_one_literals.reserve(vars.size());
690 for (const IntegerVariable var : vars) {
691 if (target == var) continue;
692 // y => X <= X_i.
693 // <=> max_term_value * y + X - X_i <= max_term_value.
694 // where max_tern_value is X_ub - X_i_lb.
695 IntegerVariable y = model->Add(NewIntegerVariable(0, 1));
696 const Literal y_lit =
697 encoder->GetOrCreateLiteralAssociatedToEquality(y, IntegerValue(1));
698
699 AppendEnforcedUpperBound(y_lit, target, var, model, relaxation);
700 IntegerSumLE* upper_bound_constraint = new IntegerSumLE(
701 {y_lit}, {target, var}, {IntegerValue(1), IntegerValue(-1)},
702 IntegerValue(0), model);
703 upper_bound_constraint->RegisterWith(watcher);
704 model->TakeOwnership(upper_bound_constraint);
705 exactly_one_literals.push_back(y_lit);
706
707 CHECK(lc_exactly_one.AddLiteralTerm(y_lit, IntegerValue(1)));
708 }
709 model->Add(ExactlyOneConstraint(exactly_one_literals));
710 relaxation->linear_constraints.push_back(lc_exactly_one.Build());
711}
712
713std::vector<IntegerVariable> AppendLinMaxRelaxation(
714 IntegerVariable target, const std::vector<LinearExpression>& exprs,
715 Model* model, LinearRelaxation* relaxation) {
716 // We want to linearize X = max(exprs[1], exprs[2], ..., exprs[d]).
717 // Part 1: Encode X >= max(exprs[1], exprs[2], ..., exprs[d])
718 for (const LinearExpression& expr : exprs) {
720 for (int i = 0; i < expr.vars.size(); ++i) {
721 lc.AddTerm(expr.vars[i], expr.coeffs[i]);
722 }
723 lc.AddTerm(target, IntegerValue(-1));
724 relaxation->linear_constraints.push_back(lc.Build());
725 }
726
727 // Part 2: Encode upper bound on X.
728
729 // Add linking constraint to the CP solver
730 // sum zi = 1 and for all i, zi => max = expr_i.
731 const int num_exprs = exprs.size();
732 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
733 GenericLiteralWatcher* watcher = model->GetOrCreate<GenericLiteralWatcher>();
734
735 // TODO(user): For the case where num_exprs = 2, Create only one z var.
736 std::vector<IntegerVariable> z_vars;
737 std::vector<Literal> z_lits;
738 z_vars.reserve(num_exprs);
739 z_lits.reserve(num_exprs);
740 LinearConstraintBuilder lc_exactly_one(model, IntegerValue(1),
741 IntegerValue(1));
742 std::vector<Literal> exactly_one_literals;
743 for (int i = 0; i < num_exprs; ++i) {
744 IntegerVariable z = model->Add(NewIntegerVariable(0, 1));
745 z_vars.push_back(z);
746 const Literal z_lit =
747 encoder->GetOrCreateLiteralAssociatedToEquality(z, IntegerValue(1));
748 z_lits.push_back(z_lit);
749 LinearExpression local_expr;
750 local_expr.vars = NegationOf(exprs[i].vars);
751 local_expr.vars.push_back(target);
752 local_expr.coeffs = exprs[i].coeffs;
753 local_expr.coeffs.push_back(IntegerValue(1));
754 IntegerSumLE* upper_bound = new IntegerSumLE(
755 {z_lit}, local_expr.vars, local_expr.coeffs, exprs[i].offset, model);
756 upper_bound->RegisterWith(watcher);
757 model->TakeOwnership(upper_bound);
758
759 CHECK(lc_exactly_one.AddLiteralTerm(z_lit, IntegerValue(1)));
760 }
761 model->Add(ExactlyOneConstraint(z_lits));
762
763 // For the relaxation, we use different constraints with a stronger linear
764 // relaxation as explained in the .h
765 // TODO(user): Consider passing the x_vars to this method instead of
766 // computing it here.
767 std::vector<IntegerVariable> x_vars;
768 for (int i = 0; i < num_exprs; ++i) {
769 x_vars.insert(x_vars.end(), exprs[i].vars.begin(), exprs[i].vars.end());
770 }
772 // All expressions should only contain positive variables.
773 DCHECK(std::all_of(x_vars.begin(), x_vars.end(), [](IntegerVariable var) {
774 return VariableIsPositive(var);
775 }));
776
777 std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
778 num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
779
780 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
781 for (int i = 0; i < num_exprs; ++i) {
782 for (int j = 0; j < num_exprs; ++j) {
783 if (i == j) continue;
784 for (const IntegerVariable x_var : x_vars) {
785 const IntegerValue lb = integer_trail->LevelZeroLowerBound(x_var);
786 const IntegerValue ub = integer_trail->LevelZeroUpperBound(x_var);
787 const IntegerValue diff =
788 GetCoefficient(x_var, exprs[j]) - GetCoefficient(x_var, exprs[i]);
789 sum_of_max_corner_diff[i][j] += std::max(diff * lb, diff * ub);
790 }
791 }
792 }
793 for (int i = 0; i < num_exprs; ++i) {
794 LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
795 lc.AddTerm(target, IntegerValue(1));
796 for (int j = 0; j < exprs[i].vars.size(); ++j) {
797 lc.AddTerm(exprs[i].vars[j], -exprs[i].coeffs[j]);
798 }
799 for (int j = 0; j < num_exprs; ++j) {
800 CHECK(lc.AddLiteralTerm(z_lits[j],
801 -exprs[j].offset - sum_of_max_corner_diff[i][j]));
802 }
803 relaxation->linear_constraints.push_back(lc.Build());
804 }
805
806 relaxation->linear_constraints.push_back(lc_exactly_one.Build());
807 return z_vars;
808}
809
810void AppendLinearConstraintRelaxation(const ConstraintProto& constraint_proto,
811 const int linearization_level,
812 const Model& model,
813 LinearRelaxation* relaxation) {
814 auto* mapping = model.Get<CpModelMapping>();
815
816 // Note that we ignore the holes in the domain.
817 //
818 // TODO(user): In LoadLinearConstraint() we already created intermediate
819 // Booleans for each disjoint interval, we should reuse them here if
820 // possible.
821 //
822 // TODO(user): process the "at most one" part of a == 1 separately?
823 const IntegerValue rhs_domain_min =
824 IntegerValue(constraint_proto.linear().domain(0));
825 const IntegerValue rhs_domain_max =
826 IntegerValue(constraint_proto.linear().domain(
827 constraint_proto.linear().domain_size() - 1));
828 if (rhs_domain_min == kint64min && rhs_domain_max == kint64max) return;
829
830 if (!HasEnforcementLiteral(constraint_proto)) {
831 LinearConstraintBuilder lc(&model, rhs_domain_min, rhs_domain_max);
832 for (int i = 0; i < constraint_proto.linear().vars_size(); i++) {
833 const int ref = constraint_proto.linear().vars(i);
834 const int64 coeff = constraint_proto.linear().coeffs(i);
835 lc.AddTerm(mapping->Integer(ref), IntegerValue(coeff));
836 }
837 relaxation->linear_constraints.push_back(lc.Build());
838 return;
839 }
840
841 // Reified version.
842 if (linearization_level < 2) return;
843
844 // We linearize fully reified constraints of size 1 all together for a given
845 // variable. But we need to process half-reified ones.
846 if (!mapping->IsHalfEncodingConstraint(&constraint_proto) &&
847 constraint_proto.linear().vars_size() <= 1) {
848 return;
849 }
850
851 std::vector<Literal> enforcing_literals;
852 enforcing_literals.reserve(constraint_proto.enforcement_literal_size());
853 for (const int enforcement_ref : constraint_proto.enforcement_literal()) {
854 enforcing_literals.push_back(mapping->Literal(enforcement_ref));
855 }
856 LinearExpression expr;
857 expr.vars.reserve(constraint_proto.linear().vars_size());
858 expr.coeffs.reserve(constraint_proto.linear().vars_size());
859 for (int i = 0; i < constraint_proto.linear().vars_size(); i++) {
860 int ref = constraint_proto.linear().vars(i);
861 IntegerValue coeff(constraint_proto.linear().coeffs(i));
862 if (!RefIsPositive(ref)) {
863 ref = PositiveRef(ref);
864 coeff = -coeff;
865 }
866 const IntegerVariable int_var = mapping->Integer(ref);
867 expr.vars.push_back(int_var);
868 expr.coeffs.push_back(coeff);
869 }
870 AppendEnforcedLinearExpression(enforcing_literals, expr, rhs_domain_min,
871 rhs_domain_max, model, relaxation);
872}
873
874} // namespace sat
875} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
std::vector< IntegerVariable > Integers(const List &list) const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
Definition: integer.cc:248
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
Definition: integer.cc:106
void RegisterWith(GenericLiteralWatcher *watcher)
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition: integer.h:1355
IntegerVariable AddIntegerVariable(IntegerValue lower_bound, IntegerValue upper_bound)
Definition: integer.cc:603
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1350
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff)
void AddTerm(IntegerVariable var, IntegerValue coeff)
Literal(int signed_value)
Definition: sat_base.h:68
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
CpModelProto const * model_proto
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
bool HasEnforcementLiteral(const ConstraintProto &ct)
std::vector< IntegerVariable > AppendLinMaxRelaxation(IntegerVariable target, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
Definition: intervals.h:662
void AppendLinearConstraintRelaxation(const ConstraintProto &constraint_proto, const int linearization_level, const Model &model, LinearRelaxation *relaxation)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
Definition: integer.h:1587
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
Definition: integer.h:1444
bool AppendFullEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1467
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
const IntegerVariable kNoIntegerVariable(-1)
LinearExpression CanonicalizeExpr(const LinearExpression &expr)
void AppendMaxRelaxation(IntegerVariable target, const std::vector< IntegerVariable > &vars, int linearization_level, Model *model, LinearRelaxation *relaxation)
void AddCumulativeCut(const std::vector< IntervalVariable > &intervals, const std::vector< IntegerVariable > &demands, IntegerValue capacity_upper_bound, Model *model, LinearRelaxation *relaxation)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1426
IntegerValue GetCoefficient(const IntegerVariable var, const LinearExpression &expr)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
Definition: intervals.h:632
void TryToLinearizeConstraint(const CpModelProto &model_proto, const ConstraintProto &ct, Model *model, int linearization_level, LinearRelaxation *relaxation)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1479
void AppendPartialEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> SpanOfIntervals(IntervalVariable span, const std::vector< IntervalVariable > &intervals)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:876
void AppendNoOverlapRelaxation(const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
void AppendCumulativeRelaxation(const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
bool RefIsPositive(int ref)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 delta
Definition: resource.cc:1684
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
std::vector< IntegerVariable > vars
std::vector< std::vector< Literal > > at_most_ones
std::vector< LinearConstraint > linear_constraints