18 #include <type_traits>
28 const std::vector<IntegerVariable>& vars) {
29 std::vector<IntegerVariable> result(vars.size());
30 for (
int i = 0; i < vars.size(); ++i) {
42 <<
"Domain too large for full encoding.";
55 tmp_values_.push_back(v);
58 for (
const IntegerValue v : tmp_values_) {
70 if (
index >= is_fully_encoded_.
size())
return false;
73 if (is_fully_encoded_[
index])
return true;
80 const int64 initial_domain_size = (*domains_)[
var].Size();
81 if (equality_by_var_[
index].size() < initial_domain_size)
return false;
90 const auto& ref = equality_by_var_[
index];
94 if (i < ref.size() && v == ref[i].value) {
99 if (i == ref.size()) {
100 is_fully_encoded_[
index] =
true;
102 return is_fully_encoded_[
index];
105 std::vector<IntegerEncoder::ValueLiteralPair>
111 std::vector<IntegerEncoder::ValueLiteralPair>
115 if (
index >= equality_by_var_.size())
return {};
118 std::vector<ValueLiteralPair>& ref = equality_by_var_[
index];
119 for (
int i = 0; i < ref.size(); ++i) {
128 ref[new_size++] = pair;
130 ref.resize(new_size);
131 std::sort(ref.begin(), ref.end());
133 std::vector<IntegerEncoder::ValueLiteralPair> result = ref;
135 std::reverse(result.begin(), result.end());
144 void IntegerEncoder::AddImplications(
145 const std::map<IntegerValue, Literal>& map,
146 std::map<IntegerValue, Literal>::const_iterator it,
148 if (!add_implications_)
return;
154 if (after_it != map.end()) {
156 {after_it->second.Negated(), associated_lit});
160 if (it != map.begin()) {
164 {associated_lit.
Negated(), before_it->second});
170 add_implications_ =
true;
171 for (
const std::map<IntegerValue, Literal>& encoding : encoding_by_var_) {
173 for (
const auto value_literal : encoding) {
174 const Literal lit = value_literal.second;
179 previous = lit.
Index();
186 const IntegerVariable
var(i_lit.
var);
187 IntegerValue after(i_lit.
bound);
188 IntegerValue before(i_lit.
bound - 1);
193 if (before > previous && before <
interval.start) before = previous;
203 if (i_lit.
bound <= (*domains_)[i_lit.
var].Min()) {
206 if (i_lit.
bound > (*domains_)[i_lit.
var].Max()) {
218 ++num_created_variables_;
225 VLOG(1) <<
"Created a fixed literal for no reason!";
231 std::pair<PositiveOnlyIndex, IntegerValue> PositiveVarKey(IntegerVariable
var,
232 IntegerValue
value) {
239 IntegerVariable
var, IntegerValue
value)
const {
241 equality_to_associated_literal_.find(PositiveVarKey(
var,
value));
242 if (it != equality_to_associated_literal_.end()) {
243 return it->second.Index();
249 IntegerVariable
var, IntegerValue
value) {
252 equality_to_associated_literal_.find(PositiveVarKey(
var,
value));
253 if (it != equality_to_associated_literal_.end()) {
267 ++num_created_variables_;
277 VLOG(1) <<
"Created a fixed literal for no reason!";
284 const auto& domain = (*domains_)[i_lit.
var];
285 const IntegerValue
min(domain.Min());
286 const IntegerValue
max(domain.Max());
293 HalfAssociateGivenLiteral(pair.first,
literal);
294 HalfAssociateGivenLiteral(pair.second,
literal.Negated());
299 if (pair.first.bound ==
max) {
302 if (-pair.second.bound ==
min) {
310 IntegerValue
value) {
315 if (
value == 1 && domain.
Min() >= 0 && domain.
Max() <= 1) {
323 if (
value == -1 && domain.
Min() >= -1 && domain.
Max() <= 0) {
334 const auto insert_result = equality_to_associated_literal_.insert(
336 if (!insert_result.second) {
357 if (
index >= equality_by_var_.size()) {
358 equality_by_var_.resize(
index.value() + 1);
361 equality_by_var_[
index].push_back(
396 const int new_size = 1 +
literal.Index().value();
397 if (new_size > full_reverse_encoding_.
size()) {
398 full_reverse_encoding_.
resize(new_size);
408 void IntegerEncoder::HalfAssociateGivenLiteral(
IntegerLiteral i_lit,
411 const int new_size = 1 +
literal.Index().value();
412 if (new_size > reverse_encoding_.
size()) {
413 reverse_encoding_.
resize(new_size);
415 if (new_size > full_reverse_encoding_.
size()) {
416 full_reverse_encoding_.
resize(new_size);
420 if (i_lit.
var >= encoding_by_var_.size()) {
421 encoding_by_var_.resize(i_lit.
var.value() + 1);
423 auto& var_encoding = encoding_by_var_[i_lit.
var];
424 auto insert_result = var_encoding.insert({i_lit.
bound,
literal});
425 if (insert_result.second) {
426 AddImplications(var_encoding, insert_result.first,
literal);
429 newly_fixed_integer_literals_.push_back(i_lit);
437 const Literal associated(insert_result.first->second);
447 if (i.
var >= encoding_by_var_.size())
return false;
448 const std::map<IntegerValue, Literal>& encoding = encoding_by_var_[i.
var];
449 return encoding.find(i.
bound) != encoding.end();
454 const std::map<IntegerValue, Literal>& encoding = encoding_by_var_[i.
var];
455 const auto result = encoding.find(i.
bound);
457 return result->second.Index();
465 const std::map<IntegerValue, Literal>& encoding = encoding_by_var_[i.
var];
466 auto after_it = encoding.upper_bound(i.
bound);
469 *
bound = after_it->first;
470 return after_it->second.Index();
474 if (parameters_.log_search_progress() && num_decisions_to_break_loop_ > 0) {
475 LOG(
INFO) <<
"Num decisions to break propagation loop: "
476 << num_decisions_to_break_loop_;
487 if (level > integer_search_levels_.size()) {
488 integer_search_levels_.push_back(integer_trail_.size());
489 reason_decision_levels_.push_back(literals_reason_starts_.size());
495 var_to_current_lb_interval_index_.
SetLevel(level);
508 if (!
Enqueue(i_lit, {}, {}))
return false;
514 if (!
Enqueue(i_lit, {}, {}))
return false;
516 integer_literal_to_fix_.clear();
518 for (
const Literal lit : literal_to_fix_) {
523 literal_to_fix_.clear();
528 while (propagation_trail_index_ < trail->
Index()) {
534 if (!EnqueueAssociatedIntegerLiteral(i_lit,
literal)) {
546 var_to_current_lb_interval_index_.
SetLevel(level);
550 if (level < first_level_without_full_propagation_) {
551 first_level_without_full_propagation_ = -1;
556 if (level >= integer_search_levels_.size())
return;
557 const int target = integer_search_levels_[level];
558 integer_search_levels_.resize(level);
560 CHECK_LE(target, integer_trail_.size());
562 for (
int index = integer_trail_.size() - 1;
index >= target; --
index) {
563 const TrailEntry& entry = integer_trail_[
index];
564 if (entry.var < 0)
continue;
565 vars_[entry.var].current_trail_index = entry.prev_trail_index;
566 vars_[entry.var].current_bound =
567 integer_trail_[entry.prev_trail_index].bound;
569 integer_trail_.resize(target);
572 const int old_size = reason_decision_levels_[level];
573 reason_decision_levels_.resize(level);
574 if (old_size < literals_reason_starts_.size()) {
575 literals_reason_buffer_.resize(literals_reason_starts_[old_size]);
577 const int bound_start = bounds_reason_starts_[old_size];
578 bounds_reason_buffer_.resize(bound_start);
579 if (bound_start < trail_index_reason_buffer_.size()) {
580 trail_index_reason_buffer_.resize(bound_start);
583 literals_reason_starts_.resize(old_size);
584 bounds_reason_starts_.resize(old_size);
594 const int size = 2 * num_vars;
596 is_ignored_literals_.
reserve(size);
597 integer_trail_.reserve(size);
599 var_trail_index_cache_.
reserve(size);
600 tmp_var_to_trail_index_in_queue_.
reserve(size);
604 IntegerValue upper_bound) {
609 DCHECK(integer_search_levels_.empty());
612 const IntegerVariable i(vars_.
size());
614 vars_.
push_back({lower_bound,
static_cast<int>(integer_trail_.size())});
615 integer_trail_.push_back({lower_bound, i});
623 vars_.
push_back({-upper_bound,
static_cast<int>(integer_trail_.size())});
624 integer_trail_.push_back({-upper_bound,
NegationOf(i)});
625 domains_->
push_back(
Domain(-upper_bound.value(), -lower_bound.value()));
627 var_trail_index_cache_.
resize(vars_.
size(), integer_trail_.size());
628 tmp_var_to_trail_index_in_queue_.
resize(vars_.
size(), 0);
639 IntegerValue(domain.
Max()));
645 return (*domains_)[
var];
653 if (old_domain == domain)
return true;
655 if (domain.
IsEmpty())
return false;
656 (*domains_)[
var] = domain;
659 var_to_current_lb_interval_index_.
Set(
var, 0);
678 if (i == domain.
NumIntervals() || pair.value < domain[i].start) {
688 <<
"Domain intersection fixed " << num_fixed
689 <<
" equality literal corresponding to values outside the new domain.";
696 IntegerValue
value) {
700 insert.first->second = new_var;
707 return insert.first->second;
713 return (constant_map_.size() + 1) / 2;
717 int threshold)
const {
721 const int index_in_queue = tmp_var_to_trail_index_in_queue_[
var];
722 if (threshold <= index_in_queue) {
723 if (index_in_queue !=
kint32max) has_dependency_ =
true;
728 int trail_index = vars_[
var].current_trail_index;
731 if (trail_index > threshold) {
732 const int cached_index = var_trail_index_cache_[
var];
733 if (cached_index >= threshold && cached_index < trail_index &&
734 integer_trail_[cached_index].
var ==
var) {
735 trail_index = cached_index;
739 while (trail_index >= threshold) {
740 trail_index = integer_trail_[trail_index].prev_trail_index;
741 if (trail_index >= var_trail_index_cache_threshold_) {
742 var_trail_index_cache_[
var] = trail_index;
746 const int num_vars = vars_.
size();
747 return trail_index < num_vars ? -1 : trail_index;
750 int IntegerTrail::FindLowestTrailIndexThatExplainBound(
754 int trail_index = vars_[i_lit.
var].current_trail_index;
762 const int cached_index = var_trail_index_cache_[i_lit.
var];
763 if (cached_index < trail_index) {
764 const TrailEntry& entry = integer_trail_[cached_index];
765 if (entry.var == i_lit.
var && entry.bound >= i_lit.
bound) {
766 trail_index = cached_index;
771 int prev_trail_index = trail_index;
773 if (trail_index >= var_trail_index_cache_threshold_) {
774 var_trail_index_cache_[i_lit.
var] = trail_index;
776 const TrailEntry& entry = integer_trail_[trail_index];
777 if (entry.bound == i_lit.
bound)
return trail_index;
778 if (entry.bound < i_lit.
bound)
return prev_trail_index;
779 prev_trail_index = trail_index;
780 trail_index = entry.prev_trail_index;
786 IntegerValue slack, absl::Span<const IntegerValue> coeffs,
787 std::vector<IntegerLiteral>* reason)
const {
789 if (slack == 0)
return;
790 const int size = reason->size();
791 tmp_indices_.resize(size);
792 for (
int i = 0; i < size; ++i) {
795 tmp_indices_[i] = vars_[(*reason)[i].var].current_trail_index;
801 for (
const int i : tmp_indices_) {
803 integer_trail_[i].
bound));
808 IntegerValue slack, absl::Span<const IntegerValue> coeffs,
809 absl::Span<const IntegerVariable> vars,
810 std::vector<IntegerLiteral>* reason)
const {
811 tmp_indices_.clear();
812 for (
const IntegerVariable
var : vars) {
813 tmp_indices_.push_back(vars_[
var].current_trail_index);
816 for (
const int i : tmp_indices_) {
818 integer_trail_[i].
bound));
823 absl::Span<const IntegerValue> coeffs,
824 std::vector<int>* trail_indices)
const {
826 DCHECK(relax_heap_.empty());
833 const int size = coeffs.size();
834 const int num_vars = vars_.
size();
835 for (
int i = 0; i < size; ++i) {
836 const int index = (*trail_indices)[i];
839 if (
index < num_vars)
continue;
842 const IntegerValue coeff = coeffs[i];
844 (*trail_indices)[new_size++] =
index;
851 const TrailEntry& entry = integer_trail_[
index];
853 index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
854 (*trail_indices)[new_size++] =
index;
859 const TrailEntry& previous_entry = integer_trail_[entry.prev_trail_index];
861 CapProd(coeff.value(), (entry.bound - previous_entry.bound).value());
863 (*trail_indices)[new_size++] =
index;
867 relax_heap_.push_back({
index, coeff, diff});
869 trail_indices->resize(new_size);
870 std::make_heap(relax_heap_.begin(), relax_heap_.end());
872 while (slack > 0 && !relax_heap_.empty()) {
873 const RelaxHeapEntry heap_entry = relax_heap_.front();
874 std::pop_heap(relax_heap_.begin(), relax_heap_.end());
875 relax_heap_.pop_back();
878 if (heap_entry.diff > slack) {
879 trail_indices->push_back(heap_entry.index);
884 slack -= heap_entry.diff;
885 const int index = integer_trail_[heap_entry.index].prev_trail_index;
888 if (
index < num_vars)
continue;
889 if (heap_entry.coeff > slack) {
890 trail_indices->push_back(
index);
893 const TrailEntry& entry = integer_trail_[
index];
895 index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
896 trail_indices->push_back(
index);
900 const TrailEntry& previous_entry = integer_trail_[entry.prev_trail_index];
902 (entry.bound - previous_entry.bound).value());
904 trail_indices->push_back(
index);
907 relax_heap_.push_back({
index, heap_entry.coeff, diff});
908 std::push_heap(relax_heap_.begin(), relax_heap_.end());
913 for (
const RelaxHeapEntry& entry : relax_heap_) {
914 trail_indices->push_back(entry.index);
920 std::vector<IntegerLiteral>* reason)
const {
924 (*reason)[new_size++] =
literal;
926 reason->resize(new_size);
929 std::vector<Literal>* IntegerTrail::InitializeConflict(
930 IntegerLiteral integer_literal,
const LazyReasonFunction& lazy_reason,
931 absl::Span<const Literal> literals_reason,
932 absl::Span<const IntegerLiteral> bounds_reason) {
933 DCHECK(tmp_queue_.empty());
935 if (lazy_reason ==
nullptr) {
936 conflict->assign(literals_reason.begin(), literals_reason.end());
937 const int num_vars = vars_.
size();
939 const int trail_index = FindLowestTrailIndexThatExplainBound(
literal);
940 if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
945 lazy_reason(integer_literal, integer_trail_.size(), conflict, &tmp_queue_);
952 std::string ReasonDebugString(absl::Span<const Literal> literal_reason,
953 absl::Span<const IntegerLiteral> integer_reason) {
954 std::string result =
"literals:{";
955 for (
const Literal l : literal_reason) {
956 if (result.back() !=
'{') result +=
",";
957 result += l.DebugString();
959 result +=
"} bounds:{";
960 for (
const IntegerLiteral l : integer_reason) {
961 if (result.back() !=
'{') result +=
",";
962 result += l.DebugString();
970 std::string IntegerTrail::DebugString() {
971 std::string result =
"trail:{";
972 const int num_vars = vars_.
size();
974 std::min(num_vars + 30,
static_cast<int>(integer_trail_.size()));
975 for (
int i = num_vars; i < limit; ++i) {
976 if (result.back() !=
'{') result +=
",";
979 integer_trail_[i].
bound)
982 if (limit < integer_trail_.size()) {
990 absl::Span<const Literal> literal_reason,
991 absl::Span<const IntegerLiteral> integer_reason) {
992 return EnqueueInternal(i_lit,
nullptr, literal_reason, integer_reason,
993 integer_trail_.size());
998 std::vector<IntegerLiteral>* integer_reason) {
1006 return Enqueue(i_lit, *literal_reason, *integer_reason);
1010 literal_reason->push_back(lit.
Negated());
1011 return Enqueue(i_lit, *literal_reason, *integer_reason);
1015 integer_reason->push_back(
1026 absl::Span<const Literal> literal_reason,
1027 absl::Span<const IntegerLiteral> integer_reason,
1028 int trail_index_with_same_reason) {
1029 return EnqueueInternal(i_lit,
nullptr, literal_reason, integer_reason,
1030 trail_index_with_same_reason);
1035 return EnqueueInternal(i_lit, lazy_reason, {}, {}, integer_trail_.size());
1038 bool IntegerTrail::ReasonIsValid(
1039 absl::Span<const Literal> literal_reason,
1040 absl::Span<const IntegerLiteral> integer_reason) {
1042 for (
const Literal lit : literal_reason) {
1045 for (
const IntegerLiteral i_lit : integer_reason) {
1046 if (i_lit.
bound > vars_[i_lit.
var].current_bound) {
1049 LOG(
INFO) <<
"Reason " << i_lit <<
" is not true!"
1050 <<
" optional variable:" << i_lit.
var
1053 <<
" current_lb:" << vars_[i_lit.
var].current_bound;
1055 LOG(
INFO) <<
"Reason " << i_lit <<
" is not true!"
1056 <<
" non-optional variable:" << i_lit.
var
1057 <<
" current_lb:" << vars_[i_lit.
var].current_bound;
1065 if (!integer_search_levels_.empty()) {
1066 int num_literal_assigned_after_root_node = 0;
1067 for (
const Literal lit : literal_reason) {
1068 if (trail_->
Info(lit.Variable()).
level > 0) {
1069 num_literal_assigned_after_root_node++;
1072 for (
const IntegerLiteral i_lit : integer_reason) {
1074 num_literal_assigned_after_root_node++;
1077 DLOG_IF(
INFO, num_literal_assigned_after_root_node == 0)
1078 <<
"Propagating a literal with no reason at a positive level!\n"
1079 <<
"level:" << integer_search_levels_.size() <<
" "
1080 << ReasonDebugString(literal_reason, integer_reason) <<
"\n"
1089 absl::Span<const IntegerLiteral> integer_reason) {
1090 EnqueueLiteralInternal(
literal,
nullptr, literal_reason, integer_reason);
1093 void IntegerTrail::EnqueueLiteralInternal(
1095 absl::Span<const Literal> literal_reason,
1096 absl::Span<const IntegerLiteral> integer_reason) {
1098 DCHECK(lazy_reason !=
nullptr ||
1099 ReasonIsValid(literal_reason, integer_reason));
1100 if (integer_search_levels_.empty()) {
1107 if (!integer_search_levels_.empty() && integer_reason.empty() &&
1108 literal_reason.empty() && lazy_reason ==
nullptr) {
1109 literal_to_fix_.push_back(
literal);
1112 const int trail_index = trail_->
Index();
1113 if (trail_index >= boolean_trail_index_to_integer_one_.size()) {
1114 boolean_trail_index_to_integer_one_.resize(trail_index + 1);
1116 boolean_trail_index_to_integer_one_[trail_index] = integer_trail_.size();
1118 int reason_index = literals_reason_starts_.size();
1119 if (lazy_reason !=
nullptr) {
1120 if (integer_trail_.size() >= lazy_reasons_.size()) {
1121 lazy_reasons_.resize(integer_trail_.size() + 1,
nullptr);
1123 lazy_reasons_[integer_trail_.size()] = lazy_reason;
1127 literals_reason_starts_.push_back(literals_reason_buffer_.size());
1128 literals_reason_buffer_.insert(literals_reason_buffer_.end(),
1129 literal_reason.begin(),
1130 literal_reason.end());
1131 bounds_reason_starts_.push_back(bounds_reason_buffer_.size());
1132 bounds_reason_buffer_.insert(bounds_reason_buffer_.end(),
1133 integer_reason.begin(), integer_reason.end());
1136 integer_trail_.push_back({IntegerValue(0),
1148 const int num_vars = vars_.
size();
1149 return (!integer_search_levels_.empty() &&
1150 integer_trail_.size() - integer_search_levels_.back() >
1152 parameters_.search_branching() != SatParameters::FIXED_SEARCH);
1159 ++num_decisions_to_break_loop_;
1160 std::vector<IntegerVariable> vars;
1161 for (
int i = integer_search_levels_.back(); i < integer_trail_.size(); ++i) {
1162 const IntegerVariable
var = integer_trail_[i].var;
1165 vars.push_back(
var);
1168 std::sort(vars.begin(), vars.end());
1169 IntegerVariable best_var = vars[0];
1172 for (
int i = 1; i < vars.size(); ++i) {
1173 if (vars[i] != vars[i - 1]) {
1177 if (count > best_count) {
1187 return first_level_without_full_propagation_ != -1;
1191 for (IntegerVariable
var(0);
var < vars_.
size();
var += 2) {
1198 bool IntegerTrail::EnqueueInternal(
1200 absl::Span<const Literal> literal_reason,
1201 absl::Span<const IntegerLiteral> integer_reason,
1202 int trail_index_with_same_reason) {
1203 DCHECK(lazy_reason !=
nullptr ||
1204 ReasonIsValid(literal_reason, integer_reason));
1206 const IntegerVariable
var(i_lit.
var);
1214 if (i_lit.
bound <= vars_[
var].current_bound)
return true;
1223 if ((*domains_)[
var].NumIntervals() > 1) {
1224 const auto& domain = (*domains_)[
var];
1226 const int size = domain.NumIntervals();
1227 while (index < size && i_lit.bound > domain[
index].end) {
1230 if (
index == size) {
1233 var_to_current_lb_interval_index_.
Set(
var,
index);
1244 Literal(is_ignored_literals_[
var]))) {
1247 auto* conflict = InitializeConflict(i_lit, lazy_reason, literal_reason,
1250 conflict->push_back(Literal(is_ignored_literals_[
var]));
1253 const int trail_index = FindLowestTrailIndexThatExplainBound(ub_reason);
1254 const int num_vars = vars_.
size();
1255 if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
1257 MergeReasonIntoInternal(conflict);
1264 const Literal is_ignored = Literal(is_ignored_literals_[
var]);
1265 if (integer_search_levels_.empty()) {
1272 if (lazy_reason !=
nullptr) {
1273 lazy_reason(i_lit, integer_trail_.size(), &lazy_reason_literals_,
1274 &lazy_reason_trail_indices_);
1275 std::vector<IntegerLiteral> temp;
1276 for (
const int trail_index : lazy_reason_trail_indices_) {
1277 const TrailEntry& entry = integer_trail_[trail_index];
1278 temp.push_back(IntegerLiteral(entry.var, entry.bound));
1286 bounds_reason_buffer_.push_back(ub_reason);
1306 if (i_lit.
bound - lb < (ub - lb) / 2) {
1307 if (first_level_without_full_propagation_ == -1) {
1315 for (SparseBitset<IntegerVariable>* bitset : watchers_) {
1316 bitset->Set(i_lit.
var);
1319 if (!integer_search_levels_.empty() && integer_reason.empty() &&
1320 literal_reason.empty() && lazy_reason ==
nullptr &&
1321 trail_index_with_same_reason >= integer_trail_.size()) {
1322 integer_literal_to_fix_.push_back(i_lit);
1338 const LiteralIndex literal_index =
1341 const Literal to_enqueue = Literal(literal_index);
1343 auto* conflict = InitializeConflict(i_lit, lazy_reason, literal_reason,
1345 conflict->push_back(to_enqueue);
1346 MergeReasonIntoInternal(conflict);
1356 EnqueueLiteralInternal(to_enqueue, lazy_reason, literal_reason,
1359 return EnqueueAssociatedIntegerLiteral(i_lit, to_enqueue);
1363 if (integer_search_levels_.empty()) {
1369 const int trail_index = trail_->
Index();
1370 if (trail_index >= boolean_trail_index_to_integer_one_.size()) {
1371 boolean_trail_index_to_integer_one_.resize(trail_index + 1);
1373 boolean_trail_index_to_integer_one_[trail_index] =
1374 trail_index_with_same_reason;
1381 if (integer_search_levels_.empty()) {
1382 ++num_level_zero_enqueues_;
1383 vars_[i_lit.
var].current_bound = i_lit.
bound;
1384 integer_trail_[i_lit.
var.value()].bound = i_lit.
bound;
1395 int reason_index = literals_reason_starts_.size();
1396 if (lazy_reason !=
nullptr) {
1397 if (integer_trail_.size() >= lazy_reasons_.size()) {
1398 lazy_reasons_.resize(integer_trail_.size() + 1,
nullptr);
1400 lazy_reasons_[integer_trail_.size()] = lazy_reason;
1402 }
else if (trail_index_with_same_reason >= integer_trail_.size()) {
1404 literals_reason_starts_.push_back(literals_reason_buffer_.size());
1405 if (!literal_reason.empty()) {
1406 literals_reason_buffer_.insert(literals_reason_buffer_.end(),
1407 literal_reason.begin(),
1408 literal_reason.end());
1410 bounds_reason_starts_.push_back(bounds_reason_buffer_.size());
1411 if (!integer_reason.empty()) {
1412 bounds_reason_buffer_.insert(bounds_reason_buffer_.end(),
1413 integer_reason.begin(),
1414 integer_reason.end());
1417 reason_index = integer_trail_[trail_index_with_same_reason].reason_index;
1420 const int prev_trail_index = vars_[i_lit.
var].current_trail_index;
1421 integer_trail_.push_back({i_lit.
bound,
1426 vars_[i_lit.
var].current_bound = i_lit.
bound;
1427 vars_[i_lit.
var].current_trail_index = integer_trail_.size() - 1;
1431 bool IntegerTrail::EnqueueAssociatedIntegerLiteral(IntegerLiteral i_lit,
1432 Literal literal_reason) {
1433 DCHECK(ReasonIsValid({literal_reason.Negated()}, {}));
1437 if (i_lit.bound <= vars_[i_lit.var].current_bound)
return true;
1445 return Enqueue(i_lit, {literal_reason.Negated()}, {});
1449 for (SparseBitset<IntegerVariable>* bitset : watchers_) {
1450 bitset->Set(i_lit.var);
1454 if (integer_search_levels_.empty()) {
1455 vars_[i_lit.var].current_bound = i_lit.bound;
1456 integer_trail_[i_lit.var.value()].bound = i_lit.bound;
1467 const int reason_index = literals_reason_starts_.size();
1468 CHECK_EQ(reason_index, bounds_reason_starts_.size());
1469 literals_reason_starts_.push_back(literals_reason_buffer_.size());
1470 bounds_reason_starts_.push_back(bounds_reason_buffer_.size());
1471 literals_reason_buffer_.push_back(literal_reason.Negated());
1473 const int prev_trail_index = vars_[i_lit.var].current_trail_index;
1474 integer_trail_.push_back({i_lit.bound,
1479 vars_[i_lit.var].current_bound = i_lit.bound;
1480 vars_[i_lit.var].current_trail_index = integer_trail_.size() - 1;
1484 void IntegerTrail::ComputeLazyReasonIfNeeded(
int trail_index)
const {
1485 const int reason_index = integer_trail_[trail_index].reason_index;
1486 if (reason_index == -1) {
1487 const TrailEntry& entry = integer_trail_[trail_index];
1488 const IntegerLiteral
literal(entry.var, entry.bound);
1489 lazy_reasons_[trail_index](
literal, trail_index, &lazy_reason_literals_,
1490 &lazy_reason_trail_indices_);
1494 absl::Span<const int> IntegerTrail::Dependencies(
int trail_index)
const {
1495 const int reason_index = integer_trail_[trail_index].reason_index;
1496 if (reason_index == -1) {
1497 return absl::Span<const int>(lazy_reason_trail_indices_);
1500 const int start = bounds_reason_starts_[reason_index];
1501 const int end = reason_index + 1 < bounds_reason_starts_.size()
1502 ? bounds_reason_starts_[reason_index + 1]
1503 : bounds_reason_buffer_.size();
1504 if (start == end)
return {};
1511 if (end > trail_index_reason_buffer_.size()) {
1512 trail_index_reason_buffer_.resize(end, -1);
1514 if (trail_index_reason_buffer_[start] == -1) {
1515 int new_end = start;
1516 const int num_vars = vars_.
size();
1517 for (
int i = start; i < end; ++i) {
1519 FindLowestTrailIndexThatExplainBound(bounds_reason_buffer_[i]);
1520 if (dep >= num_vars) {
1521 trail_index_reason_buffer_[new_end++] = dep;
1524 return absl::Span<const int>(&trail_index_reason_buffer_[start],
1530 return absl::Span<const int>(&trail_index_reason_buffer_[start],
1535 void IntegerTrail::AppendLiteralsReason(
int trail_index,
1536 std::vector<Literal>* output)
const {
1538 const int reason_index = integer_trail_[trail_index].reason_index;
1539 if (reason_index == -1) {
1540 for (
const Literal l : lazy_reason_literals_) {
1541 if (!added_variables_[l.Variable()]) {
1542 added_variables_.
Set(l.Variable());
1543 output->push_back(l);
1549 const int start = literals_reason_starts_[reason_index];
1550 const int end = reason_index + 1 < literals_reason_starts_.size()
1551 ? literals_reason_starts_[reason_index + 1]
1552 : literals_reason_buffer_.size();
1553 for (
int i = start; i < end; ++i) {
1554 const Literal l = literals_reason_buffer_[i];
1555 if (!added_variables_[l.Variable()]) {
1556 added_variables_.
Set(l.Variable());
1557 output->push_back(l);
1563 std::vector<Literal> reason;
1571 std::vector<Literal>* output)
const {
1572 DCHECK(tmp_queue_.empty());
1573 const int num_vars = vars_.
size();
1575 const int trail_index = FindLowestTrailIndexThatExplainBound(
literal);
1579 if (trail_index >= num_vars) tmp_queue_.push_back(trail_index);
1581 return MergeReasonIntoInternal(output);
1586 void IntegerTrail::MergeReasonIntoInternal(std::vector<Literal>* output)
const {
1589 DCHECK(std::all_of(tmp_var_to_trail_index_in_queue_.
begin(),
1590 tmp_var_to_trail_index_in_queue_.
end(),
1591 [](
int v) { return v == 0; }));
1594 for (
const Literal l : *output) {
1595 added_variables_.
Set(l.Variable());
1600 for (
const int trail_index : tmp_queue_) {
1602 DCHECK_LT(trail_index, integer_trail_.size());
1603 const TrailEntry& entry = integer_trail_[trail_index];
1604 tmp_var_to_trail_index_in_queue_[entry.var] =
1605 std::max(tmp_var_to_trail_index_in_queue_[entry.var], trail_index);
1610 std::make_heap(tmp_queue_.begin(), tmp_queue_.end());
1615 tmp_to_clear_.clear();
1616 while (!tmp_queue_.empty()) {
1617 const int trail_index = tmp_queue_.front();
1618 const TrailEntry& entry = integer_trail_[trail_index];
1619 std::pop_heap(tmp_queue_.begin(), tmp_queue_.end());
1620 tmp_queue_.pop_back();
1625 if (tmp_var_to_trail_index_in_queue_[entry.var] != trail_index) {
1632 var_trail_index_cache_threshold_ = trail_index;
1637 const LiteralIndex associated_lit =
1639 IntegerVariable(entry.var), entry.bound));
1642 const int reason_index = integer_trail_[trail_index].reason_index;
1645 const int start = literals_reason_starts_[reason_index];
1646 const int end = reason_index + 1 < literals_reason_starts_.size()
1647 ? literals_reason_starts_[reason_index + 1]
1648 : literals_reason_buffer_.size();
1650 CHECK_EQ(literals_reason_buffer_[start],
1651 Literal(associated_lit).Negated());
1654 const int start = bounds_reason_starts_[reason_index];
1655 const int end = reason_index + 1 < bounds_reason_starts_.size()
1656 ? bounds_reason_starts_[reason_index + 1]
1657 : bounds_reason_buffer_.size();
1671 tmp_var_to_trail_index_in_queue_[entry.var] = 0;
1672 has_dependency_ =
false;
1674 ComputeLazyReasonIfNeeded(trail_index);
1675 AppendLiteralsReason(trail_index, output);
1676 for (
const int next_trail_index : Dependencies(trail_index)) {
1677 if (next_trail_index < 0)
break;
1678 DCHECK_LT(next_trail_index, trail_index);
1679 const TrailEntry& next_entry = integer_trail_[next_trail_index];
1685 const int index_in_queue =
1686 tmp_var_to_trail_index_in_queue_[next_entry.var];
1687 if (index_in_queue !=
kint32max) has_dependency_ =
true;
1688 if (next_trail_index > index_in_queue) {
1689 tmp_var_to_trail_index_in_queue_[next_entry.var] = next_trail_index;
1691 std::push_heap(tmp_queue_.begin(), tmp_queue_.end());
1696 if (!has_dependency_) {
1697 tmp_to_clear_.push_back(entry.var);
1698 tmp_var_to_trail_index_in_queue_[entry.var] =
kint32max;
1703 for (
const IntegerVariable
var : tmp_to_clear_) {
1704 tmp_var_to_trail_index_in_queue_[
var] = 0;
1709 int trail_index)
const {
1710 const int index = boolean_trail_index_to_integer_one_[trail_index];
1714 ComputeLazyReasonIfNeeded(
index);
1715 AppendLiteralsReason(
index, reason);
1716 DCHECK(tmp_queue_.empty());
1717 for (
const int prev_trail_index : Dependencies(
index)) {
1718 if (prev_trail_index < 0)
break;
1720 tmp_queue_.push_back(prev_trail_index);
1722 MergeReasonIntoInternal(reason);
1732 const int end = vars_.
size();
1733 for (
int i = integer_trail_.size(); --i >= end;) {
1734 const TrailEntry& entry = integer_trail_[i];
1736 if (tmp_marked_[entry.var])
continue;
1738 tmp_marked_.
Set(entry.var);
1755 &id_to_greatest_common_level_since_last_call_);
1757 queue_by_priority_.resize(2);
1760 void GenericLiteralWatcher::UpdateCallingNeeds(
Trail* trail) {
1762 while (propagation_trail_index_ < trail->
Index()) {
1764 if (
literal.Index() >= literal_to_watcher_.
size())
continue;
1765 for (
const auto entry : literal_to_watcher_[
literal.Index()]) {
1766 if (!in_queue_[entry.id]) {
1767 in_queue_[entry.id] =
true;
1768 queue_by_priority_[id_to_priority_[entry.id]].push_back(entry.id);
1770 if (entry.watch_index >= 0) {
1771 id_to_watch_indices_[entry.id].push_back(entry.watch_index);
1778 if (
var.value() >= var_to_watcher_.
size())
continue;
1779 for (
const auto entry : var_to_watcher_[
var]) {
1780 if (!in_queue_[entry.id]) {
1781 in_queue_[entry.id] =
true;
1782 queue_by_priority_[id_to_priority_[entry.id]].push_back(entry.id);
1784 if (entry.watch_index >= 0) {
1785 id_to_watch_indices_[entry.id].push_back(entry.watch_index);
1791 const std::vector<IntegerVariable>& modified_vars =
1793 for (
const auto&
callback : level_zero_modified_variable_callback_) {
1806 for (
const int id : propagator_ids_to_call_at_level_zero_) {
1807 if (in_queue_[
id])
continue;
1808 in_queue_[id] =
true;
1809 queue_by_priority_[id_to_priority_[id]].push_back(
id);
1813 UpdateCallingNeeds(trail);
1818 for (
int priority = 0; priority < queue_by_priority_.size(); ++priority) {
1825 if (test_limit > 100) {
1830 std::deque<int>& queue = queue_by_priority_[priority];
1831 while (!queue.empty()) {
1832 const int id = queue.front();
1840 id_to_greatest_common_level_since_last_call_[IdType(
id)];
1841 const int high = id_to_level_at_last_call_[id];
1842 if (low < high || level > low) {
1843 id_to_level_at_last_call_[id] = level;
1844 id_to_greatest_common_level_since_last_call_.
MutableRef(IdType(
id)) =
1847 if (low < high) rev->SetLevel(low);
1848 if (level > low) rev->SetLevel(level);
1850 for (
int* rev_int : id_to_reversible_ints_[
id]) {
1851 rev_int_repository_->
SaveState(rev_int);
1858 const int64 old_boolean_timestamp = trail->
Index();
1861 std::vector<int>& watch_indices_ref = id_to_watch_indices_[id];
1863 watch_indices_ref.empty()
1864 ? watchers_[id]->Propagate()
1865 : watchers_[id]->IncrementalPropagate(watch_indices_ref);
1867 watch_indices_ref.clear();
1868 in_queue_[id] =
false;
1874 if (id_to_idempotence_[
id]) {
1878 UpdateCallingNeeds(trail);
1879 watch_indices_ref.clear();
1880 in_queue_[id] =
false;
1885 watch_indices_ref.clear();
1886 in_queue_[id] =
false;
1887 UpdateCallingNeeds(trail);
1893 if (trail->
Index() > old_boolean_timestamp) {
1905 if (integer_trail_->
num_enqueues() > old_integer_timestamp) {
1923 for (std::deque<int>& queue : queue_by_priority_) {
1924 for (
const int id : queue) {
1925 id_to_watch_indices_[id].clear();
1935 in_queue_.assign(watchers_.size(),
false);
1940 const int id = watchers_.size();
1941 watchers_.push_back(propagator);
1942 id_to_level_at_last_call_.push_back(0);
1943 id_to_greatest_common_level_since_last_call_.
GrowByOne();
1944 id_to_reversible_classes_.push_back(std::vector<ReversibleInterface*>());
1945 id_to_reversible_ints_.push_back(std::vector<int*>());
1946 id_to_watch_indices_.push_back(std::vector<int>());
1947 id_to_priority_.push_back(1);
1948 id_to_idempotence_.push_back(
true);
1957 in_queue_.push_back(
true);
1958 queue_by_priority_[1].push_back(
id);
1963 id_to_priority_[id] = priority;
1964 if (priority >= queue_by_priority_.size()) {
1965 queue_by_priority_.resize(priority + 1);
1971 id_to_idempotence_[id] =
false;
1975 propagator_ids_to_call_at_level_zero_.push_back(
id);
1980 id_to_reversible_classes_[id].push_back(rev);
1984 id_to_reversible_ints_[id].push_back(rev);
1988 std::function<void(
Model*)>
1996 std::vector<Literal> clause_to_exclude_solution;
1997 clause_to_exclude_solution.reserve(current_level);
1998 for (
int i = 0; i < current_level; ++i) {
1999 bool include_decision =
true;
2005 encoder->GetIntegerLiterals(decision);
2007 if (integer_trail->IsCurrentlyIgnored(
bound.var)) {
2013 clause_to_exclude_solution.push_back(
2014 integer_trail->IsIgnoredLiteral(
bound.var).Negated());
2015 include_decision =
false;
2019 if (include_decision) {
2020 clause_to_exclude_solution.push_back(decision.
Negated());
#define DLOG_IF(severity, condition)
#define DCHECK_LE(val1, val2)
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define DCHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define CHECK_LE(val1, val2)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
void resize(size_type new_size)
void reserve(size_type n)
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
Domain Negation() const
Returns {x ∈ Int64, ∃ e ∈ D, x = -e}.
absl::InlinedVector< ClosedInterval, 1 >::const_iterator end() const
int NumIntervals() const
Basic read-only std::vector<> wrapping to view a Domain as a sorted list of non-adjacent intervals.
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
bool IsEmpty() const
Returns true if this is the empty set.
bool Contains(int64 value) const
Returns true iff value is in Domain.
void Set(key_type key, mapped_type value)
void SetLevel(int level) final
const mapped_type & FindOrDie(key_type key) const
void SaveState(T *object)
T & MutableRef(IndexType index)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
void Set(IntegerType index)
void ClearAndResize(IntegerType size)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
bool Propagate(Trail *trail) final
void AlwaysCallAtLevelZero(int id)
void RegisterReversibleInt(int id, int *rev)
void RegisterReversibleClass(int id, ReversibleInterface *rev)
GenericLiteralWatcher(Model *model)
void SetPropagatorPriority(int id, int priority)
int Register(PropagatorInterface *propagator)
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
void Untrail(const Trail &trail, int literal_trail_index) final
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i, IntegerValue *bound) const
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
void FullyEncodeVariable(IntegerVariable var)
Literal GetFalseLiteral()
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
void ClearNewlyFixedIntegerLiterals()
const std::vector< IntegerLiteral > NewlyFixedIntegerLiterals() const
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
bool LiteralIsAssociated(IntegerLiteral i_lit) const
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
std::vector< ValueLiteralPair > PartialDomainEncoding(IntegerVariable var) const
void AddAllImplicationsBetweenAssociatedLiterals()
bool VariableIsFullyEncoded(IntegerVariable var) const
LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const
void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit)
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
IntegerVariable FirstUnassignedVariable() const
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value)
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
bool Propagate(Trail *trail) final
void ReserveSpaceForNumVariables(int num_vars)
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
bool IsCurrentlyIgnored(IntegerVariable i) const
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
std::function< void(IntegerLiteral literal_to_explain, int trail_index_of_literal, std::vector< Literal > *literals, std::vector< int > *dependencies)> LazyReasonFunction
bool IsFixed(IntegerVariable i) const
LiteralIndex OptionalLiteralIndex(IntegerVariable i) const
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
bool CurrentBranchHadAnIncompletePropagation()
bool InPropagationLoop() const
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerVariable NextVariableToBranchOnInPropagationLoop() const
IntegerValue UpperBound(IntegerVariable i) const
int64 num_enqueues() const
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
IntegerValue LowerBound(IntegerVariable i) const
int NumConstantVariables() const
void MergeReasonInto(absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
Literal IsIgnoredLiteral(IntegerVariable i) const
bool IsOptional(IntegerVariable i) const
ABSL_MUST_USE_RESULT bool ConditionalEnqueue(Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
bool IntegerLiteralIsFalse(IntegerLiteral l) const
void RemoveLevelZeroBounds(std::vector< IntegerLiteral > *reason) const
IntegerVariable AddIntegerVariable()
void RegisterReversibleClass(ReversibleInterface *rev)
const Domain & InitialVariableDomain(IntegerVariable var) const
void Untrail(const Trail &trail, int literal_trail_index) final
IntegerVariable NumIntegerVariables() const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
int propagation_trail_index_
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
BooleanVariable NewBooleanVariable()
const VariablesAssignment & Assignment() const
bool AddBinaryClause(Literal a, Literal b)
void Backtrack(int target_level)
int CurrentDecisionLevel() const
const std::vector< Decision > & Decisions() const
bool AddUnitClause(Literal true_literal)
void Enqueue(Literal true_literal, int propagator_id)
const AssignmentInfo & Info(BooleanVariable var) const
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
std::vector< Literal > * MutableConflict()
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
void EnqueueWithUnitReason(Literal true_literal)
bool LiteralIsAssigned(Literal literal) const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
static const int64 kint64max
static const int32 kint32max
static const int64 kint64min
void InsertOrDie(Collection *const collection, const typename Collection::value_type &value)
absl::InlinedVector< IntegerLiteral, 2 > InlinedIntegerLiteralVector
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
const LiteralIndex kNoLiteralIndex(-1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
bool VariableIsPositive(IntegerVariable i)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapProd(int64 x, int64 y)
Represents a closed interval [start, end].
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::string DebugString() const