21#include "absl/memory/memory.h"
39 : initial_num_variables_(num_variables), num_variables_(num_variables) {
40 reverse_mapping_.
resize(num_variables);
41 for (BooleanVariable
var(0);
var < num_variables; ++
var) {
42 reverse_mapping_[
var] =
var;
44 assignment_.
Resize(num_variables);
49 DCHECK(std::find(clause.begin(), clause.end(), x) != clause.end());
50 associated_literal_.push_back(ApplyReverseMapping(x));
51 clauses_start_.push_back(clauses_literals_.size());
52 for (
const Literal& l : clause) {
53 clauses_literals_.push_back(ApplyReverseMapping(l));
58 const Literal l = ApplyReverseMapping(x);
65 if (reverse_mapping_.
size() < mapping.
size()) {
67 while (reverse_mapping_.
size() < mapping.
size()) {
68 reverse_mapping_.
push_back(BooleanVariable(num_variables_++));
70 assignment_.
Resize(num_variables_);
72 for (BooleanVariable v(0); v < mapping.
size(); ++v) {
73 const BooleanVariable image = mapping[v];
75 if (image >= new_mapping.
size()) {
78 new_mapping[image] = reverse_mapping_[v];
82 std::swap(new_mapping, reverse_mapping_);
89 reverse_mapping_.
push_back(BooleanVariable(num_variables_++));
91 assignment_.
Resize(num_variables_);
99void SatPostsolver::Postsolve(VariablesAssignment* assignment)
const {
102 for (BooleanVariable
var(0);
var < assignment->NumberOfVariables(); ++
var) {
103 if (!assignment->VariableIsAssigned(
var)) {
104 assignment->AssignFromTrueLiteral(Literal(
var,
true));
108 int previous_start = clauses_literals_.size();
109 for (
int i =
static_cast<int>(clauses_start_.size()) - 1; i >= 0; --i) {
110 bool set_associated_var =
true;
111 const int new_start = clauses_start_[i];
112 for (
int j = new_start; j < previous_start; ++j) {
113 if (assignment->LiteralIsTrue(clauses_literals_[j])) {
114 set_associated_var =
false;
118 previous_start = new_start;
119 if (set_associated_var) {
120 assignment->UnassignLiteral(associated_literal_[i].Negated());
121 assignment->AssignFromTrueLiteral(associated_literal_[i]);
126 assignment->Resize(initial_num_variables_);
134 solution[
var.value()] =
141 const std::vector<bool>& solution) {
142 for (BooleanVariable
var(0);
var < solution.size(); ++
var) {
149 Postsolve(&assignment_);
150 std::vector<bool> postsolved_solution;
151 postsolved_solution.reserve(initial_num_variables_);
152 for (
int i = 0; i < initial_num_variables_; ++i) {
153 postsolved_solution.push_back(
156 return postsolved_solution;
162 DCHECK_GT(clause.size(), 0) <<
"Added an empty clause to the presolver";
164 clauses_.push_back(std::vector<Literal>(clause.begin(), clause.end()));
165 in_clause_to_process_.push_back(
true);
166 clause_to_process_.push_back(ci);
168 bool changed =
false;
169 std::vector<Literal>& clause_ref = clauses_.back();
170 if (!equiv_mapping_.
empty()) {
171 for (
int i = 0; i < clause_ref.size(); ++i) {
172 const Literal old_literal = clause_ref[i];
173 clause_ref[i] =
Literal(equiv_mapping_[clause_ref[i].
Index()]);
174 if (old_literal != clause_ref[i]) changed =
true;
177 std::sort(clause_ref.begin(), clause_ref.end());
178 clause_ref.erase(std::unique(clause_ref.begin(), clause_ref.end()),
182 for (
int i = 1; i < clause_ref.size(); ++i) {
183 if (clause_ref[i] == clause_ref[i - 1].Negated()) {
185 ++num_trivial_clauses_;
186 clause_to_process_.pop_back();
188 in_clause_to_process_.pop_back();
194 signatures_.push_back(ComputeSignatureOfClauseVariables(ci));
195 DCHECK_EQ(signatures_.size(), clauses_.size());
197 if (drat_proof_handler_ !=
nullptr && changed) {
198 drat_proof_handler_->
AddClause(clause_ref);
202 const Literal max_literal = clause_ref.back();
203 const int required_size =
std::max(max_literal.
Index().value(),
206 if (required_size > literal_to_clauses_.
size()) {
207 literal_to_clauses_.
resize(required_size);
208 literal_to_clause_sizes_.
resize(required_size);
211 literal_to_clauses_[e.Index()].
push_back(ci);
212 literal_to_clause_sizes_[e.Index()]++;
217 const int required_size = 2 * num_variables;
218 if (required_size > literal_to_clauses_.
size()) {
219 literal_to_clauses_.
resize(required_size);
220 literal_to_clause_sizes_.
resize(required_size);
224void SatPresolver::AddClauseInternal(std::vector<Literal>* clause) {
225 if (drat_proof_handler_ !=
nullptr) drat_proof_handler_->
AddClause(*clause);
227 DCHECK(std::is_sorted(clause->begin(), clause->end()));
228 DCHECK_GT(clause->size(), 0) <<
"TODO(fdid): Unsat during presolve?";
230 clauses_.push_back(std::vector<Literal>());
231 clauses_.back().swap(*clause);
232 in_clause_to_process_.push_back(
true);
233 clause_to_process_.push_back(ci);
234 for (
const Literal e : clauses_.back()) {
235 literal_to_clauses_[e.Index()].
push_back(ci);
236 literal_to_clause_sizes_[e.Index()]++;
237 UpdatePriorityQueue(e.Variable());
238 UpdateBvaPriorityQueue(e.Index());
241 signatures_.push_back(ComputeSignatureOfClauseVariables(ci));
242 DCHECK_EQ(signatures_.size(), clauses_.size());
248 BooleanVariable new_var(0);
265 var_pq_elements_.
clear();
266 in_clause_to_process_.clear();
267 clause_to_process_.clear();
268 literal_to_clauses_.
clear();
274 for (BooleanVariable
index : mapping) {
278 std::vector<Literal> temp;
280 for (std::vector<Literal>& clause_ref : clauses_) {
291bool SatPresolver::ProcessAllClauses() {
292 int num_skipped_checks = 0;
293 const int kCheckFrequency = 1000;
297 std::sort(clause_to_process_.begin(), clause_to_process_.end(),
299 return clauses_[c1].size() < clauses_[c2].size();
301 while (!clause_to_process_.empty()) {
303 in_clause_to_process_[ci] =
false;
304 clause_to_process_.pop_front();
306 if (++num_skipped_checks >= kCheckFrequency) {
307 if (num_inspected_signatures_ + num_inspected_literals_ > 1e9) {
308 VLOG(1) <<
"Aborting ProcessAllClauses() because work limit has been "
312 if (time_limit_ !=
nullptr && time_limit_->
LimitReached())
return true;
313 num_skipped_checks = 0;
333 int64 num_removable = 0;
334 for (
const bool b : can_be_removed) {
335 if (
b) ++num_removable;
337 LOG(
INFO) <<
"num removable Booleans: " << num_removable <<
" / "
338 << can_be_removed.size();
339 LOG(
INFO) <<
"num trivial clauses: " << num_trivial_clauses_;
345 if (!ProcessAllClauses())
return false;
346 if (log_info) DisplayStats(timer.
Get());
348 if (time_limit_ !=
nullptr && time_limit_->
LimitReached())
return true;
349 if (num_inspected_signatures_ + num_inspected_literals_ > 1e9)
return true;
351 InitializePriorityQueue();
352 while (var_pq_.
Size() > 0) {
353 const BooleanVariable
var = var_pq_.
Top()->variable;
355 if (!can_be_removed[
var.value()])
continue;
357 if (!ProcessAllClauses())
return false;
359 if (time_limit_ !=
nullptr && time_limit_->
LimitReached())
return true;
360 if (num_inspected_signatures_ + num_inspected_literals_ > 1e9)
return true;
362 if (log_info) DisplayStats(timer.
Get());
365 if (parameters_.presolve_use_bva()) {
367 if (log_info) DisplayStats(timer.
Get());
374 var_pq_elements_.
clear();
375 InitializeBvaPriorityQueue();
376 while (bva_pq_.
Size() > 0) {
377 const LiteralIndex lit = bva_pq_.
Top()->literal;
384void SatPresolver::SimpleBva(LiteralIndex l) {
385 literal_to_p_size_.
resize(literal_to_clauses_.
size(), 0);
386 DCHECK(std::all_of(literal_to_p_size_.
begin(), literal_to_p_size_.
end(),
387 [](
int v) { return v == 0; }));
392 m_cls_ = literal_to_clauses_[l];
399 flattened_p_.clear();
401 const std::vector<Literal>& clause = clauses_[c];
402 if (clause.empty())
continue;
406 const LiteralIndex l_min =
407 FindLiteralWithShortestOccurrenceListExcluding(clause, Literal(l));
412 for (
const ClauseIndex d : literal_to_clauses_[l_min]) {
413 if (clause.size() != clauses_[d].size())
continue;
414 const LiteralIndex l_diff =
417 if (l_diff == Literal(l).NegatedIndex()) {
422 VLOG(1) <<
"self-subsumbtion";
425 flattened_p_.push_back({l_diff, c});
426 const int new_size = ++literal_to_p_size_[l_diff];
427 if (new_size > max_size) {
435 const int new_m_lit_size = m_lit_.size() + 1;
436 const int new_m_cls_size = max_size;
437 const int new_reduction =
438 new_m_lit_size * new_m_cls_size - new_m_cls_size - new_m_lit_size;
440 if (new_reduction <= reduction)
break;
448 reduction = new_reduction;
453 for (
const auto entry : flattened_p_) {
454 literal_to_p_size_[entry.first] = 0;
455 if (entry.first == lmax) m_cls_.
push_back(entry.second);
457 flattened_p_.clear();
461 for (
const auto entry : flattened_p_) literal_to_p_size_[entry.first] = 0;
462 flattened_p_.
clear();
467 if (reduction <= parameters_.presolve_bva_threshold())
return;
471 const int old_size = literal_to_clauses_.
size();
472 const LiteralIndex x_true = LiteralIndex(old_size);
473 const LiteralIndex x_false = LiteralIndex(old_size + 1);
474 literal_to_clauses_.
resize(old_size + 2);
475 literal_to_clause_sizes_.
resize(old_size + 2);
476 bva_pq_elements_.resize(old_size + 2);
477 bva_pq_elements_[x_true.value()].literal = x_true;
478 bva_pq_elements_[x_false.value()].literal = x_false;
481 if (drat_proof_handler_ !=
nullptr) drat_proof_handler_->
AddOneVariable();
482 for (
const LiteralIndex lit : m_lit_) {
483 tmp_new_clause_ = {Literal(lit), Literal(x_true)};
484 AddClauseInternal(&tmp_new_clause_);
487 tmp_new_clause_ = clauses_[ci];
488 DCHECK(!tmp_new_clause_.empty());
489 for (Literal& ref : tmp_new_clause_) {
490 if (ref.Index() == l) {
491 ref = Literal(x_false);
499 std::sort(tmp_new_clause_.begin(), tmp_new_clause_.end());
500 AddClauseInternal(&tmp_new_clause_);
510 const std::vector<Literal>& clause = clauses_[c];
512 const LiteralIndex l_min =
513 FindLiteralWithShortestOccurrenceListExcluding(clause, Literal(l));
514 for (
const LiteralIndex lit : m_lit_) {
515 if (lit == l)
continue;
516 for (
const ClauseIndex d : literal_to_clauses_[l_min]) {
517 if (clause.size() != clauses_[d].size())
continue;
518 const LiteralIndex l_diff =
534 AddToBvaPriorityQueue(x_true);
535 AddToBvaPriorityQueue(x_false);
536 AddToBvaPriorityQueue(l);
539uint64 SatPresolver::ComputeSignatureOfClauseVariables(ClauseIndex ci) {
541 for (
const Literal l : clauses_[ci]) {
542 signature |= (
uint64{1} << (l.Variable().value() % 64));
544 DCHECK_EQ(signature == 0, clauses_[ci].empty());
551bool SatPresolver::ProcessClauseToSimplifyOthersUsingLiteral(
552 ClauseIndex clause_index, Literal lit) {
553 const std::vector<Literal>& clause = clauses_[clause_index];
554 const uint64 clause_signature = signatures_[clause_index];
555 LiteralIndex opposite_literal;
560 bool need_cleaning =
false;
561 num_inspected_signatures_ += literal_to_clauses_[lit.Index()].
size();
562 for (
const ClauseIndex ci : literal_to_clauses_[lit.Index()]) {
563 const uint64 ci_signature = signatures_[ci];
567 DCHECK_EQ(ci_signature, ComputeSignatureOfClauseVariables(ci));
568 if (ci_signature == 0) {
569 need_cleaning =
true;
576 if (ci != clause_index && (clause_signature & ~ci_signature) == 0 &&
578 &num_inspected_literals_)) {
580 need_cleaning =
true;
584 DCHECK_NE(opposite_literal, lit.Index());
585 if (clauses_[ci].empty())
return false;
586 if (drat_proof_handler_ !=
nullptr) {
588 drat_proof_handler_->
AddClause(clauses_[ci]);
592 signatures_[ci] = ComputeSignatureOfClauseVariables(ci);
598 --literal_to_clause_sizes_[opposite_literal];
599 UpdatePriorityQueue(Literal(opposite_literal).Variable());
601 if (!in_clause_to_process_[ci]) {
602 in_clause_to_process_[ci] =
true;
603 clause_to_process_.push_back(ci);
611 auto& occurrence_list_ref = literal_to_clauses_[lit.Index()];
613 if (signatures_[ci] != 0) occurrence_list_ref[new_index++] = ci;
615 occurrence_list_ref.
resize(new_index);
616 DCHECK_EQ(literal_to_clause_sizes_[lit.Index()], new_index);
626 const std::vector<Literal>& clause = clauses_[clause_index];
627 if (clause.empty())
return true;
628 DCHECK(std::is_sorted(clause.begin(), clause.end()));
630 LiteralIndex opposite_literal;
631 const Literal lit = FindLiteralWithShortestOccurrenceList(clause);
633 if (!ProcessClauseToSimplifyOthersUsingLiteral(clause_index, lit)) {
639 const LiteralIndex other_lit_index =
640 FindLiteralWithShortestOccurrenceListExcluding(clause, lit);
642 literal_to_clause_sizes_[other_lit_index] <
644 return ProcessClauseToSimplifyOthersUsingLiteral(clause_index,
649 bool something_removed =
false;
650 auto& occurrence_list_ref = literal_to_clauses_[lit.
NegatedIndex()];
651 const uint64 clause_signature = signatures_[clause_index];
653 const uint64 ci_signature = signatures_[ci];
654 DCHECK_EQ(ci_signature, ComputeSignatureOfClauseVariables(ci));
655 if (ci_signature == 0)
continue;
661 if ((clause_signature & ~ci_signature) == 0 &&
663 &num_inspected_literals_)) {
665 if (clauses_[ci].empty())
return false;
666 if (drat_proof_handler_ !=
nullptr) {
668 drat_proof_handler_->
AddClause(clauses_[ci]);
672 signatures_[ci] = ComputeSignatureOfClauseVariables(ci);
674 if (!in_clause_to_process_[ci]) {
675 in_clause_to_process_[ci] =
true;
676 clause_to_process_.push_back(ci);
678 something_removed =
true;
681 occurrence_list_ref[new_index] = ci;
684 occurrence_list_ref.resize(new_index);
685 literal_to_clause_sizes_[lit.
NegatedIndex()] = new_index;
686 if (something_removed) {
693void SatPresolver::RemoveAndRegisterForPostsolveAllClauseContaining(
Literal x) {
695 if (!clauses_[i].empty()) RemoveAndRegisterForPostsolve(i, x);
698 literal_to_clause_sizes_[x.
Index()] = 0;
702 const int s1 = literal_to_clause_sizes_[x.
Index()];
703 const int s2 = literal_to_clause_sizes_[x.
NegatedIndex()];
707 if (s1 == 0 && s2 == 0)
return false;
711 if (s1 > 1 && s2 > 1 && s1 * s2 > parameters_.presolve_bve_threshold()) {
717 const int clause_weight = parameters_.presolve_bve_clause_weight();
719 if (!clauses_[i].empty()) {
720 threshold += clause_weight + clauses_[i].size();
724 if (!clauses_[i].empty()) {
725 threshold += clause_weight + clauses_[i].size();
735 if (clauses_[i].empty())
continue;
736 bool no_resolvant =
true;
738 if (clauses_[j].empty())
continue;
741 no_resolvant =
false;
742 size += clause_weight + rs;
745 if (size > threshold)
return false;
748 if (no_resolvant && parameters_.presolve_blocked_clause()) {
761 RemoveAndRegisterForPostsolve(i, x);
768 std::vector<Literal> temp;
770 if (clauses_[i].empty())
continue;
772 if (clauses_[j].empty())
continue;
774 AddClauseInternal(&temp);
783 RemoveAndRegisterForPostsolveAllClauseContaining(x);
784 RemoveAndRegisterForPostsolveAllClauseContaining(x.
Negated());
791void SatPresolver::Remove(ClauseIndex ci) {
793 for (
Literal e : clauses_[ci]) {
794 literal_to_clause_sizes_[e.Index()]--;
795 UpdatePriorityQueue(e.Variable());
796 UpdateBvaPriorityQueue(
Literal(e.Variable(),
true).
Index());
797 UpdateBvaPriorityQueue(
Literal(e.Variable(),
false).
Index());
799 if (drat_proof_handler_ !=
nullptr) {
805void SatPresolver::RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x) {
806 postsolver_->
Add(x, clauses_[ci]);
810Literal SatPresolver::FindLiteralWithShortestOccurrenceList(
811 const std::vector<Literal>& clause) {
813 Literal result = clause.front();
814 int best_size = literal_to_clause_sizes_[result.Index()];
815 for (
const Literal l : clause) {
816 const int size = literal_to_clause_sizes_[l.Index()];
817 if (size < best_size) {
825LiteralIndex SatPresolver::FindLiteralWithShortestOccurrenceListExcluding(
826 const std::vector<Literal>& clause, Literal to_exclude) {
830 for (
const Literal l : clause) {
831 if (l == to_exclude)
continue;
832 if (literal_to_clause_sizes_[l.Index()] < num_occurrences) {
834 num_occurrences = literal_to_clause_sizes_[l.Index()];
840void SatPresolver::UpdatePriorityQueue(BooleanVariable
var) {
841 if (var_pq_elements_.
empty())
return;
842 PQElement* element = &var_pq_elements_[
var];
843 element->weight = literal_to_clause_sizes_[Literal(
var,
true).Index()] +
844 literal_to_clause_sizes_[Literal(
var,
false).Index()];
848 var_pq_.
Add(element);
852void SatPresolver::InitializePriorityQueue() {
854 var_pq_elements_.
resize(num_vars);
855 for (BooleanVariable
var(0);
var < num_vars; ++
var) {
856 PQElement* element = &var_pq_elements_[
var];
857 element->variable =
var;
858 element->weight = literal_to_clause_sizes_[Literal(
var,
true).Index()] +
859 literal_to_clause_sizes_[Literal(
var,
false).Index()];
860 var_pq_.
Add(element);
864void SatPresolver::UpdateBvaPriorityQueue(LiteralIndex lit) {
865 if (bva_pq_elements_.empty())
return;
867 BvaPqElement* element = &bva_pq_elements_[lit.value()];
868 element->weight = literal_to_clause_sizes_[lit];
874void SatPresolver::AddToBvaPriorityQueue(LiteralIndex lit) {
875 if (bva_pq_elements_.empty())
return;
877 BvaPqElement* element = &bva_pq_elements_[lit.value()];
878 element->weight = literal_to_clause_sizes_[lit];
880 if (element->weight > 2) bva_pq_.
Add(element);
883void SatPresolver::InitializeBvaPriorityQueue() {
886 bva_pq_elements_.assign(num_literals, BvaPqElement());
887 for (LiteralIndex lit(0); lit < num_literals; ++lit) {
888 BvaPqElement* element = &bva_pq_elements_[lit.value()];
889 element->literal = lit;
890 element->weight = literal_to_clause_sizes_[lit];
894 if (element->weight > 2) bva_pq_.
Add(element);
898void SatPresolver::DisplayStats(
double elapsed_seconds) {
899 int num_literals = 0;
901 int num_singleton_clauses = 0;
902 for (
const std::vector<Literal>& c : clauses_) {
904 if (c.size() == 1) ++num_singleton_clauses;
906 num_literals += c.size();
909 int num_one_side = 0;
910 int num_simple_definition = 0;
913 const int s1 = literal_to_clause_sizes_[Literal(
var,
true).Index()];
914 const int s2 = literal_to_clause_sizes_[Literal(
var,
false).Index()];
915 if (s1 == 0 && s2 == 0)
continue;
918 if (s1 == 0 || s2 == 0) {
920 }
else if (s1 == 1 || s2 == 1) {
921 num_simple_definition++;
924 LOG(
INFO) <<
" [" << elapsed_seconds <<
"s]"
925 <<
" clauses:" << num_clauses <<
" literals:" << num_literals
926 <<
" vars:" << num_vars <<
" one_side_vars:" << num_one_side
927 <<
" simple_definition:" << num_simple_definition
928 <<
" singleton_clauses:" << num_singleton_clauses;
932 LiteralIndex* opposite_literal,
933 int64* num_inspected_literals) {
934 if (
b->size() <
a.size())
return false;
935 DCHECK(std::is_sorted(
a.begin(),
a.end()));
936 DCHECK(std::is_sorted(
b->begin(),
b->end()));
937 if (num_inspected_literals !=
nullptr) {
938 *num_inspected_literals +=
a.size();
939 *num_inspected_literals +=
b->size();
942 *opposite_literal = LiteralIndex(-1);
945 std::vector<Literal>::const_iterator ia =
a.begin();
946 std::vector<Literal>::const_iterator ib =
b->begin();
947 std::vector<Literal>::const_iterator to_remove;
951 int size_diff =
b->size() -
a.size();
952 while (ia !=
a.end() ) {
956 }
else if (*ia == ib->Negated()) {
958 if (num_diff > 1)
return false;
962 }
else if (*ia < *ib) {
969 if (--size_diff < 0)
return false;
973 *opposite_literal = to_remove->Index();
980 const std::vector<Literal>&
b,
Literal l) {
982 DCHECK(std::is_sorted(
a.begin(),
a.end()));
983 DCHECK(std::is_sorted(
b.begin(),
b.end()));
985 std::vector<Literal>::const_iterator ia =
a.begin();
986 std::vector<Literal>::const_iterator ib =
b.begin();
987 while (ia !=
a.end() && ib !=
b.end()) {
991 }
else if (*ia < *ib) {
1000 result = (*ib).Index();
1006 if (ib !=
b.end()) {
1008 result = (*ib).Index();
1014 const std::vector<Literal>&
b,
1015 std::vector<Literal>* out) {
1016 DCHECK(std::is_sorted(
a.begin(),
a.end()));
1017 DCHECK(std::is_sorted(
b.begin(),
b.end()));
1020 std::vector<Literal>::const_iterator ia =
a.begin();
1021 std::vector<Literal>::const_iterator ib =
b.begin();
1022 while ((ia !=
a.end()) && (ib !=
b.end())) {
1024 out->push_back(*ia);
1027 }
else if (*ia == ib->Negated()) {
1028 if (*ia != x)
return false;
1032 }
else if (*ia < *ib) {
1033 out->push_back(*ia);
1036 out->push_back(*ib);
1042 out->insert(out->end(), ia,
a.end());
1043 out->insert(out->end(), ib,
b.end());
1049 const std::vector<Literal>&
b) {
1050 DCHECK(std::is_sorted(
a.begin(),
a.end()));
1051 DCHECK(std::is_sorted(
b.begin(),
b.end()));
1053 int size =
static_cast<int>(
a.size() +
b.size()) - 2;
1054 std::vector<Literal>::const_iterator ia =
a.begin();
1055 std::vector<Literal>::const_iterator ib =
b.begin();
1056 while ((ia !=
a.end()) && (ib !=
b.end())) {
1061 }
else if (*ia == ib->Negated()) {
1062 if (*ia != x)
return -1;
1066 }
else if (*ia < *ib) {
1087 deterministic_time_limit(solver->deterministic_time() +
1088 deterministic_time_limit) {}
1094 scratchpad_.clear();
1122 mutable std::vector<int32> scratchpad_;
1124 const double deterministic_time_limit;
1141 solver->
parameters().presolve_probing_deterministic_time_limit(), solver);
1143 std::vector<std::vector<int32>> scc;
1156 for (
const std::vector<int32>& component : scc) {
1157 if (component.size() > 1) {
1158 if (mapping->
empty()) mapping->
resize(size, LiteralIndex(-1));
1160 for (
int i = 1; i < component.size(); ++i) {
1161 const Literal l((LiteralIndex(component[i])));
1182 if (!mapping->
empty()) {
1192 for (LiteralIndex i(0); i < size; ++i) {
1200 if (drat_proof_handler !=
nullptr) {
1201 drat_proof_handler->
AddClause({true_lit});
1205 for (LiteralIndex i(0); i < size; ++i) {
1207 (*mapping)[i] = rep;
1214 if (drat_proof_handler !=
nullptr) {
1215 drat_proof_handler->
AddClause({true_lit});
1224 if (drat_proof_handler !=
nullptr) {
1225 drat_proof_handler->
AddClause({true_lit});
1228 }
else if (rep != i) {
1231 if (drat_proof_handler !=
nullptr) {
1238 const bool log_info =
1240 LOG_IF(
INFO, log_info) <<
"Probing. fixed " << num_already_fixed_vars <<
" + "
1242 num_already_fixed_vars
1243 <<
" equiv " << num_equiv / 2 <<
" total "
1249 std::vector<bool>* solution,
1252 const SatParameters
parameters = (*solver)->parameters();
1265 VLOG(1) <<
"UNSAT during probing.";
1268 const int num_variables = (*solver)->NumVariables();
1269 if ((*solver)->LiteralTrail().Index() == num_variables) {
1270 VLOG(1) <<
"Problem solved by trivial heuristic!";
1272 for (
int i = 0; i < (*solver)->NumVariables(); ++i) {
1273 solution->push_back((*solver)->Assignment().LiteralIsTrue(
1274 Literal(BooleanVariable(i),
true)));
1282 const int max_num_passes = 4;
1283 for (
int i = 0; i < max_num_passes && !
time_limit->LimitReached(); ++i) {
1284 const int saved_num_variables = (*solver)->NumVariables();
1299 parameters.presolve_probing_deterministic_time_limit();
1302 VLOG(1) <<
"UNSAT during probing.";
1306 postsolver.
Add(c[0], c);
1314 drat_proof_handler, &equiv_map);
1315 if ((*solver)->IsModelUnsat()) {
1316 VLOG(1) <<
"UNSAT during probing.";
1321 if (!(*solver)->ProblemIsPureSat()) {
1322 VLOG(1) <<
"The problem is not a pure SAT problem, skipping the SAT "
1323 "specific presolve.";
1329 (*solver)->Backtrack(0);
1330 for (
int i = 0; i < (*solver)->LiteralTrail().
Index(); ++i) {
1331 postsolver.
FixVariable((*solver)->LiteralTrail()[i]);
1339 (*solver)->ExtractClauses(&presolver);
1340 (*solver)->AdvanceDeterministicTime(
time_limit);
1344 time_limit->AdvanceDeterministicTime((*solver)
1346 ->GetOrCreate<TimeLimit>()
1347 ->GetElapsedDeterministicTime());
1349 (*solver).reset(
nullptr);
1350 std::vector<bool> can_be_removed(presolver.
NumVariables(),
true);
1351 if (!presolver.
Presolve(can_be_removed, log_info)) {
1352 VLOG(1) <<
"UNSAT during presolve.";
1355 (*solver) = absl::make_unique<SatSolver>();
1360 if (drat_proof_handler !=
nullptr) {
1365 (*solver) = absl::make_unique<SatSolver>();
1366 (*solver)->SetDratProofHandler(drat_proof_handler);
1371 if ((*solver)->NumVariables() == saved_num_variables)
break;
1391 model->GetOrCreate<SatParameters>()
1392 ->presolve_probing_deterministic_time_limit();
1397 postsolver.
Add(c[0], c);
#define LOG_IF(severity, condition)
#define DCHECK_NE(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
void NoteChangedPriority(T *val)
bool Contains(const T *val) const
void resize(size_type new_size)
void push_back(const value_type &x)
int MergePartsOf(int node1, int node2)
int GetRootAndCompressPath(int node)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
void DeleteClause(absl::Span< const Literal > clause)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
void AddClause(absl::Span< const Literal > clause)
bool PresolveLoop(SatPresolveOptions options)
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
BooleanVariable Variable() const
Class that owns everything related to a particular optimization model.
PropagationGraph(double deterministic_time_limit, SatSolver *solver)
const std::vector< int32 > & operator[](int32 index) const
void Add(Literal x, const absl::Span< const Literal > clause)
SatPostsolver(int num_variables)
void FixVariable(Literal x)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
std::vector< bool > PostsolveSolution(const std::vector< bool > &solution)
std::vector< bool > ExtractAndPostsolveSolution(const SatSolver &solver)
void SetNumVariables(int num_variables)
void LoadProblemIntoSatSolver(SatSolver *solver)
void AddBinaryClause(Literal a, Literal b)
void SetEquivalentLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping)
void SetParameters(const SatParameters ¶ms)
absl::StrongVector< BooleanVariable, BooleanVariable > VariableMapping() const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
void AddClause(absl::Span< const Literal > clause)
bool ProcessClauseToSimplifyOthers(ClauseIndex clause_index)
bool CrossProduct(Literal x)
void SetNumVariables(int num_variables)
const SatParameters & parameters() const
const VariablesAssignment & Assignment() const
const Trail & LiteralTrail() const
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void Backtrack(int target_level)
int CurrentDecisionLevel() const
double deterministic_time() const
bool AddProblemClause(absl::Span< const Literal > literals)
bool AddUnitClause(Literal true_literal)
bool LiteralIsAssigned(Literal literal) const
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
void AssignFromTrueLiteral(Literal literal)
void Resize(int num_variables)
SharedTimeLimit * time_limit
void STLClearObject(T *obj)
void STLEraseAllFromSequence(T *v, const E &e)
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
int ComputeResolvantSize(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b)
const LiteralIndex kNoLiteralIndex(-1)
SatSolver::Status SolveWithPresolve(std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler)
const BooleanVariable kNoBooleanVariable(-1)
LiteralIndex DifferAtGivenLiteral(const std::vector< Literal > &a, const std::vector< Literal > &b, Literal l)
bool ComputeResolvant(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b, std::vector< Literal > *out)
void ProbeAndFindEquivalentLiteral(SatSolver *solver, SatPostsolver *postsolver, DratProofHandler *drat_proof_handler, absl::StrongVector< LiteralIndex, LiteralIndex > *mapping)
bool SimplifyClause(const std::vector< Literal > &a, std::vector< Literal > *b, LiteralIndex *opposite_literal, int64 *num_inspected_literals)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
std::deque< std::vector< Literal > > clauses
bool use_transitive_reduction
bool extract_binary_clauses_in_probing
double deterministic_time_limit
#define VLOG_IS_ON(verboselevel)