18 #include "absl/strings/str_format.h"
28 bool LiteralComparator(
const LiteralWithCoeff&
a,
const LiteralWithCoeff&
b) {
29 return a.literal.Index() <
b.literal.Index();
32 bool CoeffComparator(
const LiteralWithCoeff&
a,
const LiteralWithCoeff&
b) {
33 if (
a.coefficient ==
b.coefficient) {
34 return a.literal.Index() <
b.literal.Index();
36 return a.coefficient <
b.coefficient;
42 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
43 Coefficient* max_value) {
51 std::sort(cst->begin(), cst->end(), LiteralComparator);
54 for (
int i = 0; i < cst->size(); ++i) {
75 (*cst)[
index] = current;
87 for (
int i = 0; i < cst->size(); ++i) {
98 std::sort(cst->begin(), cst->end(), CoeffComparator);
105 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
106 Coefficient* max_value) {
108 Coefficient shift_due_to_fixed_variables(0);
110 if (mapping[entry.literal.Index()] >= 0) {
115 if (!
SafeAddInto(-entry.coefficient, &shift_due_to_fixed_variables)) {
125 *bound_shift = shift_due_to_fixed_variables;
131 if (!
SafeAddInto(shift_due_to_fixed_variables, bound_shift))
return false;
137 const std::vector<LiteralWithCoeff>& cst) {
138 Coefficient previous(1);
140 if (term.coefficient < previous)
return false;
141 previous = term.coefficient;
149 std::vector<LiteralWithCoeff>* cst, Coefficient* rhs) {
156 if (x.coefficient > *rhs) x.coefficient = *rhs + 1;
161 Coefficient bound_shift,
162 Coefficient max_value) {
163 Coefficient rhs = upper_bound;
165 if (bound_shift > 0) {
171 return Coefficient(-1);
174 if (rhs < 0)
return Coefficient(-1);
179 Coefficient bound_shift,
180 Coefficient max_value) {
183 Coefficient shifted_lb = lower_bound;
185 if (bound_shift > 0) {
187 return Coefficient(-1);
193 if (shifted_lb <= 0) {
198 return max_value - shifted_lb;
202 bool use_lower_bound, Coefficient lower_bound,
bool use_upper_bound,
203 Coefficient upper_bound, std::vector<LiteralWithCoeff>* cst) {
205 Coefficient bound_shift;
206 Coefficient max_value;
211 if (use_upper_bound) {
212 const Coefficient rhs =
214 if (!AddConstraint(*cst, max_value, rhs))
return false;
216 if (use_lower_bound) {
218 for (
int i = 0; i < cst->size(); ++i) {
219 (*cst)[i].literal = (*cst)[i].literal.Negated();
221 const Coefficient rhs =
223 if (!AddConstraint(*cst, max_value, rhs))
return false;
228 bool CanonicalBooleanLinearProblem::AddConstraint(
229 const std::vector<LiteralWithCoeff>& cst, Coefficient max_value,
231 if (rhs < 0)
return false;
232 if (rhs >= max_value)
return true;
233 constraints_.emplace_back(cst.begin(), cst.end());
240 if (terms_.
size() != num_variables) {
241 terms_.
assign(num_variables, Coefficient(0));
253 terms_[
var] = Coefficient(0);
262 CHECK_LT(rhs_, max_sum_) <<
"Trivially sat.";
263 Coefficient removed_sum(0);
264 const Coefficient
bound = max_sum_ - rhs_;
273 max_sum_ -= removed_sum;
280 if (!result.empty()) result +=
" + ";
284 result += absl::StrFormat(
" <= %d", rhs_.value());
291 const Trail& trail,
int trail_index)
const {
292 Coefficient activity(0);
300 return rhs_ - activity;
306 Coefficient activity(0);
307 Coefficient removed_sum(0);
308 const Coefficient
bound = max_sum_ - rhs_;
328 max_sum_ -= removed_sum;
330 return rhs_ - activity;
334 const Trail& trail,
int trail_index, Coefficient initial_slack,
335 Coefficient target) {
337 const Coefficient slack = initial_slack;
344 const Coefficient coeff =
GetCoefficient(trail[trail_index].Variable());
348 if (slack == target)
return;
351 const Coefficient diff = slack - target;
360 terms_[
var] = (terms_[
var] > 0) ? terms_[
var] - diff : terms_[
var] + diff;
371 std::vector<LiteralWithCoeff>* output) {
379 std::sort(output->begin(), output->end(), CoeffComparator);
382 Coefficient MutableUpperBoundedLinearConstraint::ComputeMaxSum()
const {
383 Coefficient result(0);
391 const std::vector<LiteralWithCoeff>& cst)
392 : is_marked_for_deletion_(false),
394 first_reason_trail_index_(-1),
397 DCHECK(std::is_sorted(cst.begin(), cst.end(), CoeffComparator));
398 literals_.reserve(cst.size());
405 if (term.coefficient != prev) {
406 prev = term.coefficient;
410 coeffs_.reserve(size);
411 starts_.reserve(size + 1);
416 if (term.coefficient != prev) {
417 prev = term.coefficient;
418 coeffs_.push_back(term.coefficient);
419 starts_.push_back(literals_.size());
421 literals_.push_back(term.literal);
425 starts_.push_back(literals_.size());
427 hash_ =
ThoroughHash(
reinterpret_cast<const char*
>(cst.data()),
433 int literal_index = 0;
438 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
444 const std::vector<LiteralWithCoeff>& cst) {
445 if (cst.size() != literals_.size())
return false;
446 int literal_index = 0;
449 if (literals_[literal_index] != term.literal)
return false;
450 if (coeffs_[coeff_index] != term.coefficient)
return false;
452 if (literal_index == starts_[coeff_index + 1]) {
460 Coefficient rhs,
int trail_index, Coefficient* threshold,
Trail* trail,
466 Coefficient slack = rhs;
472 std::vector<Coefficient> sum_at_previous_level(last_level + 2,
475 int max_relevant_trail_index = 0;
476 if (trail_index > 0) {
477 int literal_index = 0;
480 const BooleanVariable
var =
literal.Variable();
481 const Coefficient coeff = coeffs_[coeff_index];
484 max_relevant_trail_index =
487 sum_at_previous_level[trail->
Info(
var).
level + 1] += coeff;
490 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
494 if (slack < 0)
return false;
497 for (
int i = 1; i < sum_at_previous_level.size(); ++i) {
498 sum_at_previous_level[i] += sum_at_previous_level[i - 1];
503 int literal_index = 0;
506 const BooleanVariable
var =
literal.Variable();
511 CHECK_LE(coeffs_[coeff_index], rhs_ - sum_at_previous_level[level])
512 <<
"var should have been propagated at an earlier level !";
515 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
525 index_ = coeffs_.size() - 1;
526 already_propagated_end_ = literals_.size();
527 Update(slack, threshold);
528 return *threshold < 0
529 ?
Propagate(max_relevant_trail_index, threshold, trail, helper)
534 int trail_index, Coefficient* threshold,
Trail* trail,
537 const Coefficient slack = GetSlackFromThreshold(*threshold);
538 DCHECK_GE(slack, 0) <<
"The constraint is already a conflict!";
539 while (index_ >= 0 && coeffs_[index_] > slack) --index_;
542 BooleanVariable first_propagated_variable(-1);
543 for (
int i = starts_[index_ + 1]; i < already_propagated_end_; ++i) {
548 FillReason(*trail, trail_index, literals_[i].Variable(),
550 helper->
conflict.push_back(literals_[i].Negated());
551 Update(slack, threshold);
556 if (first_propagated_variable < 0) {
557 if (first_reason_trail_index_ == -1) {
558 first_reason_trail_index_ = trail->
Index();
560 helper->
Enqueue(literals_[i].Negated(), trail_index,
this, trail);
561 first_propagated_variable = literals_[i].Variable();
567 first_propagated_variable);
571 Update(slack, threshold);
577 const Trail& trail,
int source_trail_index,
578 BooleanVariable propagated_variable, std::vector<Literal>* reason) {
584 reason->push_back(trail[source_trail_index].Negated());
591 int last_coeff_index = 0;
597 Coefficient slack = rhs_;
598 Coefficient propagated_variable_coefficient(0);
599 int coeff_index = coeffs_.size() - 1;
600 for (
int i = literals_.size() - 1; i >= 0; --i) {
602 if (
literal.Variable() == propagated_variable) {
603 propagated_variable_coefficient = coeffs_[coeff_index];
608 reason->push_back(
literal.Negated());
610 last_coeff_index = coeff_index;
612 slack -= coeffs_[coeff_index];
615 if (i == starts_[coeff_index]) {
619 DCHECK_GT(propagated_variable_coefficient, slack);
620 DCHECK_GE(propagated_variable_coefficient, 0);
623 if (reason->size() <= 1 || coeffs_.size() == 1)
return;
625 Coefficient limit = propagated_variable_coefficient - slack;
630 coeff_index = last_coeff_index;
631 if (coeffs_[coeff_index] >= limit)
return;
632 for (
int i = last_i; i < literals_.size(); ++i) {
634 if (i == starts_[coeff_index + 1]) {
636 if (coeffs_[coeff_index] >= limit)
break;
638 if (
literal.Negated() != reason->back())
continue;
639 limit -= coeffs_[coeff_index];
641 if (coeffs_[coeff_index] >= limit)
break;
648 const Trail& trail,
int trail_index,
650 Coefficient result(0);
651 int literal_index = 0;
659 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
665 const Trail& trail, BooleanVariable
var,
667 Coefficient* conflict_slack) {
673 Coefficient var_coeff(0);
674 int literal_index = 0;
680 var_coeff = coeffs_[coeff_index];
686 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
713 const Coefficient slack = rhs_ -
activity;
723 const Coefficient cancelation =
732 const Coefficient min_coeffs =
std::min(var_coeff, conflict_var_coeff);
733 const Coefficient new_slack_ub = slack + *conflict_slack - min_coeffs;
734 CHECK_LT(*conflict_slack, conflict_var_coeff);
736 if (new_slack_ub < 0) {
738 DCHECK_EQ(*conflict_slack + slack - cancelation,
753 Coefficient conflict_diff(0);
756 if (new_slack_ub <
std::max(var_coeff, conflict_var_coeff) - min_coeffs) {
757 const Coefficient reduc = new_slack_ub + 1;
758 if (var_coeff < conflict_var_coeff) {
759 conflict_diff += reduc;
768 conflict_diff = *conflict_slack;
773 CHECK_LE(conflict_diff, *conflict_slack);
774 if (conflict_diff > 0) {
775 conflict->
ReduceSlackTo(trail, limit_trail_index, *conflict_slack,
776 *conflict_slack - conflict_diff);
777 *conflict_slack -= conflict_diff;
797 const Coefficient new_coeff = coeffs_[coeff_index] - diff;
805 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
814 const Coefficient slack = GetSlackFromThreshold(*threshold);
815 while (index_ + 1 < coeffs_.size() && coeffs_[index_ + 1] <= slack) ++index_;
816 Update(slack, threshold);
817 if (first_reason_trail_index_ >= trail_index) {
818 first_reason_trail_index_ = -1;
825 Coefficient rhs,
Trail* trail) {
828 DCHECK(std::is_sorted(cst.begin(), cst.end(), CoeffComparator));
831 if (constraints_.empty()) {
838 std::unique_ptr<UpperBoundedLinearConstraint> c(
840 std::vector<UpperBoundedLinearConstraint*>& duplicate_candidates =
841 possible_duplicates_[c->hash()];
845 if (candidate->HasIdenticalTerms(cst)) {
846 if (rhs < candidate->Rhs()) {
850 ConstraintIndex i(0);
851 while (i < constraints_.size() &&
852 constraints_[i.value()].get() != candidate) {
857 &thresholds_[i], trail,
868 trail, &enqueue_helper_)) {
873 const ConstraintIndex cst_index(constraints_.size());
874 duplicate_candidates.push_back(c.get());
875 constraints_.emplace_back(c.release());
878 to_update_[term.literal.Index()].
push_back(ConstraintIndexWithCoeff(
880 cst_index, term.coefficient));
886 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
Trail* trail) {
887 DeleteSomeLearnedConstraintIfNeeded();
888 const int old_num_constraints = constraints_.size();
893 if (result && constraints_.size() > old_num_constraints) {
894 constraints_.back()->set_is_learned(
true);
899 bool PbConstraints::PropagateNext(
Trail* trail) {
907 bool conflict =
false;
908 num_threshold_updates_ += to_update_[true_literal.
Index()].
size();
909 for (ConstraintIndexWithCoeff& update : to_update_[true_literal.
Index()]) {
910 const Coefficient threshold =
911 thresholds_[update.index] - update.coefficient;
912 thresholds_[update.index] = threshold;
913 if (threshold < 0 && !conflict) {
915 constraints_[update.index.value()].get();
916 update.need_untrail_inspection =
true;
917 ++num_constraint_lookups_;
919 if (!cst->
Propagate(source_trail_index, &thresholds_[update.index], trail,
922 conflicting_constraint_index_ = update.index;
928 num_inspected_constraint_literals_ +=
936 const int old_index = trail->
Index();
938 if (!PropagateNext(trail))
return false;
949 for (ConstraintIndexWithCoeff& update : to_update_[
literal.Index()]) {
950 thresholds_[update.index] += update.coefficient;
954 if (update.need_untrail_inspection) {
955 update.need_untrail_inspection =
false;
956 to_untrail_.
Set(update.index);
961 constraints_[cst_index.value()]->Untrail(&(thresholds_[cst_index]),
967 int trail_index)
const {
970 enqueue_helper_.
reasons[trail_index];
973 trail[trail_index].Variable(), reason);
978 int trail_index)
const {
980 enqueue_helper_.
reasons[trail_index];
987 void PbConstraints::ComputeNewLearnedConstraintLimit() {
988 const int num_constraints = constraints_.size();
989 target_number_of_learned_constraint_ =
990 num_constraints + parameters_->pb_cleanup_increment();
991 num_learned_constraint_before_cleanup_ =
992 static_cast<int>(target_number_of_learned_constraint_ /
993 parameters_->pb_cleanup_ratio()) -
997 void PbConstraints::DeleteSomeLearnedConstraintIfNeeded() {
998 if (num_learned_constraint_before_cleanup_ == 0) {
1000 ComputeNewLearnedConstraintLimit();
1003 --num_learned_constraint_before_cleanup_;
1004 if (num_learned_constraint_before_cleanup_ > 0)
return;
1009 std::vector<double> activities;
1010 for (
int i = 0; i < constraints_.size(); ++i) {
1011 const UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1012 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1013 activities.push_back(constraint.activity());
1019 std::sort(activities.begin(), activities.end());
1020 const int num_constraints_to_delete =
1021 constraints_.size() - target_number_of_learned_constraint_;
1022 CHECK_GT(num_constraints_to_delete, 0);
1023 if (num_constraints_to_delete >= activities.size()) {
1026 for (
int i = 0; i < constraints_.size(); ++i) {
1027 UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1028 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1029 constraint.MarkForDeletion();
1033 const double limit_activity = activities[num_constraints_to_delete];
1034 int num_constraint_at_limit_activity = 0;
1035 for (
int i = num_constraints_to_delete; i >= 0; --i) {
1036 if (activities[i] == limit_activity) {
1037 ++num_constraint_at_limit_activity;
1047 for (
int i = constraints_.size() - 1; i >= 0; --i) {
1048 UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1049 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1050 if (constraint.activity() <= limit_activity) {
1051 if (constraint.activity() == limit_activity &&
1052 num_constraint_at_limit_activity > 0) {
1053 --num_constraint_at_limit_activity;
1055 constraint.MarkForDeletion();
1063 DeleteConstraintMarkedForDeletion();
1064 ComputeNewLearnedConstraintLimit();
1069 const double max_activity = parameters_->max_clause_activity_value();
1071 constraint_activity_increment_);
1072 if (constraint->
activity() > max_activity) {
1078 constraint_activity_increment_ *= scaling_factor;
1079 for (
int i = 0; i < constraints_.size(); ++i) {
1080 constraints_[i]->set_activity(constraints_[i]->activity() * scaling_factor);
1085 const double decay = parameters_->clause_activity_decay();
1086 constraint_activity_increment_ *= 1.0 / decay;
1089 void PbConstraints::DeleteConstraintMarkedForDeletion() {
1091 constraints_.size(), ConstraintIndex(-1));
1092 ConstraintIndex new_index(0);
1093 for (ConstraintIndex i(0); i < constraints_.size(); ++i) {
1094 if (!constraints_[i.value()]->is_marked_for_deletion()) {
1095 index_mapping[i] = new_index;
1096 if (new_index < i) {
1097 constraints_[new_index.value()] = std::move(constraints_[i.value()]);
1098 thresholds_[new_index] = thresholds_[i];
1103 UpperBoundedLinearConstraint* c = constraints_[i.value()].get();
1104 std::vector<UpperBoundedLinearConstraint*>& ref =
1105 possible_duplicates_[c->hash()];
1106 for (
int i = 0; i < ref.size(); ++i) {
1108 std::swap(ref[i], ref.back());
1115 constraints_.resize(new_index.value());
1116 thresholds_.
resize(new_index.value());
1120 for (LiteralIndex lit(0); lit < to_update_.
size(); ++lit) {
1121 std::vector<ConstraintIndexWithCoeff>& updates = to_update_[lit];
1123 for (
int i = 0; i < updates.size(); ++i) {
1124 const ConstraintIndex m = index_mapping[updates[i].index];
1126 updates[new_index] = updates[i];
1127 updates[new_index].index = m;
1131 updates.
resize(new_index);
#define CHECK_LT(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)
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
void push_back(const value_type &x)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
void Set(IntegerType index)
void ClearAndResize(IntegerType size)
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
LiteralIndex Index() const
BooleanVariable Variable() const
void ReduceCoefficients()
Literal GetLiteral(BooleanVariable var) const
Coefficient ComputeSlackForTrailPrefix(const Trail &trail, int trail_index) const
Coefficient ReduceCoefficientsAndComputeSlackForTrailPrefix(const Trail &trail, int trail_index)
void ReduceSlackTo(const Trail &trail, int trail_index, Coefficient initial_slack, Coefficient target)
const std::vector< BooleanVariable > & PossibleNonZeros() const
std::string DebugString()
Coefficient CancelationAmount(Literal literal, Coefficient coeff) const
void AddTerm(Literal literal, Coefficient coeff)
void AddToRhs(Coefficient value)
void ClearAndResize(int num_variables)
void CopyIntoVector(std::vector< LiteralWithCoeff > *output)
Coefficient GetCoefficient(BooleanVariable var) const
bool Propagate(Trail *trail) final
void RescaleActivities(double scaling_factor)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
bool AddConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
UpperBoundedLinearConstraint * ReasonPbConstraint(int trail_index) const
void UpdateActivityIncrement()
void BumpActivity(UpperBoundedLinearConstraint *constraint)
void Untrail(const Trail &trail, int trail_index) final
bool AddLearnedConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
int propagation_trail_index_
const AssignmentInfo & Info(BooleanVariable var) const
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
std::vector< Literal > * MutableConflict()
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
void set_activity(double activity)
Coefficient ComputeCancelation(const Trail &trail, int trail_index, const MutableUpperBoundedLinearConstraint &conflict)
bool Propagate(int trail_index, Coefficient *threshold, Trail *trail, PbConstraintsEnqueueHelper *helper)
void FillReason(const Trail &trail, int source_trail_index, BooleanVariable propagated_variable, std::vector< Literal > *reason)
bool HasIdenticalTerms(const std::vector< LiteralWithCoeff > &cst)
void ResolvePBConflict(const Trail &trail, BooleanVariable var, MutableUpperBoundedLinearConstraint *conflict, Coefficient *conflict_slack)
bool InitializeRhs(Coefficient rhs, int trail_index, Coefficient *threshold, Trail *trail, PbConstraintsEnqueueHelper *helper)
int already_propagated_end() const
void Untrail(Coefficient *threshold, int trail_index)
void AddToConflict(MutableUpperBoundedLinearConstraint *conflict)
UpperBoundedLinearConstraint(const std::vector< LiteralWithCoeff > &cst)
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
bool ApplyLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound, Coefficient bound_shift, Coefficient max_value)
void SimplifyCanonicalBooleanLinearConstraint(std::vector< LiteralWithCoeff > *cst, Coefficient *rhs)
const LiteralIndex kTrueLiteralIndex(-2)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
const LiteralIndex kFalseLiteralIndex(-3)
bool BooleanLinearExpressionIsCanonical(const std::vector< LiteralWithCoeff > &cst)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
uint64 ThoroughHash(const char *bytes, size_t len)
bool SafeAddInto(IntegerType a, IntegerType *b)
#define SCOPED_TIME_STAT(stats)
UpperBoundedLinearConstraint * pb_constraint
std::vector< ReasonInfo > reasons
void Enqueue(Literal l, int source_trail_index, UpperBoundedLinearConstraint *ct, Trail *trail)
std::vector< Literal > conflict