OR-Tools  8.2
all_different.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 <map>
18#include <memory>
19
20#include "absl/container/flat_hash_set.h"
26#include "ortools/util/sort.h"
27
28namespace operations_research {
29namespace sat {
30
31std::function<void(Model*)> AllDifferentBinary(
32 const std::vector<IntegerVariable>& vars) {
33 return [=](Model* model) {
34 // Fully encode all the given variables and construct a mapping value ->
35 // List of literal each indicating that a given variable takes this value.
36 //
37 // Note that we use a map to always add the constraints in the same order.
38 std::map<IntegerValue, std::vector<Literal>> value_to_literals;
39 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
40 for (const IntegerVariable var : vars) {
42 for (const auto& entry : encoder->FullDomainEncoding(var)) {
43 value_to_literals[entry.value].push_back(entry.literal);
44 }
45 }
46
47 // Add an at most one constraint for each value.
48 for (const auto& entry : value_to_literals) {
49 if (entry.second.size() > 1) {
50 model->Add(AtMostOneConstraint(entry.second));
51 }
52 }
53
54 // If the number of values is equal to the number of variables, we have
55 // a permutation. We can add a bool_or for each literals attached to a
56 // value.
57 if (value_to_literals.size() == vars.size()) {
58 for (const auto& entry : value_to_literals) {
59 model->Add(ClauseConstraint(entry.second));
60 }
61 }
62 };
63}
64
65std::function<void(Model*)> AllDifferentOnBounds(
66 const std::vector<IntegerVariable>& vars) {
67 return [=](Model* model) {
68 if (vars.empty()) return;
69 auto* constraint = new AllDifferentBoundsPropagator(
70 vars, model->GetOrCreate<IntegerTrail>());
71 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
72 model->TakeOwnership(constraint);
73 };
74}
75
76std::function<void(Model*)> AllDifferentAC(
77 const std::vector<IntegerVariable>& variables) {
78 return [=](Model* model) {
79 if (variables.size() < 3) return;
80
82 variables, model->GetOrCreate<IntegerEncoder>(),
83 model->GetOrCreate<Trail>(), model->GetOrCreate<IntegerTrail>());
84 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
85 model->TakeOwnership(constraint);
86 };
87}
88
90 std::vector<IntegerVariable> variables, IntegerEncoder* encoder,
91 Trail* trail, IntegerTrail* integer_trail)
92 : num_variables_(variables.size()),
93 variables_(std::move(variables)),
94 trail_(trail),
95 integer_trail_(integer_trail) {
96 // Initialize literals cache.
97 int64 min_value = kint64max;
98 int64 max_value = kint64min;
99 variable_min_value_.resize(num_variables_);
100 variable_max_value_.resize(num_variables_);
101 variable_literal_index_.resize(num_variables_);
102 int num_fixed_variables = 0;
103 for (int x = 0; x < num_variables_; x++) {
104 variable_min_value_[x] = integer_trail_->LowerBound(variables_[x]).value();
105 variable_max_value_[x] = integer_trail_->UpperBound(variables_[x]).value();
106
107 // Compute value range of all variables.
108 min_value = std::min(min_value, variable_min_value_[x]);
109 max_value = std::max(max_value, variable_max_value_[x]);
110
111 // FullyEncode does not like 1-value domains, handle this case first.
112 // TODO(user): Prune now, ignore these variables during solving.
113 if (variable_min_value_[x] == variable_max_value_[x]) {
114 num_fixed_variables++;
115 variable_literal_index_[x].push_back(kTrueLiteralIndex);
116 continue;
117 }
118
119 // Force full encoding if not already done.
120 if (!encoder->VariableIsFullyEncoded(variables_[x])) {
121 encoder->FullyEncodeVariable(variables_[x]);
122 }
123
124 // Fill cache with literals, default value is kFalseLiteralIndex.
125 int64 size = variable_max_value_[x] - variable_min_value_[x] + 1;
126 variable_literal_index_[x].resize(size, kFalseLiteralIndex);
127 for (const auto& entry : encoder->FullDomainEncoding(variables_[x])) {
128 int64 value = entry.value.value();
129 // Can happen because of initial propagation!
130 if (value < variable_min_value_[x] || variable_max_value_[x] < value) {
131 continue;
132 }
133 variable_literal_index_[x][value - variable_min_value_[x]] =
134 entry.literal.Index();
135 }
136 }
137 min_all_values_ = min_value;
138 num_all_values_ = max_value - min_value + 1;
139
140 successor_.resize(num_variables_);
141 variable_to_value_.assign(num_variables_, -1);
142 visiting_.resize(num_variables_);
143 variable_visited_from_.resize(num_variables_);
144 residual_graph_successors_.resize(num_variables_ + num_all_values_ + 1);
145 component_number_.resize(num_variables_ + num_all_values_ + 1);
146}
147
149 const int id = watcher->Register(this);
150 watcher->SetPropagatorPriority(id, 2);
151 for (const auto& literal_indices : variable_literal_index_) {
152 for (const LiteralIndex li : literal_indices) {
153 // Watch only unbound literals.
154 if (li >= 0 &&
155 !trail_->Assignment().VariableIsAssigned(Literal(li).Variable())) {
156 watcher->WatchLiteral(Literal(li), id);
157 watcher->WatchLiteral(Literal(li).Negated(), id);
158 }
159 }
160 }
161}
162
163LiteralIndex AllDifferentConstraint::VariableLiteralIndexOf(int x,
164 int64 value) {
165 return (value < variable_min_value_[x] || variable_max_value_[x] < value)
167 : variable_literal_index_[x][value - variable_min_value_[x]];
168}
169
170inline bool AllDifferentConstraint::VariableHasPossibleValue(int x,
171 int64 value) {
172 LiteralIndex li = VariableLiteralIndexOf(x, value);
173 if (li == kFalseLiteralIndex) return false;
174 if (li == kTrueLiteralIndex) return true;
175 DCHECK_GE(li, 0);
176 return !trail_->Assignment().LiteralIsFalse(Literal(li));
177}
178
179bool AllDifferentConstraint::MakeAugmentingPath(int start) {
180 // Do a BFS and use visiting_ as a queue, with num_visited pointing
181 // at its begin() and num_to_visit its end().
182 // To switch to the augmenting path once a nonmatched value was found,
183 // we remember the BFS tree in variable_visited_from_.
184 int num_to_visit = 0;
185 int num_visited = 0;
186 // Enqueue start.
187 visiting_[num_to_visit++] = start;
188 variable_visited_[start] = true;
189 variable_visited_from_[start] = -1;
190
191 while (num_visited < num_to_visit) {
192 // Dequeue node to visit.
193 const int node = visiting_[num_visited++];
194
195 for (const int value : successor_[node]) {
196 if (value_visited_[value]) continue;
197 value_visited_[value] = true;
198 if (value_to_variable_[value] == -1) {
199 // value is not matched: change path from node to start, and return.
200 int path_node = node;
201 int path_value = value;
202 while (path_node != -1) {
203 int old_value = variable_to_value_[path_node];
204 variable_to_value_[path_node] = path_value;
205 value_to_variable_[path_value] = path_node;
206 path_node = variable_visited_from_[path_node];
207 path_value = old_value;
208 }
209 return true;
210 } else {
211 // Enqueue node matched to value.
212 const int next_node = value_to_variable_[value];
213 variable_visited_[next_node] = true;
214 visiting_[num_to_visit++] = next_node;
215 variable_visited_from_[next_node] = node;
216 }
217 }
218 }
219 return false;
220}
221
222// The algorithm copies the solver state to successor_, which is used to compute
223// a matching. If all variables can be matched, it generates the residual graph
224// in separate vectors, computes its SCCs, and filters variable -> value if
225// variable is not in the same SCC as value.
226// Explanations for failure and filtering are fine-grained:
227// failure is explained by a Hall set, i.e. dom(variables) \subseteq {values},
228// with |variables| < |values|; filtering is explained by the Hall set that
229// would happen if the variable was assigned to the value.
230//
231// TODO(user): If needed, there are several ways performance could be
232// improved.
233// If copying the variable state is too costly, it could be maintained instead.
234// If the propagator has too many fruitless calls (without failing/pruning),
235// we can remember the O(n) arcs used in the matching and the SCC decomposition,
236// and guard calls to Propagate() if these arcs are still valid.
238 // Copy variable state to graph state.
239 prev_matching_ = variable_to_value_;
240 value_to_variable_.assign(num_all_values_, -1);
241 variable_to_value_.assign(num_variables_, -1);
242 for (int x = 0; x < num_variables_; x++) {
243 successor_[x].clear();
244 const int64 min_value = integer_trail_->LowerBound(variables_[x]).value();
245 const int64 max_value = integer_trail_->UpperBound(variables_[x]).value();
246 for (int64 value = min_value; value <= max_value; value++) {
247 if (VariableHasPossibleValue(x, value)) {
248 const int offset_value = value - min_all_values_;
249 // Forward-checking should propagate x != value.
250 successor_[x].push_back(offset_value);
251 }
252 }
253 if (successor_[x].size() == 1) {
254 const int offset_value = successor_[x][0];
255 if (value_to_variable_[offset_value] == -1) {
256 value_to_variable_[offset_value] = x;
257 variable_to_value_[x] = offset_value;
258 }
259 }
260 }
261
262 // Because we currently propagates all clauses before entering this
263 // propagator, we known that this can't happen.
264 if (DEBUG_MODE) {
265 for (int x = 0; x < num_variables_; x++) {
266 for (const int offset_value : successor_[x]) {
267 if (value_to_variable_[offset_value] != -1 &&
268 value_to_variable_[offset_value] != x) {
269 LOG(FATAL) << "Should have been propagated by AllDifferentBinary()!";
270 }
271 }
272 }
273 }
274
275 // Seed with previous matching.
276 for (int x = 0; x < num_variables_; x++) {
277 if (variable_to_value_[x] != -1) continue;
278 const int prev_value = prev_matching_[x];
279 if (prev_value == -1 || value_to_variable_[prev_value] != -1) continue;
280
281 if (VariableHasPossibleValue(x, prev_matching_[x] + min_all_values_)) {
282 variable_to_value_[x] = prev_matching_[x];
283 value_to_variable_[prev_matching_[x]] = x;
284 }
285 }
286
287 // Compute max matching.
288 int x = 0;
289 for (; x < num_variables_; x++) {
290 if (variable_to_value_[x] == -1) {
291 value_visited_.assign(num_all_values_, false);
292 variable_visited_.assign(num_variables_, false);
293 MakeAugmentingPath(x);
294 }
295 if (variable_to_value_[x] == -1) break; // No augmenting path exists.
296 }
297
298 // Fail if covering variables impossible.
299 // Explain with the forbidden parts of the graph that prevent
300 // MakeAugmentingPath from increasing the matching size.
301 if (x < num_variables_) {
302 // For now explain all forbidden arcs.
303 std::vector<Literal>* conflict = trail_->MutableConflict();
304 conflict->clear();
305 for (int y = 0; y < num_variables_; y++) {
306 if (!variable_visited_[y]) continue;
307 for (int value = variable_min_value_[y]; value <= variable_max_value_[y];
308 value++) {
309 const LiteralIndex li = VariableLiteralIndexOf(y, value);
310 if (li >= 0 && !value_visited_[value - min_all_values_]) {
311 DCHECK(trail_->Assignment().LiteralIsFalse(Literal(li)));
312 conflict->push_back(Literal(li));
313 }
314 }
315 }
316 return false;
317 }
318
319 // The current matching is a valid solution, now try to filter values.
320 // Build residual graph, compute its SCCs.
321 for (int x = 0; x < num_variables_; x++) {
322 residual_graph_successors_[x].clear();
323 for (const int succ : successor_[x]) {
324 if (succ != variable_to_value_[x]) {
325 residual_graph_successors_[x].push_back(num_variables_ + succ);
326 }
327 }
328 }
329 for (int offset_value = 0; offset_value < num_all_values_; offset_value++) {
330 residual_graph_successors_[num_variables_ + offset_value].clear();
331 if (value_to_variable_[offset_value] != -1) {
332 residual_graph_successors_[num_variables_ + offset_value].push_back(
333 value_to_variable_[offset_value]);
334 }
335 }
336 const int dummy_node = num_variables_ + num_all_values_;
337 residual_graph_successors_[dummy_node].clear();
338 if (num_variables_ < num_all_values_) {
339 for (int x = 0; x < num_variables_; x++) {
340 residual_graph_successors_[dummy_node].push_back(x);
341 }
342 for (int offset_value = 0; offset_value < num_all_values_; offset_value++) {
343 if (value_to_variable_[offset_value] == -1) {
344 residual_graph_successors_[num_variables_ + offset_value].push_back(
345 dummy_node);
346 }
347 }
348 }
349
350 // Compute SCCs, make node -> component map.
351 struct SccOutput {
352 explicit SccOutput(std::vector<int>* c) : components(c) {}
353 void emplace_back(int const* b, int const* e) {
354 for (int const* it = b; it < e; ++it) {
355 (*components)[*it] = num_components;
356 }
357 ++num_components;
358 }
359 int num_components = 0;
360 std::vector<int>* components;
361 };
362 SccOutput scc_output(&component_number_);
364 static_cast<int>(residual_graph_successors_.size()),
365 residual_graph_successors_, &scc_output);
366
367 // Remove arcs var -> val where SCC(var) -/->* SCC(val).
368 for (int x = 0; x < num_variables_; x++) {
369 if (successor_[x].size() == 1) continue;
370 for (const int offset_value : successor_[x]) {
371 const int value_node = offset_value + num_variables_;
372 if (variable_to_value_[x] != offset_value &&
373 component_number_[x] != component_number_[value_node] &&
374 VariableHasPossibleValue(x, offset_value + min_all_values_)) {
375 // We can deduce that x != value. To explain, force x == offset_value,
376 // then find another assignment for the variable matched to
377 // offset_value. It will fail: explaining why is the same as
378 // explaining failure as above, and it is an explanation of x != value.
379 value_visited_.assign(num_all_values_, false);
380 variable_visited_.assign(num_variables_, false);
381 // Undo x -> old_value and old_variable -> offset_value.
382 const int old_variable = value_to_variable_[offset_value];
383 variable_to_value_[old_variable] = -1;
384 const int old_value = variable_to_value_[x];
385 value_to_variable_[old_value] = -1;
386 variable_to_value_[x] = offset_value;
387 value_to_variable_[offset_value] = x;
388
389 value_visited_[offset_value] = true;
390 MakeAugmentingPath(old_variable);
391 DCHECK_EQ(variable_to_value_[old_variable], -1); // No reassignment.
392
393 std::vector<Literal>* reason = trail_->GetEmptyVectorToStoreReason();
394 for (int y = 0; y < num_variables_; y++) {
395 if (!variable_visited_[y]) continue;
396 for (int value = variable_min_value_[y];
397 value <= variable_max_value_[y]; value++) {
398 const LiteralIndex li = VariableLiteralIndexOf(y, value);
399 if (li >= 0 && !value_visited_[value - min_all_values_]) {
400 DCHECK(!VariableHasPossibleValue(y, value));
401 reason->push_back(Literal(li));
402 }
403 }
404 }
405
406 const LiteralIndex li =
407 VariableLiteralIndexOf(x, offset_value + min_all_values_);
410 return trail_->EnqueueWithStoredReason(Literal(li).Negated());
411 }
412 }
413 }
414
415 return true;
416}
417
419 const std::vector<IntegerVariable>& vars, IntegerTrail* integer_trail)
420 : integer_trail_(integer_trail) {
421 CHECK(!vars.empty());
422
423 // We need +2 for sentinels.
424 const int capacity = vars.size() + 2;
425 index_to_start_index_.resize(capacity);
426 index_to_end_index_.resize(capacity);
427 index_to_var_.resize(capacity, kNoIntegerVariable);
428
429 for (int i = 0; i < vars.size(); ++i) {
430 vars_.push_back({vars[i]});
431 negated_vars_.push_back({NegationOf(vars[i])});
432 }
433}
434
436 if (!PropagateLowerBounds()) return false;
437
438 // Note that it is not required to swap back vars_ and negated_vars_.
439 // TODO(user): investigate the impact.
440 std::swap(vars_, negated_vars_);
441 const bool result = PropagateLowerBounds();
442 std::swap(vars_, negated_vars_);
443 return result;
444}
445
446void AllDifferentBoundsPropagator::FillHallReason(IntegerValue hall_lb,
447 IntegerValue hall_ub) {
448 integer_reason_.clear();
449 const int limit = GetIndex(hall_ub);
450 for (int i = GetIndex(hall_lb); i <= limit; ++i) {
451 const IntegerVariable var = index_to_var_[i];
452 integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(var, hall_lb));
453 integer_reason_.push_back(IntegerLiteral::LowerOrEqual(var, hall_ub));
454 }
455}
456
457int AllDifferentBoundsPropagator::FindStartIndexAndCompressPath(int index) {
458 // First, walk the pointer until we find one pointing to itself.
459 int start_index = index;
460 while (true) {
461 const int next = index_to_start_index_[start_index];
462 if (start_index == next) break;
463 start_index = next;
464 }
465
466 // Second, redo the same thing and make everyone point to the representative.
467 while (true) {
468 const int next = index_to_start_index_[index];
469 if (start_index == next) break;
470 index_to_start_index_[index] = start_index;
471 index = next;
472 }
473 return start_index;
474}
475
476bool AllDifferentBoundsPropagator::PropagateLowerBounds() {
477 // Start by filling the cached bounds and sorting by increasing lb.
478 for (VarValue& entry : vars_) {
479 entry.lb = integer_trail_->LowerBound(entry.var);
480 entry.ub = integer_trail_->UpperBound(entry.var);
481 }
482 IncrementalSort(vars_.begin(), vars_.end(),
483 [](VarValue a, VarValue b) { return a.lb < b.lb; });
484
485 // We will split the variable in vars sorted by lb in contiguous subset with
486 // index of the form [start, start + num_in_window).
487 int start = 0;
488 int num_in_window = 1;
489
490 // Minimum lower bound in the current window.
491 IntegerValue min_lb = vars_.front().lb;
492
493 const int size = vars_.size();
494 for (int i = 1; i < size; ++i) {
495 const IntegerValue lb = vars_[i].lb;
496
497 // If the lower bounds of all the other variables is greater, then it can
498 // never fall into a potential hall interval formed by the variable in the
499 // current window, so we can split the problem into independent parts.
500 if (lb <= min_lb + IntegerValue(num_in_window - 1)) {
501 ++num_in_window;
502 continue;
503 }
504
505 // Process the current window.
506 if (num_in_window > 1) {
507 absl::Span<VarValue> window(&vars_[start], num_in_window);
508 if (!PropagateLowerBoundsInternal(min_lb, window)) {
509 return false;
510 }
511 }
512
513 // Start of the next window.
514 start = i;
515 num_in_window = 1;
516 min_lb = lb;
517 }
518
519 // Take care of the last window.
520 if (num_in_window > 1) {
521 absl::Span<VarValue> window(&vars_[start], num_in_window);
522 return PropagateLowerBoundsInternal(min_lb, window);
523 }
524
525 return true;
526}
527
528bool AllDifferentBoundsPropagator::PropagateLowerBoundsInternal(
529 IntegerValue min_lb, absl::Span<VarValue> vars) {
530 hall_starts_.clear();
531 hall_ends_.clear();
532
533 // All cached lb in vars will be in [min_lb, min_lb + vars_.size()).
534 // Make sure we change our base_ so that GetIndex() fit in our buffers.
535 base_ = min_lb - IntegerValue(1);
536
537 // Sparse cleaning of value_to_nodes_.
538 for (const int i : indices_to_clear_) {
539 index_to_var_[i] = kNoIntegerVariable;
540 }
541 indices_to_clear_.clear();
542
543 // Sort vars by increasing ub.
544 std::sort(vars.begin(), vars.end(),
545 [](VarValue a, VarValue b) { return a.ub < b.ub; });
546 for (const VarValue entry : vars) {
547 const IntegerVariable var = entry.var;
548
549 // Note that it is important to use the cache to make sure GetIndex() is
550 // not out of bound in case integer_trail_->LowerBound() changed when we
551 // pushed something.
552 const IntegerValue lb = entry.lb;
553 const int lb_index = GetIndex(lb);
554 const bool value_is_covered = PointIsPresent(lb_index);
555
556 // Check if lb is in an Hall interval, and push it if this is the case.
557 if (value_is_covered) {
558 const int hall_index =
559 std::lower_bound(hall_ends_.begin(), hall_ends_.end(), lb) -
560 hall_ends_.begin();
561 if (hall_index < hall_ends_.size() && hall_starts_[hall_index] <= lb) {
562 const IntegerValue hs = hall_starts_[hall_index];
563 const IntegerValue he = hall_ends_[hall_index];
564 FillHallReason(hs, he);
565 integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(var, hs));
566 if (!integer_trail_->Enqueue(
568 /*literal_reason=*/{}, integer_reason_)) {
569 return false;
570 }
571 }
572 }
573
574 // Update our internal representation of the non-consecutive intervals.
575 //
576 // If lb is not used, we add a node there, otherwise we add it to the
577 // right of the interval that contains lb. In both cases, if there is an
578 // interval to the left (resp. right) we merge them.
579 int new_index = lb_index;
580 int start_index = lb_index;
581 int end_index = lb_index;
582 if (value_is_covered) {
583 start_index = FindStartIndexAndCompressPath(new_index);
584 new_index = index_to_end_index_[start_index] + 1;
585 end_index = new_index;
586 } else {
587 if (PointIsPresent(new_index - 1)) {
588 start_index = FindStartIndexAndCompressPath(new_index - 1);
589 }
590 }
591 if (PointIsPresent(new_index + 1)) {
592 end_index = index_to_end_index_[new_index + 1];
593 index_to_start_index_[new_index + 1] = start_index;
594 }
595
596 // Update the end of the representative.
597 index_to_end_index_[start_index] = end_index;
598
599 // This is the only place where we "add" a new node.
600 {
601 index_to_start_index_[new_index] = start_index;
602 index_to_var_[new_index] = var;
603 indices_to_clear_.push_back(new_index);
604 }
605
606 // We cannot have a conflict, because it should have beend detected before
607 // by pushing an interval lower bound past its upper bound.
608 //
609 // TODO(user): Not 100% clear since pushing can have side-effect, maybe we
610 // should just report the conflict if it happens!
611 const IntegerValue end = GetValue(end_index);
612 DCHECK_LE(end, integer_trail_->UpperBound(var));
613
614 // If we have a new Hall interval, add it to the set. Note that it will
615 // always be last, and if it overlaps some previous Hall intervals, it
616 // always overlaps them fully.
617 //
618 // Note: It is okay to not use entry.ub here if we want to fetch the last
619 // value, but in practice it shouldn't really change when we push a
620 // lower_bound and it is faster to use the cached entry.
621 if (end == entry.ub) {
622 const IntegerValue start = GetValue(start_index);
623 while (!hall_starts_.empty() && start <= hall_starts_.back()) {
624 hall_starts_.pop_back();
625 hall_ends_.pop_back();
626 }
627 DCHECK(hall_ends_.empty() || hall_ends_.back() < start);
628 hall_starts_.push_back(start);
629 hall_ends_.push_back(end);
630 }
631 }
632 return true;
633}
634
636 GenericLiteralWatcher* watcher) {
637 const int id = watcher->Register(this);
638 for (const VarValue entry : vars_) {
639 watcher->WatchIntegerVariable(entry.var, id);
640 }
642}
643
644} // namespace sat
645} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
const std::vector< IntVar * > vars_
Definition: alldiff_cst.cc:43
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
AllDifferentBoundsPropagator(const std::vector< IntegerVariable > &vars, IntegerTrail *integer_trail)
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterWith(GenericLiteralWatcher *watcher)
AllDifferentConstraint(std::vector< IntegerVariable > variables, IntegerEncoder *encoder, Trail *trail, IntegerTrail *integer_trail)
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1365
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
Definition: integer.h:1397
void SetPropagatorPriority(int id, int priority)
Definition: integer.cc:1962
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
void FullyEncodeVariable(IntegerVariable var)
Definition: integer.cc:36
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
Definition: integer.cc:106
bool VariableIsFullyEncoded(IntegerVariable var) const
Definition: integer.cc:68
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
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason(Literal true_literal)
Definition: sat_base.h:284
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
Block * next
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int FATAL
Definition: log_severity.h:32
const bool DEBUG_MODE
Definition: macros.h:24
const LiteralIndex kFalseLiteralIndex(-3)
std::function< void(Model *)> AllDifferentAC(const std::vector< IntegerVariable > &variables)
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< IntegerVariable > &vars)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
Definition: integer.h:1587
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> AtMostOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:890
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
std::function< void(Model *)> AllDifferentBinary(const std::vector< IntegerVariable > &vars)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
const LiteralIndex kTrueLiteralIndex(-2)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
void IncrementalSort(int max_comparisons, Iterator begin, Iterator end, Compare comp=Compare{}, bool is_stable=false)
Definition: sort.h:46
STL namespace.
int index
Definition: pack.cc:508
int64 capacity
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264