OR-Tools  8.2
var_domination.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
18
19namespace operations_research {
20namespace sat {
21
22void VarDomination::Reset(int num_variables) {
23 phase_ = 0;
24 num_vars_with_negation_ = 2 * num_variables;
25 partition_ = absl::make_unique<DynamicPartition>(num_vars_with_negation_);
26
27 can_freely_decrease_.assign(num_vars_with_negation_, true);
28
29 shared_buffer_.clear();
30 initial_candidates_.assign(num_vars_with_negation_, IntegerVariableSpan());
31
32 buffer_.clear();
33 dominating_vars_.assign(num_vars_with_negation_, IntegerVariableSpan());
34
35 ct_index_for_signature_ = 0;
36 block_down_signatures_.assign(num_vars_with_negation_, 0);
37}
38
39void VarDomination::RefinePartition(std::vector<int>* vars) {
40 if (vars->empty()) return;
41 partition_->Refine(*vars);
42 for (int& var : *vars) {
43 const IntegerVariable wrapped(var);
44 can_freely_decrease_[wrapped] = false;
45 can_freely_decrease_[NegationOf(wrapped)] = false;
46 var = NegationOf(wrapped).value();
47 }
48 partition_->Refine(*vars);
49}
50
51void VarDomination::CanOnlyDominateEachOther(absl::Span<const int> refs) {
52 if (phase_ != 0) return;
53 tmp_vars_.clear();
54 for (const int ref : refs) {
55 tmp_vars_.push_back(RefToIntegerVariable(ref).value());
56 }
57 RefinePartition(&tmp_vars_);
58 tmp_vars_.clear();
59}
60
61void VarDomination::ActivityShouldNotChange(absl::Span<const int> refs,
62 absl::Span<const int64> coeffs) {
63 if (phase_ != 0) return;
64 FillTempRanks(/*reverse_references=*/false, /*enforcements=*/{}, refs,
65 coeffs);
66 tmp_vars_.clear();
67 for (int i = 0; i < tmp_ranks_.size(); ++i) {
68 if (i > 0 && tmp_ranks_[i].rank != tmp_ranks_[i - 1].rank) {
69 RefinePartition(&tmp_vars_);
70 tmp_vars_.clear();
71 }
72 tmp_vars_.push_back(tmp_ranks_[i].var.value());
73 }
74 RefinePartition(&tmp_vars_);
75 tmp_vars_.clear();
76}
77
78// This correspond to a lower bounded constraint.
79void VarDomination::ProcessTempRanks() {
80 if (phase_ == 0) {
81 // We actually "split" tmp_ranks_ according to the current partition and
82 // process each resulting list independently for a faster algo.
83 ++ct_index_for_signature_;
84 for (IntegerVariableWithRank& entry : tmp_ranks_) {
85 can_freely_decrease_[entry.var] = false;
86 block_down_signatures_[entry.var] |= uint64{1}
87 << (ct_index_for_signature_ % 64);
88 entry.part = partition_->PartOf(entry.var.value());
89 }
90 std::stable_sort(
91 tmp_ranks_.begin(), tmp_ranks_.end(),
92 [](const IntegerVariableWithRank& a, const IntegerVariableWithRank& b) {
93 return a.part < b.part;
94 });
95 int start = 0;
96 for (int i = 1; i < tmp_ranks_.size(); ++i) {
97 if (tmp_ranks_[i].part != tmp_ranks_[start].part) {
98 Initialize({&tmp_ranks_[start], static_cast<size_t>(i - start)});
99 start = i;
100 }
101 }
102 if (start < tmp_ranks_.size()) {
103 Initialize({&tmp_ranks_[start], tmp_ranks_.size() - start});
104 }
105 } else if (phase_ == 1) {
106 FilterUsingTempRanks();
107 } else {
108 // This is only used for debugging, and we shouldn't reach here in prod.
109 CheckUsingTempRanks();
110 }
111}
112
114 absl::Span<const int> enforcements, absl::Span<const int> refs,
115 absl::Span<const int64> coeffs) {
116 FillTempRanks(/*reverse_references=*/false, enforcements, refs, coeffs);
117 ProcessTempRanks();
118}
119
121 absl::Span<const int> enforcements, absl::Span<const int> refs,
122 absl::Span<const int64> coeffs) {
123 FillTempRanks(/*reverse_references=*/true, enforcements, refs, coeffs);
124 ProcessTempRanks();
125}
126
127void VarDomination::MakeRankEqualToStartOfPart(
128 absl::Span<IntegerVariableWithRank> span) {
129 const int size = span.size();
130 int start = 0;
131 int previous_value = 0;
132 for (int i = 0; i < size; ++i) {
133 const int64 value = span[i].rank;
134 if (value != previous_value) {
135 previous_value = value;
136 start = i;
137 }
138 span[i].rank = start;
139 }
140}
141
142void VarDomination::Initialize(absl::Span<IntegerVariableWithRank> span) {
143 // The rank can be wrong and need to be recomputed because of how we splitted
144 // tmp_ranks_ into spans.
145 MakeRankEqualToStartOfPart(span);
146
147 const int future_start = shared_buffer_.size();
148 int first_start = -1;
149
150 // This is mainly to avoid corner case and hopefully, it should be big enough
151 // to not matter too much.
152 const int kSizeThreshold = 1000;
153 const int size = span.size();
154 for (int i = std::max(0, size - kSizeThreshold); i < size; ++i) {
155 const IntegerVariableWithRank entry = span[i];
156 const int num_candidates = size - entry.rank;
157 if (num_candidates >= kSizeThreshold) continue;
158
159 // Compute size to beat.
160 int size_threshold = kSizeThreshold;
161
162 // Take into account the current partition size.
163 const int var_part = partition_->PartOf(entry.var.value());
164 const int part_size = partition_->SizeOfPart(var_part);
165 size_threshold = std::min(size_threshold, part_size);
166
167 // Take into account our current best candidate if there is one.
168 const int current_num_candidates = initial_candidates_[entry.var].size;
169 if (current_num_candidates != 0) {
170 size_threshold = std::min(size_threshold, current_num_candidates);
171 }
172
173 if (num_candidates < size_threshold) {
174 if (first_start == -1) first_start = entry.rank;
175 initial_candidates_[entry.var] = {
176 future_start - first_start + static_cast<int>(entry.rank),
177 num_candidates};
178 }
179 }
180
181 // Only store what is necessary.
182 if (first_start == -1) return;
183 for (int i = first_start; i < size; ++i) {
184 shared_buffer_.push_back(span[i].var);
185 }
186}
187
188// TODO(user): Use more heuristics to not miss as much dominance relation when
189// we crop initial lists.
191 CHECK_EQ(phase_, 0);
192 phase_ = 1;
193
194 // Some initial lists ar too long and will be cropped to this size.
195 // We will handle them slightly differently.
196 //
197 // TODO(user): Tune the initial size, 50 might be a bit large, since our
198 // complexity is borned by this number times the number of entries in the
199 // constraints. Still we should in most situation be a lot lower than that.
200 const int kMaxInitialSize = 50;
201 std::vector<IntegerVariable> cropped_lists;
202 absl::StrongVector<IntegerVariable, bool> is_cropped(num_vars_with_negation_,
203 false);
204
205 // Fill the initial domination candidates.
206 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
207 if (can_freely_decrease_[var]) continue;
208 const int part = partition_->PartOf(var.value());
209 const int part_size = partition_->SizeOfPart(part);
210
211 const int start = buffer_.size();
212 int new_size = 0;
213
214 const uint64 var_sig = block_down_signatures_[var];
215 const uint64 not_var_sig = block_down_signatures_[NegationOf(var)];
216 const int stored_size = initial_candidates_[var].size;
217 if (stored_size == 0 || part_size < stored_size) {
218 // We start with the partition part.
219 // Note that all constraint will be filtered again in the second pass.
220 int num_tested = 0;
221 for (const int value : partition_->ElementsInPart(part)) {
222 const IntegerVariable c = IntegerVariable(value);
223
224 // This is to limit the complexity to 1k * num_vars. We fill the list
225 // with dummy node so that the heuristic below will fill it with
226 // potential transpose candidates.
227 if (++num_tested > 1000) {
228 is_cropped[var] = true;
229 cropped_lists.push_back(var);
230 int extra = new_size;
231 while (extra < kMaxInitialSize) {
232 ++extra;
233 buffer_.push_back(kNoIntegerVariable);
234 }
235 break;
236 }
237 if (PositiveVariable(c) == PositiveVariable(var)) continue;
238 if (can_freely_decrease_[NegationOf(c)]) continue;
239 if (var_sig & ~block_down_signatures_[c]) continue; // !included.
240 if (block_down_signatures_[NegationOf(c)] & ~not_var_sig) continue;
241 ++new_size;
242 buffer_.push_back(c);
243
244 // We do not want too many candidates per variables.
245 // TODO(user): randomize?
246 if (new_size > kMaxInitialSize) {
247 is_cropped[var] = true;
248 cropped_lists.push_back(var);
249 break;
250 }
251 }
252 } else {
253 // Copy the one that are in the same partition_ part.
254 //
255 // TODO(user): This can be too long maybe? even if we have list of at
256 // most 1000 at this point, see InitializeUsingTempRanks().
257 for (const IntegerVariable c : InitialDominatingCandidates(var)) {
258 if (PositiveVariable(c) == PositiveVariable(var)) continue;
259 if (can_freely_decrease_[NegationOf(c)]) continue;
260 if (partition_->PartOf(c.value()) != part) continue;
261 if (var_sig & ~block_down_signatures_[c]) continue; // !included.
262 if (block_down_signatures_[NegationOf(c)] & ~not_var_sig) continue;
263 ++new_size;
264 buffer_.push_back(c);
265
266 // We do not want too many candidates per variables.
267 // TODO(user): randomize?
268 if (new_size > kMaxInitialSize) {
269 is_cropped[var] = true;
270 cropped_lists.push_back(var);
271 break;
272 }
273 }
274 }
275
276 dominating_vars_[var] = {start, new_size};
277 }
278
279 // Heuristic: To try not to remove domination relations corresponding to short
280 // lists during transposition (see EndSecondPhase()), we fill half of the
281 // cropped list with the transpose of the short list relations. This helps
282 // finding more relation in the presence of cropped lists.
283 for (const IntegerVariable var : cropped_lists) {
284 if (kMaxInitialSize / 2 < dominating_vars_[var].size) {
285 dominating_vars_[var].size = kMaxInitialSize / 2; // Restrict.
286 }
287 }
288 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
289 for (const IntegerVariable dom : DominatingVariables(var)) {
290 if (!is_cropped[NegationOf(dom)]) continue;
291 IntegerVariableSpan& s = dominating_vars_[NegationOf(dom)];
292 if (s.size >= kMaxInitialSize) continue;
293 buffer_[s.start + s.size++] = NegationOf(var);
294 }
295 }
296
297 // Remove any duplicates.
298 //
299 // TODO(user): Maybe we should do that with all lists in case the
300 // input function are called with duplicates too.
301 for (const IntegerVariable var : cropped_lists) {
302 if (!is_cropped[var]) continue;
303 IntegerVariableSpan& s = dominating_vars_[var];
304 std::sort(&buffer_[s.start], &buffer_[s.start + s.size]);
305 const auto p = std::unique(&buffer_[s.start], &buffer_[s.start + s.size]);
306 s.size = p - &buffer_[s.start];
307 }
308
309 // We no longer need the first phase memory.
310 VLOG(1) << "Num initial list that where cropped: " << cropped_lists.size();
311 VLOG(1) << "Shared buffer size: " << shared_buffer_.size();
312 VLOG(1) << "Buffer size: " << buffer_.size();
313 gtl::STLClearObject(&initial_candidates_);
314 gtl::STLClearObject(&shared_buffer_);
315}
316
318 CHECK_EQ(phase_, 1);
319 phase_ = 2;
320
321 // Perform intersection with transpose.
322 shared_buffer_.clear();
323 initial_candidates_.assign(num_vars_with_negation_, IntegerVariableSpan());
324
325 // Pass 1: count.
326 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
327 for (const IntegerVariable dom : DominatingVariables(var)) {
328 ++initial_candidates_[NegationOf(dom)].size;
329 }
330 }
331
332 // Pass 2: compute starts.
333 int start = 0;
334 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
335 initial_candidates_[var].start = start;
336 start += initial_candidates_[var].size;
337 initial_candidates_[var].size = 0;
338 }
339 shared_buffer_.resize(start);
340
341 // Pass 3: transpose.
342 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
343 for (const IntegerVariable dom : DominatingVariables(var)) {
344 IntegerVariableSpan& span = initial_candidates_[NegationOf(dom)];
345 shared_buffer_[span.start + span.size++] = NegationOf(var);
346 }
347 }
348
349 // Pass 4: intersect.
350 int num_removed = 0;
351 tmp_var_to_rank_.resize(num_vars_with_negation_, -1);
352 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
353 for (const IntegerVariable dom : InitialDominatingCandidates(var)) {
354 tmp_var_to_rank_[dom] = 1;
355 }
356
357 int new_size = 0;
358 IntegerVariableSpan& span = dominating_vars_[var];
359 for (const IntegerVariable dom : DominatingVariables(var)) {
360 if (tmp_var_to_rank_[dom] != 1) {
361 ++num_removed;
362 continue;
363 }
364 buffer_[span.start + new_size++] = dom;
365 }
366 span.size = new_size;
367
368 for (const IntegerVariable dom : InitialDominatingCandidates(var)) {
369 tmp_var_to_rank_[dom] = -1;
370 }
371 }
372
373 VLOG(1) << "Transpose removed " << num_removed;
374 gtl::STLClearObject(&initial_candidates_);
375 gtl::STLClearObject(&shared_buffer_);
376}
377
378void VarDomination::FillTempRanks(bool reverse_references,
379 absl::Span<const int> enforcements,
380 absl::Span<const int> refs,
381 absl::Span<const int64> coeffs) {
382 tmp_ranks_.clear();
383 if (coeffs.empty()) {
384 // Simple case: all coefficients are assumed to be the same.
385 for (const int ref : refs) {
386 const IntegerVariable var =
387 RefToIntegerVariable(reverse_references ? NegatedRef(ref) : ref);
388 tmp_ranks_.push_back({var, 0, 0});
389 }
390 } else {
391 // Complex case: different coefficients.
392 for (int i = 0; i < refs.size(); ++i) {
393 if (coeffs[i] == 0) continue;
394 const IntegerVariable var = RefToIntegerVariable(
395 reverse_references ? NegatedRef(refs[i]) : refs[i]);
396 if (coeffs[i] > 0) {
397 tmp_ranks_.push_back({var, 0, coeffs[i]});
398 } else {
399 tmp_ranks_.push_back({NegationOf(var), 0, -coeffs[i]});
400 }
401 }
402 std::sort(tmp_ranks_.begin(), tmp_ranks_.end());
403 MakeRankEqualToStartOfPart({&tmp_ranks_[0], tmp_ranks_.size()});
404 }
405
406 // Add the enforcement last with a new rank. We add their negation since
407 // we want the activity to not decrease, and we want to allow any
408 // enforcement-- to dominate a variable in the constraint.
409 const int enforcement_rank = tmp_ranks_.size();
410 for (const int ref : enforcements) {
411 tmp_ranks_.push_back(
412 {RefToIntegerVariable(NegatedRef(ref)), 0, enforcement_rank});
413 }
414}
415
416// We take the intersection of the current dominating candidate with the
417// restriction imposed by the current content of tmp_ranks_.
418void VarDomination::FilterUsingTempRanks() {
419 // Expand ranks in temp vector.
420 tmp_var_to_rank_.resize(num_vars_with_negation_, -1);
421 for (const IntegerVariableWithRank entry : tmp_ranks_) {
422 tmp_var_to_rank_[entry.var] = entry.rank;
423 }
424
425 // The activity of the variable in tmp_rank must not decrease.
426 for (const IntegerVariableWithRank entry : tmp_ranks_) {
427 // The only variables that can be paired with a var-- in the constriants are
428 // the var++ in the constraints with the same rank or higher.
429 //
430 // Note that we only filter the var-- domination lists here, we do not
431 // remove the var-- appearing in all the lists corresponding to wrong var++.
432 // This is left to the tranpose operation in EndSecondPhase().
433 {
434 IntegerVariableSpan& span = dominating_vars_[entry.var];
435 if (span.size == 0) continue;
436 int new_size = 0;
437 for (const IntegerVariable candidate : DominatingVariables(entry.var)) {
438 if (tmp_var_to_rank_[candidate] < entry.rank) continue;
439 buffer_[span.start + new_size++] = candidate;
440 }
441 span.size = new_size;
442 }
443 }
444
445 // Reset temporary vector to all -1.
446 for (const IntegerVariableWithRank entry : tmp_ranks_) {
447 tmp_var_to_rank_[entry.var] = -1;
448 }
449}
450
451// Slow: This is for debugging only.
452void VarDomination::CheckUsingTempRanks() {
453 tmp_var_to_rank_.resize(num_vars_with_negation_, -1);
454 for (const IntegerVariableWithRank entry : tmp_ranks_) {
455 tmp_var_to_rank_[entry.var] = entry.rank;
456 }
457
458 // The activity of the variable in tmp_rank must not decrease.
459 for (IntegerVariable var(0); var < num_vars_with_negation_; ++var) {
460 const int var_rank = tmp_var_to_rank_[var];
461 const int negated_var_rank = tmp_var_to_rank_[NegationOf(var)];
462 for (const IntegerVariable dom : DominatingVariables(var)) {
463 CHECK(!can_freely_decrease_[NegationOf(dom)]);
464
465 // Doing X--, Y++ is compatible if the rank[X] <= rank[Y]. But we also
466 // need to check if doing Not(Y)-- is compatible with Not(X)++.
467 CHECK_LE(var_rank, tmp_var_to_rank_[dom]);
468 CHECK_LE(tmp_var_to_rank_[NegationOf(dom)], negated_var_rank);
469 }
470 }
471
472 for (const IntegerVariableWithRank entry : tmp_ranks_) {
473 tmp_var_to_rank_[entry.var] = -1;
474 }
475}
476
479}
480
481bool VarDomination::CanFreelyDecrease(IntegerVariable var) const {
482 return can_freely_decrease_[var];
483}
484
485absl::Span<const IntegerVariable> VarDomination::InitialDominatingCandidates(
486 IntegerVariable var) const {
487 const IntegerVariableSpan span = initial_candidates_[var];
488 if (span.size == 0) return absl::Span<const IntegerVariable>();
489 return absl::Span<const IntegerVariable>(&shared_buffer_[span.start],
490 span.size);
491}
492
493absl::Span<const IntegerVariable> VarDomination::DominatingVariables(
494 int ref) const {
496}
497
498absl::Span<const IntegerVariable> VarDomination::DominatingVariables(
499 IntegerVariable var) const {
500 const IntegerVariableSpan span = dominating_vars_[var];
501 if (span.size == 0) return absl::Span<const IntegerVariable>();
502 return absl::Span<const IntegerVariable>(&buffer_[span.start], span.size);
503}
504
505std::string VarDomination::DominationDebugString(IntegerVariable var) const {
506 const int ref = IntegerVariableToRef(var);
507 std::string result =
508 absl::StrCat(PositiveRef(ref), RefIsPositive(ref) ? "--" : "++", " : ");
509 for (const IntegerVariable dom : DominatingVariables(var)) {
510 const int dom_ref = IntegerVariableToRef(dom);
511 absl::StrAppend(&result, PositiveRef(dom_ref),
512 RefIsPositive(dom_ref) ? "++" : "--", " ");
513 }
514 return result;
515}
516
517// TODO(user): No need to set locking_ct_index_[var] if num_locks_[var] > 1
518void DualBoundStrengthening::CannotDecrease(absl::Span<const int> refs,
519 int ct_index) {
520 for (const int ref : refs) {
521 const IntegerVariable var = RefToIntegerVariable(ref);
522 can_freely_decrease_until_[var] = kMaxIntegerValue;
523 num_locks_[var]++;
524 locking_ct_index_[var] = ct_index;
525 }
526}
527
528void DualBoundStrengthening::CannotIncrease(absl::Span<const int> refs,
529 int ct_index) {
530 for (const int ref : refs) {
531 const IntegerVariable var = RefToIntegerVariable(ref);
532 can_freely_decrease_until_[NegationOf(var)] = kMaxIntegerValue;
533 num_locks_[NegationOf(var)]++;
534 locking_ct_index_[NegationOf(var)] = ct_index;
535 }
536}
537
538void DualBoundStrengthening::CannotMove(absl::Span<const int> refs) {
539 for (const int ref : refs) {
540 const IntegerVariable var = RefToIntegerVariable(ref);
541 can_freely_decrease_until_[var] = kMaxIntegerValue;
542 can_freely_decrease_until_[NegationOf(var)] = kMaxIntegerValue;
543 num_locks_[var]++;
544 num_locks_[NegationOf(var)]++;
545 }
546}
547
548template <typename LinearProto>
550 bool is_objective, const PresolveContext& context,
551 const LinearProto& linear, int64 min_activity, int64 max_activity) {
552 const int64 lb_limit = linear.domain(linear.domain_size() - 2);
553 const int64 ub_limit = linear.domain(1);
554 const int num_terms = linear.vars_size();
555 for (int i = 0; i < num_terms; ++i) {
556 int ref = linear.vars(i);
557 int64 coeff = linear.coeffs(i);
558 if (coeff < 0) {
559 ref = NegatedRef(ref);
560 coeff = -coeff;
561 }
562
563 const int64 min_term = coeff * context.MinOf(ref);
564 const int64 max_term = coeff * context.MaxOf(ref);
565 const int64 term_diff = max_term - min_term;
566 const IntegerVariable var = RefToIntegerVariable(ref);
567
568 // lb side.
569 if (min_activity < lb_limit) {
570 num_locks_[var]++;
571 if (min_activity + term_diff < lb_limit) {
572 can_freely_decrease_until_[var] = kMaxIntegerValue;
573 } else {
574 const IntegerValue slack(lb_limit - min_activity);
575 const IntegerValue var_diff =
576 CeilRatio(IntegerValue(slack), IntegerValue(coeff));
577 can_freely_decrease_until_[var] =
578 std::max(can_freely_decrease_until_[var],
579 IntegerValue(context.MinOf(ref)) + var_diff);
580 }
581 }
582
583 if (is_objective) {
584 // We never want to increase the objective value.
585 num_locks_[NegationOf(var)]++;
586 can_freely_decrease_until_[NegationOf(var)] = kMaxIntegerValue;
587 continue;
588 }
589
590 // ub side.
591 if (max_activity > ub_limit) {
592 num_locks_[NegationOf(var)]++;
593 if (max_activity - term_diff > ub_limit) {
594 can_freely_decrease_until_[NegationOf(var)] = kMaxIntegerValue;
595 } else {
596 const IntegerValue slack(max_activity - ub_limit);
597 const IntegerValue var_diff =
598 CeilRatio(IntegerValue(slack), IntegerValue(coeff));
599 can_freely_decrease_until_[NegationOf(var)] =
600 std::max(can_freely_decrease_until_[NegationOf(var)],
601 -IntegerValue(context.MaxOf(ref)) + var_diff);
602 }
603 }
604 }
605}
606
608 const CpModelProto& cp_model = *context->working_model;
609 const int num_vars = cp_model.variables_size();
610 for (int var = 0; var < num_vars; ++var) {
611 if (context->IsFixed(var)) continue;
612
613 // Fix to lb?
614 const int64 lb = context->MinOf(var);
615 const int64 ub_limit = std::max(lb, CanFreelyDecreaseUntil(var));
616 if (ub_limit == lb) {
617 context->UpdateRuleStats("dual: fix variable");
618 CHECK(context->IntersectDomainWith(var, Domain(lb)));
619 continue;
620 }
621
622 // Fix to ub?
623 const int64 ub = context->MaxOf(var);
624 const int64 lb_limit =
626 if (lb_limit == ub) {
627 context->UpdateRuleStats("dual: fix variable");
628 CHECK(context->IntersectDomainWith(var, Domain(ub)));
629 continue;
630 }
631
632 // Here we can fix to any value in [ub_limit, lb_limit] that is compatible
633 // with the current domain. We prefer zero or the lowest possible magnitude.
634 if (lb_limit > ub_limit) {
635 const Domain domain =
636 context->DomainOf(var).IntersectionWith(Domain(ub_limit, lb_limit));
637 if (!domain.IsEmpty()) {
638 int64 value = domain.Contains(0) ? 0 : domain.Min();
639 if (value != 0) {
640 for (const int64 bound : domain.FlattenedIntervals()) {
641 if (std::abs(bound) < std::abs(value)) value = bound;
642 }
643 }
644 context->UpdateRuleStats("dual: fix variable with multiple choices");
645 CHECK(context->IntersectDomainWith(var, Domain(value)));
646 continue;
647 }
648 }
649
650 // Here we can reduce the domain, but we must be careful when the domain
651 // has holes.
652 if (lb_limit > lb || ub_limit < ub) {
653 const int64 new_ub =
654 ub_limit < ub ? context->DomainOf(var)
655 .IntersectionWith(Domain(ub_limit, kint64max))
656 .Min()
657 : ub;
658 const int64 new_lb =
659 lb_limit > lb ? context->DomainOf(var)
660 .IntersectionWith(Domain(kint64min, lb_limit))
661 .Max()
662 : lb;
663 context->UpdateRuleStats("dual: reduced domain");
664 CHECK(context->IntersectDomainWith(var, Domain(new_lb, new_ub)));
665 }
666 }
667
668 // If (a => b) is the only constraint blocking a literal a in the up
669 // direction, then we can set a == b !
670 //
671 // TODO(user): We can deal with more general situation. For instance an at
672 // most one that is the only blocking constraint can become an exactly one.
673 std::vector<bool> processed(num_vars, false);
674 for (int positive_ref = 0; positive_ref < num_vars; ++positive_ref) {
675 if (processed[positive_ref]) continue;
676 if (context->IsFixed(positive_ref)) continue;
677 const IntegerVariable var = RefToIntegerVariable(positive_ref);
678 int ct_index = -1;
679 if (num_locks_[var] == 1 && locking_ct_index_[var] != -1) {
680 ct_index = locking_ct_index_[var];
681 } else if (num_locks_[NegationOf(var)] == 1 &&
682 locking_ct_index_[NegationOf(var)] != -1) {
683 ct_index = locking_ct_index_[NegationOf(var)];
684 } else {
685 continue;
686 }
687 const ConstraintProto& ct = context->working_model->constraints(ct_index);
688 if (ct.constraint_case() == ConstraintProto::kAtMostOne) {
689 context->UpdateRuleStats("TODO dual: tighten at most one");
690 continue;
691 }
692
693 if (ct.constraint_case() != ConstraintProto::kBoolAnd) continue;
694 if (ct.enforcement_literal().size() != 1) continue;
695
696 // Recover a => b where a is having an unique up_lock (i.e this constraint).
697 // Note that if many implications are encoded in the same bool_and, we have
698 // to be careful that a is appearing in just one of them.
699 int a = ct.enforcement_literal(0);
700 int b = 1;
701 if (PositiveRef(a) == positive_ref &&
702 num_locks_[RefToIntegerVariable(NegatedRef(a))] == 1) {
703 // Here, we can only add the equivalence if the literal is the only
704 // on the lhs, otherwise there is actually more lock.
705 if (ct.bool_and().literals().size() != 1) continue;
706 b = ct.bool_and().literals(0);
707 } else {
708 bool found = false;
709 b = NegatedRef(ct.enforcement_literal(0));
710 for (const int lhs : ct.bool_and().literals()) {
711 if (PositiveRef(lhs) == positive_ref &&
712 num_locks_[RefToIntegerVariable(lhs)] == 1) {
713 found = true;
714 a = NegatedRef(lhs);
715 break;
716 }
717 }
718 CHECK(found);
719 }
720 CHECK_EQ(num_locks_[RefToIntegerVariable(NegatedRef(a))], 1);
721
722 processed[PositiveRef(a)] = true;
723 processed[PositiveRef(b)] = true;
724 context->StoreBooleanEqualityRelation(a, b);
725 context->UpdateRuleStats("dual: enforced equivalence");
726 }
727
728 return true;
729}
730
731namespace {
732
733// TODO(user): Maybe we should avoid recomputing that here.
734template <typename LinearExprProto>
735void FillMinMaxActivity(const PresolveContext& context,
736 const LinearExprProto& proto, int64* min_activity,
737 int64* max_activity) {
738 *min_activity = 0;
739 *max_activity = 0;
740 const int num_vars = proto.vars().size();
741 for (int i = 0; i < num_vars; ++i) {
742 const int64 a = proto.coeffs(i) * context.MinOf(proto.vars(i));
743 const int64 b = proto.coeffs(i) * context.MaxOf(proto.vars(i));
744 *min_activity += std::min(a, b);
745 *max_activity += std::max(a, b);
746 }
747}
748
749} // namespace
750
752 const PresolveContext& context, VarDomination* var_domination,
753 DualBoundStrengthening* dual_bound_strengthening) {
754 const CpModelProto& cp_model = *context.working_model;
755 const int num_vars = cp_model.variables().size();
756 var_domination->Reset(num_vars);
757 dual_bound_strengthening->Reset(num_vars);
758
759 int64 min_activity = kint64min;
760 int64 max_activity = kint64max;
761
762 for (int var = 0; var < num_vars; ++var) {
763 // Deal with the affine relations that are not part of the proto.
764 // Those only need to be processed in the first pass.
765 //
766 // TODO(user): This is not ideal since if only the representative is still
767 // used, we shouldn't restrict any dominance relation involving it.
768 const AffineRelation::Relation r = context.GetAffineRelation(var);
769 if (r.representative != var) {
770 dual_bound_strengthening->CannotMove({var, r.representative});
771 if (r.coeff == 1) {
772 var_domination->CanOnlyDominateEachOther(
774 } else if (r.coeff == -1) {
775 var_domination->CanOnlyDominateEachOther({var, r.representative});
776 } else {
777 var_domination->CanOnlyDominateEachOther({var});
778 var_domination->CanOnlyDominateEachOther({r.representative});
779 }
780 }
781
782 // Also ignore variables that have been substitued already or are unused.
783 if (context.IsFixed(var) || context.VariableWasRemoved(var) ||
784 context.VariableIsNotUsedAnymore(var)) {
785 dual_bound_strengthening->CannotMove({var});
786 var_domination->CanOnlyDominateEachOther({var});
787 }
788 }
789
790 // TODO(user): Benchmark and experiment with 3 phases algo:
791 // - Only ActivityShouldNotChange()/CanOnlyDominateEachOther().
792 // - The other cases once.
793 // - EndFirstPhase() and then the other cases a second time.
794 std::vector<int> tmp;
795 const int num_constraints = cp_model.constraints_size();
796 for (int phase = 0; phase < 2; phase++) {
797 for (int c = 0; c < num_constraints; ++c) {
798 const ConstraintProto& ct = cp_model.constraints(c);
799 if (phase == 0) {
800 dual_bound_strengthening->CannotIncrease(ct.enforcement_literal(), c);
801 }
802 switch (ct.constraint_case()) {
803 case ConstraintProto::kBoolOr:
804 if (phase == 0) {
805 dual_bound_strengthening->CannotDecrease(ct.bool_or().literals());
806 }
807 var_domination->ActivityShouldNotDecrease(ct.enforcement_literal(),
808 ct.bool_or().literals(),
809 /*coeffs=*/{});
810 break;
811 case ConstraintProto::kBoolAnd:
812 if (phase == 0) {
813 dual_bound_strengthening->CannotDecrease(ct.bool_and().literals(),
814 c);
815 }
816
817 // We process it like n clauses.
818 //
819 // TODO(user): the way we process that is a bit restrictive. By
820 // working on the implication graph we could detect more dominance
821 // relations. Since if a => b we say that a++ can only be paired with
822 // b--, but it could actually be paired with any variables that when
823 // dereased implies b = 0. This is a bit mitigated by the fact that
824 // we regroup when we can such implications into big at most ones.
825 tmp.clear();
826 for (const int ref : ct.enforcement_literal()) {
827 tmp.push_back(NegatedRef(ref));
828 }
829 for (const int ref : ct.bool_and().literals()) {
830 tmp.push_back(ref);
831 var_domination->ActivityShouldNotDecrease(/*enforcements=*/{}, tmp,
832 /*coeffs=*/{});
833 tmp.pop_back();
834 }
835 break;
836 case ConstraintProto::kAtMostOne:
837 if (phase == 0) {
838 dual_bound_strengthening->CannotIncrease(
839 ct.at_most_one().literals(), c);
840 }
841 var_domination->ActivityShouldNotIncrease(ct.enforcement_literal(),
842 ct.at_most_one().literals(),
843 /*coeffs=*/{});
844 break;
845 case ConstraintProto::kExactlyOne:
846 if (phase == 0) {
847 dual_bound_strengthening->CannotMove(ct.exactly_one().literals());
848 }
849 var_domination->ActivityShouldNotChange(ct.exactly_one().literals(),
850 /*coeffs=*/{});
851 break;
852 case ConstraintProto::kLinear: {
853 FillMinMaxActivity(context, ct.linear(), &min_activity,
854 &max_activity);
855 if (phase == 0) {
856 dual_bound_strengthening->ProcessLinearConstraint(
857 false, context, ct.linear(), min_activity, max_activity);
858 }
859 const bool domain_is_simple = ct.linear().domain().size() == 2;
860 const bool free_to_increase =
861 domain_is_simple && ct.linear().domain(1) >= max_activity;
862 const bool free_to_decrease =
863 domain_is_simple && ct.linear().domain(0) <= min_activity;
864 if (free_to_decrease && free_to_increase) break;
865 if (free_to_increase) {
866 var_domination->ActivityShouldNotDecrease(ct.enforcement_literal(),
867 ct.linear().vars(),
868 ct.linear().coeffs());
869 } else if (free_to_decrease) {
870 var_domination->ActivityShouldNotIncrease(ct.enforcement_literal(),
871 ct.linear().vars(),
872 ct.linear().coeffs());
873 } else {
874 // TODO(user): Handle enforcement better here.
875 if (!ct.enforcement_literal().empty()) {
876 var_domination->ActivityShouldNotIncrease(
877 /*enforcements=*/{}, ct.enforcement_literal(), /*coeffs=*/{});
878 }
879 var_domination->ActivityShouldNotChange(ct.linear().vars(),
880 ct.linear().coeffs());
881 }
882 break;
883 }
884 default:
885 // We cannot infer anything if we don't know the constraint.
886 // TODO(user): Handle enforcement better here.
887 if (phase == 0) {
888 dual_bound_strengthening->CannotMove(context.ConstraintToVars(c));
889 }
890 for (const int var : context.ConstraintToVars(c)) {
891 var_domination->CanOnlyDominateEachOther({var});
892 }
893 break;
894 }
895 }
896
897 // The objective is handled like a <= constraints, or an == constraint if
898 // there is a non-trivial domain.
899 if (cp_model.has_objective()) {
900 // WARNING: The proto objective might not be up to date, so we need to
901 // write it first.
902 if (phase == 0) context.WriteObjectiveToProto();
903 FillMinMaxActivity(context, cp_model.objective(), &min_activity,
904 &max_activity);
905 dual_bound_strengthening->ProcessLinearConstraint(
906 true, context, cp_model.objective(), min_activity, max_activity);
907 const auto& domain = cp_model.objective().domain();
908 if (domain.empty() || (domain.size() == 2 && domain[0] <= min_activity)) {
909 var_domination->ActivityShouldNotIncrease(
910 /*enforcements=*/{}, cp_model.objective().vars(),
911 cp_model.objective().coeffs());
912 } else {
913 var_domination->ActivityShouldNotChange(cp_model.objective().vars(),
914 cp_model.objective().coeffs());
915 }
916 }
917
918 if (phase == 0) var_domination->EndFirstPhase();
919 if (phase == 1) var_domination->EndSecondPhase();
920 }
921
922 // Some statistics.
923 int64 num_unconstrained_refs = 0;
924 int64 num_dominated_refs = 0;
925 int64 num_dominance_relations = 0;
926 for (int var = 0; var < num_vars; ++var) {
927 if (context.IsFixed(var)) continue;
928
929 for (const int ref : {var, NegatedRef(var)}) {
930 if (var_domination->CanFreelyDecrease(ref)) {
931 num_unconstrained_refs++;
932 } else if (!var_domination->DominatingVariables(ref).empty()) {
933 num_dominated_refs++;
934 num_dominance_relations +=
935 var_domination->DominatingVariables(ref).size();
936 }
937 }
938 }
939 if (num_unconstrained_refs == 0 && num_dominated_refs == 0) return;
940 VLOG(1) << "Dominance:"
941 << " num_unconstrained_refs=" << num_unconstrained_refs
942 << " num_dominated_refs=" << num_dominated_refs
943 << " num_dominance_relations=" << num_dominance_relations;
944}
945
946bool ExploitDominanceRelations(const VarDomination& var_domination,
948 const CpModelProto& cp_model = *context->working_model;
949 const int num_vars = cp_model.variables_size();
950
951 // Abort early if there is nothing to do.
952 bool work_to_do = false;
953 for (int var = 0; var < num_vars; ++var) {
954 if (context->IsFixed(var)) continue;
955 if (!var_domination.DominatingVariables(var).empty() ||
956 !var_domination.DominatingVariables(NegatedRef(var)).empty()) {
957 work_to_do = true;
958 break;
959 }
960 }
961 if (!work_to_do) return true;
962
963 absl::StrongVector<IntegerVariable, int64> var_lb_to_ub_diff(num_vars * 2, 0);
964 absl::StrongVector<IntegerVariable, bool> in_constraints(num_vars * 2, false);
965
966 const int num_constraints = cp_model.constraints_size();
967 for (int c = 0; c < num_constraints; ++c) {
968 const ConstraintProto& ct = cp_model.constraints(c);
969
970 if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
971 if (ct.enforcement_literal().size() != 1) continue;
972 const int a = ct.enforcement_literal(0);
973 if (context->IsFixed(a)) continue;
974 for (const int b : ct.bool_and().literals()) {
975 if (context->IsFixed(b)) continue;
976
977 // If (a--, b--) is valid, we can always set a to false.
978 for (const IntegerVariable ivar :
979 var_domination.DominatingVariables(a)) {
980 const int ref = VarDomination::IntegerVariableToRef(ivar);
981 if (ref == NegatedRef(b)) {
982 context->UpdateRuleStats("domination: in implication");
983 if (!context->SetLiteralToFalse(a)) return false;
984 break;
985 }
986 }
987 if (context->IsFixed(a)) break;
988
989 // If (b++, a++) is valid, then we can always set b to true.
990 for (const IntegerVariable ivar :
991 var_domination.DominatingVariables(NegatedRef(b))) {
992 const int ref = VarDomination::IntegerVariableToRef(ivar);
993 if (ref == a) {
994 context->UpdateRuleStats("domination: in implication");
995 if (!context->SetLiteralToTrue(b)) return false;
996 break;
997 }
998 }
999 }
1000 continue;
1001 }
1002
1003 if (!ct.enforcement_literal().empty()) continue;
1004
1005 // TODO(user): Also deal with exactly one.
1006 // TODO(user): More generally, combine with probing? if a dominated variable
1007 // implies one of its dominant to zero, then it can be set to zero. It seems
1008 // adding the implication below should have the same effect? but currently
1009 // it requires a lot of presolve rounds.
1010 if (ct.constraint_case() == ConstraintProto::kAtMostOne) {
1011 for (const int ref : ct.at_most_one().literals()) {
1012 in_constraints[VarDomination::RefToIntegerVariable(ref)] = true;
1013 }
1014 for (const int ref : ct.at_most_one().literals()) {
1015 if (context->IsFixed(ref)) continue;
1016
1017 const auto dominating_ivars = var_domination.DominatingVariables(ref);
1018 if (dominating_ivars.empty()) continue;
1019 for (const IntegerVariable ivar : dominating_ivars) {
1020 if (!in_constraints[ivar]) continue;
1021 if (context->IsFixed(VarDomination::IntegerVariableToRef(ivar))) {
1022 continue;
1023 }
1024
1025 // We can set the dominated variable to false.
1026 context->UpdateRuleStats("domination: in at most one");
1027 if (!context->SetLiteralToFalse(ref)) return false;
1028 break;
1029 }
1030 }
1031 for (const int ref : ct.at_most_one().literals()) {
1032 in_constraints[VarDomination::RefToIntegerVariable(ref)] = false;
1033 }
1034 }
1035
1036 if (ct.constraint_case() != ConstraintProto::kLinear) continue;
1037
1038 int num_dominated = 0;
1039 for (const int var : context->ConstraintToVars(c)) {
1040 if (!var_domination.DominatingVariables(var).empty()) ++num_dominated;
1041 if (!var_domination.DominatingVariables(NegatedRef(var)).empty()) {
1042 ++num_dominated;
1043 }
1044 }
1045 if (num_dominated == 0) continue;
1046
1047 // Precompute.
1048 int64 min_activity = 0;
1049 int64 max_activity = 0;
1050 const int num_terms = ct.linear().vars_size();
1051 for (int i = 0; i < num_terms; ++i) {
1052 int ref = ct.linear().vars(i);
1053 int64 coeff = ct.linear().coeffs(i);
1054 if (coeff < 0) {
1055 ref = NegatedRef(ref);
1056 coeff = -coeff;
1057 }
1058 const int64 min_term = coeff * context->MinOf(ref);
1059 const int64 max_term = coeff * context->MaxOf(ref);
1060 min_activity += min_term;
1061 max_activity += max_term;
1062 const IntegerVariable ivar = VarDomination::RefToIntegerVariable(ref);
1063 var_lb_to_ub_diff[ivar] = max_term - min_term;
1064 var_lb_to_ub_diff[NegationOf(ivar)] = min_term - max_term;
1065 }
1066 const int64 rhs_lb = ct.linear().domain(0);
1067 const int64 rhs_ub = ct.linear().domain(ct.linear().domain_size() - 1);
1068 if (max_activity < rhs_lb || min_activity > rhs_ub) {
1069 return context->NotifyThatModelIsUnsat("linear equation unsat.");
1070 }
1071
1072 // Look for dominated var.
1073 for (int i = 0; i < num_terms; ++i) {
1074 const int ref = ct.linear().vars(i);
1075 const int64 coeff = ct.linear().coeffs(i);
1076 const int64 coeff_magnitude = std::abs(coeff);
1077 if (context->IsFixed(ref)) continue;
1078
1079 for (const int current_ref : {ref, NegatedRef(ref)}) {
1080 const absl::Span<const IntegerVariable> dominated_by =
1081 var_domination.DominatingVariables(current_ref);
1082 if (dominated_by.empty()) continue;
1083
1084 const bool ub_side = (coeff > 0) == (current_ref == ref);
1085 if (ub_side) {
1086 if (max_activity <= rhs_ub) continue;
1087 } else {
1088 if (min_activity >= rhs_lb) continue;
1089 }
1090 const int64 slack =
1091 ub_side ? rhs_ub - min_activity : max_activity - rhs_lb;
1092
1093 // Compute the delta in activity if all dominating var moves to their
1094 // other bound.
1095 int64 delta = 0;
1096 for (const IntegerVariable ivar : dominated_by) {
1097 if (ub_side) {
1098 delta += std::max(int64{0}, var_lb_to_ub_diff[ivar]);
1099 } else {
1100 delta += std::max(int64{0}, -var_lb_to_ub_diff[ivar]);
1101 }
1102 }
1103
1104 const int64 lb = context->MinOf(current_ref);
1105 if (delta + coeff_magnitude > slack) {
1106 context->UpdateRuleStats("domination: fixed to lb.");
1107 if (!context->IntersectDomainWith(current_ref, Domain(lb))) {
1108 return false;
1109 }
1110
1111 // We need to update the precomputed quantities.
1112 const IntegerVariable current_var =
1114 if (ub_side) {
1115 CHECK_GE(var_lb_to_ub_diff[current_var], 0);
1116 max_activity -= var_lb_to_ub_diff[current_var];
1117 } else {
1118 CHECK_LE(var_lb_to_ub_diff[current_var], 0);
1119 min_activity -= var_lb_to_ub_diff[current_var];
1120 }
1121 var_lb_to_ub_diff[current_var] = 0;
1122 var_lb_to_ub_diff[NegationOf(current_var)] = 0;
1123
1124 continue;
1125 }
1126
1127 const IntegerValue diff = FloorRatio(IntegerValue(slack - delta),
1128 IntegerValue(coeff_magnitude));
1129 const int64 new_ub = lb + diff.value();
1130 if (new_ub < context->MaxOf(current_ref)) {
1131 context->UpdateRuleStats("domination: reduced ub.");
1132 if (!context->IntersectDomainWith(current_ref, Domain(lb, new_ub))) {
1133 return false;
1134 }
1135
1136 // We need to update the precomputed quantities.
1137 const IntegerVariable current_var =
1139 if (ub_side) {
1140 CHECK_GE(var_lb_to_ub_diff[current_var], 0);
1141 max_activity -= var_lb_to_ub_diff[current_var];
1142 } else {
1143 CHECK_LE(var_lb_to_ub_diff[current_var], 0);
1144 min_activity -= var_lb_to_ub_diff[current_var];
1145 }
1146 const int64 new_diff = std::abs(coeff_magnitude * (new_ub - lb));
1147 if (ub_side) {
1148 var_lb_to_ub_diff[current_var] = new_diff;
1149 var_lb_to_ub_diff[NegationOf(current_var)] = -new_diff;
1150 max_activity += new_diff;
1151 } else {
1152 var_lb_to_ub_diff[current_var] = -new_diff;
1153 var_lb_to_ub_diff[NegationOf(current_var)] = +new_diff;
1154 min_activity -= new_diff;
1155 }
1156 }
1157 }
1158 }
1159
1160 // Restore.
1161 for (const int ref : ct.linear().vars()) {
1162 const IntegerVariable ivar = VarDomination::RefToIntegerVariable(ref);
1163 var_lb_to_ub_diff[ivar] = 0;
1164 var_lb_to_ub_diff[NegationOf(ivar)] = 0;
1165 }
1166 }
1167
1168 // For any dominance relation still left (i.e. between non-fixed vars), if
1169 // the variable are Boolean and X is dominated by Y, we can add
1170 // (X == 1) => (Y = 1). But, as soon as we do that, we break some symmetry
1171 // and cannot add any incompatible relations.
1172 //
1173 // EX: It is possible that X dominate Y and Y dominate X if they are both
1174 // appearing in exactly the same constraint with the same coefficient.
1175 //
1176 // TODO(user): generalize to non Booleans?
1177 // TODO(user): We always keep adding the same relations. Do that only once!
1178 int num_added = 0;
1179 absl::StrongVector<IntegerVariable, bool> increase_is_forbidden(2 * num_vars,
1180 false);
1181 for (int positive_ref = 0; positive_ref < num_vars; ++positive_ref) {
1182 if (context->IsFixed(positive_ref)) continue;
1183 if (!context->CanBeUsedAsLiteral(positive_ref)) continue;
1184 for (const int ref : {positive_ref, NegatedRef(positive_ref)}) {
1185 const IntegerVariable var = VarDomination::RefToIntegerVariable(ref);
1186 if (increase_is_forbidden[NegationOf(var)]) continue;
1187 for (const IntegerVariable dom :
1188 var_domination.DominatingVariables(ref)) {
1189 if (increase_is_forbidden[dom]) continue;
1190 const int dom_ref = VarDomination::IntegerVariableToRef(dom);
1191 if (context->IsFixed(dom_ref)) continue;
1192 if (!context->CanBeUsedAsLiteral(dom_ref)) continue;
1193 ++num_added;
1194 context->AddImplication(ref, dom_ref);
1195
1196 // dom-- or var++ are now forbidden.
1197 increase_is_forbidden[var] = true;
1198 increase_is_forbidden[NegationOf(dom)] = true;
1199 }
1200 }
1201 }
1202 if (num_added > 0) {
1203 VLOG(1) << "Added " << num_added << " domination implications.";
1204 context->UpdateNewConstraintsVariableUsage();
1205 context->UpdateRuleStats("domination: added implications", num_added);
1206 }
1207
1208 return true;
1209}
1210
1211} // namespace sat
1212} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
#define VLOG(verboselevel)
Definition: base/logging.h:978
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
size_type size() const
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
int64 Min() const
Returns the min value of the domain.
std::vector< int64 > FlattenedIntervals() const
This method returns the flattened list of interval bounds of the domain.
bool IsEmpty() const
Returns true if this is the empty set.
bool Contains(int64 value) const
Returns true iff value is in Domain.
void CannotMove(absl::Span< const int > refs)
void ProcessLinearConstraint(bool is_objective, const PresolveContext &context, const LinearProto &linear, int64 min_activity, int64 max_activity)
void CannotIncrease(absl::Span< const int > refs, int ct_index=-1)
void CannotDecrease(absl::Span< const int > refs, int ct_index=-1)
void ActivityShouldNotDecrease(absl::Span< const int > enforcements, absl::Span< const int > refs, absl::Span< const int64 > coeffs)
void ActivityShouldNotIncrease(absl::Span< const int > enforcements, absl::Span< const int > refs, absl::Span< const int64 > coeffs)
static int IntegerVariableToRef(IntegerVariable var)
void ActivityShouldNotChange(absl::Span< const int > refs, absl::Span< const int64 > coeffs)
absl::Span< const IntegerVariable > DominatingVariables(int ref) const
std::string DominationDebugString(IntegerVariable var) const
static IntegerVariable RefToIntegerVariable(int ref)
void CanOnlyDominateEachOther(absl::Span< const int > refs)
CpModelProto proto
DecisionBuilder *const phase
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GurobiMPCallbackContext * context
static const int64 kint64max
int64_t int64
uint64_t uint64
static const int64 kint64min
void STLClearObject(T *obj)
Definition: stl_util.h:123
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
void DetectDominanceRelations(const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
bool ExploitDominanceRelations(const VarDomination &var_domination, PresolveContext *context)
bool RefIsPositive(int ref)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 delta
Definition: resource.cc:1684
Fractional coeff_magnitude
int64 bound