OR-Tools  8.2
integer_expr.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 <algorithm>
17#include <memory>
18#include <vector>
19
20#include "absl/container/flat_hash_map.h"
21#include "absl/memory/memory.h"
23#include "ortools/sat/integer.h"
26
27namespace operations_research {
28namespace sat {
29
30IntegerSumLE::IntegerSumLE(const std::vector<Literal>& enforcement_literals,
31 const std::vector<IntegerVariable>& vars,
32 const std::vector<IntegerValue>& coeffs,
33 IntegerValue upper, Model* model)
34 : enforcement_literals_(enforcement_literals),
35 upper_bound_(upper),
36 trail_(model->GetOrCreate<Trail>()),
37 integer_trail_(model->GetOrCreate<IntegerTrail>()),
38 time_limit_(model->GetOrCreate<TimeLimit>()),
39 rev_integer_value_repository_(
40 model->GetOrCreate<RevIntegerValueRepository>()),
41 vars_(vars),
42 coeffs_(coeffs) {
43 // TODO(user): deal with this corner case.
44 CHECK(!vars_.empty());
45 max_variations_.resize(vars_.size());
46
47 // Handle negative coefficients.
48 for (int i = 0; i < vars.size(); ++i) {
49 if (coeffs_[i] < 0) {
50 vars_[i] = NegationOf(vars_[i]);
51 coeffs_[i] = -coeffs_[i];
52 }
53 }
54
55 // Literal reason will only be used with the negation of enforcement_literals.
56 for (const Literal literal : enforcement_literals) {
57 literal_reason_.push_back(literal.Negated());
58 }
59
60 // Initialize the reversible numbers.
61 rev_num_fixed_vars_ = 0;
62 rev_lb_fixed_vars_ = IntegerValue(0);
63}
64
65void IntegerSumLE::FillIntegerReason() {
66 integer_reason_.clear();
67 reason_coeffs_.clear();
68 const int num_vars = vars_.size();
69 for (int i = 0; i < num_vars; ++i) {
70 const IntegerVariable var = vars_[i];
71 if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
72 integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
73 reason_coeffs_.push_back(coeffs_[i]);
74 }
75 }
76}
77
79 // Reified case: If any of the enforcement_literals are false, we ignore the
80 // constraint.
81 int num_unassigned_enforcement_literal = 0;
82 LiteralIndex unique_unnasigned_literal = kNoLiteralIndex;
83 for (const Literal literal : enforcement_literals_) {
84 if (trail_->Assignment().LiteralIsFalse(literal)) return true;
85 if (!trail_->Assignment().LiteralIsTrue(literal)) {
86 ++num_unassigned_enforcement_literal;
87 unique_unnasigned_literal = literal.Index();
88 }
89 }
90
91 // Unfortunately, we can't propagate anything if we have more than one
92 // unassigned enforcement literal.
93 if (num_unassigned_enforcement_literal > 1) return true;
94
95 // Save the current sum of fixed variables.
96 if (is_registered_) {
97 rev_integer_value_repository_->SaveState(&rev_lb_fixed_vars_);
98 } else {
99 rev_num_fixed_vars_ = 0;
100 rev_lb_fixed_vars_ = 0;
101 }
102
103 // Compute the new lower bound and update the reversible structures.
104 IntegerValue lb_unfixed_vars = IntegerValue(0);
105 const int num_vars = vars_.size();
106 for (int i = rev_num_fixed_vars_; i < num_vars; ++i) {
107 const IntegerVariable var = vars_[i];
108 const IntegerValue coeff = coeffs_[i];
109 const IntegerValue lb = integer_trail_->LowerBound(var);
110 const IntegerValue ub = integer_trail_->UpperBound(var);
111 if (lb != ub) {
112 max_variations_[i] = (ub - lb) * coeff;
113 lb_unfixed_vars += lb * coeff;
114 } else {
115 // Update the set of fixed variables.
116 std::swap(vars_[i], vars_[rev_num_fixed_vars_]);
117 std::swap(coeffs_[i], coeffs_[rev_num_fixed_vars_]);
118 std::swap(max_variations_[i], max_variations_[rev_num_fixed_vars_]);
119 rev_num_fixed_vars_++;
120 rev_lb_fixed_vars_ += lb * coeff;
121 }
122 }
123 time_limit_->AdvanceDeterministicTime(
124 static_cast<double>(num_vars - rev_num_fixed_vars_) * 1e-9);
125
126 // Conflict?
127 const IntegerValue slack =
128 upper_bound_ - (rev_lb_fixed_vars_ + lb_unfixed_vars);
129 if (slack < 0) {
130 FillIntegerReason();
131 integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs_,
132 &integer_reason_);
133
134 if (num_unassigned_enforcement_literal == 1) {
135 // Propagate the only non-true literal to false.
136 const Literal to_propagate = Literal(unique_unnasigned_literal).Negated();
137 std::vector<Literal> tmp = literal_reason_;
138 tmp.erase(std::find(tmp.begin(), tmp.end(), to_propagate));
139 integer_trail_->EnqueueLiteral(to_propagate, tmp, integer_reason_);
140 return true;
141 }
142 return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
143 }
144
145 // We can only propagate more if all the enforcement literals are true.
146 if (num_unassigned_enforcement_literal > 0) return true;
147
148 // The lower bound of all the variables except one can be used to update the
149 // upper bound of the last one.
150 for (int i = rev_num_fixed_vars_; i < num_vars; ++i) {
151 if (max_variations_[i] <= slack) continue;
152
153 const IntegerVariable var = vars_[i];
154 const IntegerValue coeff = coeffs_[i];
155 const IntegerValue div = slack / coeff;
156 const IntegerValue new_ub = integer_trail_->LowerBound(var) + div;
157 const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
158 if (!integer_trail_->Enqueue(
160 /*lazy_reason=*/[this, propagation_slack](
161 IntegerLiteral i_lit, int trail_index,
162 std::vector<Literal>* literal_reason,
163 std::vector<int>* trail_indices_reason) {
164 *literal_reason = literal_reason_;
165 trail_indices_reason->clear();
166 reason_coeffs_.clear();
167 const int size = vars_.size();
168 for (int i = 0; i < size; ++i) {
169 const IntegerVariable var = vars_[i];
170 if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
171 continue;
172 }
173 const int index =
174 integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
175 if (index >= 0) {
176 trail_indices_reason->push_back(index);
177 if (propagation_slack > 0) {
178 reason_coeffs_.push_back(coeffs_[i]);
179 }
180 }
181 }
182 if (propagation_slack > 0) {
183 integer_trail_->RelaxLinearReason(
184 propagation_slack, reason_coeffs_, trail_indices_reason);
185 }
186 })) {
187 return false;
188 }
189 }
190
191 return true;
192}
193
194bool IntegerSumLE::PropagateAtLevelZero() {
195 // TODO(user): Deal with enforcements. It is just a bit of code to read the
196 // value of the literals at level zero.
197 if (!enforcement_literals_.empty()) return true;
198
199 // Compute the new lower bound and update the reversible structures.
200 IntegerValue min_activity = IntegerValue(0);
201 const int num_vars = vars_.size();
202 for (int i = 0; i < num_vars; ++i) {
203 const IntegerVariable var = vars_[i];
204 const IntegerValue coeff = coeffs_[i];
205 const IntegerValue lb = integer_trail_->LevelZeroLowerBound(var);
206 const IntegerValue ub = integer_trail_->LevelZeroUpperBound(var);
207 max_variations_[i] = (ub - lb) * coeff;
208 min_activity += lb * coeff;
209 }
210 time_limit_->AdvanceDeterministicTime(static_cast<double>(num_vars * 1e-9));
211
212 // Conflict?
213 const IntegerValue slack = upper_bound_ - min_activity;
214 if (slack < 0) {
215 return integer_trail_->ReportConflict({}, {});
216 }
217
218 // The lower bound of all the variables except one can be used to update the
219 // upper bound of the last one.
220 for (int i = 0; i < num_vars; ++i) {
221 if (max_variations_[i] <= slack) continue;
222
223 const IntegerVariable var = vars_[i];
224 const IntegerValue coeff = coeffs_[i];
225 const IntegerValue div = slack / coeff;
226 const IntegerValue new_ub = integer_trail_->LevelZeroLowerBound(var) + div;
227 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(var, new_ub), {},
228 {})) {
229 return false;
230 }
231 }
232
233 return true;
234}
235
236void IntegerSumLE::RegisterWith(GenericLiteralWatcher* watcher) {
237 is_registered_ = true;
238 const int id = watcher->Register(this);
239 for (const IntegerVariable& var : vars_) {
240 watcher->WatchLowerBound(var, id);
241 }
242 for (const Literal literal : enforcement_literals_) {
243 // We only watch the true direction.
244 //
245 // TODO(user): if there is more than one, maybe we should watch more to
246 // propagate a "conflict" as soon as only one is unassigned?
247 watcher->WatchLiteral(Literal(literal), id);
248 }
249 watcher->RegisterReversibleInt(id, &rev_num_fixed_vars_);
250}
251
252LevelZeroEquality::LevelZeroEquality(IntegerVariable target,
253 const std::vector<IntegerVariable>& vars,
254 const std::vector<IntegerValue>& coeffs,
255 Model* model)
256 : target_(target),
257 vars_(vars),
258 coeffs_(coeffs),
259 trail_(model->GetOrCreate<Trail>()),
260 integer_trail_(model->GetOrCreate<IntegerTrail>()) {
261 auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
262 const int id = watcher->Register(this);
263 watcher->SetPropagatorPriority(id, 2);
264 watcher->WatchIntegerVariable(target, id);
265 for (const IntegerVariable& var : vars_) {
266 watcher->WatchIntegerVariable(var, id);
267 }
268}
269
270// TODO(user): We could go even further than just the GCD, and do more
271// arithmetic to tighten the target bounds. See for instance a problem like
272// ej.mps.gz that we don't solve easily, but has just 3 variables! the goal is
273// to minimize X, given 31013 X - 41014 Y - 51015 Z = -31013 (all >=0, Y and Z
274// bounded with high values). I know some MIP solvers have a basic linear
275// diophantine equation support.
277 // TODO(user): Once the GCD is not 1, we could at any level make sure the
278 // objective is of the correct form. For now, this only happen in a few
279 // miplib problem that we close quickly, so I didn't add the extra code yet.
280 if (trail_->CurrentDecisionLevel() != 0) return true;
281
282 int64 gcd = 0;
283 IntegerValue sum(0);
284 for (int i = 0; i < vars_.size(); ++i) {
285 if (integer_trail_->IsFixed(vars_[i])) {
286 sum += coeffs_[i] * integer_trail_->LowerBound(vars_[i]);
287 continue;
288 }
289 gcd = MathUtil::GCD64(gcd, std::abs(coeffs_[i].value()));
290 if (gcd == 1) break;
291 }
292 if (gcd == 0) return true; // All fixed.
293
294 if (gcd > gcd_) {
295 VLOG(1) << "Objective gcd: " << gcd;
296 }
297 CHECK_GE(gcd, gcd_);
298 gcd_ = IntegerValue(gcd);
299
300 const IntegerValue lb = integer_trail_->LowerBound(target_);
301 const IntegerValue lb_remainder = PositiveRemainder(lb - sum, gcd_);
302 if (lb_remainder != 0) {
303 if (!integer_trail_->Enqueue(
304 IntegerLiteral::GreaterOrEqual(target_, lb + gcd_ - lb_remainder),
305 {}, {}))
306 return false;
307 }
308
309 const IntegerValue ub = integer_trail_->UpperBound(target_);
310 const IntegerValue ub_remainder =
311 PositiveRemainder(ub - sum, IntegerValue(gcd));
312 if (ub_remainder != 0) {
313 if (!integer_trail_->Enqueue(
314 IntegerLiteral::LowerOrEqual(target_, ub - ub_remainder), {}, {}))
315 return false;
316 }
317
318 return true;
319}
320
321MinPropagator::MinPropagator(const std::vector<IntegerVariable>& vars,
322 IntegerVariable min_var,
323 IntegerTrail* integer_trail)
324 : vars_(vars), min_var_(min_var), integer_trail_(integer_trail) {}
325
327 if (vars_.empty()) return true;
328
329 // Count the number of interval that are possible candidate for the min.
330 // Only the intervals for which lb > current_min_ub cannot.
331 const IntegerLiteral min_ub_literal =
332 integer_trail_->UpperBoundAsLiteral(min_var_);
333 const IntegerValue current_min_ub = integer_trail_->UpperBound(min_var_);
334 int num_intervals_that_can_be_min = 0;
335 int last_possible_min_interval = 0;
336
337 IntegerValue min = kMaxIntegerValue;
338 for (int i = 0; i < vars_.size(); ++i) {
339 const IntegerValue lb = integer_trail_->LowerBound(vars_[i]);
340 min = std::min(min, lb);
341 if (lb <= current_min_ub) {
342 ++num_intervals_that_can_be_min;
343 last_possible_min_interval = i;
344 }
345 }
346
347 // Propagation a)
348 if (min > integer_trail_->LowerBound(min_var_)) {
349 integer_reason_.clear();
350 for (const IntegerVariable var : vars_) {
351 integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(var, min));
352 }
353 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(min_var_, min),
354 {}, integer_reason_)) {
355 return false;
356 }
357 }
358
359 // Propagation b)
360 if (num_intervals_that_can_be_min == 1) {
361 const IntegerValue ub_of_only_candidate =
362 integer_trail_->UpperBound(vars_[last_possible_min_interval]);
363 if (current_min_ub < ub_of_only_candidate) {
364 integer_reason_.clear();
365
366 // The reason is that all the other interval start after current_min_ub.
367 // And that min_ub has its current value.
368 integer_reason_.push_back(min_ub_literal);
369 for (const IntegerVariable var : vars_) {
370 if (var == vars_[last_possible_min_interval]) continue;
371 integer_reason_.push_back(
372 IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
373 }
374 if (!integer_trail_->Enqueue(
375 IntegerLiteral::LowerOrEqual(vars_[last_possible_min_interval],
376 current_min_ub),
377 {}, integer_reason_)) {
378 return false;
379 }
380 }
381 }
382
383 // Conflict.
384 //
385 // TODO(user): Not sure this code is useful since this will be detected
386 // by the fact that the [lb, ub] of the min is empty. It depends on the
387 // propagation order though, but probably the precedences propagator would
388 // propagate before this one. So change this to a CHECK?
389 if (num_intervals_that_can_be_min == 0) {
390 integer_reason_.clear();
391
392 // Almost the same as propagation b).
393 integer_reason_.push_back(min_ub_literal);
394 for (const IntegerVariable var : vars_) {
395 integer_reason_.push_back(
396 IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
397 }
398 return integer_trail_->ReportConflict(integer_reason_);
399 }
400
401 return true;
402}
403
405 const int id = watcher->Register(this);
406 for (const IntegerVariable& var : vars_) {
407 watcher->WatchLowerBound(var, id);
408 }
409 watcher->WatchUpperBound(min_var_, id);
410}
411
412LinMinPropagator::LinMinPropagator(const std::vector<LinearExpression>& exprs,
413 IntegerVariable min_var, Model* model)
414 : exprs_(exprs),
415 min_var_(min_var),
416 model_(model),
417 integer_trail_(model_->GetOrCreate<IntegerTrail>()) {}
418
419bool LinMinPropagator::PropagateLinearUpperBound(
420 const std::vector<IntegerVariable>& vars,
421 const std::vector<IntegerValue>& coeffs, const IntegerValue upper_bound) {
422 IntegerValue sum_lb = IntegerValue(0);
423 const int num_vars = vars.size();
424 std::vector<IntegerValue> max_variations;
425 for (int i = 0; i < num_vars; ++i) {
426 const IntegerVariable var = vars[i];
427 const IntegerValue coeff = coeffs[i];
428 // The coefficients are assumed to be positive for this to work properly.
429 DCHECK_GE(coeff, 0);
430 const IntegerValue lb = integer_trail_->LowerBound(var);
431 const IntegerValue ub = integer_trail_->UpperBound(var);
432 max_variations.push_back((ub - lb) * coeff);
433 sum_lb += lb * coeff;
434 }
435
436 model_->GetOrCreate<TimeLimit>()->AdvanceDeterministicTime(
437 static_cast<double>(num_vars) * 1e-9);
438
439 const IntegerValue slack = upper_bound - sum_lb;
440
441 std::vector<IntegerLiteral> linear_sum_reason;
442 std::vector<IntegerValue> reason_coeffs;
443 for (int i = 0; i < num_vars; ++i) {
444 const IntegerVariable var = vars[i];
445 if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
446 linear_sum_reason.push_back(integer_trail_->LowerBoundAsLiteral(var));
447 reason_coeffs.push_back(coeffs[i]);
448 }
449 }
450 if (slack < 0) {
451 // Conflict.
452 integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs,
453 &linear_sum_reason);
454 std::vector<IntegerLiteral> local_reason =
455 integer_reason_for_unique_candidate_;
456 local_reason.insert(local_reason.end(), linear_sum_reason.begin(),
457 linear_sum_reason.end());
458 return integer_trail_->ReportConflict({}, local_reason);
459 }
460
461 // The lower bound of all the variables except one can be used to update the
462 // upper bound of the last one.
463 for (int i = 0; i < num_vars; ++i) {
464 if (max_variations[i] <= slack) continue;
465
466 const IntegerVariable var = vars[i];
467 const IntegerValue coeff = coeffs[i];
468 const IntegerValue div = slack / coeff;
469 const IntegerValue new_ub = integer_trail_->LowerBound(var) + div;
470
471 const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
472 if (!integer_trail_->Enqueue(
474 /*lazy_reason=*/[this, &vars, &coeffs, propagation_slack](
475 IntegerLiteral i_lit, int trail_index,
476 std::vector<Literal>* literal_reason,
477 std::vector<int>* trail_indices_reason) {
478 literal_reason->clear();
479 trail_indices_reason->clear();
480 std::vector<IntegerValue> reason_coeffs;
481 const int size = vars.size();
482 for (int i = 0; i < size; ++i) {
483 const IntegerVariable var = vars[i];
484 if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
485 continue;
486 }
487 const int index =
488 integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
489 if (index >= 0) {
490 trail_indices_reason->push_back(index);
491 if (propagation_slack > 0) {
492 reason_coeffs.push_back(coeffs[i]);
493 }
494 }
495 }
496 if (propagation_slack > 0) {
497 integer_trail_->RelaxLinearReason(
498 propagation_slack, reason_coeffs, trail_indices_reason);
499 }
500 // Now add the old integer_reason that triggered this propatation.
501 for (IntegerLiteral reason_lit :
502 integer_reason_for_unique_candidate_) {
503 const int index = integer_trail_->FindTrailIndexOfVarBefore(
504 reason_lit.var, trail_index);
505 if (index >= 0) {
506 trail_indices_reason->push_back(index);
507 }
508 }
509 })) {
510 return false;
511 }
512 }
513 return true;
514}
515
517 if (exprs_.empty()) return true;
518
519 expr_lbs_.clear();
520
521 // Count the number of interval that are possible candidate for the min.
522 // Only the intervals for which lb > current_min_ub cannot.
523 const IntegerLiteral min_ub_literal =
524 integer_trail_->UpperBoundAsLiteral(min_var_);
525 const IntegerValue current_min_ub = integer_trail_->UpperBound(min_var_);
526 int num_intervals_that_can_be_min = 0;
527 int last_possible_min_interval = 0;
528
529 IntegerValue min_of_linear_expression_lb = kMaxIntegerValue;
530 for (int i = 0; i < exprs_.size(); ++i) {
531 const IntegerValue lb = LinExprLowerBound(exprs_[i], *integer_trail_);
532 expr_lbs_.push_back(lb);
533 min_of_linear_expression_lb = std::min(min_of_linear_expression_lb, lb);
534 if (lb <= current_min_ub) {
535 ++num_intervals_that_can_be_min;
536 last_possible_min_interval = i;
537 }
538 }
539
540 // Propagation a) lb(min) >= lb(MIN(exprs)) = MIN(lb(exprs));
541
542 // Conflict will be detected by the fact that the [lb, ub] of the min is
543 // empty. In case of conflict, we just need the reason for pushing UB + 1.
544 if (min_of_linear_expression_lb > current_min_ub) {
545 min_of_linear_expression_lb = current_min_ub + 1;
546 }
547
548 // Early experiments seems to show that the code if faster without relaxing
549 // the linear reason. But that might change in the future.
550 const bool use_slack = false;
551 if (min_of_linear_expression_lb > integer_trail_->LowerBound(min_var_)) {
552 std::vector<IntegerLiteral> local_reason;
553 for (int i = 0; i < exprs_.size(); ++i) {
554 const IntegerValue slack = expr_lbs_[i] - min_of_linear_expression_lb;
555 integer_trail_->AppendRelaxedLinearReason(
556 (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
557 exprs_[i].vars, &local_reason);
558 }
559 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(
560 min_var_, min_of_linear_expression_lb),
561 {}, local_reason)) {
562 return false;
563 }
564 }
565
566 // Propagation b) ub(min) >= ub(MIN(exprs)) and we can't propagate anything
567 // here unless there is just one possible expression 'e' that can be the min:
568 // for all u != e, lb(u) > ub(min);
569 // In this case, ub(min) >= ub(e).
570 if (num_intervals_that_can_be_min == 1) {
571 const IntegerValue ub_of_only_candidate =
572 LinExprUpperBound(exprs_[last_possible_min_interval], *integer_trail_);
573 if (current_min_ub < ub_of_only_candidate) {
574 // For this propagation, we only need to fill the integer reason once at
575 // the lowest level. At higher levels this reason still remains valid.
576 if (rev_unique_candidate_ == 0) {
577 integer_reason_for_unique_candidate_.clear();
578
579 // The reason is that all the other interval start after current_min_ub.
580 // And that min_ub has its current value.
581 integer_reason_for_unique_candidate_.push_back(min_ub_literal);
582 for (int i = 0; i < exprs_.size(); ++i) {
583 if (i == last_possible_min_interval) continue;
584 const IntegerValue slack = expr_lbs_[i] - (current_min_ub + 1);
585 integer_trail_->AppendRelaxedLinearReason(
586 (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
587 exprs_[i].vars, &integer_reason_for_unique_candidate_);
588 }
589 rev_unique_candidate_ = 1;
590 }
591
592 return PropagateLinearUpperBound(
593 exprs_[last_possible_min_interval].vars,
594 exprs_[last_possible_min_interval].coeffs,
595 current_min_ub - exprs_[last_possible_min_interval].offset);
596 }
597 }
598
599 return true;
600}
601
603 const int id = watcher->Register(this);
604 for (const LinearExpression& expr : exprs_) {
605 for (int i = 0; i < expr.vars.size(); ++i) {
606 const IntegerVariable& var = expr.vars[i];
607 const IntegerValue coeff = expr.coeffs[i];
608 if (coeff > 0) {
609 watcher->WatchLowerBound(var, id);
610 } else {
611 watcher->WatchUpperBound(var, id);
612 }
613 }
614 }
615 watcher->WatchUpperBound(min_var_, id);
616 watcher->RegisterReversibleInt(id, &rev_unique_candidate_);
617}
618
620 IntegerVariable a, IntegerVariable b, IntegerVariable p,
621 IntegerTrail* integer_trail)
622 : a_(a), b_(b), p_(p), integer_trail_(integer_trail) {
623 // Note that we assume this is true at level zero, and so we never include
624 // that fact in the reasons we compute.
625 CHECK_GE(integer_trail_->LevelZeroLowerBound(a_), 0);
626 CHECK_GE(integer_trail_->LevelZeroLowerBound(b_), 0);
627}
628
629// TODO(user): We can tighten the bounds on p by removing extreme value that
630// do not contains divisor in the domains of a or b. There is an algo in O(
631// smallest domain size between a or b).
633 const IntegerValue max_a = integer_trail_->UpperBound(a_);
634 const IntegerValue max_b = integer_trail_->UpperBound(b_);
635 const IntegerValue new_max(CapProd(max_a.value(), max_b.value()));
636 if (new_max < integer_trail_->UpperBound(p_)) {
637 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(p_, new_max), {},
638 {integer_trail_->UpperBoundAsLiteral(a_),
639 integer_trail_->UpperBoundAsLiteral(b_)})) {
640 return false;
641 }
642 }
643
644 const IntegerValue min_a = integer_trail_->LowerBound(a_);
645 const IntegerValue min_b = integer_trail_->LowerBound(b_);
646 const IntegerValue new_min(CapProd(min_a.value(), min_b.value()));
647 if (new_min > integer_trail_->LowerBound(p_)) {
648 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(p_, new_min),
649 {},
650 {integer_trail_->LowerBoundAsLiteral(a_),
651 integer_trail_->LowerBoundAsLiteral(b_)})) {
652 return false;
653 }
654 }
655
656 for (int i = 0; i < 2; ++i) {
657 const IntegerVariable a = i == 0 ? a_ : b_;
658 const IntegerVariable b = i == 0 ? b_ : a_;
659 const IntegerValue max_a = integer_trail_->UpperBound(a);
660 const IntegerValue min_b = integer_trail_->LowerBound(b);
661 const IntegerValue min_p = integer_trail_->LowerBound(p_);
662 const IntegerValue max_p = integer_trail_->UpperBound(p_);
663 const IntegerValue prod(CapProd(max_a.value(), min_b.value()));
664 if (prod > max_p) {
665 if (!integer_trail_->Enqueue(
666 IntegerLiteral::LowerOrEqual(a, FloorRatio(max_p, min_b)), {},
667 {integer_trail_->LowerBoundAsLiteral(b),
668 integer_trail_->UpperBoundAsLiteral(p_)})) {
669 return false;
670 }
671 } else if (prod < min_p) {
672 if (!integer_trail_->Enqueue(
673 IntegerLiteral::GreaterOrEqual(b, CeilRatio(min_p, max_a)), {},
674 {integer_trail_->UpperBoundAsLiteral(a),
675 integer_trail_->LowerBoundAsLiteral(p_)})) {
676 return false;
677 }
678 }
679 }
680
681 return true;
682}
683
685 const int id = watcher->Register(this);
686 watcher->WatchIntegerVariable(a_, id);
687 watcher->WatchIntegerVariable(b_, id);
688 watcher->WatchIntegerVariable(p_, id);
690}
691
692namespace {
693
694// TODO(user): Find better implementation?
695IntegerValue FloorSquareRoot(IntegerValue a) {
696 IntegerValue result(static_cast<int64>(std::floor(std::sqrt(ToDouble(a)))));
697 while (result * result > a) --result;
698 while ((result + 1) * (result + 1) <= a) ++result;
699 return result;
700}
701
702// TODO(user): Find better implementation?
703IntegerValue CeilSquareRoot(IntegerValue a) {
704 IntegerValue result(static_cast<int64>(std::ceil(std::sqrt(ToDouble(a)))));
705 while (result * result < a) ++result;
706 while ((result - 1) * (result - 1) >= a) --result;
707 return result;
708}
709
710} // namespace
711
712SquarePropagator::SquarePropagator(IntegerVariable x, IntegerVariable s,
713 IntegerTrail* integer_trail)
714 : x_(x), s_(s), integer_trail_(integer_trail) {
715 CHECK_GE(integer_trail->LevelZeroLowerBound(x), 0);
716}
717
718// Propagation from x to s: s in [min_x * min_x, max_x * max_x].
719// Propagation from s to x: x in [ceil(sqrt(min_s)), floor(sqrt(max_s))].
721 const IntegerValue min_x = integer_trail_->LowerBound(x_);
722 const IntegerValue min_s = integer_trail_->LowerBound(s_);
723 const IntegerValue min_x_square(CapProd(min_x.value(), min_x.value()));
724 if (min_x_square > min_s) {
725 if (!integer_trail_->Enqueue(
726 IntegerLiteral::GreaterOrEqual(s_, min_x_square), {},
727 {IntegerLiteral::GreaterOrEqual(x_, min_x)})) {
728 return false;
729 }
730 } else if (min_x_square < min_s) {
731 const IntegerValue new_min = CeilSquareRoot(min_s);
732 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(x_, new_min),
733 {},
734 {IntegerLiteral::GreaterOrEqual(
735 s_, (new_min - 1) * (new_min - 1) + 1)})) {
736 return false;
737 }
738 }
739
740 const IntegerValue max_x = integer_trail_->UpperBound(x_);
741 const IntegerValue max_s = integer_trail_->UpperBound(s_);
742 const IntegerValue max_x_square(CapProd(max_x.value(), max_x.value()));
743 if (max_x_square < max_s) {
744 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(s_, max_x_square),
745 {},
746 {IntegerLiteral::LowerOrEqual(x_, max_x)})) {
747 return false;
748 }
749 } else if (max_x_square > max_s) {
750 const IntegerValue new_max = FloorSquareRoot(max_s);
751 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(x_, new_max), {},
752 {IntegerLiteral::LowerOrEqual(
753 s_, (new_max + 1) * (new_max + 1) - 1)})) {
754 return false;
755 }
756 }
757
758 return true;
759}
760
762 const int id = watcher->Register(this);
763 watcher->WatchIntegerVariable(x_, id);
764 watcher->WatchIntegerVariable(s_, id);
766}
767
768DivisionPropagator::DivisionPropagator(IntegerVariable a, IntegerVariable b,
769 IntegerVariable c,
770 IntegerTrail* integer_trail)
771 : a_(a), b_(b), c_(c), integer_trail_(integer_trail) {
772 // TODO(user): support these cases.
773 CHECK_GE(integer_trail->LevelZeroLowerBound(a), 0);
774 CHECK_GT(integer_trail->LevelZeroLowerBound(b), 0); // b can never be zero.
775}
776
778 const IntegerValue min_a = integer_trail_->LowerBound(a_);
779 const IntegerValue max_a = integer_trail_->UpperBound(a_);
780 const IntegerValue min_b = integer_trail_->LowerBound(b_);
781 const IntegerValue max_b = integer_trail_->UpperBound(b_);
782 IntegerValue min_c = integer_trail_->LowerBound(c_);
783 IntegerValue max_c = integer_trail_->UpperBound(c_);
784
785 if (max_a / min_b < max_c) {
786 max_c = max_a / min_b;
787 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(c_, max_c), {},
788 {integer_trail_->UpperBoundAsLiteral(a_),
789 integer_trail_->LowerBoundAsLiteral(b_)})) {
790 return false;
791 }
792 }
793 if (min_a / max_b > min_c) {
794 min_c = min_a / max_b;
795 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(c_, min_c), {},
796 {integer_trail_->LowerBoundAsLiteral(a_),
797 integer_trail_->UpperBoundAsLiteral(b_)})) {
798 return false;
799 }
800 }
801
802 // TODO(user): propagate the bounds on a and b from the ones of c.
803 // Note however that what we did is enough to enforce the constraint when
804 // all the values are fixed.
805 return true;
806}
807
809 const int id = watcher->Register(this);
810 watcher->WatchIntegerVariable(a_, id);
811 watcher->WatchIntegerVariable(b_, id);
812 watcher->WatchIntegerVariable(c_, id);
814}
815
817 IntegerValue b,
818 IntegerVariable c,
819 IntegerTrail* integer_trail)
820 : a_(a), b_(b), c_(c), integer_trail_(integer_trail) {}
821
823 const IntegerValue min_a = integer_trail_->LowerBound(a_);
824 const IntegerValue max_a = integer_trail_->UpperBound(a_);
825 IntegerValue min_c = integer_trail_->LowerBound(c_);
826 IntegerValue max_c = integer_trail_->UpperBound(c_);
827
828 CHECK_GT(b_, 0);
829
830 if (max_a / b_ < max_c) {
831 max_c = max_a / b_;
832 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(c_, max_c), {},
833 {integer_trail_->UpperBoundAsLiteral(a_)})) {
834 return false;
835 }
836 } else if (max_a / b_ > max_c) {
837 const IntegerValue new_max_a =
838 max_c >= 0 ? max_c * b_ + b_ - 1
839 : IntegerValue(CapProd(max_c.value(), b_.value()));
840 CHECK_LT(new_max_a, max_a);
841 if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(a_, new_max_a),
842 {},
843 {integer_trail_->UpperBoundAsLiteral(c_)})) {
844 return false;
845 }
846 }
847
848 if (min_a / b_ > min_c) {
849 min_c = min_a / b_;
850 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(c_, min_c), {},
851 {integer_trail_->LowerBoundAsLiteral(a_)})) {
852 return false;
853 }
854 } else if (min_a / b_ < min_c) {
855 const IntegerValue new_min_a =
856 min_c > 0 ? IntegerValue(CapProd(min_c.value(), b_.value()))
857 : min_c * b_ - b_ + 1;
858 CHECK_GT(new_min_a, min_a);
859 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(a_, new_min_a),
860 {},
861 {integer_trail_->LowerBoundAsLiteral(c_)})) {
862 return false;
863 }
864 }
865
866 return true;
867}
868
870 const int id = watcher->Register(this);
871 watcher->WatchIntegerVariable(a_, id);
872 watcher->WatchIntegerVariable(c_, id);
873}
874
875std::function<void(Model*)> IsOneOf(IntegerVariable var,
876 const std::vector<Literal>& selectors,
877 const std::vector<IntegerValue>& values) {
878 return [=](Model* model) {
879 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
880 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
881
882 CHECK(!values.empty());
883 CHECK_EQ(values.size(), selectors.size());
884 std::vector<int64> unique_values;
885 absl::flat_hash_map<int64, std::vector<Literal>> value_to_selector;
886 for (int i = 0; i < values.size(); ++i) {
887 unique_values.push_back(values[i].value());
888 value_to_selector[values[i].value()].push_back(selectors[i]);
889 }
890 gtl::STLSortAndRemoveDuplicates(&unique_values);
891
892 integer_trail->UpdateInitialDomain(var, Domain::FromValues(unique_values));
893 if (unique_values.size() == 1) {
894 model->Add(ClauseConstraint(selectors));
895 return;
896 }
897
898 // Note that it is more efficient to call AssociateToIntegerEqualValue()
899 // with the values ordered, like we do here.
900 for (const int64 v : unique_values) {
901 const std::vector<Literal>& selectors = value_to_selector[v];
902 if (selectors.size() == 1) {
903 encoder->AssociateToIntegerEqualValue(selectors[0], var,
904 IntegerValue(v));
905 } else {
906 const Literal l(model->Add(NewBooleanVariable()), true);
907 model->Add(ReifiedBoolOr(selectors, l));
908 encoder->AssociateToIntegerEqualValue(l, var, IntegerValue(v));
909 }
910 }
911 };
912}
913
914} // namespace sat
915} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
const std::vector< IntVar * > vars_
Definition: alldiff_cst.cc:43
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define VLOG(verboselevel)
Definition: base/logging.h:978
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
static int64 GCD64(int64 x, int64 y)
Definition: mathutil.h:107
void SaveState(T *object)
Definition: rev.h:61
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 AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
Definition: time_limit.h:226
void RegisterWith(GenericLiteralWatcher *watcher)
DivisionPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable c, IntegerTrail *integer_trail)
FixedDivisionPropagator(IntegerVariable a, IntegerValue b, IntegerVariable c, IntegerTrail *integer_trail)
void RegisterWith(GenericLiteralWatcher *watcher)
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1365
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1373
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
Definition: integer.h:1397
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1391
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
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
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:989
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
Definition: integer.cc:716
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1330
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.h:810
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1087
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const
Definition: integer.h:827
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:807
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1350
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:785
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1335
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
LinMinPropagator(const std::vector< LinearExpression > &exprs, IntegerVariable min_var, Model *model)
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
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
Definition: sat/model.h:106
void RegisterWith(GenericLiteralWatcher *watcher)
PositiveProductPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable p, IntegerTrail *integer_trail)
void RegisterWith(GenericLiteralWatcher *watcher)
SquarePropagator(IntegerVariable x, IntegerVariable s, IntegerTrail *integer_trail)
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
std::function< void(Model *)> ReifiedBoolOr(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:934
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:102
double ToDouble(IntegerValue value)
Definition: integer.h:69
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1509
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
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...
int64 CapProd(int64 x, int64 y)
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
if(!yyg->yy_init)
Definition: parser.yy.cc:965
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264