14#ifndef OR_TOOLS_SAT_INTEGER_EXPR_H_
15#define OR_TOOLS_SAT_INTEGER_EXPR_H_
56 IntegerSumLE(
const std::vector<Literal>& enforcement_literals,
57 const std::vector<IntegerVariable>& vars,
58 const std::vector<IntegerValue>& coeffs,
78 void FillIntegerReason();
80 const std::vector<Literal> enforcement_literals_;
81 const IntegerValue upper_bound_;
89 bool is_registered_ =
false;
90 IntegerValue rev_lb_fixed_vars_;
93 int rev_num_fixed_vars_;
98 std::vector<IntegerVariable> vars_;
99 std::vector<IntegerValue> coeffs_;
100 std::vector<IntegerValue> max_variations_;
102 std::vector<Literal> literal_reason_;
105 std::vector<IntegerLiteral> integer_reason_;
106 std::vector<IntegerValue> reason_coeffs_;
122 const std::vector<IntegerVariable>& vars,
123 const std::vector<IntegerValue>& coeffs,
Model*
model);
128 const IntegerVariable target_;
129 const std::vector<IntegerVariable> vars_;
130 const std::vector<IntegerValue> coeffs_;
132 IntegerValue gcd_ = IntegerValue(1);
171 const std::vector<IntegerVariable> vars_;
172 const IntegerVariable min_var_;
175 std::vector<IntegerLiteral> integer_reason_;
197 bool PropagateLinearUpperBound(const
std::vector<IntegerVariable>& vars,
198 const
std::vector<IntegerValue>& coeffs,
199 IntegerValue upper_bound);
202 const IntegerVariable min_var_;
203 std::vector<IntegerValue> expr_lbs_;
207 int rev_unique_candidate_ = 0;
224 const IntegerVariable a_;
225 const IntegerVariable b_;
226 const IntegerVariable p_;
248 const IntegerVariable a_;
249 const IntegerVariable b_;
250 const IntegerVariable c_;
267 const IntegerVariable a_;
268 const IntegerValue b_;
269 const IntegerVariable c_;
286 const IntegerVariable x_;
287 const IntegerVariable s_;
298template <
typename VectorInt>
300 const std::vector<IntegerVariable>& vars,
const VectorInt&
coefficients,
304 if (vars.size() == 1) {
344 const int num_vars = vars.size();
345 if (num_vars > 100) {
346 std::vector<IntegerVariable> bucket_sum_vars;
348 std::vector<IntegerVariable> local_vars;
349 std::vector<IntegerValue> local_coeffs;
352 const int num_buckets =
static_cast<int>(std::round(std::sqrt(num_vars)));
353 for (
int b = 0;
b < num_buckets; ++
b) {
355 local_coeffs.clear();
358 const int limit = num_vars * (
b + 1);
359 for (; i * num_buckets < limit; ++i) {
360 local_vars.push_back(vars[i]);
364 bucket_lb +=
std::min(term1, term2);
365 bucket_ub +=
std::max(term1, term2);
368 const IntegerVariable bucket_sum =
370 bucket_sum_vars.push_back(bucket_sum);
371 local_vars.push_back(bucket_sum);
372 local_coeffs.push_back(IntegerValue(-1));
374 {}, local_vars, local_coeffs, IntegerValue(0),
model);
376 model->TakeOwnership(constraint);
381 local_coeffs.clear();
382 for (
const IntegerVariable
var : bucket_sum_vars) {
383 local_vars.push_back(
var);
384 local_coeffs.push_back(IntegerValue(1));
387 {}, local_vars, local_coeffs, IntegerValue(upper_bound),
model);
389 model->TakeOwnership(constraint);
396 IntegerValue(upper_bound),
model);
398 model->TakeOwnership(constraint);
403template <
typename VectorInt>
405 const std::vector<IntegerVariable>& vars,
const VectorInt&
coefficients,
409 for (
int64& ref : negated_coeffs) ref = -ref;
414template <
typename VectorInt>
416 const std::vector<IntegerVariable>& vars,
const VectorInt&
coefficients,
425template <
typename VectorInt>
427 const std::vector<Literal>& enforcement_literals,
428 const std::vector<IntegerVariable>& vars,
const VectorInt&
coefficients,
432 if (vars.size() == 1) {
436 enforcement_literals,
438 vars[0],
FloorRatio(IntegerValue(upper_bound),
442 enforcement_literals,
444 vars[0],
CeilRatio(IntegerValue(-upper_bound),
454 enforcement_literals);
463 enforcement_literals);
468 IntegerValue expression_min(0);
470 for (
int i = 0; i < vars.size(); ++i) {
473 ? integer_trail->LowerBound(vars[i])
474 : integer_trail->UpperBound(vars[i]));
476 if (expression_min == upper_bound) {
480 IntegerValue non_cached_min;
481 for (
int i = 0; i < vars.size(); ++i) {
483 const IntegerValue lb = integer_trail->LowerBound(vars[i]);
488 const IntegerValue ub = integer_trail->UpperBound(vars[i]);
494 if (non_cached_min > expression_min) {
495 std::vector<Literal> clause;
496 for (
const Literal l : enforcement_literals) {
497 clause.push_back(l.Negated());
503 enforcement_literals, vars,
505 IntegerValue(upper_bound),
model);
507 model->TakeOwnership(constraint);
513template <
typename VectorInt>
515 const std::vector<Literal>& enforcement_literals,
516 const std::vector<IntegerVariable>& vars,
const VectorInt&
coefficients,
520 for (
int64& ref : negated_coeffs) ref = -ref;
522 negated_coeffs, -lower_bound);
526template <
typename VectorInt>
528 Literal is_le,
const std::vector<IntegerVariable>& vars,
539template <
typename VectorInt>
541 Literal is_ge,
const std::vector<IntegerVariable>& vars,
553 if (cst.
vars.empty()) {
554 if (cst.
lb <= 0 && cst.
ub >= 0)
return;
560 std::vector<int64> converted_coeffs;
561 for (
const IntegerValue v : cst.
coeffs) converted_coeffs.push_back(v.value());
573 const absl::Span<const Literal> enforcement_literals,
575 if (enforcement_literals.empty()) {
578 if (cst.
vars.empty()) {
579 if (cst.
lb <= 0 && cst.
ub >= 0)
return;
584 std::vector<Literal> converted_literals(enforcement_literals.begin(),
585 enforcement_literals.end());
586 std::vector<int64> converted_coeffs;
587 for (
const IntegerValue v : cst.
coeffs) converted_coeffs.push_back(v.value());
591 converted_literals, cst.
vars, converted_coeffs, cst.
ub.value()));
595 converted_literals, cst.
vars, converted_coeffs, cst.
lb.value()));
601template <
typename VectorInt>
603 Literal is_eq,
const std::vector<IntegerVariable>& vars,
618template <
typename VectorInt>
620 const std::vector<IntegerVariable>& vars,
const VectorInt&
coefficients,
640template <
typename VectorInt>
642 const VectorInt&
coefficients,
const std::vector<IntegerVariable>& vars) {
644 std::vector<IntegerVariable> new_vars = vars;
651 for (
int i = 0; i < new_vars.size(); ++i) {
662 new_vars.push_back(sum);
664 new_coeffs.push_back(-1);
673 IntegerVariable min_var,
const std::vector<IntegerVariable>& vars) {
675 for (
const IntegerVariable&
var : vars) {
682 model->TakeOwnership(constraint);
691 const std::vector<LinearExpression>& exprs) {
695 IntegerVariable min_var;
696 if (min_expr.
vars.size() == 1 &&
697 std::abs(min_expr.
coeffs[0].value()) == 1) {
698 if (min_expr.
coeffs[0].value() == 1) {
699 min_var = min_expr.
vars[0];
710 std::vector<IntegerVariable> min_sum_vars = min_expr.
vars;
711 std::vector<int64> min_sum_coeffs;
712 for (IntegerValue coeff : min_expr.
coeffs) {
713 min_sum_coeffs.push_back(coeff.value());
715 min_sum_vars.push_back(min_var);
716 min_sum_coeffs.push_back(-1);
719 -min_expr.
offset.value()));
723 std::vector<IntegerVariable> vars = expr.vars;
724 std::vector<int64> coeffs;
725 for (IntegerValue coeff : expr.coeffs) {
726 coeffs.push_back(coeff.value());
728 vars.push_back(min_var);
729 coeffs.push_back(-1);
735 model->TakeOwnership(constraint);
742 IntegerVariable max_var,
const std::vector<IntegerVariable>& vars) {
744 std::vector<IntegerVariable> negated_vars;
745 for (
const IntegerVariable&
var : vars) {
753 model->TakeOwnership(constraint);
759std::function<void(Model*)>
IsOneOf(IntegerVariable
var,
760 const std::vector<Literal>& selectors,
761 const std::vector<IntegerValue>& values);
818 model->TakeOwnership(constraint);
833 model->TakeOwnership(constraint);
#define CHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
void RegisterWith(GenericLiteralWatcher *watcher)
bool PropagateAtLevelZero()
IntegerSumLE(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, IntegerValue upper_bound, Model *model)
IntegerVariable AddIntegerVariable(IntegerValue lower_bound, IntegerValue upper_bound)
LevelZeroEquality(IntegerVariable target, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, Model *model)
LinMinPropagator & operator=(const LinMinPropagator &)=delete
LinMinPropagator(const std::vector< LinearExpression > &exprs, IntegerVariable min_var, Model *model)
LinMinPropagator(const LinMinPropagator &)=delete
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterWith(GenericLiteralWatcher *watcher)
MinPropagator(const std::vector< IntegerVariable > &vars, IntegerVariable min_var, IntegerTrail *integer_trail)
Class that owns everything related to a particular optimization model.
#define DISALLOW_COPY_AND_ASSIGN(TypeName)
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> ConditionalSum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub, const std::vector< Literal > &enforcement_literals)
std::function< void(Model *)> Sum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub)
std::function< void(Model *)> ConditionalWeightedSumLowerOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
std::function< IntegerVariable(Model *)> NewWeightedSum(const VectorInt &coefficients, const std::vector< IntegerVariable > &vars)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
void RegisterAndTransferOwnership(Model *model, T *ct)
std::function< void(Model *)> ProductConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable p)
std::function< void(Model *)> IsEqualToMinOf(IntegerVariable min_var, const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
std::function< void(Model *)> FixedDivisionConstraint(IntegerVariable a, IntegerValue b, IntegerVariable c)
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> WeightedSumGreaterOrEqualReif(Literal is_ge, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
std::function< void(Model *)> ConditionalSum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub, const std::vector< Literal > &enforcement_literals)
std::function< void(Model *)> FixedWeightedSum(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::function< void(Model *)> ConditionalWeightedSumGreaterOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
std::function< void(Model *)> Sum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> DivisionConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable c)
std::function< void(Model *)> WeightedSumLowerOrEqualReif(Literal is_le, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< void(Model *)> FixedWeightedSumReif(Literal is_eq, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::function< void(Model *)> WeightedSumNotEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< void(Model *)> IsEqualToMaxOf(IntegerVariable max_var, const std::vector< IntegerVariable > &vars)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::vector< double > coefficients
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars