18 #include "absl/strings/str_format.h"
27 bool LiteralComparator(
const LiteralWithCoeff&
a,
const LiteralWithCoeff&
b) {
28 return a.literal.Index() <
b.literal.Index();
31 bool CoeffComparator(
const LiteralWithCoeff&
a,
const LiteralWithCoeff&
b) {
32 if (
a.coefficient ==
b.coefficient) {
33 return a.literal.Index() <
b.literal.Index();
35 return a.coefficient <
b.coefficient;
41 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
42 Coefficient* max_value) {
50 std::sort(cst->begin(), cst->end(), LiteralComparator);
53 for (
int i = 0; i < cst->size(); ++i) {
74 (*cst)[
index] = current;
86 for (
int i = 0; i < cst->size(); ++i) {
97 std::sort(cst->begin(), cst->end(), CoeffComparator);
104 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
105 Coefficient* max_value) {
107 Coefficient shift_due_to_fixed_variables(0);
109 if (mapping[entry.literal.Index()] >= 0) {
114 if (!
SafeAddInto(-entry.coefficient, &shift_due_to_fixed_variables)) {
124 *bound_shift = shift_due_to_fixed_variables;
130 if (!
SafeAddInto(shift_due_to_fixed_variables, bound_shift))
return false;
136 const std::vector<LiteralWithCoeff>& cst) {
137 Coefficient previous(1);
139 if (term.coefficient < previous)
return false;
140 previous = term.coefficient;
148 std::vector<LiteralWithCoeff>* cst, Coefficient* rhs) {
155 if (x.coefficient > *rhs) x.coefficient = *rhs + 1;
160 Coefficient bound_shift,
161 Coefficient max_value) {
162 Coefficient rhs = upper_bound;
164 if (bound_shift > 0) {
170 return Coefficient(-1);
173 if (rhs < 0)
return Coefficient(-1);
178 Coefficient bound_shift,
179 Coefficient max_value) {
182 Coefficient shifted_lb = lower_bound;
184 if (bound_shift > 0) {
186 return Coefficient(-1);
192 if (shifted_lb <= 0) {
197 return max_value - shifted_lb;
201 bool use_lower_bound, Coefficient lower_bound,
bool use_upper_bound,
202 Coefficient upper_bound, std::vector<LiteralWithCoeff>* cst) {
204 Coefficient bound_shift;
205 Coefficient max_value;
210 if (use_upper_bound) {
211 const Coefficient rhs =
213 if (!AddConstraint(*cst, max_value, rhs))
return false;
215 if (use_lower_bound) {
217 for (
int i = 0; i < cst->size(); ++i) {
218 (*cst)[i].literal = (*cst)[i].literal.Negated();
220 const Coefficient rhs =
222 if (!AddConstraint(*cst, max_value, rhs))
return false;
227 bool CanonicalBooleanLinearProblem::AddConstraint(
228 const std::vector<LiteralWithCoeff>& cst, Coefficient max_value,
230 if (rhs < 0)
return false;
231 if (rhs >= max_value)
return true;
232 constraints_.emplace_back(cst.begin(), cst.end());
239 if (terms_.
size() != num_variables) {
240 terms_.
assign(num_variables, Coefficient(0));
252 terms_[
var] = Coefficient(0);
261 CHECK_LT(rhs_, max_sum_) <<
"Trivially sat.";
262 Coefficient removed_sum(0);
263 const Coefficient
bound = max_sum_ - rhs_;
272 max_sum_ -= removed_sum;
279 if (!result.empty()) result +=
" + ";
283 result += absl::StrFormat(
" <= %d", rhs_.value());
290 const Trail& trail,
int trail_index)
const {
291 Coefficient activity(0);
299 return rhs_ - activity;
305 Coefficient activity(0);
306 Coefficient removed_sum(0);
307 const Coefficient
bound = max_sum_ - rhs_;
327 max_sum_ -= removed_sum;
329 return rhs_ - activity;
333 const Trail& trail,
int trail_index, Coefficient initial_slack,
334 Coefficient target) {
336 const Coefficient slack = initial_slack;
343 const Coefficient coeff =
GetCoefficient(trail[trail_index].Variable());
347 if (slack == target)
return;
350 const Coefficient diff = slack - target;
359 terms_[
var] = (terms_[
var] > 0) ? terms_[
var] - diff : terms_[
var] + diff;
370 std::vector<LiteralWithCoeff>* output) {
378 std::sort(output->begin(), output->end(), CoeffComparator);
381 Coefficient MutableUpperBoundedLinearConstraint::ComputeMaxSum()
const {
382 Coefficient result(0);
390 const std::vector<LiteralWithCoeff>& cst)
391 : is_marked_for_deletion_(false),
393 first_reason_trail_index_(-1),
396 DCHECK(std::is_sorted(cst.begin(), cst.end(), CoeffComparator));
397 literals_.reserve(cst.size());
404 if (term.coefficient != prev) {
405 prev = term.coefficient;
409 coeffs_.reserve(size);
410 starts_.reserve(size + 1);
415 if (term.coefficient != prev) {
416 prev = term.coefficient;
417 coeffs_.push_back(term.coefficient);
418 starts_.push_back(literals_.size());
420 literals_.push_back(term.literal);
424 starts_.push_back(literals_.size());
426 hash_ =
ThoroughHash(
reinterpret_cast<const char*
>(cst.data()),
432 int literal_index = 0;
437 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
443 const std::vector<LiteralWithCoeff>& cst) {
444 if (cst.size() != literals_.size())
return false;
445 int literal_index = 0;
448 if (literals_[literal_index] != term.literal)
return false;
449 if (coeffs_[coeff_index] != term.coefficient)
return false;
451 if (literal_index == starts_[coeff_index + 1]) {
459 Coefficient rhs,
int trail_index, Coefficient* threshold,
Trail* trail,
465 Coefficient slack = rhs;
471 std::vector<Coefficient> sum_at_previous_level(last_level + 2,
474 int max_relevant_trail_index = 0;
475 if (trail_index > 0) {
476 int literal_index = 0;
479 const BooleanVariable
var =
literal.Variable();
480 const Coefficient coeff = coeffs_[coeff_index];
483 max_relevant_trail_index =
486 sum_at_previous_level[trail->
Info(
var).
level + 1] += coeff;
489 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
493 if (slack < 0)
return false;
496 for (
int i = 1; i < sum_at_previous_level.size(); ++i) {
497 sum_at_previous_level[i] += sum_at_previous_level[i - 1];
502 int literal_index = 0;
505 const BooleanVariable
var =
literal.Variable();
510 CHECK_LE(coeffs_[coeff_index], rhs_ - sum_at_previous_level[level])
511 <<
"var should have been propagated at an earlier level !";
514 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
524 index_ = coeffs_.size() - 1;
525 already_propagated_end_ = literals_.size();
526 Update(slack, threshold);
527 return *threshold < 0
528 ?
Propagate(max_relevant_trail_index, threshold, trail, helper)
533 int trail_index, Coefficient* threshold,
Trail* trail,
536 const Coefficient slack = GetSlackFromThreshold(*threshold);
537 DCHECK_GE(slack, 0) <<
"The constraint is already a conflict!";
538 while (index_ >= 0 && coeffs_[index_] > slack) --index_;
541 BooleanVariable first_propagated_variable(-1);
542 for (
int i = starts_[index_ + 1]; i < already_propagated_end_; ++i) {
547 FillReason(*trail, trail_index, literals_[i].Variable(),
549 helper->
conflict.push_back(literals_[i].Negated());
550 Update(slack, threshold);
555 if (first_propagated_variable < 0) {
556 if (first_reason_trail_index_ == -1) {
557 first_reason_trail_index_ = trail->
Index();
559 helper->
Enqueue(literals_[i].Negated(), trail_index,
this, trail);
560 first_propagated_variable = literals_[i].Variable();
566 first_propagated_variable);
570 Update(slack, threshold);
576 const Trail& trail,
int source_trail_index,
577 BooleanVariable propagated_variable, std::vector<Literal>* reason) {
583 reason->push_back(trail[source_trail_index].Negated());
590 int last_coeff_index = 0;
596 Coefficient slack = rhs_;
597 Coefficient propagated_variable_coefficient(0);
598 int coeff_index = coeffs_.size() - 1;
599 for (
int i = literals_.size() - 1; i >= 0; --i) {
601 if (
literal.Variable() == propagated_variable) {
602 propagated_variable_coefficient = coeffs_[coeff_index];
607 reason->push_back(
literal.Negated());
609 last_coeff_index = coeff_index;
611 slack -= coeffs_[coeff_index];
614 if (i == starts_[coeff_index]) {
618 DCHECK_GT(propagated_variable_coefficient, slack);
619 DCHECK_GE(propagated_variable_coefficient, 0);
622 if (reason->size() <= 1 || coeffs_.size() == 1)
return;
624 Coefficient limit = propagated_variable_coefficient - slack;
629 coeff_index = last_coeff_index;
630 if (coeffs_[coeff_index] >= limit)
return;
631 for (
int i = last_i; i < literals_.size(); ++i) {
633 if (i == starts_[coeff_index + 1]) {
635 if (coeffs_[coeff_index] >= limit)
break;
637 if (
literal.Negated() != reason->back())
continue;
638 limit -= coeffs_[coeff_index];
640 if (coeffs_[coeff_index] >= limit)
break;
647 const Trail& trail,
int trail_index,
649 Coefficient result(0);
650 int literal_index = 0;
658 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
664 const Trail& trail, BooleanVariable
var,
666 Coefficient* conflict_slack) {
672 Coefficient var_coeff(0);
673 int literal_index = 0;
679 var_coeff = coeffs_[coeff_index];
685 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
712 const Coefficient slack = rhs_ -
activity;
722 const Coefficient cancelation =
731 const Coefficient min_coeffs =
std::min(var_coeff, conflict_var_coeff);
732 const Coefficient new_slack_ub = slack + *conflict_slack - min_coeffs;
733 CHECK_LT(*conflict_slack, conflict_var_coeff);
735 if (new_slack_ub < 0) {
737 DCHECK_EQ(*conflict_slack + slack - cancelation,
752 Coefficient conflict_diff(0);
755 if (new_slack_ub <
std::max(var_coeff, conflict_var_coeff) - min_coeffs) {
756 const Coefficient reduc = new_slack_ub + 1;
757 if (var_coeff < conflict_var_coeff) {
758 conflict_diff += reduc;
767 conflict_diff = *conflict_slack;
772 CHECK_LE(conflict_diff, *conflict_slack);
773 if (conflict_diff > 0) {
774 conflict->
ReduceSlackTo(trail, limit_trail_index, *conflict_slack,
775 *conflict_slack - conflict_diff);
776 *conflict_slack -= conflict_diff;
796 const Coefficient new_coeff = coeffs_[coeff_index] - diff;
804 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
813 const Coefficient slack = GetSlackFromThreshold(*threshold);
814 while (index_ + 1 < coeffs_.size() && coeffs_[index_ + 1] <= slack) ++index_;
815 Update(slack, threshold);
816 if (first_reason_trail_index_ >= trail_index) {
817 first_reason_trail_index_ = -1;
824 Coefficient rhs,
Trail* trail) {
827 DCHECK(std::is_sorted(cst.begin(), cst.end(), CoeffComparator));
830 if (constraints_.empty()) {
837 std::unique_ptr<UpperBoundedLinearConstraint> c(
839 std::vector<UpperBoundedLinearConstraint*>& duplicate_candidates =
840 possible_duplicates_[c->hash()];
844 if (candidate->HasIdenticalTerms(cst)) {
845 if (rhs < candidate->Rhs()) {
849 ConstraintIndex i(0);
850 while (i < constraints_.size() &&
851 constraints_[i.value()].get() != candidate) {
856 &thresholds_[i], trail,
867 trail, &enqueue_helper_)) {
872 const ConstraintIndex cst_index(constraints_.size());
873 duplicate_candidates.push_back(c.get());
874 constraints_.emplace_back(c.release());
877 to_update_[term.literal.Index()].
push_back(ConstraintIndexWithCoeff(
879 cst_index, term.coefficient));
885 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
Trail* trail) {
886 DeleteSomeLearnedConstraintIfNeeded();
887 const int old_num_constraints = constraints_.size();
892 if (result && constraints_.size() > old_num_constraints) {
893 constraints_.back()->set_is_learned(
true);
898 bool PbConstraints::PropagateNext(
Trail* trail) {
906 bool conflict =
false;
907 num_threshold_updates_ += to_update_[true_literal.
Index()].
size();
908 for (ConstraintIndexWithCoeff& update : to_update_[true_literal.
Index()]) {
909 const Coefficient threshold =
910 thresholds_[update.index] - update.coefficient;
911 thresholds_[update.index] = threshold;
912 if (threshold < 0 && !conflict) {
914 constraints_[update.index.value()].get();
915 update.need_untrail_inspection =
true;
916 ++num_constraint_lookups_;
918 if (!cst->
Propagate(source_trail_index, &thresholds_[update.index], trail,
921 conflicting_constraint_index_ = update.index;
927 num_inspected_constraint_literals_ +=
935 const int old_index = trail->
Index();
937 if (!PropagateNext(trail))
return false;
948 for (ConstraintIndexWithCoeff& update : to_update_[
literal.Index()]) {
949 thresholds_[update.index] += update.coefficient;
953 if (update.need_untrail_inspection) {
954 update.need_untrail_inspection =
false;
955 to_untrail_.
Set(update.index);
960 constraints_[cst_index.value()]->Untrail(&(thresholds_[cst_index]),
966 int trail_index)
const {
969 enqueue_helper_.
reasons[trail_index];
972 trail[trail_index].Variable(), reason);
977 int trail_index)
const {
979 enqueue_helper_.
reasons[trail_index];
986 void PbConstraints::ComputeNewLearnedConstraintLimit() {
987 const int num_constraints = constraints_.size();
988 target_number_of_learned_constraint_ =
989 num_constraints + parameters_->pb_cleanup_increment();
990 num_learned_constraint_before_cleanup_ =
991 static_cast<int>(target_number_of_learned_constraint_ /
992 parameters_->pb_cleanup_ratio()) -
996 void PbConstraints::DeleteSomeLearnedConstraintIfNeeded() {
997 if (num_learned_constraint_before_cleanup_ == 0) {
999 ComputeNewLearnedConstraintLimit();
1002 --num_learned_constraint_before_cleanup_;
1003 if (num_learned_constraint_before_cleanup_ > 0)
return;
1008 std::vector<double> activities;
1009 for (
int i = 0; i < constraints_.size(); ++i) {
1010 const UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1011 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1012 activities.push_back(constraint.activity());
1018 std::sort(activities.begin(), activities.end());
1019 const int num_constraints_to_delete =
1020 constraints_.size() - target_number_of_learned_constraint_;
1021 CHECK_GT(num_constraints_to_delete, 0);
1022 if (num_constraints_to_delete >= activities.size()) {
1025 for (
int i = 0; i < constraints_.size(); ++i) {
1026 UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1027 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1028 constraint.MarkForDeletion();
1032 const double limit_activity = activities[num_constraints_to_delete];
1033 int num_constraint_at_limit_activity = 0;
1034 for (
int i = num_constraints_to_delete; i >= 0; --i) {
1035 if (activities[i] == limit_activity) {
1036 ++num_constraint_at_limit_activity;
1046 for (
int i = constraints_.size() - 1; i >= 0; --i) {
1047 UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1048 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1049 if (constraint.activity() <= limit_activity) {
1050 if (constraint.activity() == limit_activity &&
1051 num_constraint_at_limit_activity > 0) {
1052 --num_constraint_at_limit_activity;
1054 constraint.MarkForDeletion();
1062 DeleteConstraintMarkedForDeletion();
1063 ComputeNewLearnedConstraintLimit();
1068 const double max_activity = parameters_->max_clause_activity_value();
1070 constraint_activity_increment_);
1071 if (constraint->
activity() > max_activity) {
1077 constraint_activity_increment_ *= scaling_factor;
1078 for (
int i = 0; i < constraints_.size(); ++i) {
1079 constraints_[i]->set_activity(constraints_[i]->activity() * scaling_factor);
1084 const double decay = parameters_->clause_activity_decay();
1085 constraint_activity_increment_ *= 1.0 / decay;
1088 void PbConstraints::DeleteConstraintMarkedForDeletion() {
1090 constraints_.size(), ConstraintIndex(-1));
1091 ConstraintIndex new_index(0);
1092 for (ConstraintIndex i(0); i < constraints_.size(); ++i) {
1093 if (!constraints_[i.value()]->is_marked_for_deletion()) {
1094 index_mapping[i] = new_index;
1095 if (new_index < i) {
1096 constraints_[new_index.value()] = std::move(constraints_[i.value()]);
1097 thresholds_[new_index] = thresholds_[i];
1102 UpperBoundedLinearConstraint* c = constraints_[i.value()].get();
1103 std::vector<UpperBoundedLinearConstraint*>& ref =
1104 possible_duplicates_[c->hash()];
1105 for (
int i = 0; i < ref.size(); ++i) {
1107 std::swap(ref[i], ref.back());
1114 constraints_.resize(new_index.value());
1115 thresholds_.
resize(new_index.value());
1119 for (LiteralIndex lit(0); lit < to_update_.
size(); ++lit) {
1120 std::vector<ConstraintIndexWithCoeff>& updates = to_update_[lit];
1122 for (
int i = 0; i < updates.size(); ++i) {
1123 const ConstraintIndex m = index_mapping[updates[i].index];
1125 updates[new_index] = updates[i];
1126 updates[new_index].index = m;
1130 updates.
resize(new_index);