16 #include "absl/container/inlined_vector.h"
29 clauses.emplace_back(clause.begin(), clause.end());
30 for (
int i = 0; i < clause.size(); ++i) {
40 #define RETURN_IF_FALSE(f) \
41 if (!(f)) return false;
51 double probing_time = 0.0;
83 !implication_graph_->
IsDag()) {
89 !implication_graph_->
IsDag()) {
96 blocked_clause_simplifier_->
DoOneRound(log_round_info);
102 const double time_left =
104 if (time_left <= 0)
break;
106 probing_options.
log_info = log_round_info;
114 !implication_graph_->
IsDag()) {
126 <<
" num_fixed: " << trail_->
Index()
134 <<
" non-probing time: " << (
wall_timer.
Get() - probing_time);
146 double probing_time = 0.0;
150 if (total_dtime_ > 0.1 * start_dtime)
return true;
166 probing_options.
log_info = log_round_info;
187 blocked_clause_simplifier_->
DoOneRound(log_round_info);
194 <<
" num_fixed: " << trail_->
Index()
201 <<
" non-probing time: " << (
wall_timer.
Get() - probing_time);
207 #undef RETURN_IF_FALSE
210 const int64 new_num_fixed_variables = trail_->
Index();
211 return last_num_fixed_variables_ < new_num_fixed_variables;
215 const int64 new_num_redundant_literals =
217 return last_num_redundant_literals_ < new_num_redundant_literals;
232 if (!implication_graph_->
IsDag()) {
238 if (use_transitive_reduction) {
265 const int64 new_num_redundant_literals =
267 const int64 new_num_fixed_variables = trail_->
Index();
268 if (last_num_redundant_literals_ == new_num_redundant_literals &&
269 last_num_fixed_variables_ == new_num_fixed_variables) {
272 last_num_fixed_variables_ = new_num_fixed_variables;
273 last_num_redundant_literals_ = new_num_redundant_literals;
279 int64 num_removed_literals = 0;
280 int64 num_inspected_literals = 0;
284 std::vector<Literal> new_clause;
287 const int num_literals(sat_solver_->
NumVariables() * 2);
293 bool removed =
false;
294 bool need_rewrite =
false;
297 for (
const Literal l : clause->AsSpan()) {
304 num_removed_literals += clause->size();
314 num_inspected_literals += clause->size();
315 if (removed || !need_rewrite)
continue;
316 num_inspected_literals += clause->size();
320 for (
const Literal l : clause->AsSpan()) {
327 num_removed_literals += clause->size();
331 marked[r.
Index()] =
true;
336 for (
const Literal l : new_clause) marked[l.Index()] =
false;
337 if (removed)
continue;
339 num_removed_literals += clause->
size() - new_clause.size();
346 const double dtime =
static_cast<double>(num_inspected_literals) * 1e-8;
348 LOG_IF(
INFO, log_info) <<
"Cleanup. num_removed_literals: "
349 << num_removed_literals <<
" dtime: " << dtime
363 int64 num_subsumed_clauses = 0;
364 int64 num_removed_literals = 0;
365 int64 num_inspected_signatures = 0;
366 int64 num_inspected_literals = 0;
370 std::vector<Literal> new_clause;
382 std::vector<SatClause*> clauses =
384 std::sort(clauses.begin(), clauses.end(),
388 const LiteralIndex num_literals(sat_solver_->
NumVariables() * 2);
394 num_literals.value());
397 std::vector<uint64> signatures(clauses.size());
399 std::vector<Literal> candidates_for_removal;
400 for (
int clause_index = 0; clause_index < clauses.size(); ++clause_index) {
401 SatClause* clause = clauses[clause_index];
407 if (num_inspected_literals + num_inspected_signatures > 1e9) {
425 marked.
Set(l.Index());
426 signature |= (
uint64{1} << (l.Variable().value() % 64));
432 bool removed =
false;
433 candidates_for_removal.clear();
434 const uint64 mask = ~signature;
436 num_inspected_signatures += one_watcher[l.Index()].
size();
437 for (
const int i : one_watcher[l.Index()]) {
438 if ((mask & signatures[i]) != 0)
continue;
440 bool subsumed =
true;
441 bool stengthen =
true;
443 num_inspected_literals += clauses[i]->size();
444 for (
const Literal o : clauses[i]->AsSpan()) {
445 if (!marked[o.Index()]) {
448 to_remove = o.NegatedIndex();
456 ++num_subsumed_clauses;
457 num_removed_literals += clause->
size();
464 candidates_for_removal.push_back(
Literal(to_remove));
469 if (removed)
continue;
473 num_inspected_signatures += one_watcher[l.NegatedIndex()].
size();
474 for (
const int i : one_watcher[l.NegatedIndex()]) {
475 if ((mask & signatures[i]) != 0)
continue;
477 bool stengthen =
true;
478 num_inspected_literals += clauses[i]->size();
479 for (
const Literal o : clauses[i]->AsSpan()) {
480 if (o == l.Negated())
continue;
481 if (!marked[o.Index()]) {
487 candidates_for_removal.push_back(l);
498 if (!candidates_for_removal.empty()) {
501 new_clause.push_back(l);
505 for (
const Literal l : new_clause) {
506 if (l == candidates_for_removal[0])
continue;
507 new_clause[new_size++] = l;
509 CHECK_EQ(new_size + 1, new_clause.size());
510 new_clause.resize(new_size);
512 num_removed_literals += clause->
size() - new_clause.size();
516 if (clause->
size() == 0)
continue;
521 signature |= (
uint64{1} << (l.Variable().value() % 64));
542 if (one_watcher[l.Index()].
size() < min_size) {
543 min_size = one_watcher[l.Index()].
size();
544 min_literal = l.Index();
554 signatures[clause_index] = signature;
555 one_watcher[min_literal].
push_back(clause_index);
563 const double dtime =
static_cast<double>(num_inspected_signatures) * 1e-8 +
564 static_cast<double>(num_inspected_literals) * 5e-9;
566 LOG_IF(
INFO, log_info) <<
"Subsume. num_removed_literals: "
567 << num_removed_literals
568 <<
" num_subsumed: " << num_subsumed_clauses
569 <<
" dtime: " << dtime
579 num_subsumed_clauses_ = 0;
580 num_removed_literals_ = 0;
583 if (implication_graph_->
literal_size() == 0)
return true;
586 if (!stamps_are_already_computed_) {
595 stamps_are_already_computed_ =
false;
602 LOG_IF(
INFO, log_info) <<
"Stamping. num_removed_literals: "
603 << num_removed_literals_
604 <<
" num_subsumed: " << num_subsumed_clauses_
605 <<
" num_fixed: " << num_fixed_ <<
" dtime: " << dtime_
616 if (implication_graph_->
literal_size() == 0)
return true;
623 stamps_are_already_computed_ =
true;
629 <<
" num_fixed: " << num_fixed_ <<
" dtime: " << dtime_
638 for (LiteralIndex i(0); i < size; ++i) {
651 const auto& children_of_not_l =
653 if (children_of_not_l.empty())
continue;
654 for (
int num_tries = 0; num_tries < 10; ++num_tries) {
656 children_of_not_l[absl::Uniform<int>(*random_, 0,
657 children_of_not_l.size())]
659 if (implication_graph_->
IsRedundant(candidate))
continue;
660 if (i == candidate.
Index())
continue;
663 parents_[i] = candidate.
Index();
674 for (LiteralIndex i(0); i < size; ++i) {
675 if (parents_[i] == i)
continue;
676 sizes_[parents_[i]]++;
681 starts_[LiteralIndex(0)] = 0;
682 for (LiteralIndex i(1); i <= size; ++i) {
683 starts_[i] = starts_[i - 1] + sizes_[i - 1];
687 children_.resize(size);
688 for (LiteralIndex i(0); i < size; ++i) {
689 if (parents_[i] == i)
continue;
690 children_[starts_[parents_[i]]++] = i;
694 for (LiteralIndex i(0); i < size; ++i) {
695 starts_[i] -= sizes_[i];
699 CHECK_EQ(starts_[LiteralIndex(0)], 0);
700 for (LiteralIndex i(1); i <= size; ++i) {
701 CHECK_EQ(starts_[i], starts_[i - 1] + sizes_[i - 1]);
707 first_stamps_.
resize(size);
708 last_stamps_.
resize(size);
709 marked_.
assign(size,
false);
710 for (LiteralIndex i(0); i < size; ++i) {
711 if (parents_[i] != i)
continue;
713 const LiteralIndex tree_root = i;
714 dfs_stack_.push_back(i);
715 while (!dfs_stack_.empty()) {
716 const LiteralIndex top = dfs_stack_.back();
718 dfs_stack_.pop_back();
719 last_stamps_[top] = stamp++;
722 first_stamps_[top] = stamp++;
727 if (marked_[
Literal(top).NegatedIndex()] &&
728 first_stamps_[
Literal(top).NegatedIndex()] >=
729 first_stamps_[tree_root]) {
732 LiteralIndex lca = top;
733 while (first_stamps_[lca] > first_stamp) {
742 const int end = starts_[top + 1];
743 for (
int j = starts_[top]; j < end; ++j) {
745 DCHECK(!marked_[children_[j]]);
746 dfs_stack_.push_back(children_[j]);
760 bool operator<(
const Entry& o)
const {
return start < o.start; }
762 std::vector<int> to_remove;
763 std::vector<Literal> new_clause;
764 std::vector<Entry> entries;
768 const auto span = clause->AsSpan();
769 if (span.empty())
continue;
778 for (
int i = 0; i < span.size(); ++i) {
784 entries.push_back({i,
false, first_stamps_[span[i].Index()],
785 last_stamps_[span[i].
Index()]});
786 entries.push_back({i,
true, first_stamps_[span[i].NegatedIndex()],
787 last_stamps_[span[i].NegatedIndex()]});
789 if (clause->empty())
continue;
792 if (!entries.empty()) {
793 const double n =
static_cast<double>(entries.size());
794 dtime_ += 1.5e-8 * n * std::log(n);
795 std::sort(entries.begin(), entries.end());
801 for (
const Entry& e : entries) {
802 if (e.end < top_entry.end) {
804 const Literal lhs = top_entry.is_negated ? span[top_entry.i].
Negated()
806 const Literal rhs = e.is_negated ? span[e.i].
Negated() : span[e.i];
809 if (top_entry.is_negated != e.is_negated) {
811 if (top_entry.i == e.i) {
813 if (top_entry.is_negated) {
822 span[top_entry.i].Negated())) {
825 to_remove.push_back(top_entry.i);
834 if (top_entry.is_negated) {
835 num_subsumed_clauses_++;
841 if (top_entry.is_negated) {
843 to_remove.push_back(e.i);
852 to_remove.push_back(top_entry.i);
860 if (clause->empty())
continue;
863 if (!to_remove.empty() || entries.size() < span.size()) {
866 int to_remove_index = 0;
867 for (
int i = 0; i < span.size(); ++i) {
868 if (to_remove_index < to_remove.size() &&
869 i == to_remove[to_remove_index]) {
878 new_clause.push_back(span[i]);
880 num_removed_literals_ += span.size() - new_clause.size();
894 num_blocked_clauses_ = 0;
895 num_inspected_literals_ = 0;
897 InitializeForNewRound();
899 while (!time_limit_->
LimitReached() && !queue_.empty()) {
900 const Literal l = queue_.front();
901 in_queue_[l.
Index()] =
false;
907 literal_to_clauses_.
clear();
909 dtime_ += 1e-8 * num_inspected_literals_;
912 LOG_IF(
INFO, log_info) <<
"Blocked clause. num_blocked_clauses: "
913 << num_blocked_clauses_ <<
" dtime: " << dtime_
917 void BlockedClauseSimplifier::InitializeForNewRound() {
925 clauses_.push_back(c);
927 const int num_literals = clause_manager_->
literal_size();
931 in_queue_.
assign(num_literals,
true);
932 for (LiteralIndex l(0); l < num_literals; ++l) {
933 queue_.push_back(Literal(l));
936 marked_.
resize(num_literals);
938 std::all_of(marked_.
begin(), marked_.
end(), [](
bool b) { return !b; }));
942 literal_to_clauses_.
clear();
943 literal_to_clauses_.
resize(num_literals);
944 for (ClauseIndex i(0); i < clauses_.size(); ++i) {
945 for (
const Literal l : clauses_[i]->AsSpan()) {
946 literal_to_clauses_[l.Index()].
push_back(i);
948 num_inspected_literals_ += clauses_[i]->size();
952 void BlockedClauseSimplifier::ProcessLiteral(Literal current_literal) {
954 if (implication_graph_->
IsRemoved(current_literal))
return;
969 const std::vector<Literal>& implications =
971 for (
const Literal l : implications) {
972 if (l == current_literal)
continue;
974 marked_[l.Index()] =
true;
980 std::vector<ClauseIndex> clauses_to_process;
981 for (
const ClauseIndex i : literal_to_clauses_[current_literal.Index()]) {
982 if (clauses_[i]->empty())
continue;
988 if (num_binary > 0) {
989 if (clauses_[i]->size() <= num_binary)
continue;
990 int num_with_negation_marked = 0;
991 for (
const Literal l : clauses_[i]->AsSpan()) {
992 if (l == current_literal)
continue;
993 if (marked_[l.NegatedIndex()]) {
994 ++num_with_negation_marked;
997 num_inspected_literals_ += clauses_[i]->size();
998 if (num_with_negation_marked < num_binary)
continue;
1000 clauses_to_process.push_back(i);
1004 for (
const Literal l : implications) {
1005 marked_[l.Index()] =
false;
1016 for (
const ClauseIndex i : clauses_to_process) {
1017 const auto c = clauses_[i]->AsSpan();
1018 if (ClauseIsBlocked(current_literal, c)) {
1025 for (
const Literal l : c) {
1026 if (!in_queue_[l.NegatedIndex()]) {
1027 in_queue_[l.NegatedIndex()] =
true;
1028 queue_.push_back(l.Negated());
1036 ++num_blocked_clauses_;
1043 bool BlockedClauseSimplifier::ClauseIsBlocked(
1044 Literal current_literal, absl::Span<const Literal> clause) {
1045 bool is_blocked =
true;
1046 for (
const Literal l : clause) marked_[l.Index()] =
true;
1050 for (
const ClauseIndex i :
1051 literal_to_clauses_[current_literal.NegatedIndex()]) {
1052 if (clauses_[i]->empty())
continue;
1053 bool some_marked =
false;
1054 for (
const Literal l : clauses_[i]->AsSpan()) {
1056 ++num_inspected_literals_;
1058 if (l == current_literal.Negated())
continue;
1059 if (marked_[l.NegatedIndex()]) {
1070 for (
const Literal l : clause) marked_[l.Index()] =
false;
1079 num_inspected_literals_ = 0;
1080 num_eliminated_variables_ = 0;
1081 num_literals_diff_ = 0;
1082 num_clauses_diff_ = 0;
1083 num_simplifications_ = 0;
1084 num_blocked_clauses_ = 0;
1095 clauses_.push_back(c);
1097 const int num_literals = clause_manager_->
literal_size();
1098 const int num_variables = num_literals / 2;
1100 literal_to_clauses_.
clear();
1101 literal_to_clauses_.
resize(num_literals);
1102 literal_to_num_clauses_.
assign(num_literals, 0);
1103 for (ClauseIndex i(0); i < clauses_.size(); ++i) {
1104 for (
const Literal l : clauses_[i]->AsSpan()) {
1105 literal_to_clauses_[l.Index()].
push_back(i);
1106 literal_to_num_clauses_[l.Index()]++;
1108 num_inspected_literals_ += clauses_[i]->size();
1111 const int saved_trail_index = trail_->
Index();
1112 propagation_index_ = trail_->
Index();
1114 need_to_be_updated_.clear();
1115 in_need_to_be_updated_.
resize(num_variables);
1116 queue_.
Reserve(num_variables);
1117 for (BooleanVariable v(0); v < num_variables; ++v) {
1120 UpdatePriorityQueue(v);
1123 marked_.
resize(num_literals);
1125 std::all_of(marked_.
begin(), marked_.
end(), [](
bool b) { return !b; }));
1131 const BooleanVariable top = queue_.
Top().var;
1139 bool is_unsat =
false;
1140 if (!Propagate())
return false;
1142 if (!Propagate())
return false;
1144 if (is_unsat)
return false;
1146 if (!CrossProduct(top))
return false;
1148 for (
const BooleanVariable v : need_to_be_updated_) {
1149 in_need_to_be_updated_[v] =
false;
1152 if (v != top) UpdatePriorityQueue(v);
1154 in_need_to_be_updated_.
clear();
1155 need_to_be_updated_.clear();
1164 bool remove =
false;
1165 for (
const Literal l : c->AsSpan()) {
1175 literal_to_clauses_.
clear();
1176 literal_to_num_clauses_.
clear();
1178 dtime_ += 1e-8 * num_inspected_literals_;
1183 << trail_->
Index() - saved_trail_index
1184 <<
" num_simplified_literals: " << num_simplifications_
1185 <<
" num_blocked_clauses_: " << num_blocked_clauses_
1186 <<
" num_eliminations: " << num_eliminated_variables_
1187 <<
" num_literals_diff: " << num_literals_diff_
1188 <<
" num_clause_diff: " << num_clauses_diff_
1189 <<
" dtime: " << dtime_
1194 bool BoundedVariableElimination::RemoveLiteralFromClause(
1196 num_literals_diff_ -= sat_clause->
size();
1200 literal_to_num_clauses_[l.Index()]--;
1204 num_clauses_diff_--;
1208 resolvant_.push_back(l);
1213 if (sat_clause->
empty()) {
1214 --num_clauses_diff_;
1215 for (
const Literal l : resolvant_) literal_to_num_clauses_[l.Index()]--;
1217 num_literals_diff_ += sat_clause->
size();
1222 bool BoundedVariableElimination::Propagate() {
1223 for (; propagation_index_ < trail_->
Index(); ++propagation_index_) {
1225 if (!implication_graph_->
Propagate(trail_))
return false;
1227 const Literal l = (*trail_)[propagation_index_];
1228 for (
const ClauseIndex
index : literal_to_clauses_[l.Index()]) {
1229 if (clauses_[
index]->empty())
continue;
1230 num_clauses_diff_--;
1231 num_literals_diff_ -= clauses_[
index]->size();
1234 literal_to_clauses_[l.Index()].
clear();
1235 for (
const ClauseIndex
index : literal_to_clauses_[l.NegatedIndex()]) {
1236 if (clauses_[
index]->empty())
continue;
1237 if (!RemoveLiteralFromClause(l.Negated(), clauses_[
index]))
return false;
1239 literal_to_clauses_[l.NegatedIndex()].
clear();
1246 int BoundedVariableElimination::NumClausesContaining(Literal l) {
1247 return literal_to_num_clauses_[l.Index()] +
1252 void BoundedVariableElimination::UpdatePriorityQueue(BooleanVariable
var) {
1254 const int priority = -NumClausesContaining(Literal(
var,
true)) -
1255 NumClausesContaining(Literal(
var,
false));
1259 queue_.
Add({
var, priority});
1263 void BoundedVariableElimination::DeleteClause(SatClause* sat_clause) {
1264 const auto clause = sat_clause->AsSpan();
1266 num_clauses_diff_--;
1267 num_literals_diff_ -= clause.size();
1270 for (
const Literal l : clause) {
1271 literal_to_num_clauses_[l.Index()]--;
1272 if (!in_need_to_be_updated_[l.Variable()]) {
1273 in_need_to_be_updated_[l.Variable()] =
true;
1274 need_to_be_updated_.push_back(l.Variable());
1282 void BoundedVariableElimination::DeleteAllClausesContaining(Literal
literal) {
1283 for (
const ClauseIndex i : literal_to_clauses_[
literal.Index()]) {
1284 const auto clause = clauses_[i]->AsSpan();
1285 if (clause.empty())
continue;
1287 DeleteClause(clauses_[i]);
1292 void BoundedVariableElimination::AddClause(absl::Span<const Literal> clause) {
1294 if (pt ==
nullptr)
return;
1296 num_clauses_diff_++;
1297 num_literals_diff_ += clause.size();
1299 const ClauseIndex
index(clauses_.size());
1300 clauses_.push_back(pt);
1301 for (
const Literal l : clause) {
1302 literal_to_num_clauses_[l.Index()]++;
1304 if (!in_need_to_be_updated_[l.Variable()]) {
1305 in_need_to_be_updated_[l.Variable()] =
true;
1306 need_to_be_updated_.push_back(l.Variable());
1311 template <
bool score_only,
bool with_binary_only>
1312 bool BoundedVariableElimination::ResolveAllClauseContaining(Literal lit) {
1313 const int clause_weight = parameters_.presolve_bve_clause_weight();
1315 const std::vector<Literal>& implications =
1317 auto& clause_containing_lit = literal_to_clauses_[lit.Index()];
1318 for (
int i = 0; i < clause_containing_lit.size(); ++i) {
1319 const ClauseIndex clause_index = clause_containing_lit[i];
1320 const auto clause = clauses_[clause_index]->AsSpan();
1321 if (clause.empty())
continue;
1323 if (!score_only) resolvant_.clear();
1324 for (
const Literal l : clause) {
1325 if (!score_only && l != lit) resolvant_.push_back(l);
1326 marked_[l.Index()] =
true;
1328 num_inspected_literals_ += clause.size() + implications.size();
1332 bool clause_can_be_simplified =
false;
1333 const int64 saved_score = new_score_;
1336 for (
const Literal l : implications) {
1338 if (marked_[l.NegatedIndex()])
continue;
1339 if (marked_[l.Index()]) {
1340 clause_can_be_simplified =
true;
1344 new_score_ += clause_weight + clause.size();
1346 resolvant_.push_back(l);
1347 AddClause(resolvant_);
1348 resolvant_.pop_back();
1354 if (!with_binary_only && !clause_can_be_simplified) {
1355 auto& clause_containing_not_lit = literal_to_clauses_[lit.NegatedIndex()];
1356 for (
int j = 0; j < clause_containing_not_lit.size(); ++j) {
1357 if (score_only && new_score_ > score_threshold_)
break;
1358 const ClauseIndex other_index = clause_containing_not_lit[j];
1359 const auto other = clauses_[other_index]->AsSpan();
1360 if (other.empty())
continue;
1361 bool trivial =
false;
1363 for (
const Literal l : other) {
1365 ++num_inspected_literals_;
1366 if (l == lit.Negated())
continue;
1367 if (marked_[l.NegatedIndex()]) {
1371 if (!marked_[l.Index()]) {
1373 if (!score_only) resolvant_.push_back(l);
1377 if (!score_only) resolvant_.resize(resolvant_.size() - extra_size);
1383 if (score_only && clause.size() + extra_size <= other.size()) {
1384 CHECK_EQ(clause.size() + extra_size, other.size());
1385 ++num_simplifications_;
1389 score_threshold_ -= clause_weight + other.size();
1391 if (extra_size == 0) {
1395 DeleteClause(clauses_[other_index]);
1397 if (!RemoveLiteralFromClause(lit.Negated(),
1398 clauses_[other_index])) {
1401 std::swap(clause_containing_not_lit[j],
1402 clause_containing_not_lit.back());
1403 clause_containing_not_lit.pop_back();
1409 if (extra_size == 0) {
1410 clause_can_be_simplified =
true;
1415 if (clause.size() - 1 + extra_size > 100) {
1416 new_score_ = score_threshold_ + 1;
1420 new_score_ += clause_weight + clause.size() - 1 + extra_size;
1422 AddClause(resolvant_);
1423 resolvant_.resize(resolvant_.size() - extra_size);
1430 for (
const Literal l : clause) marked_[l.Index()] =
false;
1433 if (clause_can_be_simplified) {
1434 ++num_simplifications_;
1437 new_score_ = saved_score;
1438 score_threshold_ -= clause_weight + clause.size();
1440 if (!RemoveLiteralFromClause(lit, clauses_[clause_index]))
return false;
1441 std::swap(clause_containing_lit[i], clause_containing_lit.back());
1442 clause_containing_lit.pop_back();
1446 if (score_only && new_score_ > score_threshold_)
return true;
1458 if (score_only && !with_binary_only && !clause_can_be_simplified &&
1459 new_score_ == saved_score) {
1460 ++num_blocked_clauses_;
1461 score_threshold_ -= clause_weight + clause.size();
1463 DeleteClause(clauses_[clause_index]);
1469 bool BoundedVariableElimination::CrossProduct(BooleanVariable
var) {
1472 const Literal lit(
var,
true);
1473 const Literal not_lit(
var,
false);
1475 const int s1 = NumClausesContaining(lit);
1476 const int s2 = NumClausesContaining(not_lit);
1477 if (s1 == 0 && s2 == 0)
return true;
1478 if (s1 > 0 && s2 == 0) {
1479 num_eliminated_variables_++;
1481 DeleteAllClausesContaining(lit);
1484 if (s1 == 0 && s2 > 0) {
1485 num_eliminated_variables_++;
1487 DeleteAllClausesContaining(not_lit);
1495 num_eliminated_variables_++;
1502 if (s1 > 1 && s2 > 1 && s1 * s2 > parameters_.presolve_bve_threshold()) {
1515 const int clause_weight = parameters_.presolve_bve_clause_weight();
1519 (clause_weight + 2);
1520 for (
const ClauseIndex i : literal_to_clauses_[lit.Index()]) {
1521 const auto c = clauses_[i]->AsSpan();
1522 if (!c.empty()) score += clause_weight + c.size();
1524 for (
const ClauseIndex i : literal_to_clauses_[not_lit.Index()]) {
1525 const auto c = clauses_[i]->AsSpan();
1526 if (!c.empty()) score += clause_weight + c.size();
1537 score_threshold_ = score;
1539 (clause_weight + 2);
1540 if (new_score_ > score_threshold_)
return true;
1541 if (!ResolveAllClauseContaining<
true,
1545 if (new_score_ > score_threshold_)
return true;
1546 if (!ResolveAllClauseContaining<
true,
1550 if (new_score_ > score_threshold_)
return true;
1553 if (new_score_ > 0) {
1554 if (!ResolveAllClauseContaining<
false,
1558 if (!ResolveAllClauseContaining<
false,
1564 ++num_eliminated_variables_;
1566 DeleteAllClausesContaining(lit);
1567 DeleteAllClausesContaining(not_lit);
#define LOG_IF(severity, condition)
#define DCHECK_NE(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK(condition)
#define DCHECK_EQ(val1, val2)
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
void push_back(const value_type &x)
bool Contains(int index) const
void ChangePriority(Element element)
void Add(Element element)
void Set(IntegerType index)
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
double GetElapsedDeterministicTime() const
Returns the elapsed deterministic time since the construction of this object.
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
int64 num_redundant_literals() const
bool Propagate(Trail *trail) final
bool ComputeTransitiveReduction(bool log_info=false)
int64 literal_size() const
int64 num_implications() const
Literal RepresentativeOf(Literal l) const
const std::vector< Literal > & DirectImplications(Literal literal)
bool IsRedundant(Literal l) const
bool DetectEquivalences(bool log_info=false)
void CleanupAllRemovedVariables()
void RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal >> *postsolve_clauses)
bool FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat)
void RemoveFixedVariables()
bool IsRemoved(Literal l) const
int64 NumImplicationOnVariableRemoval(BooleanVariable var)
int DirectImplicationsEstimatedSize(Literal literal) const
void DoOneRound(bool log_info)
bool DoOneRound(bool log_info)
bool PresolveLoop(SatPresolveOptions options)
bool MoreFixedVariableToClean() const
bool RemoveFixedAndEquivalentVariables(bool log_info)
bool LevelZeroPropagate()
bool MoreRedundantVariableToClean() const
bool SubsumeAndStrenghtenRound(bool log_info)
bool DetectEquivalencesAndStamp(bool use_transitive_reduction, bool log_info)
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
const std::vector< SatClause * > & AllClausesInCreationOrder() const
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)
void InprocessingRemoveClause(SatClause *clause)
int64 literal_size() const
SatClause * InprocessingAddClause(absl::Span< const Literal > new_clause)
int64 num_watched_clauses() const
bool IsRemovable(SatClause *const clause) const
ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause)
void DeleteRemovedClauses()
absl::Span< const Literal > AsSpan() const
void MaybeEnablePhaseSaving(bool save_phase)
void MinimizeSomeClauses(int decisions_budget)
int CurrentDecisionLevel() const
bool DoOneRound(bool log_info)
bool ComputeStampsForNextRound(bool log_info)
bool ImplicationIsInTree(Literal a, Literal b) const
void SampleTreeAndFillParent()
bool LiteralIsAssigned(Literal literal) const
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
static const int32 kint32max
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
const LiteralIndex kNoLiteralIndex(-1)
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
#define RETURN_IF_FALSE(f)
std::deque< std::vector< Literal > > clauses
void AddClauseWithSpecialLiteral(Literal literal, absl::Span< const Literal > clause)
double deterministic_limit
bool extract_binary_clauses
bool use_transitive_reduction
bool extract_binary_clauses_in_probing
double deterministic_time_limit
#define VLOG_IS_ON(verboselevel)