16 #include "absl/container/inlined_vector.h"
28 clauses.emplace_back(clause.begin(), clause.end());
29 for (
int i = 0; i < clause.size(); ++i) {
39 #define RETURN_IF_FALSE(f) \
40 if (!(f)) return false;
50 double probing_time = 0.0;
82 !implication_graph_->
IsDag()) {
88 !implication_graph_->
IsDag()) {
95 blocked_clause_simplifier_->
DoOneRound(log_round_info);
101 const double time_left =
103 if (time_left <= 0)
break;
105 probing_options.
log_info = log_round_info;
113 !implication_graph_->
IsDag()) {
125 <<
" num_fixed: " << trail_->
Index()
133 <<
" non-probing time: " << (
wall_timer.
Get() - probing_time);
145 double probing_time = 0.0;
149 if (total_dtime_ > 0.1 * start_dtime)
return true;
165 probing_options.
log_info = log_round_info;
186 blocked_clause_simplifier_->
DoOneRound(log_round_info);
193 <<
" num_fixed: " << trail_->
Index()
200 <<
" non-probing time: " << (
wall_timer.
Get() - probing_time);
206 #undef RETURN_IF_FALSE
209 const int64 new_num_fixed_variables = trail_->
Index();
210 return last_num_fixed_variables_ < new_num_fixed_variables;
214 const int64 new_num_redundant_literals =
216 return last_num_redundant_literals_ < new_num_redundant_literals;
231 if (!implication_graph_->
IsDag()) {
237 if (use_transitive_reduction) {
264 const int64 new_num_redundant_literals =
266 const int64 new_num_fixed_variables = trail_->
Index();
267 if (last_num_redundant_literals_ == new_num_redundant_literals &&
268 last_num_fixed_variables_ == new_num_fixed_variables) {
271 last_num_fixed_variables_ = new_num_fixed_variables;
272 last_num_redundant_literals_ = new_num_redundant_literals;
278 int64 num_removed_literals = 0;
279 int64 num_inspected_literals = 0;
283 std::vector<Literal> new_clause;
286 const int num_literals(sat_solver_->
NumVariables() * 2);
292 bool removed =
false;
293 bool need_rewrite =
false;
296 for (
const Literal l : clause->AsSpan()) {
303 num_removed_literals += clause->size();
313 num_inspected_literals += clause->size();
314 if (removed || !need_rewrite)
continue;
315 num_inspected_literals += clause->size();
319 for (
const Literal l : clause->AsSpan()) {
326 num_removed_literals += clause->size();
330 marked[r.
Index()] =
true;
331 new_clause.push_back(r);
335 for (
const Literal l : new_clause) marked[l.Index()] =
false;
336 if (removed)
continue;
338 num_removed_literals += clause->
size() - new_clause.size();
345 const double dtime =
static_cast<double>(num_inspected_literals) * 1e-8;
347 LOG_IF(
INFO, log_info) <<
"Cleanup. num_removed_literals: "
348 << num_removed_literals <<
" dtime: " << dtime
362 int64 num_subsumed_clauses = 0;
363 int64 num_removed_literals = 0;
364 int64 num_inspected_signatures = 0;
365 int64 num_inspected_literals = 0;
369 std::vector<Literal> new_clause;
381 std::vector<SatClause*> clauses =
383 std::sort(clauses.begin(), clauses.end(),
387 const LiteralIndex num_literals(sat_solver_->
NumVariables() * 2);
393 num_literals.value());
396 std::vector<uint64> signatures(clauses.size());
398 std::vector<Literal> candidates_for_removal;
399 for (
int clause_index = 0; clause_index < clauses.size(); ++clause_index) {
400 SatClause* clause = clauses[clause_index];
406 if (num_inspected_literals + num_inspected_signatures > 1e9) {
424 marked.
Set(l.Index());
425 signature |= (
uint64{1} << (l.Variable().value() % 64));
431 bool removed =
false;
432 candidates_for_removal.clear();
433 const uint64 mask = ~signature;
435 num_inspected_signatures += one_watcher[l.Index()].
size();
436 for (
const int i : one_watcher[l.Index()]) {
437 if ((mask & signatures[i]) != 0)
continue;
439 bool subsumed =
true;
440 bool stengthen =
true;
442 num_inspected_literals += clauses[i]->size();
443 for (
const Literal o : clauses[i]->AsSpan()) {
444 if (!marked[o.Index()]) {
447 to_remove = o.NegatedIndex();
455 ++num_subsumed_clauses;
456 num_removed_literals += clause->
size();
463 candidates_for_removal.push_back(
Literal(to_remove));
468 if (removed)
continue;
472 num_inspected_signatures += one_watcher[l.NegatedIndex()].
size();
473 for (
const int i : one_watcher[l.NegatedIndex()]) {
474 if ((mask & signatures[i]) != 0)
continue;
476 bool stengthen =
true;
477 num_inspected_literals += clauses[i]->size();
478 for (
const Literal o : clauses[i]->AsSpan()) {
479 if (o == l.Negated())
continue;
480 if (!marked[o.Index()]) {
486 candidates_for_removal.push_back(l);
497 if (!candidates_for_removal.empty()) {
500 new_clause.push_back(l);
504 for (
const Literal l : new_clause) {
505 if (l == candidates_for_removal[0])
continue;
506 new_clause[new_size++] = l;
508 CHECK_EQ(new_size + 1, new_clause.size());
509 new_clause.resize(new_size);
511 num_removed_literals += clause->
size() - new_clause.size();
515 if (clause->
size() == 0)
continue;
520 signature |= (
uint64{1} << (l.Variable().value() % 64));
541 if (one_watcher[l.Index()].
size() < min_size) {
542 min_size = one_watcher[l.Index()].
size();
543 min_literal = l.Index();
553 signatures[clause_index] = signature;
554 one_watcher[min_literal].
push_back(clause_index);
562 const double dtime =
static_cast<double>(num_inspected_signatures) * 1e-8 +
563 static_cast<double>(num_inspected_literals) * 5e-9;
565 LOG_IF(
INFO, log_info) <<
"Subsume. num_removed_literals: "
566 << num_removed_literals
567 <<
" num_subsumed: " << num_subsumed_clauses
568 <<
" dtime: " << dtime
578 num_subsumed_clauses_ = 0;
579 num_removed_literals_ = 0;
582 if (implication_graph_->
literal_size() == 0)
return true;
585 if (!stamps_are_already_computed_) {
594 stamps_are_already_computed_ =
false;
601 LOG_IF(
INFO, log_info) <<
"Stamping. num_removed_literals: "
602 << num_removed_literals_
603 <<
" num_subsumed: " << num_subsumed_clauses_
604 <<
" num_fixed: " << num_fixed_ <<
" dtime: " << dtime_
615 if (implication_graph_->
literal_size() == 0)
return true;
622 stamps_are_already_computed_ =
true;
628 <<
" num_fixed: " << num_fixed_ <<
" dtime: " << dtime_
637 for (LiteralIndex i(0); i < size; ++i) {
650 const auto& children_of_not_l =
652 if (children_of_not_l.empty())
continue;
653 for (
int num_tries = 0; num_tries < 10; ++num_tries) {
655 children_of_not_l[absl::Uniform<int>(*random_, 0,
656 children_of_not_l.size())]
658 if (implication_graph_->
IsRedundant(candidate))
continue;
659 if (i == candidate.
Index())
continue;
662 parents_[i] = candidate.
Index();
673 for (LiteralIndex i(0); i < size; ++i) {
674 if (parents_[i] == i)
continue;
675 sizes_[parents_[i]]++;
680 starts_[LiteralIndex(0)] = 0;
681 for (LiteralIndex i(1); i <= size; ++i) {
682 starts_[i] = starts_[i - 1] + sizes_[i - 1];
686 children_.resize(size);
687 for (LiteralIndex i(0); i < size; ++i) {
688 if (parents_[i] == i)
continue;
689 children_[starts_[parents_[i]]++] = i;
693 for (LiteralIndex i(0); i < size; ++i) {
694 starts_[i] -= sizes_[i];
698 CHECK_EQ(starts_[LiteralIndex(0)], 0);
699 for (LiteralIndex i(1); i <= size; ++i) {
700 CHECK_EQ(starts_[i], starts_[i - 1] + sizes_[i - 1]);
706 first_stamps_.
resize(size);
707 last_stamps_.
resize(size);
708 marked_.
assign(size,
false);
709 for (LiteralIndex i(0); i < size; ++i) {
710 if (parents_[i] != i)
continue;
712 const LiteralIndex tree_root = i;
713 dfs_stack_.push_back(i);
714 while (!dfs_stack_.empty()) {
715 const LiteralIndex top = dfs_stack_.back();
717 dfs_stack_.pop_back();
718 last_stamps_[top] = stamp++;
721 first_stamps_[top] = stamp++;
726 if (marked_[
Literal(top).NegatedIndex()] &&
727 first_stamps_[
Literal(top).NegatedIndex()] >=
728 first_stamps_[tree_root]) {
731 LiteralIndex lca = top;
732 while (first_stamps_[lca] > first_stamp) {
741 const int end = starts_[top + 1];
742 for (
int j = starts_[top]; j < end; ++j) {
744 DCHECK(!marked_[children_[j]]);
745 dfs_stack_.push_back(children_[j]);
759 bool operator<(
const Entry& o)
const {
return start < o.start; }
761 std::vector<int> to_remove;
762 std::vector<Literal> new_clause;
763 std::vector<Entry> entries;
767 const auto span = clause->AsSpan();
768 if (span.empty())
continue;
777 for (
int i = 0; i < span.size(); ++i) {
783 entries.push_back({i,
false, first_stamps_[span[i].Index()],
784 last_stamps_[span[i].
Index()]});
785 entries.push_back({i,
true, first_stamps_[span[i].NegatedIndex()],
786 last_stamps_[span[i].NegatedIndex()]});
788 if (clause->empty())
continue;
791 if (!entries.empty()) {
792 const double n =
static_cast<double>(entries.size());
793 dtime_ += 1.5e-8 * n * std::log(n);
794 std::sort(entries.begin(), entries.end());
800 for (
const Entry& e : entries) {
801 if (e.end < top_entry.end) {
803 const Literal lhs = top_entry.is_negated ? span[top_entry.i].Negated()
805 const Literal rhs = e.is_negated ? span[e.i].
Negated() : span[e.i];
808 if (top_entry.is_negated != e.is_negated) {
810 if (top_entry.i == e.i) {
812 if (top_entry.is_negated) {
821 span[top_entry.i].Negated())) {
824 to_remove.push_back(top_entry.i);
833 if (top_entry.is_negated) {
834 num_subsumed_clauses_++;
840 if (top_entry.is_negated) {
842 to_remove.push_back(e.i);
851 to_remove.push_back(top_entry.i);
859 if (clause->empty())
continue;
862 if (!to_remove.empty() || entries.size() < span.size()) {
865 int to_remove_index = 0;
866 for (
int i = 0; i < span.size(); ++i) {
867 if (to_remove_index < to_remove.size() &&
868 i == to_remove[to_remove_index]) {
877 new_clause.push_back(span[i]);
879 num_removed_literals_ += span.size() - new_clause.size();
893 num_blocked_clauses_ = 0;
894 num_inspected_literals_ = 0;
896 InitializeForNewRound();
898 while (!time_limit_->
LimitReached() && !queue_.empty()) {
899 const Literal l = queue_.front();
900 in_queue_[l.
Index()] =
false;
906 literal_to_clauses_.
clear();
908 dtime_ += 1e-8 * num_inspected_literals_;
911 LOG_IF(
INFO, log_info) <<
"Blocked clause. num_blocked_clauses: "
912 << num_blocked_clauses_ <<
" dtime: " << dtime_
916 void BlockedClauseSimplifier::InitializeForNewRound() {
924 clauses_.push_back(c);
926 const int num_literals = clause_manager_->
literal_size();
930 in_queue_.
assign(num_literals,
true);
931 for (LiteralIndex l(0); l < num_literals; ++l) {
932 queue_.push_back(Literal(l));
935 marked_.
resize(num_literals);
937 std::all_of(marked_.
begin(), marked_.
end(), [](
bool b) { return !b; }));
941 literal_to_clauses_.
clear();
942 literal_to_clauses_.
resize(num_literals);
943 for (ClauseIndex i(0); i < clauses_.size(); ++i) {
944 for (
const Literal l : clauses_[i]->AsSpan()) {
945 literal_to_clauses_[l.Index()].
push_back(i);
947 num_inspected_literals_ += clauses_[i]->size();
951 void BlockedClauseSimplifier::ProcessLiteral(Literal current_literal) {
953 if (implication_graph_->
IsRemoved(current_literal))
return;
968 const std::vector<Literal>& implications =
970 for (
const Literal l : implications) {
971 if (l == current_literal)
continue;
973 marked_[l.Index()] =
true;
979 std::vector<ClauseIndex> clauses_to_process;
980 for (
const ClauseIndex i : literal_to_clauses_[current_literal.Index()]) {
981 if (clauses_[i]->empty())
continue;
987 if (num_binary > 0) {
988 if (clauses_[i]->size() <= num_binary)
continue;
989 int num_with_negation_marked = 0;
990 for (
const Literal l : clauses_[i]->AsSpan()) {
991 if (l == current_literal)
continue;
992 if (marked_[l.NegatedIndex()]) {
993 ++num_with_negation_marked;
996 num_inspected_literals_ += clauses_[i]->size();
997 if (num_with_negation_marked < num_binary)
continue;
999 clauses_to_process.push_back(i);
1003 for (
const Literal l : implications) {
1004 marked_[l.Index()] =
false;
1015 for (
const ClauseIndex i : clauses_to_process) {
1016 const auto c = clauses_[i]->AsSpan();
1017 if (ClauseIsBlocked(current_literal, c)) {
1024 for (
const Literal l : c) {
1025 if (!in_queue_[l.NegatedIndex()]) {
1026 in_queue_[l.NegatedIndex()] =
true;
1027 queue_.push_back(l.Negated());
1035 ++num_blocked_clauses_;
1042 bool BlockedClauseSimplifier::ClauseIsBlocked(
1043 Literal current_literal, absl::Span<const Literal> clause) {
1044 bool is_blocked =
true;
1045 for (
const Literal l : clause) marked_[l.Index()] =
true;
1049 for (
const ClauseIndex i :
1050 literal_to_clauses_[current_literal.NegatedIndex()]) {
1051 if (clauses_[i]->empty())
continue;
1052 bool some_marked =
false;
1053 for (
const Literal l : clauses_[i]->AsSpan()) {
1055 ++num_inspected_literals_;
1057 if (l == current_literal.Negated())
continue;
1058 if (marked_[l.NegatedIndex()]) {
1069 for (
const Literal l : clause) marked_[l.Index()] =
false;
1078 num_inspected_literals_ = 0;
1079 num_eliminated_variables_ = 0;
1080 num_literals_diff_ = 0;
1081 num_clauses_diff_ = 0;
1082 num_simplifications_ = 0;
1083 num_blocked_clauses_ = 0;
1094 clauses_.push_back(c);
1096 const int num_literals = clause_manager_->
literal_size();
1097 const int num_variables = num_literals / 2;
1099 literal_to_clauses_.
clear();
1100 literal_to_clauses_.
resize(num_literals);
1101 literal_to_num_clauses_.
assign(num_literals, 0);
1102 for (ClauseIndex i(0); i < clauses_.size(); ++i) {
1103 for (
const Literal l : clauses_[i]->AsSpan()) {
1104 literal_to_clauses_[l.Index()].
push_back(i);
1105 literal_to_num_clauses_[l.Index()]++;
1107 num_inspected_literals_ += clauses_[i]->size();
1110 const int saved_trail_index = trail_->
Index();
1111 propagation_index_ = trail_->
Index();
1113 need_to_be_updated_.clear();
1114 in_need_to_be_updated_.
resize(num_variables);
1115 queue_.
Reserve(num_variables);
1116 for (BooleanVariable v(0); v < num_variables; ++v) {
1119 UpdatePriorityQueue(v);
1122 marked_.
resize(num_literals);
1124 std::all_of(marked_.
begin(), marked_.
end(), [](
bool b) { return !b; }));
1130 const BooleanVariable top = queue_.
Top().var;
1138 bool is_unsat =
false;
1139 if (!Propagate())
return false;
1141 if (!Propagate())
return false;
1143 if (is_unsat)
return false;
1145 if (!CrossProduct(top))
return false;
1147 for (
const BooleanVariable v : need_to_be_updated_) {
1148 in_need_to_be_updated_[v] =
false;
1151 if (v != top) UpdatePriorityQueue(v);
1153 in_need_to_be_updated_.
clear();
1154 need_to_be_updated_.clear();
1163 bool remove =
false;
1164 for (
const Literal l : c->AsSpan()) {
1174 literal_to_clauses_.
clear();
1175 literal_to_num_clauses_.
clear();
1177 dtime_ += 1e-8 * num_inspected_literals_;
1182 << trail_->
Index() - saved_trail_index
1183 <<
" num_simplified_literals: " << num_simplifications_
1184 <<
" num_blocked_clauses_: " << num_blocked_clauses_
1185 <<
" num_eliminations: " << num_eliminated_variables_
1186 <<
" num_literals_diff: " << num_literals_diff_
1187 <<
" num_clause_diff: " << num_clauses_diff_
1188 <<
" dtime: " << dtime_
1193 bool BoundedVariableElimination::RemoveLiteralFromClause(
1195 num_literals_diff_ -= sat_clause->
size();
1199 literal_to_num_clauses_[l.Index()]--;
1203 num_clauses_diff_--;
1207 resolvant_.push_back(l);
1212 if (sat_clause->
empty()) {
1213 --num_clauses_diff_;
1214 for (
const Literal l : resolvant_) literal_to_num_clauses_[l.Index()]--;
1216 num_literals_diff_ += sat_clause->
size();
1221 bool BoundedVariableElimination::Propagate() {
1222 for (; propagation_index_ < trail_->
Index(); ++propagation_index_) {
1224 if (!implication_graph_->
Propagate(trail_))
return false;
1226 const Literal l = (*trail_)[propagation_index_];
1227 for (
const ClauseIndex
index : literal_to_clauses_[l.Index()]) {
1228 if (clauses_[
index]->empty())
continue;
1229 num_clauses_diff_--;
1230 num_literals_diff_ -= clauses_[
index]->size();
1233 literal_to_clauses_[l.Index()].
clear();
1234 for (
const ClauseIndex
index : literal_to_clauses_[l.NegatedIndex()]) {
1235 if (clauses_[
index]->empty())
continue;
1236 if (!RemoveLiteralFromClause(l.Negated(), clauses_[
index]))
return false;
1238 literal_to_clauses_[l.NegatedIndex()].
clear();
1245 int BoundedVariableElimination::NumClausesContaining(Literal l) {
1246 return literal_to_num_clauses_[l.Index()] +
1251 void BoundedVariableElimination::UpdatePriorityQueue(BooleanVariable
var) {
1253 const int priority = -NumClausesContaining(Literal(
var,
true)) -
1254 NumClausesContaining(Literal(
var,
false));
1258 queue_.
Add({
var, priority});
1262 void BoundedVariableElimination::DeleteClause(SatClause* sat_clause) {
1263 const auto clause = sat_clause->AsSpan();
1265 num_clauses_diff_--;
1266 num_literals_diff_ -= clause.size();
1269 for (
const Literal l : clause) {
1270 literal_to_num_clauses_[l.Index()]--;
1271 if (!in_need_to_be_updated_[l.Variable()]) {
1272 in_need_to_be_updated_[l.Variable()] =
true;
1273 need_to_be_updated_.push_back(l.Variable());
1281 void BoundedVariableElimination::DeleteAllClausesContaining(Literal
literal) {
1282 for (
const ClauseIndex i : literal_to_clauses_[
literal.Index()]) {
1283 const auto clause = clauses_[i]->AsSpan();
1284 if (clause.empty())
continue;
1286 DeleteClause(clauses_[i]);
1291 void BoundedVariableElimination::AddClause(absl::Span<const Literal> clause) {
1293 if (pt ==
nullptr)
return;
1295 num_clauses_diff_++;
1296 num_literals_diff_ += clause.size();
1298 const ClauseIndex
index(clauses_.size());
1299 clauses_.push_back(pt);
1300 for (
const Literal l : clause) {
1301 literal_to_num_clauses_[l.Index()]++;
1303 if (!in_need_to_be_updated_[l.Variable()]) {
1304 in_need_to_be_updated_[l.Variable()] =
true;
1305 need_to_be_updated_.push_back(l.Variable());
1310 template <
bool score_only,
bool with_binary_only>
1311 bool BoundedVariableElimination::ResolveAllClauseContaining(Literal lit) {
1312 const int clause_weight = parameters_.presolve_bve_clause_weight();
1314 const std::vector<Literal>& implications =
1316 auto& clause_containing_lit = literal_to_clauses_[lit.Index()];
1317 for (
int i = 0; i < clause_containing_lit.size(); ++i) {
1318 const ClauseIndex clause_index = clause_containing_lit[i];
1319 const auto clause = clauses_[clause_index]->AsSpan();
1320 if (clause.empty())
continue;
1322 if (!score_only) resolvant_.clear();
1323 for (
const Literal l : clause) {
1324 if (!score_only && l != lit) resolvant_.push_back(l);
1325 marked_[l.Index()] =
true;
1327 num_inspected_literals_ += clause.size() + implications.size();
1331 bool clause_can_be_simplified =
false;
1332 const int64 saved_score = new_score_;
1335 for (
const Literal l : implications) {
1337 if (marked_[l.NegatedIndex()])
continue;
1338 if (marked_[l.Index()]) {
1339 clause_can_be_simplified =
true;
1343 new_score_ += clause_weight + clause.size();
1345 resolvant_.push_back(l);
1346 AddClause(resolvant_);
1347 resolvant_.pop_back();
1353 if (!with_binary_only && !clause_can_be_simplified) {
1354 auto& clause_containing_not_lit = literal_to_clauses_[lit.NegatedIndex()];
1355 for (
int j = 0; j < clause_containing_not_lit.size(); ++j) {
1356 if (score_only && new_score_ > score_threshold_)
break;
1357 const ClauseIndex other_index = clause_containing_not_lit[j];
1358 const auto other = clauses_[other_index]->AsSpan();
1359 if (other.empty())
continue;
1360 bool trivial =
false;
1362 for (
const Literal l : other) {
1364 ++num_inspected_literals_;
1365 if (l == lit.Negated())
continue;
1366 if (marked_[l.NegatedIndex()]) {
1370 if (!marked_[l.Index()]) {
1372 if (!score_only) resolvant_.push_back(l);
1376 if (!score_only) resolvant_.resize(resolvant_.size() - extra_size);
1382 if (score_only && clause.size() + extra_size <= other.size()) {
1383 CHECK_EQ(clause.size() + extra_size, other.size());
1384 ++num_simplifications_;
1388 score_threshold_ -= clause_weight + other.size();
1390 if (extra_size == 0) {
1394 DeleteClause(clauses_[other_index]);
1396 if (!RemoveLiteralFromClause(lit.Negated(),
1397 clauses_[other_index])) {
1400 std::swap(clause_containing_not_lit[j],
1401 clause_containing_not_lit.back());
1402 clause_containing_not_lit.pop_back();
1408 if (extra_size == 0) {
1409 clause_can_be_simplified =
true;
1414 if (clause.size() - 1 + extra_size > 100) {
1415 new_score_ = score_threshold_ + 1;
1419 new_score_ += clause_weight + clause.size() - 1 + extra_size;
1421 AddClause(resolvant_);
1422 resolvant_.resize(resolvant_.size() - extra_size);
1429 for (
const Literal l : clause) marked_[l.Index()] =
false;
1432 if (clause_can_be_simplified) {
1433 ++num_simplifications_;
1436 new_score_ = saved_score;
1437 score_threshold_ -= clause_weight + clause.size();
1439 if (!RemoveLiteralFromClause(lit, clauses_[clause_index]))
return false;
1440 std::swap(clause_containing_lit[i], clause_containing_lit.back());
1441 clause_containing_lit.pop_back();
1445 if (score_only && new_score_ > score_threshold_)
return true;
1457 if (score_only && !with_binary_only && !clause_can_be_simplified &&
1458 new_score_ == saved_score) {
1459 ++num_blocked_clauses_;
1460 score_threshold_ -= clause_weight + clause.size();
1462 DeleteClause(clauses_[clause_index]);
1468 bool BoundedVariableElimination::CrossProduct(BooleanVariable
var) {
1471 const Literal lit(
var,
true);
1472 const Literal not_lit(
var,
false);
1474 const int s1 = NumClausesContaining(lit);
1475 const int s2 = NumClausesContaining(not_lit);
1476 if (s1 == 0 && s2 == 0)
return true;
1477 if (s1 > 0 && s2 == 0) {
1478 num_eliminated_variables_++;
1480 DeleteAllClausesContaining(lit);
1483 if (s1 == 0 && s2 > 0) {
1484 num_eliminated_variables_++;
1486 DeleteAllClausesContaining(not_lit);
1494 num_eliminated_variables_++;
1501 if (s1 > 1 && s2 > 1 && s1 * s2 > parameters_.presolve_bve_threshold()) {
1514 const int clause_weight = parameters_.presolve_bve_clause_weight();
1518 (clause_weight + 2);
1519 for (
const ClauseIndex i : literal_to_clauses_[lit.Index()]) {
1520 const auto c = clauses_[i]->AsSpan();
1521 if (!c.empty()) score += clause_weight + c.size();
1523 for (
const ClauseIndex i : literal_to_clauses_[not_lit.Index()]) {
1524 const auto c = clauses_[i]->AsSpan();
1525 if (!c.empty()) score += clause_weight + c.size();
1536 score_threshold_ = score;
1538 (clause_weight + 2);
1539 if (new_score_ > score_threshold_)
return true;
1540 if (!ResolveAllClauseContaining<
true,
1544 if (new_score_ > score_threshold_)
return true;
1545 if (!ResolveAllClauseContaining<
true,
1549 if (new_score_ > score_threshold_)
return true;
1552 if (new_score_ > 0) {
1553 if (!ResolveAllClauseContaining<
false,
1557 if (!ResolveAllClauseContaining<
false,
1563 ++num_eliminated_variables_;
1565 DeleteAllClausesContaining(lit);
1566 DeleteAllClausesContaining(not_lit);