25#include "absl/base/attributes.h"
26#include "absl/container/btree_set.h"
27#include "absl/container/flat_hash_map.h"
28#include "absl/log/check.h"
29#include "absl/log/log.h"
30#include "absl/log/vlog_is_on.h"
31#include "absl/meta/type_traits.h"
32#include "absl/strings/str_cat.h"
33#include "absl/strings/str_format.h"
34#include "absl/types/span.h"
47#include "ortools/sat/sat_parameters.pb.h"
60 owned_model_.reset(model_);
69 track_binary_clauses_(false),
72 parameters_(
model->GetOrCreate<SatParameters>()),
76 clause_activity_increment_(1.0),
77 same_reason_identifier_(*trail_),
78 is_relevant_for_core_computation_(true),
79 drat_proof_handler_(nullptr),
81 InitializePropagators();
88 CHECK_GE(num_variables, num_variables_);
90 num_variables_ = num_variables;
91 binary_implication_graph_->Resize(num_variables);
92 clauses_propagator_->Resize(num_variables);
93 trail_->Resize(num_variables);
94 decision_policy_->IncreaseNumVariables(num_variables);
95 pb_constraints_->Resize(num_variables);
96 same_reason_identifier_.Resize(num_variables);
101 decisions_.resize(num_variables + 1);
109 return trail_->NumberOfEnqueues() - counters_.num_branches;
123 return 1e-8 * (8.0 * trail_->NumberOfEnqueues() +
124 1.0 * binary_implication_graph_->num_inspections() +
125 4.0 * clauses_propagator_->num_inspected_clauses() +
126 1.0 * clauses_propagator_->num_inspected_clause_literals() +
129 20.0 * pb_constraints_->num_constraint_lookups() +
130 2.0 * pb_constraints_->num_threshold_updates() +
131 1.0 * pb_constraints_->num_inspected_constraint_literals());
143 time_limit_->ResetLimitFromParameters(
parameters);
144 logger_->EnableLogging(
parameters.log_search_progress() || VLOG_IS_ON(1));
145 logger_->SetLogToStdOut(
parameters.log_to_stdout());
148bool SatSolver::IsMemoryLimitReached()
const {
149 const int64_t memory_usage =
151 const int64_t kMegaByte = 1024 * 1024;
152 return memory_usage > kMegaByte * parameters_->max_memory_in_mb();
155bool SatSolver::SetModelUnsat() {
156 model_is_unsat_ =
true;
161 if (model_is_unsat_)
return false;
164 if (trail_->CurrentDecisionLevel() == 0) {
168 const int index = trail_->Index();
169 if (literals.empty())
return SetModelUnsat();
171 if (literals.size() == 2) {
175 if (!binary_implication_graph_->AddBinaryClause(literals[0], literals[1])) {
177 return SetModelUnsat();
180 if (!clauses_propagator_->AddClause(literals)) {
182 return SetModelUnsat();
189 if (trail_->Index() == index)
return true;
214 if (model_is_unsat_)
return false;
218 literals_scratchpad_.clear();
220 l = binary_implication_graph_->RepresentativeOf(l);
221 if (trail_->Assignment().LiteralIsTrue(l))
return true;
222 if (trail_->Assignment().LiteralIsFalse(l))
continue;
223 literals_scratchpad_.push_back(l);
228 for (
int i = 0;
i + 1 < literals_scratchpad_.size(); ++
i) {
229 if (literals_scratchpad_[
i] == literals_scratchpad_[
i + 1].Negated()) {
234 return AddProblemClauseInternal(literals_scratchpad_);
237bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
240 for (
const Literal l : literals) {
245 if (literals.empty())
return SetModelUnsat();
247 if (literals.size() == 1) {
248 if (drat_proof_handler_ !=
nullptr) {
251 drat_proof_handler_->
AddClause({literals[0]});
253 trail_->EnqueueWithUnitReason(literals[0]);
254 }
else if (literals.size() == 2) {
256 if (literals[0] == literals[1]) {
258 trail_->EnqueueWithUnitReason(literals[0]);
259 }
else if (literals[0] == literals[1].Negated()) {
263 AddBinaryClauseInternal(literals[0], literals[1]);
266 if (!clauses_propagator_->AddClause(literals, trail_, -1)) {
267 return SetModelUnsat();
275 if (!PropagationIsDone() && !
Propagate()) {
276 return SetModelUnsat();
281bool SatSolver::AddLinearConstraintInternal(
282 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
283 Coefficient max_value) {
286 if (rhs < 0)
return SetModelUnsat();
287 if (rhs >= max_value)
return true;
290 const Coefficient min_coeff = cst.front().coefficient;
291 const Coefficient max_coeff = cst.back().coefficient;
295 if (max_value - min_coeff <= rhs) {
297 literals_scratchpad_.clear();
298 for (
const LiteralWithCoeff& term : cst) {
299 literals_scratchpad_.push_back(term.literal.Negated());
301 return AddProblemClauseInternal(literals_scratchpad_);
306 if (!parameters_->use_pb_resolution() && max_coeff <= rhs &&
307 2 * min_coeff > rhs) {
308 literals_scratchpad_.clear();
309 for (
const LiteralWithCoeff& term : cst) {
310 literals_scratchpad_.push_back(term.literal);
312 if (!binary_implication_graph_->AddAtMostOne(literals_scratchpad_)) {
313 return SetModelUnsat();
320 return pb_constraints_->AddConstraint(cst, rhs, trail_);
323void SatSolver::CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
324 Coefficient* bound_shift,
325 Coefficient* max_value) {
327 Coefficient fixed_variable_shift(0);
330 for (
const LiteralWithCoeff& term : *cst) {
331 if (trail_->Assignment().LiteralIsFalse(term.literal))
continue;
332 if (trail_->Assignment().LiteralIsTrue(term.literal)) {
333 CHECK(
SafeAddInto(-term.coefficient, &fixed_variable_shift));
336 (*cst)[index] = term;
344 Coefficient bound_delta(0);
349 CHECK(
SafeAddInto(fixed_variable_shift, bound_shift));
353 Coefficient lower_bound,
354 bool use_upper_bound,
355 Coefficient upper_bound,
356 std::vector<LiteralWithCoeff>* cst) {
359 if (model_is_unsat_)
return false;
361 Coefficient bound_shift(0);
363 if (use_upper_bound) {
364 Coefficient max_value(0);
365 CanonicalizeLinear(cst, &bound_shift, &max_value);
366 const Coefficient rhs =
368 if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
369 return SetModelUnsat();
373 if (use_lower_bound) {
376 Coefficient max_value(0);
377 CanonicalizeLinear(cst, &bound_shift, &max_value);
380 for (
int i = 0;
i < cst->size(); ++
i) {
381 (*cst)[
i].literal = (*cst)[
i].literal.Negated();
383 const Coefficient rhs =
385 if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
386 return SetModelUnsat();
394 if (!PropagationIsDone() && !
Propagate()) {
395 return SetModelUnsat();
400int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
401 const std::vector<Literal>& literals,
bool is_redundant) {
404 if (literals.size() == 1) {
412 if (literals.size() == 2) {
413 if (track_binary_clauses_) {
415 CHECK(binary_clauses_.
Add(BinaryClause(literals[0], literals[1])));
417 CHECK(binary_implication_graph_->
AddBinaryClause(literals[0], literals[1]));
421 CleanClauseDatabaseIfNeeded();
425 const int lbd = ComputeLbd(literals);
426 if (is_redundant && lbd > parameters_->clause_cleanup_lbd_bound()) {
427 --num_learned_clause_before_cleanup_;
430 clauses_propagator_->AddRemovableClause(literals, trail_, lbd);
434 (*clauses_propagator_->mutable_clauses_info())[clause].lbd = lbd;
435 BumpClauseActivity(clause);
437 CHECK(clauses_propagator_->AddClause(literals, trail_, lbd));
444 trail_->RegisterPropagator(propagator);
445 external_propagators_.push_back(propagator);
446 InitializePropagators();
451 CHECK(last_propagator_ ==
nullptr);
452 trail_->RegisterPropagator(propagator);
453 last_propagator_ = propagator;
454 InitializePropagators();
458 BooleanVariable var)
const {
468SatClause* SatSolver::ReasonClauseOrNull(BooleanVariable var)
const {
470 const AssignmentInfo& info = trail_->
Info(var);
472 return clauses_propagator_->
ReasonClause(info.trail_index);
478 debug_assignment_.Resize(num_variables_.value());
479 for (BooleanVariable
i(0);
i < num_variables_; ++
i) {
480 debug_assignment_.AssignFromTrueLiteral(
481 trail_->Assignment().GetTrueLiteralForAssignedVariable(
i));
486 debug_assignment_.Resize(num_variables_.value());
487 for (BooleanVariable var(0); var < num_variables_; ++var) {
488 if (!debug_assignment_.VariableIsAssigned(var))
continue;
489 debug_assignment_.UnassignLiteral(
Literal(var,
true));
492 debug_assignment_.AssignFromTrueLiteral(l);
496 for (BooleanVariable var(0); var < num_variables_; ++var) {
497 CHECK(debug_assignment_.VariableIsAssigned(var));
502 if (track_binary_clauses_) {
513bool SatSolver::ClauseIsValidUnderDebugAssignment(
514 absl::Span<const Literal> clause)
const {
515 if (debug_assignment_.NumberOfVariables() == 0)
return true;
516 for (Literal l : clause) {
517 if (l.Variable() >= debug_assignment_.NumberOfVariables() ||
518 debug_assignment_.LiteralIsTrue(l)) {
525bool SatSolver::PBConstraintIsValidUnderDebugAssignment(
526 absl::Span<const LiteralWithCoeff> cst,
const Coefficient rhs)
const {
527 Coefficient sum(0.0);
528 for (LiteralWithCoeff term : cst) {
529 if (term.literal.Variable() >= debug_assignment_.NumberOfVariables()) {
532 if (debug_assignment_.LiteralIsTrue(term.literal)) {
533 sum += term.coefficient;
543bool ClauseSubsumption(absl::Span<const Literal> a,
SatClause*
b) {
544 std::vector<Literal> superset(
b->begin(),
b->end());
545 std::vector<Literal> subset(a.begin(), a.end());
546 std::sort(superset.begin(), superset.end());
547 std::sort(subset.begin(), subset.end());
548 return std::includes(superset.begin(), superset.end(), subset.begin(),
557 DCHECK(PropagationIsDone());
561 CHECK_GE(current_decision_level_, assumption_level_);
564 EnqueueNewDecision(true_literal);
566 return last_decision_or_backtrack_trail_index_;
570 if (model_is_unsat_)
return false;
580 if (model_is_unsat_)
return false;
583 const int old_decision_level = current_decision_level_;
586 if (model_is_unsat_)
return false;
587 if (current_decision_level_ == old_decision_level) {
588 CHECK(!assumptions_.empty());
592 if (++num_loop % 16 == 0 && time_limit_->LimitReached()) {
603 DCHECK(PropagationIsDone());
608 if (model_is_unsat_)
return false;
609 assumption_level_ = 0;
610 assumptions_.clear();
616 const std::vector<Literal>& assumptions) {
618 if (assumptions.empty())
return true;
625 DCHECK(assumptions_.empty());
626 assumption_level_ = 1;
627 assumptions_ = assumptions;
633 if (model_is_unsat_)
return false;
639 CHECK_EQ(current_decision_level_, 0);
640 last_decision_or_backtrack_trail_index_ = trail_->Index();
643 ++current_decision_level_;
644 trail_->SetDecisionLevel(current_decision_level_);
647 int num_decisions = 0;
648 for (
const Literal lit : assumptions_) {
649 if (
Assignment().LiteralIsTrue(lit))
continue;
652 *trail_->MutableConflict() = {lit.Negated(), lit};
653 if (num_decisions == 0) {
655 current_decision_level_ = 0;
656 trail_->SetDecisionLevel(0);
661 trail_->EnqueueSearchDecision(lit);
665 if (num_decisions == 0) {
666 current_decision_level_ = 0;
667 trail_->SetDecisionLevel(0);
675 DCHECK(assumptions_.empty());
676 const int64_t old_num_branches = counters_.num_branches;
678 counters_.num_branches = old_num_branches;
685 if (model_is_unsat_)
return;
687 ++counters_.num_failures;
688 const int conflict_trail_index = trail_->Index();
689 const int conflict_decision_level = current_decision_level_;
692 same_reason_identifier_.Clear();
693 const int max_trail_index = ComputeMaxTrailIndex(trail_->FailingClause());
694 if (!assumptions_.empty() && !trail_->FailingClause().empty()) {
701 const int highest_level =
702 DecisionLevel((*trail_)[max_trail_index].
Variable());
703 if (highest_level == 1)
return;
706 ComputeFirstUIPConflict(max_trail_index, &learned_conflict_,
707 &reason_used_to_infer_the_conflict_,
711 if (learned_conflict_.empty())
return (
void)SetModelUnsat();
712 DCHECK(IsConflictValid(learned_conflict_));
713 DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
719 decision_policy_->BumpVariableActivities(learned_conflict_);
720 decision_policy_->BumpVariableActivities(reason_used_to_infer_the_conflict_);
721 if (parameters_->also_bump_variables_in_conflict_reasons()) {
722 ComputeUnionOfReasons(learned_conflict_, &extra_reason_literals_);
723 decision_policy_->BumpVariableActivities(extra_reason_literals_);
729 if (trail_->FailingSatClause() !=
nullptr) {
730 BumpClauseActivity(trail_->FailingSatClause());
732 BumpReasonActivities(reason_used_to_infer_the_conflict_);
735 decision_policy_->UpdateVariableActivityIncrement();
736 UpdateClauseActivityIncrement();
737 pb_constraints_->UpdateActivityIncrement();
740 const int period = parameters_->glucose_decay_increment_period();
741 const double max_decay = parameters_->glucose_max_decay();
742 if (counters_.num_failures % period == 0 &&
743 parameters_->variable_activity_decay() < max_decay) {
744 parameters_->set_variable_activity_decay(
745 parameters_->variable_activity_decay() +
746 parameters_->glucose_decay_increment());
752 bool compute_pb_conflict =
false;
753 if (parameters_->use_pb_resolution()) {
754 compute_pb_conflict = (pb_constraints_->ConflictingConstraint() !=
nullptr);
755 if (!compute_pb_conflict) {
756 for (
Literal lit : reason_used_to_infer_the_conflict_) {
757 if (ReasonPbConstraintOrNull(lit.Variable()) !=
nullptr) {
758 compute_pb_conflict =
true;
767 if (compute_pb_conflict) {
768 pb_conflict_.ClearAndResize(num_variables_.value());
769 Coefficient initial_slack(-1);
770 if (pb_constraints_->ConflictingConstraint() ==
nullptr) {
772 Coefficient num_literals(0);
773 for (
Literal literal : trail_->FailingClause()) {
774 pb_conflict_.AddTerm(literal.Negated(), Coefficient(1.0));
777 pb_conflict_.AddToRhs(num_literals - 1);
780 pb_constraints_->ConflictingConstraint()->AddToConflict(&pb_conflict_);
781 pb_constraints_->ClearConflictingConstraint();
783 pb_conflict_.ComputeSlackForTrailPrefix(*trail_, max_trail_index + 1);
786 int pb_backjump_level;
787 ComputePBConflict(max_trail_index, initial_slack, &pb_conflict_,
789 if (pb_backjump_level == -1)
return (
void)SetModelUnsat();
792 std::vector<LiteralWithCoeff> cst;
793 pb_conflict_.CopyIntoVector(&cst);
794 DCHECK(PBConstraintIsValidUnderDebugAssignment(cst, pb_conflict_.Rhs()));
798 bool conflict_is_a_clause = (pb_conflict_.Rhs() == cst.size() - 1);
799 if (conflict_is_a_clause) {
801 if (term.coefficient != Coefficient(1)) {
802 conflict_is_a_clause =
false;
808 if (!conflict_is_a_clause) {
810 DCHECK_GT(pb_constraints_->NumberOfConstraints(), 0);
813 CHECK(pb_constraints_->AddLearnedConstraint(cst, pb_conflict_.Rhs(),
815 CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_);
816 counters_.num_learned_pb_literals += cst.size();
822 if (pb_backjump_level < ComputeBacktrackLevel(learned_conflict_)) {
823 subsumed_clauses_.clear();
824 learned_conflict_.clear();
825 is_marked_.ClearAndResize(num_variables_);
829 DCHECK(
Assignment().LiteralIsTrue(term.literal));
830 DCHECK_EQ(term.coefficient, 1);
831 const int level = trail_->Info(term.literal.Variable()).level;
832 if (level == 0)
continue;
833 if (level > max_level) {
835 max_index = learned_conflict_.size();
837 learned_conflict_.push_back(term.literal.Negated());
841 is_marked_.Set(term.literal.Variable());
843 CHECK(!learned_conflict_.empty());
844 std::swap(learned_conflict_.front(), learned_conflict_[max_index]);
845 DCHECK(IsConflictValid(learned_conflict_));
854 DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
855 if (!binary_implication_graph_->IsEmpty()) {
856 if (parameters_->binary_minimization_algorithm() ==
857 SatParameters::BINARY_MINIMIZATION_FIRST) {
858 binary_implication_graph_->MinimizeConflictFirst(
859 *trail_, &learned_conflict_, &is_marked_);
860 }
else if (parameters_->binary_minimization_algorithm() ==
862 BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION) {
863 binary_implication_graph_->MinimizeConflictFirstWithTransitiveReduction(
864 *trail_, &learned_conflict_,
867 DCHECK(IsConflictValid(learned_conflict_));
871 MinimizeConflict(&learned_conflict_);
874 if (!binary_implication_graph_->IsEmpty()) {
878 switch (parameters_->binary_minimization_algorithm()) {
879 case SatParameters::NO_BINARY_MINIMIZATION:
880 ABSL_FALLTHROUGH_INTENDED;
881 case SatParameters::BINARY_MINIMIZATION_FIRST:
882 ABSL_FALLTHROUGH_INTENDED;
883 case SatParameters::BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION:
885 case SatParameters::BINARY_MINIMIZATION_WITH_REACHABILITY:
886 binary_implication_graph_->MinimizeConflictWithReachability(
889 case SatParameters::EXPERIMENTAL_BINARY_MINIMIZATION:
890 binary_implication_graph_->MinimizeConflictExperimental(
891 *trail_, &learned_conflict_);
894 DCHECK(IsConflictValid(learned_conflict_));
905 decision_policy_->BeforeConflict(trail_->Index());
908 counters_.num_literals_learned += learned_conflict_.size();
909 Backtrack(ComputeBacktrackLevel(learned_conflict_));
910 DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
916 if (drat_proof_handler_ !=
nullptr) {
917 drat_proof_handler_->AddClause(learned_conflict_);
926 if (parameters_->minimization_algorithm() == SatParameters::EXPERIMENTAL) {
927 subsumed_clauses_.clear();
932 bool is_redundant =
true;
933 if (!subsumed_clauses_.empty() &&
934 parameters_->subsumption_during_conflict_analysis()) {
935 for (
SatClause* clause : subsumed_clauses_) {
936 DCHECK(ClauseSubsumption(learned_conflict_, clause));
937 if (!clauses_propagator_->IsRemovable(clause)) {
938 is_redundant =
false;
940 clauses_propagator_->LazyDetach(clause);
942 clauses_propagator_->CleanUpWatchers();
943 counters_.num_subsumed_clauses += subsumed_clauses_.size();
947 const int conflict_lbd = AddLearnedClauseAndEnqueueUnitPropagation(
948 learned_conflict_, is_redundant);
949 restart_->OnConflict(conflict_trail_index, conflict_decision_level,
954 int max_level,
int* first_propagation_index) {
956 DCHECK(assumptions_.empty());
957 int decision_index = current_decision_level_;
958 while (decision_index <= max_level) {
959 DCHECK_GE(decision_index, current_decision_level_);
960 const Literal previous_decision = decisions_[decision_index].literal;
962 if (
Assignment().LiteralIsTrue(previous_decision)) {
968 if (
Assignment().LiteralIsFalse(previous_decision)) {
976 const int old_level = current_decision_level_;
978 if (first_propagation_index !=
nullptr) {
979 *first_propagation_index = std::min(*first_propagation_index, index);
982 if (current_decision_level_ <= old_level) {
994 decision_index = current_decision_level_;
1001 Literal true_literal,
int* first_propagation_index) {
1003 CHECK(PropagationIsDone());
1004 CHECK(assumptions_.empty());
1008 if (first_propagation_index !=
nullptr) {
1009 *first_propagation_index = trail_->Index();
1016 DCHECK(PropagationIsDone());
1020 EnqueueNewDecision(true_literal);
1040 DCHECK(target_level == 0 || !
Decisions().empty());
1042 DCHECK_GE(target_level, 0);
1046 counters_.num_backtracks++;
1047 if (target_level == 0) counters_.num_restarts++;
1050 trail_->SetDecisionLevel(target_level);
1052 current_decision_level_ = target_level;
1053 const int target_trail_index =
1054 decisions_[current_decision_level_].trail_index;
1056 DCHECK_LT(target_trail_index, trail_->Index());
1058 if (propagator->IsEmpty())
continue;
1059 propagator->Untrail(*trail_, target_trail_index);
1061 decision_policy_->Untrail(target_trail_index);
1062 trail_->Untrail(target_trail_index);
1064 last_decision_or_backtrack_trail_index_ = trail_->Index();
1073 if (!
Propagate())
return SetModelUnsat();
1078 return binary_clauses_.newly_added();
1082 binary_clauses_.ClearNewlyAdded();
1087int64_t NextMultipleOf(int64_t value, int64_t interval) {
1088 return interval * (1 + value / interval);
1093 const std::vector<Literal>& assumptions, int64_t max_number_of_conflicts) {
1096 return SolveInternal(time_limit_,
1097 max_number_of_conflicts >= 0
1098 ? max_number_of_conflicts
1099 : parameters_->max_number_of_conflicts());
1103 SOLVER_LOG(logger_, RunningStatisticsString());
1109 CHECK_GE(assumption_level, 0);
1111 assumption_level_ = assumption_level;
1114 if (!assumptions_.empty()) {
1115 CHECK_EQ(assumption_level, 0);
1116 assumptions_.clear();
1122 parameters_->max_number_of_conflicts());
1126 return SolveInternal(time_limit_, parameters_->max_number_of_conflicts());
1129void SatSolver::KeepAllClausesUsedToInfer(BooleanVariable variable) {
1130 CHECK(
Assignment().VariableIsAssigned(variable));
1131 if (trail_->
Info(variable).
level == 0)
return;
1133 std::vector<bool> is_marked(trail_index + 1,
false);
1134 is_marked[trail_index] =
true;
1136 for (; num > 0 && trail_index >= 0; --trail_index) {
1137 if (!is_marked[trail_index])
continue;
1138 is_marked[trail_index] =
false;
1141 const BooleanVariable var = (*trail_)[trail_index].Variable();
1142 SatClause* clause = ReasonClauseOrNull(var);
1143 if (clause !=
nullptr) {
1150 for (
const Literal l : trail_->
Reason(var)) {
1151 const AssignmentInfo& info = trail_->
Info(l.Variable());
1152 if (info.level == 0)
continue;
1153 if (!is_marked[info.trail_index]) {
1154 is_marked[info.trail_index] =
true;
1161bool SatSolver::SubsumptionIsInteresting(BooleanVariable variable,
1166 const int binary_id = binary_implication_graph_->PropagatorId();
1167 const int clause_id = clauses_propagator_->PropagatorId();
1169 CHECK(
Assignment().VariableIsAssigned(variable));
1170 if (trail_->Info(variable).level == 0)
return true;
1171 int trail_index = trail_->Info(variable).trail_index;
1172 std::vector<bool> is_marked(trail_index + 1,
false);
1173 is_marked[trail_index] =
true;
1175 int num_clause_to_mark_as_non_deletable = 0;
1176 for (; num > 0 && trail_index >= 0; --trail_index) {
1177 if (!is_marked[trail_index])
continue;
1178 is_marked[trail_index] =
false;
1181 const BooleanVariable var = (*trail_)[trail_index].Variable();
1182 const int type = trail_->AssignmentType(var);
1184 if (type != binary_id && type != clause_id)
return false;
1185 SatClause* clause = ReasonClauseOrNull(var);
1186 if (clause !=
nullptr && clauses_propagator_->IsRemovable(clause)) {
1187 if (clause->size() > max_size) {
1190 if (++num_clause_to_mark_as_non_deletable > 1)
return false;
1192 for (
const Literal l : trail_->Reason(var)) {
1193 const AssignmentInfo& info = trail_->Info(l.Variable());
1194 if (info.level == 0)
continue;
1195 if (!is_marked[info.trail_index]) {
1196 is_marked[info.trail_index] =
true;
1201 return num_clause_to_mark_as_non_deletable <= 1;
1210void SatSolver::TryToMinimizeClause(
SatClause* clause) {
1211 CHECK(clause !=
nullptr);
1212 ++counters_.minimization_num_clauses;
1214 std::vector<Literal> candidate;
1215 candidate.reserve(clause->size());
1225 int longest_valid_prefix = 0;
1227 candidate.resize(clause->size());
1229 for (Literal lit : *clause) {
1230 if (!
Assignment().LiteralIsFalse(lit))
continue;
1231 const AssignmentInfo& info = trail_->Info(lit.Variable());
1232 if (info.level <= 0 || info.level > clause->size())
continue;
1233 if (decisions_[info.level - 1].literal == lit.Negated()) {
1234 candidate[info.level - 1] = lit;
1238 for (
int i = 0;
i < candidate.size(); ++
i) {
1239 if (candidate[
i] != Literal()) {
1240 ++longest_valid_prefix;
1245 counters_.minimization_num_reused += longest_valid_prefix;
1246 candidate.resize(longest_valid_prefix);
1249 for (Literal lit : *clause) {
1250 const AssignmentInfo& info = trail_->Info(lit.Variable());
1252 if (info.level >= 1 && info.level <= longest_valid_prefix &&
1253 candidate[info.level - 1] == lit) {
1256 candidate.push_back(lit);
1258 CHECK_EQ(candidate.size(), clause->size());
1261 absl::btree_set<LiteralIndex> moved_last;
1262 while (!model_is_unsat_) {
1269 if (target_level == -1)
break;
1273 if (time_limit_->LimitReached())
return;
1275 const Literal literal = candidate[level];
1278 candidate[level] = candidate.back();
1279 candidate.pop_back();
1281 }
else if (
Assignment().LiteralIsTrue(literal)) {
1282 const int variable_level =
1284 if (variable_level == 0) {
1285 ProcessNewlyFixedVariablesForDratProof();
1286 counters_.minimization_num_true++;
1287 counters_.minimization_num_removed_literals += clause->size();
1289 clauses_propagator_->Detach(clause);
1293 if (parameters_->inprocessing_minimization_use_conflict_analysis()) {
1299 candidate.push_back(lit.Negated());
1302 candidate.resize(variable_level);
1304 candidate.push_back(literal);
1312 if (ReasonClauseOrNull(literal.Variable()) != clause &&
1313 SubsumptionIsInteresting(literal.Variable(), candidate.size())) {
1314 counters_.minimization_num_subsumed++;
1315 counters_.minimization_num_removed_literals += clause->size();
1316 KeepAllClausesUsedToInfer(literal.Variable());
1318 clauses_propagator_->Detach(clause);
1324 ++counters_.minimization_num_decisions;
1326 if (clause->IsRemoved()) {
1330 if (model_is_unsat_)
return;
1342 if (candidate.empty()) {
1343 model_is_unsat_ =
true;
1346 if (!parameters_->inprocessing_minimization_use_all_orderings())
break;
1347 moved_last.insert(candidate.back().Index());
1350 if (candidate.empty()) {
1351 model_is_unsat_ =
true;
1356 if (candidate.size() == clause->size())
return;
1359 if (candidate.size() == 1) {
1360 if (drat_proof_handler_ !=
nullptr) {
1361 drat_proof_handler_->AddClause(candidate);
1363 if (!
Assignment().VariableIsAssigned(candidate[0].Variable())) {
1364 counters_.minimization_num_removed_literals += clause->size();
1365 trail_->EnqueueWithUnitReason(candidate[0]);
1371 if (candidate.size() == 2) {
1372 counters_.minimization_num_removed_literals += clause->size() - 2;
1375 AddBinaryClauseInternal(candidate[0], candidate[1]);
1376 clauses_propagator_->Detach(clause);
1384 counters_.minimization_num_removed_literals +=
1385 clause->size() - candidate.size();
1389 if (!clauses_propagator_->InprocessingRewriteClause(clause, candidate)) {
1390 model_is_unsat_ =
true;
1395 int64_t max_number_of_conflicts) {
1405 if (logger_->LoggingIsEnabled()) {
1407 SOLVER_LOG(logger_,
"Number of variables: ", num_variables_.value());
1408 SOLVER_LOG(logger_,
"Number of clauses (size > 2): ",
1409 clauses_propagator_->num_clauses());
1410 SOLVER_LOG(logger_,
"Number of binary clauses: ",
1411 binary_implication_graph_->ComputeNumImplicationsForLog());
1412 SOLVER_LOG(logger_,
"Number of linear constraints: ",
1413 pb_constraints_->NumberOfConstraints());
1414 SOLVER_LOG(logger_,
"Number of fixed variables: ", trail_->Index());
1415 SOLVER_LOG(logger_,
"Number of watched clauses: ",
1416 clauses_propagator_->num_watched_clauses());
1421 const int64_t kDisplayFrequency = 10000;
1422 int64_t next_display = parameters_->log_search_progress()
1424 : std::numeric_limits<int64_t>::max();
1427 const int64_t kMemoryCheckFrequency = 10000;
1428 int64_t next_memory_check =
1433 const int64_t kFailureLimit =
1434 max_number_of_conflicts == std::numeric_limits<int64_t>::max()
1435 ? std::numeric_limits<int64_t>::max()
1444 SOLVER_LOG(logger_,
"The time limit has been reached. Aborting.");
1449 SOLVER_LOG(logger_,
"The conflict limit has been reached. Aborting.");
1458 if (counters_.num_failures >= next_memory_check) {
1459 next_memory_check = NextMultipleOf(
num_failures(), kMemoryCheckFrequency);
1460 if (IsMemoryLimitReached()) {
1461 SOLVER_LOG(logger_,
"The memory limit has been reached. Aborting.");
1468 if (counters_.num_failures >= next_display) {
1469 SOLVER_LOG(logger_, RunningStatisticsString());
1470 next_display = NextMultipleOf(
num_failures(), kDisplayFrequency);
1473 const int old_level = current_decision_level_;
1477 if (model_is_unsat_)
return StatusWithLog(
INFEASIBLE);
1478 if (old_level == current_decision_level_) {
1479 CHECK(!assumptions_.empty());
1487 if (trail_->Index() == num_variables_.value()) {
1491 if (restart_->ShouldRestart()) {
1496 EnqueueNewDecision(decision_policy_->NextBranch());
1502 bool minimize_new_clauses_only) {
1503 CHECK(time_limit_ !=
nullptr);
1505 const double threshold = time_limit_->GetElapsedDeterministicTime() + dtime;
1509 block_clause_deletion_ =
true;
1512 while (!time_limit_->LimitReached() &&
1513 time_limit_->GetElapsedDeterministicTime() < threshold) {
1514 SatClause* to_minimize = clauses_propagator_->NextNewClauseToMinimize();
1515 if (!minimize_new_clauses_only && to_minimize ==
nullptr) {
1516 to_minimize = clauses_propagator_->NextClauseToMinimize();
1519 if (to_minimize !=
nullptr) {
1520 TryToMinimizeClause(to_minimize);
1521 if (model_is_unsat_)
return false;
1522 }
else if (minimize_new_clauses_only) {
1526 VLOG(1) <<
"Minimized all clauses, restarting from first one.";
1527 clauses_propagator_->ResetToMinimizeIndex();
1528 if (num_resets > 1)
break;
1539 block_clause_deletion_ =
false;
1540 clauses_propagator_->DeleteRemovedClauses();
1545 std::vector<Literal>* clause = trail_->MutableConflict();
1547 for (
int i = 0;
i < clause->size(); ++
i) {
1548 const Literal literal = (*clause)[
i];
1553 std::swap((*clause)[
i], (*clause)[num_true++]);
1556 CHECK_LE(num_true, 1);
1557 std::vector<Literal> result =
1559 for (
int i = 0;
i < num_true; ++
i) {
1560 result.push_back((*clause)[
i].Negated());
1566 absl::Span<const Literal> literals) {
1568 std::vector<Literal> unsat_assumptions;
1570 is_marked_.ClearAndResize(num_variables_);
1572 int trail_index = 0;
1573 for (
const Literal lit : literals) {
1576 std::max(trail_index, trail_->Info(lit.Variable()).trail_index);
1577 is_marked_.Set(lit.Variable());
1583 CHECK_LT(trail_index, trail_->Index());
1586 while (trail_index >= limit &&
1587 !is_marked_[(*trail_)[trail_index].
Variable()]) {
1590 if (trail_index < limit)
break;
1591 const Literal marked_literal = (*trail_)[trail_index];
1594 if (trail_->AssignmentType(marked_literal.
Variable()) ==
1596 unsat_assumptions.push_back(marked_literal);
1599 for (
const Literal literal : trail_->Reason(marked_literal.
Variable())) {
1600 const BooleanVariable var = literal.Variable();
1601 const int level = DecisionLevel(var);
1602 if (level > 0 && !is_marked_[var]) is_marked_.Set(var);
1609 std::reverse(unsat_assumptions.begin(), unsat_assumptions.end());
1610 return unsat_assumptions;
1613void SatSolver::BumpReasonActivities(absl::Span<const Literal> literals) {
1615 for (
const Literal literal : literals) {
1616 const BooleanVariable var = literal.Variable();
1617 if (DecisionLevel(var) > 0) {
1618 SatClause* clause = ReasonClauseOrNull(var);
1619 if (clause !=
nullptr) {
1620 BumpClauseActivity(clause);
1622 UpperBoundedLinearConstraint* pb_constraint =
1623 ReasonPbConstraintOrNull(var);
1624 if (pb_constraint !=
nullptr) {
1634void SatSolver::BumpClauseActivity(
SatClause* clause) {
1639 auto it = clauses_propagator_->mutable_clauses_info()->find(clause);
1640 if (it == clauses_propagator_->mutable_clauses_info()->end())
return;
1645 const int new_lbd = ComputeLbd(*clause);
1646 if (new_lbd + 1 <= parameters_->clause_cleanup_lbd_bound()) {
1647 clauses_propagator_->mutable_clauses_info()->erase(clause);
1652 switch (parameters_->clause_cleanup_protection()) {
1653 case SatParameters::PROTECTION_NONE:
1655 case SatParameters::PROTECTION_ALWAYS:
1656 it->second.protected_during_next_cleanup =
true;
1658 case SatParameters::PROTECTION_LBD:
1663 if (new_lbd + 1 < it->second.lbd) {
1664 it->second.protected_during_next_cleanup =
true;
1665 it->second.lbd = new_lbd;
1670 const double activity = it->second.activity += clause_activity_increment_;
1671 if (activity > parameters_->max_clause_activity_value()) {
1672 RescaleClauseActivities(1.0 / parameters_->max_clause_activity_value());
1676void SatSolver::RescaleClauseActivities(
double scaling_factor) {
1678 clause_activity_increment_ *= scaling_factor;
1679 for (
auto& entry : *clauses_propagator_->mutable_clauses_info()) {
1680 entry.second.activity *= scaling_factor;
1684void SatSolver::UpdateClauseActivityIncrement() {
1686 clause_activity_increment_ *= 1.0 / parameters_->clause_activity_decay();
1689bool SatSolver::IsConflictValid(absl::Span<const Literal> literals) {
1691 if (literals.empty())
return false;
1692 const int highest_level = DecisionLevel(literals[0].Variable());
1693 for (
int i = 1;
i < literals.size(); ++
i) {
1694 const int level = DecisionLevel(literals[
i].Variable());
1695 if (level <= 0 || level >= highest_level)
return false;
1700int SatSolver::ComputeBacktrackLevel(absl::Span<const Literal> literals) {
1713 int backtrack_level = 0;
1714 for (
int i = 1;
i < literals.size(); ++
i) {
1715 const int level = DecisionLevel(literals[
i].Variable());
1716 backtrack_level = std::max(backtrack_level, level);
1718 DCHECK_LT(backtrack_level, DecisionLevel(literals[0].Variable()));
1720 return backtrack_level;
1723template <
typename LiteralList>
1724int SatSolver::ComputeLbd(
const LiteralList& literals) {
1727 parameters_->count_assumption_levels_in_lbd() ? 0 : assumption_level_;
1730 is_level_marked_.ClearAndResize(
1731 SatDecisionLevel(DecisionLevel(literals.begin()->Variable()) + 1));
1732 for (
const Literal literal : literals) {
1733 const SatDecisionLevel level(DecisionLevel(literal.Variable()));
1734 DCHECK_GE(level, 0);
1735 if (level > limit && !is_level_marked_[level]) {
1736 is_level_marked_.Set(level);
1739 return is_level_marked_.NumberOfSetCallsWithDifferentArguments();
1742std::string SatSolver::StatusString(Status status)
const {
1743 const double time_in_s = timer_.Get();
1745 absl::StrFormat(
" time: %fs\n", time_in_s) +
1748 " num failures: %d (%.0f /sec)\n", counters_.num_failures,
1749 static_cast<double>(counters_.num_failures) / time_in_s) +
1751 " num branches: %d (%.0f /sec)\n", counters_.num_branches,
1752 static_cast<double>(counters_.num_branches) / time_in_s) +
1753 absl::StrFormat(
" num propagations: %d (%.0f /sec)\n",
1756 absl::StrFormat(
" num binary propagations: %d\n",
1757 binary_implication_graph_->num_propagations()) +
1758 absl::StrFormat(
" num binary inspections: %d\n",
1759 binary_implication_graph_->num_inspections()) +
1761 " num binary redundant implications: %d\n",
1762 binary_implication_graph_->num_redundant_implications()) +
1764 " num classic minimizations: %d"
1765 " (literals removed: %d)\n",
1766 counters_.num_minimizations, counters_.num_literals_removed) +
1768 " num binary minimizations: %d"
1769 " (literals removed: %d)\n",
1770 binary_implication_graph_->num_minimization(),
1771 binary_implication_graph_->num_literals_removed()) +
1772 absl::StrFormat(
" num inspected clauses: %d\n",
1773 clauses_propagator_->num_inspected_clauses()) +
1774 absl::StrFormat(
" num inspected clause_literals: %d\n",
1775 clauses_propagator_->num_inspected_clause_literals()) +
1777 " num learned literals: %d (avg: %.1f /clause)\n",
1778 counters_.num_literals_learned,
1779 1.0 * counters_.num_literals_learned / counters_.num_failures) +
1781 " num learned PB literals: %d (avg: %.1f /clause)\n",
1782 counters_.num_learned_pb_literals,
1783 1.0 * counters_.num_learned_pb_literals / counters_.num_failures) +
1784 absl::StrFormat(
" num subsumed clauses: %d\n",
1785 counters_.num_subsumed_clauses) +
1786 absl::StrFormat(
" minimization_num_clauses: %d\n",
1787 counters_.minimization_num_clauses) +
1788 absl::StrFormat(
" minimization_num_decisions: %d\n",
1789 counters_.minimization_num_decisions) +
1790 absl::StrFormat(
" minimization_num_true: %d\n",
1791 counters_.minimization_num_true) +
1792 absl::StrFormat(
" minimization_num_subsumed: %d\n",
1793 counters_.minimization_num_subsumed) +
1794 absl::StrFormat(
" minimization_num_removed_literals: %d\n",
1795 counters_.minimization_num_removed_literals) +
1796 absl::StrFormat(
" pb num threshold updates: %d\n",
1797 pb_constraints_->num_threshold_updates()) +
1798 absl::StrFormat(
" pb num constraint lookups: %d\n",
1799 pb_constraints_->num_constraint_lookups()) +
1800 absl::StrFormat(
" pb num inspected constraint literals: %d\n",
1801 pb_constraints_->num_inspected_constraint_literals()) +
1802 restart_->InfoString() +
1806std::string SatSolver::RunningStatisticsString()
const {
1807 const double time_in_s = timer_.Get();
1808 return absl::StrFormat(
1809 "%6.2fs, mem:%s, fails:%d, depth:%d, clauses:%d, tmp:%d, bin:%u, "
1810 "restarts:%d, vars:%d",
1812 clauses_propagator_->num_clauses() -
1813 clauses_propagator_->num_removable_clauses(),
1814 clauses_propagator_->num_removable_clauses(),
1815 binary_implication_graph_->ComputeNumImplicationsForLog(),
1816 restart_->NumRestarts(),
1817 num_variables_.value() - num_processed_fixed_variables_);
1820void SatSolver::ProcessNewlyFixedVariablesForDratProof() {
1821 if (drat_proof_handler_ ==
nullptr)
return;
1835 for (; drat_num_processed_fixed_variables_ < trail_->Index();
1836 ++drat_num_processed_fixed_variables_) {
1837 temp = (*trail_)[drat_num_processed_fixed_variables_];
1838 drat_proof_handler_->AddClause({&temp, 1});
1845 int num_detached_clauses = 0;
1848 ProcessNewlyFixedVariablesForDratProof();
1853 const int saved_index = trail_->Index();
1854 for (
SatClause* clause : clauses_propagator_->AllClausesInCreationOrder()) {
1855 if (clause->IsRemoved())
continue;
1857 const size_t old_size = clause->size();
1858 if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->Assignment())) {
1860 clauses_propagator_->LazyDetach(clause);
1861 ++num_detached_clauses;
1865 const size_t new_size = clause->size();
1866 if (new_size == old_size)
continue;
1868 if (drat_proof_handler_ !=
nullptr) {
1869 CHECK_GT(new_size, 0);
1870 drat_proof_handler_->AddClause({clause->begin(), new_size});
1871 drat_proof_handler_->DeleteClause({clause->begin(), old_size});
1874 if (new_size == 2) {
1878 AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
1879 clauses_propagator_->LazyDetach(clause);
1889 DCHECK_EQ(trail_->Index(), saved_index);
1895 clauses_propagator_->CleanUpWatchers();
1896 if (num_detached_clauses > 0 || num_binary > 0) {
1897 VLOG(1) << trail_->Index() <<
" fixed variables at level 0. " <<
"Detached "
1898 << num_detached_clauses <<
" clauses. " << num_binary
1899 <<
" converted to binary.";
1906 CHECK(binary_implication_graph_->Propagate(trail_));
1907 binary_implication_graph_->RemoveFixedVariables();
1908 num_processed_fixed_variables_ = trail_->Index();
1912bool SatSolver::PropagationIsDone()
const {
1914 if (propagator->IsEmpty())
continue;
1915 if (!propagator->PropagationIsDone(*trail_))
return false;
1932 non_empty_propagators_.clear();
1934 if (!propagator->IsEmpty()) {
1935 non_empty_propagators_.push_back(propagator);
1947 const int old_index = trail_->Index();
1949 DCHECK(propagator->PropagatePreconditionsAreSatisfied(*trail_));
1950 if (!propagator->Propagate(trail_))
return false;
1951 if (trail_->Index() > old_index)
break;
1953 if (trail_->Index() == old_index)
break;
1959 if (PropagationIsDone())
return true;
1964void SatSolver::InitializePropagators() {
1965 propagators_.clear();
1966 propagators_.push_back(binary_implication_graph_);
1967 propagators_.push_back(clauses_propagator_);
1968 propagators_.push_back(pb_constraints_);
1969 for (
int i = 0;
i < external_propagators_.size(); ++
i) {
1970 propagators_.push_back(external_propagators_[
i]);
1972 if (last_propagator_ !=
nullptr) {
1973 propagators_.push_back(last_propagator_);
1977bool SatSolver::ResolvePBConflict(BooleanVariable var,
1979 Coefficient* slack) {
1980 const int trail_index = trail_->Info(var).trail_index;
1983 DCHECK_EQ(*slack, conflict->ComputeSlackForTrailPrefix(*trail_, trail_index));
1986 UpperBoundedLinearConstraint* pb_reason = ReasonPbConstraintOrNull(var);
1987 if (pb_reason !=
nullptr) {
1988 pb_reason->ResolvePBConflict(*trail_, var, conflict, slack);
1993 Coefficient multiplier(1);
1996 const int algorithm = 1;
1997 switch (algorithm) {
2001 conflict->ReduceSlackTo(*trail_, trail_index, *slack, Coefficient(0));
2005 multiplier = *slack + 1;
2009 multiplier = conflict->GetCoefficient(var);
2012 Coefficient num_literals(1);
2014 trail_->Assignment().GetTrueLiteralForAssignedVariable(var).Negated(),
2016 for (Literal literal : trail_->Reason(var)) {
2017 DCHECK_NE(literal.Variable(), var);
2018 DCHECK(
Assignment().LiteralIsFalse(literal));
2019 conflict->AddTerm(literal.Negated(), multiplier);
2022 conflict->AddToRhs((num_literals - 1) * multiplier);
2026 DCHECK_EQ(*slack, conflict->ComputeSlackForTrailPrefix(*trail_, trail_index));
2030void SatSolver::EnqueueNewDecision(
Literal literal) {
2032 CHECK(!
Assignment().VariableIsAssigned(literal.Variable()));
2041 const double kMinDeterministicTimeBetweenCleanups = 1.0;
2042 if (num_processed_fixed_variables_ < trail_->
Index() &&
2044 deterministic_time_of_last_fixed_variables_cleanup_ +
2045 kMinDeterministicTimeBetweenCleanups) {
2050 counters_.num_branches++;
2051 last_decision_or_backtrack_trail_index_ = trail_->Index();
2052 decisions_[current_decision_level_] =
Decision(trail_->Index(), literal);
2053 ++current_decision_level_;
2054 trail_->SetDecisionLevel(current_decision_level_);
2055 trail_->EnqueueSearchDecision(literal);
2058std::string SatSolver::DebugString(
const SatClause& clause)
const {
2060 for (
const Literal literal : clause) {
2061 if (!result.empty()) {
2062 result.append(
" || ");
2064 const std::string value =
2065 trail_->Assignment().LiteralIsTrue(literal)
2067 : (trail_->Assignment().LiteralIsFalse(literal) ?
"false"
2069 result.append(absl::StrFormat(
"%s(%s)", literal.DebugString(), value));
2074int SatSolver::ComputeMaxTrailIndex(absl::Span<const Literal> clause)
const {
2076 int trail_index = -1;
2077 for (
const Literal literal : clause) {
2079 std::max(trail_index, trail_->Info(literal.Variable()).trail_index);
2087void SatSolver::ComputeFirstUIPConflict(
2088 int max_trail_index, std::vector<Literal>* conflict,
2089 std::vector<Literal>* reason_used_to_infer_the_conflict,
2090 std::vector<SatClause*>* subsumed_clauses) {
2092 const int64_t conflict_id = counters_.num_failures;
2096 is_marked_.ClearAndResize(num_variables_);
2099 reason_used_to_infer_the_conflict->clear();
2100 subsumed_clauses->clear();
2101 if (max_trail_index == -1)
return;
2106 DCHECK_EQ(max_trail_index, ComputeMaxTrailIndex(trail_->FailingClause()));
2107 int trail_index = max_trail_index;
2108 const int highest_level = DecisionLevel((*trail_)[trail_index].Variable());
2109 if (highest_level == 0)
return;
2126 absl::Span<const Literal> clause_to_expand = trail_->FailingClause();
2127 SatClause* sat_clause = trail_->FailingSatClause();
2128 DCHECK(!clause_to_expand.empty());
2129 int num_literal_at_highest_level_that_needs_to_be_processed = 0;
2131 int num_new_vars_at_positive_level = 0;
2132 int num_vars_at_positive_level_in_clause_to_expand = 0;
2133 for (
const Literal literal : clause_to_expand) {
2134 const BooleanVariable var = literal.Variable();
2135 const int level = DecisionLevel(var);
2136 if (level == 0)
continue;
2137 ++num_vars_at_positive_level_in_clause_to_expand;
2138 if (!is_marked_[var]) {
2139 is_marked_.Set(var);
2140 ++num_new_vars_at_positive_level;
2141 if (level == highest_level) {
2142 ++num_literal_at_highest_level_that_needs_to_be_processed;
2146 DCHECK(trail_->Assignment().LiteralIsFalse(literal));
2147 conflict->push_back(literal);
2154 if (num_new_vars_at_positive_level > 0) {
2157 subsumed_clauses->clear();
2164 if (sat_clause !=
nullptr &&
2165 num_vars_at_positive_level_in_clause_to_expand ==
2167 num_literal_at_highest_level_that_needs_to_be_processed) {
2168 subsumed_clauses->push_back(sat_clause);
2172 DCHECK_GT(num_literal_at_highest_level_that_needs_to_be_processed, 0);
2173 while (!is_marked_[(*trail_)[trail_index].Variable()]) {
2175 DCHECK_GE(trail_index, 0);
2176 DCHECK_EQ(DecisionLevel((*trail_)[trail_index].Variable()),
2180 if (num_literal_at_highest_level_that_needs_to_be_processed == 1) {
2184 conflict->push_back((*trail_)[trail_index].Negated());
2187 std::swap(conflict->back(), conflict->front());
2191 const Literal literal = (*trail_)[trail_index];
2192 reason_used_to_infer_the_conflict->push_back(literal);
2196 if (same_reason_identifier_.FirstVariableWithSameReason(
2197 literal.Variable()) != literal.Variable()) {
2198 clause_to_expand = {};
2200 clause_to_expand = trail_->Reason(literal.Variable(), conflict_id);
2202 sat_clause = ReasonClauseOrNull(literal.Variable());
2204 --num_literal_at_highest_level_that_needs_to_be_processed;
2209void SatSolver::ComputeUnionOfReasons(absl::Span<const Literal>
input,
2210 std::vector<Literal>* literals) {
2211 tmp_mark_.ClearAndResize(num_variables_);
2213 for (
const Literal l :
input) tmp_mark_.Set(l.Variable());
2214 for (
const Literal l :
input) {
2215 for (
const Literal r : trail_->Reason(l.Variable())) {
2216 if (!tmp_mark_[r.Variable()]) {
2217 tmp_mark_.Set(r.Variable());
2218 literals->push_back(r);
2222 for (
const Literal l :
input) tmp_mark_.Clear(l.Variable());
2223 for (
const Literal l : *literals) tmp_mark_.Clear(l.Variable());
2227void SatSolver::ComputePBConflict(
int max_trail_index,
2228 Coefficient initial_slack,
2230 int* pb_backjump_level) {
2232 int trail_index = max_trail_index;
2236 Coefficient slack = initial_slack;
2238 conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1));
2239 CHECK_LT(slack, 0) <<
"We don't have a conflict!";
2242 int backjump_level = 0;
2244 const BooleanVariable var = (*trail_)[trail_index].Variable();
2247 if (conflict->GetCoefficient(var) > 0 &&
2248 trail_->Assignment().LiteralIsTrue(conflict->GetLiteral(var))) {
2249 if (parameters_->minimize_reduction_during_pb_resolution()) {
2254 conflict->ReduceGivenCoefficient(var);
2258 slack += conflict->GetCoefficient(var);
2262 if (slack < 0)
continue;
2268 const int current_level = DecisionLevel(var);
2269 int i = trail_index;
2271 const BooleanVariable previous_var = (*trail_)[
i].Variable();
2272 if (conflict->GetCoefficient(previous_var) > 0 &&
2273 trail_->Assignment().LiteralIsTrue(
2274 conflict->GetLiteral(previous_var))) {
2279 if (
i < 0 || DecisionLevel((*trail_)[
i].Variable()) < current_level) {
2280 backjump_level =
i < 0 ? 0 : DecisionLevel((*trail_)[
i].Variable());
2286 const bool clause_used = ResolvePBConflict(var, conflict, &slack);
2295 const Coefficient slack_only_for_debug =
2297 ? conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1)
2302 if (!parameters_->minimize_reduction_during_pb_resolution()) {
2303 conflict->ReduceCoefficients();
2309 if (parameters_->minimize_reduction_during_pb_resolution()) {
2311 conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1);
2313 slack = conflict->ReduceCoefficientsAndComputeSlackForTrailPrefix(
2314 *trail_, trail_index + 1);
2317 DCHECK_EQ(slack, slack_only_for_debug);
2319 if (conflict->Rhs() < 0) {
2320 *pb_backjump_level = -1;
2328 if (!parameters_->minimize_reduction_during_pb_resolution()) {
2329 conflict->ReduceCoefficients();
2334 std::vector<Coefficient> sum_for_le_level(backjump_level + 2, Coefficient(0));
2335 std::vector<Coefficient> max_coeff_for_ge_level(backjump_level + 2,
2338 Coefficient max_sum(0);
2339 for (BooleanVariable var : conflict->PossibleNonZeros()) {
2340 const Coefficient coeff = conflict->GetCoefficient(var);
2341 if (coeff == 0)
continue;
2344 if (!trail_->Assignment().VariableIsAssigned(var) ||
2345 DecisionLevel(var) > backjump_level) {
2346 max_coeff_for_ge_level[backjump_level + 1] =
2347 std::max(max_coeff_for_ge_level[backjump_level + 1], coeff);
2349 const int level = DecisionLevel(var);
2350 if (trail_->Assignment().LiteralIsTrue(conflict->GetLiteral(var))) {
2351 sum_for_le_level[level] += coeff;
2353 max_coeff_for_ge_level[level] =
2354 std::max(max_coeff_for_ge_level[level], coeff);
2359 for (
int i = 1;
i < sum_for_le_level.size(); ++
i) {
2360 sum_for_le_level[
i] += sum_for_le_level[
i - 1];
2362 for (
int i = max_coeff_for_ge_level.size() - 2;
i >= 0; --
i) {
2363 max_coeff_for_ge_level[
i] =
2364 std::max(max_coeff_for_ge_level[
i], max_coeff_for_ge_level[
i + 1]);
2369 if (sum_for_le_level[0] > conflict->Rhs()) {
2370 *pb_backjump_level = -1;
2373 for (
int i = 0;
i <= backjump_level; ++
i) {
2374 const Coefficient level_sum = sum_for_le_level[
i];
2375 CHECK_LE(level_sum, conflict->Rhs());
2376 if (conflict->Rhs() - level_sum < max_coeff_for_ge_level[
i + 1]) {
2377 *pb_backjump_level =
i;
2381 LOG(FATAL) <<
"The code should never reach here.";
2384void SatSolver::MinimizeConflict(std::vector<Literal>* conflict) {
2387 const int old_size = conflict->size();
2388 switch (parameters_->minimization_algorithm()) {
2389 case SatParameters::NONE:
2391 case SatParameters::SIMPLE: {
2392 MinimizeConflictSimple(conflict);
2395 case SatParameters::RECURSIVE: {
2396 MinimizeConflictRecursively(conflict);
2399 case SatParameters::EXPERIMENTAL: {
2400 MinimizeConflictExperimental(conflict);
2404 if (conflict->size() < old_size) {
2405 ++counters_.num_minimizations;
2406 counters_.num_literals_removed += old_size - conflict->size();
2417void SatSolver::MinimizeConflictSimple(std::vector<Literal>* conflict) {
2424 for (
int i = 1;
i < conflict->size(); ++
i) {
2425 const BooleanVariable var = (*conflict)[
i].Variable();
2426 bool can_be_removed =
false;
2427 if (DecisionLevel(var) != current_level) {
2429 const absl::Span<const Literal> reason = trail_->Reason(var);
2430 if (!reason.empty()) {
2431 can_be_removed =
true;
2432 for (Literal literal : reason) {
2433 if (DecisionLevel(literal.Variable()) == 0)
continue;
2434 if (!is_marked_[literal.Variable()]) {
2435 can_be_removed =
false;
2441 if (!can_be_removed) {
2442 (*conflict)[index] = (*conflict)[
i];
2446 conflict->erase(conflict->begin() + index, conflict->end());
2455void SatSolver::MinimizeConflictRecursively(std::vector<Literal>* conflict) {
2468 is_independent_.ClearAndResize(num_variables_);
2476 std::numeric_limits<int>::max());
2488 for (BooleanVariable var : is_marked_.PositionsSetAtLeastOnce()) {
2489 const int level = DecisionLevel(var);
2490 min_trail_index_per_level_[level] = std::min(
2491 min_trail_index_per_level_[level], trail_->Info(var).trail_index);
2498 TimeLimitCheckEveryNCalls time_limit_check(100, time_limit_);
2499 for (
int i = 1;
i < conflict->size(); ++
i) {
2500 const BooleanVariable var = (*conflict)[
i].Variable();
2501 const AssignmentInfo& info = trail_->Info(var);
2502 if (time_limit_check.LimitReached() ||
2504 info.trail_index <= min_trail_index_per_level_[info.level] ||
2505 !CanBeInferedFromConflictVariables(var)) {
2508 is_independent_.Set(var);
2509 (*conflict)[index] = (*conflict)[
i];
2513 conflict->resize(index);
2517 const int threshold = min_trail_index_per_level_.size() / 2;
2518 if (is_marked_.PositionsSetAtLeastOnce().size() < threshold) {
2519 for (BooleanVariable var : is_marked_.PositionsSetAtLeastOnce()) {
2520 min_trail_index_per_level_[DecisionLevel(var)] =
2521 std::numeric_limits<int>::max();
2524 min_trail_index_per_level_.clear();
2528bool SatSolver::CanBeInferedFromConflictVariables(BooleanVariable variable) {
2531 DCHECK(is_marked_[variable]);
2532 const BooleanVariable v =
2533 same_reason_identifier_.FirstVariableWithSameReason(variable);
2534 if (v != variable)
return !is_independent_[v];
2547 dfs_stack_.push_back(variable);
2548 variable_to_process_.clear();
2549 variable_to_process_.push_back(variable);
2552 for (
const Literal literal : trail_->Reason(variable)) {
2553 const BooleanVariable var = literal.Variable();
2554 DCHECK_NE(var, variable);
2555 if (is_marked_[var])
continue;
2556 const AssignmentInfo& info = trail_->Info(var);
2557 if (info.level == 0) {
2562 is_marked_.Set(var);
2565 if (info.trail_index <= min_trail_index_per_level_[info.level] ||
2569 variable_to_process_.push_back(var);
2573 while (!variable_to_process_.empty()) {
2574 const BooleanVariable current_var = variable_to_process_.back();
2575 if (current_var == dfs_stack_.back()) {
2578 if (dfs_stack_.size() > 1) {
2579 DCHECK(!is_marked_[current_var]);
2580 is_marked_.Set(current_var);
2582 variable_to_process_.pop_back();
2583 dfs_stack_.pop_back();
2588 if (is_marked_[current_var]) {
2589 variable_to_process_.pop_back();
2595 DCHECK(!is_independent_[current_var]);
2599 const BooleanVariable v =
2600 same_reason_identifier_.FirstVariableWithSameReason(current_var);
2601 if (v != current_var) {
2602 if (is_independent_[v])
break;
2603 DCHECK(is_marked_[v]);
2604 variable_to_process_.pop_back();
2610 dfs_stack_.push_back(current_var);
2611 bool abort_early =
false;
2612 for (Literal literal : trail_->Reason(current_var)) {
2613 const BooleanVariable var = literal.Variable();
2614 DCHECK_NE(var, current_var);
2615 const AssignmentInfo& info = trail_->Info(var);
2616 if (info.level == 0 || is_marked_[var])
continue;
2617 if (info.trail_index <= min_trail_index_per_level_[info.level] ||
2619 is_independent_[var]) {
2623 variable_to_process_.push_back(var);
2625 if (abort_early)
break;
2629 for (
const BooleanVariable var : dfs_stack_) {
2630 is_independent_.Set(var);
2632 return dfs_stack_.empty();
2637struct WeightedVariable {
2638 WeightedVariable(BooleanVariable v,
int w) : var(v), weight(
w) {}
2640 BooleanVariable var;
2646struct VariableWithLargerWeightFirst {
2647 bool operator()(
const WeightedVariable& wv1,
2648 const WeightedVariable& wv2)
const {
2649 return (wv1.weight > wv2.weight ||
2650 (wv1.weight == wv2.weight && wv1.var < wv2.var));
2666void SatSolver::MinimizeConflictExperimental(std::vector<Literal>* conflict) {
2671 is_marked_.ClearAndResize(num_variables_);
2673 std::vector<WeightedVariable> variables_sorted_by_level;
2674 for (Literal literal : *conflict) {
2675 const BooleanVariable var = literal.Variable();
2676 is_marked_.Set(var);
2677 const int level = DecisionLevel(var);
2678 if (level < current_level) {
2679 variables_sorted_by_level.push_back(WeightedVariable(var, level));
2682 std::sort(variables_sorted_by_level.begin(), variables_sorted_by_level.end(),
2683 VariableWithLargerWeightFirst());
2686 std::vector<BooleanVariable> to_remove;
2687 for (WeightedVariable weighted_var : variables_sorted_by_level) {
2688 const BooleanVariable var = weighted_var.var;
2692 const absl::Span<const Literal> reason = trail_->Reason(var);
2693 if (reason.empty())
continue;
2697 std::vector<Literal> not_contained_literals;
2698 for (
const Literal reason_literal : reason) {
2699 const BooleanVariable reason_var = reason_literal.Variable();
2702 if (DecisionLevel(reason_var) == 0)
continue;
2707 if (!is_marked_[reason_var]) {
2708 not_contained_literals.push_back(reason_literal);
2709 if (not_contained_literals.size() > 1)
break;
2712 if (not_contained_literals.empty()) {
2717 to_remove.push_back(var);
2718 }
else if (not_contained_literals.size() == 1) {
2721 to_remove.push_back(var);
2722 is_marked_.Set(not_contained_literals.front().Variable());
2723 conflict->push_back(not_contained_literals.front());
2728 for (BooleanVariable var : to_remove) {
2729 is_marked_.Clear(var);
2734 for (
int i = 0;
i < conflict->size(); ++
i) {
2735 const Literal literal = (*conflict)[
i];
2736 if (is_marked_[literal.Variable()]) {
2737 (*conflict)[index] = literal;
2741 conflict->erase(conflict->begin() + index, conflict->end());
2744void SatSolver::CleanClauseDatabaseIfNeeded() {
2745 if (num_learned_clause_before_cleanup_ > 0)
return;
2750 typedef std::pair<SatClause*, ClauseInfo> Entry;
2751 std::vector<Entry> entries;
2752 auto& clauses_info = *(clauses_propagator_->mutable_clauses_info());
2753 for (
auto& entry : clauses_info) {
2754 if (ClauseIsUsedAsReason(entry.first))
continue;
2755 if (entry.second.protected_during_next_cleanup) {
2756 entry.second.protected_during_next_cleanup =
false;
2759 entries.push_back(entry);
2761 const int num_protected_clauses = clauses_info.size() - entries.size();
2763 if (parameters_->clause_cleanup_ordering() == SatParameters::CLAUSE_LBD) {
2765 std::sort(entries.begin(), entries.end(),
2766 [](
const Entry& a,
const Entry&
b) {
2767 if (a.second.lbd == b.second.lbd) {
2768 return a.second.activity < b.second.activity;
2770 return a.second.lbd >
b.second.lbd;
2774 std::sort(entries.begin(), entries.end(),
2775 [](
const Entry& a,
const Entry&
b) {
2776 if (a.second.activity == b.second.activity) {
2777 return a.second.lbd > b.second.lbd;
2779 return a.second.activity <
b.second.activity;
2784 int num_kept_clauses =
2785 (parameters_->clause_cleanup_target() > 0)
2786 ? std::min(
static_cast<int>(entries.size()),
2787 parameters_->clause_cleanup_target())
2788 : static_cast<int>(parameters_->clause_cleanup_ratio() *
2789 static_cast<double>(entries.size()));
2791 int num_deleted_clauses = entries.size() - num_kept_clauses;
2796 if (num_kept_clauses > 0) {
2797 while (num_deleted_clauses > 0) {
2798 const ClauseInfo& a = entries[num_deleted_clauses].second;
2799 const ClauseInfo&
b = entries[num_deleted_clauses - 1].second;
2800 if (a.activity !=
b.activity || a.lbd !=
b.lbd)
break;
2801 --num_deleted_clauses;
2805 if (num_deleted_clauses > 0) {
2806 entries.resize(num_deleted_clauses);
2807 for (
const Entry& entry : entries) {
2808 SatClause* clause = entry.first;
2809 counters_.num_literals_forgotten += clause->size();
2810 clauses_propagator_->LazyDetach(clause);
2812 clauses_propagator_->CleanUpWatchers();
2816 if (!block_clause_deletion_) {
2817 clauses_propagator_->DeleteRemovedClauses();
2821 num_learned_clause_before_cleanup_ = parameters_->clause_cleanup_period();
2822 VLOG(1) <<
"Database cleanup, #protected:" << num_protected_clauses
2823 <<
" #kept:" << num_kept_clauses
2824 <<
" #deleted:" << num_deleted_clauses;
2830 return "ASSUMPTIONS_UNSAT";
2832 return "INFEASIBLE";
2836 return "LIMIT_REACHED";
2840 LOG(DFATAL) <<
"Invalid SatSolver::Status " << status;
2845 std::vector<Literal> result;
2847 for (
const Literal lit : *core) {
2849 result.push_back(lit);
2853 if (result.size() < core->size()) {
2854 VLOG(1) <<
"minimization " << core->size() <<
" -> " << result.size();
bool AddBinaryClause(Literal a, Literal b)
SatClause * ReasonClause(int trail_index) const
absl::flat_hash_map< SatClause *, ClauseInfo > * mutable_clauses_info()
void AddClause(absl::Span< const Literal > clause)
BooleanVariable Variable() const
UpperBoundedLinearConstraint * ReasonPbConstraint(int trail_index) const
void BumpActivity(UpperBoundedLinearConstraint *constraint)
Contain the logic to decide when to restart a SAT tree search.
Base class for all the SAT constraints.
Status EnqueueDecisionAndBacktrackOnConflict(Literal true_literal, int *first_propagation_index=nullptr)
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
void LoadDebugSolution(absl::Span< const Literal > solution)
Status SolveWithTimeLimit(TimeLimit *time_limit)
double deterministic_time() const
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
bool MinimizeByPropagation(double dtime, bool minimize_new_clauses_only=false)
void ProcessCurrentConflict()
Status UnsatStatus() const
bool AddBinaryClauses(absl::Span< const BinaryClause > clauses)
void ProcessNewlyFixedVariables()
Simplifies the problem when new variables are assigned at level 0.
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
int64_t num_branches() const
Some statistics since the creation of the solver.
bool AddProblemClause(absl::Span< const Literal > literals)
std::vector< Literal > GetLastIncompatibleDecisions()
bool RestoreSolverToAssumptionLevel()
bool AddBinaryClause(Literal a, Literal b)
Same as AddProblemClause() below, but for small clauses.
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
int64_t num_failures() const
bool ModelIsUnsat() const
void Backtrack(int target_level)
bool ReapplyAssumptionsIfNeeded()
void ClearNewlyAddedBinaryClauses()
int64_t num_propagations() const
int64_t num_backtracks() const
const SatParameters & parameters() const
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
ABSL_MUST_USE_RESULT bool Propagate()
std::vector< Literal > GetDecisionsFixing(absl::Span< const Literal > literals)
void SetAssumptionLevel(int assumption_level)
int64_t num_restarts() const
ABSL_MUST_USE_RESULT bool AddUnitClause(Literal true_literal)
bool AddTernaryClause(Literal a, Literal b, Literal c)
void AdvanceDeterministicTime(TimeLimit *limit)
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions, int64_t max_number_of_conflicts=-1)
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
ABSL_MUST_USE_RESULT bool ResetToLevelZero()
void SaveDebugAssignment()
void AddLastPropagator(SatPropagator *propagator)
const std::vector< Decision > & Decisions() const
ABSL_MUST_USE_RESULT bool FinishPropagation()
const Trail & LiteralTrail() const
void SetNumVariables(int num_variables)
void AddPropagator(SatPropagator *propagator)
void SetParameters(const SatParameters ¶meters)
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const
std::vector< Literal > * MutableConflict()
int AssignmentType(BooleanVariable var) const
absl::Span< const Literal > Reason(BooleanVariable var, int64_t conflict_id=-1) const
void EnqueueWithUnitReason(Literal true_literal)
Specific Enqueue() version for a fixed variable.
const AssignmentInfo & Info(BooleanVariable var) const
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 STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
std::string SatStatusString(SatSolver::Status status)
Returns a string representation of a SatSolver::Status.
Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound, Coefficient bound_shift, Coefficient max_value)
bool BooleanLinearExpressionIsCanonical(absl::Span< const LiteralWithCoeff > cst)
Returns true iff the Boolean linear expression is in canonical form.
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
int MoveOneUnprocessedLiteralLast(const absl::btree_set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
int64_t MemoryUsageProcess()
In SWIG mode, we don't want anything besides these top-level includes.
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
std::string ProtobufShortDebugString(const P &message)
std::string MemoryUsage()
Returns the current thread's total memory usage in an human-readable string.
bool SafeAddInto(IntegerType a, IntegerType *b)
trees with all degrees equal w the current value of w
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)
Information about a variable assignment.
int32_t trail_index
The index of this assignment in the trail.
static constexpr int kSearchDecision
A binary clause. This is used by BinaryClauseManager.
Represents a term in a pseudo-Boolean formula.
#define SOLVER_LOG(logger,...)