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