24#include "absl/strings/str_format.h"
38 owned_model_.reset(model_);
47 track_binary_clauses_(false),
50 parameters_(
model->GetOrCreate<SatParameters>()),
53 clause_activity_increment_(1.0),
54 same_reason_identifier_(*trail_),
55 is_relevant_for_core_computation_(true),
56 problem_is_pure_sat_(true),
57 drat_proof_handler_(nullptr),
59 InitializePropagators();
66 CHECK_GE(num_variables, num_variables_);
68 num_variables_ = num_variables;
69 binary_implication_graph_->
Resize(num_variables);
70 clauses_propagator_->
Resize(num_variables);
71 trail_->
Resize(num_variables);
73 pb_constraints_->
Resize(num_variables);
74 same_reason_identifier_.
Resize(num_variables);
79 decisions_.resize(num_variables + 1);
122bool SatSolver::IsMemoryLimitReached()
const {
123 const int64 memory_usage =
125 const int64 kMegaByte = 1024 * 1024;
126 return memory_usage > kMegaByte * parameters_->max_memory_in_mb();
129bool SatSolver::SetModelUnsat() {
130 model_is_unsat_ =
true;
135 if (model_is_unsat_)
return false;
137 if (literals.empty())
return SetModelUnsat();
139 if (literals.size() == 2) {
144 return SetModelUnsat();
148 InitializePropagators();
151 if (!clauses_propagator_->
AddClause(literals)) {
153 return SetModelUnsat();
167 if (model_is_unsat_)
return false;
170 if (drat_proof_handler_ !=
nullptr) {
173 drat_proof_handler_->
AddClause({true_literal});
176 if (!
Propagate())
return SetModelUnsat();
182 tmp_pb_constraint_.clear();
186 true, Coefficient(1),
187 false, Coefficient(0),
188 &tmp_pb_constraint_);
193 tmp_pb_constraint_.clear();
198 true, Coefficient(1),
199 false, Coefficient(0),
200 &tmp_pb_constraint_);
209 tmp_pb_constraint_.clear();
214 true, Coefficient(1),
215 false, Coefficient(0),
216 &tmp_pb_constraint_);
219bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
227 if (literals.size() == 1) {
234 if (parameters_->treat_binary_clauses_separately() && literals.size() == 2) {
235 AddBinaryClauseInternal(literals[0], literals[1]);
237 if (!clauses_propagator_->
AddClause(literals, trail_)) {
238 return SetModelUnsat();
244bool SatSolver::AddLinearConstraintInternal(
245 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
246 Coefficient max_value) {
249 if (rhs < 0)
return SetModelUnsat();
250 if (rhs >= max_value)
return true;
257 const Coefficient min_coeff = cst.front().coefficient;
258 const Coefficient max_coeff = cst.back().coefficient;
262 if (max_value - min_coeff <= rhs) {
264 literals_scratchpad_.clear();
265 for (
const LiteralWithCoeff& term : cst) {
266 literals_scratchpad_.push_back(term.literal.Negated());
268 return AddProblemClauseInternal(literals_scratchpad_);
273 if (parameters_->treat_binary_clauses_separately() &&
274 !parameters_->use_pb_resolution() && max_coeff <= rhs &&
275 2 * min_coeff > rhs) {
276 literals_scratchpad_.clear();
277 for (
const LiteralWithCoeff& term : cst) {
278 literals_scratchpad_.push_back(term.literal);
280 if (!binary_implication_graph_->
AddAtMostOne(literals_scratchpad_)) {
281 return SetModelUnsat();
286 InitializePropagators();
290 problem_is_pure_sat_ =
false;
294 const bool result = pb_constraints_->
AddConstraint(cst, rhs, trail_);
295 InitializePropagators();
300 Coefficient lower_bound,
301 bool use_upper_bound,
302 Coefficient upper_bound,
303 std::vector<LiteralWithCoeff>* cst) {
306 if (model_is_unsat_)
return false;
309 Coefficient fixed_variable_shift(0);
318 (*cst)[
index] = term;
326 Coefficient bound_shift;
327 Coefficient max_value;
332 if (use_upper_bound) {
333 const Coefficient rhs =
335 if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
336 return SetModelUnsat();
339 if (use_lower_bound) {
341 for (
int i = 0; i < cst->size(); ++i) {
342 (*cst)[i].literal = (*cst)[i].literal.Negated();
344 const Coefficient rhs =
346 if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
347 return SetModelUnsat();
355 if (!PropagationIsDone() && !
Propagate()) {
356 return SetModelUnsat();
361int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
362 const std::vector<Literal>& literals,
bool is_redundant) {
365 if (literals.size() == 1) {
373 if (literals.size() == 2 && parameters_->treat_binary_clauses_separately()) {
374 if (track_binary_clauses_) {
375 CHECK(binary_clauses_.
Add(BinaryClause(literals[0], literals[1])));
380 InitializePropagators();
384 CleanClauseDatabaseIfNeeded();
388 const int lbd = ComputeLbd(literals);
389 if (is_redundant && lbd > parameters_->clause_cleanup_lbd_bound()) {
390 --num_learned_clause_before_cleanup_;
398 BumpClauseActivity(clause);
407 problem_is_pure_sat_ =
false;
409 external_propagators_.push_back(propagator);
410 InitializePropagators();
415 CHECK(last_propagator_ ==
nullptr);
416 problem_is_pure_sat_ =
false;
418 last_propagator_ = propagator;
419 InitializePropagators();
423 BooleanVariable
var)
const {
433SatClause* SatSolver::ReasonClauseOrNull(BooleanVariable
var)
const {
435 const AssignmentInfo& info = trail_->
Info(
var);
437 return clauses_propagator_->
ReasonClause(info.trail_index);
443 debug_assignment_.
Resize(num_variables_.value());
444 for (BooleanVariable i(0); i < num_variables_; ++i) {
455 InitializePropagators();
459bool SatSolver::ClauseIsValidUnderDebugAssignement(
460 const std::vector<Literal>& clause)
const {
461 for (Literal l : clause) {
470bool SatSolver::PBConstraintIsValidUnderDebugAssignment(
471 const std::vector<LiteralWithCoeff>& cst,
const Coefficient rhs)
const {
472 Coefficient sum(0.0);
473 for (LiteralWithCoeff term : cst) {
478 sum += term.coefficient;
488bool ClauseSubsumption(
const std::vector<Literal>&
a, SatClause*
b) {
489 std::vector<Literal> superset(
b->begin(),
b->end());
490 std::vector<Literal> subset(
a.begin(),
a.end());
491 std::sort(superset.begin(), superset.end());
492 std::sort(subset.begin(), subset.end());
493 return std::includes(superset.begin(), superset.end(), subset.begin(),
502 CHECK(PropagationIsDone());
503 EnqueueNewDecision(true_literal);
504 while (!PropagateAndStopAfterOneConflictResolution()) {
507 CHECK(PropagationIsDone());
508 return last_decision_or_backtrack_trail_index_;
512 if (model_is_unsat_)
return false;
522 if (model_is_unsat_)
return false;
523 while (!PropagateAndStopAfterOneConflictResolution()) {
524 if (model_is_unsat_)
return false;
530 if (model_is_unsat_)
return false;
531 assumption_level_ = 0;
537 const std::vector<Literal>& assumptions) {
546 std::min<int>(assumptions.size(), num_variables_.value() + 1);
547 for (
int i = 0; i < assumption_level_; ++i) {
548 decisions_[i].literal = assumptions[i];
555 if (model_is_unsat_)
return false;
559 const int64 old_num_branches = counters_.num_branches;
561 ReapplyDecisionsUpTo(assumption_level_ - 1, &unused);
562 counters_.num_branches = old_num_branches;
567bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
571 ++counters_.num_failures;
572 const int conflict_trail_index = trail_->
Index();
573 const int conflict_decision_level = current_decision_level_;
576 same_reason_identifier_.
Clear();
577 const int max_trail_index = ComputeMaxTrailIndex(trail_->
FailingClause());
578 ComputeFirstUIPConflict(max_trail_index, &learned_conflict_,
579 &reason_used_to_infer_the_conflict_,
583 if (learned_conflict_.empty())
return SetModelUnsat();
584 DCHECK(IsConflictValid(learned_conflict_));
585 DCHECK(ClauseIsValidUnderDebugAssignement(learned_conflict_));
593 if (parameters_->also_bump_variables_in_conflict_reasons()) {
594 ComputeUnionOfReasons(learned_conflict_, &extra_reason_literals_);
604 BumpReasonActivities(reason_used_to_infer_the_conflict_);
608 UpdateClauseActivityIncrement();
612 const int period = parameters_->glucose_decay_increment_period();
613 const double max_decay = parameters_->glucose_max_decay();
614 if (counters_.num_failures % period == 0 &&
615 parameters_->variable_activity_decay() < max_decay) {
616 parameters_->set_variable_activity_decay(
617 parameters_->variable_activity_decay() +
618 parameters_->glucose_decay_increment());
624 bool compute_pb_conflict =
false;
625 if (parameters_->use_pb_resolution()) {
627 if (!compute_pb_conflict) {
628 for (Literal lit : reason_used_to_infer_the_conflict_) {
629 if (ReasonPbConstraintOrNull(lit.Variable()) !=
nullptr) {
630 compute_pb_conflict =
true;
639 if (compute_pb_conflict) {
641 Coefficient initial_slack(-1);
644 Coefficient num_literals(0);
649 pb_conflict_.
AddToRhs(num_literals - 1);
658 int pb_backjump_level;
659 ComputePBConflict(max_trail_index, initial_slack, &pb_conflict_,
661 if (pb_backjump_level == -1)
return SetModelUnsat();
664 std::vector<LiteralWithCoeff> cst;
666 DCHECK(PBConstraintIsValidUnderDebugAssignment(cst, pb_conflict_.
Rhs()));
670 bool conflict_is_a_clause = (pb_conflict_.
Rhs() == cst.size() - 1);
671 if (conflict_is_a_clause) {
672 for (LiteralWithCoeff term : cst) {
673 if (term.coefficient != Coefficient(1)) {
674 conflict_is_a_clause =
false;
680 if (!conflict_is_a_clause) {
689 CHECK_GT(trail_->
Index(), last_decision_or_backtrack_trail_index_);
690 counters_.num_learned_pb_literals += cst.size();
696 if (pb_backjump_level < ComputeBacktrackLevel(learned_conflict_)) {
697 subsumed_clauses_.clear();
698 learned_conflict_.clear();
702 for (LiteralWithCoeff term : cst) {
705 const int level = trail_->
Info(term.literal.Variable()).
level;
706 if (level == 0)
continue;
707 if (level > max_level) {
709 max_index = learned_conflict_.size();
711 learned_conflict_.push_back(term.literal.Negated());
715 is_marked_.
Set(term.literal.Variable());
717 CHECK(!learned_conflict_.empty());
718 std::swap(learned_conflict_.front(), learned_conflict_[max_index]);
719 DCHECK(IsConflictValid(learned_conflict_));
728 DCHECK(ClauseIsValidUnderDebugAssignement(learned_conflict_));
729 if (!binary_implication_graph_->
IsEmpty()) {
730 if (parameters_->binary_minimization_algorithm() ==
731 SatParameters::BINARY_MINIMIZATION_FIRST) {
733 *trail_, &learned_conflict_, &is_marked_);
734 }
else if (parameters_->binary_minimization_algorithm() ==
736 BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION) {
738 *trail_, &learned_conflict_, &is_marked_,
741 DCHECK(IsConflictValid(learned_conflict_));
745 MinimizeConflict(&learned_conflict_, &reason_used_to_infer_the_conflict_);
748 if (!binary_implication_graph_->
IsEmpty()) {
752 switch (parameters_->binary_minimization_algorithm()) {
753 case SatParameters::NO_BINARY_MINIMIZATION:
754 ABSL_FALLTHROUGH_INTENDED;
755 case SatParameters::BINARY_MINIMIZATION_FIRST:
756 ABSL_FALLTHROUGH_INTENDED;
757 case SatParameters::BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION:
759 case SatParameters::BINARY_MINIMIZATION_WITH_REACHABILITY:
763 case SatParameters::EXPERIMENTAL_BINARY_MINIMIZATION:
765 *trail_, &learned_conflict_);
768 DCHECK(IsConflictValid(learned_conflict_));
782 counters_.num_literals_learned += learned_conflict_.size();
783 Backtrack(ComputeBacktrackLevel(learned_conflict_));
784 DCHECK(ClauseIsValidUnderDebugAssignement(learned_conflict_));
790 if (drat_proof_handler_ !=
nullptr) {
791 drat_proof_handler_->
AddClause(learned_conflict_);
796 bool is_redundant =
true;
797 if (!subsumed_clauses_.empty() &&
798 parameters_->subsumption_during_conflict_analysis()) {
799 for (SatClause* clause : subsumed_clauses_) {
800 DCHECK(ClauseSubsumption(learned_conflict_, clause));
802 is_redundant =
false;
807 counters_.num_subsumed_clauses += subsumed_clauses_.size();
811 const int conflict_lbd = AddLearnedClauseAndEnqueueUnitPropagation(
812 learned_conflict_, is_redundant);
813 restart_->
OnConflict(conflict_trail_index, conflict_decision_level,
819 int max_level,
int* first_propagation_index) {
821 int decision_index = current_decision_level_;
822 while (decision_index <= max_level) {
823 DCHECK_GE(decision_index, current_decision_level_);
824 const Literal previous_decision = decisions_[decision_index].literal;
826 if (
Assignment().LiteralIsTrue(previous_decision)) {
832 if (
Assignment().LiteralIsFalse(previous_decision)) {
834 decisions_[current_decision_level_].literal = previous_decision;
839 const int old_level = current_decision_level_;
841 *first_propagation_index =
std::min(*first_propagation_index,
index);
843 if (current_decision_level_ <= old_level) {
855 decision_index = current_decision_level_;
863 CHECK(PropagationIsDone());
868 int first_propagation_index = trail_->
Index();
870 return first_propagation_index;
875 CHECK(PropagationIsDone());
879 EnqueueNewDecision(true_literal);
904 if (target_level == 0) counters_.num_restarts++;
909 int target_trail_index = 0;
910 while (current_decision_level_ > target_level) {
911 --current_decision_level_;
912 target_trail_index = decisions_[current_decision_level_].trail_index;
914 Untrail(target_trail_index);
915 last_decision_or_backtrack_trail_index_ = trail_->
Index();
924 return SetModelUnsat();
926 AddBinaryClauseInternal(c.a, c.b);
928 if (!
Propagate())
return SetModelUnsat();
948 const std::vector<Literal>& assumptions) {
951 return SolveInternal(time_limit_);
955 if (parameters_->log_search_progress()) {
956 LOG(
INFO) << RunningStatisticsString();
957 LOG(
INFO) << StatusString(status);
965 assumption_level_ = assumption_level;
974void SatSolver::KeepAllClauseUsedToInfer(BooleanVariable variable) {
976 if (trail_->
Info(variable).
level == 0)
return;
978 std::vector<bool> is_marked(trail_index + 1,
false);
979 is_marked[trail_index] =
true;
981 for (; num > 0 && trail_index >= 0; --trail_index) {
982 if (!is_marked[trail_index])
continue;
983 is_marked[trail_index] =
false;
986 const BooleanVariable
var = (*trail_)[trail_index].Variable();
988 if (clause !=
nullptr) {
991 for (
const Literal l : trail_->
Reason(
var)) {
992 const AssignmentInfo& info = trail_->
Info(l.Variable());
993 if (info.level == 0)
continue;
994 if (!is_marked[info.trail_index]) {
995 is_marked[info.trail_index] =
true;
1005void SatSolver::TryToMinimizeClause(SatClause* clause) {
1007 ++counters_.minimization_num_clauses;
1009 std::set<LiteralIndex> moved_last;
1010 std::vector<Literal> candidate(clause->begin(), clause->end());
1011 while (!model_is_unsat_) {
1018 if (target_level == -1)
break;
1022 const Literal
literal = candidate[level];
1024 candidate.erase(candidate.begin() + level);
1027 const int variable_level =
1029 if (variable_level == 0) {
1030 ProcessNewlyFixedVariablesForDratProof();
1031 counters_.minimization_num_true++;
1032 counters_.minimization_num_removed_literals += clause->size();
1034 clauses_propagator_->
Detach(clause);
1042 if (ReasonClauseOrNull(
literal.Variable()) != clause) {
1043 counters_.minimization_num_subsumed++;
1044 counters_.minimization_num_removed_literals += clause->size();
1047 KeepAllClauseUsedToInfer(
literal.Variable());
1049 clauses_propagator_->
Detach(clause);
1055 if (variable_level + 1 < candidate.size()) {
1056 candidate.resize(variable_level);
1062 ++counters_.minimization_num_decisions;
1064 if (!clause->IsAttached()) {
1068 if (model_is_unsat_)
return;
1071 if (candidate.empty()) {
1072 model_is_unsat_ =
true;
1075 moved_last.insert(candidate.back().Index());
1080 if (candidate.size() == clause->size())
return;
1082 if (candidate.size() == 1) {
1083 if (drat_proof_handler_ !=
nullptr) {
1084 drat_proof_handler_->
AddClause(candidate);
1086 if (!
Assignment().VariableIsAssigned(candidate[0].Variable())) {
1087 counters_.minimization_num_removed_literals += clause->size();
1094 if (parameters_->treat_binary_clauses_separately() && candidate.size() == 2) {
1095 counters_.minimization_num_removed_literals += clause->size() - 2;
1098 AddBinaryClauseInternal(candidate[0], candidate[1]);
1099 clauses_propagator_->
Detach(clause);
1108 counters_.minimization_num_removed_literals +=
1109 clause->size() - candidate.size();
1114 model_is_unsat_ =
true;
1128 if (parameters_->log_search_progress()) {
1130 LOG(
INFO) <<
"Number of variables: " << num_variables_;
1131 LOG(
INFO) <<
"Number of clauses (size > 2): "
1133 LOG(
INFO) <<
"Number of binary clauses: "
1135 LOG(
INFO) <<
"Number of linear constraints: "
1137 LOG(
INFO) <<
"Number of fixed variables: " << trail_->
Index();
1138 LOG(
INFO) <<
"Number of watched clauses: "
1144 int64 next_minimization_num_restart =
1146 parameters_->minimize_with_propagation_restart_period();
1149 const int64 kDisplayFrequency = 10000;
1150 int64 next_display = parameters_->log_search_progress()
1155 const int64 kMemoryCheckFrequency = 10000;
1156 int64 next_memory_check =
1161 const int64 kFailureLimit =
1162 parameters_->max_number_of_conflicts() ==
1165 : counters_.
num_failures + parameters_->max_number_of_conflicts();
1173 if (parameters_->log_search_progress()) {
1174 LOG(
INFO) <<
"The time limit has been reached. Aborting.";
1180 if (parameters_->log_search_progress()) {
1181 LOG(
INFO) <<
"The conflict limit has been reached. Aborting.";
1191 if (counters_.num_failures >= next_memory_check) {
1192 next_memory_check = NextMultipleOf(
num_failures(), kMemoryCheckFrequency);
1193 if (IsMemoryLimitReached()) {
1194 if (parameters_->log_search_progress()) {
1195 LOG(
INFO) <<
"The memory limit has been reached. Aborting.";
1203 if (counters_.num_failures >= next_display) {
1204 LOG(
INFO) << RunningStatisticsString();
1205 next_display = NextMultipleOf(
num_failures(), kDisplayFrequency);
1208 if (!PropagateAndStopAfterOneConflictResolution()) {
1210 if (model_is_unsat_)
return StatusWithLog(
INFEASIBLE);
1216 if (trail_->
Index() == num_variables_.value()) {
1226 restart_->
NumRestarts() >= next_minimization_num_restart) {
1227 next_minimization_num_restart =
1229 parameters_->minimize_with_propagation_restart_period();
1231 parameters_->minimize_with_propagation_num_decisions());
1235 if (model_is_unsat_)
return StatusWithLog(
INFEASIBLE);
1236 if (trail_->
Index() == num_variables_.value()) {
1242 EnqueueNewDecision(decision_policy_->
NextBranch());
1250 block_clause_deletion_ =
true;
1252 const int64 target_num_branches = counters_.num_branches + decisions_budget;
1253 while (counters_.num_branches < target_num_branches &&
1254 (time_limit_ ==
nullptr || !time_limit_->
LimitReached())) {
1256 if (to_minimize !=
nullptr) {
1257 TryToMinimizeClause(to_minimize);
1258 if (model_is_unsat_)
return;
1260 if (to_minimize ==
nullptr) {
1261 VLOG(1) <<
"Minimized all clauses, restarting from first one.";
1268 block_clause_deletion_ =
false;
1275 std::vector<Literal> unsat_assumptions;
1291 unsat_assumptions.push_back(decisions_[i].
literal);
1293 return unsat_assumptions;
1296 unsat_assumptions.push_back(false_assumption);
1303 int trail_index = trail_->
Info(false_assumption.
Variable()).trail_index;
1309 while (trail_index >= 0 && !is_marked_[(*trail_)[trail_index].Variable()]) {
1312 if (trail_index < limit)
break;
1313 const Literal marked_literal = (*trail_)[trail_index];
1318 unsat_assumptions.push_back(marked_literal);
1322 const BooleanVariable
var =
literal.Variable();
1323 const int level = DecisionLevel(
var);
1324 if (level > 0 && !is_marked_[
var]) is_marked_.
Set(
var);
1331 std::reverse(unsat_assumptions.begin(), unsat_assumptions.end());
1332 return unsat_assumptions;
1335void SatSolver::BumpReasonActivities(
const std::vector<Literal>& literals) {
1338 const BooleanVariable
var =
literal.Variable();
1339 if (DecisionLevel(
var) > 0) {
1341 if (clause !=
nullptr) {
1342 BumpClauseActivity(clause);
1344 UpperBoundedLinearConstraint* pb_constraint =
1345 ReasonPbConstraintOrNull(
var);
1346 if (pb_constraint !=
nullptr) {
1356void SatSolver::BumpClauseActivity(SatClause* clause) {
1367 const int new_lbd = ComputeLbd(*clause);
1368 if (new_lbd + 1 <= parameters_->clause_cleanup_lbd_bound()) {
1374 switch (parameters_->clause_cleanup_protection()) {
1375 case SatParameters::PROTECTION_NONE:
1377 case SatParameters::PROTECTION_ALWAYS:
1378 it->second.protected_during_next_cleanup =
true;
1380 case SatParameters::PROTECTION_LBD:
1385 if (new_lbd + 1 < it->second.lbd) {
1386 it->second.protected_during_next_cleanup =
true;
1387 it->second.lbd = new_lbd;
1392 const double activity = it->second.activity += clause_activity_increment_;
1393 if (activity > parameters_->max_clause_activity_value()) {
1394 RescaleClauseActivities(1.0 / parameters_->max_clause_activity_value());
1398void SatSolver::RescaleClauseActivities(
double scaling_factor) {
1400 clause_activity_increment_ *= scaling_factor;
1402 entry.second.activity *= scaling_factor;
1406void SatSolver::UpdateClauseActivityIncrement() {
1408 clause_activity_increment_ *= 1.0 / parameters_->clause_activity_decay();
1411bool SatSolver::IsConflictValid(
const std::vector<Literal>& literals) {
1413 if (literals.empty())
return false;
1414 const int highest_level = DecisionLevel(literals[0].Variable());
1415 for (
int i = 1; i < literals.size(); ++i) {
1416 const int level = DecisionLevel(literals[i].Variable());
1417 if (level <= 0 || level >= highest_level)
return false;
1422int SatSolver::ComputeBacktrackLevel(
const std::vector<Literal>& literals) {
1435 int backtrack_level = 0;
1436 for (
int i = 1; i < literals.size(); ++i) {
1437 const int level = DecisionLevel(literals[i].Variable());
1438 backtrack_level =
std::max(backtrack_level, level);
1440 DCHECK_LT(backtrack_level, DecisionLevel(literals[0].Variable()));
1442 return backtrack_level;
1445template <
typename LiteralList>
1446int SatSolver::ComputeLbd(
const LiteralList& literals) {
1449 parameters_->count_assumption_levels_in_lbd() ? 0 : assumption_level_;
1453 SatDecisionLevel(DecisionLevel(literals.begin()->Variable()) + 1));
1454 for (
const Literal
literal : literals) {
1455 const SatDecisionLevel level(DecisionLevel(
literal.Variable()));
1457 if (level > limit && !is_level_marked_[level]) {
1458 is_level_marked_.
Set(level);
1464std::string SatSolver::StatusString(Status status)
const {
1465 const double time_in_s = timer_.
Get();
1467 absl::StrFormat(
" time: %fs\n", time_in_s) +
1470 " num failures: %d (%.0f /sec)\n", counters_.num_failures,
1471 static_cast<double>(counters_.num_failures) / time_in_s) +
1473 " num branches: %d (%.0f /sec)\n", counters_.num_branches,
1474 static_cast<double>(counters_.num_branches) / time_in_s) +
1475 absl::StrFormat(
" num propagations: %d (%.0f /sec)\n",
1478 absl::StrFormat(
" num binary propagations: %d\n",
1480 absl::StrFormat(
" num binary inspections: %d\n",
1483 " num binary redundant implications: %d\n",
1486 " num classic minimizations: %d"
1487 " (literals removed: %d)\n",
1488 counters_.num_minimizations, counters_.num_literals_removed) +
1490 " num binary minimizations: %d"
1491 " (literals removed: %d)\n",
1494 absl::StrFormat(
" num inspected clauses: %d\n",
1496 absl::StrFormat(
" num inspected clause_literals: %d\n",
1499 " num learned literals: %d (avg: %.1f /clause)\n",
1500 counters_.num_literals_learned,
1501 1.0 * counters_.num_literals_learned / counters_.num_failures) +
1503 " num learned PB literals: %d (avg: %.1f /clause)\n",
1504 counters_.num_learned_pb_literals,
1505 1.0 * counters_.num_learned_pb_literals / counters_.num_failures) +
1506 absl::StrFormat(
" num subsumed clauses: %d\n",
1507 counters_.num_subsumed_clauses) +
1508 absl::StrFormat(
" minimization_num_clauses: %d\n",
1509 counters_.minimization_num_clauses) +
1510 absl::StrFormat(
" minimization_num_decisions: %d\n",
1511 counters_.minimization_num_decisions) +
1512 absl::StrFormat(
" minimization_num_true: %d\n",
1513 counters_.minimization_num_true) +
1514 absl::StrFormat(
" minimization_num_subsumed: %d\n",
1515 counters_.minimization_num_subsumed) +
1516 absl::StrFormat(
" minimization_num_removed_literals: %d\n",
1517 counters_.minimization_num_removed_literals) +
1518 absl::StrFormat(
" pb num threshold updates: %d\n",
1520 absl::StrFormat(
" pb num constraint lookups: %d\n",
1522 absl::StrFormat(
" pb num inspected constraint literals: %d\n",
1528std::string SatSolver::RunningStatisticsString()
const {
1529 const double time_in_s = timer_.
Get();
1530 return absl::StrFormat(
1531 "%6.2fs, mem:%s, fails:%d, depth:%d, clauses:%d, tmp:%d, bin:%u, "
1532 "restarts:%d, vars:%d",
1538 num_variables_.value() - num_processed_fixed_variables_);
1541void SatSolver::ProcessNewlyFixedVariablesForDratProof() {
1542 if (drat_proof_handler_ ==
nullptr)
return;
1556 for (; drat_num_processed_fixed_variables_ < trail_->
Index();
1557 ++drat_num_processed_fixed_variables_) {
1558 temp = (*trail_)[drat_num_processed_fixed_variables_];
1559 drat_proof_handler_->
AddClause({&temp, 1});
1566 int num_detached_clauses = 0;
1569 ProcessNewlyFixedVariablesForDratProof();
1575 if (!clause->IsAttached())
continue;
1577 const size_t old_size = clause->size();
1578 if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->
Assignment())) {
1581 ++num_detached_clauses;
1585 const size_t new_size = clause->size();
1586 if (new_size == old_size)
continue;
1588 if (drat_proof_handler_ !=
nullptr) {
1590 drat_proof_handler_->
AddClause({clause->begin(), new_size});
1591 drat_proof_handler_->
DeleteClause({clause->begin(), old_size});
1594 if (new_size == 2 && parameters_->treat_binary_clauses_separately()) {
1598 AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
1607 if (num_detached_clauses > 0 || num_binary > 0) {
1608 VLOG(1) << trail_->
Index() <<
" fixed variables at level 0. "
1609 <<
"Detached " << num_detached_clauses <<
" clauses. " << num_binary
1610 <<
" converted to binary.";
1615 num_processed_fixed_variables_ = trail_->
Index();
1632 const int old_index = trail_->
Index();
1634 DCHECK(propagator->PropagatePreconditionsAreSatisfied(*trail_));
1635 if (!propagator->Propagate(trail_))
return false;
1636 if (trail_->
Index() > old_index)
break;
1638 if (trail_->
Index() == old_index)
break;
1643void SatSolver::InitializePropagators() {
1644 propagators_.clear();
1655 if (!binary_implication_graph_->
IsEmpty()) {
1656 propagators_.push_back(binary_implication_graph_);
1658 propagators_.push_back(clauses_propagator_);
1660 propagators_.push_back(pb_constraints_);
1662 for (
int i = 0; i < external_propagators_.size(); ++i) {
1663 propagators_.push_back(external_propagators_[i]);
1665 if (last_propagator_ !=
nullptr) {
1666 propagators_.push_back(last_propagator_);
1670bool SatSolver::PropagationIsDone()
const {
1671 for (SatPropagator* propagator : propagators_) {
1672 if (!propagator->PropagationIsDone(*trail_))
return false;
1677bool SatSolver::ResolvePBConflict(BooleanVariable
var,
1678 MutableUpperBoundedLinearConstraint* conflict,
1679 Coefficient* slack) {
1683 DCHECK_EQ(*slack, conflict->ComputeSlackForTrailPrefix(*trail_, trail_index));
1686 UpperBoundedLinearConstraint* pb_reason = ReasonPbConstraintOrNull(
var);
1687 if (pb_reason !=
nullptr) {
1688 pb_reason->ResolvePBConflict(*trail_,
var, conflict, slack);
1693 Coefficient multiplier(1);
1696 const int algorithm = 1;
1697 switch (algorithm) {
1701 conflict->ReduceSlackTo(*trail_, trail_index, *slack, Coefficient(0));
1705 multiplier = *slack + 1;
1709 multiplier = conflict->GetCoefficient(
var);
1712 Coefficient num_literals(1);
1719 conflict->AddTerm(
literal.Negated(), multiplier);
1722 conflict->AddToRhs((num_literals - 1) * multiplier);
1726 DCHECK_EQ(*slack, conflict->ComputeSlackForTrailPrefix(*trail_, trail_index));
1730void SatSolver::EnqueueNewDecision(Literal
literal) {
1741 const double kMinDeterministicTimeBetweenCleanups = 1.0;
1742 if (num_processed_fixed_variables_ < trail_->
Index() &&
1744 deterministic_time_of_last_fixed_variables_cleanup_ +
1745 kMinDeterministicTimeBetweenCleanups) {
1750 counters_.num_branches++;
1751 last_decision_or_backtrack_trail_index_ = trail_->
Index();
1752 decisions_[current_decision_level_] = Decision(trail_->
Index(),
literal);
1753 ++current_decision_level_;
1758void SatSolver::Untrail(
int target_trail_index) {
1761 for (SatPropagator* propagator : propagators_) {
1762 propagator->Untrail(*trail_, target_trail_index);
1764 decision_policy_->
Untrail(target_trail_index);
1765 trail_->
Untrail(target_trail_index);
1768std::string SatSolver::DebugString(
const SatClause& clause)
const {
1770 for (
const Literal
literal : clause) {
1771 if (!result.empty()) {
1772 result.append(
" || ");
1774 const std::string
value =
1779 result.append(absl::StrFormat(
"%s(%s)",
literal.DebugString(),
value));
1784int SatSolver::ComputeMaxTrailIndex(absl::Span<const Literal> clause)
const {
1786 int trail_index = -1;
1787 for (
const Literal
literal : clause) {
1797void SatSolver::ComputeFirstUIPConflict(
1798 int max_trail_index, std::vector<Literal>* conflict,
1799 std::vector<Literal>* reason_used_to_infer_the_conflict,
1800 std::vector<SatClause*>* subsumed_clauses) {
1808 reason_used_to_infer_the_conflict->clear();
1809 subsumed_clauses->clear();
1810 if (max_trail_index == -1)
return;
1816 int trail_index = max_trail_index;
1817 const int highest_level = DecisionLevel((*trail_)[trail_index].Variable());
1818 if (highest_level == 0)
return;
1835 absl::Span<const Literal> clause_to_expand = trail_->
FailingClause();
1837 DCHECK(!clause_to_expand.empty());
1838 int num_literal_at_highest_level_that_needs_to_be_processed = 0;
1840 int num_new_vars_at_positive_level = 0;
1841 int num_vars_at_positive_level_in_clause_to_expand = 0;
1842 for (
const Literal
literal : clause_to_expand) {
1843 const BooleanVariable
var =
literal.Variable();
1844 const int level = DecisionLevel(
var);
1845 if (level > 0) ++num_vars_at_positive_level_in_clause_to_expand;
1846 if (!is_marked_[
var]) {
1848 if (level == highest_level) {
1849 ++num_new_vars_at_positive_level;
1850 ++num_literal_at_highest_level_that_needs_to_be_processed;
1851 }
else if (level > 0) {
1852 ++num_new_vars_at_positive_level;
1858 reason_used_to_infer_the_conflict->push_back(
literal);
1865 if (num_new_vars_at_positive_level > 0) {
1868 subsumed_clauses->clear();
1875 if (sat_clause !=
nullptr &&
1876 num_vars_at_positive_level_in_clause_to_expand ==
1878 num_literal_at_highest_level_that_needs_to_be_processed) {
1879 subsumed_clauses->push_back(sat_clause);
1883 DCHECK_GT(num_literal_at_highest_level_that_needs_to_be_processed, 0);
1884 while (!is_marked_[(*trail_)[trail_index].Variable()]) {
1887 DCHECK_EQ(DecisionLevel((*trail_)[trail_index].Variable()),
1891 if (num_literal_at_highest_level_that_needs_to_be_processed == 1) {
1895 conflict->push_back((*trail_)[trail_index].Negated());
1898 std::swap(conflict->back(), conflict->front());
1902 const Literal
literal = (*trail_)[trail_index];
1903 reason_used_to_infer_the_conflict->push_back(
literal);
1909 clause_to_expand = {};
1913 sat_clause = ReasonClauseOrNull(
literal.Variable());
1915 --num_literal_at_highest_level_that_needs_to_be_processed;
1920void SatSolver::ComputeUnionOfReasons(
const std::vector<Literal>&
input,
1921 std::vector<Literal>* literals) {
1924 for (
const Literal l :
input) tmp_mark_.
Set(l.Variable());
1925 for (
const Literal l :
input) {
1926 for (
const Literal r : trail_->
Reason(l.Variable())) {
1927 if (!tmp_mark_[r.Variable()]) {
1928 tmp_mark_.
Set(r.Variable());
1929 literals->push_back(r);
1933 for (
const Literal l :
input) tmp_mark_.
Clear(l.Variable());
1934 for (
const Literal l : *literals) tmp_mark_.
Clear(l.Variable());
1938void SatSolver::ComputePBConflict(
int max_trail_index,
1939 Coefficient initial_slack,
1940 MutableUpperBoundedLinearConstraint* conflict,
1941 int* pb_backjump_level) {
1943 int trail_index = max_trail_index;
1947 Coefficient slack = initial_slack;
1949 conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1));
1950 CHECK_LT(slack, 0) <<
"We don't have a conflict!";
1953 int backjump_level = 0;
1955 const BooleanVariable
var = (*trail_)[trail_index].Variable();
1958 if (conflict->GetCoefficient(
var) > 0 &&
1960 if (parameters_->minimize_reduction_during_pb_resolution()) {
1965 conflict->ReduceGivenCoefficient(
var);
1969 slack += conflict->GetCoefficient(
var);
1973 if (slack < 0)
continue;
1979 const int current_level = DecisionLevel(
var);
1980 int i = trail_index;
1982 const BooleanVariable previous_var = (*trail_)[i].Variable();
1983 if (conflict->GetCoefficient(previous_var) > 0 &&
1985 conflict->GetLiteral(previous_var))) {
1990 if (i < 0 || DecisionLevel((*trail_)[i].Variable()) < current_level) {
1991 backjump_level = i < 0 ? 0 : DecisionLevel((*trail_)[i].Variable());
1997 const bool clause_used = ResolvePBConflict(
var, conflict, &slack);
2006 const Coefficient slack_only_for_debug =
2008 ? conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1)
2013 if (!parameters_->minimize_reduction_during_pb_resolution()) {
2014 conflict->ReduceCoefficients();
2020 if (parameters_->minimize_reduction_during_pb_resolution()) {
2022 conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1);
2024 slack = conflict->ReduceCoefficientsAndComputeSlackForTrailPrefix(
2025 *trail_, trail_index + 1);
2030 if (conflict->Rhs() < 0) {
2031 *pb_backjump_level = -1;
2039 if (!parameters_->minimize_reduction_during_pb_resolution()) {
2040 conflict->ReduceCoefficients();
2045 std::vector<Coefficient> sum_for_le_level(backjump_level + 2, Coefficient(0));
2046 std::vector<Coefficient> max_coeff_for_ge_level(backjump_level + 2,
2049 Coefficient max_sum(0);
2050 for (BooleanVariable
var : conflict->PossibleNonZeros()) {
2051 const Coefficient coeff = conflict->GetCoefficient(
var);
2052 if (coeff == 0)
continue;
2056 DecisionLevel(
var) > backjump_level) {
2057 max_coeff_for_ge_level[backjump_level + 1] =
2058 std::max(max_coeff_for_ge_level[backjump_level + 1], coeff);
2060 const int level = DecisionLevel(
var);
2062 sum_for_le_level[level] += coeff;
2064 max_coeff_for_ge_level[level] =
2065 std::max(max_coeff_for_ge_level[level], coeff);
2070 for (
int i = 1; i < sum_for_le_level.size(); ++i) {
2071 sum_for_le_level[i] += sum_for_le_level[i - 1];
2073 for (
int i = max_coeff_for_ge_level.size() - 2; i >= 0; --i) {
2074 max_coeff_for_ge_level[i] =
2075 std::max(max_coeff_for_ge_level[i], max_coeff_for_ge_level[i + 1]);
2080 if (sum_for_le_level[0] > conflict->Rhs()) {
2081 *pb_backjump_level = -1;
2084 for (
int i = 0; i <= backjump_level; ++i) {
2085 const Coefficient level_sum = sum_for_le_level[i];
2086 CHECK_LE(level_sum, conflict->Rhs());
2087 if (conflict->Rhs() - level_sum < max_coeff_for_ge_level[i + 1]) {
2088 *pb_backjump_level = i;
2092 LOG(
FATAL) <<
"The code should never reach here.";
2095void SatSolver::MinimizeConflict(
2096 std::vector<Literal>* conflict,
2097 std::vector<Literal>* reason_used_to_infer_the_conflict) {
2100 const int old_size = conflict->size();
2101 switch (parameters_->minimization_algorithm()) {
2102 case SatParameters::NONE:
2104 case SatParameters::SIMPLE: {
2105 MinimizeConflictSimple(conflict);
2108 case SatParameters::RECURSIVE: {
2109 MinimizeConflictRecursively(conflict);
2112 case SatParameters::EXPERIMENTAL: {
2113 MinimizeConflictExperimental(conflict);
2117 if (conflict->size() < old_size) {
2118 ++counters_.num_minimizations;
2119 counters_.num_literals_removed += old_size - conflict->size();
2130void SatSolver::MinimizeConflictSimple(std::vector<Literal>* conflict) {
2137 for (
int i = 1; i < conflict->size(); ++i) {
2138 const BooleanVariable
var = (*conflict)[i].Variable();
2139 bool can_be_removed =
false;
2140 if (DecisionLevel(
var) != current_level) {
2142 const absl::Span<const Literal> reason = trail_->
Reason(
var);
2143 if (!reason.empty()) {
2144 can_be_removed =
true;
2145 for (Literal
literal : reason) {
2146 if (DecisionLevel(
literal.Variable()) == 0)
continue;
2147 if (!is_marked_[
literal.Variable()]) {
2148 can_be_removed =
false;
2154 if (!can_be_removed) {
2155 (*conflict)[
index] = (*conflict)[i];
2159 conflict->erase(conflict->begin() +
index, conflict->end());
2168void SatSolver::MinimizeConflictRecursively(std::vector<Literal>* conflict) {
2202 const int level = DecisionLevel(
var);
2203 min_trail_index_per_level_[level] =
std::min(
2211 for (
int i = 1; i < conflict->size(); ++i) {
2212 const BooleanVariable
var = (*conflict)[i].Variable();
2215 min_trail_index_per_level_[DecisionLevel(
var)] ||
2216 !CanBeInferedFromConflictVariables(
var)) {
2219 is_independent_.
Set(
var);
2220 (*conflict)[
index] = (*conflict)[i];
2224 conflict->resize(
index);
2228 const int threshold = min_trail_index_per_level_.size() / 2;
2231 min_trail_index_per_level_[DecisionLevel(
var)] =
2235 min_trail_index_per_level_.clear();
2239bool SatSolver::CanBeInferedFromConflictVariables(BooleanVariable variable) {
2242 DCHECK(is_marked_[variable]);
2243 const BooleanVariable v =
2245 if (v != variable)
return !is_independent_[v];
2258 dfs_stack_.push_back(variable);
2259 variable_to_process_.clear();
2260 variable_to_process_.push_back(variable);
2264 const BooleanVariable
var =
literal.Variable();
2266 if (is_marked_[
var])
continue;
2267 const int level = DecisionLevel(
var);
2277 is_independent_[
var]) {
2280 variable_to_process_.push_back(
var);
2284 while (!variable_to_process_.empty()) {
2285 const BooleanVariable current_var = variable_to_process_.back();
2286 if (current_var == dfs_stack_.back()) {
2289 if (dfs_stack_.size() > 1) {
2290 DCHECK(!is_marked_[current_var]);
2291 is_marked_.
Set(current_var);
2293 variable_to_process_.pop_back();
2294 dfs_stack_.pop_back();
2299 if (is_marked_[current_var]) {
2300 variable_to_process_.pop_back();
2306 DCHECK(!is_independent_[current_var]);
2310 const BooleanVariable v =
2312 if (v != current_var) {
2313 if (is_independent_[v])
break;
2315 variable_to_process_.pop_back();
2321 dfs_stack_.push_back(current_var);
2322 bool abort_early =
false;
2324 const BooleanVariable
var =
literal.Variable();
2326 const int level = DecisionLevel(
var);
2327 if (level == 0 || is_marked_[
var])
continue;
2329 is_independent_[
var]) {
2333 variable_to_process_.push_back(
var);
2335 if (abort_early)
break;
2339 for (
const BooleanVariable
var : dfs_stack_) {
2340 is_independent_.
Set(
var);
2342 return dfs_stack_.empty();
2347struct WeightedVariable {
2348 WeightedVariable(BooleanVariable v,
int w) :
var(v),
weight(w) {}
2356struct VariableWithLargerWeightFirst {
2357 bool operator()(
const WeightedVariable& wv1,
2358 const WeightedVariable& wv2)
const {
2359 return (wv1.weight > wv2.weight ||
2360 (wv1.weight == wv2.weight && wv1.var < wv2.var));
2376void SatSolver::MinimizeConflictExperimental(std::vector<Literal>* conflict) {
2383 std::vector<WeightedVariable> variables_sorted_by_level;
2384 for (Literal
literal : *conflict) {
2385 const BooleanVariable
var =
literal.Variable();
2387 const int level = DecisionLevel(
var);
2388 if (level < current_level) {
2389 variables_sorted_by_level.push_back(WeightedVariable(
var, level));
2392 std::sort(variables_sorted_by_level.begin(), variables_sorted_by_level.end(),
2393 VariableWithLargerWeightFirst());
2396 std::vector<BooleanVariable> to_remove;
2397 for (WeightedVariable weighted_var : variables_sorted_by_level) {
2398 const BooleanVariable
var = weighted_var.var;
2402 const absl::Span<const Literal> reason = trail_->
Reason(
var);
2403 if (reason.empty())
continue;
2407 std::vector<Literal> not_contained_literals;
2408 for (
const Literal reason_literal : reason) {
2409 const BooleanVariable reason_var = reason_literal.Variable();
2412 if (DecisionLevel(reason_var) == 0)
continue;
2417 if (!is_marked_[reason_var]) {
2418 not_contained_literals.push_back(reason_literal);
2419 if (not_contained_literals.size() > 1)
break;
2422 if (not_contained_literals.empty()) {
2427 to_remove.push_back(
var);
2428 }
else if (not_contained_literals.size() == 1) {
2431 to_remove.push_back(
var);
2432 is_marked_.
Set(not_contained_literals.front().Variable());
2433 conflict->push_back(not_contained_literals.front());
2438 for (BooleanVariable
var : to_remove) {
2444 for (
int i = 0; i < conflict->size(); ++i) {
2445 const Literal
literal = (*conflict)[i];
2446 if (is_marked_[
literal.Variable()]) {
2451 conflict->erase(conflict->begin() +
index, conflict->end());
2454void SatSolver::CleanClauseDatabaseIfNeeded() {
2455 if (num_learned_clause_before_cleanup_ > 0)
return;
2460 typedef std::pair<SatClause*, ClauseInfo> Entry;
2461 std::vector<Entry> entries;
2463 for (
auto& entry : clauses_info) {
2464 if (ClauseIsUsedAsReason(entry.first))
continue;
2465 if (entry.second.protected_during_next_cleanup) {
2466 entry.second.protected_during_next_cleanup =
false;
2469 entries.push_back(entry);
2471 const int num_protected_clauses = clauses_info.size() - entries.size();
2473 if (parameters_->clause_cleanup_ordering() == SatParameters::CLAUSE_LBD) {
2475 std::sort(entries.begin(), entries.end(),
2476 [](
const Entry&
a,
const Entry&
b) {
2477 if (a.second.lbd == b.second.lbd) {
2478 return a.second.activity < b.second.activity;
2480 return a.second.lbd >
b.second.lbd;
2484 std::sort(entries.begin(), entries.end(),
2485 [](
const Entry&
a,
const Entry&
b) {
2486 if (a.second.activity == b.second.activity) {
2487 return a.second.lbd > b.second.lbd;
2489 return a.second.activity <
b.second.activity;
2494 int num_kept_clauses =
std::min(
static_cast<int>(entries.size()),
2495 parameters_->clause_cleanup_target());
2496 int num_deleted_clauses = entries.size() - num_kept_clauses;
2501 while (num_deleted_clauses > 0) {
2502 const ClauseInfo&
a = entries[num_deleted_clauses].second;
2503 const ClauseInfo&
b = entries[num_deleted_clauses - 1].second;
2504 if (
a.activity !=
b.activity ||
a.lbd !=
b.lbd)
break;
2505 --num_deleted_clauses;
2508 if (num_deleted_clauses > 0) {
2509 entries.resize(num_deleted_clauses);
2510 for (
const Entry& entry : entries) {
2511 SatClause* clause = entry.first;
2512 counters_.num_literals_forgotten += clause->size();
2513 clauses_propagator_->LazyDetach(clause);
2515 clauses_propagator_->CleanUpWatchers();
2519 if (!block_clause_deletion_) {
2520 clauses_propagator_->DeleteRemovedClauses();
2524 num_learned_clause_before_cleanup_ = parameters_->clause_cleanup_period();
2525 VLOG(1) <<
"Database cleanup, #protected:" << num_protected_clauses
2526 <<
" #kept:" << num_kept_clauses
2527 <<
" #deleted:" << num_deleted_clauses;
2532 case SatSolver::ASSUMPTIONS_UNSAT:
2533 return "ASSUMPTIONS_UNSAT";
2534 case SatSolver::INFEASIBLE:
2535 return "INFEASIBLE";
2536 case SatSolver::FEASIBLE:
2538 case SatSolver::LIMIT_REACHED:
2539 return "LIMIT_REACHED";
2543 LOG(DFATAL) <<
"Invalid SatSolver::Status " << status;
2548 std::vector<Literal> temp = *core;
2549 std::reverse(temp.begin(), temp.end());
2559 if (status != SatSolver::ASSUMPTIONS_UNSAT) {
2560 if (status != SatSolver::LIMIT_REACHED) {
2561 CHECK_NE(status, SatSolver::FEASIBLE);
2565 LOG(
WARNING) <<
"This should only happen rarely! otherwise, investigate. "
2571 if (temp.size() < core->size()) {
2572 VLOG(1) <<
"minimization " << core->size() <<
" -> " << temp.size();
2573 std::reverse(temp.begin(), temp.end());
#define DCHECK_LE(val1, val2)
#define DCHECK_NE(val1, val2)
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define CHECK_GT(val1, val2)
#define DCHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define CHECK_LE(val1, val2)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
void Set(IntegerType index)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
int NumberOfSetCallsWithDifferentArguments() const
void Clear(IntegerType index)
void ClearAndResize(IntegerType size)
std::string StatString() const
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
void ResetLimitFromParameters(const Parameters ¶meters)
Sets new time limits.
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
const std::vector< BinaryClause > & newly_added() const
int64 num_inspections() const
void AddBinaryClause(Literal a, Literal b)
int64 num_literals_removed() const
void MinimizeConflictWithReachability(std::vector< Literal > *c)
int64 num_minimization() const
bool AddBinaryClauseDuringSearch(Literal a, Literal b)
void MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, absl::BitGenRef random)
int64 num_implications() const
int64 num_propagations() const
void MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked)
void RemoveFixedVariables()
int64 num_redundant_implications() const
ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span< const Literal > at_most_one)
void MinimizeConflictExperimental(const Trail &trail, std::vector< Literal > *c)
void Resize(int num_variables)
void DeleteClause(absl::Span< const Literal > clause)
void AddClause(absl::Span< const Literal > clause)
BooleanVariable Variable() const
SatClause * NextClauseToMinimize()
absl::flat_hash_map< SatClause *, ClauseInfo > * mutable_clauses_info()
SatClause * AddRemovableClause(const std::vector< Literal > &literals, Trail *trail)
int64 num_removable_clauses() const
int64 num_clauses() const
int64 num_inspected_clauses() const
int64 num_watched_clauses() const
int64 num_inspected_clause_literals() const
bool AddClause(absl::Span< const Literal > literals, Trail *trail)
SatClause * ReasonClause(int trail_index) const
bool IsRemovable(SatClause *const clause) const
ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause)
void LazyDetach(SatClause *clause)
const std::vector< SatClause * > & AllClausesInCreationOrder() const
void ResetToMinimizeIndex()
void DeleteRemovedClauses()
void Detach(SatClause *clause)
void Resize(int num_variables)
Class that owns everything related to a particular optimization model.
void Register(T *non_owned_class)
Register a non-owned class that will be "singleton" in the model.
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
Coefficient ComputeSlackForTrailPrefix(const Trail &trail, int trail_index) const
void AddTerm(Literal literal, Coefficient coeff)
void AddToRhs(Coefficient value)
void ClearAndResize(int num_variables)
void CopyIntoVector(std::vector< LiteralWithCoeff > *output)
int NumberOfConstraints() const
int64 num_threshold_updates() const
void ClearConflictingConstraint()
bool AddConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
UpperBoundedLinearConstraint * ConflictingConstraint()
int64 num_inspected_constraint_literals() const
int64 num_constraint_lookups() const
UpperBoundedLinearConstraint * ReasonPbConstraint(int trail_index) const
void UpdateActivityIncrement()
void BumpActivity(UpperBoundedLinearConstraint *constraint)
void Resize(int num_variables)
bool AddLearnedConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
std::string InfoString() const
void OnConflict(int conflict_trail_index, int conflict_decision_level, int conflict_lbd)
void IncreaseNumVariables(int num_variables)
void UpdateVariableActivityIncrement()
void Untrail(int target_trail_index)
void BumpVariableActivities(const std::vector< Literal > &literals)
void BeforeConflict(int trail_index)
void UpdateWeightedSign(const std::vector< LiteralWithCoeff > &terms, Coefficient rhs)
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
void SetNumVariables(int num_variables)
bool AddTernaryClause(Literal a, Literal b, Literal c)
void AddLastPropagator(SatPropagator *propagator)
const SatParameters & parameters() const
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
Status SolveWithTimeLimit(TimeLimit *time_limit)
void ProcessNewlyFixedVariables()
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)
void AddPropagator(SatPropagator *propagator)
int64 num_failures() const
const VariablesAssignment & Assignment() const
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
int64 num_branches() const
bool AddBinaryClauses(const std::vector< BinaryClause > &clauses)
const Trail & LiteralTrail() const
Status UnsatStatus() const
void SetAssumptionLevel(int assumption_level)
void SaveDebugAssignment()
void AdvanceDeterministicTime(TimeLimit *limit)
int64 num_propagations() const
void MinimizeSomeClauses(int decisions_budget)
int64 num_restarts() const
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void SetParameters(const SatParameters ¶meters)
bool AddBinaryClause(Literal a, Literal b)
int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal)
void Backtrack(int target_level)
bool RestoreSolverToAssumptionLevel()
std::vector< Literal > GetLastIncompatibleDecisions()
bool ReapplyAssumptionsIfNeeded()
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
int CurrentDecisionLevel() const
double deterministic_time() const
bool AddProblemClause(absl::Span< const Literal > literals)
bool AddUnitClause(Literal true_literal)
void ClearNewlyAddedBinaryClauses()
void RegisterPropagator(SatPropagator *propagator)
SatClause * FailingSatClause() const
const VariablesAssignment & Assignment() const
int AssignmentType(BooleanVariable var) const
absl::Span< const Literal > Reason(BooleanVariable var) const
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const
void Untrail(int target_trail_index)
int64 NumberOfEnqueues() const
const AssignmentInfo & Info(BooleanVariable var) const
absl::Span< const Literal > FailingClause() const
void SetDecisionLevel(int level)
void Resize(int num_variables)
void EnqueueWithUnitReason(Literal true_literal)
void EnqueueSearchDecision(Literal true_literal)
void AddToConflict(MutableUpperBoundedLinearConstraint *conflict)
BooleanVariable FirstVariableWithSameReason(BooleanVariable var)
void Resize(int num_variables)
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
void AssignFromTrueLiteral(Literal literal)
Literal GetTrueLiteralForAssignedVariable(BooleanVariable var) const
bool LiteralIsFalse(Literal literal) const
int NumberOfVariables() const
void Resize(int num_variables)
SharedTimeLimit * time_limit
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
int MoveOneUnprocessedLiteralLast(const std::set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound, Coefficient bound_shift, Coefficient max_value)
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
std::string SatStatusString(SatSolver::Status status)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
bool BooleanLinearExpressionIsCanonical(const std::vector< LiteralWithCoeff > &cst)
const int kUnsatTrailIndex
int64 MemoryUsageProcess()
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool SafeAddInto(IntegerType a, IntegerType *b)
std::string MemoryUsage()
std::string ProtobufShortDebugString(const P &message)
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)
static constexpr int kSearchDecision