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
23
24namespace operations_research {
25namespace sat {
26
27std::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
68bool 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
105std::vector<IntegerEncoder::ValueLiteralPair>
109}
110
111std::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.
144void 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
184std::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
230namespace {
231std::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.
408void IntegerEncoder::HalfAssociateGivenLiteral(IntegerLiteral i_lit,
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 }
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
543void 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
603IntegerVariable 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
636IntegerVariable 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
644const Domain& IntegerTrail::InitialVariableDomain(IntegerVariable var) const {
645 return (*domains_)[var];
646}
647
648bool 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
750int 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
822void 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
929std::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
950namespace {
951
952std::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
970std::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
1038bool 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
1093void 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.
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
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
1198bool 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
1431bool 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
1484void 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
1494absl::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
1535void 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
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.
1570void 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.
1586void 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
1708absl::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!
1728void 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
1760void 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
1915void 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().
1988std::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}.
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.
absl::InlinedVector< ClosedInterval, 1 >::const_iterator end() const
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
void Set(IntegerType index)
Definition: bitset.h:803
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
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
const std::vector< IntegerLiteral > NewlyFixedIntegerLiterals() const
Definition: integer.h:409
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
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
Definition: integer.cc:308
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
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
Definition: integer.h:390
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
const std::vector< Decision > & Decisions() const
Definition: sat_solver.h:359
bool AddBinaryClause(Literal a, Literal b)
Definition: sat_solver.cc:180
void Backtrack(int target_level)
Definition: sat_solver.cc:888
bool AddUnitClause(Literal true_literal)
Definition: sat_solver.cc:164
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
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
bool VariableIsPositive(IntegerVariable i)
Definition: integer.h:130
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
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
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 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