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 
16 #include "ortools/base/stl_util.h"
18 
19 namespace operations_research {
20 namespace sat {
21 
22 void 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 
39 void 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 
51 void 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 
61 void 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.
79 void 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 
127 void 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 
142 void 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 
378 void 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_.
418 void 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.
452 void 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 
477 bool VarDomination::CanFreelyDecrease(int ref) const {
479 }
480 
481 bool VarDomination::CanFreelyDecrease(IntegerVariable var) const {
482  return can_freely_decrease_[var];
483 }
484 
485 absl::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 
493 absl::Span<const IntegerVariable> VarDomination::DominatingVariables(
494  int ref) const {
496 }
497 
498 absl::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 
505 std::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
518 void 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 
528 void 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 
538 void 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 
548 template <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 
731 namespace {
732 
733 // TODO(user): Maybe we should avoid recomputing that here.
734 template <typename LinearExprProto>
735 void 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 
946 bool 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
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
bool RefIsPositive(int ref)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
const IntegerVariable kNoIntegerVariable(-1)
void DetectDominanceRelations(const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
bool ExploitDominanceRelations(const VarDomination &var_domination, PresolveContext *context)
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