14#ifndef OR_TOOLS_SAT_PB_CONSTRAINT_H_
15#define OR_TOOLS_SAT_PB_CONSTRAINT_H_
23#include "absl/container/flat_hash_map.h"
24#include "absl/types/span.h"
32#include "ortools/sat/sat_parameters.pb.h"
82 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
83 Coefficient* max_value);
97 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
98 Coefficient* max_value);
108 Coefficient bound_shift, Coefficient max_value);
116 Coefficient bound_shift,
117 Coefficient max_value);
121 const std::vector<LiteralWithCoeff>& cst);
126 std::vector<LiteralWithCoeff>* cst, Coefficient* rhs);
151 bool use_upper_bound, Coefficient upper_bound,
152 std::vector<LiteralWithCoeff>* cst);
156 const Coefficient
Rhs(
int i)
const {
return rhs_[i]; }
157 const std::vector<LiteralWithCoeff>&
Constraint(
int i)
const {
158 return constraints_[i];
162 bool AddConstraint(
const std::vector<LiteralWithCoeff>& cst,
163 Coefficient max_value, Coefficient rhs);
165 std::vector<Coefficient> rhs_;
166 std::vector<std::vector<LiteralWithCoeff>> constraints_;
185 return AbsCoefficient(terms_[
var]);
209 const Coefficient
bound = max_sum_ - rhs_;
221 int trail_index)
const;
233 const Trail& trail,
int trail_index);
258 Coefficient initial_slack, Coefficient target);
268 Coefficient
Rhs()
const {
return rhs_; }
269 Coefficient
MaxSum()
const {
return max_sum_; }
275 const BooleanVariable
var =
literal.Variable();
276 const Coefficient term_encoding =
literal.IsPositive() ? coeff : -coeff;
283 rhs_ -=
std::min(coeff, AbsCoefficient(terms_[
var]));
284 max_sum_ += AbsCoefficient(term_encoding + terms_[
var]) -
285 AbsCoefficient(terms_[
var]);
290 CHECK_GE(max_sum_, 0) <<
"Overflow";
291 terms_[
var] += term_encoding;
298 const BooleanVariable
var =
literal.Variable();
300 return std::min(coeff, AbsCoefficient(terms_[
var]));
313 Coefficient AbsCoefficient(Coefficient
a)
const {
return a > 0 ?
a : -
a; }
316 Coefficient ComputeMaxSum()
const;
328 Coefficient max_sum_;
336class UpperBoundedLinearConstraint;
377 const std::vector<LiteralWithCoeff>& cst);
381 Coefficient
Rhs()
const {
return rhs_; }
389 bool InitializeRhs(Coefficient rhs,
int trail_index, Coefficient* threshold,
405 bool Propagate(
int trail_index, Coefficient* threshold,
Trail* trail,
412 void Untrail(Coefficient* threshold,
int trail_index);
430 BooleanVariable propagated_variable,
431 std::vector<Literal>* reason);
437 Coefficient* conflict_slack);
452 const Trail& trail,
int trail_index,
479 Coefficient GetSlackFromThreshold(Coefficient threshold) {
480 return (index_ < 0) ? threshold : coeffs_[index_] + threshold;
482 void Update(Coefficient slack, Coefficient* threshold) {
483 *threshold = (index_ < 0) ? slack : slack - coeffs_[index_];
484 already_propagated_end_ = starts_[index_ + 1];
489 bool is_marked_for_deletion_;
491 int first_reason_trail_index_;
496 int already_propagated_end_;
505 std::vector<Coefficient> coeffs_;
506 std::vector<int> starts_;
507 std::vector<Literal> literals_;
519 conflicting_constraint_index_(-1),
520 num_learned_constraint_before_cleanup_(0),
521 constraint_activity_increment_(1.0),
522 parameters_(
model->GetOrCreate<SatParameters>()),
523 stats_(
"PbConstraints"),
524 num_constraint_lookups_(0),
525 num_inspected_constraint_literals_(0),
526 num_threshold_updates_(0) {
527 model->GetOrCreate<
Trail>()->RegisterPropagator(
this);
532 LOG(
INFO) <<
"num_constraint_lookups_: " << num_constraint_lookups_;
533 LOG(
INFO) <<
"num_threshold_updates_: " << num_threshold_updates_;
538 void Untrail(
const Trail& trail,
int trail_index)
final;
539 absl::Span<const Literal>
Reason(
const Trail& trail,
540 int trail_index)
const final;
547 if (!constraints_.empty()) {
548 to_update_.
resize(num_variables << 1);
549 enqueue_helper_.
reasons.resize(num_variables);
563 bool AddConstraint(
const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
569 Coefficient rhs,
Trail* trail);
581 if (conflicting_constraint_index_ == -1)
return nullptr;
582 return constraints_[conflicting_constraint_index_.value()].get();
597 constraints_[
index]->MarkForDeletion();
598 DeleteConstraintMarkedForDeletion();
604 return num_inspected_constraint_literals_;
609 bool PropagateNext(
Trail* trail);
613 void ComputeNewLearnedConstraintLimit();
614 void DeleteSomeLearnedConstraintIfNeeded();
619 void DeleteConstraintMarkedForDeletion();
628 DEFINE_INT_TYPE(ConstraintIndex,
int32);
629 struct ConstraintIndexWithCoeff {
630 ConstraintIndexWithCoeff() {}
631 ConstraintIndexWithCoeff(
bool n, ConstraintIndex i, Coefficient c)
633 bool need_untrail_inspection;
634 ConstraintIndex
index;
639 std::vector<std::unique_ptr<UpperBoundedLinearConstraint>> constraints_;
650 SparseBitset<ConstraintIndex> to_untrail_;
654 absl::flat_hash_map<int64, std::vector<UpperBoundedLinearConstraint*>>
655 possible_duplicates_;
658 PbConstraintsEnqueueHelper enqueue_helper_;
662 ConstraintIndex conflicting_constraint_index_;
665 int target_number_of_learned_constraint_;
666 int num_learned_constraint_before_cleanup_;
667 double constraint_activity_increment_;
670 SatParameters* parameters_;
673 mutable StatsGroup stats_;
674 int64 num_constraint_lookups_;
675 int64 num_inspected_constraint_literals_;
676 int64 num_threshold_updates_;
693 first_variable_.
resize(num_variables);
704 if (seen_[
var])
return first_variable_[
var];
705 const BooleanVariable reference_var =
707 if (reference_var ==
var)
return var;
708 if (seen_[reference_var])
return first_variable_[reference_var];
709 seen_.
Set(reference_var);
710 first_variable_[reference_var] =
var;
#define CHECK_GE(val1, val2)
#define CHECK_GT(val1, val2)
#define DCHECK_GT(val1, val2)
void resize(size_type new_size)
void Set(IntegerType index)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
void ClearAndResize(IntegerType size)
std::string StatString() const
int NumConstraints() const
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
const std::vector< LiteralWithCoeff > & Constraint(int i) const
CanonicalBooleanLinearProblem()
const Coefficient Rhs(int i) const
LiteralIndex Index() const
std::string DebugString() const
Class that owns everything related to a particular optimization model.
void ReduceCoefficients()
Coefficient MaxSum() const
Literal GetLiteral(BooleanVariable var) const
const std::vector< BooleanVariable > & PossibleNonZeros() 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)
std::string DebugString()
Coefficient CancelationAmount(Literal literal, Coefficient coeff) const
void ReduceGivenCoefficient(BooleanVariable var)
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
int NumberOfConstraints() const
bool Propagate(Trail *trail) final
~PbConstraints() override
void RescaleActivities(double scaling_factor)
int64 num_threshold_updates() const
void ClearConflictingConstraint()
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 * ConflictingConstraint()
int64 num_inspected_constraint_literals() const
int64 num_constraint_lookups() const
void DeleteConstraint(int index)
PbConstraints(Model *model)
UpperBoundedLinearConstraint * ReasonPbConstraint(int trail_index) const
void UpdateActivityIncrement()
void BumpActivity(UpperBoundedLinearConstraint *constraint)
void Untrail(const Trail &trail, int trail_index) final
void Resize(int num_variables)
bool AddLearnedConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
void Enqueue(Literal true_literal, int propagator_id)
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) 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 set_is_learned(bool is_learned)
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 is_used_as_a_reason() const
bool is_marked_for_deletion() const
BooleanVariable FirstVariableWithSameReason(BooleanVariable var)
VariableWithSameReasonIdentifier(const Trail &trail)
void Resize(int num_variables)
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
DEFINE_INT_TYPE(ClauseIndex, int)
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)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
bool BooleanLinearExpressionIsCanonical(const std::vector< LiteralWithCoeff > &cst)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
#define IF_STATS_ENABLED(instructions)
LiteralWithCoeff(Literal l, int64 c)
bool operator==(const LiteralWithCoeff &other) const
LiteralWithCoeff(Literal l, Coefficient c)
UpperBoundedLinearConstraint * pb_constraint
std::vector< ReasonInfo > reasons
void Enqueue(Literal l, int source_trail_index, UpperBoundedLinearConstraint *ct, Trail *trail)
std::vector< Literal > conflict