OR-Tools  8.2
integer.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 
14 #include "ortools/sat/integer.h"
15 
16 #include <algorithm>
17 #include <queue>
18 #include <type_traits>
19 
21 #include "ortools/base/stl_util.h"
23 
24 namespace operations_research {
25 namespace sat {
26 
27 std::vector<IntegerVariable> NegationOf(
28  const std::vector<IntegerVariable>& vars) {
29  std::vector<IntegerVariable> result(vars.size());
30  for (int i = 0; i < vars.size(); ++i) {
31  result[i] = NegationOf(vars[i]);
32  }
33  return result;
34 }
35 
37  if (VariableIsFullyEncoded(var)) return;
38 
39  CHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
40  CHECK(!(*domains_)[var].IsEmpty()); // UNSAT. We don't deal with that here.
41  CHECK_LT((*domains_)[var].Size(), 100000)
42  << "Domain too large for full encoding.";
43 
44  // TODO(user): Maybe we can optimize the literal creation order and their
45  // polarity as our default SAT heuristics initially depends on this.
46  //
47  // TODO(user): Currently, in some corner cases,
48  // GetOrCreateLiteralAssociatedToEquality() might trigger some propagation
49  // that update the domain of var, so we need to cache the values to not read
50  // garbage. Note that it is okay to call the function on values no longer
51  // reachable, as this will just do nothing.
52  tmp_values_.clear();
53  for (const ClosedInterval interval : (*domains_)[var]) {
54  for (IntegerValue v(interval.start); v <= interval.end; ++v) {
55  tmp_values_.push_back(v);
56  }
57  }
58  for (const IntegerValue v : tmp_values_) {
60  }
61 
62  // Mark var and Negation(var) as fully encoded.
63  CHECK_LT(GetPositiveOnlyIndex(var), is_fully_encoded_.size());
64  CHECK(!equality_by_var_[GetPositiveOnlyIndex(var)].empty());
65  is_fully_encoded_[GetPositiveOnlyIndex(var)] = true;
66 }
67 
68 bool IntegerEncoder::VariableIsFullyEncoded(IntegerVariable var) const {
69  const PositiveOnlyIndex index = GetPositiveOnlyIndex(var);
70  if (index >= is_fully_encoded_.size()) return false;
71 
72  // Once fully encoded, the status never changes.
73  if (is_fully_encoded_[index]) return true;
75 
76  // TODO(user): Cache result as long as equality_by_var_[index] is unchanged?
77  // It might not be needed since if the variable is not fully encoded, then
78  // PartialDomainEncoding() will filter unreachable values, and so the size
79  // check will be false until further value have been encoded.
80  const int64 initial_domain_size = (*domains_)[var].Size();
81  if (equality_by_var_[index].size() < initial_domain_size) return false;
82 
83  // This cleans equality_by_var_[index] as a side effect and in particular,
84  // sorts it by values.
86 
87  // TODO(user): Comparing the size might be enough, but we want to be always
88  // valid even if either (*domains_[var]) or PartialDomainEncoding(var) are
89  // not properly synced because the propagation is not finished.
90  const auto& ref = equality_by_var_[index];
91  int i = 0;
92  for (const ClosedInterval interval : (*domains_)[var]) {
93  for (int64 v = interval.start; v <= interval.end; ++v) {
94  if (i < ref.size() && v == ref[i].value) {
95  i++;
96  }
97  }
98  }
99  if (i == ref.size()) {
100  is_fully_encoded_[index] = true;
101  }
102  return is_fully_encoded_[index];
103 }
104 
105 std::vector<IntegerEncoder::ValueLiteralPair>
106 IntegerEncoder::FullDomainEncoding(IntegerVariable var) const {
108  return PartialDomainEncoding(var);
109 }
110 
111 std::vector<IntegerEncoder::ValueLiteralPair>
113  CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
114  const PositiveOnlyIndex index = GetPositiveOnlyIndex(var);
115  if (index >= equality_by_var_.size()) return {};
116 
117  int new_size = 0;
118  std::vector<ValueLiteralPair>& ref = equality_by_var_[index];
119  for (int i = 0; i < ref.size(); ++i) {
120  const ValueLiteralPair pair = ref[i];
121  if (sat_solver_->Assignment().LiteralIsFalse(pair.literal)) continue;
122  if (sat_solver_->Assignment().LiteralIsTrue(pair.literal)) {
123  ref.clear();
124  ref.push_back(pair);
125  new_size = 1;
126  break;
127  }
128  ref[new_size++] = pair;
129  }
130  ref.resize(new_size);
131  std::sort(ref.begin(), ref.end());
132 
133  std::vector<IntegerEncoder::ValueLiteralPair> result = ref;
134  if (!VariableIsPositive(var)) {
135  std::reverse(result.begin(), result.end());
136  for (ValueLiteralPair& ref : result) ref.value = -ref.value;
137  }
138  return result;
139 }
140 
141 // Note that by not inserting the literal in "order" we can in the worst case
142 // use twice as much implication (2 by literals) instead of only one between
143 // consecutive literals.
144 void IntegerEncoder::AddImplications(
145  const std::map<IntegerValue, Literal>& map,
146  std::map<IntegerValue, Literal>::const_iterator it,
147  Literal associated_lit) {
148  if (!add_implications_) return;
149  DCHECK_EQ(it->second, associated_lit);
150 
151  // Literal(after) => associated_lit
152  auto after_it = it;
153  ++after_it;
154  if (after_it != map.end()) {
155  sat_solver_->AddClauseDuringSearch(
156  {after_it->second.Negated(), associated_lit});
157  }
158 
159  // associated_lit => Literal(before)
160  if (it != map.begin()) {
161  auto before_it = it;
162  --before_it;
163  sat_solver_->AddClauseDuringSearch(
164  {associated_lit.Negated(), before_it->second});
165  }
166 }
167 
169  CHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
170  add_implications_ = true;
171  for (const std::map<IntegerValue, Literal>& encoding : encoding_by_var_) {
172  LiteralIndex previous = kNoLiteralIndex;
173  for (const auto value_literal : encoding) {
174  const Literal lit = value_literal.second;
175  if (previous != kNoLiteralIndex) {
176  // lit => previous.
177  sat_solver_->AddBinaryClause(lit.Negated(), Literal(previous));
178  }
179  previous = lit.Index();
180  }
181  }
182 }
183 
184 std::pair<IntegerLiteral, IntegerLiteral> IntegerEncoder::Canonicalize(
185  IntegerLiteral i_lit) const {
186  const IntegerVariable var(i_lit.var);
187  IntegerValue after(i_lit.bound);
188  IntegerValue before(i_lit.bound - 1);
189  CHECK_GE(before, (*domains_)[var].Min());
190  CHECK_LE(after, (*domains_)[var].Max());
191  int64 previous = kint64min;
192  for (const ClosedInterval& interval : (*domains_)[var]) {
193  if (before > previous && before < interval.start) before = previous;
194  if (after > previous && after < interval.start) after = interval.start;
195  if (after <= interval.end) break;
196  previous = interval.end;
197  }
198  return {IntegerLiteral::GreaterOrEqual(var, after),
200 }
201 
203  if (i_lit.bound <= (*domains_)[i_lit.var].Min()) {
204  return GetTrueLiteral();
205  }
206  if (i_lit.bound > (*domains_)[i_lit.var].Max()) {
207  return GetFalseLiteral();
208  }
209 
210  const auto canonicalization = Canonicalize(i_lit);
211  const IntegerLiteral new_lit = canonicalization.first;
212 
213  const LiteralIndex index = GetAssociatedLiteral(new_lit);
214  if (index != kNoLiteralIndex) return Literal(index);
215  const LiteralIndex n_index = GetAssociatedLiteral(canonicalization.second);
216  if (n_index != kNoLiteralIndex) return Literal(n_index).Negated();
217 
218  ++num_created_variables_;
219  const Literal literal(sat_solver_->NewBooleanVariable(), true);
221 
222  // TODO(user): on some problem this happens. We should probably make sure that
223  // we don't create extra fixed Boolean variable for no reason.
224  if (sat_solver_->Assignment().LiteralIsAssigned(literal)) {
225  VLOG(1) << "Created a fixed literal for no reason!";
226  }
227  return literal;
228 }
229 
230 namespace {
231 std::pair<PositiveOnlyIndex, IntegerValue> PositiveVarKey(IntegerVariable var,
232  IntegerValue value) {
233  return std::make_pair(GetPositiveOnlyIndex(var),
235 }
236 } // namespace
237 
239  IntegerVariable var, IntegerValue value) const {
240  const auto it =
241  equality_to_associated_literal_.find(PositiveVarKey(var, value));
242  if (it != equality_to_associated_literal_.end()) {
243  return it->second.Index();
244  }
245  return kNoLiteralIndex;
246 }
247 
249  IntegerVariable var, IntegerValue value) {
250  {
251  const auto it =
252  equality_to_associated_literal_.find(PositiveVarKey(var, value));
253  if (it != equality_to_associated_literal_.end()) {
254  return it->second;
255  }
256  }
257 
258  // Check for trivial true/false literal to avoid creating variable for no
259  // reasons.
260  const Domain& domain = (*domains_)[var];
261  if (!domain.Contains(value.value())) return GetFalseLiteral();
262  if (value == domain.Min() && value == domain.Max()) {
264  return GetTrueLiteral();
265  }
266 
267  ++num_created_variables_;
268  const Literal literal(sat_solver_->NewBooleanVariable(), true);
270 
271  // TODO(user): this happens on some problem. We should probably
272  // make sure that we don't create extra fixed Boolean variable for no reason.
273  // Note that here we could detect the case before creating the literal. The
274  // initial domain didn't contain it, but maybe the one of (>= value) or (<=
275  // value) is false?
276  if (sat_solver_->Assignment().LiteralIsAssigned(literal)) {
277  VLOG(1) << "Created a fixed literal for no reason!";
278  }
279  return literal;
280 }
281 
283  IntegerLiteral i_lit) {
284  const auto& domain = (*domains_)[i_lit.var];
285  const IntegerValue min(domain.Min());
286  const IntegerValue max(domain.Max());
287  if (i_lit.bound <= min) {
288  sat_solver_->AddUnitClause(literal);
289  } else if (i_lit.bound > max) {
290  sat_solver_->AddUnitClause(literal.Negated());
291  } else {
292  const auto pair = Canonicalize(i_lit);
293  HalfAssociateGivenLiteral(pair.first, literal);
294  HalfAssociateGivenLiteral(pair.second, literal.Negated());
295 
296  // Detect the case >= max or <= min and properly register them. Note that
297  // both cases will happen at the same time if there is just two possible
298  // value in the domain.
299  if (pair.first.bound == max) {
301  }
302  if (-pair.second.bound == min) {
303  AssociateToIntegerEqualValue(literal.Negated(), i_lit.var, min);
304  }
305  }
306 }
307 
309  IntegerVariable var,
310  IntegerValue value) {
311  // Detect literal view. Note that the same literal can be associated to more
312  // than one variable, and thus already have a view. We don't change it in
313  // this case.
314  const Domain& domain = (*domains_)[var];
315  if (value == 1 && domain.Min() >= 0 && domain.Max() <= 1) {
316  if (literal.Index() >= literal_view_.size()) {
317  literal_view_.resize(literal.Index().value() + 1, kNoIntegerVariable);
318  literal_view_[literal.Index()] = var;
319  } else if (literal_view_[literal.Index()] == kNoIntegerVariable) {
320  literal_view_[literal.Index()] = var;
321  }
322  }
323  if (value == -1 && domain.Min() >= -1 && domain.Max() <= 0) {
324  if (literal.Index() >= literal_view_.size()) {
325  literal_view_.resize(literal.Index().value() + 1, kNoIntegerVariable);
326  literal_view_[literal.Index()] = NegationOf(var);
327  } else if (literal_view_[literal.Index()] == kNoIntegerVariable) {
328  literal_view_[literal.Index()] = NegationOf(var);
329  }
330  }
331 
332  // We use the "do not insert if present" behavior of .insert() to do just one
333  // lookup.
334  const auto insert_result = equality_to_associated_literal_.insert(
335  {PositiveVarKey(var, value), literal});
336  if (!insert_result.second) {
337  // If this key is already associated, make the two literals equal.
338  const Literal representative = insert_result.first->second;
339  if (representative != literal) {
340  DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
341  sat_solver_->AddClauseDuringSearch({literal, representative.Negated()});
342  sat_solver_->AddClauseDuringSearch({literal.Negated(), representative});
343  }
344  return;
345  }
346 
347  // Fix literal for value outside the domain.
348  if (!domain.Contains(value.value())) {
349  sat_solver_->AddUnitClause(literal.Negated());
350  return;
351  }
352 
353  // Update equality_by_var. Note that due to the
354  // equality_to_associated_literal_ hash table, there should never be any
355  // duplicate values for a given variable.
356  const PositiveOnlyIndex index = GetPositiveOnlyIndex(var);
357  if (index >= equality_by_var_.size()) {
358  equality_by_var_.resize(index.value() + 1);
359  is_fully_encoded_.resize(index.value() + 1);
360  }
361  equality_by_var_[index].push_back(
363 
364  // Fix literal for constant domain.
365  if (value == domain.Min() && value == domain.Max()) {
366  sat_solver_->AddUnitClause(literal);
367  return;
368  }
369 
372 
373  // Special case for the first and last value.
374  if (value == domain.Min()) {
375  // Note that this will recursively call AssociateToIntegerEqualValue() but
376  // since equality_to_associated_literal_[] is now set, the recursion will
377  // stop there. When a domain has just 2 values, this allows to call just
378  // once AssociateToIntegerEqualValue() and also associate the other value to
379  // the negation of the given literal.
381  return;
382  }
383  if (value == domain.Max()) {
385  return;
386  }
387 
388  // (var == value) <=> (var >= value) and (var <= value).
391  sat_solver_->AddClauseDuringSearch({a, literal.Negated()});
392  sat_solver_->AddClauseDuringSearch({b, literal.Negated()});
393  sat_solver_->AddClauseDuringSearch({a.Negated(), b.Negated(), literal});
394 
395  // Update reverse encoding.
396  const int new_size = 1 + literal.Index().value();
397  if (new_size > full_reverse_encoding_.size()) {
398  full_reverse_encoding_.resize(new_size);
399  }
400  full_reverse_encoding_[literal.Index()].push_back(le);
401  full_reverse_encoding_[literal.Index()].push_back(ge);
402 }
403 
404 // TODO(user): The hard constraints we add between associated literals seems to
405 // work for optional variables, but I am not 100% sure why!! I think it works
406 // because these literals can only appear in a conflict if the presence literal
407 // of the optional variables is true.
408 void IntegerEncoder::HalfAssociateGivenLiteral(IntegerLiteral i_lit,
409  Literal literal) {
410  // Resize reverse encoding.
411  const int new_size = 1 + literal.Index().value();
412  if (new_size > reverse_encoding_.size()) {
413  reverse_encoding_.resize(new_size);
414  }
415  if (new_size > full_reverse_encoding_.size()) {
416  full_reverse_encoding_.resize(new_size);
417  }
418 
419  // Associate the new literal to i_lit.
420  if (i_lit.var >= encoding_by_var_.size()) {
421  encoding_by_var_.resize(i_lit.var.value() + 1);
422  }
423  auto& var_encoding = encoding_by_var_[i_lit.var];
424  auto insert_result = var_encoding.insert({i_lit.bound, literal});
425  if (insert_result.second) { // New item.
426  AddImplications(var_encoding, insert_result.first, literal);
427  if (sat_solver_->Assignment().LiteralIsTrue(literal)) {
428  if (sat_solver_->CurrentDecisionLevel() == 0) {
429  newly_fixed_integer_literals_.push_back(i_lit);
430  }
431  }
432 
433  // TODO(user): do that for the other branch too?
434  reverse_encoding_[literal.Index()].push_back(i_lit);
435  full_reverse_encoding_[literal.Index()].push_back(i_lit);
436  } else {
437  const Literal associated(insert_result.first->second);
438  if (associated != literal) {
439  DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
440  sat_solver_->AddClauseDuringSearch({literal, associated.Negated()});
441  sat_solver_->AddClauseDuringSearch({literal.Negated(), associated});
442  }
443  }
444 }
445 
447  if (i.var >= encoding_by_var_.size()) return false;
448  const std::map<IntegerValue, Literal>& encoding = encoding_by_var_[i.var];
449  return encoding.find(i.bound) != encoding.end();
450 }
451 
453  if (i.var >= encoding_by_var_.size()) return kNoLiteralIndex;
454  const std::map<IntegerValue, Literal>& encoding = encoding_by_var_[i.var];
455  const auto result = encoding.find(i.bound);
456  if (result == encoding.end()) return kNoLiteralIndex;
457  return result->second.Index();
458 }
459 
461  IntegerLiteral i, IntegerValue* bound) const {
462  // We take the element before the upper_bound() which is either the encoding
463  // of i if it already exists, or the encoding just before it.
464  if (i.var >= encoding_by_var_.size()) return kNoLiteralIndex;
465  const std::map<IntegerValue, Literal>& encoding = encoding_by_var_[i.var];
466  auto after_it = encoding.upper_bound(i.bound);
467  if (after_it == encoding.begin()) return kNoLiteralIndex;
468  --after_it;
469  *bound = after_it->first;
470  return after_it->second.Index();
471 }
472 
474  if (parameters_.log_search_progress() && num_decisions_to_break_loop_ > 0) {
475  LOG(INFO) << "Num decisions to break propagation loop: "
476  << num_decisions_to_break_loop_;
477  }
478 }
479 
481  const int level = trail->CurrentDecisionLevel();
482  for (ReversibleInterface* rev : reversible_classes_) rev->SetLevel(level);
483 
484  // Make sure that our internal "integer_search_levels_" size matches the
485  // sat decision levels. At the level zero, integer_search_levels_ should
486  // be empty.
487  if (level > integer_search_levels_.size()) {
488  integer_search_levels_.push_back(integer_trail_.size());
489  reason_decision_levels_.push_back(literals_reason_starts_.size());
490  CHECK_EQ(trail->CurrentDecisionLevel(), integer_search_levels_.size());
491  }
492 
493  // This is used to map any integer literal out of the initial variable domain
494  // into one that use one of the domain value.
495  var_to_current_lb_interval_index_.SetLevel(level);
496 
497  // This is required because when loading a model it is possible that we add
498  // (literal <-> integer literal) associations for literals that have already
499  // been propagated here. This often happens when the presolve is off
500  // and many variables are fixed.
501  //
502  // TODO(user): refactor the interaction IntegerTrail <-> IntegerEncoder so
503  // that we can just push right away such literal. Unfortunately, this is is
504  // a big chunck of work.
505  if (level == 0) {
506  for (const IntegerLiteral i_lit : encoder_->NewlyFixedIntegerLiterals()) {
507  if (IsCurrentlyIgnored(i_lit.var)) continue;
508  if (!Enqueue(i_lit, {}, {})) return false;
509  }
510  encoder_->ClearNewlyFixedIntegerLiterals();
511 
512  for (const IntegerLiteral i_lit : integer_literal_to_fix_) {
513  if (IsCurrentlyIgnored(i_lit.var)) continue;
514  if (!Enqueue(i_lit, {}, {})) return false;
515  }
516  integer_literal_to_fix_.clear();
517 
518  for (const Literal lit : literal_to_fix_) {
519  if (trail_->Assignment().LiteralIsFalse(lit)) return false;
520  if (trail_->Assignment().LiteralIsTrue(lit)) continue;
521  trail_->EnqueueWithUnitReason(lit);
522  }
523  literal_to_fix_.clear();
524  }
525 
526  // Process all the "associated" literals and Enqueue() the corresponding
527  // bounds.
528  while (propagation_trail_index_ < trail->Index()) {
529  const Literal literal = (*trail)[propagation_trail_index_++];
530  for (const IntegerLiteral i_lit : encoder_->GetIntegerLiterals(literal)) {
531  if (IsCurrentlyIgnored(i_lit.var)) continue;
532 
533  // The reason is simply the associated literal.
534  if (!EnqueueAssociatedIntegerLiteral(i_lit, literal)) {
535  return false;
536  }
537  }
538  }
539 
540  return true;
541 }
542 
543 void IntegerTrail::Untrail(const Trail& trail, int literal_trail_index) {
544  ++num_untrails_;
545  const int level = trail.CurrentDecisionLevel();
546  var_to_current_lb_interval_index_.SetLevel(level);
548  std::min(propagation_trail_index_, literal_trail_index);
549 
550  if (level < first_level_without_full_propagation_) {
551  first_level_without_full_propagation_ = -1;
552  }
553 
554  // Note that if a conflict was detected before Propagate() of this class was
555  // even called, it is possible that there is nothing to backtrack.
556  if (level >= integer_search_levels_.size()) return;
557  const int target = integer_search_levels_[level];
558  integer_search_levels_.resize(level);
559  CHECK_GE(target, vars_.size());
560  CHECK_LE(target, integer_trail_.size());
561 
562  for (int index = integer_trail_.size() - 1; index >= target; --index) {
563  const TrailEntry& entry = integer_trail_[index];
564  if (entry.var < 0) continue; // entry used by EnqueueLiteral().
565  vars_[entry.var].current_trail_index = entry.prev_trail_index;
566  vars_[entry.var].current_bound =
567  integer_trail_[entry.prev_trail_index].bound;
568  }
569  integer_trail_.resize(target);
570 
571  // Clear reason.
572  const int old_size = reason_decision_levels_[level];
573  reason_decision_levels_.resize(level);
574  if (old_size < literals_reason_starts_.size()) {
575  literals_reason_buffer_.resize(literals_reason_starts_[old_size]);
576 
577  const int bound_start = bounds_reason_starts_[old_size];
578  bounds_reason_buffer_.resize(bound_start);
579  if (bound_start < trail_index_reason_buffer_.size()) {
580  trail_index_reason_buffer_.resize(bound_start);
581  }
582 
583  literals_reason_starts_.resize(old_size);
584  bounds_reason_starts_.resize(old_size);
585  }
586 
587  // We notify the new level once all variables have been restored to their
588  // old value.
589  for (ReversibleInterface* rev : reversible_classes_) rev->SetLevel(level);
590 }
591 
593  // Because we always create both a variable and its negation.
594  const int size = 2 * num_vars;
595  vars_.reserve(size);
596  is_ignored_literals_.reserve(size);
597  integer_trail_.reserve(size);
598  domains_->reserve(size);
599  var_trail_index_cache_.reserve(size);
600  tmp_var_to_trail_index_in_queue_.reserve(size);
601 }
602 
603 IntegerVariable IntegerTrail::AddIntegerVariable(IntegerValue lower_bound,
604  IntegerValue upper_bound) {
605  DCHECK_GE(lower_bound, kMinIntegerValue);
606  DCHECK_LE(lower_bound, upper_bound);
607  DCHECK_LE(upper_bound, kMaxIntegerValue);
608  DCHECK(lower_bound >= 0 || lower_bound + kint64max >= upper_bound);
609  DCHECK(integer_search_levels_.empty());
610  DCHECK_EQ(vars_.size(), integer_trail_.size());
611 
612  const IntegerVariable i(vars_.size());
613  is_ignored_literals_.push_back(kNoLiteralIndex);
614  vars_.push_back({lower_bound, static_cast<int>(integer_trail_.size())});
615  integer_trail_.push_back({lower_bound, i});
616  domains_->push_back(Domain(lower_bound.value(), upper_bound.value()));
617 
618  // TODO(user): the is_ignored_literals_ Booleans are currently always the same
619  // for a variable and its negation. So it may be better not to store it twice
620  // so that we don't have to be careful when setting them.
621  CHECK_EQ(NegationOf(i).value(), vars_.size());
622  is_ignored_literals_.push_back(kNoLiteralIndex);
623  vars_.push_back({-upper_bound, static_cast<int>(integer_trail_.size())});
624  integer_trail_.push_back({-upper_bound, NegationOf(i)});
625  domains_->push_back(Domain(-upper_bound.value(), -lower_bound.value()));
626 
627  var_trail_index_cache_.resize(vars_.size(), integer_trail_.size());
628  tmp_var_to_trail_index_in_queue_.resize(vars_.size(), 0);
629 
630  for (SparseBitset<IntegerVariable>* w : watchers_) {
631  w->Resize(NumIntegerVariables());
632  }
633  return i;
634 }
635 
636 IntegerVariable IntegerTrail::AddIntegerVariable(const Domain& domain) {
637  CHECK(!domain.IsEmpty());
638  const IntegerVariable var = AddIntegerVariable(IntegerValue(domain.Min()),
639  IntegerValue(domain.Max()));
640  CHECK(UpdateInitialDomain(var, domain));
641  return var;
642 }
643 
644 const Domain& IntegerTrail::InitialVariableDomain(IntegerVariable var) const {
645  return (*domains_)[var];
646 }
647 
648 bool IntegerTrail::UpdateInitialDomain(IntegerVariable var, Domain domain) {
649  CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
650 
651  const Domain& old_domain = InitialVariableDomain(var);
652  domain = domain.IntersectionWith(old_domain);
653  if (old_domain == domain) return true;
654 
655  if (domain.IsEmpty()) return false;
656  (*domains_)[var] = domain;
657  (*domains_)[NegationOf(var)] = domain.Negation();
658  if (domain.NumIntervals() > 1) {
659  var_to_current_lb_interval_index_.Set(var, 0);
660  var_to_current_lb_interval_index_.Set(NegationOf(var), 0);
661  }
662 
663  // TODO(user): That works, but it might be better to simply update the
664  // bounds here directly. This is because these function might call again
665  // UpdateInitialDomain(), and we will abort after realizing that the domain
666  // didn't change this time.
667  CHECK(Enqueue(IntegerLiteral::GreaterOrEqual(var, IntegerValue(domain.Min())),
668  {}, {}));
669  CHECK(Enqueue(IntegerLiteral::LowerOrEqual(var, IntegerValue(domain.Max())),
670  {}, {}));
671 
672  // Set to false excluded literals.
673  int i = 0;
674  int num_fixed = 0;
675  for (const IntegerEncoder::ValueLiteralPair pair :
676  encoder_->PartialDomainEncoding(var)) {
677  while (i < domain.NumIntervals() && pair.value > domain[i].end) ++i;
678  if (i == domain.NumIntervals() || pair.value < domain[i].start) {
679  ++num_fixed;
680  if (trail_->Assignment().LiteralIsTrue(pair.literal)) return false;
681  if (!trail_->Assignment().LiteralIsFalse(pair.literal)) {
682  trail_->EnqueueWithUnitReason(pair.literal.Negated());
683  }
684  }
685  }
686  if (num_fixed > 0) {
687  VLOG(1)
688  << "Domain intersection fixed " << num_fixed
689  << " equality literal corresponding to values outside the new domain.";
690  }
691 
692  return true;
693 }
694 
696  IntegerValue value) {
697  auto insert = constant_map_.insert(std::make_pair(value, kNoIntegerVariable));
698  if (insert.second) { // new element.
699  const IntegerVariable new_var = AddIntegerVariable(value, value);
700  insert.first->second = new_var;
701  if (value != 0) {
702  // Note that this might invalidate insert.first->second.
703  gtl::InsertOrDie(&constant_map_, -value, NegationOf(new_var));
704  }
705  return new_var;
706  }
707  return insert.first->second;
708 }
709 
711  // The +1 if for the special key zero (the only case when we have an odd
712  // number of entries).
713  return (constant_map_.size() + 1) / 2;
714 }
715 
717  int threshold) const {
718  // Optimization. We assume this is only called when computing a reason, so we
719  // can ignore this trail_index if we already need a more restrictive reason
720  // for this var.
721  const int index_in_queue = tmp_var_to_trail_index_in_queue_[var];
722  if (threshold <= index_in_queue) {
723  if (index_in_queue != kint32max) has_dependency_ = true;
724  return -1;
725  }
726 
727  DCHECK_GE(threshold, vars_.size());
728  int trail_index = vars_[var].current_trail_index;
729 
730  // Check the validity of the cached index and use it if possible.
731  if (trail_index > threshold) {
732  const int cached_index = var_trail_index_cache_[var];
733  if (cached_index >= threshold && cached_index < trail_index &&
734  integer_trail_[cached_index].var == var) {
735  trail_index = cached_index;
736  }
737  }
738 
739  while (trail_index >= threshold) {
740  trail_index = integer_trail_[trail_index].prev_trail_index;
741  if (trail_index >= var_trail_index_cache_threshold_) {
742  var_trail_index_cache_[var] = trail_index;
743  }
744  }
745 
746  const int num_vars = vars_.size();
747  return trail_index < num_vars ? -1 : trail_index;
748 }
749 
750 int IntegerTrail::FindLowestTrailIndexThatExplainBound(
751  IntegerLiteral i_lit) const {
752  DCHECK_LE(i_lit.bound, vars_[i_lit.var].current_bound);
753  if (i_lit.bound <= LevelZeroLowerBound(i_lit.var)) return -1;
754  int trail_index = vars_[i_lit.var].current_trail_index;
755 
756  // Check the validity of the cached index and use it if possible. This caching
757  // mechanism is important in case of long chain of propagation on the same
758  // variable. Because during conflict resolution, we call
759  // FindLowestTrailIndexThatExplainBound() with lowest and lowest bound, this
760  // cache can transform a quadratic complexity into a linear one.
761  {
762  const int cached_index = var_trail_index_cache_[i_lit.var];
763  if (cached_index < trail_index) {
764  const TrailEntry& entry = integer_trail_[cached_index];
765  if (entry.var == i_lit.var && entry.bound >= i_lit.bound) {
766  trail_index = cached_index;
767  }
768  }
769  }
770 
771  int prev_trail_index = trail_index;
772  while (true) {
773  if (trail_index >= var_trail_index_cache_threshold_) {
774  var_trail_index_cache_[i_lit.var] = trail_index;
775  }
776  const TrailEntry& entry = integer_trail_[trail_index];
777  if (entry.bound == i_lit.bound) return trail_index;
778  if (entry.bound < i_lit.bound) return prev_trail_index;
779  prev_trail_index = trail_index;
780  trail_index = entry.prev_trail_index;
781  }
782 }
783 
784 // TODO(user): Get rid of this function and only keep the trail index one?
786  IntegerValue slack, absl::Span<const IntegerValue> coeffs,
787  std::vector<IntegerLiteral>* reason) const {
788  CHECK_GE(slack, 0);
789  if (slack == 0) return;
790  const int size = reason->size();
791  tmp_indices_.resize(size);
792  for (int i = 0; i < size; ++i) {
793  CHECK_EQ((*reason)[i].bound, LowerBound((*reason)[i].var));
794  CHECK_GE(coeffs[i], 0);
795  tmp_indices_[i] = vars_[(*reason)[i].var].current_trail_index;
796  }
797 
798  RelaxLinearReason(slack, coeffs, &tmp_indices_);
799 
800  reason->clear();
801  for (const int i : tmp_indices_) {
802  reason->push_back(IntegerLiteral::GreaterOrEqual(integer_trail_[i].var,
803  integer_trail_[i].bound));
804  }
805 }
806 
808  IntegerValue slack, absl::Span<const IntegerValue> coeffs,
809  absl::Span<const IntegerVariable> vars,
810  std::vector<IntegerLiteral>* reason) const {
811  tmp_indices_.clear();
812  for (const IntegerVariable var : vars) {
813  tmp_indices_.push_back(vars_[var].current_trail_index);
814  }
815  if (slack > 0) RelaxLinearReason(slack, coeffs, &tmp_indices_);
816  for (const int i : tmp_indices_) {
817  reason->push_back(IntegerLiteral::GreaterOrEqual(integer_trail_[i].var,
818  integer_trail_[i].bound));
819  }
820 }
821 
822 void IntegerTrail::RelaxLinearReason(IntegerValue slack,
823  absl::Span<const IntegerValue> coeffs,
824  std::vector<int>* trail_indices) const {
825  DCHECK_GT(slack, 0);
826  DCHECK(relax_heap_.empty());
827 
828  // We start by filtering *trail_indices:
829  // - remove all level zero entries.
830  // - keep the one that cannot be relaxed.
831  // - move the other one to the relax_heap_ (and creating the heap).
832  int new_size = 0;
833  const int size = coeffs.size();
834  const int num_vars = vars_.size();
835  for (int i = 0; i < size; ++i) {
836  const int index = (*trail_indices)[i];
837 
838  // We ignore level zero entries.
839  if (index < num_vars) continue;
840 
841  // If the coeff is too large, we cannot relax this entry.
842  const IntegerValue coeff = coeffs[i];
843  if (coeff > slack) {
844  (*trail_indices)[new_size++] = index;
845  continue;
846  }
847 
848  // This is a bit hacky, but when it is used from MergeReasonIntoInternal(),
849  // we never relax a reason that will not be expanded because it is already
850  // part of the current conflict.
851  const TrailEntry& entry = integer_trail_[index];
852  if (entry.var != kNoIntegerVariable &&
853  index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
854  (*trail_indices)[new_size++] = index;
855  continue;
856  }
857 
858  // Note that both terms of the product are positive.
859  const TrailEntry& previous_entry = integer_trail_[entry.prev_trail_index];
860  const int64 diff =
861  CapProd(coeff.value(), (entry.bound - previous_entry.bound).value());
862  if (diff > slack) {
863  (*trail_indices)[new_size++] = index;
864  continue;
865  }
866 
867  relax_heap_.push_back({index, coeff, diff});
868  }
869  trail_indices->resize(new_size);
870  std::make_heap(relax_heap_.begin(), relax_heap_.end());
871 
872  while (slack > 0 && !relax_heap_.empty()) {
873  const RelaxHeapEntry heap_entry = relax_heap_.front();
874  std::pop_heap(relax_heap_.begin(), relax_heap_.end());
875  relax_heap_.pop_back();
876 
877  // The slack might have changed since the entry was added.
878  if (heap_entry.diff > slack) {
879  trail_indices->push_back(heap_entry.index);
880  continue;
881  }
882 
883  // Relax, and decide what to do with the new value of index.
884  slack -= heap_entry.diff;
885  const int index = integer_trail_[heap_entry.index].prev_trail_index;
886 
887  // Same code as in the first block.
888  if (index < num_vars) continue;
889  if (heap_entry.coeff > slack) {
890  trail_indices->push_back(index);
891  continue;
892  }
893  const TrailEntry& entry = integer_trail_[index];
894  if (entry.var != kNoIntegerVariable &&
895  index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
896  trail_indices->push_back(index);
897  continue;
898  }
899 
900  const TrailEntry& previous_entry = integer_trail_[entry.prev_trail_index];
901  const int64 diff = CapProd(heap_entry.coeff.value(),
902  (entry.bound - previous_entry.bound).value());
903  if (diff > slack) {
904  trail_indices->push_back(index);
905  continue;
906  }
907  relax_heap_.push_back({index, heap_entry.coeff, diff});
908  std::push_heap(relax_heap_.begin(), relax_heap_.end());
909  }
910 
911  // If we aborted early because of the slack, we need to push all remaining
912  // indices back into the reason.
913  for (const RelaxHeapEntry& entry : relax_heap_) {
914  trail_indices->push_back(entry.index);
915  }
916  relax_heap_.clear();
917 }
918 
920  std::vector<IntegerLiteral>* reason) const {
921  int new_size = 0;
922  for (const IntegerLiteral literal : *reason) {
923  if (literal.bound <= LevelZeroLowerBound(literal.var)) continue;
924  (*reason)[new_size++] = literal;
925  }
926  reason->resize(new_size);
927 }
928 
929 std::vector<Literal>* IntegerTrail::InitializeConflict(
930  IntegerLiteral integer_literal, const LazyReasonFunction& lazy_reason,
931  absl::Span<const Literal> literals_reason,
932  absl::Span<const IntegerLiteral> bounds_reason) {
933  DCHECK(tmp_queue_.empty());
934  std::vector<Literal>* conflict = trail_->MutableConflict();
935  if (lazy_reason == nullptr) {
936  conflict->assign(literals_reason.begin(), literals_reason.end());
937  const int num_vars = vars_.size();
938  for (const IntegerLiteral& literal : bounds_reason) {
939  const int trail_index = FindLowestTrailIndexThatExplainBound(literal);
940  if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
941  }
942  } else {
943  // We use the current trail index here.
944  conflict->clear();
945  lazy_reason(integer_literal, integer_trail_.size(), conflict, &tmp_queue_);
946  }
947  return conflict;
948 }
949 
950 namespace {
951 
952 std::string ReasonDebugString(absl::Span<const Literal> literal_reason,
953  absl::Span<const IntegerLiteral> integer_reason) {
954  std::string result = "literals:{";
955  for (const Literal l : literal_reason) {
956  if (result.back() != '{') result += ",";
957  result += l.DebugString();
958  }
959  result += "} bounds:{";
960  for (const IntegerLiteral l : integer_reason) {
961  if (result.back() != '{') result += ",";
962  result += l.DebugString();
963  }
964  result += "}";
965  return result;
966 }
967 
968 } // namespace
969 
970 std::string IntegerTrail::DebugString() {
971  std::string result = "trail:{";
972  const int num_vars = vars_.size();
973  const int limit =
974  std::min(num_vars + 30, static_cast<int>(integer_trail_.size()));
975  for (int i = num_vars; i < limit; ++i) {
976  if (result.back() != '{') result += ",";
977  result +=
978  IntegerLiteral::GreaterOrEqual(IntegerVariable(integer_trail_[i].var),
979  integer_trail_[i].bound)
980  .DebugString();
981  }
982  if (limit < integer_trail_.size()) {
983  result += ", ...";
984  }
985  result += "}";
986  return result;
987 }
988 
990  absl::Span<const Literal> literal_reason,
991  absl::Span<const IntegerLiteral> integer_reason) {
992  return EnqueueInternal(i_lit, nullptr, literal_reason, integer_reason,
993  integer_trail_.size());
994 }
995 
997  Literal lit, IntegerLiteral i_lit, std::vector<Literal>* literal_reason,
998  std::vector<IntegerLiteral>* integer_reason) {
999  const VariablesAssignment& assignment = trail_->Assignment();
1000  if (assignment.LiteralIsFalse(lit)) return true;
1001 
1002  // We can always push var if the optional literal is the same.
1003  //
1004  // TODO(user): we can also push lit.var if its presence implies lit.
1005  if (lit.Index() == OptionalLiteralIndex(i_lit.var)) {
1006  return Enqueue(i_lit, *literal_reason, *integer_reason);
1007  }
1008 
1009  if (assignment.LiteralIsTrue(lit)) {
1010  literal_reason->push_back(lit.Negated());
1011  return Enqueue(i_lit, *literal_reason, *integer_reason);
1012  }
1013 
1014  if (IntegerLiteralIsFalse(i_lit)) {
1015  integer_reason->push_back(
1016  IntegerLiteral::LowerOrEqual(i_lit.var, i_lit.bound - 1));
1017  EnqueueLiteral(lit.Negated(), *literal_reason, *integer_reason);
1018  return true;
1019  }
1020 
1021  // We can't push anything in this case.
1022  return true;
1023 }
1024 
1026  absl::Span<const Literal> literal_reason,
1027  absl::Span<const IntegerLiteral> integer_reason,
1028  int trail_index_with_same_reason) {
1029  return EnqueueInternal(i_lit, nullptr, literal_reason, integer_reason,
1030  trail_index_with_same_reason);
1031 }
1032 
1034  LazyReasonFunction lazy_reason) {
1035  return EnqueueInternal(i_lit, lazy_reason, {}, {}, integer_trail_.size());
1036 }
1037 
1038 bool IntegerTrail::ReasonIsValid(
1039  absl::Span<const Literal> literal_reason,
1040  absl::Span<const IntegerLiteral> integer_reason) {
1041  const VariablesAssignment& assignment = trail_->Assignment();
1042  for (const Literal lit : literal_reason) {
1043  if (!assignment.LiteralIsFalse(lit)) return false;
1044  }
1045  for (const IntegerLiteral i_lit : integer_reason) {
1046  if (i_lit.bound > vars_[i_lit.var].current_bound) {
1047  if (IsOptional(i_lit.var)) {
1048  const Literal is_ignored = IsIgnoredLiteral(i_lit.var);
1049  LOG(INFO) << "Reason " << i_lit << " is not true!"
1050  << " optional variable:" << i_lit.var
1051  << " present:" << assignment.LiteralIsFalse(is_ignored)
1052  << " absent:" << assignment.LiteralIsTrue(is_ignored)
1053  << " current_lb:" << vars_[i_lit.var].current_bound;
1054  } else {
1055  LOG(INFO) << "Reason " << i_lit << " is not true!"
1056  << " non-optional variable:" << i_lit.var
1057  << " current_lb:" << vars_[i_lit.var].current_bound;
1058  }
1059  return false;
1060  }
1061  }
1062 
1063  // This may not indicate an incorectness, but just some propagators that
1064  // didn't reach a fixed-point at level zero.
1065  if (!integer_search_levels_.empty()) {
1066  int num_literal_assigned_after_root_node = 0;
1067  for (const Literal lit : literal_reason) {
1068  if (trail_->Info(lit.Variable()).level > 0) {
1069  num_literal_assigned_after_root_node++;
1070  }
1071  }
1072  for (const IntegerLiteral i_lit : integer_reason) {
1073  if (LevelZeroLowerBound(i_lit.var) < i_lit.bound) {
1074  num_literal_assigned_after_root_node++;
1075  }
1076  }
1077  DLOG_IF(INFO, num_literal_assigned_after_root_node == 0)
1078  << "Propagating a literal with no reason at a positive level!\n"
1079  << "level:" << integer_search_levels_.size() << " "
1080  << ReasonDebugString(literal_reason, integer_reason) << "\n"
1081  << DebugString();
1082  }
1083 
1084  return true;
1085 }
1086 
1088  Literal literal, absl::Span<const Literal> literal_reason,
1089  absl::Span<const IntegerLiteral> integer_reason) {
1090  EnqueueLiteralInternal(literal, nullptr, literal_reason, integer_reason);
1091 }
1092 
1093 void IntegerTrail::EnqueueLiteralInternal(
1094  Literal literal, LazyReasonFunction lazy_reason,
1095  absl::Span<const Literal> literal_reason,
1096  absl::Span<const IntegerLiteral> integer_reason) {
1098  DCHECK(lazy_reason != nullptr ||
1099  ReasonIsValid(literal_reason, integer_reason));
1100  if (integer_search_levels_.empty()) {
1101  // Level zero. We don't keep any reason.
1102  trail_->EnqueueWithUnitReason(literal);
1103  return;
1104  }
1105 
1106  // If we are fixing something at a positive level, remember it.
1107  if (!integer_search_levels_.empty() && integer_reason.empty() &&
1108  literal_reason.empty() && lazy_reason == nullptr) {
1109  literal_to_fix_.push_back(literal);
1110  }
1111 
1112  const int trail_index = trail_->Index();
1113  if (trail_index >= boolean_trail_index_to_integer_one_.size()) {
1114  boolean_trail_index_to_integer_one_.resize(trail_index + 1);
1115  }
1116  boolean_trail_index_to_integer_one_[trail_index] = integer_trail_.size();
1117 
1118  int reason_index = literals_reason_starts_.size();
1119  if (lazy_reason != nullptr) {
1120  if (integer_trail_.size() >= lazy_reasons_.size()) {
1121  lazy_reasons_.resize(integer_trail_.size() + 1, nullptr);
1122  }
1123  lazy_reasons_[integer_trail_.size()] = lazy_reason;
1124  reason_index = -1;
1125  } else {
1126  // Copy the reason.
1127  literals_reason_starts_.push_back(literals_reason_buffer_.size());
1128  literals_reason_buffer_.insert(literals_reason_buffer_.end(),
1129  literal_reason.begin(),
1130  literal_reason.end());
1131  bounds_reason_starts_.push_back(bounds_reason_buffer_.size());
1132  bounds_reason_buffer_.insert(bounds_reason_buffer_.end(),
1133  integer_reason.begin(), integer_reason.end());
1134  }
1135 
1136  integer_trail_.push_back({/*bound=*/IntegerValue(0),
1137  /*var=*/kNoIntegerVariable,
1138  /*prev_trail_index=*/-1,
1139  /*reason_index=*/reason_index});
1140 
1141  trail_->Enqueue(literal, propagator_id_);
1142 }
1143 
1144 // We count the number of propagation at the current level, and returns true
1145 // if it seems really large. Note that we disable this if we are in fixed
1146 // search.
1148  const int num_vars = vars_.size();
1149  return (!integer_search_levels_.empty() &&
1150  integer_trail_.size() - integer_search_levels_.back() >
1151  std::max(10000, num_vars) &&
1152  parameters_.search_branching() != SatParameters::FIXED_SEARCH);
1153 }
1154 
1155 // We try to select a variable with a large domain that was propagated a lot
1156 // already.
1159  ++num_decisions_to_break_loop_;
1160  std::vector<IntegerVariable> vars;
1161  for (int i = integer_search_levels_.back(); i < integer_trail_.size(); ++i) {
1162  const IntegerVariable var = integer_trail_[i].var;
1163  if (var == kNoIntegerVariable) continue;
1164  if (UpperBound(var) - LowerBound(var) <= 100) continue;
1165  vars.push_back(var);
1166  }
1167  if (vars.empty()) return kNoIntegerVariable;
1168  std::sort(vars.begin(), vars.end());
1169  IntegerVariable best_var = vars[0];
1170  int best_count = 1;
1171  int count = 1;
1172  for (int i = 1; i < vars.size(); ++i) {
1173  if (vars[i] != vars[i - 1]) {
1174  count = 1;
1175  } else {
1176  ++count;
1177  if (count > best_count) {
1178  best_count = count;
1179  best_var = vars[i];
1180  }
1181  }
1182  }
1183  return best_var;
1184 }
1185 
1187  return first_level_without_full_propagation_ != -1;
1188 }
1189 
1190 IntegerVariable IntegerTrail::FirstUnassignedVariable() const {
1191  for (IntegerVariable var(0); var < vars_.size(); var += 2) {
1192  if (IsCurrentlyIgnored(var)) continue;
1193  if (!IsFixed(var)) return var;
1194  }
1195  return kNoIntegerVariable;
1196 }
1197 
1198 bool IntegerTrail::EnqueueInternal(
1199  IntegerLiteral i_lit, LazyReasonFunction lazy_reason,
1200  absl::Span<const Literal> literal_reason,
1201  absl::Span<const IntegerLiteral> integer_reason,
1202  int trail_index_with_same_reason) {
1203  DCHECK(lazy_reason != nullptr ||
1204  ReasonIsValid(literal_reason, integer_reason));
1205 
1206  const IntegerVariable var(i_lit.var);
1207 
1208  // No point doing work if the variable is already ignored.
1209  if (IsCurrentlyIgnored(var)) return true;
1210 
1211  // Nothing to do if the bound is not better than the current one.
1212  // TODO(user): Change this to a CHECK? propagator shouldn't try to push such
1213  // bound and waste time explaining it.
1214  if (i_lit.bound <= vars_[var].current_bound) return true;
1215  ++num_enqueues_;
1216 
1217  // If the domain of var is not a single intervals and i_lit.bound fall into a
1218  // "hole", we increase it to the next possible value. This ensure that we
1219  // never Enqueue() non-canonical literals. See also Canonicalize().
1220  //
1221  // Note: The literals in the reason are not necessarily canonical, but then
1222  // we always map these to enqueued literals during conflict resolution.
1223  if ((*domains_)[var].NumIntervals() > 1) {
1224  const auto& domain = (*domains_)[var];
1225  int index = var_to_current_lb_interval_index_.FindOrDie(var);
1226  const int size = domain.NumIntervals();
1227  while (index < size && i_lit.bound > domain[index].end) {
1228  ++index;
1229  }
1230  if (index == size) {
1231  return ReportConflict(literal_reason, integer_reason);
1232  } else {
1233  var_to_current_lb_interval_index_.Set(var, index);
1234  i_lit.bound = std::max(i_lit.bound, IntegerValue(domain[index].start));
1235  }
1236  }
1237 
1238  // Check if the integer variable has an empty domain.
1239  if (i_lit.bound > UpperBound(var)) {
1240  // We relax the upper bound as much as possible to still have a conflict.
1241  const auto ub_reason = IntegerLiteral::LowerOrEqual(var, i_lit.bound - 1);
1242 
1243  if (!IsOptional(var) || trail_->Assignment().LiteralIsFalse(
1244  Literal(is_ignored_literals_[var]))) {
1245  // Note that we want only one call to MergeReasonIntoInternal() for
1246  // efficiency and a potential smaller reason.
1247  auto* conflict = InitializeConflict(i_lit, lazy_reason, literal_reason,
1248  integer_reason);
1249  if (IsOptional(var)) {
1250  conflict->push_back(Literal(is_ignored_literals_[var]));
1251  }
1252  {
1253  const int trail_index = FindLowestTrailIndexThatExplainBound(ub_reason);
1254  const int num_vars = vars_.size(); // must be signed.
1255  if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
1256  }
1257  MergeReasonIntoInternal(conflict);
1258  return false;
1259  } else {
1260  // Note(user): We never make the bound of an optional literal cross. We
1261  // used to have a bug where we propagated these bounds and their
1262  // associated literals, and we were reaching a conflict while propagating
1263  // the associated literal instead of setting is_ignored below to false.
1264  const Literal is_ignored = Literal(is_ignored_literals_[var]);
1265  if (integer_search_levels_.empty()) {
1266  trail_->EnqueueWithUnitReason(is_ignored);
1267  } else {
1268  // Here we currently expand any lazy reason because we need to add
1269  // to it the reason for the upper bound.
1270  // TODO(user): A possible solution would be to support the two types
1271  // of reason (lazy and not) at the same time and use the union of both?
1272  if (lazy_reason != nullptr) {
1273  lazy_reason(i_lit, integer_trail_.size(), &lazy_reason_literals_,
1274  &lazy_reason_trail_indices_);
1275  std::vector<IntegerLiteral> temp;
1276  for (const int trail_index : lazy_reason_trail_indices_) {
1277  const TrailEntry& entry = integer_trail_[trail_index];
1278  temp.push_back(IntegerLiteral(entry.var, entry.bound));
1279  }
1280  EnqueueLiteral(is_ignored, lazy_reason_literals_, temp);
1281  } else {
1282  EnqueueLiteral(is_ignored, literal_reason, integer_reason);
1283  }
1284 
1285  // Hack, we add the upper bound reason here.
1286  bounds_reason_buffer_.push_back(ub_reason);
1287  }
1288  return true;
1289  }
1290  }
1291 
1292  // Stop propagating if we detect a propagation loop. The search heuristic will
1293  // then take an appropriate next decision. Note that we do that after checking
1294  // for a potential conflict if the two bounds of a variable cross. This is
1295  // important, so that in the corner case where all variables are actually
1296  // fixed, we still make sure no propagator detect a conflict.
1297  //
1298  // TODO(user): Some propagation code have CHECKS in place and not like when
1299  // something they just pushed is not reflected right away. They must be aware
1300  // of that, which is a bit tricky.
1301  if (InPropagationLoop()) {
1302  // Note that we still propagate "big" push as it seems better to do that
1303  // now rather than to delay to the next decision.
1304  const IntegerValue lb = LowerBound(i_lit.var);
1305  const IntegerValue ub = UpperBound(i_lit.var);
1306  if (i_lit.bound - lb < (ub - lb) / 2) {
1307  if (first_level_without_full_propagation_ == -1) {
1308  first_level_without_full_propagation_ = trail_->CurrentDecisionLevel();
1309  }
1310  return true;
1311  }
1312  }
1313 
1314  // Notify the watchers.
1315  for (SparseBitset<IntegerVariable>* bitset : watchers_) {
1316  bitset->Set(i_lit.var);
1317  }
1318 
1319  if (!integer_search_levels_.empty() && integer_reason.empty() &&
1320  literal_reason.empty() && lazy_reason == nullptr &&
1321  trail_index_with_same_reason >= integer_trail_.size()) {
1322  integer_literal_to_fix_.push_back(i_lit);
1323  }
1324 
1325  // Enqueue the strongest associated Boolean literal implied by this one.
1326  // Because we linked all such literal with implications, all the one before
1327  // will be propagated by the SAT solver.
1328  //
1329  // Important: It is possible that such literal or even stronger ones are
1330  // already true! This is because we might push stuff while Propagate() haven't
1331  // been called yet. Maybe we should call it?
1332  //
1333  // TODO(user): It might be simply better and more efficient to simply enqueue
1334  // all of them here. We have also more liberty to choose the explanation we
1335  // want. A drawback might be that the implications might not be used in the
1336  // binary conflict minimization algo.
1337  IntegerValue bound;
1338  const LiteralIndex literal_index =
1339  encoder_->SearchForLiteralAtOrBefore(i_lit, &bound);
1340  if (literal_index != kNoLiteralIndex) {
1341  const Literal to_enqueue = Literal(literal_index);
1342  if (trail_->Assignment().LiteralIsFalse(to_enqueue)) {
1343  auto* conflict = InitializeConflict(i_lit, lazy_reason, literal_reason,
1344  integer_reason);
1345  conflict->push_back(to_enqueue);
1346  MergeReasonIntoInternal(conflict);
1347  return false;
1348  }
1349 
1350  // If the associated literal exactly correspond to i_lit, then we push
1351  // it first, and then we use it as a reason for i_lit. We do that so that
1352  // MergeReasonIntoInternal() will not unecessarily expand further the reason
1353  // for i_lit.
1354  if (IntegerLiteral::GreaterOrEqual(i_lit.var, bound) == i_lit) {
1355  if (!trail_->Assignment().LiteralIsTrue(to_enqueue)) {
1356  EnqueueLiteralInternal(to_enqueue, lazy_reason, literal_reason,
1357  integer_reason);
1358  }
1359  return EnqueueAssociatedIntegerLiteral(i_lit, to_enqueue);
1360  }
1361 
1362  if (!trail_->Assignment().LiteralIsTrue(to_enqueue)) {
1363  if (integer_search_levels_.empty()) {
1364  trail_->EnqueueWithUnitReason(to_enqueue);
1365  } else {
1366  // Subtle: the reason is the same as i_lit, that we will enqueue if no
1367  // conflict occur at position integer_trail_.size(), so we just refer to
1368  // this index here.
1369  const int trail_index = trail_->Index();
1370  if (trail_index >= boolean_trail_index_to_integer_one_.size()) {
1371  boolean_trail_index_to_integer_one_.resize(trail_index + 1);
1372  }
1373  boolean_trail_index_to_integer_one_[trail_index] =
1374  trail_index_with_same_reason;
1375  trail_->Enqueue(to_enqueue, propagator_id_);
1376  }
1377  }
1378  }
1379 
1380  // Special case for level zero.
1381  if (integer_search_levels_.empty()) {
1382  ++num_level_zero_enqueues_;
1383  vars_[i_lit.var].current_bound = i_lit.bound;
1384  integer_trail_[i_lit.var.value()].bound = i_lit.bound;
1385 
1386  // We also update the initial domain. If this fail, since we are at level
1387  // zero, we don't care about the reason.
1388  trail_->MutableConflict()->clear();
1389  return UpdateInitialDomain(
1390  i_lit.var,
1391  Domain(LowerBound(i_lit.var).value(), UpperBound(i_lit.var).value()));
1392  }
1393  DCHECK_GT(trail_->CurrentDecisionLevel(), 0);
1394 
1395  int reason_index = literals_reason_starts_.size();
1396  if (lazy_reason != nullptr) {
1397  if (integer_trail_.size() >= lazy_reasons_.size()) {
1398  lazy_reasons_.resize(integer_trail_.size() + 1, nullptr);
1399  }
1400  lazy_reasons_[integer_trail_.size()] = lazy_reason;
1401  reason_index = -1;
1402  } else if (trail_index_with_same_reason >= integer_trail_.size()) {
1403  // Save the reason into our internal buffers.
1404  literals_reason_starts_.push_back(literals_reason_buffer_.size());
1405  if (!literal_reason.empty()) {
1406  literals_reason_buffer_.insert(literals_reason_buffer_.end(),
1407  literal_reason.begin(),
1408  literal_reason.end());
1409  }
1410  bounds_reason_starts_.push_back(bounds_reason_buffer_.size());
1411  if (!integer_reason.empty()) {
1412  bounds_reason_buffer_.insert(bounds_reason_buffer_.end(),
1413  integer_reason.begin(),
1414  integer_reason.end());
1415  }
1416  } else {
1417  reason_index = integer_trail_[trail_index_with_same_reason].reason_index;
1418  }
1419 
1420  const int prev_trail_index = vars_[i_lit.var].current_trail_index;
1421  integer_trail_.push_back({/*bound=*/i_lit.bound,
1422  /*var=*/i_lit.var,
1423  /*prev_trail_index=*/prev_trail_index,
1424  /*reason_index=*/reason_index});
1425 
1426  vars_[i_lit.var].current_bound = i_lit.bound;
1427  vars_[i_lit.var].current_trail_index = integer_trail_.size() - 1;
1428  return true;
1429 }
1430 
1431 bool IntegerTrail::EnqueueAssociatedIntegerLiteral(IntegerLiteral i_lit,
1432  Literal literal_reason) {
1433  DCHECK(ReasonIsValid({literal_reason.Negated()}, {}));
1434  DCHECK(!IsCurrentlyIgnored(i_lit.var));
1435 
1436  // Nothing to do if the bound is not better than the current one.
1437  if (i_lit.bound <= vars_[i_lit.var].current_bound) return true;
1438  ++num_enqueues_;
1439 
1440  // Check if the integer variable has an empty domain. Note that this should
1441  // happen really rarely since in most situation, pushing the upper bound would
1442  // have resulted in this literal beeing false. Because of this we revert to
1443  // the "generic" Enqueue() to avoid some code duplication.
1444  if (i_lit.bound > UpperBound(i_lit.var)) {
1445  return Enqueue(i_lit, {literal_reason.Negated()}, {});
1446  }
1447 
1448  // Notify the watchers.
1449  for (SparseBitset<IntegerVariable>* bitset : watchers_) {
1450  bitset->Set(i_lit.var);
1451  }
1452 
1453  // Special case for level zero.
1454  if (integer_search_levels_.empty()) {
1455  vars_[i_lit.var].current_bound = i_lit.bound;
1456  integer_trail_[i_lit.var.value()].bound = i_lit.bound;
1457 
1458  // We also update the initial domain. If this fail, since we are at level
1459  // zero, we don't care about the reason.
1460  trail_->MutableConflict()->clear();
1461  return UpdateInitialDomain(
1462  i_lit.var,
1463  Domain(LowerBound(i_lit.var).value(), UpperBound(i_lit.var).value()));
1464  }
1465  DCHECK_GT(trail_->CurrentDecisionLevel(), 0);
1466 
1467  const int reason_index = literals_reason_starts_.size();
1468  CHECK_EQ(reason_index, bounds_reason_starts_.size());
1469  literals_reason_starts_.push_back(literals_reason_buffer_.size());
1470  bounds_reason_starts_.push_back(bounds_reason_buffer_.size());
1471  literals_reason_buffer_.push_back(literal_reason.Negated());
1472 
1473  const int prev_trail_index = vars_[i_lit.var].current_trail_index;
1474  integer_trail_.push_back({/*bound=*/i_lit.bound,
1475  /*var=*/i_lit.var,
1476  /*prev_trail_index=*/prev_trail_index,
1477  /*reason_index=*/reason_index});
1478 
1479  vars_[i_lit.var].current_bound = i_lit.bound;
1480  vars_[i_lit.var].current_trail_index = integer_trail_.size() - 1;
1481  return true;
1482 }
1483 
1484 void IntegerTrail::ComputeLazyReasonIfNeeded(int trail_index) const {
1485  const int reason_index = integer_trail_[trail_index].reason_index;
1486  if (reason_index == -1) {
1487  const TrailEntry& entry = integer_trail_[trail_index];
1488  const IntegerLiteral literal(entry.var, entry.bound);
1489  lazy_reasons_[trail_index](literal, trail_index, &lazy_reason_literals_,
1490  &lazy_reason_trail_indices_);
1491  }
1492 }
1493 
1494 absl::Span<const int> IntegerTrail::Dependencies(int trail_index) const {
1495  const int reason_index = integer_trail_[trail_index].reason_index;
1496  if (reason_index == -1) {
1497  return absl::Span<const int>(lazy_reason_trail_indices_);
1498  }
1499 
1500  const int start = bounds_reason_starts_[reason_index];
1501  const int end = reason_index + 1 < bounds_reason_starts_.size()
1502  ? bounds_reason_starts_[reason_index + 1]
1503  : bounds_reason_buffer_.size();
1504  if (start == end) return {};
1505 
1506  // Cache the result if not already computed. Remark, if the result was never
1507  // computed then the span trail_index_reason_buffer_[start, end) will either
1508  // be non-existent or full of -1.
1509  //
1510  // TODO(user): For empty reason, we will always recompute them.
1511  if (end > trail_index_reason_buffer_.size()) {
1512  trail_index_reason_buffer_.resize(end, -1);
1513  }
1514  if (trail_index_reason_buffer_[start] == -1) {
1515  int new_end = start;
1516  const int num_vars = vars_.size();
1517  for (int i = start; i < end; ++i) {
1518  const int dep =
1519  FindLowestTrailIndexThatExplainBound(bounds_reason_buffer_[i]);
1520  if (dep >= num_vars) {
1521  trail_index_reason_buffer_[new_end++] = dep;
1522  }
1523  }
1524  return absl::Span<const int>(&trail_index_reason_buffer_[start],
1525  new_end - start);
1526  } else {
1527  // TODO(user): We didn't store new_end in a previous call, so end might be
1528  // larger. That is a bit annoying since we have to test for -1 while
1529  // iterating.
1530  return absl::Span<const int>(&trail_index_reason_buffer_[start],
1531  end - start);
1532  }
1533 }
1534 
1535 void IntegerTrail::AppendLiteralsReason(int trail_index,
1536  std::vector<Literal>* output) const {
1537  CHECK_GE(trail_index, vars_.size());
1538  const int reason_index = integer_trail_[trail_index].reason_index;
1539  if (reason_index == -1) {
1540  for (const Literal l : lazy_reason_literals_) {
1541  if (!added_variables_[l.Variable()]) {
1542  added_variables_.Set(l.Variable());
1543  output->push_back(l);
1544  }
1545  }
1546  return;
1547  }
1548 
1549  const int start = literals_reason_starts_[reason_index];
1550  const int end = reason_index + 1 < literals_reason_starts_.size()
1551  ? literals_reason_starts_[reason_index + 1]
1552  : literals_reason_buffer_.size();
1553  for (int i = start; i < end; ++i) {
1554  const Literal l = literals_reason_buffer_[i];
1555  if (!added_variables_[l.Variable()]) {
1556  added_variables_.Set(l.Variable());
1557  output->push_back(l);
1558  }
1559  }
1560 }
1561 
1562 std::vector<Literal> IntegerTrail::ReasonFor(IntegerLiteral literal) const {
1563  std::vector<Literal> reason;
1564  MergeReasonInto({literal}, &reason);
1565  return reason;
1566 }
1567 
1568 // TODO(user): If this is called many time on the same variables, it could be
1569 // made faster by using some caching mecanism.
1570 void IntegerTrail::MergeReasonInto(absl::Span<const IntegerLiteral> literals,
1571  std::vector<Literal>* output) const {
1572  DCHECK(tmp_queue_.empty());
1573  const int num_vars = vars_.size();
1574  for (const IntegerLiteral& literal : literals) {
1575  const int trail_index = FindLowestTrailIndexThatExplainBound(literal);
1576 
1577  // Any indices lower than that means that there is no reason needed.
1578  // Note that it is important for size to be signed because of -1 indices.
1579  if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
1580  }
1581  return MergeReasonIntoInternal(output);
1582 }
1583 
1584 // This will expand the reason of the IntegerLiteral already in tmp_queue_ until
1585 // everything is explained in term of Literal.
1586 void IntegerTrail::MergeReasonIntoInternal(std::vector<Literal>* output) const {
1587  // All relevant trail indices will be >= vars_.size(), so we can safely use
1588  // zero to means that no literal refering to this variable is in the queue.
1589  DCHECK(std::all_of(tmp_var_to_trail_index_in_queue_.begin(),
1590  tmp_var_to_trail_index_in_queue_.end(),
1591  [](int v) { return v == 0; }));
1592 
1593  added_variables_.ClearAndResize(BooleanVariable(trail_->NumVariables()));
1594  for (const Literal l : *output) {
1595  added_variables_.Set(l.Variable());
1596  }
1597 
1598  // During the algorithm execution, all the queue entries that do not match the
1599  // content of tmp_var_to_trail_index_in_queue_[] will be ignored.
1600  for (const int trail_index : tmp_queue_) {
1601  DCHECK_GE(trail_index, vars_.size());
1602  DCHECK_LT(trail_index, integer_trail_.size());
1603  const TrailEntry& entry = integer_trail_[trail_index];
1604  tmp_var_to_trail_index_in_queue_[entry.var] =
1605  std::max(tmp_var_to_trail_index_in_queue_[entry.var], trail_index);
1606  }
1607 
1608  // We manage our heap by hand so that we can range iterate over it above, and
1609  // this initial heapify is faster.
1610  std::make_heap(tmp_queue_.begin(), tmp_queue_.end());
1611 
1612  // We process the entries by highest trail_index first. The content of the
1613  // queue will always be a valid reason for the literals we already added to
1614  // the output.
1615  tmp_to_clear_.clear();
1616  while (!tmp_queue_.empty()) {
1617  const int trail_index = tmp_queue_.front();
1618  const TrailEntry& entry = integer_trail_[trail_index];
1619  std::pop_heap(tmp_queue_.begin(), tmp_queue_.end());
1620  tmp_queue_.pop_back();
1621 
1622  // Skip any stale queue entry. Amongst all the entry refering to a given
1623  // variable, only the latest added to the queue is valid and we detect it
1624  // using its trail index.
1625  if (tmp_var_to_trail_index_in_queue_[entry.var] != trail_index) {
1626  continue;
1627  }
1628 
1629  // Set the cache threshold. Since we process trail indices in decreasing
1630  // order and we only have single linked list, we only want to advance the
1631  // "cache" up to this threshold.
1632  var_trail_index_cache_threshold_ = trail_index;
1633 
1634  // If this entry has an associated literal, then it should always be the
1635  // one we used for the reason. This code DCHECK that.
1636  if (DEBUG_MODE) {
1637  const LiteralIndex associated_lit =
1639  IntegerVariable(entry.var), entry.bound));
1640  if (associated_lit != kNoLiteralIndex) {
1641  // We check that the reason is the same!
1642  const int reason_index = integer_trail_[trail_index].reason_index;
1643  CHECK_NE(reason_index, -1);
1644  {
1645  const int start = literals_reason_starts_[reason_index];
1646  const int end = reason_index + 1 < literals_reason_starts_.size()
1647  ? literals_reason_starts_[reason_index + 1]
1648  : literals_reason_buffer_.size();
1649  CHECK_EQ(start + 1, end);
1650  CHECK_EQ(literals_reason_buffer_[start],
1651  Literal(associated_lit).Negated());
1652  }
1653  {
1654  const int start = bounds_reason_starts_[reason_index];
1655  const int end = reason_index + 1 < bounds_reason_starts_.size()
1656  ? bounds_reason_starts_[reason_index + 1]
1657  : bounds_reason_buffer_.size();
1658  CHECK_EQ(start, end);
1659  }
1660  }
1661  }
1662 
1663  // Process this entry. Note that if any of the next expansion include the
1664  // variable entry.var in their reason, we must process it again because we
1665  // cannot easily detect if it was needed to infer the current entry.
1666  //
1667  // Important: the queue might already contains entries refering to the same
1668  // variable. The code act like if we deleted all of them at this point, we
1669  // just do that lazily. tmp_var_to_trail_index_in_queue_[var] will
1670  // only refer to newly added entries.
1671  tmp_var_to_trail_index_in_queue_[entry.var] = 0;
1672  has_dependency_ = false;
1673 
1674  ComputeLazyReasonIfNeeded(trail_index);
1675  AppendLiteralsReason(trail_index, output);
1676  for (const int next_trail_index : Dependencies(trail_index)) {
1677  if (next_trail_index < 0) break;
1678  DCHECK_LT(next_trail_index, trail_index);
1679  const TrailEntry& next_entry = integer_trail_[next_trail_index];
1680 
1681  // Only add literals that are not "implied" by the ones already present.
1682  // For instance, do not add (x >= 4) if we already have (x >= 7). This
1683  // translate into only adding a trail index if it is larger than the one
1684  // in the queue refering to the same variable.
1685  const int index_in_queue =
1686  tmp_var_to_trail_index_in_queue_[next_entry.var];
1687  if (index_in_queue != kint32max) has_dependency_ = true;
1688  if (next_trail_index > index_in_queue) {
1689  tmp_var_to_trail_index_in_queue_[next_entry.var] = next_trail_index;
1690  tmp_queue_.push_back(next_trail_index);
1691  std::push_heap(tmp_queue_.begin(), tmp_queue_.end());
1692  }
1693  }
1694 
1695  // Special case for a "leaf", we will never need this variable again.
1696  if (!has_dependency_) {
1697  tmp_to_clear_.push_back(entry.var);
1698  tmp_var_to_trail_index_in_queue_[entry.var] = kint32max;
1699  }
1700  }
1701 
1702  // clean-up.
1703  for (const IntegerVariable var : tmp_to_clear_) {
1704  tmp_var_to_trail_index_in_queue_[var] = 0;
1705  }
1706 }
1707 
1708 absl::Span<const Literal> IntegerTrail::Reason(const Trail& trail,
1709  int trail_index) const {
1710  const int index = boolean_trail_index_to_integer_one_[trail_index];
1711  std::vector<Literal>* reason = trail.GetEmptyVectorToStoreReason(trail_index);
1712  added_variables_.ClearAndResize(BooleanVariable(trail_->NumVariables()));
1713 
1714  ComputeLazyReasonIfNeeded(index);
1715  AppendLiteralsReason(index, reason);
1716  DCHECK(tmp_queue_.empty());
1717  for (const int prev_trail_index : Dependencies(index)) {
1718  if (prev_trail_index < 0) break;
1719  DCHECK_GE(prev_trail_index, vars_.size());
1720  tmp_queue_.push_back(prev_trail_index);
1721  }
1722  MergeReasonIntoInternal(reason);
1723  return *reason;
1724 }
1725 
1726 // TODO(user): Implement a dense version if there is more trail entries
1727 // than variables!
1728 void IntegerTrail::AppendNewBounds(std::vector<IntegerLiteral>* output) const {
1729  tmp_marked_.ClearAndResize(IntegerVariable(vars_.size()));
1730 
1731  // In order to push the best bound for each variable, we loop backward.
1732  const int end = vars_.size();
1733  for (int i = integer_trail_.size(); --i >= end;) {
1734  const TrailEntry& entry = integer_trail_[i];
1735  if (entry.var == kNoIntegerVariable) continue;
1736  if (tmp_marked_[entry.var]) continue;
1737 
1738  tmp_marked_.Set(entry.var);
1739  output->push_back(IntegerLiteral::GreaterOrEqual(entry.var, entry.bound));
1740  }
1741 }
1742 
1744  : SatPropagator("GenericLiteralWatcher"),
1745  time_limit_(model->GetOrCreate<TimeLimit>()),
1746  integer_trail_(model->GetOrCreate<IntegerTrail>()),
1747  rev_int_repository_(model->GetOrCreate<RevIntRepository>()) {
1748  // TODO(user): This propagator currently needs to be last because it is the
1749  // only one enforcing that a fix-point is reached on the integer variables.
1750  // Figure out a better interaction between the sat propagation loop and
1751  // this one.
1752  model->GetOrCreate<SatSolver>()->AddLastPropagator(this);
1753 
1754  integer_trail_->RegisterReversibleClass(
1755  &id_to_greatest_common_level_since_last_call_);
1756  integer_trail_->RegisterWatcher(&modified_vars_);
1757  queue_by_priority_.resize(2); // Because default priority is 1.
1758 }
1759 
1760 void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) {
1761  // Process any new Literal on the trail.
1762  while (propagation_trail_index_ < trail->Index()) {
1763  const Literal literal = (*trail)[propagation_trail_index_++];
1764  if (literal.Index() >= literal_to_watcher_.size()) continue;
1765  for (const auto entry : literal_to_watcher_[literal.Index()]) {
1766  if (!in_queue_[entry.id]) {
1767  in_queue_[entry.id] = true;
1768  queue_by_priority_[id_to_priority_[entry.id]].push_back(entry.id);
1769  }
1770  if (entry.watch_index >= 0) {
1771  id_to_watch_indices_[entry.id].push_back(entry.watch_index);
1772  }
1773  }
1774  }
1775 
1776  // Process the newly changed variables lower bounds.
1777  for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
1778  if (var.value() >= var_to_watcher_.size()) continue;
1779  for (const auto entry : var_to_watcher_[var]) {
1780  if (!in_queue_[entry.id]) {
1781  in_queue_[entry.id] = true;
1782  queue_by_priority_[id_to_priority_[entry.id]].push_back(entry.id);
1783  }
1784  if (entry.watch_index >= 0) {
1785  id_to_watch_indices_[entry.id].push_back(entry.watch_index);
1786  }
1787  }
1788  }
1789 
1790  if (trail->CurrentDecisionLevel() == 0) {
1791  const std::vector<IntegerVariable>& modified_vars =
1792  modified_vars_.PositionsSetAtLeastOnce();
1793  for (const auto& callback : level_zero_modified_variable_callback_) {
1794  callback(modified_vars);
1795  }
1796  }
1797 
1798  modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
1799 }
1800 
1802  // Only once per call to Propagate(), if we are at level zero, we might want
1803  // to call propagators even if the bounds didn't change.
1804  const int level = trail->CurrentDecisionLevel();
1805  if (level == 0) {
1806  for (const int id : propagator_ids_to_call_at_level_zero_) {
1807  if (in_queue_[id]) continue;
1808  in_queue_[id] = true;
1809  queue_by_priority_[id_to_priority_[id]].push_back(id);
1810  }
1811  }
1812 
1813  UpdateCallingNeeds(trail);
1814 
1815  // Note that the priority may be set to -1 inside the loop in order to restart
1816  // at zero.
1817  int test_limit = 0;
1818  for (int priority = 0; priority < queue_by_priority_.size(); ++priority) {
1819  // We test the time limit from time to time. This is in order to return in
1820  // case of slow propagation.
1821  //
1822  // TODO(user): The queue will not be emptied, but I am not sure the solver
1823  // will be left in an usable state. Fix if it become needed to resume
1824  // the solve from the last time it was interupted.
1825  if (test_limit > 100) {
1826  test_limit = 0;
1827  if (time_limit_->LimitReached()) break;
1828  }
1829 
1830  std::deque<int>& queue = queue_by_priority_[priority];
1831  while (!queue.empty()) {
1832  const int id = queue.front();
1833  current_id_ = id;
1834  queue.pop_front();
1835 
1836  // Before we propagate, make sure any reversible structure are up to date.
1837  // Note that we never do anything expensive more than once per level.
1838  {
1839  const int low =
1840  id_to_greatest_common_level_since_last_call_[IdType(id)];
1841  const int high = id_to_level_at_last_call_[id];
1842  if (low < high || level > low) { // Equivalent to not all equal.
1843  id_to_level_at_last_call_[id] = level;
1844  id_to_greatest_common_level_since_last_call_.MutableRef(IdType(id)) =
1845  level;
1846  for (ReversibleInterface* rev : id_to_reversible_classes_[id]) {
1847  if (low < high) rev->SetLevel(low);
1848  if (level > low) rev->SetLevel(level);
1849  }
1850  for (int* rev_int : id_to_reversible_ints_[id]) {
1851  rev_int_repository_->SaveState(rev_int);
1852  }
1853  }
1854  }
1855 
1856  // This is needed to detect if the propagator propagated anything or not.
1857  const int64 old_integer_timestamp = integer_trail_->num_enqueues();
1858  const int64 old_boolean_timestamp = trail->Index();
1859 
1860  // TODO(user): Maybe just provide one function Propagate(watch_indices) ?
1861  std::vector<int>& watch_indices_ref = id_to_watch_indices_[id];
1862  const bool result =
1863  watch_indices_ref.empty()
1864  ? watchers_[id]->Propagate()
1865  : watchers_[id]->IncrementalPropagate(watch_indices_ref);
1866  if (!result) {
1867  watch_indices_ref.clear();
1868  in_queue_[id] = false;
1869  return false;
1870  }
1871 
1872  // Update the propagation queue. At this point, the propagator has been
1873  // removed from the queue but in_queue_ is still true.
1874  if (id_to_idempotence_[id]) {
1875  // If the propagator is assumed to be idempotent, then we set in_queue_
1876  // to false after UpdateCallingNeeds() so this later function will never
1877  // add it back.
1878  UpdateCallingNeeds(trail);
1879  watch_indices_ref.clear();
1880  in_queue_[id] = false;
1881  } else {
1882  // Otherwise, we set in_queue_ to false first so that
1883  // UpdateCallingNeeds() may add it back if the propagator modified any
1884  // of its watched variables.
1885  watch_indices_ref.clear();
1886  in_queue_[id] = false;
1887  UpdateCallingNeeds(trail);
1888  }
1889 
1890  // If the propagator pushed a literal, we exit in order to rerun all SAT
1891  // only propagators first. Note that since a literal was pushed we are
1892  // guaranteed to be called again, and we will resume from priority 0.
1893  if (trail->Index() > old_boolean_timestamp) {
1894  // Important: for now we need to re-run the clauses propagator each time
1895  // we push a new literal because some propagator like the arc consistent
1896  // all diff relies on this.
1897  //
1898  // TODO(user): However, on some problem, it seems to work better to not
1899  // do that. One possible reason is that the reason of a "natural"
1900  // propagation might be better than one we learned.
1901  return true;
1902  }
1903 
1904  // If the propagator pushed an integer bound, we revert to priority = 0.
1905  if (integer_trail_->num_enqueues() > old_integer_timestamp) {
1906  ++test_limit;
1907  priority = -1; // Because of the ++priority in the for loop.
1908  break;
1909  }
1910  }
1911  }
1912  return true;
1913 }
1914 
1915 void GenericLiteralWatcher::Untrail(const Trail& trail, int trail_index) {
1916  if (propagation_trail_index_ <= trail_index) {
1917  // Nothing to do since we found a conflict before Propagate() was called.
1918  CHECK_EQ(propagation_trail_index_, trail_index);
1919  return;
1920  }
1921 
1922  // We need to clear the watch indices on untrail.
1923  for (std::deque<int>& queue : queue_by_priority_) {
1924  for (const int id : queue) {
1925  id_to_watch_indices_[id].clear();
1926  }
1927  queue.clear();
1928  }
1929 
1930  // This means that we already propagated all there is to propagate
1931  // at the level trail_index, so we can safely clear modified_vars_ in case
1932  // it wasn't already done.
1933  propagation_trail_index_ = trail_index;
1934  modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
1935  in_queue_.assign(watchers_.size(), false);
1936 }
1937 
1938 // Registers a propagator and returns its unique ids.
1940  const int id = watchers_.size();
1941  watchers_.push_back(propagator);
1942  id_to_level_at_last_call_.push_back(0);
1943  id_to_greatest_common_level_since_last_call_.GrowByOne();
1944  id_to_reversible_classes_.push_back(std::vector<ReversibleInterface*>());
1945  id_to_reversible_ints_.push_back(std::vector<int*>());
1946  id_to_watch_indices_.push_back(std::vector<int>());
1947  id_to_priority_.push_back(1);
1948  id_to_idempotence_.push_back(true);
1949 
1950  // Call this propagator at least once the next time Propagate() is called.
1951  //
1952  // TODO(user): This initial propagation does not respect any later priority
1953  // settings. Fix this. Maybe we should force users to pass the priority at
1954  // registration. For now I didn't want to change the interface because there
1955  // are plans to implement a kind of "dynamic" priority, and if it works we may
1956  // want to get rid of this altogether.
1957  in_queue_.push_back(true);
1958  queue_by_priority_[1].push_back(id);
1959  return id;
1960 }
1961 
1963  id_to_priority_[id] = priority;
1964  if (priority >= queue_by_priority_.size()) {
1965  queue_by_priority_.resize(priority + 1);
1966  }
1967 }
1968 
1970  int id) {
1971  id_to_idempotence_[id] = false;
1972 }
1973 
1975  propagator_ids_to_call_at_level_zero_.push_back(id);
1976 }
1977 
1979  ReversibleInterface* rev) {
1980  id_to_reversible_classes_[id].push_back(rev);
1981 }
1982 
1984  id_to_reversible_ints_[id].push_back(rev);
1985 }
1986 
1987 // This is really close to ExcludeCurrentSolutionAndBacktrack().
1988 std::function<void(Model*)>
1990  return [=](Model* model) {
1991  SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
1992  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
1993  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1994 
1995  const int current_level = sat_solver->CurrentDecisionLevel();
1996  std::vector<Literal> clause_to_exclude_solution;
1997  clause_to_exclude_solution.reserve(current_level);
1998  for (int i = 0; i < current_level; ++i) {
1999  bool include_decision = true;
2000  const Literal decision = sat_solver->Decisions()[i].literal;
2001 
2002  // Tests if this decision is associated to a bound of an ignored variable
2003  // in the current assignment.
2004  const InlinedIntegerLiteralVector& associated_literals =
2005  encoder->GetIntegerLiterals(decision);
2006  for (const IntegerLiteral bound : associated_literals) {
2007  if (integer_trail->IsCurrentlyIgnored(bound.var)) {
2008  // In this case we replace the decision (which is a bound on an
2009  // ignored variable) with the fact that the integer variable was
2010  // ignored. This works because the only impact a bound of an ignored
2011  // variable can have on the rest of the model is through the
2012  // is_ignored literal.
2013  clause_to_exclude_solution.push_back(
2014  integer_trail->IsIgnoredLiteral(bound.var).Negated());
2015  include_decision = false;
2016  }
2017  }
2018 
2019  if (include_decision) {
2020  clause_to_exclude_solution.push_back(decision.Negated());
2021  }
2022  }
2023 
2024  // Note that it is okay to add duplicates literals in ClauseConstraint(),
2025  // the clause will be preprocessed correctly.
2026  sat_solver->Backtrack(0);
2027  model->Add(ClauseConstraint(clause_to_exclude_solution));
2028  };
2029 }
2030 
2031 } // namespace sat
2032 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define DLOG_IF(severity, condition)
Definition: base/logging.h:877
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
#define VLOG(verboselevel)
Definition: base/logging.h:978
void resize(size_type new_size)
void reserve(size_type n)
size_type size() const
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
Domain Negation() const
Returns {x ∈ Int64, ∃ e ∈ D, x = -e}.
absl::InlinedVector< ClosedInterval, 1 >::const_iterator end() const
int NumIntervals() const
Basic read-only std::vector<> wrapping to view a Domain as a sorted list of non-adjacent intervals.
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and 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 Set(key_type key, mapped_type value)
Definition: rev.h:238
void SetLevel(int level) final
Definition: rev.h:206
const mapped_type & FindOrDie(key_type key) const
Definition: rev.h:172
void SaveState(T *object)
Definition: rev.h:61
T & MutableRef(IndexType index)
Definition: rev.h:95
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
void Set(IntegerType index)
Definition: bitset.h:803
void ClearAndResize(IntegerType size)
Definition: bitset.h:778
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
Definition: time_limit.h:532
void RegisterReversibleClass(int id, ReversibleInterface *rev)
Definition: integer.cc:1978
void SetPropagatorPriority(int id, int priority)
Definition: integer.cc:1962
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
void Untrail(const Trail &trail, int literal_trail_index) final
Definition: integer.cc:1915
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
Definition: integer.cc:248
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i, IntegerValue *bound) const
Definition: integer.cc:460
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
Definition: integer.cc:452
void FullyEncodeVariable(IntegerVariable var)
Definition: integer.cc:36
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
Definition: integer.cc:184
const std::vector< IntegerLiteral > NewlyFixedIntegerLiterals() const
Definition: integer.h:409
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
Definition: integer.cc:308
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
Definition: integer.h:390
bool LiteralIsAssociated(IntegerLiteral i_lit) const
Definition: integer.cc:446
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
Definition: integer.cc:106
std::vector< ValueLiteralPair > PartialDomainEncoding(IntegerVariable var) const
Definition: integer.cc:112
bool VariableIsFullyEncoded(IntegerVariable var) const
Definition: integer.cc:68
LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const
Definition: integer.cc:238
void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit)
Definition: integer.cc:282
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
Definition: integer.cc:202
IntegerVariable FirstUnassignedVariable() const
Definition: integer.cc:1190
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:989
IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value)
Definition: integer.cc:695
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
Definition: integer.h:803
bool Propagate(Trail *trail) final
Definition: integer.cc:480
void ReserveSpaceForNumVariables(int num_vars)
Definition: integer.cc:592
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
Definition: integer.cc:716
bool IsCurrentlyIgnored(IntegerVariable i) const
Definition: integer.h:625
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
Definition: integer.cc:1562
std::function< void(IntegerLiteral literal_to_explain, int trail_index_of_literal, std::vector< Literal > *literals, std::vector< int > *dependencies)> LazyReasonFunction
Definition: integer.h:769
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
LiteralIndex OptionalLiteralIndex(IntegerVariable i) const
Definition: integer.h:634
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: integer.cc:1708
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.h:810
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1087
IntegerVariable NextVariableToBranchOnInPropagationLoop() const
Definition: integer.cc:1157
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:807
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1350
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:785
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
Definition: integer.cc:1728
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
void MergeReasonInto(absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
Definition: integer.cc:1570
Literal IsIgnoredLiteral(IntegerVariable i) const
Definition: integer.h:630
bool IsOptional(IntegerVariable i) const
Definition: integer.h:622
ABSL_MUST_USE_RESULT bool ConditionalEnqueue(Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
Definition: integer.cc:996
bool IntegerLiteralIsFalse(IntegerLiteral l) const
Definition: integer.h:1344
void RemoveLevelZeroBounds(std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:919
IntegerVariable AddIntegerVariable()
Definition: integer.h:613
void RegisterReversibleClass(ReversibleInterface *rev)
Definition: integer.h:833
const Domain & InitialVariableDomain(IntegerVariable var) const
Definition: integer.cc:644
void Untrail(const Trail &trail, int literal_trail_index) final
Definition: integer.cc:543
IntegerVariable NumIntegerVariables() const
Definition: integer.h:565
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
LiteralIndex Index() const
Definition: sat_base.h:84
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
Definition: sat_solver.cc:134
BooleanVariable NewBooleanVariable()
Definition: sat_solver.h:83
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
bool AddBinaryClause(Literal a, Literal b)
Definition: sat_solver.cc:180
void Backtrack(int target_level)
Definition: sat_solver.cc:888
const std::vector< Decision > & Decisions() const
Definition: sat_solver.h:359
bool AddUnitClause(Literal true_literal)
Definition: sat_solver.cc:164
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
void EnqueueWithUnitReason(Literal true_literal)
Definition: sat_base.h:265
bool LiteralIsAssigned(Literal literal) const
Definition: sat_base.h:153
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
MPCallback * callback
static const int64 kint64max
int64_t int64
static const int32 kint32max
static const int64 kint64min
const int INFO
Definition: log_severity.h:31
const bool DEBUG_MODE
Definition: macros.h:24
void InsertOrDie(Collection *const collection, const typename Collection::value_type &value)
Definition: map_util.h:135
absl::InlinedVector< IntegerLiteral, 2 > InlinedIntegerLiteralVector
Definition: integer.h:198
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
const LiteralIndex kNoLiteralIndex(-1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
Definition: integer.cc:1989
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
Definition: integer.h:140
bool VariableIsPositive(IntegerVariable i)
Definition: integer.h:130
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapProd(int64 x, int64 y)
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
ColIndex representative
IntervalVar * interval
Definition: resource.cc:98
int64 bound
Represents a closed interval [start, end].
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264