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