225 const double deterministic_time_limit,
226 absl::Span<const BooleanVariable> bool_vars) {
234 num_new_integer_bounds_ = 0;
235 num_new_literals_fixed_ = 0;
238 const int num_variables = sat_solver_->NumVariables();
239 propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
242 if (!sat_solver_->ResetToLevelZero())
return false;
244 const int initial_num_fixed = sat_solver_->LiteralTrail().Index();
245 const double initial_deterministic_time =
246 time_limit_->GetElapsedDeterministicTime();
247 const double limit = initial_deterministic_time + deterministic_time_limit;
249 bool limit_reached =
false;
252 for (
const BooleanVariable
b : bool_vars) {
254 if (implication_graph_->RepresentativeOf(literal) != literal) {
260 if (time_limit_->LimitReached() ||
261 time_limit_->GetElapsedDeterministicTime() > limit) {
262 limit_reached =
true;
268 if (!ProbeOneVariableInternal(
b)) {
274 const int num_fixed = sat_solver_->LiteralTrail().Index();
275 num_new_literals_fixed_ = num_fixed - initial_num_fixed;
278 if (logger_->LoggingIsEnabled()) {
279 const double time_diff =
280 time_limit_->GetElapsedDeterministicTime() - initial_deterministic_time;
281 SOLVER_LOG(logger_,
"[Probing] deterministic_time: ", time_diff,
282 " (limit: ", deterministic_time_limit,
283 ") wall_time: ", wall_timer.
Get(),
" (",
284 (limit_reached ?
"Aborted " :
""), num_probed,
"/",
285 bool_vars.size(),
")");
286 if (num_new_literals_fixed_ > 0) {
288 "[Probing] - new fixed Boolean: ", num_new_literals_fixed_,
289 " (", num_fixed,
"/", sat_solver_->NumVariables(),
")");
291 if (num_new_holes_ > 0) {
292 SOLVER_LOG(logger_,
"[Probing] - new integer holes: ", num_new_holes_);
294 if (num_new_integer_bounds_ > 0) {
296 "[Probing] - new integer bounds: ", num_new_integer_bounds_);
298 if (num_new_binary_ > 0) {
299 SOLVER_LOG(logger_,
"[Probing] - new binary clause: ", num_new_binary_);
307 absl::Span<
const std::vector<Literal>> dnf) {
308 if (dnf.size() <= 1)
return true;
311 if (!sat_solver_->ResetToLevelZero())
return false;
313 always_propagated_bounds_.clear();
314 always_propagated_literals_.clear();
315 int num_valid_conjunctions = 0;
316 for (
const std::vector<Literal>& conjunction : dnf) {
317 if (!sat_solver_->ResetToLevelZero())
return false;
318 if (num_valid_conjunctions > 0 && always_propagated_bounds_.empty() &&
319 always_propagated_literals_.empty()) {
324 bool conjunction_is_valid =
true;
325 int num_literals_enqueued = 0;
326 const int root_trail_index = trail_.Index();
327 const int root_integer_trail_index = integer_trail_->Index();
328 for (
const Literal& lit : conjunction) {
329 if (assignment_.LiteralIsAssigned(lit)) {
330 if (assignment_.LiteralIsTrue(lit))
continue;
331 conjunction_is_valid =
false;
334 ++num_literals_enqueued;
335 const int decision_level_before_enqueue =
336 sat_solver_->CurrentDecisionLevel();
337 sat_solver_->EnqueueDecisionAndBackjumpOnConflict(lit);
338 sat_solver_->AdvanceDeterministicTime(time_limit_);
339 const int decision_level_after_enqueue =
340 sat_solver_->CurrentDecisionLevel();
343 if (sat_solver_->ModelIsUnsat())
return false;
346 if (decision_level_after_enqueue <= decision_level_before_enqueue) {
347 conjunction_is_valid =
false;
352 if (conjunction_is_valid) {
353 ++num_valid_conjunctions;
359 new_propagated_literals_.clear();
360 for (
int i = root_trail_index;
i < trail_.Index(); ++
i) {
361 const LiteralIndex literal_index = trail_[
i].Index();
362 if (num_valid_conjunctions == 1 ||
363 always_propagated_literals_.contains(literal_index)) {
364 new_propagated_literals_.insert(literal_index);
367 std::swap(new_propagated_literals_, always_propagated_literals_);
370 new_integer_bounds_.clear();
371 integer_trail_->AppendNewBoundsFrom(root_integer_trail_index,
372 &new_integer_bounds_);
373 new_propagated_bounds_.clear();
375 const auto it = always_propagated_bounds_.find(entry.var);
376 if (num_valid_conjunctions == 1) {
377 new_propagated_bounds_[entry.var] = entry.bound;
378 }
else if (it != always_propagated_bounds_.end()) {
379 new_propagated_bounds_[entry.var] = std::min(entry.bound, it->second);
382 std::swap(new_propagated_bounds_, always_propagated_bounds_);
385 if (!sat_solver_->ResetToLevelZero())
return false;
387 const int previous_num_literals_fixed = num_new_literals_fixed_;
388 for (
const LiteralIndex literal_index : always_propagated_literals_) {
389 const Literal lit(literal_index);
390 if (assignment_.LiteralIsTrue(lit))
continue;
391 ++num_new_literals_fixed_;
392 if (!sat_solver_->AddUnitClause(lit))
return false;
396 int previous_num_integer_bounds = num_new_integer_bounds_;
397 for (
const auto& [var, bound] : always_propagated_bounds_) {
398 if (bound > integer_trail_->LowerBound(var)) {
399 ++num_new_integer_bounds_;
407 if (!sat_solver_->FinishPropagation())
return false;
409 if (num_new_integer_bounds_ > previous_num_integer_bounds ||
410 num_new_literals_fixed_ > previous_num_literals_fixed) {
411 VLOG(1) <<
"ProbeDnf(" << name <<
", num_fixed_literals="
412 << num_new_literals_fixed_ - previous_num_literals_fixed
413 <<
", num_pushed_integer_bounds="
414 << num_new_integer_bounds_ - previous_num_integer_bounds
415 <<
", num_valid_conjunctions=" << num_valid_conjunctions <<
"/"
416 << dnf.size() <<
")";
432 if (!sat_solver->ResetToLevelZero())
return false;
435 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
442 new_params.set_max_number_of_conflicts(1);
443 new_params.set_max_deterministic_time(deterministic_time_limit);
445 double elapsed_dtime = 0.0;
447 const int num_times = 1000;
448 bool limit_reached =
false;
450 for (
int i = 0;
i < num_times; ++
i) {
452 elapsed_dtime > deterministic_time_limit) {
453 limit_reached =
true;
458 sat_solver->SetParameters(new_params);
459 sat_solver->ResetDecisionHeuristic();
461 elapsed_dtime +=
time_limit->GetElapsedDeterministicTime();
464 SOLVER_LOG(logger,
"Trivial exploration found feasible solution!");
465 time_limit->AdvanceDeterministicTime(elapsed_dtime);
469 if (!sat_solver->ResetToLevelZero()) {
470 SOLVER_LOG(logger,
"UNSAT during trivial exploration heuristic.");
471 time_limit->AdvanceDeterministicTime(elapsed_dtime);
478 new_params.set_random_seed(
i);
479 new_params.set_max_deterministic_time(deterministic_time_limit -
484 sat_solver->SetParameters(initial_params);
485 sat_solver->ResetDecisionHeuristic();
486 time_limit->AdvanceDeterministicTime(elapsed_dtime);
487 if (!sat_solver->ResetToLevelZero())
return false;
490 const int num_fixed = sat_solver->LiteralTrail().Index();
491 const int num_newly_fixed = num_fixed - initial_num_fixed;
492 const int num_variables = sat_solver->NumVariables();
493 SOLVER_LOG(logger,
"[Random exploration]",
" num_fixed: +", num_newly_fixed,
494 " (", num_fixed,
"/", num_variables,
")",
495 " dtime: ", elapsed_dtime,
"/", deterministic_time_limit,
496 " wtime: ", wall_timer.
Get(),
497 (limit_reached ?
" (Aborted)" :
""));
499 return sat_solver->FinishPropagation();
509 if (!sat_solver->ResetToLevelZero())
return false;
515 if (!implication_graph->DetectEquivalences())
return false;
516 if (!sat_solver->FinishPropagation())
return false;
519 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
520 const double initial_deterministic_time =
524 const int num_variables = sat_solver->NumVariables();
527 int64_t num_probed = 0;
528 int64_t num_explicit_fix = 0;
529 int64_t num_conflicts = 0;
530 int64_t num_new_binary = 0;
531 int64_t num_subsumed = 0;
533 const auto& trail = *(model->
Get<
Trail>());
534 const auto& assignment = trail.Assignment();
537 const int clause_id = clause_manager->PropagatorId();
540 struct SavedNextLiteral {
541 LiteralIndex literal_index;
544 bool operator<(
const SavedNextLiteral& o)
const {
return rank < o.rank; }
546 std::vector<SavedNextLiteral> queue;
555 std::vector<Literal> to_fix;
569 std::vector<LiteralIndex> probing_order =
570 implication_graph->ReverseTopologicalOrder();
572 std::reverse(probing_order.begin(), probing_order.end());
577 position_in_order.
assign(2 * num_variables, -1);
578 for (
int i = 0;
i < probing_order.size(); ++
i) {
579 position_in_order[probing_order[
i]] =
i;
584 time_limit->GetElapsedDeterministicTime() <= limit) {
589 if (options.
use_queue && sat_solver->CurrentDecisionLevel() > 0) {
594 sat_solver->Decisions()[sat_solver->CurrentDecisionLevel() - 1]
597 implication_graph->Implications(prev_decision.
Negated());
598 const int saved_queue_size = queue.size();
601 if (processed[candidate])
continue;
602 if (position_in_order[candidate] == -1)
continue;
603 if (assignment.LiteralIsAssigned(candidate)) {
604 if (assignment.LiteralIsFalse(candidate)) {
609 queue.push_back({candidate.
Index(), -position_in_order[candidate]});
611 std::sort(queue.begin() + saved_queue_size, queue.end());
614 while (!queue.empty()) {
615 const LiteralIndex index = queue.back().literal_index;
619 CHECK_GT(sat_solver->CurrentDecisionLevel(), 0);
620 sat_solver->Backtrack(sat_solver->CurrentDecisionLevel() - 1);
623 const Literal candidate(index);
624 if (processed[candidate])
continue;
625 if (assignment.LiteralIsAssigned(candidate)) {
626 if (assignment.LiteralIsFalse(candidate)) {
631 next_decision = candidate.
Index();
636 if (sat_solver->CurrentDecisionLevel() == 0) {
638 for (
const Literal literal : to_fix) {
639 if (!assignment.LiteralIsTrue(literal)) {
641 if (!sat_solver->AddUnitClause(literal))
return false;
645 if (!sat_solver->FinishPropagation())
return false;
648 for (; order_index < probing_order.size(); ++order_index) {
649 const Literal candidate(probing_order[order_index]);
650 if (processed[candidate])
continue;
651 if (assignment.LiteralIsAssigned(candidate))
continue;
652 next_decision = candidate.
Index();
659 const int level = sat_solver->CurrentDecisionLevel();
660 const Literal prev_decision = sat_solver->Decisions()[level - 1].literal;
662 implication_graph->Implications(prev_decision.
Negated());
669 for (
int i = 0;
i < list.size(); ++
i, ++j) {
672 if (processed[candidate])
continue;
673 if (assignment.LiteralIsFalse(candidate)) {
680 if (assignment.LiteralIsTrue(candidate))
continue;
681 next_decision = candidate.
Index();
686 sat_solver->Backtrack(level - 1);
692 processed.
Set(next_decision);
695 const int level = sat_solver->CurrentDecisionLevel();
696 const int first_new_trail_index =
697 sat_solver->EnqueueDecisionAndBackjumpOnConflict(
699 const int new_level = sat_solver->CurrentDecisionLevel();
700 sat_solver->AdvanceDeterministicTime(
time_limit);
701 if (sat_solver->ModelIsUnsat())
return false;
702 if (new_level <= level) {
707 if (new_level == 0) {
710 int queue_level = level + 1;
711 while (queue_level > new_level) {
712 CHECK(!queue.empty());
734 if (sat_solver->CurrentDecisionLevel() != 0 ||
735 assignment.LiteralIsFalse(
Literal(next_decision))) {
736 to_fix.push_back(
Literal(next_decision).Negated());
743 if (new_level == 0)
continue;
745 sat_solver->Decisions()[new_level - 1].literal;
746 int num_new_subsumed = 0;
747 for (
int i = first_new_trail_index;
i < trail.Index(); ++
i) {
749 if (l == last_decision)
continue;
756 bool subsumed =
false;
758 trail.AssignmentType(l.
Variable()) == clause_id) {
760 if (lit == last_decision.
Negated()) {
768 CHECK(implication_graph->AddBinaryClause(last_decision.
Negated(), l));
769 const int trail_index = trail.Info(l.
Variable()).trail_index;
773 clause_manager->ReasonClause(trail_index)->AsSpan()) {
774 if (lit == l) ++test;
775 if (lit == last_decision.
Negated()) ++test;
778 clause_manager->LazyDetach(clause_manager->ReasonClause(trail_index));
781 implication_graph->ChangeReason(trail_index, last_decision);
803 if (!subsumed && trail.AssignmentType(l.
Variable()) !=
id) {
805 CHECK(implication_graph->AddBinaryClause(last_decision.
Negated(), l));
831 const bool always_add_binary = sat_solver->CurrentDecisionLevel() > 1 &&
835 clause_manager->WatcherListOnFalse(last_decision.
Negated())) {
836 if (assignment.LiteralIsTrue(
w.blocking_literal)) {
837 if (
w.clause->IsRemoved())
continue;
838 CHECK_NE(
w.blocking_literal, last_decision.
Negated());
848 if (always_add_binary ||
849 trail.AssignmentType(
w.blocking_literal.Variable()) !=
id) {
852 const auto& info = trail.Info(
w.blocking_literal.Variable());
853 if (info.level > 0) {
855 CHECK(implication_graph->AddBinaryClause(last_decision.
Negated(),
856 w.blocking_literal));
858 const Literal d = sat_solver->Decisions()[info.level - 1].literal;
859 if (d !=
w.blocking_literal) {
860 implication_graph->ChangeReason(info.trail_index, d);
866 clause_manager->LazyDetach(
w.clause);
871 if (num_new_subsumed > 0) {
875 clause_manager->CleanUpWatchers();
876 num_subsumed += num_new_subsumed;
880 if (!sat_solver->ResetToLevelZero())
return false;
881 for (
const Literal literal : to_fix) {
883 if (!sat_solver->AddUnitClause(literal))
return false;
886 if (!sat_solver->FinishPropagation())
return false;
889 const int num_fixed = sat_solver->LiteralTrail().Index();
890 const int num_newly_fixed = num_fixed - initial_num_fixed;
891 const double time_diff =
892 time_limit->GetElapsedDeterministicTime() - initial_deterministic_time;
893 const bool limit_reached =
time_limit->LimitReached() ||
894 time_limit->GetElapsedDeterministicTime() > limit;
897 <<
" num_probed: " << num_probed <<
"/" << probing_order.size()
898 <<
" num_fixed: +" << num_newly_fixed <<
" (" << num_fixed <<
"/"
899 << num_variables <<
")"
900 <<
" explicit_fix:" << num_explicit_fix
901 <<
" num_conflicts:" << num_conflicts
902 <<
" new_binary_clauses: " << num_new_binary
903 <<
" subsumed: " << num_subsumed <<
" dtime: " << time_diff
904 <<
" wtime: " << wall_timer.
Get() << (limit_reached ?
" (Aborted)" :
"");
905 return sat_solver->FinishPropagation();