27#include "absl/container/flat_hash_map.h"
28#include "absl/container/flat_hash_set.h"
29#include "absl/container/inlined_vector.h"
30#include "absl/log/check.h"
31#include "absl/log/log.h"
32#include "absl/log/vlog_is_on.h"
33#include "absl/random/bit_gen_ref.h"
34#include "absl/random/distributions.h"
35#include "absl/types/span.h"
56template <
typename Watcher>
57bool WatcherListContains(
const std::vector<Watcher>& list,
59 for (
const Watcher& watcher : list) {
60 if (watcher.clause == &candidate)
return true;
66template <
typename Container,
typename Predicate>
67void RemoveIf(Container c, Predicate p) {
68 c->erase(std::remove_if(
c->begin(),
c->end(), p),
c->end());
78 trail_(model->GetOrCreate<
Trail>()),
79 num_inspected_clauses_(0),
80 num_inspected_clause_literals_(0),
81 num_watched_clauses_(0),
82 stats_(
"ClauseManager") {
83 trail_->RegisterPropagator(
this);
93 watchers_on_false_.resize(num_variables << 1);
94 reasons_.resize(num_variables);
95 needs_cleaning_.Resize(LiteralIndex(num_variables << 1));
100void ClauseManager::AttachOnFalse(
Literal literal,
Literal blocking_literal,
104 DCHECK(!WatcherListContains(watchers_on_false_[literal], *clause));
105 watchers_on_false_[literal].push_back(Watcher(clause, blocking_literal));
108bool ClauseManager::PropagateOnFalse(Literal false_literal,
Trail* trail) {
111 std::vector<Watcher>& watchers = watchers_on_false_[false_literal];
112 const auto assignment = AssignmentView(trail->Assignment());
117 auto new_it = watchers.begin();
118 const auto end = watchers.end();
119 while (new_it !=
end && assignment.LiteralIsTrue(new_it->blocking_literal)) {
122 for (
auto it = new_it; it !=
end; ++it) {
124 if (assignment.LiteralIsTrue(it->blocking_literal)) {
128 ++num_inspected_clauses_;
133 Literal* literals = it->clause->literals();
134 const Literal other_watched_literal(
135 LiteralIndex(literals[0].
Index().value() ^ literals[1].
Index().value() ^
136 false_literal.Index().value()));
137 if (assignment.LiteralIsTrue(other_watched_literal)) {
139 new_it->blocking_literal = other_watched_literal;
141 ++num_inspected_clause_literals_;
149 const int start = it->start_index;
150 const int size = it->clause->size();
154 while (
i < size && assignment.LiteralIsFalse(literals[
i])) ++
i;
155 num_inspected_clause_literals_ +=
i - start + 2;
158 while (
i < start && assignment.LiteralIsFalse(literals[
i])) ++
i;
159 num_inspected_clause_literals_ +=
i - 2;
160 if (
i >= start)
i = size;
166 literals[0] = other_watched_literal;
167 literals[1] = literals[
i];
168 literals[
i] = false_literal;
169 watchers_on_false_[literals[1]].emplace_back(
170 it->clause, other_watched_literal,
i + 1);
177 if (assignment.LiteralIsFalse(other_watched_literal)) {
182 trail->MutableConflict()->assign(it->clause->begin(), it->clause->end());
183 trail->SetFailingSatClause(it->clause);
184 num_inspected_clause_literals_ += it - watchers.begin() + 1;
185 watchers.erase(new_it, it);
192 literals[0] = other_watched_literal;
193 literals[1] = false_literal;
194 reasons_[trail->Index()] = it->clause;
199 num_inspected_clause_literals_ += watchers.size();
200 watchers.erase(new_it,
end);
205 const int old_index = trail->
Index();
208 if (!PropagateOnFalse(literal.
Negated(), trail))
return false;
216 return reasons_[trail_index]->PropagationReason();
220 return reasons_[trail_index];
230 clauses_.push_back(clause);
231 if (add_clause_callback_ !=
nullptr) add_clause_callback_(lbd, literals);
232 return AttachAndPropagate(clause, trail);
236 Trail* trail,
int lbd) {
238 clauses_.push_back(clause);
239 if (add_clause_callback_ !=
nullptr) add_clause_callback_(lbd, literals);
240 CHECK(AttachAndPropagate(clause, trail));
249bool ClauseManager::AttachAndPropagate(
SatClause* clause,
Trail* trail) {
252 const int size = clause->
size();
253 Literal* literals = clause->literals();
257 int num_literal_not_false = 0;
258 for (
int i = 0;
i < size; ++
i) {
260 std::swap(literals[
i], literals[num_literal_not_false]);
261 ++num_literal_not_false;
262 if (num_literal_not_false == 2) {
271 if (num_literal_not_false == 0)
return false;
273 if (num_literal_not_false == 1) {
276 int max_level = trail->
Info(literals[1].Variable()).
level;
277 for (
int i = 2;
i < size; ++
i) {
278 const int level = trail->
Info(literals[
i].Variable()).
level;
279 if (level > max_level) {
281 std::swap(literals[1], literals[
i]);
287 reasons_[trail->
Index()] = clause;
292 ++num_watched_clauses_;
293 AttachOnFalse(literals[0], literals[1], clause);
294 AttachOnFalse(literals[1], literals[0], clause);
299 Literal* literals = clause->literals();
303 ++num_watched_clauses_;
304 AttachOnFalse(literals[0], literals[1], clause);
305 AttachOnFalse(literals[1], literals[0], clause);
308void ClauseManager::InternalDetach(
SatClause* clause) {
309 --num_watched_clauses_;
310 const size_t size = clause->
size();
311 if (drat_proof_handler_ !=
nullptr && size > 2) {
314 clauses_info_.erase(clause);
319 InternalDetach(clause);
326 InternalDetach(clause);
328 needs_cleaning_.Clear(l);
329 RemoveIf(&(watchers_on_false_[l]), [](
const Watcher& watcher) {
336 if (!all_clauses_are_attached_)
return;
337 all_clauses_are_attached_ =
false;
342 num_watched_clauses_ = 0;
343 watchers_on_false_.clear();
347 if (all_clauses_are_attached_)
return;
348 all_clauses_are_attached_ =
true;
350 needs_cleaning_.ResetAllToFalse();
351 watchers_on_false_.resize(needs_cleaning_.size().value());
355 ++num_watched_clauses_;
356 DCHECK_GE(clause->
size(), 2);
364 DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
365 if (drat_proof_handler_ !=
nullptr) {
366 drat_proof_handler_->AddClause({true_literal});
370 if (!trail_->Assignment().LiteralIsTrue(true_literal)) {
371 trail_->EnqueueWithUnitReason(true_literal);
375 return implication_graph_->Propagate(trail_);
383 DCHECK(!all_clauses_are_attached_);
384 if (drat_proof_handler_ !=
nullptr) {
385 drat_proof_handler_->DeleteClause(clause->
AsSpan());
387 clauses_info_.erase(clause);
392 SatClause* clause, absl::Span<const Literal> new_clause) {
393 if (new_clause.empty())
return false;
396 for (
const Literal l : new_clause) {
397 DCHECK(!trail_->Assignment().LiteralIsAssigned(l));
401 if (new_clause.size() == 1) {
407 if (new_clause.size() == 2) {
408 CHECK(implication_graph_->AddBinaryClause(new_clause[0], new_clause[1]));
413 if (drat_proof_handler_ !=
nullptr) {
415 drat_proof_handler_->AddClause(new_clause);
416 drat_proof_handler_->DeleteClause(clause->
AsSpan());
419 if (all_clauses_are_attached_) {
422 --num_watched_clauses_;
425 needs_cleaning_.Clear(l);
426 RemoveIf(&(watchers_on_false_[l]), [](
const Watcher& watcher) {
432 clause->Rewrite(new_clause);
435 if (all_clauses_are_attached_)
Attach(clause, trail_);
440 absl::Span<const Literal> new_clause) {
441 DCHECK(!new_clause.empty());
442 DCHECK(!all_clauses_are_attached_);
444 for (
const Literal l : new_clause) {
445 DCHECK(!trail_->Assignment().LiteralIsAssigned(l));
449 if (new_clause.size() == 1) {
455 if (new_clause.size() == 2) {
456 implication_graph_->AddBinaryClause(new_clause[0], new_clause[1]);
461 clauses_.push_back(clause);
467 for (
const LiteralIndex index : needs_cleaning_.PositionsSetAtLeastOnce()) {
468 DCHECK(needs_cleaning_[index]);
469 RemoveIf(&(watchers_on_false_[index]), [](
const Watcher& watcher) {
472 needs_cleaning_.Clear(index);
474 needs_cleaning_.NotifyAllClear();
486 const int old_size = clauses_.size();
487 for (
int i = 0;
i < old_size; ++
i) {
488 if (
i == to_minimize_index_) to_minimize_index_ = new_size;
489 if (
i == to_first_minimize_index_) to_first_minimize_index_ = new_size;
490 if (
i == to_probe_index_) to_probe_index_ = new_size;
491 if (clauses_[
i]->IsRemoved()) {
494 clauses_[new_size++] = clauses_[
i];
497 clauses_.resize(new_size);
499 if (to_minimize_index_ > new_size) to_minimize_index_ = new_size;
500 if (to_first_minimize_index_ > new_size) to_first_minimize_index_ = new_size;
501 if (to_probe_index_ > new_size) to_probe_index_ = new_size;
505 for (; to_first_minimize_index_ < clauses_.size();
506 ++to_first_minimize_index_) {
507 if (clauses_[to_first_minimize_index_]->IsRemoved())
continue;
508 if (!
IsRemovable(clauses_[to_first_minimize_index_])) {
512 if (to_minimize_index_ == to_first_minimize_index_) {
513 ++to_minimize_index_;
515 return clauses_[to_first_minimize_index_++];
522 for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
523 if (clauses_[to_minimize_index_]->IsRemoved())
continue;
525 return clauses_[to_minimize_index_++];
532 for (; to_probe_index_ < clauses_.size(); ++to_probe_index_) {
533 if (clauses_[to_probe_index_]->IsRemoved())
continue;
534 return clauses_[to_probe_index_++];
543 bfs_stack_.resize(num_variables << 1);
544 implications_.resize(num_variables << 1);
545 implies_something_.resize(num_variables << 1);
546 might_have_dups_.resize(num_variables << 1);
547 is_redundant_.resize(implications_.size());
548 is_removed_.resize(implications_.size(),
false);
549 estimated_sizes_.resize(implications_.size(), 0);
550 in_direct_implications_.resize(implications_.size(),
false);
551 reasons_.resize(num_variables);
554void BinaryImplicationGraph::NotifyPossibleDuplicate(
Literal a) {
555 if (might_have_dups_[a.
Index()])
return;
556 might_have_dups_[a.
Index()] =
true;
557 to_clean_.push_back(a);
561 for (
const Literal l : to_clean_) {
562 might_have_dups_[l.Index()] =
false;
578 no_constraint_ever_added_ =
false;
580 if (drat_proof_handler_ !=
nullptr) {
585 drat_proof_handler_->AddClause({a,
b});
589 if (is_redundant_[
b.Index()])
b =
Literal(representative_of_[
b.Index()]);
590 if (a ==
b.Negated())
return true;
591 if (a ==
b)
return FixLiteral(a);
593 DCHECK(!is_removed_[a]);
594 DCHECK(!is_removed_[
b]);
596 estimated_sizes_[
b.NegatedIndex()]++;
598 implications_[
b.NegatedIndex()].push_back(a);
600 implies_something_.Set(
b.NegatedIndex());
601 NotifyPossibleDuplicate(a);
602 NotifyPossibleDuplicate(
b);
605 if (enable_sharing_ && add_binary_callback_ !=
nullptr) {
606 add_binary_callback_(a,
b);
609 const auto& assignment = trail_->Assignment();
610 if (trail_->CurrentDecisionLevel() == 0) {
611 DCHECK(!assignment.LiteralIsAssigned(a));
612 DCHECK(!assignment.LiteralIsAssigned(
b));
614 if (assignment.LiteralIsFalse(a)) {
615 if (assignment.LiteralIsAssigned(
b)) {
616 if (assignment.LiteralIsFalse(
b))
return false;
618 reasons_[trail_->Index()] = a;
621 }
else if (assignment.LiteralIsFalse(
b)) {
622 if (!assignment.LiteralIsAssigned(a)) {
623 reasons_[trail_->Index()] =
b;
633 absl::Span<const Literal> at_most_one) {
634 DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
635 if (at_most_one.size() <= 1)
return true;
639 no_constraint_ever_added_ =
false;
644 const int base_index = at_most_one_buffer_.size();
645 at_most_one_buffer_.push_back(
Literal(LiteralIndex(at_most_one.size())));
646 at_most_one_buffer_.insert(at_most_one_buffer_.end(), at_most_one.begin(),
650 return CleanUpAndAddAtMostOnes(base_index);
657bool BinaryImplicationGraph::FixLiteral(
Literal true_literal) {
662 if (drat_proof_handler_ !=
nullptr) {
663 drat_proof_handler_->
AddClause({true_literal});
673bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(
int base_index) {
674 const VariablesAssignment& assignment = trail_->Assignment();
675 int local_end = base_index;
676 const int buffer_size = at_most_one_buffer_.size();
677 for (
int i = base_index;
i < buffer_size;) {
681 const int local_start = local_end;
686 if (
i == at_most_one_iterator_) {
687 at_most_one_iterator_ = local_start;
691 const absl::Span<const Literal> initial_amo = AtMostOne(
i);
692 i += initial_amo.size() + 1;
696 bool set_all_left_to_false =
false;
697 for (
const Literal l : initial_amo) {
698 if (assignment.LiteralIsFalse(l))
continue;
699 if (is_removed_[l])
continue;
700 if (!set_all_left_to_false && assignment.LiteralIsTrue(l)) {
701 set_all_left_to_false =
true;
706 at_most_one_buffer_[local_start] =
707 Literal(LiteralIndex(local_end - local_start - 1));
711 bool some_duplicates =
false;
712 if (!set_all_left_to_false) {
715 Literal* pt = &at_most_one_buffer_[local_start + 1];
716 std::sort(pt, pt + AtMostOne(local_start).size());
719 bool remove_previous =
false;
720 int new_local_end = local_start + 1;
721 for (
const Literal l : AtMostOne(local_start)) {
722 if (l.Index() == previous) {
723 if (assignment.LiteralIsTrue(l))
return false;
724 if (!assignment.LiteralIsFalse(l)) {
725 if (!FixLiteral(l.Negated()))
return false;
727 remove_previous =
true;
728 some_duplicates =
true;
734 if (remove_previous) {
736 remove_previous =
false;
738 previous = l.Index();
739 at_most_one_buffer_[new_local_end++] = l;
741 if (remove_previous) --new_local_end;
744 local_end = new_local_end;
745 at_most_one_buffer_[local_start] =
746 Literal(LiteralIndex(local_end - local_start - 1));
751 if (some_duplicates) {
752 int new_local_end = local_start + 1;
753 for (
const Literal l : AtMostOne(local_start)) {
754 if (assignment.LiteralIsFalse(l))
continue;
755 if (!set_all_left_to_false && assignment.LiteralIsTrue(l)) {
756 set_all_left_to_false =
true;
759 at_most_one_buffer_[new_local_end++] = l;
763 local_end = new_local_end;
764 at_most_one_buffer_[local_start] =
765 Literal(LiteralIndex(local_end - local_start - 1));
769 if (set_all_left_to_false) {
770 for (
const Literal l : AtMostOne(local_start)) {
771 if (assignment.LiteralIsFalse(l))
continue;
772 if (assignment.LiteralIsTrue(l))
return false;
773 if (!FixLiteral(l.Negated()))
return false;
777 local_end = local_start;
782 const absl::Span<const Literal> at_most_one = AtMostOne(local_start);
786 if (at_most_one.size() <= std::max(2, at_most_one_max_expansion_size_)) {
787 for (
const Literal a : at_most_one) {
788 for (
const Literal
b : at_most_one) {
789 if (a ==
b)
continue;
790 implications_[a].push_back(
b.Negated());
791 implies_something_.Set(a);
792 NotifyPossibleDuplicate(a);
797 local_end = local_start;
802 for (
const Literal l : at_most_one) {
803 if (l.Index() >= at_most_ones_.size()) {
804 at_most_ones_.resize(l.Index().value() + 1);
806 DCHECK(!is_redundant_[l]);
807 at_most_ones_[l].push_back(local_start);
808 implies_something_.Set(l);
812 at_most_one_buffer_.resize(local_end);
826 const auto implies_something = implies_something_.view();
827 auto* implications = implications_.data();
831 DCHECK(assignment.LiteralIsTrue(true_literal));
832 if (!implies_something[true_literal])
continue;
837 const absl::Span<const Literal> implied =
838 implications[true_literal.
Index().value()];
839 num_inspections_ += implied.size();
840 for (
const Literal literal : implied) {
841 if (assignment.LiteralIsTrue(literal)) {
851 if (assignment.LiteralIsFalse(literal)) {
863 if (true_literal.
Index() < at_most_ones_.size()) {
864 for (
const int start : at_most_ones_[true_literal]) {
866 for (
const Literal literal : AtMostOne(start)) {
868 if (literal == true_literal) {
875 if (assignment.LiteralIsFalse(literal))
continue;
878 if (assignment.LiteralIsTrue(literal)) {
885 reasons_[trail->
Index()] = true_literal.Negated();
897 const Trail& ,
int trail_index, int64_t )
const {
898 return {&reasons_[trail_index], 1};
909 std::vector<Literal>* conflict) {
915 const LiteralIndex root_literal_index = conflict->front().NegatedIndex();
916 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
917 is_marked_.Set(root_literal_index);
926 const bool also_prune_direct_implication_list =
false;
930 auto& direct_implications = implications_[root_literal_index];
931 for (
const Literal l : direct_implications) {
932 if (is_marked_[l])
continue;
933 dfs_stack_.push_back(l);
934 while (!dfs_stack_.empty()) {
935 const LiteralIndex index = dfs_stack_.back().Index();
936 dfs_stack_.pop_back();
937 if (!is_marked_[index]) {
938 is_marked_.Set(index);
939 for (
const Literal implied : implications_[index]) {
940 if (!is_marked_[implied]) dfs_stack_.push_back(implied);
956 if (also_prune_direct_implication_list) {
963 if (also_prune_direct_implication_list) {
965 for (
const Literal l : direct_implications) {
966 if (!is_marked_[l]) {
968 direct_implications[new_size] = l;
972 if (new_size < direct_implications.size()) {
973 num_redundant_implications_ += direct_implications.size() - new_size;
974 direct_implications.resize(new_size);
978 RemoveRedundantLiterals(conflict);
986 const Trail& trail, std::vector<Literal>* conflict,
989 DCHECK(!conflict->empty());
990 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
991 MarkDescendants(conflict->front().Negated());
992 for (
const LiteralIndex
i : is_marked_.PositionsSetAtLeastOnce()) {
1001 RemoveRedundantLiterals(conflict);
1008 const Trail& , std::vector<Literal>* conflict,
1009 absl::BitGenRef random) {
1011 const LiteralIndex root_literal_index = conflict->front().NegatedIndex();
1012 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
1013 is_marked_.Set(root_literal_index);
1016 auto& direct_implications = implications_[root_literal_index];
1022 std::shuffle(direct_implications.begin(), direct_implications.end(), random);
1024 for (
const Literal l : direct_implications) {
1025 if (is_marked_[l]) {
1031 direct_implications[new_size++] = l;
1032 dfs_stack_.push_back(l);
1033 while (!dfs_stack_.empty()) {
1034 const LiteralIndex index = dfs_stack_.back().Index();
1035 dfs_stack_.pop_back();
1036 if (!is_marked_[index]) {
1037 is_marked_.Set(index);
1038 for (
const Literal implied : implications_[index]) {
1039 if (!is_marked_[implied]) dfs_stack_.push_back(implied);
1044 if (new_size < direct_implications.size()) {
1045 num_redundant_implications_ += direct_implications.size() - new_size;
1046 direct_implications.resize(new_size);
1048 RemoveRedundantLiterals(conflict);
1051void BinaryImplicationGraph::RemoveRedundantLiterals(
1052 std::vector<Literal>* conflict) {
1055 for (
int i = 1;
i < conflict->size(); ++
i) {
1056 if (!is_marked_[(*conflict)[
i].NegatedIndex()]) {
1057 (*conflict)[new_index] = (*conflict)[
i];
1061 if (new_index < conflict->size()) {
1062 ++num_minimization_;
1063 num_literals_removed_ += conflict->size() - new_index;
1064 conflict->resize(new_index);
1070 const Trail& trail, std::vector<Literal>* conflict) {
1072 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
1073 is_simplified_.ClearAndResize(LiteralIndex(implications_.size()));
1074 for (
const Literal lit : *conflict) {
1075 is_marked_.Set(lit);
1091 for (
int i = 1;
i < conflict->size(); ++
i) {
1092 const Literal lit = (*conflict)[
i];
1094 bool keep_literal =
true;
1095 for (
const Literal implied : implications_[lit]) {
1096 if (is_marked_[implied]) {
1097 DCHECK_LE(lit_level, trail.
Info(implied.Variable()).
level);
1098 if (lit_level == trail.
Info(implied.Variable()).
level &&
1099 is_simplified_[implied]) {
1102 keep_literal =
false;
1107 (*conflict)[index] = lit;
1110 is_simplified_.Set(lit);
1113 if (index < conflict->size()) {
1114 ++num_minimization_;
1115 num_literals_removed_ += conflict->size() - index;
1116 conflict->erase(conflict->begin() + index, conflict->end());
1122 DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
1126 const int new_num_fixed = trail_->Index();
1128 if (num_processed_fixed_variables_ == new_num_fixed)
return;
1131 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
1132 for (; num_processed_fixed_variables_ < new_num_fixed;
1133 ++num_processed_fixed_variables_) {
1134 const Literal true_literal = (*trail_)[num_processed_fixed_variables_];
1138 for (
const Literal lit : implications_[true_literal]) {
1139 DCHECK(trail_->Assignment().LiteralIsTrue(lit));
1152 if (lit.NegatedIndex() < representative_of_.size() &&
1155 is_marked_.Set(representative_of_[lit.Negated()]);
1157 is_marked_.Set(lit.NegatedIndex());
1163 if (true_literal.
Index() < at_most_ones_.size()) {
1166 if (true_literal.
NegatedIndex() < at_most_ones_.size()) {
1170 for (
const LiteralIndex
i : is_marked_.PositionsSetAtLeastOnce()) {
1171 RemoveIf(&implications_[
i], [&assignment](
const Literal& lit) {
1178 at_most_ones_.clear();
1179 CHECK(CleanUpAndAddAtMostOnes(0));
1180 DCHECK(InvariantsAreOk());
1195 std::vector<Literal>* at_most_one_buffer)
1197 implications_(*graph),
1198 at_most_ones_(*at_most_ones),
1199 at_most_one_buffer_(*at_most_one_buffer) {}
1203 for (
const Literal l : implications_[LiteralIndex(node)]) {
1204 tmp_.push_back(l.Index().value());
1205 if (finder_.NodeIsInCurrentDfsPath(l.NegatedIndex().value())) {
1209 if (node < at_most_ones_.size()) {
1210 for (
const int start : at_most_ones_[LiteralIndex(node)]) {
1211 if (start >= at_most_one_already_explored_.size()) {
1212 at_most_one_already_explored_.resize(start + 1,
false);
1213 previous_node_to_explore_at_most_one_.resize(start + 1);
1223 if (at_most_one_already_explored_[start]) {
1225 const int first_node = previous_node_to_explore_at_most_one_[start];
1226 DCHECK_NE(node, first_node);
1228 if (finder_.NodeIsInCurrentDfsPath(first_node)) {
1244 previous_node_to_explore_at_most_one_[start] = node;
1249 Literal(LiteralIndex(first_node)).NegatedIndex().value());
1253 at_most_one_already_explored_[start] =
true;
1254 previous_node_to_explore_at_most_one_[start] = node;
1257 const absl::Span<const Literal> amo =
1258 absl::MakeSpan(&at_most_one_buffer_[start + 1],
1259 at_most_one_buffer_[start].Index().value());
1261 if (l.Index() == node)
continue;
1262 tmp_.push_back(l.NegatedIndex().value());
1263 if (finder_.NodeIsInCurrentDfsPath(l.Index().value())) {
1264 to_fix_.push_back(l.Negated());
1283 const std::vector<Literal>& at_most_one_buffer_;
1285 mutable std::vector<int32_t> tmp_;
1288 mutable std::vector<bool> at_most_one_already_explored_;
1289 mutable std::vector<int> previous_node_to_explore_at_most_one_;
1295 if (is_dag_)
return true;
1298 log_info |= VLOG_IS_ON(1);
1304 DCHECK(InvariantsAreOk());
1307 const int32_t size(implications_.size());
1313 SccGraph graph(&finder, &implications_, &at_most_ones_,
1314 &at_most_one_buffer_);
1321 if (!FixLiteral(l))
return false;
1327 is_redundant_.resize(size);
1329 int num_equivalences = 0;
1330 reverse_topological_order_.clear();
1331 for (
int index = 0; index < scc.
size(); ++index) {
1332 const absl::Span<int32_t> component = scc[index];
1341 bool all_fixed =
false;
1342 bool all_true =
false;
1343 for (
const int32_t
i : component) {
1345 if (trail_->Assignment().LiteralIsAssigned(l)) {
1347 all_true = trail_->Assignment().LiteralIsTrue(l);
1352 for (
const int32_t
i : component) {
1354 if (!is_redundant_[l]) {
1355 ++num_redundant_literals_;
1356 is_redundant_.Set(l);
1357 representative_of_[l] = l.
Index();
1362 if (!FixLiteral(l))
return false;
1371 if (component.size() == 1 && is_removed_[LiteralIndex(component[0])]) {
1380 std::sort(component.begin(), component.end());
1381 const LiteralIndex representative(component[0]);
1382 reverse_topological_order_.push_back(representative);
1384 if (component.size() == 1) {
1387 if (num_equivalences > 0) {
1388 auto& representative_list = implications_[representative];
1389 for (
Literal& ref : representative_list) {
1390 const LiteralIndex rep = representative_of_[ref];
1391 if (rep == representative)
continue;
1401 for (
int i = 1;
i < component.size(); ++
i) {
1403 if (!is_redundant_[literal]) {
1404 ++num_redundant_literals_;
1405 is_redundant_.Set(literal);
1407 representative_of_[literal] = representative;
1411 if (
Literal(LiteralIndex(component[
i - 1])).Negated() == literal) {
1412 LOG_IF(INFO, log_info) <<
"Trivially UNSAT in DetectEquivalences()";
1419 auto& representative_list = implications_[representative];
1421 for (
const Literal l : representative_list) {
1423 if (rep.
Index() == representative)
continue;
1424 representative_list[new_size++] = rep;
1426 representative_list.resize(new_size);
1427 for (
int i = 1;
i < component.size(); ++
i) {
1429 auto& ref = implications_[literal];
1432 if (rep.
Index() != representative) representative_list.push_back(rep);
1434 dtime += 1e-8 *
static_cast<double>(ref.size());
1441 representative_list.push_back(literal);
1443 ref.push_back(
Literal(representative));
1446 num_equivalences += component.size() - 1;
1450 if (num_equivalences != 0) {
1454 at_most_ones_.clear();
1456 if (!CleanUpAndAddAtMostOnes(0))
return false;
1469 time_limit_->AdvanceDeterministicTime(dtime);
1470 const int num_fixed_during_scc =
1471 trail_->Index() - num_processed_fixed_variables_;
1473 DCHECK(InvariantsAreOk());
1474 LOG_IF(INFO, log_info) <<
"SCC. " << num_equivalences
1475 <<
" redundant equivalent literals. "
1476 << num_fixed_during_scc <<
" fixed. "
1478 <<
" implications left. " << implications_.size()
1480 <<
" size of at_most_one buffer = "
1481 << at_most_one_buffer_.size() <<
"."
1482 <<
" dtime: " << dtime
1483 <<
" wtime: " << wall_timer.
Get();
1493 DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
1494 if (time_limit_->LimitReached())
return true;
1500 if (time_limit_->LimitReached())
return true;
1503 DCHECK(InvariantsAreOk());
1504 if (time_limit_->LimitReached())
return true;
1506 log_info |= VLOG_IS_ON(1);
1510 int64_t num_fixed = 0;
1511 int64_t num_new_redundant_implications = 0;
1512 bool aborted =
false;
1513 tmp_removed_.clear();
1514 work_done_in_mark_descendants_ = 0;
1515 int marked_index = 0;
1531 const LiteralIndex size(implications_.size());
1533 for (
const LiteralIndex root : reverse_topological_order_) {
1538 if (is_redundant_[root])
continue;
1539 if (trail_->Assignment().LiteralIsAssigned(
Literal(root)))
continue;
1541 auto& direct_implications = implications_[root];
1542 if (direct_implications.empty())
continue;
1551 bool clear_previous_reachability =
true;
1552 for (
const Literal direct_child : direct_implications) {
1553 if (direct_child.Index() == previous) {
1554 clear_previous_reachability =
false;
1555 is_marked_.Clear(previous);
1559 if (clear_previous_reachability) {
1560 is_marked_.ClearAndResize(size);
1565 for (
const Literal direct_child : direct_implications) {
1566 if (is_redundant_[direct_child])
continue;
1567 if (is_marked_[direct_child])
continue;
1571 if (direct_child.Index() == root)
continue;
1575 if (direct_child.NegatedIndex() == root) {
1576 is_marked_.Set(direct_child);
1580 MarkDescendants(direct_child);
1583 is_marked_.Clear(direct_child);
1585 DCHECK(!is_marked_[root])
1586 <<
"DetectEquivalences() should have removed cycles!";
1587 is_marked_.Set(root);
1590 if (root < at_most_ones_.size()) {
1591 auto is_marked = is_marked_.BitsetView();
1592 for (
const int start : at_most_ones_[root]) {
1593 for (
const Literal l : AtMostOne(start)) {
1594 if (l.Index() == root)
continue;
1595 if (!is_marked[l.Negated()] && !is_redundant_[l.Negated()]) {
1596 is_marked_.SetUnsafe(is_marked, l.Negated());
1597 MarkDescendants(l.Negated());
1606 const auto& marked_positions = is_marked_.PositionsSetAtLeastOnce();
1607 for (; marked_index < marked_positions.size(); ++marked_index) {
1608 const LiteralIndex
i = marked_positions[marked_index];
1609 if (is_marked_[
Literal(
i).NegatedIndex()]) {
1611 DCHECK(!trail_->Assignment().LiteralIsAssigned(
Literal(root)));
1617 if (!FixLiteral(
Literal(root).Negated()))
return false;
1625 if (trail_->Assignment().LiteralIsAssigned(
Literal(root)))
continue;
1631 for (
const Literal l : direct_implications) {
1632 if (!is_marked_[l]) {
1633 direct_implications[new_size++] = l;
1635 tmp_removed_.push_back({
Literal(root), l});
1636 DCHECK(!is_redundant_[l]);
1639 const int diff = direct_implications.size() - new_size;
1640 direct_implications.resize(new_size);
1641 direct_implications.shrink_to_fit();
1642 num_new_redundant_implications += diff;
1645 if (work_done_in_mark_descendants_ > 1e8) {
1651 is_marked_.ClearAndResize(size);
1657 absl::flat_hash_set<std::pair<LiteralIndex, LiteralIndex>> removed;
1658 for (
const auto [a,
b] : tmp_removed_) {
1659 removed.insert({a.
Index(),
b.Index()});
1661 for (LiteralIndex
i(0);
i < implications_.size(); ++
i) {
1664 auto& implication = implications_[
i];
1665 for (
const Literal l : implication) {
1666 if (removed.contains({l.NegatedIndex(), negated_i}))
continue;
1667 implication[new_size++] = l;
1669 implication.resize(new_size);
1672 if (num_fixed > 0) {
1675 DCHECK(InvariantsAreOk());
1678 const double dtime = 1e-8 * work_done_in_mark_descendants_;
1679 time_limit_->AdvanceDeterministicTime(dtime);
1680 num_redundant_implications_ += num_new_redundant_implications;
1681 LOG_IF(INFO, log_info) <<
"Transitive reduction removed "
1682 << num_new_redundant_implications <<
" literals. "
1683 << num_fixed <<
" fixed. "
1685 <<
" implications left. " << implications_.size()
1686 <<
" literals." <<
" dtime: " << dtime
1687 <<
" wtime: " << wall_timer.
Get()
1688 << (aborted ?
" Aborted." :
"");
1694int ElementInIntersectionOrMinusOne(absl::Span<const int> a,
1695 absl::Span<const int>
b) {
1696 DCHECK(std::is_sorted(a.begin(), a.end()));
1697 DCHECK(std::is_sorted(
b.begin(),
b.end()));
1698 if (a.empty() ||
b.empty())
return -1;
1702 if (a[
i] ==
b[j])
return a[
i];
1704 if (++
i == a.size())
return -1;
1706 if (++j ==
b.size())
return -1;
1713std::vector<std::pair<int, int>>
1714BinaryImplicationGraph::FilterAndSortAtMostOnes(
1715 absl::Span<std::vector<Literal>> at_most_ones) {
1718 std::vector<std::pair<int, int>> index_size_vector;
1719 const int num_amos = at_most_ones.size();
1720 index_size_vector.reserve(num_amos);
1721 for (
int index = 0; index < num_amos; ++index) {
1722 std::vector<Literal>& clique = at_most_ones[index];
1723 if (clique.size() <= 1)
continue;
1731 for (Literal& ref : clique) {
1732 DCHECK_LT(ref.Index(), representative_of_.size());
1733 const LiteralIndex rep = representative_of_[ref];
1743 std::sort(clique.begin(), clique.end());
1744 for (
int i = 1;
i < clique.size(); ++
i) {
1745 if (clique[
i] == clique[
i - 1] || clique[
i] == clique[
i -
i].Negated()) {
1752 index_size_vector.push_back({index, clique.size()});
1755 index_size_vector.begin(), index_size_vector.end(),
1756 [](
const std::pair<int, int> a,
const std::pair<int, int>&
b) {
1757 return a.second > b.second;
1759 return index_size_vector;
1763 std::vector<std::vector<Literal>>* at_most_ones,
1764 int64_t max_num_explored_nodes) {
1767 work_done_in_mark_descendants_ = 0;
1769 int num_extended = 0;
1770 int num_removed = 0;
1774 std::vector<int> detector_clique_index;
1779 std::vector<int> dense_index_to_index;
1781 max_cliques_containing(implications_.size());
1783 const std::vector<std::pair<int, int>> index_size_vector =
1784 FilterAndSortAtMostOnes(absl::MakeSpan(*at_most_ones));
1786 absl::flat_hash_set<int> cannot_be_removed;
1787 std::vector<bool> was_extended(at_most_ones->size(),
false);
1788 for (
const auto& [index, old_size] : index_size_vector) {
1789 std::vector<Literal>& clique = (*at_most_ones)[index];
1790 if (time_limit_->LimitReached())
break;
1794 if (clique.size() == 2) {
1795 DCHECK_NE(clique[0], clique[1]);
1796 const int dense_index = ElementInIntersectionOrMinusOne(
1797 max_cliques_containing[clique[0]], max_cliques_containing[clique[1]]);
1798 if (dense_index >= 0) {
1799 const int superset_index = dense_index_to_index[dense_index];
1800 if (was_extended[superset_index]) {
1801 cannot_be_removed.insert(superset_index);
1811 detector_clique_index.push_back(index);
1815 if (work_done_in_mark_descendants_ < max_num_explored_nodes) {
1816 clique = ExpandAtMostOne(clique, max_num_explored_nodes);
1820 detector_clique_index.push_back(index);
1824 const int dense_index = dense_index_to_index.size();
1825 dense_index_to_index.push_back(index);
1826 for (
const Literal l : clique) {
1827 max_cliques_containing[l].
push_back(dense_index);
1830 if (clique.size() > old_size) {
1831 was_extended[index] =
true;
1839 const int subset_index = detector_clique_index[subset];
1840 const int superset_index = detector_clique_index[superset];
1841 if (subset_index == superset_index)
return;
1844 if ((*at_most_ones)[subset_index].empty())
return;
1845 if ((*at_most_ones)[superset_index].empty())
return;
1849 if (cannot_be_removed.contains(subset_index))
return;
1852 (*at_most_ones)[subset_index].clear();
1853 if (was_extended[superset_index]) cannot_be_removed.insert(superset_index);
1856 if (num_extended > 0 || num_removed > 0 || num_added > 0) {
1857 VLOG(1) <<
"Clique Extended: " << num_extended
1858 <<
" Removed: " << num_removed <<
" Added: " << num_added
1859 << (work_done_in_mark_descendants_ > max_num_explored_nodes
1867 absl::Span<std::vector<Literal>> at_most_ones,
1868 int64_t max_num_explored_nodes,
double* dtime) {
1871 work_done_in_mark_descendants_ = 0;
1873 const std::vector<std::pair<int, int>> index_size_vector =
1874 FilterAndSortAtMostOnes(at_most_ones);
1877 std::vector<int> detector_clique_index;
1879 for (
const auto& [index, old_size] : index_size_vector) {
1880 if (time_limit_->LimitReached())
break;
1881 detector_clique_index.push_back(index);
1888 detector.IndexAllStorageAsSubsets();
1895 std::vector<int> intersection;
1896 const int num_to_consider = index_size_vector.size();
1897 for (
int subset_index = 0; subset_index < num_to_consider; ++subset_index) {
1898 const int index = index_size_vector[subset_index].first;
1899 std::vector<Literal>& clique = at_most_ones[index];
1900 if (clique.empty())
continue;
1902 if (work_done_in_mark_descendants_ > max_num_explored_nodes)
break;
1903 if (detector.
Stopped())
break;
1908 int next_index_to_try = 0;
1909 intersection.clear();
1910 tmp_bitset_.ClearAndResize(LiteralIndex(implications_.size()));
1911 for (
const Literal l : clique) {
1912 intersection.push_back(l.Index().value());
1917 if (work_done_in_mark_descendants_ > max_num_explored_nodes)
break;
1918 if (detector.
Stopped())
break;
1925 if (clique_i > 0 && intersection.size() == clique.size()) {
1926 clique_i = clique.size();
1928 for (; clique_i < clique.size(); ++clique_i) {
1929 const Literal l = clique[clique_i];
1931 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
1934 if (clique_i == 0) {
1937 for (
const LiteralIndex index :
1938 is_marked_.PositionsSetAtLeastOnce()) {
1940 if (!tmp_bitset_[lit]) {
1941 intersection.push_back(lit.
Index().value());
1949 const int old_size = intersection.size();
1950 for (
int i = 0;
i < old_size; ++
i) {
1951 if (
i == next_index_to_try) {
1952 next_index_to_try = new_size;
1954 const int index = intersection[
i];
1956 if (tmp_bitset_[lit] || is_marked_[lit.
Negated()]) {
1957 intersection[new_size++] = index;
1960 intersection.resize(new_size);
1965 if (intersection.size() <= clique.size())
break;
1971 CHECK_GE(intersection.size(), clique.size());
1980 detector.
FindSubsets(intersection, &next_index_to_try, [&](
int subset) {
1981 if (subset == subset_index) {
1987 for (
const int index : storage[subset]) {
1988 const LiteralIndex lit_index = LiteralIndex(index);
1989 if (tmp_bitset_[lit_index])
continue;
1990 tmp_bitset_.Set(lit_index);
1991 clique.push_back(
Literal(lit_index));
1994 if (num_extra == 0) {
1996 at_most_ones[detector_clique_index[subset]].clear();
2005 if (num_extra == 0)
break;
2008 if (dtime !=
nullptr) {
2010 1e-8 * work_done_in_mark_descendants_ + 1e-9 * detector.
work_done();
2015template <
bool use_weight>
2017 const absl::Span<const Literal> at_most_one,
2020 std::vector<Literal> clique(at_most_one.begin(), at_most_one.end());
2021 std::vector<LiteralIndex> intersection;
2022 const int64_t old_work = work_done_in_mark_descendants_;
2023 for (
int i = 0;
i < clique.size(); ++
i) {
2025 if (work_done_in_mark_descendants_ - old_work > 1e8)
break;
2027 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
2028 MarkDescendants(clique[
i]);
2030 for (
const LiteralIndex index : is_marked_.PositionsSetAtLeastOnce()) {
2031 if (can_be_included[
Literal(index).NegatedIndex()]) {
2032 intersection.push_back(index);
2035 for (
const Literal l : clique) is_marked_.Clear(l.NegatedIndex());
2039 is_marked_.Clear(clique[
i]);
2040 is_marked_.Clear(clique[
i].NegatedIndex());
2041 for (
const LiteralIndex index : intersection) {
2042 if (!is_marked_[index])
continue;
2043 intersection[new_size++] = index;
2045 intersection.resize(new_size);
2046 if (intersection.empty())
break;
2050 if (
i + 1 == clique.size()) {
2053 double max_lp = 0.0;
2054 for (
int j = 0; j < intersection.size(); ++j) {
2059 absl::Uniform<double>(*random_, 0.0, 1e-4)
2060 : can_be_included.size() - intersection[j].value();
2061 if (index == -1 || lp > max_lp) {
2067 clique.push_back(
Literal(intersection[index]).Negated());
2068 std::swap(intersection.back(), intersection[index]);
2069 intersection.pop_back();
2077template std::vector<Literal>
2079 const absl::Span<const Literal> at_most_one,
2082template std::vector<Literal>
2084 const absl::Span<const Literal> at_most_one,
2096const std::vector<std::vector<Literal>>&
2098 absl::Span<const Literal> literals, absl::Span<const double> lp_values,
2099 absl::Span<const double> reduced_costs) {
2101 const int num_literals = implications_.size();
2108 const int size = literals.size();
2109 for (
int i = 0;
i < size; ++
i) {
2111 can_be_included[l] =
true;
2114 const double value = lp_values[
i];
2115 expanded_lp_values[l] = value;
2131 const double rc = reduced_costs[
i];
2132 heuristic_weights[l] = -rc;
2141 bool operator<(
const Candidate& other)
const {
return sum > other.sum; }
2143 std::vector<Candidate> candidates;
2151 std::vector<Literal> fractional_literals;
2152 for (
int i = 0;
i < size; ++
i) {
2153 Literal current_literal = literals[
i];
2154 double current_value = lp_values[
i];
2155 if (trail_->Assignment().LiteralIsAssigned(current_literal))
continue;
2156 if (is_redundant_[current_literal])
continue;
2158 if (current_value < 0.5) {
2159 current_literal = current_literal.
Negated();
2160 current_value = 1.0 - current_value;
2163 if (current_value < 0.99) {
2164 fractional_literals.push_back(current_literal);
2169 double best_value = 0.0;
2170 for (
const Literal l : implications_[current_literal]) {
2171 if (!can_be_included[l])
continue;
2172 const double activity =
2173 current_value + expanded_lp_values[l.NegatedIndex()];
2174 if (activity <= 1.01)
continue;
2175 const double v = activity + absl::Uniform<double>(*random_, 0.0, 1e-4);
2178 best = l.NegatedIndex();
2182 const double activity = current_value + expanded_lp_values[best];
2183 candidates.push_back({current_literal,
Literal(best), activity});
2188 const int kMaxNumberOfCutPerCall = 10;
2189 std::sort(candidates.begin(), candidates.end());
2190 if (candidates.size() > kMaxNumberOfCutPerCall) {
2191 candidates.resize(kMaxNumberOfCutPerCall);
2197 for (
const Candidate& candidate : candidates) {
2199 {candidate.a, candidate.b}, can_be_included, heuristic_weights));
2204 if (fractional_literals.size() > 1) {
2209 const int max_graph_size = 1024;
2210 if (fractional_literals.size() > max_graph_size) {
2211 std::shuffle(fractional_literals.begin(), fractional_literals.end(),
2213 fractional_literals.resize(max_graph_size);
2216 bron_kerbosch_.Initialize(fractional_literals.size() * 2);
2220 tmp_mapping_.resize(implications_.size(), -1);
2221 for (
const Literal l : fractional_literals) {
2222 bron_kerbosch_.SetWeight(
i, expanded_lp_values[l]);
2223 tmp_mapping_[l] =
i++;
2224 bron_kerbosch_.SetWeight(
i, expanded_lp_values[l.Negated()]);
2225 tmp_mapping_[l.Negated()] =
i++;
2234 const int from = tmp_mapping_[l];
2237 const int to = tmp_mapping_[next.Negated()];
2239 bron_kerbosch_.AddEdge(from,
to);
2247 bron_kerbosch_.TakeTransitiveClosureOfImplicationGraph();
2249 bron_kerbosch_.SetWorkLimit(1e8);
2250 bron_kerbosch_.SetMinimumWeight(1.001);
2251 std::vector<std::vector<int>> cliques = bron_kerbosch_.Run();
2255 const int max_num_per_batch = 5;
2256 std::vector<std::pair<int, double>> with_weight =
2257 bron_kerbosch_.GetMutableIndexAndWeight();
2258 if (with_weight.size() > max_num_per_batch) {
2260 with_weight.begin(), with_weight.end(),
2261 [](
const std::pair<int, double>& a,
const std::pair<int, double>&
b) {
2262 return a.second > b.second;
2264 with_weight.resize(max_num_per_batch);
2267 std::vector<Literal> at_most_one;
2268 for (
const auto [index, weight] : with_weight) {
2270 at_most_one.clear();
2271 for (
const int i : cliques[index]) {
2272 const Literal l = fractional_literals[
i / 2];
2273 at_most_one.push_back(
i % 2 == 1 ? l.
Negated() : l);
2282 at_most_one, can_be_included, heuristic_weights));
2286 for (
const Literal l : fractional_literals) {
2287 tmp_mapping_[l] = -1;
2288 tmp_mapping_[l.Negated()] = -1;
2298std::vector<absl::Span<const Literal>>
2300 std::vector<absl::Span<const Literal>> result;
2303 implications_.size(),
false);
2304 for (
const Literal l : *literals) to_consider[l] =
true;
2307 std::priority_queue<std::pair<int, int>> pq;
2313 absl::flat_hash_set<int> explored_amo;
2314 for (
const Literal l : *literals) {
2315 if (l.Index() >= at_most_ones_.size())
continue;
2316 for (
const int start : at_most_ones_[l]) {
2317 const auto [_, inserted] = explored_amo.insert(start);
2318 if (!inserted)
continue;
2320 int intersection_size = 0;
2321 for (
const Literal l : AtMostOne(start)) {
2322 if (to_consider[l]) ++intersection_size;
2324 if (intersection_size > 1) {
2325 pq.push({intersection_size, start});
2329 if (intersection_size == literals->size())
break;
2334 int num_processed = 0;
2335 while (!pq.empty()) {
2336 const auto [old_size, start] = pq.top();
2340 int intersection_size = 0;
2341 for (
const Literal l : AtMostOne(start)) {
2342 if (to_consider[l]) ++intersection_size;
2344 if (intersection_size != old_size) {
2346 if (intersection_size > 1) {
2347 pq.push({intersection_size, start});
2353 for (
const Literal l : AtMostOne(start)) {
2354 to_consider[l] =
false;
2359 const int span_start = num_processed;
2360 for (
int i = num_processed;
i < literals->size(); ++
i) {
2361 if (to_consider[(*literals)[
i]])
continue;
2362 std::swap((*literals)[num_processed], (*literals)[
i]);
2365 result.push_back(absl::MakeSpan(literals->data() + span_start,
2366 num_processed - span_start));
2373 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
2374 return MarkDescendants(root);
2377absl::Span<const Literal> BinaryImplicationGraph::MarkDescendants(
2379 auto*
const stack = bfs_stack_.data();
2381 auto is_redundant = is_redundant_.
const_view();
2385 if (is_redundant[root])
return absl::MakeSpan(stack, 1);
2386 is_marked_.
Set(root);
2387 const int amo_size =
static_cast<int>(at_most_ones_.size());
2388 auto implies_something = implies_something_.
const_view();
2389 for (
int j = 0; j < stack_size; ++j) {
2390 const Literal current = stack[j];
2391 if (!implies_something[current])
continue;
2393 work_done_in_mark_descendants_ += implications_[current].size();
2394 for (
const Literal l : implications_[current]) {
2395 if (!is_marked[l] && !is_redundant[l]) {
2397 stack[stack_size++] = l;
2401 if (current.Index() >= amo_size)
continue;
2402 for (
const int start : at_most_ones_[current]) {
2403 work_done_in_mark_descendants_ += AtMostOne(start).size();
2404 for (
const Literal l : AtMostOne(start)) {
2405 if (l == current)
continue;
2406 if (!is_marked[l.NegatedIndex()] && !is_redundant[l.NegatedIndex()]) {
2407 is_marked_.
SetUnsafe(is_marked, l.NegatedIndex());
2408 stack[stack_size++] = l.Negated();
2413 work_done_in_mark_descendants_ += stack_size;
2414 return absl::MakeSpan(stack, stack_size);
2417std::vector<Literal> BinaryImplicationGraph::ExpandAtMostOne(
2418 const absl::Span<const Literal> at_most_one,
2419 int64_t max_num_explored_nodes) {
2420 std::vector<Literal> clique(at_most_one.begin(), at_most_one.end());
2423 for (
const Literal l : clique) {
2424 if (!implies_something_[l]) {
2432 std::vector<LiteralIndex> intersection;
2433 for (
int i = 0;
i < clique.size(); ++
i) {
2434 if (work_done_in_mark_descendants_ > max_num_explored_nodes)
break;
2435 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
2436 MarkDescendants(clique[
i]);
2439 intersection = is_marked_.PositionsSetAtLeastOnce();
2440 for (
const Literal l : clique) is_marked_.Clear(l.NegatedIndex());
2444 is_marked_.Clear(clique[
i].NegatedIndex());
2445 for (
const LiteralIndex index : intersection) {
2446 if (is_marked_[index]) intersection[new_size++] = index;
2448 intersection.resize(new_size);
2449 if (intersection.empty())
break;
2456 if (
i + 1 == clique.size()) {
2457 clique.push_back(Literal(intersection.back()).Negated());
2458 intersection.pop_back();
2468 DCHECK(!is_removed_[literal]);
2471 for (
const Literal l : direct_implications_) {
2472 in_direct_implications_[l] =
false;
2474 direct_implications_.clear();
2479 for (
const Literal l : implications_[literal]) {
2480 if (l == literal)
continue;
2482 if (!is_removed_[l] && !in_direct_implications_[l]) {
2483 in_direct_implications_[l] =
true;
2484 direct_implications_.push_back(l);
2487 if (literal.
Index() < at_most_ones_.size()) {
2488 if (is_redundant_[literal]) {
2489 DCHECK(at_most_ones_[literal].empty());
2491 for (
const int start : at_most_ones_[literal]) {
2492 for (
const Literal l : AtMostOne(start)) {
2493 if (l == literal)
continue;
2495 if (!is_removed_[l] && !in_direct_implications_[l.NegatedIndex()]) {
2496 in_direct_implications_[l.NegatedIndex()] =
true;
2497 direct_implications_.push_back(l.Negated());
2502 estimated_sizes_[literal] = direct_implications_.size();
2503 return direct_implications_;
2506absl::Span<const Literal> BinaryImplicationGraph::AtMostOne(
int start)
const {
2507 const int size = at_most_one_buffer_[start].Index().value();
2508 return absl::MakeSpan(&at_most_one_buffer_[start + 1], size);
2512 const int size1 = implications_[lhs].size();
2514 lhs.
Index() < at_most_ones_.size() ? at_most_ones_[lhs].size() : 0;
2517 const int choice = absl::Uniform<int>(*random_, 0, size1 + size2);
2518 if (choice < size1) {
2519 return implications_[lhs][choice].Index();
2522 const absl::Span<const Literal> amo =
2523 AtMostOne(at_most_ones_[lhs][choice - size1]);
2524 CHECK_GE(amo.size(), 2);
2525 const int first_choice = absl::Uniform<int>(*random_, 0, amo.size());
2526 const Literal lit = amo[first_choice];
2530 int next_choice = absl::Uniform<int>(*random_, 0, amo.size() - 1);
2531 if (next_choice >= first_choice) {
2534 CHECK_NE(amo[next_choice], lhs);
2535 return amo[next_choice].NegatedIndex();
2546 const Literal literal(var,
true);
2547 direct_implications_of_negated_literal_ =
2550 for (
const Literal l : direct_implications_of_negated_literal_) {
2551 if (in_direct_implications_[l]) {
2553 if (!FixLiteral(l)) {
2564 BooleanVariable var) {
2565 const Literal literal(var,
true);
2567 direct_implications_of_negated_literal_ =
2570 for (
const Literal l : direct_implications_of_negated_literal_) {
2574 DCHECK(!in_direct_implications_[l]);
2577 if (in_direct_implications_[l.NegatedIndex()]) result--;
2584 BooleanVariable var, std::deque<std::vector<Literal>>* postsolve_clauses) {
2585 const Literal literal(var,
true);
2586 DCHECK(!is_removed_[literal.
Index()]);
2587 DCHECK(!is_redundant_[literal.
Index()]);
2589 direct_implications_of_negated_literal_ =
2592 if (is_removed_[
b])
continue;
2593 DCHECK(!is_redundant_[
b]);
2594 estimated_sizes_[
b.NegatedIndex()]--;
2595 for (
const Literal a_negated : direct_implications_of_negated_literal_) {
2596 if (a_negated.Negated() ==
b)
continue;
2597 if (is_removed_[a_negated])
continue;
2601 for (
const Literal a_negated : direct_implications_of_negated_literal_) {
2602 if (is_removed_[a_negated])
continue;
2603 DCHECK(!is_redundant_[a_negated]);
2604 estimated_sizes_[a_negated.NegatedIndex()]--;
2609 for (
const Literal b : direct_implications_) {
2610 if (drat_proof_handler_ !=
nullptr) {
2611 drat_proof_handler_->DeleteClause({
Literal(var,
false),
b});
2613 postsolve_clauses->push_back({
Literal(var,
false),
b});
2615 for (
const Literal a_negated : direct_implications_of_negated_literal_) {
2616 if (drat_proof_handler_ !=
nullptr) {
2617 drat_proof_handler_->DeleteClause({
Literal(var,
true), a_negated});
2619 postsolve_clauses->push_back({
Literal(var,
true), a_negated});
2625 is_removed_[index] =
true;
2626 implications_[index].clear();
2627 if (!is_redundant_[index]) {
2628 ++num_redundant_literals_;
2629 is_redundant_.Set(index);
2635 std::deque<std::vector<Literal>>* postsolve_clauses) {
2636 for (LiteralIndex a(0); a < implications_.size(); ++a) {
2637 if (is_redundant_[a] && !is_removed_[a]) {
2638 postsolve_clauses->push_back(
2640 is_removed_[a] =
true;
2646 auto& implication = implications_[a];
2647 for (
const Literal l : implication) {
2648 if (!is_redundant_[l]) {
2649 implication[new_size++] = l;
2652 implication.resize(new_size);
2658 for (LiteralIndex a(0); a < implications_.size(); ++a) {
2663 for (
const Literal lit : implications_[a]) {
2664 DCHECK(trail_->Assignment().LiteralIsTrue(lit));
2673 auto& implication = implications_[a];
2674 for (
const Literal l : implication) {
2676 implication[new_size++] = l;
2679 implication.resize(new_size);
2683 at_most_ones_.clear();
2684 CHECK(CleanUpAndAddAtMostOnes(0));
2687 DCHECK(InvariantsAreOk());
2690bool BinaryImplicationGraph::InvariantsAreOk() {
2693 absl::flat_hash_set<std::pair<LiteralIndex, LiteralIndex>> seen;
2694 int num_redundant = 0;
2697 for (LiteralIndex a_index(0); a_index < implications_.size(); ++a_index) {
2698 if (time_limit_check.LimitReached())
return true;
2701 if (!implications_[a_index].empty()) {
2702 LOG(ERROR) <<
"Fixed literal has non-cleared implications";
2707 if (is_removed_[a_index]) {
2708 if (!implications_[a_index].empty()) {
2709 LOG(ERROR) <<
"Removed literal has non-cleared implications";
2714 if (is_redundant_[a_index]) {
2716 if (implications_[a_index].size() != 1) {
2718 <<
"Redundant literal should only point to its representative "
2719 << Literal(a_index) <<
" => " << implications_[a_index];
2723 for (
const Literal
b : implications_[a_index]) {
2724 seen.insert({a_index,
b.Index()});
2729 util_intops::StrongVector<LiteralIndex, int> lit_to_order;
2731 lit_to_order.
assign(implications_.size(), -1);
2732 for (
int i = 0;
i < reverse_topological_order_.size(); ++
i) {
2733 lit_to_order[reverse_topological_order_[
i]] =
i;
2737 VLOG(2) <<
"num_redundant " << num_redundant;
2738 VLOG(2) <<
"num_fixed " << num_fixed;
2739 for (LiteralIndex a_index(0); a_index < implications_.size(); ++a_index) {
2740 if (time_limit_check.LimitReached())
return true;
2741 const LiteralIndex not_a_index = Literal(a_index).NegatedIndex();
2742 for (
const Literal
b : implications_[a_index]) {
2743 if (is_removed_[
b]) {
2744 LOG(ERROR) <<
"A removed literal still appear! " << Literal(a_index)
2749 if (!seen.contains({b.NegatedIndex(), not_a_index})) {
2750 LOG(ERROR) <<
"We have " << Literal(a_index) <<
" => " <<
b
2751 <<
" but not the reverse implication!";
2752 LOG(ERROR) <<
"redundant[a]: " << is_redundant_[a_index]
2754 << trail_->Assignment().LiteralIsAssigned(Literal(a_index))
2755 <<
" removed[a]: " << is_removed_[a_index]
2756 <<
" redundant[b]: " << is_redundant_[
b] <<
" assigned[b]: "
2757 << trail_->Assignment().LiteralIsAssigned(
b)
2758 <<
" removed[b]: " << is_removed_[
b];
2764 if (is_dag_ && !is_redundant_[
b] && !is_redundant_[a_index]) {
2765 DCHECK_NE(lit_to_order[
b], -1);
2766 DCHECK_LE(lit_to_order[
b], lit_to_order[a_index]);
2772 absl::flat_hash_set<std::pair<LiteralIndex, int>> lit_to_start;
2773 for (LiteralIndex
i(0);
i < at_most_ones_.size(); ++
i) {
2774 for (
const int start : at_most_ones_[
i]) {
2775 lit_to_start.insert({
i, start});
2779 for (
int start = 0; start < at_most_one_buffer_.size();) {
2780 const absl::Span<const Literal> amo = AtMostOne(start);
2781 for (
const Literal l : amo) {
2782 if (is_removed_[l]) {
2783 LOG(ERROR) <<
"A removed literal still appear in an amo " << l;
2786 if (!lit_to_start.contains({l, start})) {
2790 start += amo.size() + 1;
2797 if (at_most_one_iterator_ >= at_most_one_buffer_.size()) {
2798 return absl::Span<const Literal>();
2801 const absl::Span<const Literal> result = AtMostOne(at_most_one_iterator_);
2802 at_most_one_iterator_ += result.size() + 1;
2810 DCHECK_GE(literals.size(), 2);
2813 clause->size_ = literals.size();
2814 for (
int i = 0;
i < literals.size(); ++
i) {
2815 clause->literals_[
i] = literals[
i];
2834 for (
int i = j;
i < size_; ++
i) {
2838 std::swap(literals_[j], literals_[
i]);
2847 for (
const Literal literal : *
this) {
2855 for (
const Literal literal : *
this) {
2856 if (!result.empty()) result.append(
" ");
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
void Start()
When Start() is called multiple times, only the most recent is used.
ConstView const_view() const
void Set(IntegerType index)
Bitset64< IntegerType >::View BitsetView()
A bit hacky for really hot loop.
void SetUnsafe(typename Bitset64< IntegerType >::View view, IntegerType index)
bool ComputeTransitiveReduction(bool log_info=false)
Literal RepresentativeOf(Literal l) const
void Resize(int num_variables)
Resizes the data structure.
const std::vector< std::vector< Literal > > & GenerateAtMostOnesWithLargeWeight(absl::Span< const Literal > literals, absl::Span< const double > lp_values, absl::Span< const double > reduced_costs)
bool Propagate(Trail *trail) final
SatPropagator interface.
void RemoveDuplicates()
Clean up implications list that might have duplicates.
void MinimizeConflictWithReachability(std::vector< Literal > *c)
std::vector< Literal > ExpandAtMostOneWithWeight(absl::Span< const Literal > at_most_one, const util_intops::StrongVector< LiteralIndex, bool > &can_be_included, const util_intops::StrongVector< LiteralIndex, double > &expanded_lp_values)
Same as ExpandAtMostOne() but try to maximize the weight in the clique.
bool TransformIntoMaxCliques(std::vector< std::vector< Literal > > *at_most_ones, int64_t max_num_explored_nodes=1e8)
absl::Span< const Literal > GetAllImpliedLiterals(Literal root)
void CleanupAllRemovedAndFixedVariables()
int64_t NumImplicationOnVariableRemoval(BooleanVariable var)
bool IsEmpty() const final
Returns true if no constraints where ever added to this class.
bool AddBinaryClause(Literal a, Literal b)
void RemoveFixedVariables()
absl::Span< const Literal > NextAtMostOne()
Returns the next at_most_one, or a span of size 0 when finished.
int64_t ComputeNumImplicationsForLog() const
bool AddImplication(Literal a, Literal b)
void RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
For all possible a => var => b, add a => b.
void MinimizeConflictExperimental(const Trail &trail, std::vector< Literal > *c)
void MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, absl::BitGenRef random)
bool DetectEquivalences(bool log_info=false)
void MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked)
const std::vector< Literal > & DirectImplications(Literal literal)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final
bool MergeAtMostOnes(absl::Span< std::vector< Literal > > at_most_ones, int64_t max_num_explored_nodes=1e8, double *dtime=nullptr)
void RemoveAllRedundantVariables(std::deque< std::vector< Literal > > *postsolve_clauses)
bool FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat)
LiteralIndex RandomImpliedLiteral(Literal lhs)
ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span< const Literal > at_most_one)
std::vector< absl::Span< const Literal > > HeuristicAmoPartition(std::vector< Literal > *literals)
SatClause * InprocessingAddClause(absl::Span< const Literal > new_clause)
void LazyDetach(SatClause *clause)
void InprocessingRemoveClause(SatClause *clause)
These must only be called between [Detach/Attach]AllClauses() calls.
SatClause * NextClauseToMinimize()
bool IsRemovable(SatClause *const clause) const
void Detach(SatClause *clause)
~ClauseManager() override
void DeleteRemovedClauses()
absl::Span< const Literal > Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final
bool AddClause(absl::Span< const Literal > literals, Trail *trail, int lbd)
Adds a new clause and perform initial propagation for this clause only.
SatClause * NextClauseToProbe()
Returns the next clause to probe in round-robin order.
ClauseManager(Model *model)
--— ClauseManager --—
SatClause * ReasonClause(int trail_index) const
SatClause * AddRemovableClause(absl::Span< const Literal > literals, Trail *trail, int lbd)
void Resize(int num_variables)
Must be called before adding clauses referring to such variables.
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)
This one do not need the clause to be detached.
void Attach(SatClause *clause, Trail *trail)
SatClause * NextNewClauseToMinimize()
ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause)
bool Propagate(Trail *trail) final
SatPropagator API.
int AddLiterals(const std::vector< L > &wrapped_values)
size_t size() const
Size of the "key" space, always in [0, size()).
void reserve(int size)
Reserve memory if it is already known or tightly estimated.
void AddClause(absl::Span< const Literal > clause)
void DeleteClause(absl::Span< const Literal > clause)
void AddPotentialSubset(int index)
void DetectInclusions(const std::function< void(int subset, int superset)> &process)
void SetWorkLimit(uint64_t work_limit)
void AddPotentialSuperset(int index)
std::string DebugString() const
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
BooleanVariable Variable() const
Literal FirstLiteral() const
static SatClause * Create(absl::Span< const Literal > literals)
--— SatClause --—
absl::Span< const Literal > AsSpan() const
Returns a Span<> representation of the clause.
const Literal * begin() const
Allows for range based iteration: for (Literal literal : clause) {}.
bool IsSatisfied(const VariablesAssignment &assignment) const
int size() const
Number of literals in the clause.
std::string DebugString() const
bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment &assignment)
Literal SecondLiteral() const
SatPropagator(const std::string &name)
int propagation_trail_index_
util_intops::StrongVector< LiteralIndex, absl::InlinedVector< int32_t, 6 > > AtMostOnes
SccGraph(SccFinder *finder, Implications *graph, AtMostOnes *at_most_ones, std::vector< Literal > *at_most_one_buffer)
int64_t work_done_
For the deterministic time.
util_intops::StrongVector< LiteralIndex, absl::InlinedVector< Literal, 6 > > Implications
StronglyConnectedComponentsFinder< int32_t, SccGraph, CompactVectorVector< int32_t, int32_t > > SccFinder
std::vector< Literal > to_fix_
All these literals where detected to be true during the SCC computation.
const std::vector< int32_t > & operator[](int32_t node) const
void StopProcessingCurrentSubset()
void FindSubsets(absl::Span< const int > superset, int *next_index_to_try, const std::function< void(int subset)> &process)
void StopProcessingCurrentSuperset()
void SetWorkLimit(uint64_t work_limit)
uint64_t work_done() const
std::vector< Literal > * MutableConflict()
void Enqueue(Literal true_literal, int propagator_id)
void EnqueueWithUnitReason(Literal true_literal)
Specific Enqueue() version for a fixed variable.
int CurrentDecisionLevel() const
const AssignmentInfo & Info(BooleanVariable var) const
void SetCurrentPropagatorId(int propagator_id)
void FastEnqueue(Literal true_literal)
const VariablesAssignment & Assignment() const
bool VariableIsAssigned(BooleanVariable var) const
Returns true iff the given variable is assigned.
bool LiteralIsAssigned(Literal literal) const
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
void assign(size_type n, const value_type &val)
void push_back(const value_type &val)
int RemoveIf(RepeatedPtrField< T > *array, const Pred &pr)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
void STLDeleteElements(T *container)
void STLClearObject(T *obj)
const LiteralIndex kNoLiteralIndex(-1)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
trees with all degrees equal to
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)