34template <
typename Watcher>
35bool WatcherListContains(
const std::vector<Watcher>& list,
36 const SatClause& candidate) {
37 for (
const Watcher& watcher : list) {
38 if (watcher.clause == &candidate)
return true;
44template <
typename Container,
typename Predicate>
45void RemoveIf(Container c, Predicate p) {
46 c->erase(std::remove_if(c->begin(), c->end(), p), c->end());
57 num_inspected_clauses_(0),
58 num_inspected_clause_literals_(0),
59 num_watched_clauses_(0),
60 stats_(
"LiteralWatchers") {
71 watchers_on_false_.resize(num_variables << 1);
72 reasons_.resize(num_variables);
73 needs_cleaning_.
Resize(LiteralIndex(num_variables << 1));
82 DCHECK(!WatcherListContains(watchers_on_false_[
literal.Index()], *clause));
83 watchers_on_false_[
literal.Index()].push_back(
84 Watcher(clause, blocking_literal));
87bool LiteralWatchers::PropagateOnFalse(Literal false_literal,
Trail* trail) {
90 std::vector<Watcher>& watchers = watchers_on_false_[false_literal.Index()];
91 const VariablesAssignment& assignment = trail->Assignment();
96 auto new_it = watchers.begin();
97 const auto end = watchers.end();
98 while (new_it != end && assignment.LiteralIsTrue(new_it->blocking_literal)) {
101 for (
auto it = new_it; it != end; ++it) {
103 if (assignment.LiteralIsTrue(it->blocking_literal)) {
107 ++num_inspected_clauses_;
112 Literal* literals = it->clause->literals();
113 const Literal other_watched_literal(
115 false_literal.Index().value()));
116 if (assignment.LiteralIsTrue(other_watched_literal)) {
118 new_it->blocking_literal = other_watched_literal;
120 ++num_inspected_clause_literals_;
128 const int start = it->start_index;
129 const int size = it->clause->size();
133 while (i < size && assignment.LiteralIsFalse(literals[i])) ++i;
134 num_inspected_clause_literals_ += i - start + 2;
137 while (i < start && assignment.LiteralIsFalse(literals[i])) ++i;
138 num_inspected_clause_literals_ += i - 2;
139 if (i >= start) i = size;
145 literals[0] = other_watched_literal;
146 literals[1] = literals[i];
147 literals[i] = false_literal;
148 watchers_on_false_[literals[1].Index()].emplace_back(
149 it->clause, other_watched_literal, i + 1);
156 if (assignment.LiteralIsFalse(other_watched_literal)) {
161 trail->MutableConflict()->assign(it->clause->begin(), it->clause->end());
162 trail->SetFailingSatClause(it->clause);
163 num_inspected_clause_literals_ += it - watchers.begin() + 1;
164 watchers.erase(new_it, it);
171 literals[0] = other_watched_literal;
172 literals[1] = false_literal;
173 reasons_[trail->Index()] = it->clause;
178 num_inspected_clause_literals_ += watchers.size();
179 watchers.erase(new_it, end);
184 const int old_index = trail->
Index();
187 if (!PropagateOnFalse(
literal.Negated(), trail))
return false;
193 int trail_index)
const {
194 return reasons_[trail_index]->PropagationReason();
198 return reasons_[trail_index];
208 clauses_.push_back(clause);
209 return AttachAndPropagate(clause, trail);
213 const std::vector<Literal>& literals,
Trail* trail) {
215 clauses_.push_back(clause);
216 CHECK(AttachAndPropagate(clause, trail));
225bool LiteralWatchers::AttachAndPropagate(
SatClause* clause,
Trail* trail) {
228 const int size = clause->
size();
229 Literal* literals = clause->literals();
233 int num_literal_not_false = 0;
234 for (
int i = 0; i < size; ++i) {
236 std::swap(literals[i], literals[num_literal_not_false]);
237 ++num_literal_not_false;
238 if (num_literal_not_false == 2) {
247 if (num_literal_not_false == 0)
return false;
249 if (num_literal_not_false == 1) {
252 int max_level = trail->
Info(literals[1].Variable()).
level;
253 for (
int i = 2; i < size; ++i) {
254 const int level = trail->
Info(literals[i].Variable()).
level;
255 if (level > max_level) {
257 std::swap(literals[1], literals[i]);
263 reasons_[trail->
Index()] = clause;
268 ++num_watched_clauses_;
269 AttachOnFalse(literals[0], literals[1], clause);
270 AttachOnFalse(literals[1], literals[0], clause);
275 Literal* literals = clause->literals();
279 ++num_watched_clauses_;
280 AttachOnFalse(literals[0], literals[1], clause);
281 AttachOnFalse(literals[1], literals[0], clause);
284void LiteralWatchers::InternalDetach(
SatClause* clause) {
285 --num_watched_clauses_;
286 const size_t size = clause->
size();
287 if (drat_proof_handler_ !=
nullptr && size > 2) {
290 clauses_info_.erase(clause);
295 InternalDetach(clause);
302 InternalDetach(clause);
304 needs_cleaning_.
Clear(l.Index());
305 RemoveIf(&(watchers_on_false_[l.Index()]), [](
const Watcher& watcher) {
306 return !watcher.clause->IsAttached();
312 if (!all_clauses_are_attached_)
return;
313 all_clauses_are_attached_ =
false;
318 num_watched_clauses_ = 0;
319 watchers_on_false_.clear();
323 if (all_clauses_are_attached_)
return;
324 all_clauses_are_attached_ =
true;
327 watchers_on_false_.resize(needs_cleaning_.
size().value());
331 ++num_watched_clauses_;
341 if (drat_proof_handler_ !=
nullptr) {
342 drat_proof_handler_->
AddClause({true_literal});
351 return implication_graph_->
Propagate(trail_);
359 CHECK(!all_clauses_are_attached_);
360 if (drat_proof_handler_ !=
nullptr) {
363 clauses_info_.erase(clause);
368 SatClause* clause, absl::Span<const Literal> new_clause) {
369 if (new_clause.empty())
return false;
372 for (
const Literal l : new_clause) {
377 if (new_clause.size() == 1) {
383 if (new_clause.size() == 2) {
389 if (drat_proof_handler_ !=
nullptr) {
391 drat_proof_handler_->
AddClause(new_clause);
395 if (all_clauses_are_attached_) {
398 --num_watched_clauses_;
401 needs_cleaning_.
Clear(l.Index());
402 RemoveIf(&(watchers_on_false_[l.Index()]), [](
const Watcher& watcher) {
403 return !watcher.clause->IsAttached();
408 clause->Rewrite(new_clause);
411 if (all_clauses_are_attached_)
Attach(clause, trail_);
416 absl::Span<const Literal> new_clause) {
417 CHECK(!new_clause.empty());
418 CHECK(!all_clauses_are_attached_);
420 for (
const Literal l : new_clause) {
425 if (new_clause.size() == 1) {
431 if (new_clause.size() == 2) {
437 clauses_.push_back(clause);
445 RemoveIf(&(watchers_on_false_[
index]), [](
const Watcher& watcher) {
458 if (to_minimize_index_ >= clauses_.size()) {
459 to_minimize_index_ = clauses_.size();
462 std::stable_partition(clauses_.begin(),
463 clauses_.begin() + to_minimize_index_,
464 [](
SatClause*
a) { return a->IsAttached(); }) -
468 std::vector<SatClause*>::iterator iter =
469 std::stable_partition(clauses_.begin(), clauses_.end(),
470 [](
SatClause*
a) { return a->IsAttached(); });
472 clauses_.erase(iter, clauses_.end());
479 implications_.resize(num_variables << 1);
480 is_redundant_.
resize(implications_.size(),
false);
481 is_removed_.
resize(implications_.size(),
false);
482 estimated_sizes_.
resize(implications_.size(), 0);
483 in_direct_implications_.
resize(implications_.size(),
false);
484 reasons_.resize(num_variables);
493 if (drat_proof_handler_ !=
nullptr) {
500 estimated_sizes_[
a.NegatedIndex()]++;
501 estimated_sizes_[
b.NegatedIndex()]++;
502 implications_[
a.NegatedIndex()].push_back(
b);
503 implications_[
b.NegatedIndex()].push_back(
a);
505 num_implications_ += 2;
513 const auto& assignment = trail_->
Assignment();
514 if (assignment.LiteralIsFalse(
a)) {
515 if (assignment.LiteralIsAssigned(
b)) {
516 if (assignment.LiteralIsFalse(
b))
return false;
518 reasons_[trail_->
Index()] =
a;
521 }
else if (assignment.LiteralIsFalse(
b)) {
522 if (!assignment.LiteralIsAssigned(
a)) {
523 reasons_[trail_->
Index()] =
b;
532 absl::Span<const Literal> at_most_one) {
534 if (at_most_one.size() <= 1)
return true;
539 const int base_index = at_most_one_buffer_.size();
540 at_most_one_buffer_.insert(at_most_one_buffer_.end(), at_most_one.begin(),
545 return CleanUpAndAddAtMostOnes(base_index);
550bool BinaryImplicationGraph::FixLiteral(
Literal true_literal) {
554 if (drat_proof_handler_ !=
nullptr) {
555 drat_proof_handler_->
AddClause({true_literal});
565bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(
const int base_index) {
566 const VariablesAssignment& assignment = trail_->
Assignment();
567 int local_end = base_index;
568 const int buffer_size = at_most_one_buffer_.size();
569 for (
int i = base_index; i < buffer_size; ++i) {
574 const int local_start = local_end;
575 bool set_all_left_to_false =
false;
577 const Literal l = at_most_one_buffer_[i];
579 if (assignment.LiteralIsFalse(l))
continue;
580 if (is_removed_[l.Index()])
continue;
581 if (!set_all_left_to_false && assignment.LiteralIsTrue(l)) {
582 set_all_left_to_false =
true;
589 if (set_all_left_to_false) {
590 for (
int j = local_start; j < local_end; ++j) {
591 const Literal l = at_most_one_buffer_[j];
592 if (assignment.LiteralIsFalse(l))
continue;
593 if (assignment.LiteralIsTrue(l))
return false;
594 if (!FixLiteral(l.Negated()))
return false;
596 local_end = local_start;
603 int new_local_end = local_start;
604 std::sort(&at_most_one_buffer_[local_start],
605 &at_most_one_buffer_[local_end]);
606 for (
int j = local_start; j < local_end; ++j) {
607 const Literal l = at_most_one_buffer_[j];
608 if (new_local_end > local_start &&
609 l == at_most_one_buffer_[new_local_end - 1]) {
610 if (assignment.LiteralIsTrue(l))
return false;
611 if (!assignment.LiteralIsFalse(l)) {
612 if (!FixLiteral(l.Negated()))
return false;
617 at_most_one_buffer_[new_local_end++] = l;
619 local_end = new_local_end;
623 const absl::Span<const Literal> at_most_one(
624 &at_most_one_buffer_[local_start], local_end - local_start);
628 if (at_most_one.size() < 10) {
630 for (
const Literal
a : at_most_one) {
631 for (
const Literal
b : at_most_one) {
632 if (
a ==
b)
continue;
633 implications_[
a.Index()].push_back(
b.Negated());
636 num_implications_ += at_most_one.size() * (at_most_one.size() - 1);
639 local_end = local_start;
644 for (
const Literal l : at_most_one) {
645 if (l.Index() >= at_most_ones_.
size()) {
646 at_most_ones_.
resize(l.Index().value() + 1);
648 CHECK(!is_redundant_[l.Index()]);
649 at_most_ones_[l.Index()].
push_back(local_start);
656 at_most_one_buffer_.resize(local_end);
660bool BinaryImplicationGraph::PropagateOnTrue(Literal true_literal,
664 const VariablesAssignment& assignment = trail->Assignment();
665 DCHECK(assignment.LiteralIsTrue(true_literal));
670 num_inspections_ += implications_[true_literal.Index()].size();
672 for (Literal
literal : implications_[true_literal.Index()]) {
673 if (assignment.LiteralIsTrue(
literal)) {
683 if (assignment.LiteralIsFalse(
literal)) {
685 *(trail->MutableConflict()) = {true_literal.Negated(),
literal};
689 reasons_[trail->Index()] = true_literal.Negated();
695 if (true_literal.Index() < at_most_ones_.
size()) {
696 for (
const int start : at_most_ones_[true_literal.Index()]) {
698 for (
int i = start;; ++i) {
699 const Literal
literal = at_most_one_buffer_[i];
710 if (assignment.LiteralIsFalse(
literal))
continue;
713 if (assignment.LiteralIsTrue(
literal)) {
715 *(trail->MutableConflict()) = {true_literal.Negated(),
720 reasons_[trail->Index()] = true_literal.Negated();
735 while (propagation_trail_index_ < trail->
Index()) {
737 if (!PropagateOnTrue(
literal, trail))
return false;
743 const Trail& trail,
int trail_index)
const {
744 return {&reasons_[trail_index], 1};
755 std::vector<Literal>* conflict) {
761 const LiteralIndex root_literal_index = conflict->front().NegatedIndex();
763 is_marked_.
Set(root_literal_index);
772 const bool also_prune_direct_implication_list =
false;
776 auto& direct_implications = implications_[root_literal_index];
777 for (
const Literal l : direct_implications) {
778 if (is_marked_[l.Index()])
continue;
779 dfs_stack_.push_back(l);
780 while (!dfs_stack_.empty()) {
781 const LiteralIndex
index = dfs_stack_.back().Index();
782 dfs_stack_.pop_back();
783 if (!is_marked_[
index]) {
786 if (!is_marked_[implied.Index()]) dfs_stack_.push_back(implied);
802 if (also_prune_direct_implication_list) {
803 is_marked_.
Clear(l.Index());
809 if (also_prune_direct_implication_list) {
811 for (
const Literal l : direct_implications) {
812 if (!is_marked_[l.Index()]) {
813 is_marked_.
Set(l.Index());
814 direct_implications[new_size] = l;
818 if (new_size < direct_implications.size()) {
819 num_redundant_implications_ += direct_implications.size() - new_size;
820 direct_implications.resize(new_size);
824 RemoveRedundantLiterals(conflict);
832 const Trail& trail, std::vector<Literal>* conflict,
835 CHECK(!conflict->empty());
837 MarkDescendants(conflict->front().Negated());
843 RemoveRedundantLiterals(conflict);
850 const Trail& trail, std::vector<Literal>* conflict,
853 const LiteralIndex root_literal_index = conflict->front().NegatedIndex();
855 is_marked_.
Set(root_literal_index);
858 auto& direct_implications = implications_[root_literal_index];
864 std::shuffle(direct_implications.begin(), direct_implications.end(), random);
866 for (
const Literal l : direct_implications) {
867 if (is_marked_[l.Index()]) {
873 direct_implications[new_size++] = l;
874 dfs_stack_.push_back(l);
875 while (!dfs_stack_.empty()) {
876 const LiteralIndex
index = dfs_stack_.back().Index();
877 dfs_stack_.pop_back();
878 if (!is_marked_[
index]) {
881 if (!is_marked_[implied.Index()]) dfs_stack_.push_back(implied);
886 if (new_size < direct_implications.size()) {
887 num_redundant_implications_ += direct_implications.size() - new_size;
888 direct_implications.resize(new_size);
890 RemoveRedundantLiterals(conflict);
893void BinaryImplicationGraph::RemoveRedundantLiterals(
894 std::vector<Literal>* conflict) {
897 for (
int i = 1; i < conflict->size(); ++i) {
898 if (!is_marked_[(*conflict)[i].NegatedIndex()]) {
899 (*conflict)[new_index] = (*conflict)[i];
903 if (new_index < conflict->size()) {
905 num_literals_removed_ += conflict->size() - new_index;
906 conflict->resize(new_index);
912 const Trail& trail, std::vector<Literal>* conflict) {
915 is_simplified_.
ClearAndResize(LiteralIndex(implications_.size()));
916 for (
Literal lit : *conflict) {
917 is_marked_.
Set(lit.Index());
933 for (
int i = 1; i < conflict->size(); ++i) {
934 const Literal lit = (*conflict)[i];
936 bool keep_literal =
true;
938 if (is_marked_[implied.Index()]) {
940 if (lit_level == trail.
Info(implied.Variable()).
level &&
941 is_simplified_[implied.Index()]) {
944 keep_literal =
false;
949 (*conflict)[
index] = lit;
955 if (index < conflict->size()) {
957 num_literals_removed_ += conflict->size() -
index;
958 conflict->erase(conflict->begin() +
index, conflict->end());
967 const int new_num_fixed = trail_->
Index();
968 if (num_processed_fixed_variables_ == new_num_fixed)
return;
972 for (; num_processed_fixed_variables_ < new_num_fixed;
973 ++num_processed_fixed_variables_) {
974 const Literal true_literal = (*trail_)[num_processed_fixed_variables_];
978 for (
const Literal lit : implications_[true_literal.
Index()]) {
992 is_marked_.
Set(lit.NegatedIndex());
997 if (true_literal.
Index() < at_most_ones_.
size()) {
1005 RemoveIf(&implications_[i], [&assignment](
const Literal& lit) {
1012 at_most_ones_.
clear();
1013 CleanUpAndAddAtMostOnes(0);
1024 std::vector<std::vector<int32>>>;
1028 std::vector<Literal>* at_most_one_buffer)
1030 implications_(*graph),
1031 at_most_ones_(*at_most_ones),
1032 at_most_one_buffer_(*at_most_one_buffer) {}
1036 for (
const Literal l : implications_[LiteralIndex(node)]) {
1037 tmp_.push_back(l.Index().value());
1042 if (node < at_most_ones_.
size()) {
1043 for (
const int start : at_most_ones_[LiteralIndex(node)]) {
1044 if (start >= at_most_one_already_explored_.size()) {
1045 at_most_one_already_explored_.resize(start + 1,
false);
1046 previous_node_to_explore_at_most_one_.resize(start + 1);
1056 if (at_most_one_already_explored_[start]) {
1058 const int first_node = previous_node_to_explore_at_most_one_[start];
1077 previous_node_to_explore_at_most_one_[start] = node;
1082 Literal(LiteralIndex(first_node)).NegatedIndex().
value());
1086 at_most_one_already_explored_[start] =
true;
1087 previous_node_to_explore_at_most_one_[start] = node;
1090 for (
int i = start;; ++i) {
1091 const Literal l = at_most_one_buffer_[i];
1093 if (l.
Index() == node)
continue;
1115 const std::vector<Literal>& at_most_one_buffer_;
1117 mutable std::vector<int32> tmp_;
1120 mutable std::vector<bool> at_most_one_already_explored_;
1121 mutable std::vector<int> previous_node_to_explore_at_most_one_;
1127 if (is_dag_)
return true;
1138 int num_fixed_during_scc = 0;
1139 const int32 size(implications_.size());
1140 std::vector<std::vector<int32>> scc;
1144 SccGraph graph(&finder, &implications_, &at_most_ones_,
1145 &at_most_one_buffer_);
1152 ++num_fixed_during_scc;
1153 if (!FixLiteral(l))
return false;
1159 is_redundant_.
resize(size,
false);
1161 int num_equivalences = 0;
1162 reverse_topological_order_.clear();
1163 for (std::vector<int32>& component : scc) {
1171 bool all_fixed =
false;
1172 bool all_true =
false;
1173 for (
const int32 i : component) {
1182 for (
const int32 i : component) {
1184 if (!is_redundant_[l.
Index()]) {
1185 ++num_redundant_literals_;
1186 is_redundant_[l.
Index()] =
true;
1191 ++num_fixed_during_scc;
1192 if (!FixLiteral(l))
return false;
1201 if (component.size() == 1 && is_removed_[LiteralIndex(component[0])]) {
1210 std::sort(component.begin(), component.end());
1214 if (component.size() == 1) {
1217 if (num_equivalences > 0) {
1219 for (
Literal& ref : representative_list) {
1220 const LiteralIndex rep = representative_of_[ref.Index()];
1231 for (
int i = 1; i < component.size(); ++i) {
1233 if (!is_redundant_[
literal.Index()]) {
1234 ++num_redundant_literals_;
1235 is_redundant_[
literal.Index()] =
true;
1241 if (
Literal(LiteralIndex(component[i - 1])).Negated() ==
literal) {
1242 LOG_IF(
INFO, log_info) <<
"Trivially UNSAT in DetectEquivalences()";
1251 for (
const Literal l : representative_list) {
1254 representative_list[new_size++] = rep;
1256 representative_list.resize(new_size);
1257 for (
int i = 1; i < component.size(); ++i) {
1259 auto& ref = implications_[
literal.Index()];
1270 representative_list.push_back(
literal);
1275 num_equivalences += component.size() - 1;
1279 if (num_equivalences != 0) {
1283 at_most_ones_.
clear();
1284 CleanUpAndAddAtMostOnes(0);
1286 num_implications_ = 0;
1287 for (LiteralIndex i(0); i < size; ++i) {
1288 num_implications_ += implications_[i].size();
1290 dtime += 2e-8 * num_implications_;
1294 LOG_IF(
INFO, log_info) <<
"SCC. " << num_equivalences
1295 <<
" redundant equivalent literals. "
1296 << num_fixed_during_scc <<
" fixed. "
1297 << num_implications_ <<
" implications left. "
1298 << implications_.size() <<
" literals."
1299 <<
" size of at_most_one buffer = "
1300 << at_most_one_buffer_.size() <<
"."
1301 <<
" dtime: " << dtime
1325 int64 num_fixed = 0;
1326 int64 num_new_redundant_implications = 0;
1327 bool aborted =
false;
1328 work_done_in_mark_descendants_ = 0;
1329 int marked_index = 0;
1347 const LiteralIndex size(implications_.size());
1349 for (
const LiteralIndex root : reverse_topological_order_) {
1354 if (is_redundant_[root])
continue;
1357 auto& direct_implications = implications_[root];
1358 if (direct_implications.empty())
continue;
1367 bool clear_previous_reachability =
true;
1368 for (
const Literal direct_child : direct_implications) {
1369 if (direct_child.Index() == previous) {
1370 clear_previous_reachability =
false;
1371 is_marked_.
Clear(previous);
1375 if (clear_previous_reachability) {
1381 for (
const Literal direct_child : direct_implications) {
1382 if (is_redundant_[direct_child.Index()])
continue;
1383 if (is_marked_[direct_child.Index()])
continue;
1387 if (direct_child.Index() == root)
continue;
1391 if (direct_child.NegatedIndex() == root) {
1392 is_marked_.
Set(direct_child.Index());
1396 MarkDescendants(direct_child);
1399 is_marked_.
Clear(direct_child.Index());
1401 CHECK(!is_marked_[root])
1402 <<
"DetectEquivalences() should have removed cycles!";
1403 is_marked_.
Set(root);
1409 for (; marked_index < marked_positions.size(); ++marked_index) {
1410 const LiteralIndex i = marked_positions[marked_index];
1411 if (is_marked_[
Literal(i).NegatedIndex()]) {
1419 if (!FixLiteral(
Literal(root).Negated()))
return false;
1433 for (
const Literal l : direct_implications) {
1434 if (!is_marked_[l.Index()]) {
1435 direct_implications[new_size++] = l;
1437 CHECK(!is_redundant_[l.Index()]);
1440 const int diff = direct_implications.size() - new_size;
1441 direct_implications.resize(new_size);
1442 direct_implications.shrink_to_fit();
1443 num_new_redundant_implications += diff;
1444 num_implications_ -= diff;
1447 if (work_done_in_mark_descendants_ > 1e8) {
1455 const double dtime = 1e-8 * work_done_in_mark_descendants_;
1457 num_redundant_implications_ += num_new_redundant_implications;
1458 LOG_IF(
INFO, log_info) <<
"Transitive reduction removed "
1459 << num_new_redundant_implications <<
" literals. "
1460 << num_fixed <<
" fixed. " << num_implications_
1461 <<
" implications left. " << implications_.size()
1463 <<
" dtime: " << dtime
1465 << (aborted ?
" Aborted." :
"");
1471bool IntersectionIsEmpty(
const std::vector<int>&
a,
const std::vector<int>&
b) {
1472 DCHECK(std::is_sorted(
a.begin(),
a.end()));
1473 DCHECK(std::is_sorted(
b.begin(),
b.end()));
1476 for (; i <
a.size() && j <
b.size();) {
1477 if (
a[i] ==
b[j])
return false;
1489 std::size_t operator()(
const std::vector<Literal>& at_most_one)
const {
1491 for (Literal
literal : at_most_one) {
1501 std::vector<std::vector<Literal>>* at_most_ones,
1502 int64 max_num_explored_nodes) {
1505 work_done_in_mark_descendants_ = 0;
1507 int num_extended = 0;
1508 int num_removed = 0;
1511 absl::flat_hash_set<std::vector<Literal>, VectorHash> max_cliques;
1513 implications_.size());
1516 std::sort(at_most_ones->begin(), at_most_ones->end(),
1517 [](
const std::vector<Literal>
a,
const std::vector<Literal>
b) {
1518 return a.size() > b.size();
1520 for (std::vector<Literal>& clique : *at_most_ones) {
1521 const int old_size = clique.size();
1531 const LiteralIndex rep = representative_of_[ref.Index()];
1540 if (old_size == 2 && clique[0] != clique[1]) {
1541 if (!IntersectionIsEmpty(max_cliques_containing[clique[0].
Index()],
1542 max_cliques_containing[clique[1].
Index()])) {
1550 if (work_done_in_mark_descendants_ < max_num_explored_nodes) {
1551 clique = ExpandAtMostOne(clique);
1553 std::sort(clique.begin(), clique.end());
1560 const int clique_index = max_cliques.size();
1561 for (
const Literal l : clique) {
1562 max_cliques_containing[l.Index()].
push_back(clique_index);
1564 if (clique.size() > old_size) ++num_extended;
1568 if (num_extended > 0 || num_removed > 0 || num_added > 0) {
1569 VLOG(1) <<
"Clique Extended: " << num_extended
1570 <<
" Removed: " << num_removed <<
" Added: " << num_added
1571 << (work_done_in_mark_descendants_ > max_num_explored_nodes
1578std::vector<Literal> BinaryImplicationGraph::ExpandAtMostOneWithWeight(
1579 const absl::Span<const Literal> at_most_one,
1582 std::vector<Literal> clique(at_most_one.begin(), at_most_one.end());
1583 std::vector<LiteralIndex> intersection;
1584 double clique_weight = 0.0;
1585 const int64 old_work = work_done_in_mark_descendants_;
1586 for (
const Literal l : clique) clique_weight += expanded_lp_values[l.Index()];
1587 for (
int i = 0; i < clique.size(); ++i) {
1589 if (work_done_in_mark_descendants_ - old_work > 1e8)
break;
1592 MarkDescendants(clique[i]);
1595 if (can_be_included[
index]) intersection.push_back(
index);
1597 for (
const Literal l : clique) is_marked_.
Clear(l.NegatedIndex());
1601 double intersection_weight = 0.0;
1603 is_marked_.
Clear(clique[i].NegatedIndex());
1604 for (
const LiteralIndex
index : intersection) {
1605 if (!is_marked_[
index])
continue;
1606 intersection[new_size++] =
index;
1607 intersection_weight += expanded_lp_values[
index];
1609 intersection.
resize(new_size);
1610 if (intersection.empty())
break;
1614 if (clique_weight + intersection_weight <= 1.0) {
1621 if (i + 1 == clique.size()) {
1624 double max_lp = 0.0;
1625 for (
int j = 0; j < intersection.size(); ++j) {
1626 const double lp = 1.0 - expanded_lp_values[intersection[j]] +
1627 absl::Uniform<double>(*random_, 0.0, 1e-4);
1628 if (
index == -1 || lp > max_lp) {
1634 clique.push_back(Literal(intersection[
index]).Negated());
1635 std::swap(intersection.back(), intersection[
index]);
1636 intersection.pop_back();
1637 clique_weight += expanded_lp_values[clique.back().Index()];
1644const std::vector<std::vector<Literal>>&
1646 const std::vector<Literal>& literals,
1647 const std::vector<double>& lp_values) {
1649 const int num_literals = implications_.size();
1653 const int size = literals.size();
1654 for (
int i = 0; i < size; ++i) {
1655 const Literal l = literals[i];
1656 can_be_included[l.
Index()] =
true;
1659 const double value = lp_values[i];
1669 bool operator<(
const Candidate& other)
const {
return sum > other.sum; }
1671 std::vector<Candidate> candidates;
1679 for (
int i = 0; i < size; ++i) {
1680 Literal current_literal = literals[i];
1681 double current_value = lp_values[i];
1683 if (is_redundant_[current_literal.
Index()])
continue;
1685 if (current_value < 0.5) {
1686 current_literal = current_literal.
Negated();
1687 current_value = 1.0 - current_value;
1692 double best_value = 0.0;
1693 for (
const Literal l : implications_[current_literal.
Index()]) {
1694 if (!can_be_included[l.Index()])
continue;
1695 const double activity =
1696 current_value + expanded_lp_values[l.NegatedIndex()];
1697 if (activity <= 1.01)
continue;
1698 const double v = activity + absl::Uniform<double>(*random_, 0.0, 1e-4);
1701 best = l.NegatedIndex();
1705 const double activity = current_value + expanded_lp_values[best];
1711 const int kMaxNumberOfCutPerCall = 50;
1712 std::sort(candidates.begin(), candidates.end());
1713 if (candidates.size() > kMaxNumberOfCutPerCall) {
1714 candidates.resize(kMaxNumberOfCutPerCall);
1720 std::vector<Literal> at_most_one;
1721 for (
const Candidate& candidate : candidates) {
1722 at_most_one = ExpandAtMostOneWithWeight(
1723 {candidate.a, candidate.b}, can_be_included, expanded_lp_values);
1724 if (!at_most_one.empty()) tmp_cuts_.push_back(at_most_one);
1730void BinaryImplicationGraph::MarkDescendants(
Literal root) {
1731 dfs_stack_ = {root};
1733 if (is_redundant_[root.
Index()])
return;
1734 for (
int j = 0; j < dfs_stack_.size(); ++j) {
1735 const Literal current = dfs_stack_[j];
1736 for (
const Literal l : implications_[current.Index()]) {
1737 if (!is_marked_[l.Index()] && !is_redundant_[l.Index()]) {
1738 dfs_stack_.push_back(l);
1739 is_marked_.
Set(l.Index());
1743 if (current.Index() >= at_most_ones_.
size())
continue;
1744 for (
const int start : at_most_ones_[current.Index()]) {
1745 for (
int i = start;; ++i) {
1746 const Literal l = at_most_one_buffer_[i];
1748 if (l == current)
continue;
1749 if (!is_marked_[l.NegatedIndex()] && !is_redundant_[l.NegatedIndex()]) {
1750 dfs_stack_.push_back(l.Negated());
1751 is_marked_.
Set(l.NegatedIndex());
1756 work_done_in_mark_descendants_ += dfs_stack_.size();
1759std::vector<Literal> BinaryImplicationGraph::ExpandAtMostOne(
1760 const absl::Span<const Literal> at_most_one) {
1761 std::vector<Literal> clique(at_most_one.begin(), at_most_one.end());
1764 for (
int i = 0; i < clique.size(); ++i) {
1765 if (implications_[clique[i].
Index()].empty() ||
1766 is_redundant_[clique[i].
Index()]) {
1771 std::vector<LiteralIndex> intersection;
1772 for (
int i = 0; i < clique.size(); ++i) {
1774 MarkDescendants(clique[i]);
1777 for (
const Literal l : clique) is_marked_.
Clear(l.NegatedIndex());
1781 is_marked_.
Clear(clique[i].NegatedIndex());
1782 for (
const LiteralIndex
index : intersection) {
1783 if (is_marked_[
index]) intersection[new_size++] =
index;
1785 intersection.resize(new_size);
1786 if (intersection.empty())
break;
1789 if (i + 1 == clique.size()) {
1790 clique.push_back(Literal(intersection.back()).Negated());
1791 intersection.pop_back();
1804 for (
const Literal l : direct_implications_) {
1805 in_direct_implications_[l.Index()] =
false;
1807 direct_implications_.
clear();
1815 if (!is_removed_[l.Index()] && !in_direct_implications_[l.Index()]) {
1816 in_direct_implications_[l.Index()] =
true;
1821 if (is_redundant_[
literal.Index()]) {
1824 for (
const int start : at_most_ones_[
literal.Index()]) {
1825 for (
int i = start;; ++i) {
1826 const Literal l = at_most_one_buffer_[i];
1830 if (!is_removed_[l.
Index()] &&
1838 estimated_sizes_[
literal.Index()] = direct_implications_.
size();
1839 return direct_implications_;
1851 direct_implications_of_negated_literal_ =
1854 for (
const Literal l : direct_implications_of_negated_literal_) {
1855 if (in_direct_implications_[l.Index()]) {
1857 if (!FixLiteral(l)) {
1868 BooleanVariable
var) {
1871 direct_implications_of_negated_literal_ =
1874 for (
const Literal l : direct_implications_of_negated_literal_) {
1878 CHECK(!in_direct_implications_[l.Index()]);
1881 if (in_direct_implications_[l.NegatedIndex()]) result--;
1888 BooleanVariable
var, std::deque<std::vector<Literal>>* postsolve_clauses) {
1890 direct_implications_of_negated_literal_ =
1893 estimated_sizes_[
b.NegatedIndex()]--;
1894 for (
const Literal a_negated : direct_implications_of_negated_literal_) {
1895 if (a_negated.Negated() ==
b)
continue;
1899 for (
const Literal a_negated : direct_implications_of_negated_literal_) {
1900 estimated_sizes_[a_negated.NegatedIndex()]--;
1905 for (
const Literal b : direct_implications_) {
1906 if (drat_proof_handler_ !=
nullptr) {
1909 postsolve_clauses->push_back({
Literal(
var,
false),
b});
1911 for (
const Literal a_negated : direct_implications_of_negated_literal_) {
1912 if (drat_proof_handler_ !=
nullptr) {
1915 postsolve_clauses->push_back({
Literal(
var,
true), a_negated});
1921 is_removed_[
index] =
true;
1922 if (!is_redundant_[
index]) {
1923 ++num_redundant_literals_;
1924 is_redundant_[
index] =
true;
1926 implications_[
index].clear();
1931 for (
auto& implication : implications_) {
1933 for (
const Literal l : implication) {
1934 if (!is_removed_[l.Index()]) implication[new_size++] = l;
1936 implication.resize(new_size);
1940 at_most_ones_.
clear();
1941 CleanUpAndAddAtMostOnes(0);
1951 clause->size_ = literals.size();
1952 for (
int i = 0; i < literals.size(); ++i) {
1953 clause->literals_[i] = literals[i];
1972 for (
int i = j; i < size_; ++i) {
1976 std::swap(literals_[j], literals_[i]);
1994 if (!result.empty()) result.append(
" ");
1995 result.append(
literal.DebugString());
#define LOG_IF(severity, condition)
#define DCHECK_LE(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define DCHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define VLOG(verboselevel)
bool NodeIsInCurrentDfsPath(NodeIndex node) const
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
void resize(size_type new_size)
void push_back(const value_type &x)
void Set(IntegerType index)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
void Clear(IntegerType index)
void Resize(IntegerType size)
void ClearAndResize(IntegerType size)
std::string StatString() const
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
bool Propagate(Trail *trail) final
void AddBinaryClause(Literal a, Literal b)
bool ComputeTransitiveReduction(bool log_info=false)
void MinimizeConflictWithReachability(std::vector< Literal > *c)
bool AddBinaryClauseDuringSearch(Literal a, Literal b)
const std::vector< std::vector< Literal > > & GenerateAtMostOnesWithLargeWeight(const std::vector< Literal > &literals, const std::vector< double > &lp_values)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
bool TransformIntoMaxCliques(std::vector< std::vector< Literal > > *at_most_ones, int64 max_num_explored_nodes=1e8)
void RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
void MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, absl::BitGenRef random)
Literal RepresentativeOf(Literal l) const
const std::vector< Literal > & DirectImplications(Literal literal)
void AddImplication(Literal a, Literal b)
void MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked)
bool DetectEquivalences(bool log_info=false)
void CleanupAllRemovedVariables()
bool FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat)
void RemoveFixedVariables()
int64 NumImplicationOnVariableRemoval(BooleanVariable var)
ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span< const Literal > at_most_one)
void MinimizeConflictExperimental(const Trail &trail, std::vector< Literal > *c)
void Resize(int num_variables)
void DeleteClause(absl::Span< const Literal > clause)
void AddClause(absl::Span< const Literal > clause)
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
BooleanVariable Variable() const
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)
LiteralWatchers(Model *model)
bool Propagate(Trail *trail) final
void InprocessingRemoveClause(SatClause *clause)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
SatClause * AddRemovableClause(const std::vector< Literal > &literals, Trail *trail)
SatClause * InprocessingAddClause(absl::Span< const Literal > new_clause)
void Attach(SatClause *clause, Trail *trail)
bool AddClause(absl::Span< const Literal > literals, Trail *trail)
SatClause * ReasonClause(int trail_index) const
ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause)
void LazyDetach(SatClause *clause)
~LiteralWatchers() override
void DeleteRemovedClauses()
void Detach(SatClause *clause)
void Resize(int num_variables)
Class that owns everything related to a particular optimization model.
absl::Span< const Literal > AsSpan() const
const Literal *const begin() const
Literal SecondLiteral() const
bool IsSatisfied(const VariablesAssignment &assignment) const
bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment &assignment)
std::string DebugString() const
Literal FirstLiteral() const
static SatClause * Create(absl::Span< const Literal > literals)
int propagation_trail_index_
SccGraph(SccFinder *finder, Implication *graph, AtMostOne *at_most_ones, std::vector< Literal > *at_most_one_buffer)
std::vector< Literal > to_fix_
const std::vector< int32 > & operator[](int32 node) const
void RegisterPropagator(SatPropagator *propagator)
void Enqueue(Literal true_literal, int propagator_id)
const VariablesAssignment & Assignment() const
const AssignmentInfo & Info(BooleanVariable var) const
int CurrentDecisionLevel() const
void EnqueueWithUnitReason(Literal true_literal)
bool LiteralIsAssigned(Literal literal) const
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
bool InsertIfNotPresent(Collection *const collection, const typename Collection::value_type &value)
void STLClearObject(T *obj)
void STLDeleteElements(T *container)
void STLDeleteContainerPointers(ForwardIterator begin, ForwardIterator end)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
const LiteralIndex kNoLiteralIndex(-1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
uint64 Hash(uint64 num, uint64 c)
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)
#define VLOG_IS_ON(verboselevel)