2021-04-01 21:00:53 +02:00
|
|
|
// Copyright 2010-2021 Google LLC
|
2016-09-12 13:51:04 +02:00
|
|
|
// Licensed under the Apache License, Version 2.0 (the "License");
|
|
|
|
|
// you may not use this file except in compliance with the License.
|
|
|
|
|
// You may obtain a copy of the License at
|
|
|
|
|
//
|
|
|
|
|
// http://www.apache.org/licenses/LICENSE-2.0
|
|
|
|
|
//
|
|
|
|
|
// Unless required by applicable law or agreed to in writing, software
|
|
|
|
|
// distributed under the License is distributed on an "AS IS" BASIS,
|
|
|
|
|
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
|
|
|
// See the License for the specific language governing permissions and
|
|
|
|
|
// limitations under the License.
|
|
|
|
|
|
|
|
|
|
#ifndef OR_TOOLS_SAT_INTEGER_EXPR_H_
|
|
|
|
|
#define OR_TOOLS_SAT_INTEGER_EXPR_H_
|
|
|
|
|
|
2021-03-04 18:26:01 +01:00
|
|
|
#include <cstdint>
|
2017-07-27 11:28:55 -07:00
|
|
|
#include <functional>
|
|
|
|
|
#include <vector>
|
|
|
|
|
|
2018-06-08 16:40:43 +02:00
|
|
|
#include "ortools/base/int_type.h"
|
2017-07-27 11:28:55 -07:00
|
|
|
#include "ortools/base/integral_types.h"
|
|
|
|
|
#include "ortools/base/logging.h"
|
|
|
|
|
#include "ortools/base/macros.h"
|
2020-10-18 16:38:25 +02:00
|
|
|
#include "ortools/base/mathutil.h"
|
2017-04-26 17:30:25 +02:00
|
|
|
#include "ortools/sat/integer.h"
|
2020-02-03 16:21:57 +01:00
|
|
|
#include "ortools/sat/linear_constraint.h"
|
2017-04-26 17:30:25 +02:00
|
|
|
#include "ortools/sat/model.h"
|
|
|
|
|
#include "ortools/sat/precedences.h"
|
|
|
|
|
#include "ortools/sat/sat_base.h"
|
2017-07-27 11:28:55 -07:00
|
|
|
#include "ortools/sat/sat_solver.h"
|
2019-12-16 12:34:56 +01:00
|
|
|
#include "ortools/util/rev.h"
|
2016-09-12 13:51:04 +02:00
|
|
|
|
|
|
|
|
namespace operations_research {
|
|
|
|
|
namespace sat {
|
|
|
|
|
|
2016-09-22 15:18:08 +02:00
|
|
|
// A really basic implementation of an upper-bounded sum of integer variables.
|
2016-09-12 13:51:04 +02:00
|
|
|
// The complexity is in O(num_variables) at each propagation.
|
|
|
|
|
//
|
2018-09-12 15:07:23 +02:00
|
|
|
// Note that we assume that there can be NO integer overflow. This must be
|
|
|
|
|
// checked at model validation time before this is even created.
|
|
|
|
|
//
|
2016-09-12 13:51:04 +02:00
|
|
|
// TODO(user): If one has many such constraint, it will be more efficient to
|
|
|
|
|
// propagate all of them at once rather than doing it one at the time.
|
2016-09-22 15:18:08 +02:00
|
|
|
//
|
|
|
|
|
// TODO(user): Explore tree structure to get a log(n) complexity.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): When the variables are Boolean, use directly the pseudo-Boolean
|
2018-09-12 15:07:23 +02:00
|
|
|
// constraint implementation. But we do need support for enforcement literals
|
|
|
|
|
// there.
|
2016-09-22 15:18:08 +02:00
|
|
|
class IntegerSumLE : public PropagatorInterface {
|
2016-09-12 13:51:04 +02:00
|
|
|
public:
|
2016-10-05 13:53:30 +02:00
|
|
|
// If refied_literal is kNoLiteralIndex then this is a normal constraint,
|
|
|
|
|
// otherwise we enforce the implication refied_literal => constraint is true.
|
|
|
|
|
// Note that we don't do the reverse implication here, it is usually done by
|
|
|
|
|
// another IntegerSumLE constraint on the negated variables.
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerSumLE(const std::vector<Literal>& enforcement_literals,
|
|
|
|
|
const std::vector<IntegerVariable>& vars,
|
|
|
|
|
const std::vector<IntegerValue>& coeffs,
|
|
|
|
|
IntegerValue upper_bound, Model* model);
|
2016-09-22 15:18:08 +02:00
|
|
|
|
|
|
|
|
// We propagate:
|
|
|
|
|
// - If the sum of the individual lower-bound is > upper_bound, we fail.
|
|
|
|
|
// - For all i, upper-bound of i
|
|
|
|
|
// <= upper_bound - Sum {individual lower-bound excluding i).
|
2016-10-29 20:12:59 +02:00
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2020-11-16 17:01:21 +01:00
|
|
|
// Same as Propagate() but only consider current root level bounds. This is
|
|
|
|
|
// mainly useful for the LP propagator since it can find relevant optimal
|
|
|
|
|
// really late in the search tree.
|
|
|
|
|
bool PropagateAtLevelZero();
|
|
|
|
|
|
2016-09-12 13:51:04 +02:00
|
|
|
private:
|
2016-10-20 22:05:03 +02:00
|
|
|
// Fills integer_reason_ with all the current lower_bounds. The real
|
|
|
|
|
// explanation may require removing one of them, but as an optimization, we
|
|
|
|
|
// always keep all the IntegerLiteral in integer_reason_, and swap them as
|
|
|
|
|
// needed just before pushing something.
|
|
|
|
|
void FillIntegerReason();
|
|
|
|
|
|
2018-09-12 15:07:23 +02:00
|
|
|
const std::vector<Literal> enforcement_literals_;
|
2016-09-22 15:18:08 +02:00
|
|
|
const IntegerValue upper_bound_;
|
2017-04-26 17:30:25 +02:00
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
Trail* trail_;
|
|
|
|
|
IntegerTrail* integer_trail_;
|
|
|
|
|
TimeLimit* time_limit_;
|
|
|
|
|
RevIntegerValueRepository* rev_integer_value_repository_;
|
2017-04-26 17:30:25 +02:00
|
|
|
|
|
|
|
|
// Reversible sum of the lower bound of the fixed variables.
|
2018-12-21 13:59:58 +01:00
|
|
|
bool is_registered_ = false;
|
2017-04-26 17:30:25 +02:00
|
|
|
IntegerValue rev_lb_fixed_vars_;
|
|
|
|
|
|
|
|
|
|
// Reversible number of fixed variables.
|
|
|
|
|
int rev_num_fixed_vars_;
|
|
|
|
|
|
|
|
|
|
// Those vectors are shuffled during search to ensure that the variables
|
|
|
|
|
// (resp. coefficients) contained in the range [0, rev_num_fixed_vars_) of
|
|
|
|
|
// vars_ (resp. coeffs_) are fixed (resp. belong to fixed variables).
|
|
|
|
|
std::vector<IntegerVariable> vars_;
|
|
|
|
|
std::vector<IntegerValue> coeffs_;
|
2019-01-07 18:04:21 +01:00
|
|
|
std::vector<IntegerValue> max_variations_;
|
2017-04-26 17:30:25 +02:00
|
|
|
|
2016-09-12 13:51:04 +02:00
|
|
|
std::vector<Literal> literal_reason_;
|
2018-12-18 11:42:14 +01:00
|
|
|
|
|
|
|
|
// Parallel vectors.
|
2016-09-12 13:51:04 +02:00
|
|
|
std::vector<IntegerLiteral> integer_reason_;
|
2018-12-18 11:42:14 +01:00
|
|
|
std::vector<IntegerValue> reason_coeffs_;
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2016-09-22 15:18:08 +02:00
|
|
|
DISALLOW_COPY_AND_ASSIGN(IntegerSumLE);
|
2016-09-12 13:51:04 +02:00
|
|
|
};
|
|
|
|
|
|
2020-10-18 16:38:25 +02:00
|
|
|
// This assumes target = SUM_i coeffs[i] * vars[i], and detects that the target
|
|
|
|
|
// must be of the form (a*X + b).
|
|
|
|
|
//
|
|
|
|
|
// This propagator is quite specific and runs only at level zero. For now, this
|
|
|
|
|
// is mainly used for the objective variable. As we fix terms with high
|
|
|
|
|
// objective coefficient, it is possible the only terms left have a common
|
|
|
|
|
// divisor. This close app2-2.mps in less than a second instead of running
|
|
|
|
|
// forever to prove the optimal (in single thread).
|
|
|
|
|
class LevelZeroEquality : PropagatorInterface {
|
|
|
|
|
public:
|
|
|
|
|
LevelZeroEquality(IntegerVariable target,
|
2020-10-29 14:25:39 +01:00
|
|
|
const std::vector<IntegerVariable>& vars,
|
|
|
|
|
const std::vector<IntegerValue>& coeffs, Model* model);
|
2020-10-18 16:38:25 +02:00
|
|
|
|
|
|
|
|
bool Propagate() final;
|
|
|
|
|
|
|
|
|
|
private:
|
|
|
|
|
const IntegerVariable target_;
|
|
|
|
|
const std::vector<IntegerVariable> vars_;
|
|
|
|
|
const std::vector<IntegerValue> coeffs_;
|
|
|
|
|
|
|
|
|
|
IntegerValue gcd_ = IntegerValue(1);
|
|
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
Trail* trail_;
|
|
|
|
|
IntegerTrail* integer_trail_;
|
2020-10-18 16:38:25 +02:00
|
|
|
};
|
|
|
|
|
|
2021-09-29 16:18:52 +02:00
|
|
|
// A min (resp max) constraint of the form min == MIN(vars) can be decomposed
|
2016-09-12 13:51:04 +02:00
|
|
|
// into two inequalities:
|
|
|
|
|
// 1/ min <= MIN(vars), which is the same as for all v in vars, "min <= v".
|
|
|
|
|
// This can be taken care of by the LowerOrEqual(min, v) constraint.
|
|
|
|
|
// 2/ min >= MIN(vars).
|
|
|
|
|
//
|
|
|
|
|
// And in turn, 2/ can be decomposed in:
|
|
|
|
|
// a) lb(min) >= lb(MIN(vars)) = MIN(lb(var));
|
|
|
|
|
// b) ub(min) >= ub(MIN(vars)) and we can't propagate anything here unless
|
|
|
|
|
// there is just one possible variable 'v' that can be the min:
|
|
|
|
|
// for all u != v, lb(u) > ub(min);
|
|
|
|
|
// In this case, ub(min) >= ub(v).
|
|
|
|
|
//
|
|
|
|
|
// This constraint take care of a) and b). That is:
|
|
|
|
|
// - If the min of the lower bound of the vars increase, then the lower bound of
|
|
|
|
|
// the min_var will be >= to it.
|
|
|
|
|
// - If there is only one candidate for the min, then if the ub(min) decrease,
|
|
|
|
|
// the ub of the only candidate will be <= to it.
|
|
|
|
|
//
|
|
|
|
|
// Complexity: This is a basic implementation in O(num_vars) on each call to
|
|
|
|
|
// Propagate(), which will happen each time one or more variables in vars_
|
|
|
|
|
// changed.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): Implement a more efficient algorithm when the need arise.
|
|
|
|
|
class MinPropagator : public PropagatorInterface {
|
|
|
|
|
public:
|
2020-10-29 14:25:39 +01:00
|
|
|
MinPropagator(const std::vector<IntegerVariable>& vars,
|
|
|
|
|
IntegerVariable min_var, IntegerTrail* integer_trail);
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2016-10-29 20:12:59 +02:00
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2016-09-12 13:51:04 +02:00
|
|
|
|
|
|
|
|
private:
|
|
|
|
|
const std::vector<IntegerVariable> vars_;
|
|
|
|
|
const IntegerVariable min_var_;
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerTrail* integer_trail_;
|
2016-09-12 13:51:04 +02:00
|
|
|
|
|
|
|
|
std::vector<IntegerLiteral> integer_reason_;
|
|
|
|
|
|
|
|
|
|
DISALLOW_COPY_AND_ASSIGN(MinPropagator);
|
|
|
|
|
};
|
|
|
|
|
|
2019-12-16 12:34:56 +01:00
|
|
|
// Same as MinPropagator except this works on min = MIN(exprs) where exprs are
|
|
|
|
|
// linear expressions. It uses IntegerSumLE to propagate bounds on the exprs.
|
|
|
|
|
// Assumes Canonical expressions (all positive coefficients).
|
|
|
|
|
class LinMinPropagator : public PropagatorInterface {
|
|
|
|
|
public:
|
2020-10-29 14:25:39 +01:00
|
|
|
LinMinPropagator(const std::vector<LinearExpression>& exprs,
|
|
|
|
|
IntegerVariable min_var, Model* model);
|
|
|
|
|
LinMinPropagator(const LinMinPropagator&) = delete;
|
|
|
|
|
LinMinPropagator& operator=(const LinMinPropagator&) = delete;
|
2019-12-16 12:34:56 +01:00
|
|
|
|
|
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2019-12-16 12:34:56 +01:00
|
|
|
|
|
|
|
|
private:
|
2020-01-07 16:51:46 +01:00
|
|
|
// Lighter version of IntegerSumLE. This uses the current value of
|
|
|
|
|
// integer_reason_ in addition to the reason for propagating the linear
|
|
|
|
|
// constraint. The coeffs are assumed to be positive here.
|
2020-10-29 14:25:39 +01:00
|
|
|
bool PropagateLinearUpperBound(const std::vector<IntegerVariable>& vars,
|
|
|
|
|
const std::vector<IntegerValue>& coeffs,
|
2020-01-07 16:51:46 +01:00
|
|
|
IntegerValue upper_bound);
|
|
|
|
|
|
2019-12-16 12:34:56 +01:00
|
|
|
const std::vector<LinearExpression> exprs_;
|
|
|
|
|
const IntegerVariable min_var_;
|
|
|
|
|
std::vector<IntegerValue> expr_lbs_;
|
2020-10-29 14:25:39 +01:00
|
|
|
Model* model_;
|
|
|
|
|
IntegerTrail* integer_trail_;
|
2020-01-20 10:51:53 +01:00
|
|
|
std::vector<IntegerLiteral> integer_reason_for_unique_candidate_;
|
|
|
|
|
int rev_unique_candidate_ = 0;
|
2019-12-16 12:34:56 +01:00
|
|
|
};
|
|
|
|
|
|
2016-10-05 13:53:30 +02:00
|
|
|
// Propagates a * b = c. Basic version, we don't extract any special cases, and
|
|
|
|
|
// we only propagates the bounds.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): For now this only works on variables that are non-negative.
|
|
|
|
|
// TODO(user): Deal with overflow.
|
2017-04-26 17:30:25 +02:00
|
|
|
class PositiveProductPropagator : public PropagatorInterface {
|
2016-10-05 13:53:30 +02:00
|
|
|
public:
|
2021-10-27 13:22:27 +02:00
|
|
|
PositiveProductPropagator(AffineExpression a, AffineExpression b,
|
|
|
|
|
AffineExpression p, IntegerTrail* integer_trail);
|
2016-10-05 13:53:30 +02:00
|
|
|
|
2016-10-29 20:12:59 +02:00
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2016-10-05 13:53:30 +02:00
|
|
|
|
|
|
|
|
private:
|
2021-10-27 13:22:27 +02:00
|
|
|
const AffineExpression a_;
|
|
|
|
|
const AffineExpression b_;
|
|
|
|
|
const AffineExpression p_;
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerTrail* integer_trail_;
|
2016-10-05 13:53:30 +02:00
|
|
|
|
2017-04-26 17:30:25 +02:00
|
|
|
DISALLOW_COPY_AND_ASSIGN(PositiveProductPropagator);
|
2016-10-05 13:53:30 +02:00
|
|
|
};
|
|
|
|
|
|
2021-09-29 16:36:42 +02:00
|
|
|
// Propagates num / denom = div. Basic version, we don't extract any special
|
2021-10-27 13:22:27 +02:00
|
|
|
// cases, and we only propagates the bounds. It expects denom to be > 0.
|
2016-10-07 17:29:33 +02:00
|
|
|
//
|
|
|
|
|
// TODO(user): Deal with overflow.
|
2021-10-27 13:22:27 +02:00
|
|
|
class DivisionPropagator : public PropagatorInterface {
|
2016-10-07 17:29:33 +02:00
|
|
|
public:
|
2021-10-27 13:22:27 +02:00
|
|
|
DivisionPropagator(AffineExpression num, AffineExpression denom,
|
|
|
|
|
AffineExpression div, IntegerTrail* integer_trail);
|
2016-10-07 17:29:33 +02:00
|
|
|
|
2016-10-29 20:12:59 +02:00
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2016-10-07 17:29:33 +02:00
|
|
|
|
|
|
|
|
private:
|
2021-10-27 13:22:27 +02:00
|
|
|
// Propagates the fact that the signs of each domain, if fixed, are
|
|
|
|
|
// compatible.
|
|
|
|
|
bool PropagateSigns();
|
|
|
|
|
|
|
|
|
|
// If both num and div >= 0, we can propagate their upper bounds.
|
|
|
|
|
bool PropagateUpperBounds(AffineExpression num, AffineExpression denom,
|
|
|
|
|
AffineExpression div);
|
|
|
|
|
|
|
|
|
|
// When the sign of all 3 expressions are fixed, we can do morel propagation.
|
|
|
|
|
//
|
|
|
|
|
// By using negated expressions, we can make sure the domains of num, denom,
|
|
|
|
|
// and div are positive.
|
|
|
|
|
bool PropagatePositiveDomains(AffineExpression num, AffineExpression denom,
|
|
|
|
|
AffineExpression div);
|
|
|
|
|
|
|
|
|
|
const AffineExpression num_;
|
|
|
|
|
const AffineExpression denom_;
|
|
|
|
|
const AffineExpression div_;
|
|
|
|
|
const AffineExpression negated_num_;
|
|
|
|
|
const AffineExpression negated_div_;
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerTrail* integer_trail_;
|
2016-10-07 17:29:33 +02:00
|
|
|
|
2021-10-27 13:22:27 +02:00
|
|
|
DISALLOW_COPY_AND_ASSIGN(DivisionPropagator);
|
2016-10-07 17:29:33 +02:00
|
|
|
};
|
|
|
|
|
|
2019-02-28 13:30:01 +01:00
|
|
|
// Propagates var_a / cst_b = var_c. Basic version, we don't extract any special
|
2019-02-28 17:07:29 +01:00
|
|
|
// cases, and we only propagates the bounds. cst_b must be > 0.
|
2019-02-28 13:30:01 +01:00
|
|
|
class FixedDivisionPropagator : public PropagatorInterface {
|
|
|
|
|
public:
|
2021-10-25 16:30:57 +02:00
|
|
|
FixedDivisionPropagator(AffineExpression a, IntegerValue b,
|
|
|
|
|
AffineExpression c, IntegerTrail* integer_trail);
|
2019-02-28 13:30:01 +01:00
|
|
|
|
|
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2019-02-28 13:30:01 +01:00
|
|
|
|
|
|
|
|
private:
|
2021-10-25 16:30:57 +02:00
|
|
|
const AffineExpression a_;
|
2019-02-28 13:30:01 +01:00
|
|
|
const IntegerValue b_;
|
2021-10-25 16:30:57 +02:00
|
|
|
const AffineExpression c_;
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerTrail* integer_trail_;
|
2019-02-28 13:30:01 +01:00
|
|
|
|
|
|
|
|
DISALLOW_COPY_AND_ASSIGN(FixedDivisionPropagator);
|
|
|
|
|
};
|
|
|
|
|
|
2017-07-21 11:13:10 -07:00
|
|
|
// Propagates x * x = s.
|
|
|
|
|
// TODO(user): Only works for x nonnegative.
|
|
|
|
|
class SquarePropagator : public PropagatorInterface {
|
|
|
|
|
public:
|
2021-10-27 13:22:27 +02:00
|
|
|
SquarePropagator(AffineExpression x, AffineExpression s,
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerTrail* integer_trail);
|
2017-07-21 11:13:10 -07:00
|
|
|
|
|
|
|
|
bool Propagate() final;
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterWith(GenericLiteralWatcher* watcher);
|
2017-07-21 11:13:10 -07:00
|
|
|
|
|
|
|
|
private:
|
2021-10-27 13:22:27 +02:00
|
|
|
const AffineExpression x_;
|
|
|
|
|
const AffineExpression s_;
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerTrail* integer_trail_;
|
2017-07-21 11:13:10 -07:00
|
|
|
|
|
|
|
|
DISALLOW_COPY_AND_ASSIGN(SquarePropagator);
|
|
|
|
|
};
|
|
|
|
|
|
2016-09-12 13:51:04 +02:00
|
|
|
// =============================================================================
|
|
|
|
|
// Model based functions.
|
|
|
|
|
// =============================================================================
|
|
|
|
|
|
2016-09-22 15:18:08 +02:00
|
|
|
// Weighted sum <= constant.
|
|
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> WeightedSumLowerOrEqual(
|
|
|
|
|
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
|
2021-03-04 18:26:01 +01:00
|
|
|
int64_t upper_bound) {
|
2016-10-12 12:07:20 -07:00
|
|
|
// Special cases.
|
2017-03-28 16:11:06 +02:00
|
|
|
CHECK_GE(vars.size(), 1);
|
2016-12-14 22:03:52 +01:00
|
|
|
if (vars.size() == 1) {
|
2021-03-04 18:26:01 +01:00
|
|
|
const int64_t c = coefficients[0];
|
2018-09-02 17:15:55 +02:00
|
|
|
CHECK_NE(c, 0);
|
|
|
|
|
if (c > 0) {
|
2020-10-22 23:36:58 +02:00
|
|
|
return LowerOrEqual(
|
|
|
|
|
vars[0],
|
|
|
|
|
FloorRatio(IntegerValue(upper_bound), IntegerValue(c)).value());
|
2016-12-14 22:03:52 +01:00
|
|
|
} else {
|
2020-10-22 23:36:58 +02:00
|
|
|
return GreaterOrEqual(
|
|
|
|
|
vars[0],
|
|
|
|
|
CeilRatio(IntegerValue(-upper_bound), IntegerValue(-c)).value());
|
2016-12-14 22:03:52 +01:00
|
|
|
}
|
|
|
|
|
}
|
2016-10-12 12:07:20 -07:00
|
|
|
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
|
|
|
|
|
(coefficients[1] == 1 || coefficients[1] == -1)) {
|
|
|
|
|
return Sum2LowerOrEqual(
|
|
|
|
|
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
|
|
|
|
|
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound);
|
|
|
|
|
}
|
|
|
|
|
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
|
|
|
|
|
(coefficients[1] == 1 || coefficients[1] == -1) &&
|
|
|
|
|
(coefficients[2] == 1 || coefficients[2] == -1)) {
|
|
|
|
|
return Sum3LowerOrEqual(
|
|
|
|
|
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
|
|
|
|
|
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
|
|
|
|
|
coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound);
|
|
|
|
|
}
|
2019-02-13 11:02:17 +01:00
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2019-02-13 11:02:17 +01:00
|
|
|
// We split large constraints into a square root number of parts.
|
|
|
|
|
// This is to avoid a bad complexity while propagating them since our
|
|
|
|
|
// algorithm is not in O(num_changes).
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): Alternatively, we could use a O(num_changes) propagation (a
|
|
|
|
|
// bit tricky to implement), or a decomposition into a tree with more than
|
|
|
|
|
// one level. Both requires experimentations.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): If the initial constraint was an equalilty we will create
|
|
|
|
|
// the "intermediate" variable twice where we could have use the same for
|
|
|
|
|
// both direction. Improve?
|
|
|
|
|
const int num_vars = vars.size();
|
|
|
|
|
if (num_vars > 100) {
|
|
|
|
|
std::vector<IntegerVariable> bucket_sum_vars;
|
|
|
|
|
|
|
|
|
|
std::vector<IntegerVariable> local_vars;
|
|
|
|
|
std::vector<IntegerValue> local_coeffs;
|
|
|
|
|
|
|
|
|
|
int i = 0;
|
|
|
|
|
const int num_buckets = static_cast<int>(std::round(std::sqrt(num_vars)));
|
|
|
|
|
for (int b = 0; b < num_buckets; ++b) {
|
|
|
|
|
local_vars.clear();
|
|
|
|
|
local_coeffs.clear();
|
2021-04-01 12:13:35 +02:00
|
|
|
int64_t bucket_lb = 0;
|
|
|
|
|
int64_t bucket_ub = 0;
|
2019-02-13 11:02:17 +01:00
|
|
|
const int limit = num_vars * (b + 1);
|
|
|
|
|
for (; i * num_buckets < limit; ++i) {
|
|
|
|
|
local_vars.push_back(vars[i]);
|
|
|
|
|
local_coeffs.push_back(IntegerValue(coefficients[i]));
|
2021-04-08 18:26:14 +02:00
|
|
|
const int64_t term1 =
|
|
|
|
|
model->Get(LowerBound(vars[i])) * coefficients[i];
|
|
|
|
|
const int64_t term2 =
|
|
|
|
|
model->Get(UpperBound(vars[i])) * coefficients[i];
|
2019-02-13 11:02:17 +01:00
|
|
|
bucket_lb += std::min(term1, term2);
|
|
|
|
|
bucket_ub += std::max(term1, term2);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
const IntegerVariable bucket_sum =
|
|
|
|
|
model->Add(NewIntegerVariable(bucket_lb, bucket_ub));
|
|
|
|
|
bucket_sum_vars.push_back(bucket_sum);
|
|
|
|
|
local_vars.push_back(bucket_sum);
|
|
|
|
|
local_coeffs.push_back(IntegerValue(-1));
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerSumLE* constraint = new IntegerSumLE(
|
2020-10-22 23:36:58 +02:00
|
|
|
{}, local_vars, local_coeffs, IntegerValue(0), model);
|
2019-02-13 11:02:17 +01:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Create the root-level sum.
|
|
|
|
|
local_vars.clear();
|
|
|
|
|
local_coeffs.clear();
|
|
|
|
|
for (const IntegerVariable var : bucket_sum_vars) {
|
|
|
|
|
local_vars.push_back(var);
|
|
|
|
|
local_coeffs.push_back(IntegerValue(1));
|
|
|
|
|
}
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerSumLE* constraint = new IntegerSumLE(
|
2020-10-22 23:36:58 +02:00
|
|
|
{}, local_vars, local_coeffs, IntegerValue(upper_bound), model);
|
2019-02-13 11:02:17 +01:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerSumLE* constraint = new IntegerSumLE(
|
2020-10-22 23:36:58 +02:00
|
|
|
{}, vars,
|
2016-10-05 13:53:30 +02:00
|
|
|
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
|
2017-07-06 04:56:28 -07:00
|
|
|
IntegerValue(upper_bound), model);
|
2016-09-22 15:18:08 +02:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-09-22 15:18:08 +02:00
|
|
|
}
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2016-09-22 15:18:08 +02:00
|
|
|
// Weighted sum >= constant.
|
|
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> WeightedSumGreaterOrEqual(
|
|
|
|
|
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
|
2021-03-04 18:26:01 +01:00
|
|
|
int64_t lower_bound) {
|
2016-10-13 10:44:35 -07:00
|
|
|
// We just negate everything and use an <= constraints.
|
2021-03-04 18:26:01 +01:00
|
|
|
std::vector<int64_t> negated_coeffs(coefficients.begin(), coefficients.end());
|
|
|
|
|
for (int64_t& ref : negated_coeffs) ref = -ref;
|
2016-10-12 12:07:20 -07:00
|
|
|
return WeightedSumLowerOrEqual(vars, negated_coeffs, -lower_bound);
|
2016-09-22 15:18:08 +02:00
|
|
|
}
|
|
|
|
|
|
2016-10-05 13:53:30 +02:00
|
|
|
// Weighted sum == constant.
|
2016-09-22 15:18:08 +02:00
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> FixedWeightedSum(
|
|
|
|
|
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
|
2021-03-04 18:26:01 +01:00
|
|
|
int64_t value) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2016-09-22 15:18:08 +02:00
|
|
|
model->Add(WeightedSumGreaterOrEqual(vars, coefficients, value));
|
|
|
|
|
model->Add(WeightedSumLowerOrEqual(vars, coefficients, value));
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-09-22 15:18:08 +02:00
|
|
|
}
|
|
|
|
|
|
2018-09-12 15:07:23 +02:00
|
|
|
// enforcement_literals => sum <= upper_bound
|
2016-10-13 10:44:35 -07:00
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
|
|
|
|
|
const std::vector<Literal>& enforcement_literals,
|
|
|
|
|
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
|
2021-03-04 18:26:01 +01:00
|
|
|
int64_t upper_bound) {
|
2016-10-13 10:44:35 -07:00
|
|
|
// Special cases.
|
2016-12-14 22:03:52 +01:00
|
|
|
CHECK_GE(vars.size(), 1);
|
|
|
|
|
if (vars.size() == 1) {
|
2017-03-28 16:11:06 +02:00
|
|
|
CHECK_NE(coefficients[0], 0);
|
|
|
|
|
if (coefficients[0] > 0) {
|
|
|
|
|
return Implication(
|
2018-09-12 15:07:23 +02:00
|
|
|
enforcement_literals,
|
|
|
|
|
IntegerLiteral::LowerOrEqual(
|
2020-01-07 16:51:46 +01:00
|
|
|
vars[0], FloorRatio(IntegerValue(upper_bound),
|
|
|
|
|
IntegerValue(coefficients[0]))));
|
2017-03-28 16:11:06 +02:00
|
|
|
} else {
|
|
|
|
|
return Implication(
|
2018-09-12 15:07:23 +02:00
|
|
|
enforcement_literals,
|
|
|
|
|
IntegerLiteral::GreaterOrEqual(
|
2020-01-07 16:51:46 +01:00
|
|
|
vars[0], CeilRatio(IntegerValue(-upper_bound),
|
|
|
|
|
IntegerValue(-coefficients[0]))));
|
2017-03-28 16:11:06 +02:00
|
|
|
}
|
2016-12-14 22:03:52 +01:00
|
|
|
}
|
2019-08-22 13:15:49 +02:00
|
|
|
|
2016-10-13 10:44:35 -07:00
|
|
|
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
|
|
|
|
|
(coefficients[1] == 1 || coefficients[1] == -1)) {
|
|
|
|
|
return ConditionalSum2LowerOrEqual(
|
|
|
|
|
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
|
|
|
|
|
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound,
|
2018-09-12 15:07:23 +02:00
|
|
|
enforcement_literals);
|
2016-10-13 10:44:35 -07:00
|
|
|
}
|
|
|
|
|
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
|
|
|
|
|
(coefficients[1] == 1 || coefficients[1] == -1) &&
|
|
|
|
|
(coefficients[2] == 1 || coefficients[2] == -1)) {
|
|
|
|
|
return ConditionalSum3LowerOrEqual(
|
|
|
|
|
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
|
|
|
|
|
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
|
|
|
|
|
coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound,
|
2018-09-12 15:07:23 +02:00
|
|
|
enforcement_literals);
|
2016-10-13 10:44:35 -07:00
|
|
|
}
|
2019-08-22 13:15:49 +02:00
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2019-08-22 13:15:49 +02:00
|
|
|
// If value == min(expression), then we can avoid creating the sum.
|
|
|
|
|
IntegerValue expression_min(0);
|
2020-10-29 14:25:39 +01:00
|
|
|
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
|
2019-08-22 13:15:49 +02:00
|
|
|
for (int i = 0; i < vars.size(); ++i) {
|
|
|
|
|
expression_min +=
|
2020-10-22 23:36:58 +02:00
|
|
|
coefficients[i] * (coefficients[i] >= 0
|
|
|
|
|
? integer_trail->LowerBound(vars[i])
|
|
|
|
|
: integer_trail->UpperBound(vars[i]));
|
2019-08-22 13:15:49 +02:00
|
|
|
}
|
|
|
|
|
if (expression_min == upper_bound) {
|
2020-11-25 22:38:26 +01:00
|
|
|
// Tricky: as we create integer literal, we might propagate stuff and
|
|
|
|
|
// the bounds might change, so if the expression_min increase with the
|
|
|
|
|
// bound we use, then the literal must be false.
|
|
|
|
|
IntegerValue non_cached_min;
|
2019-08-22 13:15:49 +02:00
|
|
|
for (int i = 0; i < vars.size(); ++i) {
|
|
|
|
|
if (coefficients[i] > 0) {
|
2020-11-25 22:38:26 +01:00
|
|
|
const IntegerValue lb = integer_trail->LowerBound(vars[i]);
|
|
|
|
|
non_cached_min += coefficients[i] * lb;
|
|
|
|
|
model->Add(Implication(enforcement_literals,
|
|
|
|
|
IntegerLiteral::LowerOrEqual(vars[i], lb)));
|
2019-08-22 13:15:49 +02:00
|
|
|
} else if (coefficients[i] < 0) {
|
2020-11-25 22:38:26 +01:00
|
|
|
const IntegerValue ub = integer_trail->UpperBound(vars[i]);
|
|
|
|
|
non_cached_min += coefficients[i] * ub;
|
|
|
|
|
model->Add(Implication(enforcement_literals,
|
|
|
|
|
IntegerLiteral::GreaterOrEqual(vars[i], ub)));
|
2019-08-22 13:15:49 +02:00
|
|
|
}
|
|
|
|
|
}
|
2020-11-25 22:38:26 +01:00
|
|
|
if (non_cached_min > expression_min) {
|
|
|
|
|
std::vector<Literal> clause;
|
|
|
|
|
for (const Literal l : enforcement_literals) {
|
|
|
|
|
clause.push_back(l.Negated());
|
|
|
|
|
}
|
|
|
|
|
model->Add(ClauseConstraint(clause));
|
|
|
|
|
}
|
2019-08-22 13:15:49 +02:00
|
|
|
} else {
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerSumLE* constraint = new IntegerSumLE(
|
2019-08-22 13:15:49 +02:00
|
|
|
enforcement_literals, vars,
|
|
|
|
|
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
|
|
|
|
|
IntegerValue(upper_bound), model);
|
|
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
|
|
|
|
}
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-10-13 10:44:35 -07:00
|
|
|
}
|
|
|
|
|
|
2018-09-12 15:07:23 +02:00
|
|
|
// enforcement_literals => sum >= lower_bound
|
2016-10-13 10:44:35 -07:00
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> ConditionalWeightedSumGreaterOrEqual(
|
|
|
|
|
const std::vector<Literal>& enforcement_literals,
|
|
|
|
|
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
|
2021-03-04 18:26:01 +01:00
|
|
|
int64_t lower_bound) {
|
2016-10-13 10:44:35 -07:00
|
|
|
// We just negate everything and use an <= constraint.
|
2021-03-04 18:26:01 +01:00
|
|
|
std::vector<int64_t> negated_coeffs(coefficients.begin(), coefficients.end());
|
|
|
|
|
for (int64_t& ref : negated_coeffs) ref = -ref;
|
2018-09-12 15:07:23 +02:00
|
|
|
return ConditionalWeightedSumLowerOrEqual(enforcement_literals, vars,
|
|
|
|
|
negated_coeffs, -lower_bound);
|
2016-10-13 10:44:35 -07:00
|
|
|
}
|
|
|
|
|
|
2016-10-05 13:53:30 +02:00
|
|
|
// Weighted sum <= constant reified.
|
|
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> WeightedSumLowerOrEqualReif(
|
|
|
|
|
Literal is_le, const std::vector<IntegerVariable>& vars,
|
2021-03-04 18:26:01 +01:00
|
|
|
const VectorInt& coefficients, int64_t upper_bound) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2020-10-22 23:36:58 +02:00
|
|
|
model->Add(ConditionalWeightedSumLowerOrEqual({is_le}, vars, coefficients,
|
2016-10-13 10:44:35 -07:00
|
|
|
upper_bound));
|
2020-10-22 23:36:58 +02:00
|
|
|
model->Add(ConditionalWeightedSumGreaterOrEqual(
|
|
|
|
|
{is_le.Negated()}, vars, coefficients, upper_bound + 1));
|
|
|
|
|
};
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Weighted sum >= constant reified.
|
|
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> WeightedSumGreaterOrEqualReif(
|
|
|
|
|
Literal is_ge, const std::vector<IntegerVariable>& vars,
|
2021-03-04 18:26:01 +01:00
|
|
|
const VectorInt& coefficients, int64_t lower_bound) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2020-10-22 23:36:58 +02:00
|
|
|
model->Add(ConditionalWeightedSumGreaterOrEqual({is_ge}, vars, coefficients,
|
2016-10-13 10:44:35 -07:00
|
|
|
lower_bound));
|
2020-10-22 23:36:58 +02:00
|
|
|
model->Add(ConditionalWeightedSumLowerOrEqual(
|
|
|
|
|
{is_ge.Negated()}, vars, coefficients, lower_bound - 1));
|
|
|
|
|
};
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
2020-02-03 16:21:57 +01:00
|
|
|
// LinearConstraint version.
|
2020-10-29 14:25:39 +01:00
|
|
|
inline void LoadLinearConstraint(const LinearConstraint& cst, Model* model) {
|
2020-02-03 16:21:57 +01:00
|
|
|
if (cst.vars.empty()) {
|
2020-10-22 23:36:58 +02:00
|
|
|
if (cst.lb <= 0 && cst.ub >= 0) return;
|
2020-02-03 16:21:57 +01:00
|
|
|
model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// TODO(user): Remove the conversion!
|
2021-03-04 18:26:01 +01:00
|
|
|
std::vector<int64_t> converted_coeffs;
|
2021-10-27 13:22:27 +02:00
|
|
|
|
2020-10-22 23:36:58 +02:00
|
|
|
for (const IntegerValue v : cst.coeffs) converted_coeffs.push_back(v.value());
|
2020-02-03 16:21:57 +01:00
|
|
|
if (cst.ub < kMaxIntegerValue) {
|
|
|
|
|
model->Add(
|
|
|
|
|
WeightedSumLowerOrEqual(cst.vars, converted_coeffs, cst.ub.value()));
|
|
|
|
|
}
|
|
|
|
|
if (cst.lb > kMinIntegerValue) {
|
|
|
|
|
model->Add(
|
|
|
|
|
WeightedSumGreaterOrEqual(cst.vars, converted_coeffs, cst.lb.value()));
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
inline void LoadConditionalLinearConstraint(
|
|
|
|
|
const absl::Span<const Literal> enforcement_literals,
|
2020-10-29 14:25:39 +01:00
|
|
|
const LinearConstraint& cst, Model* model) {
|
2020-02-03 16:21:57 +01:00
|
|
|
if (enforcement_literals.empty()) {
|
|
|
|
|
return LoadLinearConstraint(cst, model);
|
|
|
|
|
}
|
|
|
|
|
if (cst.vars.empty()) {
|
2020-10-22 23:36:58 +02:00
|
|
|
if (cst.lb <= 0 && cst.ub >= 0) return;
|
2020-02-03 16:21:57 +01:00
|
|
|
return model->Add(ClauseConstraint(enforcement_literals));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// TODO(user): Remove the conversion!
|
|
|
|
|
std::vector<Literal> converted_literals(enforcement_literals.begin(),
|
|
|
|
|
enforcement_literals.end());
|
2021-03-04 18:26:01 +01:00
|
|
|
std::vector<int64_t> converted_coeffs;
|
2020-10-22 23:36:58 +02:00
|
|
|
for (const IntegerValue v : cst.coeffs) converted_coeffs.push_back(v.value());
|
2020-02-03 16:21:57 +01:00
|
|
|
|
|
|
|
|
if (cst.ub < kMaxIntegerValue) {
|
|
|
|
|
model->Add(ConditionalWeightedSumLowerOrEqual(
|
|
|
|
|
converted_literals, cst.vars, converted_coeffs, cst.ub.value()));
|
|
|
|
|
}
|
|
|
|
|
if (cst.lb > kMinIntegerValue) {
|
|
|
|
|
model->Add(ConditionalWeightedSumGreaterOrEqual(
|
|
|
|
|
converted_literals, cst.vars, converted_coeffs, cst.lb.value()));
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
2016-10-05 13:53:30 +02:00
|
|
|
// Weighted sum == constant reified.
|
2016-11-18 15:32:26 +01:00
|
|
|
// TODO(user): Simplify if the constant is at the edge of the possible values.
|
2016-10-05 13:53:30 +02:00
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> FixedWeightedSumReif(
|
|
|
|
|
Literal is_eq, const std::vector<IntegerVariable>& vars,
|
2021-03-04 18:26:01 +01:00
|
|
|
const VectorInt& coefficients, int64_t value) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2016-10-05 13:53:30 +02:00
|
|
|
// We creates two extra Boolean variables in this case. The alternative is
|
|
|
|
|
// to code a custom propagator for the direction equality => reified.
|
|
|
|
|
const Literal is_le = Literal(model->Add(NewBooleanVariable()), true);
|
|
|
|
|
const Literal is_ge = Literal(model->Add(NewBooleanVariable()), true);
|
2020-10-22 23:36:58 +02:00
|
|
|
model->Add(ReifiedBoolAnd({is_le, is_ge}, is_eq));
|
2016-10-05 13:53:30 +02:00
|
|
|
model->Add(WeightedSumLowerOrEqualReif(is_le, vars, coefficients, value));
|
|
|
|
|
model->Add(WeightedSumGreaterOrEqualReif(is_ge, vars, coefficients, value));
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Weighted sum != constant.
|
2016-11-18 15:32:26 +01:00
|
|
|
// TODO(user): Simplify if the constant is at the edge of the possible values.
|
2016-10-05 13:53:30 +02:00
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> WeightedSumNotEqual(
|
|
|
|
|
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
|
2021-03-04 18:26:01 +01:00
|
|
|
int64_t value) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
2016-10-13 10:44:35 -07:00
|
|
|
// Exactly one of these alternative must be true.
|
2016-10-05 13:53:30 +02:00
|
|
|
const Literal is_lt = Literal(model->Add(NewBooleanVariable()), true);
|
2016-10-13 10:44:35 -07:00
|
|
|
const Literal is_gt = is_lt.Negated();
|
|
|
|
|
model->Add(ConditionalWeightedSumLowerOrEqual(is_lt, vars, coefficients,
|
|
|
|
|
value - 1));
|
|
|
|
|
model->Add(ConditionalWeightedSumGreaterOrEqual(is_gt, vars, coefficients,
|
|
|
|
|
value + 1));
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
2016-09-22 15:18:08 +02:00
|
|
|
// Model-based function to create an IntegerVariable that corresponds to the
|
|
|
|
|
// given weighted sum of other IntegerVariables.
|
|
|
|
|
//
|
2019-11-20 14:28:11 -08:00
|
|
|
// Note that this is templated so that it can seamlessly accept vector<int> or
|
2021-04-01 12:13:35 +02:00
|
|
|
// vector<int64_t>.
|
2016-09-22 15:18:08 +02:00
|
|
|
//
|
|
|
|
|
// TODO(user): invert the coefficients/vars arguments.
|
|
|
|
|
template <typename VectorInt>
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<IntegerVariable(Model*)> NewWeightedSum(
|
|
|
|
|
const VectorInt& coefficients, const std::vector<IntegerVariable>& vars) {
|
|
|
|
|
return [=](Model* model) {
|
2020-10-22 23:36:58 +02:00
|
|
|
std::vector<IntegerVariable> new_vars = vars;
|
2016-09-22 15:18:08 +02:00
|
|
|
// To avoid overflow in the FixedWeightedSum() constraint, we need to
|
|
|
|
|
// compute the basic bounds on the sum.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): deal with overflow here too!
|
2021-04-01 12:13:35 +02:00
|
|
|
int64_t sum_lb(0);
|
|
|
|
|
int64_t sum_ub(0);
|
2016-09-22 15:18:08 +02:00
|
|
|
for (int i = 0; i < new_vars.size(); ++i) {
|
|
|
|
|
if (coefficients[i] > 0) {
|
|
|
|
|
sum_lb += coefficients[i] * model->Get(LowerBound(new_vars[i]));
|
|
|
|
|
sum_ub += coefficients[i] * model->Get(UpperBound(new_vars[i]));
|
|
|
|
|
} else {
|
|
|
|
|
sum_lb += coefficients[i] * model->Get(UpperBound(new_vars[i]));
|
|
|
|
|
sum_ub += coefficients[i] * model->Get(LowerBound(new_vars[i]));
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
const IntegerVariable sum = model->Add(NewIntegerVariable(sum_lb, sum_ub));
|
|
|
|
|
new_vars.push_back(sum);
|
2021-04-01 12:13:35 +02:00
|
|
|
std::vector<int64_t> new_coeffs(coefficients.begin(), coefficients.end());
|
2016-12-14 22:03:52 +01:00
|
|
|
new_coeffs.push_back(-1);
|
2016-09-22 15:18:08 +02:00
|
|
|
model->Add(FixedWeightedSum(new_vars, new_coeffs, 0));
|
2016-09-12 13:51:04 +02:00
|
|
|
return sum;
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-09-12 13:51:04 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Expresses the fact that an existing integer variable is equal to the minimum
|
|
|
|
|
// of other integer variables.
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> IsEqualToMinOf(
|
|
|
|
|
IntegerVariable min_var, const std::vector<IntegerVariable>& vars) {
|
|
|
|
|
return [=](Model* model) {
|
|
|
|
|
for (const IntegerVariable& var : vars) {
|
2020-10-22 23:36:58 +02:00
|
|
|
model->Add(LowerOrEqual(min_var, var));
|
|
|
|
|
}
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
MinPropagator* constraint =
|
2016-10-29 20:12:59 +02:00
|
|
|
new MinPropagator(vars, min_var, model->GetOrCreate<IntegerTrail>());
|
2016-09-12 13:51:04 +02:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-09-12 13:51:04 +02:00
|
|
|
}
|
|
|
|
|
|
2019-12-16 12:34:56 +01:00
|
|
|
// Expresses the fact that an existing integer variable is equal to the minimum
|
|
|
|
|
// of linear expressions. Assumes Canonical expressions (all positive
|
|
|
|
|
// coefficients).
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> IsEqualToMinOf(
|
|
|
|
|
const LinearExpression& min_expr,
|
|
|
|
|
const std::vector<LinearExpression>& exprs) {
|
|
|
|
|
return [=](Model* model) {
|
|
|
|
|
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
|
2019-12-16 12:34:56 +01:00
|
|
|
|
|
|
|
|
IntegerVariable min_var;
|
|
|
|
|
if (min_expr.vars.size() == 1 &&
|
2021-06-29 17:16:44 +02:00
|
|
|
std::abs(min_expr.coeffs[0].value()) == 1 && min_expr.offset == 0) {
|
2019-12-16 12:34:56 +01:00
|
|
|
if (min_expr.coeffs[0].value() == 1) {
|
|
|
|
|
min_var = min_expr.vars[0];
|
|
|
|
|
} else {
|
|
|
|
|
min_var = NegationOf(min_expr.vars[0]);
|
|
|
|
|
}
|
|
|
|
|
} else {
|
|
|
|
|
// Create a new variable if the expression is not just a single variable.
|
|
|
|
|
IntegerValue min_lb = LinExprLowerBound(min_expr, *integer_trail);
|
|
|
|
|
IntegerValue min_ub = LinExprUpperBound(min_expr, *integer_trail);
|
|
|
|
|
min_var = integer_trail->AddIntegerVariable(min_lb, min_ub);
|
|
|
|
|
|
|
|
|
|
// min_var = min_expr
|
|
|
|
|
std::vector<IntegerVariable> min_sum_vars = min_expr.vars;
|
2021-04-01 12:13:35 +02:00
|
|
|
std::vector<int64_t> min_sum_coeffs;
|
2019-12-16 12:34:56 +01:00
|
|
|
for (IntegerValue coeff : min_expr.coeffs) {
|
|
|
|
|
min_sum_coeffs.push_back(coeff.value());
|
|
|
|
|
}
|
|
|
|
|
min_sum_vars.push_back(min_var);
|
|
|
|
|
min_sum_coeffs.push_back(-1);
|
|
|
|
|
|
|
|
|
|
model->Add(FixedWeightedSum(min_sum_vars, min_sum_coeffs,
|
|
|
|
|
-min_expr.offset.value()));
|
|
|
|
|
}
|
2020-10-29 14:25:39 +01:00
|
|
|
for (const LinearExpression& expr : exprs) {
|
2019-12-16 12:34:56 +01:00
|
|
|
// min_var <= expr
|
|
|
|
|
std::vector<IntegerVariable> vars = expr.vars;
|
2021-04-01 12:13:35 +02:00
|
|
|
std::vector<int64_t> coeffs;
|
2019-12-16 12:34:56 +01:00
|
|
|
for (IntegerValue coeff : expr.coeffs) {
|
|
|
|
|
coeffs.push_back(coeff.value());
|
|
|
|
|
}
|
|
|
|
|
vars.push_back(min_var);
|
|
|
|
|
coeffs.push_back(-1);
|
|
|
|
|
model->Add(WeightedSumGreaterOrEqual(vars, coeffs, -expr.offset.value()));
|
|
|
|
|
}
|
|
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
LinMinPropagator* constraint = new LinMinPropagator(exprs, min_var, model);
|
2019-12-16 12:34:56 +01:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2019-12-16 12:34:56 +01:00
|
|
|
}
|
|
|
|
|
|
2016-09-12 13:51:04 +02:00
|
|
|
// Expresses the fact that an existing integer variable is equal to the maximum
|
|
|
|
|
// of other integer variables.
|
2020-10-29 14:25:39 +01:00
|
|
|
inline std::function<void(Model*)> IsEqualToMaxOf(
|
|
|
|
|
IntegerVariable max_var, const std::vector<IntegerVariable>& vars) {
|
|
|
|
|
return [=](Model* model) {
|
2020-10-22 23:36:58 +02:00
|
|
|
std::vector<IntegerVariable> negated_vars;
|
2020-10-29 14:25:39 +01:00
|
|
|
for (const IntegerVariable& var : vars) {
|
2016-09-12 13:51:04 +02:00
|
|
|
negated_vars.push_back(NegationOf(var));
|
|
|
|
|
model->Add(GreaterOrEqual(max_var, var));
|
|
|
|
|
}
|
|
|
|
|
|
2020-10-29 14:25:39 +01:00
|
|
|
MinPropagator* constraint = new MinPropagator(
|
2016-10-29 20:12:59 +02:00
|
|
|
negated_vars, NegationOf(max_var), model->GetOrCreate<IntegerTrail>());
|
2016-09-12 13:51:04 +02:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-09-12 13:51:04 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Expresses the fact that an existing integer variable is equal to one of
|
|
|
|
|
// the given values, each selected by a given literal.
|
2020-10-29 14:25:39 +01:00
|
|
|
std::function<void(Model*)> IsOneOf(IntegerVariable var,
|
|
|
|
|
const std::vector<Literal>& selectors,
|
|
|
|
|
const std::vector<IntegerValue>& values);
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2020-10-22 23:36:58 +02:00
|
|
|
template <class T>
|
2020-10-29 14:25:39 +01:00
|
|
|
void RegisterAndTransferOwnership(Model* model, T* ct) {
|
2017-04-26 17:30:25 +02:00
|
|
|
ct->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(ct);
|
|
|
|
|
}
|
2016-10-05 13:53:30 +02:00
|
|
|
// Adds the constraint: a * b = p.
|
2021-10-27 13:22:27 +02:00
|
|
|
inline std::function<void(Model*)> ProductConstraint(AffineExpression a,
|
|
|
|
|
AffineExpression b,
|
|
|
|
|
AffineExpression p) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
|
|
|
|
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
|
2017-07-21 11:13:10 -07:00
|
|
|
if (a == b) {
|
2021-10-27 13:22:27 +02:00
|
|
|
if (integer_trail->LowerBound(a) >= 0) {
|
2017-07-21 11:13:10 -07:00
|
|
|
RegisterAndTransferOwnership(model,
|
|
|
|
|
new SquarePropagator(a, p, integer_trail));
|
2021-10-27 13:22:27 +02:00
|
|
|
} else if (integer_trail->UpperBound(a) <= 0) {
|
2017-07-21 11:13:10 -07:00
|
|
|
RegisterAndTransferOwnership(
|
2021-10-27 13:22:27 +02:00
|
|
|
model, new SquarePropagator(a.Negated(), p, integer_trail));
|
2017-07-21 11:13:10 -07:00
|
|
|
} else {
|
|
|
|
|
LOG(FATAL) << "Not supported";
|
|
|
|
|
}
|
2021-10-27 13:22:27 +02:00
|
|
|
} else if (integer_trail->LowerBound(a) >= 0 &&
|
|
|
|
|
integer_trail->LowerBound(b) >= 0) {
|
2017-04-26 17:30:25 +02:00
|
|
|
RegisterAndTransferOwnership(
|
|
|
|
|
model, new PositiveProductPropagator(a, b, p, integer_trail));
|
2021-10-27 13:22:27 +02:00
|
|
|
} else if (integer_trail->LowerBound(a) >= 0 &&
|
|
|
|
|
integer_trail->UpperBound(b) <= 0) {
|
2017-04-26 17:30:25 +02:00
|
|
|
RegisterAndTransferOwnership(
|
2021-10-27 13:22:27 +02:00
|
|
|
model, new PositiveProductPropagator(a, b.Negated(), p.Negated(),
|
2017-04-26 17:30:25 +02:00
|
|
|
integer_trail));
|
2021-10-27 13:22:27 +02:00
|
|
|
} else if (integer_trail->UpperBound(a) <= 0 &&
|
|
|
|
|
integer_trail->LowerBound(b) >= 0) {
|
2017-04-26 17:30:25 +02:00
|
|
|
RegisterAndTransferOwnership(
|
2021-10-27 13:22:27 +02:00
|
|
|
model, new PositiveProductPropagator(a.Negated(), b, p.Negated(),
|
2017-04-26 17:30:25 +02:00
|
|
|
integer_trail));
|
2021-10-27 13:22:27 +02:00
|
|
|
} else if (integer_trail->UpperBound(a) <= 0 &&
|
|
|
|
|
integer_trail->UpperBound(b) <= 0) {
|
2017-04-26 17:30:25 +02:00
|
|
|
RegisterAndTransferOwnership(
|
2021-10-27 13:22:27 +02:00
|
|
|
model, new PositiveProductPropagator(a.Negated(), b.Negated(), p,
|
2017-04-26 17:30:25 +02:00
|
|
|
integer_trail));
|
|
|
|
|
} else {
|
2018-09-12 15:07:23 +02:00
|
|
|
LOG(FATAL) << "Not supported";
|
2017-04-26 17:30:25 +02:00
|
|
|
}
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
2021-10-27 13:22:27 +02:00
|
|
|
// Adds the constraint: num / denom = div. (denom > 0).
|
|
|
|
|
inline std::function<void(Model*)> DivisionConstraint(AffineExpression num,
|
|
|
|
|
AffineExpression denom,
|
|
|
|
|
AffineExpression div) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
|
|
|
|
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
|
2021-10-27 13:22:27 +02:00
|
|
|
DivisionPropagator* constraint;
|
|
|
|
|
if (integer_trail->UpperBound(denom) < 0) {
|
|
|
|
|
constraint = new DivisionPropagator(num.Negated(), denom.Negated(), div,
|
|
|
|
|
integer_trail);
|
|
|
|
|
|
|
|
|
|
} else {
|
|
|
|
|
constraint = new DivisionPropagator(num, denom, div, integer_trail);
|
|
|
|
|
}
|
2016-10-05 13:53:30 +02:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
2019-12-16 12:34:56 +01:00
|
|
|
// Adds the constraint: a / b = c where b is a constant.
|
2021-10-25 16:30:57 +02:00
|
|
|
inline std::function<void(Model*)> FixedDivisionConstraint(AffineExpression a,
|
2020-10-29 14:25:39 +01:00
|
|
|
IntegerValue b,
|
2021-10-25 16:30:57 +02:00
|
|
|
AffineExpression c) {
|
2020-10-29 14:25:39 +01:00
|
|
|
return [=](Model* model) {
|
|
|
|
|
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
|
|
|
|
|
FixedDivisionPropagator* constraint =
|
2021-10-25 16:30:57 +02:00
|
|
|
b > 0 ? new FixedDivisionPropagator(a, b, c, integer_trail)
|
|
|
|
|
: new FixedDivisionPropagator(a.Negated(), -b, c, integer_trail);
|
2019-02-28 13:30:01 +01:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
2020-10-22 23:36:58 +02:00
|
|
|
};
|
2019-02-28 13:30:01 +01:00
|
|
|
}
|
|
|
|
|
|
2020-10-22 23:36:58 +02:00
|
|
|
} // namespace sat
|
|
|
|
|
} // namespace operations_research
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2020-10-22 23:36:58 +02:00
|
|
|
#endif // OR_TOOLS_SAT_INTEGER_EXPR_H_
|
