OR-Tools  8.2
integer_expr.h
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14#ifndef OR_TOOLS_SAT_INTEGER_EXPR_H_
15#define OR_TOOLS_SAT_INTEGER_EXPR_H_
16
17#include <functional>
18#include <vector>
19
23#include "ortools/base/macros.h"
25#include "ortools/sat/integer.h"
27#include "ortools/sat/model.h"
31#include "ortools/util/rev.h"
32
33namespace operations_research {
34namespace sat {
35
36// A really basic implementation of an upper-bounded sum of integer variables.
37// The complexity is in O(num_variables) at each propagation.
38//
39// Note that we assume that there can be NO integer overflow. This must be
40// checked at model validation time before this is even created.
41//
42// TODO(user): If one has many such constraint, it will be more efficient to
43// propagate all of them at once rather than doing it one at the time.
44//
45// TODO(user): Explore tree structure to get a log(n) complexity.
46//
47// TODO(user): When the variables are Boolean, use directly the pseudo-Boolean
48// constraint implementation. But we do need support for enforcement literals
49// there.
51 public:
52 // If refied_literal is kNoLiteralIndex then this is a normal constraint,
53 // otherwise we enforce the implication refied_literal => constraint is true.
54 // Note that we don't do the reverse implication here, it is usually done by
55 // another IntegerSumLE constraint on the negated variables.
56 IntegerSumLE(const std::vector<Literal>& enforcement_literals,
57 const std::vector<IntegerVariable>& vars,
58 const std::vector<IntegerValue>& coeffs,
59 IntegerValue upper_bound, Model* model);
60
61 // We propagate:
62 // - If the sum of the individual lower-bound is > upper_bound, we fail.
63 // - For all i, upper-bound of i
64 // <= upper_bound - Sum {individual lower-bound excluding i).
65 bool Propagate() final;
67
68 // Same as Propagate() but only consider current root level bounds. This is
69 // mainly useful for the LP propagator since it can find relevant optimal
70 // really late in the search tree.
72
73 private:
74 // Fills integer_reason_ with all the current lower_bounds. The real
75 // explanation may require removing one of them, but as an optimization, we
76 // always keep all the IntegerLiteral in integer_reason_, and swap them as
77 // needed just before pushing something.
78 void FillIntegerReason();
79
80 const std::vector<Literal> enforcement_literals_;
81 const IntegerValue upper_bound_;
82
83 Trail* trail_;
84 IntegerTrail* integer_trail_;
85 TimeLimit* time_limit_;
86 RevIntegerValueRepository* rev_integer_value_repository_;
87
88 // Reversible sum of the lower bound of the fixed variables.
89 bool is_registered_ = false;
90 IntegerValue rev_lb_fixed_vars_;
91
92 // Reversible number of fixed variables.
93 int rev_num_fixed_vars_;
94
95 // Those vectors are shuffled during search to ensure that the variables
96 // (resp. coefficients) contained in the range [0, rev_num_fixed_vars_) of
97 // vars_ (resp. coeffs_) are fixed (resp. belong to fixed variables).
98 std::vector<IntegerVariable> vars_;
99 std::vector<IntegerValue> coeffs_;
100 std::vector<IntegerValue> max_variations_;
101
102 std::vector<Literal> literal_reason_;
103
104 // Parallel vectors.
105 std::vector<IntegerLiteral> integer_reason_;
106 std::vector<IntegerValue> reason_coeffs_;
107
108 DISALLOW_COPY_AND_ASSIGN(IntegerSumLE);
109};
110
111// This assumes target = SUM_i coeffs[i] * vars[i], and detects that the target
112// must be of the form (a*X + b).
113//
114// This propagator is quite specific and runs only at level zero. For now, this
115// is mainly used for the objective variable. As we fix terms with high
116// objective coefficient, it is possible the only terms left have a common
117// divisor. This close app2-2.mps in less than a second instead of running
118// forever to prove the optimal (in single thread).
120 public:
121 LevelZeroEquality(IntegerVariable target,
122 const std::vector<IntegerVariable>& vars,
123 const std::vector<IntegerValue>& coeffs, Model* model);
124
125 bool Propagate() final;
126
127 private:
128 const IntegerVariable target_;
129 const std::vector<IntegerVariable> vars_;
130 const std::vector<IntegerValue> coeffs_;
131
132 IntegerValue gcd_ = IntegerValue(1);
133
134 Trail* trail_;
135 IntegerTrail* integer_trail_;
136};
137
138// A min (resp max) contraint of the form min == MIN(vars) can be decomposed
139// into two inequalities:
140// 1/ min <= MIN(vars), which is the same as for all v in vars, "min <= v".
141// This can be taken care of by the LowerOrEqual(min, v) constraint.
142// 2/ min >= MIN(vars).
143//
144// And in turn, 2/ can be decomposed in:
145// a) lb(min) >= lb(MIN(vars)) = MIN(lb(var));
146// b) ub(min) >= ub(MIN(vars)) and we can't propagate anything here unless
147// there is just one possible variable 'v' that can be the min:
148// for all u != v, lb(u) > ub(min);
149// In this case, ub(min) >= ub(v).
150//
151// This constraint take care of a) and b). That is:
152// - If the min of the lower bound of the vars increase, then the lower bound of
153// the min_var will be >= to it.
154// - If there is only one candidate for the min, then if the ub(min) decrease,
155// the ub of the only candidate will be <= to it.
156//
157// Complexity: This is a basic implementation in O(num_vars) on each call to
158// Propagate(), which will happen each time one or more variables in vars_
159// changed.
160//
161// TODO(user): Implement a more efficient algorithm when the need arise.
163 public:
164 MinPropagator(const std::vector<IntegerVariable>& vars,
165 IntegerVariable min_var, IntegerTrail* integer_trail);
166
167 bool Propagate() final;
168 void RegisterWith(GenericLiteralWatcher* watcher);
169
170 private:
171 const std::vector<IntegerVariable> vars_;
172 const IntegerVariable min_var_;
173 IntegerTrail* integer_trail_;
174
175 std::vector<IntegerLiteral> integer_reason_;
176
177 DISALLOW_COPY_AND_ASSIGN(MinPropagator);
178};
179
180// Same as MinPropagator except this works on min = MIN(exprs) where exprs are
181// linear expressions. It uses IntegerSumLE to propagate bounds on the exprs.
182// Assumes Canonical expressions (all positive coefficients).
184 public:
185 LinMinPropagator(const std::vector<LinearExpression>& exprs,
186 IntegerVariable min_var, Model* model);
189
190 bool Propagate() final;
191 void RegisterWith(GenericLiteralWatcher* watcher);
192
193 private:
194 // Lighter version of IntegerSumLE. This uses the current value of
195 // integer_reason_ in addition to the reason for propagating the linear
196 // constraint. The coeffs are assumed to be positive here.
197 bool PropagateLinearUpperBound(const std::vector<IntegerVariable>& vars,
198 const std::vector<IntegerValue>& coeffs,
199 IntegerValue upper_bound);
200
201 const std::vector<LinearExpression> exprs_;
202 const IntegerVariable min_var_;
203 std::vector<IntegerValue> expr_lbs_;
204 Model* model_;
205 IntegerTrail* integer_trail_;
206 std::vector<IntegerLiteral> integer_reason_for_unique_candidate_;
207 int rev_unique_candidate_ = 0;
208};
209
210// Propagates a * b = c. Basic version, we don't extract any special cases, and
211// we only propagates the bounds.
212//
213// TODO(user): For now this only works on variables that are non-negative.
214// TODO(user): Deal with overflow.
216 public:
217 PositiveProductPropagator(IntegerVariable a, IntegerVariable b,
218 IntegerVariable p, IntegerTrail* integer_trail);
219
220 bool Propagate() final;
221 void RegisterWith(GenericLiteralWatcher* watcher);
222
223 private:
224 const IntegerVariable a_;
225 const IntegerVariable b_;
226 const IntegerVariable p_;
227 IntegerTrail* integer_trail_;
228
230};
231
232// Propagates a / b = c. Basic version, we don't extract any special cases, and
233// we only propagates the bounds.
234//
235// TODO(user): For now this only works on variables that are non-negative.
236// TODO(user): This only propagate the direction => c, do the reverse.
237// TODO(user): Deal with overflow.
238// TODO(user): Unit-test this like the ProductPropagator.
240 public:
241 DivisionPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable c,
242 IntegerTrail* integer_trail);
243
244 bool Propagate() final;
245 void RegisterWith(GenericLiteralWatcher* watcher);
246
247 private:
248 const IntegerVariable a_;
249 const IntegerVariable b_;
250 const IntegerVariable c_;
251 IntegerTrail* integer_trail_;
252
254};
255
256// Propagates var_a / cst_b = var_c. Basic version, we don't extract any special
257// cases, and we only propagates the bounds. cst_b must be > 0.
259 public:
260 FixedDivisionPropagator(IntegerVariable a, IntegerValue b, IntegerVariable c,
261 IntegerTrail* integer_trail);
262
263 bool Propagate() final;
264 void RegisterWith(GenericLiteralWatcher* watcher);
265
266 private:
267 const IntegerVariable a_;
268 const IntegerValue b_;
269 const IntegerVariable c_;
270 IntegerTrail* integer_trail_;
271
273};
274
275// Propagates x * x = s.
276// TODO(user): Only works for x nonnegative.
278 public:
279 SquarePropagator(IntegerVariable x, IntegerVariable s,
280 IntegerTrail* integer_trail);
281
282 bool Propagate() final;
283 void RegisterWith(GenericLiteralWatcher* watcher);
284
285 private:
286 const IntegerVariable x_;
287 const IntegerVariable s_;
288 IntegerTrail* integer_trail_;
289
291};
292
293// =============================================================================
294// Model based functions.
295// =============================================================================
296
297// Weighted sum <= constant.
298template <typename VectorInt>
299inline std::function<void(Model*)> WeightedSumLowerOrEqual(
300 const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
301 int64 upper_bound) {
302 // Special cases.
303 CHECK_GE(vars.size(), 1);
304 if (vars.size() == 1) {
305 const int64 c = coefficients[0];
306 CHECK_NE(c, 0);
307 if (c > 0) {
308 return LowerOrEqual(
309 vars[0],
310 FloorRatio(IntegerValue(upper_bound), IntegerValue(c)).value());
311 } else {
312 return GreaterOrEqual(
313 vars[0],
314 CeilRatio(IntegerValue(-upper_bound), IntegerValue(-c)).value());
315 }
316 }
317 if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
318 (coefficients[1] == 1 || coefficients[1] == -1)) {
319 return Sum2LowerOrEqual(
320 coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
321 coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound);
322 }
323 if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
324 (coefficients[1] == 1 || coefficients[1] == -1) &&
325 (coefficients[2] == 1 || coefficients[2] == -1)) {
326 return Sum3LowerOrEqual(
327 coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
328 coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
329 coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound);
330 }
331
332 return [=](Model* model) {
333 // We split large constraints into a square root number of parts.
334 // This is to avoid a bad complexity while propagating them since our
335 // algorithm is not in O(num_changes).
336 //
337 // TODO(user): Alternatively, we could use a O(num_changes) propagation (a
338 // bit tricky to implement), or a decomposition into a tree with more than
339 // one level. Both requires experimentations.
340 //
341 // TODO(user): If the initial constraint was an equalilty we will create
342 // the "intermediate" variable twice where we could have use the same for
343 // both direction. Improve?
344 const int num_vars = vars.size();
345 if (num_vars > 100) {
346 std::vector<IntegerVariable> bucket_sum_vars;
347
348 std::vector<IntegerVariable> local_vars;
349 std::vector<IntegerValue> local_coeffs;
350
351 int i = 0;
352 const int num_buckets = static_cast<int>(std::round(std::sqrt(num_vars)));
353 for (int b = 0; b < num_buckets; ++b) {
354 local_vars.clear();
355 local_coeffs.clear();
356 int64 bucket_lb = 0;
357 int64 bucket_ub = 0;
358 const int limit = num_vars * (b + 1);
359 for (; i * num_buckets < limit; ++i) {
360 local_vars.push_back(vars[i]);
361 local_coeffs.push_back(IntegerValue(coefficients[i]));
362 const int64 term1 = model->Get(LowerBound(vars[i])) * coefficients[i];
363 const int64 term2 = model->Get(UpperBound(vars[i])) * coefficients[i];
364 bucket_lb += std::min(term1, term2);
365 bucket_ub += std::max(term1, term2);
366 }
367
368 const IntegerVariable bucket_sum =
369 model->Add(NewIntegerVariable(bucket_lb, bucket_ub));
370 bucket_sum_vars.push_back(bucket_sum);
371 local_vars.push_back(bucket_sum);
372 local_coeffs.push_back(IntegerValue(-1));
373 IntegerSumLE* constraint = new IntegerSumLE(
374 {}, local_vars, local_coeffs, IntegerValue(0), model);
375 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
376 model->TakeOwnership(constraint);
377 }
378
379 // Create the root-level sum.
380 local_vars.clear();
381 local_coeffs.clear();
382 for (const IntegerVariable var : bucket_sum_vars) {
383 local_vars.push_back(var);
384 local_coeffs.push_back(IntegerValue(1));
385 }
386 IntegerSumLE* constraint = new IntegerSumLE(
387 {}, local_vars, local_coeffs, IntegerValue(upper_bound), model);
388 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
389 model->TakeOwnership(constraint);
390 return;
391 }
392
393 IntegerSumLE* constraint = new IntegerSumLE(
394 {}, vars,
395 std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
396 IntegerValue(upper_bound), model);
397 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
398 model->TakeOwnership(constraint);
399 };
400}
401
402// Weighted sum >= constant.
403template <typename VectorInt>
404inline std::function<void(Model*)> WeightedSumGreaterOrEqual(
405 const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
406 int64 lower_bound) {
407 // We just negate everything and use an <= constraints.
408 std::vector<int64> negated_coeffs(coefficients.begin(), coefficients.end());
409 for (int64& ref : negated_coeffs) ref = -ref;
410 return WeightedSumLowerOrEqual(vars, negated_coeffs, -lower_bound);
411}
412
413// Weighted sum == constant.
414template <typename VectorInt>
415inline std::function<void(Model*)> FixedWeightedSum(
416 const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
417 int64 value) {
418 return [=](Model* model) {
421 };
422}
423
424// enforcement_literals => sum <= upper_bound
425template <typename VectorInt>
426inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
427 const std::vector<Literal>& enforcement_literals,
428 const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
429 int64 upper_bound) {
430 // Special cases.
431 CHECK_GE(vars.size(), 1);
432 if (vars.size() == 1) {
433 CHECK_NE(coefficients[0], 0);
434 if (coefficients[0] > 0) {
435 return Implication(
436 enforcement_literals,
438 vars[0], FloorRatio(IntegerValue(upper_bound),
439 IntegerValue(coefficients[0]))));
440 } else {
441 return Implication(
442 enforcement_literals,
444 vars[0], CeilRatio(IntegerValue(-upper_bound),
445 IntegerValue(-coefficients[0]))));
446 }
447 }
448
449 if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
450 (coefficients[1] == 1 || coefficients[1] == -1)) {
452 coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
453 coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound,
454 enforcement_literals);
455 }
456 if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
457 (coefficients[1] == 1 || coefficients[1] == -1) &&
458 (coefficients[2] == 1 || coefficients[2] == -1)) {
460 coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
461 coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
462 coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound,
463 enforcement_literals);
464 }
465
466 return [=](Model* model) {
467 // If value == min(expression), then we can avoid creating the sum.
468 IntegerValue expression_min(0);
469 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
470 for (int i = 0; i < vars.size(); ++i) {
471 expression_min +=
472 coefficients[i] * (coefficients[i] >= 0
473 ? integer_trail->LowerBound(vars[i])
474 : integer_trail->UpperBound(vars[i]));
475 }
476 if (expression_min == upper_bound) {
477 // Tricky: as we create integer literal, we might propagate stuff and
478 // the bounds might change, so if the expression_min increase with the
479 // bound we use, then the literal must be false.
480 IntegerValue non_cached_min;
481 for (int i = 0; i < vars.size(); ++i) {
482 if (coefficients[i] > 0) {
483 const IntegerValue lb = integer_trail->LowerBound(vars[i]);
484 non_cached_min += coefficients[i] * lb;
485 model->Add(Implication(enforcement_literals,
486 IntegerLiteral::LowerOrEqual(vars[i], lb)));
487 } else if (coefficients[i] < 0) {
488 const IntegerValue ub = integer_trail->UpperBound(vars[i]);
489 non_cached_min += coefficients[i] * ub;
490 model->Add(Implication(enforcement_literals,
491 IntegerLiteral::GreaterOrEqual(vars[i], ub)));
492 }
493 }
494 if (non_cached_min > expression_min) {
495 std::vector<Literal> clause;
496 for (const Literal l : enforcement_literals) {
497 clause.push_back(l.Negated());
498 }
499 model->Add(ClauseConstraint(clause));
500 }
501 } else {
502 IntegerSumLE* constraint = new IntegerSumLE(
503 enforcement_literals, vars,
504 std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
505 IntegerValue(upper_bound), model);
506 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
507 model->TakeOwnership(constraint);
508 }
509 };
510}
511
512// enforcement_literals => sum >= lower_bound
513template <typename VectorInt>
514inline std::function<void(Model*)> ConditionalWeightedSumGreaterOrEqual(
515 const std::vector<Literal>& enforcement_literals,
516 const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
517 int64 lower_bound) {
518 // We just negate everything and use an <= constraint.
519 std::vector<int64> negated_coeffs(coefficients.begin(), coefficients.end());
520 for (int64& ref : negated_coeffs) ref = -ref;
521 return ConditionalWeightedSumLowerOrEqual(enforcement_literals, vars,
522 negated_coeffs, -lower_bound);
523}
524
525// Weighted sum <= constant reified.
526template <typename VectorInt>
527inline std::function<void(Model*)> WeightedSumLowerOrEqualReif(
528 Literal is_le, const std::vector<IntegerVariable>& vars,
529 const VectorInt& coefficients, int64 upper_bound) {
530 return [=](Model* model) {
532 upper_bound));
534 {is_le.Negated()}, vars, coefficients, upper_bound + 1));
535 };
536}
537
538// Weighted sum >= constant reified.
539template <typename VectorInt>
540inline std::function<void(Model*)> WeightedSumGreaterOrEqualReif(
541 Literal is_ge, const std::vector<IntegerVariable>& vars,
542 const VectorInt& coefficients, int64 lower_bound) {
543 return [=](Model* model) {
545 lower_bound));
547 {is_ge.Negated()}, vars, coefficients, lower_bound - 1));
548 };
549}
550
551// LinearConstraint version.
553 if (cst.vars.empty()) {
554 if (cst.lb <= 0 && cst.ub >= 0) return;
555 model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
556 return;
557 }
558
559 // TODO(user): Remove the conversion!
560 std::vector<int64> converted_coeffs;
561 for (const IntegerValue v : cst.coeffs) converted_coeffs.push_back(v.value());
562 if (cst.ub < kMaxIntegerValue) {
563 model->Add(
564 WeightedSumLowerOrEqual(cst.vars, converted_coeffs, cst.ub.value()));
565 }
566 if (cst.lb > kMinIntegerValue) {
567 model->Add(
568 WeightedSumGreaterOrEqual(cst.vars, converted_coeffs, cst.lb.value()));
569 }
570}
571
573 const absl::Span<const Literal> enforcement_literals,
574 const LinearConstraint& cst, Model* model) {
575 if (enforcement_literals.empty()) {
576 return LoadLinearConstraint(cst, model);
577 }
578 if (cst.vars.empty()) {
579 if (cst.lb <= 0 && cst.ub >= 0) return;
580 return model->Add(ClauseConstraint(enforcement_literals));
581 }
582
583 // TODO(user): Remove the conversion!
584 std::vector<Literal> converted_literals(enforcement_literals.begin(),
585 enforcement_literals.end());
586 std::vector<int64> converted_coeffs;
587 for (const IntegerValue v : cst.coeffs) converted_coeffs.push_back(v.value());
588
589 if (cst.ub < kMaxIntegerValue) {
591 converted_literals, cst.vars, converted_coeffs, cst.ub.value()));
592 }
593 if (cst.lb > kMinIntegerValue) {
595 converted_literals, cst.vars, converted_coeffs, cst.lb.value()));
596 }
597}
598
599// Weighted sum == constant reified.
600// TODO(user): Simplify if the constant is at the edge of the possible values.
601template <typename VectorInt>
602inline std::function<void(Model*)> FixedWeightedSumReif(
603 Literal is_eq, const std::vector<IntegerVariable>& vars,
604 const VectorInt& coefficients, int64 value) {
605 return [=](Model* model) {
606 // We creates two extra Boolean variables in this case. The alternative is
607 // to code a custom propagator for the direction equality => reified.
608 const Literal is_le = Literal(model->Add(NewBooleanVariable()), true);
609 const Literal is_ge = Literal(model->Add(NewBooleanVariable()), true);
610 model->Add(ReifiedBoolAnd({is_le, is_ge}, is_eq));
613 };
614}
615
616// Weighted sum != constant.
617// TODO(user): Simplify if the constant is at the edge of the possible values.
618template <typename VectorInt>
619inline std::function<void(Model*)> WeightedSumNotEqual(
620 const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
621 int64 value) {
622 return [=](Model* model) {
623 // Exactly one of these alternative must be true.
624 const Literal is_lt = Literal(model->Add(NewBooleanVariable()), true);
625 const Literal is_gt = is_lt.Negated();
627 value - 1));
629 value + 1));
630 };
631}
632
633// Model-based function to create an IntegerVariable that corresponds to the
634// given weighted sum of other IntegerVariables.
635//
636// Note that this is templated so that it can seamlessly accept vector<int> or
637// vector<int64>.
638//
639// TODO(user): invert the coefficients/vars arguments.
640template <typename VectorInt>
641inline std::function<IntegerVariable(Model*)> NewWeightedSum(
642 const VectorInt& coefficients, const std::vector<IntegerVariable>& vars) {
643 return [=](Model* model) {
644 std::vector<IntegerVariable> new_vars = vars;
645 // To avoid overflow in the FixedWeightedSum() constraint, we need to
646 // compute the basic bounds on the sum.
647 //
648 // TODO(user): deal with overflow here too!
649 int64 sum_lb(0);
650 int64 sum_ub(0);
651 for (int i = 0; i < new_vars.size(); ++i) {
652 if (coefficients[i] > 0) {
653 sum_lb += coefficients[i] * model->Get(LowerBound(new_vars[i]));
654 sum_ub += coefficients[i] * model->Get(UpperBound(new_vars[i]));
655 } else {
656 sum_lb += coefficients[i] * model->Get(UpperBound(new_vars[i]));
657 sum_ub += coefficients[i] * model->Get(LowerBound(new_vars[i]));
658 }
659 }
660
661 const IntegerVariable sum = model->Add(NewIntegerVariable(sum_lb, sum_ub));
662 new_vars.push_back(sum);
663 std::vector<int64> new_coeffs(coefficients.begin(), coefficients.end());
664 new_coeffs.push_back(-1);
665 model->Add(FixedWeightedSum(new_vars, new_coeffs, 0));
666 return sum;
667 };
668}
669
670// Expresses the fact that an existing integer variable is equal to the minimum
671// of other integer variables.
672inline std::function<void(Model*)> IsEqualToMinOf(
673 IntegerVariable min_var, const std::vector<IntegerVariable>& vars) {
674 return [=](Model* model) {
675 for (const IntegerVariable& var : vars) {
676 model->Add(LowerOrEqual(min_var, var));
677 }
678
679 MinPropagator* constraint =
680 new MinPropagator(vars, min_var, model->GetOrCreate<IntegerTrail>());
681 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
682 model->TakeOwnership(constraint);
683 };
684}
685
686// Expresses the fact that an existing integer variable is equal to the minimum
687// of linear expressions. Assumes Canonical expressions (all positive
688// coefficients).
689inline std::function<void(Model*)> IsEqualToMinOf(
690 const LinearExpression& min_expr,
691 const std::vector<LinearExpression>& exprs) {
692 return [=](Model* model) {
693 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
694
695 IntegerVariable min_var;
696 if (min_expr.vars.size() == 1 &&
697 std::abs(min_expr.coeffs[0].value()) == 1) {
698 if (min_expr.coeffs[0].value() == 1) {
699 min_var = min_expr.vars[0];
700 } else {
701 min_var = NegationOf(min_expr.vars[0]);
702 }
703 } else {
704 // Create a new variable if the expression is not just a single variable.
705 IntegerValue min_lb = LinExprLowerBound(min_expr, *integer_trail);
706 IntegerValue min_ub = LinExprUpperBound(min_expr, *integer_trail);
707 min_var = integer_trail->AddIntegerVariable(min_lb, min_ub);
708
709 // min_var = min_expr
710 std::vector<IntegerVariable> min_sum_vars = min_expr.vars;
711 std::vector<int64> min_sum_coeffs;
712 for (IntegerValue coeff : min_expr.coeffs) {
713 min_sum_coeffs.push_back(coeff.value());
714 }
715 min_sum_vars.push_back(min_var);
716 min_sum_coeffs.push_back(-1);
717
718 model->Add(FixedWeightedSum(min_sum_vars, min_sum_coeffs,
719 -min_expr.offset.value()));
720 }
721 for (const LinearExpression& expr : exprs) {
722 // min_var <= expr
723 std::vector<IntegerVariable> vars = expr.vars;
724 std::vector<int64> coeffs;
725 for (IntegerValue coeff : expr.coeffs) {
726 coeffs.push_back(coeff.value());
727 }
728 vars.push_back(min_var);
729 coeffs.push_back(-1);
730 model->Add(WeightedSumGreaterOrEqual(vars, coeffs, -expr.offset.value()));
731 }
732
733 LinMinPropagator* constraint = new LinMinPropagator(exprs, min_var, model);
734 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
735 model->TakeOwnership(constraint);
736 };
737}
738
739// Expresses the fact that an existing integer variable is equal to the maximum
740// of other integer variables.
741inline std::function<void(Model*)> IsEqualToMaxOf(
742 IntegerVariable max_var, const std::vector<IntegerVariable>& vars) {
743 return [=](Model* model) {
744 std::vector<IntegerVariable> negated_vars;
745 for (const IntegerVariable& var : vars) {
746 negated_vars.push_back(NegationOf(var));
747 model->Add(GreaterOrEqual(max_var, var));
748 }
749
750 MinPropagator* constraint = new MinPropagator(
751 negated_vars, NegationOf(max_var), model->GetOrCreate<IntegerTrail>());
752 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
753 model->TakeOwnership(constraint);
754 };
755}
756
757// Expresses the fact that an existing integer variable is equal to one of
758// the given values, each selected by a given literal.
759std::function<void(Model*)> IsOneOf(IntegerVariable var,
760 const std::vector<Literal>& selectors,
761 const std::vector<IntegerValue>& values);
762
763template <class T>
765 ct->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
766 model->TakeOwnership(ct);
767}
768// Adds the constraint: a * b = p.
769inline std::function<void(Model*)> ProductConstraint(IntegerVariable a,
770 IntegerVariable b,
771 IntegerVariable p) {
772 return [=](Model* model) {
773 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
774 if (a == b) {
775 if (model->Get(LowerBound(a)) >= 0) {
777 new SquarePropagator(a, p, integer_trail));
778 } else if (model->Get(UpperBound(a)) <= 0) {
780 model, new SquarePropagator(NegationOf(a), p, integer_trail));
781 } else {
782 LOG(FATAL) << "Not supported";
783 }
784 } else if (model->Get(LowerBound(a)) >= 0 &&
785 model->Get(LowerBound(b)) >= 0) {
787 model, new PositiveProductPropagator(a, b, p, integer_trail));
788 } else if (model->Get(LowerBound(a)) >= 0 &&
789 model->Get(UpperBound(b)) <= 0) {
792 integer_trail));
793 } else if (model->Get(UpperBound(a)) <= 0 &&
794 model->Get(LowerBound(b)) >= 0) {
797 integer_trail));
798 } else if (model->Get(UpperBound(a)) <= 0 &&
799 model->Get(UpperBound(b)) <= 0) {
802 integer_trail));
803 } else {
804 LOG(FATAL) << "Not supported";
805 }
806 };
807}
808
809// Adds the constraint: a / b = c.
810inline std::function<void(Model*)> DivisionConstraint(IntegerVariable a,
811 IntegerVariable b,
812 IntegerVariable c) {
813 return [=](Model* model) {
814 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
815 DivisionPropagator* constraint =
816 new DivisionPropagator(a, b, c, integer_trail);
817 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
818 model->TakeOwnership(constraint);
819 };
820}
821
822// Adds the constraint: a / b = c where b is a constant.
823inline std::function<void(Model*)> FixedDivisionConstraint(IntegerVariable a,
824 IntegerValue b,
825 IntegerVariable c) {
826 return [=](Model* model) {
827 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
828 FixedDivisionPropagator* constraint =
829 b > 0
830 ? new FixedDivisionPropagator(a, b, c, integer_trail)
831 : new FixedDivisionPropagator(NegationOf(a), -b, c, integer_trail);
832 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
833 model->TakeOwnership(constraint);
834 };
835}
836
837} // namespace sat
838} // namespace operations_research
839
840#endif // OR_TOOLS_SAT_INTEGER_EXPR_H_
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define LOG(severity)
Definition: base/logging.h:420
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
void RegisterWith(GenericLiteralWatcher *watcher)
IntegerSumLE(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, IntegerValue upper_bound, Model *model)
Definition: integer_expr.cc:30
IntegerVariable AddIntegerVariable(IntegerValue lower_bound, IntegerValue upper_bound)
Definition: integer.cc:603
LevelZeroEquality(IntegerVariable target, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, Model *model)
LinMinPropagator & operator=(const LinMinPropagator &)=delete
LinMinPropagator(const std::vector< LinearExpression > &exprs, IntegerVariable min_var, Model *model)
LinMinPropagator(const LinMinPropagator &)=delete
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterWith(GenericLiteralWatcher *watcher)
MinPropagator(const std::vector< IntegerVariable > &vars, IntegerVariable min_var, IntegerTrail *integer_trail)
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
const int FATAL
Definition: log_severity.h:32
#define DISALLOW_COPY_AND_ASSIGN(TypeName)
Definition: macros.h:29
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
Definition: integer_expr.h:299
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> ConditionalSum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub, const std::vector< Literal > &enforcement_literals)
Definition: precedences.h:381
std::function< void(Model *)> Sum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub)
Definition: precedences.h:352
std::function< void(Model *)> ConditionalWeightedSumLowerOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
Definition: integer_expr.h:426
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
std::function< IntegerVariable(Model *)> NewWeightedSum(const VectorInt &coefficients, const std::vector< IntegerVariable > &vars)
Definition: integer_expr.h:641
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1467
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:404
void RegisterAndTransferOwnership(Model *model, T *ct)
Definition: integer_expr.h:764
std::function< void(Model *)> ProductConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable p)
Definition: integer_expr.h:769
std::function< void(Model *)> IsEqualToMinOf(IntegerVariable min_var, const std::vector< IntegerVariable > &vars)
Definition: integer_expr.h:672
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
Definition: integer.h:1495
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1426
std::function< void(Model *)> FixedDivisionConstraint(IntegerVariable a, IntegerValue b, IntegerVariable c)
Definition: integer_expr.h:823
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> WeightedSumGreaterOrEqualReif(Literal is_ge, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:540
std::function< void(Model *)> ConditionalSum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub, const std::vector< Literal > &enforcement_literals)
Definition: precedences.h:359
std::function< void(Model *)> FixedWeightedSum(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
Definition: integer_expr.h:415
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
std::function< void(Model *)> ConditionalWeightedSumGreaterOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:514
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
Definition: integer_expr.h:572
std::function< void(Model *)> Sum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub)
Definition: precedences.h:370
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> DivisionConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable c)
Definition: integer_expr.h:810
std::function< void(Model *)> WeightedSumLowerOrEqualReif(Literal is_le, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
Definition: integer_expr.h:527
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1509
std::function< void(Model *)> FixedWeightedSumReif(Literal is_eq, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
Definition: integer_expr.h:602
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
std::function< void(Model *)> WeightedSumNotEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
Definition: integer_expr.h:619
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:968
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
Definition: integer.h:1537
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< void(Model *)> IsEqualToMaxOf(IntegerVariable max_var, const std::vector< IntegerVariable > &vars)
Definition: integer_expr.h:741
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
STL namespace.
std::vector< double > coefficients
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
std::vector< IntegerVariable > vars