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"
40#include "ortools/sat/sat_parameters.pb.h"
53 absl::Span<const IntegerVariable> vars) {
54 std::vector<IntegerVariable> result(vars.size());
55 for (
int i = 0;
i < vars.size(); ++
i) {
62 return absl::StrCat(
"(literal = ",
literal.DebugString(),
63 ", value = ",
value.value(),
")");
75 encoding_by_var_.reserve(num_vars);
76 equality_to_associated_literal_.reserve(num_vars);
77 equality_by_var_.reserve(num_vars);
83 CHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
86 CHECK(!domains_[index].IsEmpty());
87 CHECK_LT(domains_[index].Size(), 100000)
88 <<
"Domain too large for full encoding.";
99 for (
const int64_t v : domains_[index].Values()) {
100 tmp_values_.push_back(IntegerValue(v));
102 for (
const IntegerValue v : tmp_values_) {
113 if (index >= is_fully_encoded_.size())
return false;
116 if (is_fully_encoded_[index])
return true;
123 const int64_t initial_domain_size = domains_[index].Size();
124 if (equality_by_var_[index].size() < initial_domain_size)
return false;
133 const auto& ref = equality_by_var_[index];
135 for (
const int64_t v : domains_[index].Values()) {
136 if (
i < ref.size() && v == ref[
i].value) {
140 if (
i == ref.size()) {
141 is_fully_encoded_[index] =
true;
143 return is_fully_encoded_[index];
147 IntegerVariable var)
const {
153 IntegerVariable var)
const {
155 if (index >= equality_by_var_.size()) {
156 partial_encoding_.clear();
157 return partial_encoding_;
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) {
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);
172 partial_encoding_[new_size++] = pair;
174 partial_encoding_.resize(new_size);
175 std::sort(partial_encoding_.begin(), partial_encoding_.end(),
178 if (trail_->CurrentDecisionLevel() == 0) {
180 equality_by_var_[index].assign(partial_encoding_.begin(),
181 partial_encoding_.end());
185 std::reverse(partial_encoding_.begin(), partial_encoding_.end());
188 return partial_encoding_;
194void IntegerEncoder::AddImplications(
195 const absl::btree_map<IntegerValue, Literal>& map,
196 absl::btree_map<IntegerValue, Literal>::const_iterator it,
198 if (!add_implications_)
return;
199 DCHECK_EQ(it->second, associated_lit);
204 if (it != map.begin()) {
207 before_index = before_it->second.Index();
213 if (after_it != map.end()) after_index = after_it->second.Index();
219 {Literal(after_index).Negated(), associated_lit});
222 sat_solver_->AddClauseDuringSearch(
223 {associated_lit.
Negated(), Literal(before_index)});
228 CHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
229 add_implications_ =
true;
233 const int num_vars = encoding_by_var_.size();
234 for (PositiveOnlyIndex index(0); index < num_vars; ++index) {
236 const IntegerVariable var(2 * index.value());
240 sat_solver_->AddBinaryClause(literal.Negated(),
Literal(previous));
242 previous = literal.Index();
250 if (!positive) i_lit = i_lit.
Negated();
252 const IntegerVariable var(i_lit.
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();
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;
282 const IntegerValue bound = -i_lit.
bound;
298 ++num_created_variables_;
299 const Literal literal(sat_solver_->NewBooleanVariable(),
true);
304 if (sat_solver_->Assignment().LiteralIsAssigned(literal)) {
305 VLOG(1) <<
"Created a fixed literal for no reason!";
311std::pair<PositiveOnlyIndex, IntegerValue> PositiveVarKey(IntegerVariable var,
312 IntegerValue value) {
319 IntegerVariable var, IntegerValue value)
const {
321 equality_to_associated_literal_.find(PositiveVarKey(var, value));
322 if (it != equality_to_associated_literal_.end()) {
323 return it->second.Index();
329 IntegerVariable var, IntegerValue value) {
332 equality_to_associated_literal_.find(PositiveVarKey(var, value));
333 if (it != equality_to_associated_literal_.end()) {
350 ++num_created_variables_;
351 const Literal literal(sat_solver_->NewBooleanVariable(),
true);
359 if (sat_solver_->Assignment().LiteralIsAssigned(literal)) {
360 VLOG(1) <<
"Created a fixed literal for no reason!";
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);
380 if (i_lit.
bound > max) {
381 return (
void)sat_solver_->AddUnitClause(literal.
Negated());
384 if (index >= encoding_by_var_.size()) {
385 encoding_by_var_.resize(index.value() + 1);
387 auto& var_encoding = encoding_by_var_[index];
392 const auto [it, inserted] =
393 var_encoding.insert({canonical_pair.first.bound, literal});
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});
403 AddImplications(var_encoding, it, literal);
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);
410 if (sat_solver_->Assignment().LiteralIsFalse(literal)) {
411 delayed_to_fix_->integer_literal_to_fix.push_back(canonical_pair.second);
418 if (new_size > reverse_encoding_.size()) {
419 reverse_encoding_.resize(new_size);
421 reverse_encoding_[literal].push_back(canonical_pair.first);
422 reverse_encoding_[literal.
NegatedIndex()].push_back(canonical_pair.second);
427 if (canonical_pair.first.bound == max) {
430 if (-canonical_pair.second.bound == min) {
437 IntegerValue value) {
448 const Domain& domain = domains_[index];
449 if (value == 1 && domain.
Min() >= 0 && domain.
Max() <= 1) {
450 if (literal.
Index() >= literal_view_.size()) {
452 literal_view_[literal] = var;
454 literal_view_[literal] = var;
460 const auto insert_result = equality_to_associated_literal_.insert(
461 {PositiveVarKey(var, value), literal});
462 if (!insert_result.second) {
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});
473 if (!domain.
Contains(value.value())) {
474 return (
void)sat_solver_->AddUnitClause(literal.
Negated());
480 if (index >= equality_by_var_.size()) {
481 equality_by_var_.resize(index.value() + 1);
482 is_fully_encoded_.resize(index.value() + 1);
484 equality_by_var_[index].push_back({value, literal});
488 return (
void)sat_solver_->AddUnitClause(literal);
495 if (value == domain.
Min()) {
504 if (value == domain.
Max()) {
512 sat_solver_->AddClauseDuringSearch({a, literal.
Negated()});
513 sat_solver_->AddClauseDuringSearch({
b, literal.
Negated()});
514 sat_solver_->AddClauseDuringSearch({a.
Negated(),
b.Negated(), literal});
517 const int new_size = 1 + literal.
Index().value();
518 if (new_size > reverse_equality_encoding_.size()) {
519 reverse_equality_encoding_.resize(new_size);
521 reverse_equality_encoding_[literal].push_back({var, value});
527 if (i_lit.
bound <= domains_[index].Min())
return true;
528 if (i_lit.
bound > domains_[index].Max())
return true;
536 const LiteralIndex result =
551 const auto& encoding = encoding_by_var_[index];
556 auto after_it = encoding.upper_bound(i_lit.
bound);
559 *bound = after_it->first;
560 return after_it->second.Index();
564 auto after_it = encoding.upper_bound(-i_lit.
bound);
568 const Domain& domain = domains_[index];
571 return after_it->second.NegatedIndex();
576 Literal lit, IntegerVariable* view,
bool* view_is_direct)
const {
583 if (view !=
nullptr) *view = direct_var;
584 if (view_is_direct !=
nullptr) *view_is_direct =
true;
588 if (view !=
nullptr) *view = opposite_var;
589 if (view_is_direct !=
nullptr) *view_is_direct =
false;
596 IntegerVariable var)
const {
597 std::vector<ValueLiteralPair> result;
599 if (index >= encoding_by_var_.size())
return result;
601 for (
const auto [value, literal] : encoding_by_var_[index]) {
602 result.push_back({value, literal});
608 const Domain& domain = domains_[index];
609 if (domain.
IsEmpty())
return result;
613 for (
const auto [value, literal] : encoding_by_var_[index]) {
614 while (value > domain[
i].
end) {
615 previous = domain[
i].
end;
617 if (
i == num_intervals)
break;
619 if (
i == num_intervals)
break;
620 if (value <= domain[
i].start) {
621 if (
i == 0)
continue;
622 result.push_back({-previous, literal.Negated()});
624 result.push_back({-value + 1, literal.Negated()});
627 std::reverse(result.begin(), result.end());
635 if (index >= encoding_by_var_.size())
return true;
641 tmp_encoding_.clear();
642 for (
const auto [value, literal] : encoding_by_var_[index]) {
646 if (trail_->Assignment().LiteralIsTrue(literal))
return false;
647 if (trail_->Assignment().LiteralIsFalse(literal))
continue;
649 trail_->EnqueueWithUnitReason(literal.Negated());
652 if (
i == 0 && value <= domain[0].start) {
654 if (trail_->Assignment().LiteralIsTrue(literal))
continue;
655 if (trail_->Assignment().LiteralIsFalse(literal))
return false;
657 trail_->EnqueueWithUnitReason(literal);
662 tmp_encoding_.push_back(
663 {std::max<IntegerValue>(value, domain[
i].start), literal});
665 encoding_by_var_[index].clear();
666 for (
const auto [value, literal] : tmp_encoding_) {
667 encoding_by_var_[index].insert({value, literal});
676 if (trail_->Assignment().LiteralIsTrue(pair.literal))
return false;
677 if (trail_->Assignment().LiteralIsFalse(pair.literal))
continue;
679 trail_->EnqueueWithUnitReason(pair.literal.Negated());
684 VLOG(1) <<
"Domain intersection fixed " << num_fixed
685 <<
" encoding literals";
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_;
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());
721 for (
const IntegerLiteral i_lit : delayed_to_fix_->integer_literal_to_fix) {
725 const IntegerValue lb =
729 sat_solver_->NotifyThatModelIsUnsat();
733 delayed_to_fix_->integer_literal_to_fix.clear();
735 for (
const Literal lit : delayed_to_fix_->literal_to_fix) {
736 if (trail_->Assignment().LiteralIsFalse(lit)) {
737 sat_solver_->NotifyThatModelIsUnsat();
740 if (trail_->Assignment().LiteralIsTrue(lit))
continue;
741 trail_->EnqueueWithUnitReason(lit);
743 delayed_to_fix_->literal_to_fix.clear();
750 for (
const IntegerLiteral i_lit : encoder_->GetIntegerLiterals(literal)) {
752 if (!EnqueueAssociatedIntegerLiteral(i_lit, literal)) {
763 conditional_lbs_.clear();
768 if (level < first_level_without_full_propagation_) {
769 first_level_without_full_propagation_ = -1;
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());
780 for (
int index = integer_trail_.size() - 1; index >= target; --index) {
781 const TrailEntry& entry = integer_trail_[index];
782 if (entry.var < 0)
continue;
783 var_trail_index_[entry.var] = entry.prev_trail_index;
784 var_lbs_[entry.var] = integer_trail_[entry.prev_trail_index].bound;
786 integer_trail_.resize(target);
789 lazy_reasons_.resize(lazy_reason_decision_levels_[level]);
790 lazy_reason_decision_levels_.resize(level);
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]);
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);
804 literals_reason_starts_.resize(old_size);
805 bounds_reason_starts_.resize(old_size);
806 cached_sizes_.resize(old_size);
816 domains_->reserve(num_vars);
817 encoder_->ReserveSpaceForNumVariables(num_vars);
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);
827 var_to_trail_index_at_lower_level_.reserve(size);
831 IntegerValue upper_bound) {
833 DCHECK_LE(lower_bound, upper_bound);
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());
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()));
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)});
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);
864 IntegerValue(domain.
Max()));
872 temp_domain_ = (*domains_)[index].Negation();
880 CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
887 const Domain& old_domain = (*domains_)[index];
889 if (old_domain == domain)
return true;
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;
903 var_lbs_[var] = domain.
Min();
904 integer_trail_[var.value()].bound = domain.
Min();
906 integer_trail_[
NegationOf(var).value()].bound = -domain.
Max();
910 if (lb_changed) bitset->Set(var);
915 return encoder_->UpdateEncodingOnInitialDomainChange(var, domain);
919 IntegerValue value) {
923 insert.first->second = new_var;
926 CHECK(constant_map_.emplace(-value,
NegationOf(new_var)).second);
930 return insert.first->second;
936 return (constant_map_.size() + 1) / 2;
940 int threshold)
const {
948 const int index_in_queue = tmp_var_to_trail_index_in_queue_[var];
949 if (threshold <= index_in_queue) {
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;
960 DCHECK_GE(threshold, var_lbs_.size());
961 int trail_index = var_trail_index_[var];
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;
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;
979 const int num_vars = var_lbs_.size();
980 return trail_index < num_vars ? -1 : trail_index;
983int IntegerTrail::FindLowestTrailIndexThatExplainBound(
985 DCHECK_LE(i_lit.
bound, var_lbs_[i_lit.
var]);
987 int trail_index = var_trail_index_[i_lit.
var];
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;
1004 int prev_trail_index = trail_index;
1006 if (trail_index >= var_trail_index_cache_threshold_) {
1007 var_trail_index_cache_[i_lit.
var] = trail_index;
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;
1019 IntegerValue slack, absl::Span<const IntegerValue> coeffs,
1020 std::vector<IntegerLiteral>* reason)
const {
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];
1034 for (
const int i : tmp_indices_) {
1036 integer_trail_[
i].bound));
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]);
1049 for (
const int i : tmp_indices_) {
1051 integer_trail_[
i].bound));
1056 absl::Span<const IntegerValue> coeffs,
1057 std::vector<int>* trail_indices)
const {
1058 DCHECK_GT(slack, 0);
1059 DCHECK(relax_heap_.empty());
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];
1072 if (index < num_vars)
continue;
1075 const IntegerValue coeff = coeffs[
i];
1076 if (coeff > slack) {
1077 (*trail_indices)[new_size++] = index;
1084 const TrailEntry& entry = integer_trail_[index];
1086 index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
1087 (*trail_indices)[new_size++] = index;
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());
1096 (*trail_indices)[new_size++] = index;
1100 relax_heap_.push_back({index, coeff, diff});
1102 trail_indices->resize(new_size);
1103 std::make_heap(relax_heap_.begin(), relax_heap_.end());
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();
1111 if (heap_entry.diff > slack) {
1112 trail_indices->push_back(heap_entry.index);
1117 slack -= heap_entry.diff;
1118 const int index = integer_trail_[heap_entry.index].prev_trail_index;
1121 if (index < num_vars)
continue;
1122 if (heap_entry.coeff > slack) {
1123 trail_indices->push_back(index);
1126 const TrailEntry& entry = integer_trail_[index];
1128 index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
1129 trail_indices->push_back(index);
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());
1137 trail_indices->push_back(index);
1140 relax_heap_.push_back({index, heap_entry.coeff, diff});
1141 std::push_heap(relax_heap_.begin(), relax_heap_.end());
1146 for (
const RelaxHeapEntry& entry : relax_heap_) {
1147 trail_indices->push_back(entry.index);
1149 relax_heap_.clear();
1153 std::vector<IntegerLiteral>* reason)
const {
1157 (*reason)[new_size++] = literal;
1159 reason->resize(new_size);
1162std::vector<Literal>* IntegerTrail::InitializeConflict(
1164 absl::Span<const Literal> literals_reason,
1165 absl::Span<const IntegerLiteral> bounds_reason) {
1166 DCHECK(tmp_queue_.empty());
1168 if (use_lazy_reason) {
1171 lazy_reasons_.back().Explain(conflict, &tmp_queue_);
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);
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();
1192 result +=
"} bounds:{";
1194 if (result.back() !=
'{') result +=
",";
1195 result += l.DebugString();
1203std::string IntegerTrail::DebugString() {
1204 std::string result =
"trail:{";
1205 const int num_vars = var_lbs_.size();
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 +=
",";
1212 integer_trail_[
i].bound)
1215 if (limit < integer_trail_.size()) {
1223 DCHECK(ReasonIsValid(i_lit, {}, {}));
1226 sat_solver_->NotifyThatModelIsUnsat();
1229 if (trail_->CurrentDecisionLevel() == 0) {
1230 if (!
Enqueue(i_lit, {}, {})) {
1231 sat_solver_->NotifyThatModelIsUnsat();
1240 integer_trail_[i_lit.
var.value()].bound = i_lit.
bound;
1241 delayed_to_fix_->integer_literal_to_fix.push_back(i_lit);
1246 IntegerLiteral i_lit, absl::Span<const IntegerLiteral> integer_reason) {
1253 tmp_cleaned_reason_.clear();
1255 DCHECK(!lit.IsAlwaysFalse());
1256 if (lit.IsAlwaysTrue())
continue;
1257 tmp_cleaned_reason_.push_back(lit);
1259 return Enqueue(i_lit, {}, tmp_cleaned_reason_);
1264 std::vector<IntegerLiteral>* integer_reason) {
1269 literal_reason->push_back(lit.
Negated());
1270 return Enqueue(i_lit, *literal_reason, *integer_reason);
1274 integer_reason->push_back(
1290 const auto [it, inserted] =
1291 conditional_lbs_.insert({{lit.
Index(), i_lit.
var}, i_lit.
bound});
1293 it->second = std::max(it->second, i_lit.
bound);
1299bool IntegerTrail::ReasonIsValid(
1300 absl::Span<const Literal> literal_reason,
1301 absl::Span<const IntegerLiteral> integer_reason) {
1303 for (
const Literal lit : literal_reason) {
1306 for (
const IntegerLiteral i_lit : integer_reason) {
1309 LOG(INFO) <<
"Reason has a constant false literal!";
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];
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++;
1329 for (
const IntegerLiteral i_lit : integer_reason) {
1332 num_literal_assigned_after_root_node++;
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"
1346bool IntegerTrail::ReasonIsValid(
1348 absl::Span<const IntegerLiteral> integer_reason) {
1349 if (!ReasonIsValid(literal_reason, integer_reason))
return false;
1350 if (debug_checker_ ==
nullptr)
return true;
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());
1357 if (!debug_checker_(clause, {i_lit})) {
1358 LOG(INFO) <<
"Invalid reason for loaded solution: " << i_lit <<
" "
1359 << literal_reason <<
" " << integer_reason;
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;
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());
1377 if (!debug_checker_(clause, {})) {
1378 LOG(INFO) <<
"Invalid reason for loaded solution: " << lit <<
" "
1379 << literal_reason <<
" " << integer_reason;
1386 Literal literal, absl::Span<const Literal> literal_reason,
1387 absl::Span<const IntegerLiteral> integer_reason) {
1388 EnqueueLiteralInternal(literal,
false, literal_reason, integer_reason);
1391void IntegerTrail::EnqueueLiteralInternal(
1392 Literal literal,
bool use_lazy_reason,
1393 absl::Span<const Literal> literal_reason,
1394 absl::Span<const IntegerLiteral> integer_reason) {
1396 DCHECK(!use_lazy_reason ||
1397 ReasonIsValid(literal, literal_reason, integer_reason));
1398 if (integer_search_levels_.empty()) {
1405 if (!integer_search_levels_.empty() && integer_reason.empty() &&
1406 literal_reason.empty() && !use_lazy_reason) {
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);
1415 const int reason_index =
1417 ? -
static_cast<int>(lazy_reasons_.size())
1418 : AppendReasonToInternalBuffers(literal_reason, integer_reason);
1419 boolean_trail_index_to_reason_index_[trail_index] = reason_index;
1428 if (parameters_.propagation_loop_detection_factor() == 0.0)
return false;
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);
1438 if (first_level_without_full_propagation_ == -1) {
1439 first_level_without_full_propagation_ = trail_->CurrentDecisionLevel();
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;
1453 vars.push_back(var);
1456 std::sort(vars.begin(), vars.end());
1457 IntegerVariable best_var = vars[0];
1460 for (
int i = 1;
i < vars.size(); ++
i) {
1461 if (vars[
i] != vars[
i - 1]) {
1465 if (count > best_count) {
1475 return first_level_without_full_propagation_ != -1;
1479 for (IntegerVariable var(0); var < var_lbs_.size(); var += 2) {
1480 if (!
IsFixed(var))
return var;
1485void IntegerTrail::CanonicalizeLiteralIfNeeded(
IntegerLiteral* i_lit) {
1487 const Domain& domain = (*domains_)[index];
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());
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());
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());
1517 return reason_index;
1520int64_t IntegerTrail::NextConflictId() {
1521 return sat_solver_->num_failures() + 1;
1524bool IntegerTrail::EnqueueInternal(
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);
1536 if (i_lit.bound <= var_lbs_[var])
return true;
1545 CanonicalizeLiteralIfNeeded(&i_lit);
1554 auto* conflict = InitializeConflict(i_lit, use_lazy_reason, literal_reason,
1557 const int trail_index = FindLowestTrailIndexThatExplainBound(ub_reason);
1558 if (trail_index >= 0) tmp_queue_.push_back(trail_index);
1560 MergeReasonIntoInternal(conflict, NextConflictId());
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();
1587 for (SparseBitset<IntegerVariable>* bitset : watchers_) {
1588 bitset->Set(i_lit.var);
1604 const LiteralIndex literal_index =
1605 encoder_->SearchForLiteralAtOrBefore(i_lit, &bound);
1606 int bool_index = -1;
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());
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,
1627 return EnqueueAssociatedIntegerLiteral(i_lit, to_enqueue);
1630 if (!trail_->Assignment().LiteralIsTrue(to_enqueue)) {
1631 if (integer_search_levels_.empty()) {
1632 trail_->EnqueueWithUnitReason(to_enqueue);
1637 bool_index = trail_->Index();
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;
1651 trail_->MutableConflict()->clear();
1656 DCHECK_GT(trail_->CurrentDecisionLevel(), 0);
1660 if (!integer_search_levels_.empty() && integer_reason.empty() &&
1661 literal_reason.empty() && !use_lazy_reason) {
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()) {
1670 AppendReasonToInternalBuffers(literal_reason, integer_reason);
1672 reason_index = integer_trail_[trail_index_with_same_reason].reason_index;
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);
1678 boolean_trail_index_to_reason_index_[bool_index] = reason_index;
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({i_lit.bound,
1692bool IntegerTrail::EnqueueAssociatedIntegerLiteral(
IntegerLiteral i_lit,
1694 DCHECK(ReasonIsValid(i_lit, {literal_reason.Negated()}, {}));
1697 if (i_lit.bound <= var_lbs_[i_lit.var])
return true;
1701 CanonicalizeLiteralIfNeeded(&i_lit);
1708 return Enqueue(i_lit, {literal_reason.Negated()}, {});
1712 for (SparseBitset<IntegerVariable>* bitset : watchers_) {
1713 bitset->Set(i_lit.var);
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;
1723 trail_->MutableConflict()->clear();
1728 DCHECK_GT(trail_->CurrentDecisionLevel(), 0);
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({i_lit.bound,
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_);
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_);
1755 const int cached_size = cached_sizes_[reason_index];
1756 if (cached_size == 0)
return {};
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);
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);
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) {
1777 FindLowestTrailIndexThatExplainBound(bounds_reason_buffer_[
i]);
1778 if (dep >= num_vars) {
1779 data[new_size++] = dep;
1782 cached_sizes_[reason_index] = new_size;
1783 if (new_size == 0)
return {};
1784 return absl::MakeSpan(data, new_size);
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);
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);
1813 std::vector<Literal> reason;
1819 std::vector<Literal>* output)
const {
1820 DCHECK(tmp_queue_.empty());
1821 const int num_vars = var_lbs_.size();
1823 if (literal.IsAlwaysTrue())
continue;
1824 const int trail_index = FindLowestTrailIndexThatExplainBound(literal);
1828 if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
1830 return MergeReasonIntoInternal(output, -1);
1835void IntegerTrail::MergeReasonIntoInternal(std::vector<Literal>* output,
1836 int64_t conflict_id)
const {
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());
1844 info_is_valid_on_subsequent_last_level_expansion_ =
true;
1845 if (conflict_id == -1 || last_conflict_id_ != conflict_id) {
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;
1852 to_clear_for_lower_level_.clear();
1855 const int last_decision_index =
1856 integer_search_levels_.empty() || conflict_id == -1
1858 : integer_search_levels_.back();
1861 for (
const Literal l : *output) {
1862 added_variables_.
Set(l.Variable());
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);
1877 std::make_heap(tmp_queue_.begin(), tmp_queue_.end());
1882 int64_t work_done = 0;
1883 while (!tmp_queue_.empty()) {
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();
1893 if (tmp_var_to_trail_index_in_queue_[entry.var] != trail_index) {
1908 tmp_var_to_trail_index_in_queue_[entry.var] = 0;
1909 has_dependency_ =
false;
1913 if (var_to_trail_index_at_lower_level_[entry.var] >= trail_index) {
1922 if (trail_index < last_decision_index) {
1923 tmp_seen_.push_back(trail_index);
1929 var_trail_index_cache_threshold_ = trail_index;
1934 const LiteralIndex associated_lit =
1936 IntegerVariable(entry.var), entry.bound));
1939 const int reason_index = integer_trail_[trail_index].reason_index;
1940 CHECK_GE(reason_index, 0);
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);
1953 CHECK_EQ(literals_reason_buffer_[start],
1954 Literal(associated_lit).Negated());
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);
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];
1979 const int index_in_queue =
1980 tmp_var_to_trail_index_in_queue_[next_entry.var];
1984 if (index_in_queue >= trail_index) {
1987 if (index_in_queue >= last_decision_index) {
1988 info_is_valid_on_subsequent_last_level_expansion_ =
false;
1993 if (next_trail_index <=
1994 var_to_trail_index_at_lower_level_[next_entry.var]) {
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());
2008 if (!has_dependency_) {
2009 tmp_to_clear_.push_back(entry.var);
2010 tmp_var_to_trail_index_in_queue_[entry.var] = trail_index;
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];
2021 to_clear_for_lower_level_.push_back(entry.var);
2023 var_to_trail_index_at_lower_level_[entry.var] =
2024 std::max(old, trail_index);
2030 for (
const IntegerVariable var : tmp_to_clear_) {
2031 tmp_var_to_trail_index_in_queue_[var] = 0;
2033 tmp_to_clear_.clear();
2035 time_limit_->AdvanceDeterministicTime(work_done * 5e-9);
2042 int64_t conflict_id)
const {
2044 added_variables_.ClearAndResize(BooleanVariable(trail_->NumVariables()));
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);
2054 MergeReasonIntoInternal(reason, conflict_id);
2065 int base_index, std::vector<IntegerLiteral>* output)
const {
2066 tmp_marked_.ClearAndResize(IntegerVariable(var_lbs_.size()));
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];
2073 if (tmp_marked_[entry.var])
continue;
2075 tmp_marked_.Set(entry.var);
2082 time_limit_(model->GetOrCreate<
TimeLimit>()),
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);
2098 var_to_watcher_.reserve(2 * num_vars);
2102 if (in_queue_[
id])
return;
2103 in_queue_[id] =
true;
2104 queue_by_priority_[id_to_priority_[id]].push_back(
id);
2107void GenericLiteralWatcher::UpdateCallingNeeds(
Trail* trail) {
2109 const int literal_limit = literal_to_watcher_.size();
2112 if (literal.
Index() >= literal_limit)
continue;
2113 for (
const auto entry : literal_to_watcher_[literal]) {
2115 if (entry.watch_index >= 0) {
2116 id_to_watch_indices_[entry.id].push_back(entry.watch_index);
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]) {
2127 if (entry.watch_index >= 0) {
2128 id_to_watch_indices_[entry.id].push_back(entry.watch_index);
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);
2141 modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
2149 for (
const int id : propagator_ids_to_call_at_level_zero_) {
2154 UpdateCallingNeeds(trail);
2158 int64_t num_propagate_calls = 0;
2159 const int64_t old_enqueue = integer_trail_->num_enqueues();
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 +
2170 for (
int priority = 0; priority < queue_by_priority_.size(); ++priority) {
2178 if (test_limit > 100) {
2180 if (time_limit_->LimitReached())
break;
2182 if (stop_propagation_callback_ !=
nullptr && stop_propagation_callback_()) {
2183 integer_trail_->NotifyThatPropagationWasAborted();
2187 std::deque<int>& queue = queue_by_priority_[priority];
2188 while (!queue.empty()) {
2189 const int id = queue.front();
2194 if (id_need_reversible_support_[
id]) {
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) {
2199 id_to_level_at_last_call_[id] = level;
2200 id_to_greatest_common_level_since_last_call_.MutableRef(IdType(
id)) =
2203 if (low < high) rev->SetLevel(low);
2204 if (level > low) rev->SetLevel(level);
2206 for (
int* rev_int : id_to_reversible_ints_[
id]) {
2207 rev_int_repository_->SaveState(rev_int);
2213 const int64_t old_integer_timestamp = integer_trail_->num_enqueues();
2214 const int64_t old_boolean_timestamp = trail->
Index();
2218 call_again_ =
false;
2221 ++num_propagate_calls;
2223 id_to_watch_indices_[id].empty()
2224 ? watchers_[id]->Propagate()
2225 : watchers_[id]->IncrementalPropagate(id_to_watch_indices_[
id]);
2227 id_to_watch_indices_[id].clear();
2228 in_queue_[id] =
false;
2234 if (id_to_idempotence_[
id]) {
2238 UpdateCallingNeeds(trail);
2239 id_to_watch_indices_[id].clear();
2240 in_queue_[id] =
false;
2245 id_to_watch_indices_[id].clear();
2246 in_queue_[id] =
false;
2247 UpdateCallingNeeds(trail);
2257 if (trail->
Index() > old_boolean_timestamp) {
2269 if (integer_trail_->num_enqueues() > old_integer_timestamp) {
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);
2284 modified_vars_for_callback_.ClearAndResize(
2285 integer_trail_->NumIntegerVariables());
2296 if (time_limit_->LimitReached())
return;
2306 for (
bool* to_reset : bool_to_reset_on_backtrack_) *to_reset =
false;
2307 bool_to_reset_on_backtrack_.clear();
2310 for (std::deque<int>& queue : queue_by_priority_) {
2311 for (
const int id : queue) {
2312 id_to_watch_indices_[id].clear();
2321 modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
2322 in_queue_.assign(watchers_.size(),
false);
2327 const int id = watchers_.size();
2328 watchers_.push_back(propagator);
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*>());
2336 id_to_watch_indices_.push_back(std::vector<int>());
2337 id_to_priority_.push_back(1);
2338 id_to_idempotence_.push_back(
true);
2347 in_queue_.push_back(
true);
2348 queue_by_priority_[1].push_back(
id);
2353 id_to_priority_[id] = priority;
2354 if (priority >= queue_by_priority_.size()) {
2355 queue_by_priority_.resize(priority + 1);
2361 id_to_idempotence_[id] =
false;
2365 propagator_ids_to_call_at_level_zero_.push_back(
id);
2370 id_need_reversible_support_[id] =
true;
2371 id_to_reversible_classes_[id].push_back(rev);
2375 id_need_reversible_support_[id] =
true;
2376 id_to_reversible_ints_[id].push_back(rev);
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)
void Set(IntegerType index)
bool Propagate(Trail *trail) final
void RegisterReversibleInt(int id, int *rev)
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
void Untrail(const Trail &trail, int literal_trail_index) final
void SetPropagatorPriority(int id, int priority)
void RegisterReversibleClass(int id, ReversibleInterface *rev)
void ReserveSpaceForNumVariables(int num_vars)
Memory optimization: you can call this before registering watchers.
int Register(PropagatorInterface *propagator)
Registers a propagator and returns its unique ids.
void CallOnNextPropagate(int id)
GenericLiteralWatcher(Model *model)
void AlwaysCallAtLevelZero(int id)
const std::vector< ValueLiteralPair > & FullDomainEncoding(IntegerVariable var) const
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit)
IntegerVariable GetLiteralView(Literal lit) const
void AddAllImplicationsBetweenAssociatedLiterals()
Literal GetFalseLiteral()
void FullyEncodeVariable(IntegerVariable var)
Literal GetTrueLiteral()
Gets the literal always set to true, make it if it does not exist.
bool VariableIsFullyEncoded(IntegerVariable var) const
bool IsFixedOrHasAssociatedLiteral(IntegerLiteral i_lit) const
const std::vector< ValueLiteralPair > & PartialDomainEncoding(IntegerVariable var) const
LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i_lit, IntegerValue *bound) const
void ReserveSpaceForNumVariables(int num_vars)
Memory optimization: you can call this before encoding variables.
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
ABSL_MUST_USE_RESULT bool LiteralOrNegationHasView(Literal lit, IntegerVariable *view=nullptr, bool *view_is_direct=nullptr) const
std::vector< ValueLiteralPair > PartialGreaterThanEncoding(IntegerVariable var) const
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
bool UpdateEncodingOnInitialDomainChange(IntegerVariable var, Domain domain)
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
void NotifyThatPropagationWasAborted()
ABSL_MUST_USE_RESULT bool ConditionalEnqueue(Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
void RemoveLevelZeroBounds(std::vector< IntegerLiteral > *reason) const
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
int NumConstantVariables() const
ABSL_MUST_USE_RESULT bool SafeEnqueue(IntegerLiteral i_lit, absl::Span< const IntegerLiteral > integer_reason)
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
IntegerValue UpperBound(IntegerVariable i) const
void AppendNewBoundsFrom(int base_index, std::vector< IntegerLiteral > *output) const
bool IntegerLiteralIsFalse(IntegerLiteral l) const
IntegerVariable AddIntegerVariable()
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
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.
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
bool InPropagationLoop() const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
bool IsFixed(IntegerVariable i) const
Checks if the variable is fixed.
IntegerVariable NumIntegerVariables() const
IntegerVariable NextVariableToBranchOnInPropagationLoop() const
ABSL_MUST_USE_RESULT bool RootLevelEnqueue(IntegerLiteral i_lit)
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
void MergeReasonInto(absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
const Domain & InitialVariableDomain(IntegerVariable var) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
void Untrail(const Trail &trail, int literal_trail_index) final
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit)
IntegerVariable FirstUnassignedVariable() const
void ReserveSpaceForNumVariables(int num_vars)
bool Propagate(Trail *trail) final
IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value)
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
bool CurrentBranchHadAnIncompletePropagation()
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
Base class for CP like propagators.
SatPropagator(const std::string &name)
int propagation_trail_index_
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
void AddLastPropagator(SatPropagator *propagator)
int NumVariables() const
Getters.
std::vector< Literal > * MutableConflict()
void EnqueueWithUnitReason(Literal true_literal)
Specific Enqueue() version for a fixed variable.
int CurrentDecisionLevel() const
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
const VariablesAssignment & Assignment() const
bool LiteralIsAssigned(Literal literal) const
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
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.
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
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)
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
std::vector< Literal > literal_to_fix
bool IsAlwaysFalse() const
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
IntegerLiteral Negated() const
The negation of x >= bound is x <= bound - 1.
std::string DebugString() const
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
bool IsAlwaysTrue() const
std::string DebugString() const