2025-01-10 11:33:35 +01:00
|
|
|
// Copyright 2010-2025 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.
|
|
|
|
|
|
2025-11-05 10:23:28 +01:00
|
|
|
#ifndef ORTOOLS_SAT_INTEGER_EXPR_H_
|
|
|
|
|
#define ORTOOLS_SAT_INTEGER_EXPR_H_
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2022-02-15 18:00:11 +01:00
|
|
|
#include <cmath>
|
2021-03-04 18:26:01 +01:00
|
|
|
#include <cstdint>
|
2022-02-15 18:00:11 +01:00
|
|
|
#include <cstdlib>
|
2017-07-27 11:28:55 -07:00
|
|
|
#include <functional>
|
2023-09-13 18:16:28 +02:00
|
|
|
#include <memory>
|
2025-09-26 15:52:20 +02:00
|
|
|
#include <string>
|
2022-02-15 18:00:11 +01:00
|
|
|
#include <utility>
|
2017-07-27 11:28:55 -07:00
|
|
|
#include <vector>
|
|
|
|
|
|
2025-07-24 23:51:00 +02:00
|
|
|
#include "absl/base/attributes.h"
|
2023-05-24 11:42:11 +02:00
|
|
|
#include "absl/log/check.h"
|
2025-02-24 22:59:21 +01:00
|
|
|
#include "absl/log/log.h"
|
2022-02-15 18:00:11 +01:00
|
|
|
#include "absl/types/span.h"
|
2025-09-08 18:15:23 +02:00
|
|
|
#include "ortools/sat/enforcement.h"
|
|
|
|
|
#include "ortools/sat/enforcement_helper.h"
|
2017-04-26 17:30:25 +02:00
|
|
|
#include "ortools/sat/integer.h"
|
2024-12-04 17:47:10 +01:00
|
|
|
#include "ortools/sat/integer_base.h"
|
2020-02-03 16:21:57 +01:00
|
|
|
#include "ortools/sat/linear_constraint.h"
|
2022-09-23 18:09:18 +02:00
|
|
|
#include "ortools/sat/linear_propagation.h"
|
2017-04-26 17:30:25 +02:00
|
|
|
#include "ortools/sat/model.h"
|
2025-07-28 10:34:04 -07:00
|
|
|
#include "ortools/sat/old_precedences_propagator.h"
|
2017-04-26 17:30:25 +02:00
|
|
|
#include "ortools/sat/sat_base.h"
|
2023-05-24 11:42:11 +02:00
|
|
|
#include "ortools/sat/sat_parameters.pb.h"
|
2017-07-27 11:28:55 -07:00
|
|
|
#include "ortools/sat/sat_solver.h"
|
2022-02-07 14:31:18 +01:00
|
|
|
#include "ortools/util/strong_integers.h"
|
2022-02-15 18:00:11 +01:00
|
|
|
#include "ortools/util/time_limit.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
|
2023-03-22 19:37:00 +01:00
|
|
|
// checked at model validation time before this is even created. If
|
|
|
|
|
// use_int128 is true, then we actually do the computations that could overflow
|
|
|
|
|
// in 128 bits, so that we can deal with constraints that might overflow (like
|
|
|
|
|
// the one scaled from the LP relaxation). Note that we still use some
|
|
|
|
|
// preconditions, such that for each variable the difference between their
|
|
|
|
|
// bounds fit on an int64_t.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): Technically we could still have an int128 overflow since we
|
|
|
|
|
// sum n terms that cannot overflow but can still be pretty close to the limit.
|
|
|
|
|
// Make sure this never happens! For most problem though, because the variable
|
|
|
|
|
// bounds will be smaller than 10^9, we are pretty safe.
|
2018-09-12 15:07:23 +02:00
|
|
|
//
|
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.
|
2023-03-22 19:37:00 +01:00
|
|
|
template <bool use_int128 = false>
|
2024-07-10 17:41:32 +02:00
|
|
|
class LinearConstraintPropagator : public PropagatorInterface,
|
|
|
|
|
LazyReasonInterface {
|
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
|
2023-03-22 19:37:00 +01:00
|
|
|
// another LinearConstraintPropagator constraint on the negated variables.
|
2024-01-10 16:42:04 +01:00
|
|
|
LinearConstraintPropagator(absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
absl::Span<const IntegerVariable> vars,
|
|
|
|
|
absl::Span<const IntegerValue> coeffs,
|
2023-03-22 19:37:00 +01:00
|
|
|
IntegerValue upper_bound, Model* model);
|
2016-09-22 15:18:08 +02:00
|
|
|
|
2024-01-10 16:42:04 +01:00
|
|
|
// This version allow to std::move the memory from the LinearConstraint
|
|
|
|
|
// directly. It Only uses the upper bound. Id does not support
|
|
|
|
|
// enforcement_literals.
|
|
|
|
|
LinearConstraintPropagator(LinearConstraint ct, Model* model);
|
|
|
|
|
|
2025-09-26 15:52:20 +02:00
|
|
|
std::string LazyReasonName() const override {
|
|
|
|
|
return use_int128 ? "IntegerSumLE128" : "IntegerSumLE";
|
|
|
|
|
}
|
|
|
|
|
|
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();
|
|
|
|
|
|
2021-10-29 14:02:25 +02:00
|
|
|
// This is a pretty usage specific function. Returns the implied lower bound
|
2021-11-04 18:58:34 +01:00
|
|
|
// on target_var if the given integer literal is false (resp. true). If the
|
|
|
|
|
// variables do not appear both in the linear inequality, this returns two
|
|
|
|
|
// kMinIntegerValue.
|
2021-10-29 14:02:25 +02:00
|
|
|
std::pair<IntegerValue, IntegerValue> ConditionalLb(
|
2021-11-04 18:58:34 +01:00
|
|
|
IntegerLiteral integer_literal, IntegerVariable target_var) const;
|
2021-10-29 14:02:25 +02:00
|
|
|
|
2024-07-10 17:41:32 +02:00
|
|
|
// For LazyReasonInterface.
|
2025-10-16 13:28:10 +02:00
|
|
|
void Explain(int id, IntegerLiteral to_explain, IntegerReason* reason) final;
|
2024-07-10 17:41:32 +02:00
|
|
|
|
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();
|
|
|
|
|
|
2016-09-22 15:18:08 +02:00
|
|
|
const IntegerValue upper_bound_;
|
2017-04-26 17:30:25 +02:00
|
|
|
|
2023-09-13 18:16:28 +02:00
|
|
|
// To gain a bit on memory (since we might have many linear constraint),
|
|
|
|
|
// we share this amongst all of them. Note that this is not accessed by
|
|
|
|
|
// two different thread though. Also the vector are only used as "temporary"
|
|
|
|
|
// so they are okay to be shared.
|
|
|
|
|
struct Shared {
|
|
|
|
|
explicit Shared(Model* model)
|
|
|
|
|
: assignment(model->GetOrCreate<Trail>()->Assignment()),
|
|
|
|
|
integer_trail(model->GetOrCreate<IntegerTrail>()),
|
|
|
|
|
time_limit(model->GetOrCreate<TimeLimit>()),
|
2023-09-21 13:07:09 +02:00
|
|
|
rev_int_repository(model->GetOrCreate<RevIntRepository>()),
|
2023-09-13 18:16:28 +02:00
|
|
|
rev_integer_value_repository(
|
|
|
|
|
model->GetOrCreate<RevIntegerValueRepository>()) {}
|
|
|
|
|
|
|
|
|
|
const VariablesAssignment& assignment;
|
|
|
|
|
IntegerTrail* integer_trail;
|
|
|
|
|
TimeLimit* time_limit;
|
2023-09-21 13:07:09 +02:00
|
|
|
RevIntRepository* rev_int_repository;
|
2023-09-13 18:16:28 +02:00
|
|
|
RevIntegerValueRepository* rev_integer_value_repository;
|
|
|
|
|
|
|
|
|
|
// Parallel vectors.
|
|
|
|
|
std::vector<IntegerLiteral> integer_reason;
|
|
|
|
|
std::vector<IntegerValue> reason_coeffs;
|
|
|
|
|
};
|
|
|
|
|
Shared* shared_;
|
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).
|
2023-09-13 18:16:28 +02:00
|
|
|
const int size_;
|
2023-10-25 17:05:22 +02:00
|
|
|
const std::unique_ptr<IntegerVariable[]> vars_;
|
|
|
|
|
const std::unique_ptr<IntegerValue[]> coeffs_;
|
|
|
|
|
const std::unique_ptr<IntegerValue[]> max_variations_;
|
2017-04-26 17:30:25 +02:00
|
|
|
|
2023-09-13 18:16:28 +02:00
|
|
|
// This is just the negation of the enforcement literal and it never changes.
|
2016-09-12 13:51:04 +02:00
|
|
|
std::vector<Literal> literal_reason_;
|
|
|
|
|
};
|
|
|
|
|
|
2023-03-22 19:37:00 +01:00
|
|
|
using IntegerSumLE = LinearConstraintPropagator<false>;
|
|
|
|
|
using IntegerSumLE128 = LinearConstraintPropagator<true>;
|
|
|
|
|
|
2024-03-29 15:05:05 +01:00
|
|
|
// Explicit instantiations in integer_expr.cc.
|
|
|
|
|
extern template class LinearConstraintPropagator<true>;
|
|
|
|
|
extern template class LinearConstraintPropagator<false>;
|
|
|
|
|
|
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:
|
2024-12-16 14:09:39 +01:00
|
|
|
MinPropagator(std::vector<AffineExpression> vars, AffineExpression min_var,
|
|
|
|
|
IntegerTrail* integer_trail);
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2023-08-30 10:04:11 -04:00
|
|
|
// This type is neither copyable nor movable.
|
|
|
|
|
MinPropagator(const MinPropagator&) = delete;
|
|
|
|
|
MinPropagator& operator=(const MinPropagator&) = delete;
|
|
|
|
|
|
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:
|
2024-12-16 14:09:39 +01:00
|
|
|
const std::vector<AffineExpression> vars_;
|
|
|
|
|
const AffineExpression 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_;
|
|
|
|
|
};
|
|
|
|
|
|
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).
|
2025-08-31 14:07:56 +02:00
|
|
|
class GreaterThanMinOfExprsPropagator : public PropagatorInterface,
|
|
|
|
|
LazyReasonInterface {
|
2019-12-16 12:34:56 +01:00
|
|
|
public:
|
2025-08-31 14:07:56 +02:00
|
|
|
GreaterThanMinOfExprsPropagator(
|
|
|
|
|
absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
std::vector<LinearExpression> exprs, IntegerVariable min_var,
|
|
|
|
|
Model* model);
|
|
|
|
|
GreaterThanMinOfExprsPropagator(const GreaterThanMinOfExprsPropagator&) =
|
|
|
|
|
delete;
|
|
|
|
|
GreaterThanMinOfExprsPropagator& operator=(
|
|
|
|
|
const GreaterThanMinOfExprsPropagator&) = delete;
|
2019-12-16 12:34:56 +01:00
|
|
|
|
2025-09-26 15:52:20 +02:00
|
|
|
std::string LazyReasonName() const override {
|
|
|
|
|
return "GreaterThanMinOfExprsPropagator";
|
|
|
|
|
}
|
|
|
|
|
|
2019-12-16 12:34:56 +01:00
|
|
|
bool Propagate() final;
|
|
|
|
|
|
2024-07-10 17:41:32 +02:00
|
|
|
// For LazyReasonInterface.
|
2025-10-16 13:28:10 +02:00
|
|
|
void Explain(int id, IntegerLiteral to_explain, IntegerReason* reason) final;
|
2024-07-10 17:41:32 +02:00
|
|
|
|
2019-12-16 12:34:56 +01:00
|
|
|
private:
|
2025-08-31 14:07:56 +02:00
|
|
|
int RegisterWith(GenericLiteralWatcher* watcher);
|
|
|
|
|
|
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.
|
2024-07-10 17:41:32 +02:00
|
|
|
bool PropagateLinearUpperBound(int id, absl::Span<const IntegerVariable> vars,
|
|
|
|
|
absl::Span<const 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_;
|
2025-08-31 14:07:56 +02:00
|
|
|
IntegerTrail& integer_trail_;
|
2025-09-08 18:15:23 +02:00
|
|
|
EnforcementHelper& enforcement_helper_;
|
2025-08-31 14:07:56 +02:00
|
|
|
EnforcementId enforcement_id_;
|
2023-01-27 16:53:53 +01:00
|
|
|
std::vector<IntegerValue> max_variations_;
|
|
|
|
|
std::vector<IntegerValue> reason_coeffs_;
|
|
|
|
|
std::vector<IntegerLiteral> local_reason_;
|
2020-01-20 10:51:53 +01:00
|
|
|
std::vector<IntegerLiteral> integer_reason_for_unique_candidate_;
|
|
|
|
|
int rev_unique_candidate_ = 0;
|
2025-10-16 13:28:10 +02:00
|
|
|
|
|
|
|
|
std::vector<IntegerVariable> tmp_vars_;
|
|
|
|
|
std::vector<IntegerValue> tmp_coeffs_;
|
2019-12-16 12:34:56 +01:00
|
|
|
};
|
|
|
|
|
|
2021-10-27 20:56:28 +02:00
|
|
|
// Propagates a * b = p.
|
2016-10-05 13:53:30 +02:00
|
|
|
//
|
2021-10-27 20:56:28 +02:00
|
|
|
// The bounds [min, max] of a and b will be propagated perfectly, but not
|
|
|
|
|
// the bounds on p as this require more complex arithmetics.
|
|
|
|
|
class ProductPropagator : public PropagatorInterface {
|
2016-10-05 13:53:30 +02:00
|
|
|
public:
|
2025-07-24 23:51:00 +02:00
|
|
|
ProductPropagator(absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
AffineExpression a, AffineExpression b, AffineExpression p,
|
2025-07-26 21:29:40 +02:00
|
|
|
Model* model);
|
2016-10-05 13:53:30 +02:00
|
|
|
|
2023-08-30 10:04:11 -04:00
|
|
|
// This type is neither copyable nor movable.
|
|
|
|
|
ProductPropagator(const ProductPropagator&) = delete;
|
|
|
|
|
ProductPropagator& operator=(const ProductPropagator&) = delete;
|
|
|
|
|
|
2016-10-29 20:12:59 +02:00
|
|
|
bool Propagate() final;
|
2016-10-05 13:53:30 +02:00
|
|
|
|
|
|
|
|
private:
|
2025-07-26 21:29:40 +02:00
|
|
|
int RegisterWith(GenericLiteralWatcher* watcher);
|
|
|
|
|
|
2021-10-27 20:56:28 +02:00
|
|
|
// Maybe replace a_, b_ or c_ by their negation to simplify the cases.
|
|
|
|
|
bool CanonicalizeCases();
|
|
|
|
|
|
|
|
|
|
// Special case when all are >= 0.
|
|
|
|
|
// We use faster code and better reasons than the generic code.
|
|
|
|
|
bool PropagateWhenAllNonNegative();
|
|
|
|
|
|
|
|
|
|
// Internal helper, see code for more details.
|
|
|
|
|
bool PropagateMaxOnPositiveProduct(AffineExpression a, AffineExpression b,
|
|
|
|
|
IntegerValue min_p, IntegerValue max_p);
|
|
|
|
|
|
|
|
|
|
// Note that we might negate any two terms in CanonicalizeCases() during
|
|
|
|
|
// each propagation. This is fine.
|
|
|
|
|
AffineExpression a_;
|
|
|
|
|
AffineExpression b_;
|
|
|
|
|
AffineExpression p_;
|
2025-07-26 21:29:40 +02:00
|
|
|
const IntegerTrail& integer_trail_;
|
2025-09-08 18:15:23 +02:00
|
|
|
EnforcementHelper& enforcement_helper_;
|
2025-07-24 23:51:00 +02:00
|
|
|
EnforcementId enforcement_id_;
|
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:
|
2025-07-26 21:29:40 +02:00
|
|
|
DivisionPropagator(absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
AffineExpression num, AffineExpression denom,
|
|
|
|
|
AffineExpression div, Model* model);
|
2016-10-07 17:29:33 +02:00
|
|
|
|
2023-08-30 10:04:11 -04:00
|
|
|
// This type is neither copyable nor movable.
|
|
|
|
|
DivisionPropagator(const DivisionPropagator&) = delete;
|
|
|
|
|
DivisionPropagator& operator=(const DivisionPropagator&) = delete;
|
|
|
|
|
|
2016-10-29 20:12:59 +02:00
|
|
|
bool Propagate() final;
|
2016-10-07 17:29:33 +02:00
|
|
|
|
|
|
|
|
private:
|
2025-07-26 21:29:40 +02:00
|
|
|
int RegisterWith(GenericLiteralWatcher* watcher);
|
|
|
|
|
|
2021-10-27 13:22:27 +02:00
|
|
|
// Propagates the fact that the signs of each domain, if fixed, are
|
|
|
|
|
// compatible.
|
2023-10-12 10:06:27 +02:00
|
|
|
bool PropagateSigns(AffineExpression num, AffineExpression denom,
|
|
|
|
|
AffineExpression div);
|
2021-10-27 13:22:27 +02:00
|
|
|
|
|
|
|
|
// 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);
|
|
|
|
|
|
2025-09-08 18:15:23 +02:00
|
|
|
AffineExpression num_;
|
|
|
|
|
AffineExpression denom_;
|
2021-10-27 13:22:27 +02:00
|
|
|
const AffineExpression div_;
|
|
|
|
|
const AffineExpression negated_div_;
|
2025-07-26 21:29:40 +02:00
|
|
|
const IntegerTrail& integer_trail_;
|
2025-09-08 18:15:23 +02:00
|
|
|
EnforcementHelper& enforcement_helper_;
|
2025-07-26 21:29:40 +02:00
|
|
|
EnforcementId enforcement_id_;
|
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:
|
2025-07-26 21:29:40 +02:00
|
|
|
FixedDivisionPropagator(absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
AffineExpression a, IntegerValue b,
|
|
|
|
|
AffineExpression c, Model* model);
|
2019-02-28 13:30:01 +01:00
|
|
|
|
2023-08-30 10:04:11 -04:00
|
|
|
// This type is neither copyable nor movable.
|
|
|
|
|
FixedDivisionPropagator(const FixedDivisionPropagator&) = delete;
|
|
|
|
|
FixedDivisionPropagator& operator=(const FixedDivisionPropagator&) = delete;
|
|
|
|
|
|
2019-02-28 13:30:01 +01:00
|
|
|
bool Propagate() final;
|
|
|
|
|
|
|
|
|
|
private:
|
2025-07-26 21:29:40 +02:00
|
|
|
int RegisterWith(GenericLiteralWatcher* watcher);
|
|
|
|
|
|
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_;
|
2025-07-26 21:29:40 +02:00
|
|
|
const IntegerTrail& integer_trail_;
|
2025-09-08 18:15:23 +02:00
|
|
|
EnforcementHelper& enforcement_helper_;
|
2025-07-26 21:29:40 +02:00
|
|
|
EnforcementId enforcement_id_;
|
2019-02-28 13:30:01 +01:00
|
|
|
};
|
|
|
|
|
|
2021-10-28 15:44:12 +02:00
|
|
|
// Propagates target == expr % mod. Basic version, we don't extract any special
|
|
|
|
|
// cases, and we only propagates the bounds. mod must be > 0.
|
2021-10-27 20:56:28 +02:00
|
|
|
class FixedModuloPropagator : public PropagatorInterface {
|
|
|
|
|
public:
|
2025-07-26 21:29:40 +02:00
|
|
|
FixedModuloPropagator(absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
AffineExpression expr, IntegerValue mod,
|
|
|
|
|
AffineExpression target, Model* model);
|
2021-10-27 20:56:28 +02:00
|
|
|
|
2023-08-30 10:04:11 -04:00
|
|
|
// This type is neither copyable nor movable.
|
|
|
|
|
FixedModuloPropagator(const FixedModuloPropagator&) = delete;
|
|
|
|
|
FixedModuloPropagator& operator=(const FixedModuloPropagator&) = delete;
|
|
|
|
|
|
2021-10-27 20:56:28 +02:00
|
|
|
bool Propagate() final;
|
|
|
|
|
|
|
|
|
|
private:
|
2025-07-26 21:29:40 +02:00
|
|
|
int RegisterWith(GenericLiteralWatcher* watcher);
|
|
|
|
|
|
|
|
|
|
bool PropagateWhenFalseAndTargetIsPositive(AffineExpression expr,
|
|
|
|
|
AffineExpression target);
|
|
|
|
|
bool PropagateWhenFalseAndTargetDomainContainsZero();
|
2021-10-27 20:56:28 +02:00
|
|
|
bool PropagateSignsAndTargetRange();
|
2025-07-26 21:29:40 +02:00
|
|
|
bool PropagateBoundsWhenExprIsNonNegative(AffineExpression expr,
|
|
|
|
|
AffineExpression target);
|
2021-10-27 20:56:28 +02:00
|
|
|
bool PropagateOuterBounds();
|
|
|
|
|
|
|
|
|
|
const AffineExpression expr_;
|
|
|
|
|
const IntegerValue mod_;
|
|
|
|
|
const AffineExpression target_;
|
|
|
|
|
const AffineExpression negated_expr_;
|
|
|
|
|
const AffineExpression negated_target_;
|
2025-07-26 21:29:40 +02:00
|
|
|
const IntegerTrail& integer_trail_;
|
2025-09-08 18:15:23 +02:00
|
|
|
EnforcementHelper& enforcement_helper_;
|
2025-07-26 21:29:40 +02:00
|
|
|
EnforcementId enforcement_id_;
|
2021-10-27 20:56:28 +02:00
|
|
|
};
|
|
|
|
|
|
2017-07-21 11:13:10 -07:00
|
|
|
// Propagates x * x = s.
|
|
|
|
|
// TODO(user): Only works for x nonnegative.
|
|
|
|
|
class SquarePropagator : public PropagatorInterface {
|
|
|
|
|
public:
|
2025-07-24 23:51:00 +02:00
|
|
|
SquarePropagator(absl::Span<const Literal> enforcement_literals,
|
2025-07-26 21:29:40 +02:00
|
|
|
AffineExpression x, AffineExpression s, Model* model);
|
2017-07-21 11:13:10 -07:00
|
|
|
|
2023-08-30 10:04:11 -04:00
|
|
|
// This type is neither copyable nor movable.
|
|
|
|
|
SquarePropagator(const SquarePropagator&) = delete;
|
|
|
|
|
SquarePropagator& operator=(const SquarePropagator&) = delete;
|
|
|
|
|
|
2017-07-21 11:13:10 -07:00
|
|
|
bool Propagate() final;
|
|
|
|
|
|
|
|
|
|
private:
|
2025-07-26 21:29:40 +02:00
|
|
|
int RegisterWith(GenericLiteralWatcher* watcher);
|
2025-07-24 23:51:00 +02:00
|
|
|
|
2021-10-27 13:22:27 +02:00
|
|
|
const AffineExpression x_;
|
|
|
|
|
const AffineExpression s_;
|
2025-07-26 21:29:40 +02:00
|
|
|
const IntegerTrail& integer_trail_;
|
2025-09-08 18:15:23 +02:00
|
|
|
EnforcementHelper& enforcement_helper_;
|
2025-07-24 23:51:00 +02:00
|
|
|
EnforcementId enforcement_id_;
|
2017-07-21 11:13:10 -07:00
|
|
|
};
|
|
|
|
|
|
2016-09-12 13:51:04 +02:00
|
|
|
// =============================================================================
|
|
|
|
|
// Model based functions.
|
|
|
|
|
// =============================================================================
|
|
|
|
|
|
2018-09-12 15:07:23 +02:00
|
|
|
// enforcement_literals => sum <= upper_bound
|
2024-03-26 12:35:12 +01:00
|
|
|
inline void AddWeightedSumLowerOrEqual(
|
|
|
|
|
absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
absl::Span<const IntegerVariable> vars,
|
2025-10-16 13:28:10 +02:00
|
|
|
absl::Span<const IntegerValue> coefficients, int64_t upper_bound,
|
|
|
|
|
Model* model) {
|
2024-03-26 12:35:12 +01:00
|
|
|
// Linear1.
|
|
|
|
|
DCHECK_GE(vars.size(), 1);
|
2016-12-14 22:03:52 +01:00
|
|
|
if (vars.size() == 1) {
|
2024-03-26 12:35:12 +01:00
|
|
|
DCHECK_NE(coefficients[0], 0);
|
|
|
|
|
IntegerVariable var = vars[0];
|
|
|
|
|
IntegerValue coeff(coefficients[0]);
|
|
|
|
|
if (coeff < 0) {
|
|
|
|
|
var = NegationOf(var);
|
|
|
|
|
coeff = -coeff;
|
|
|
|
|
}
|
|
|
|
|
const IntegerValue rhs = FloorRatio(IntegerValue(upper_bound), coeff);
|
|
|
|
|
if (enforcement_literals.empty()) {
|
2026-02-26 16:45:05 +01:00
|
|
|
AddLowerOrEqual(var, rhs.value(), model);
|
2017-03-28 16:11:06 +02:00
|
|
|
} else {
|
2026-02-26 16:45:05 +01:00
|
|
|
AddImplication(enforcement_literals,
|
|
|
|
|
IntegerLiteral::LowerOrEqual(var, rhs), model);
|
2017-03-28 16:11:06 +02:00
|
|
|
}
|
2024-03-26 12:35:12 +01:00
|
|
|
return;
|
2016-12-14 22:03:52 +01:00
|
|
|
}
|
2019-08-22 13:15:49 +02:00
|
|
|
|
2024-03-26 12:35:12 +01:00
|
|
|
// Detect precedences with 2 and 3 terms.
|
|
|
|
|
const SatParameters& params = *model->GetOrCreate<SatParameters>();
|
|
|
|
|
if (!params.new_linear_propagation()) {
|
|
|
|
|
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
|
|
|
|
|
(coefficients[1] == 1 || coefficients[1] == -1)) {
|
|
|
|
|
AddConditionalSum2LowerOrEqual(
|
|
|
|
|
enforcement_literals,
|
|
|
|
|
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
|
|
|
|
|
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound,
|
|
|
|
|
model);
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
|
|
|
|
|
(coefficients[1] == 1 || coefficients[1] == -1) &&
|
|
|
|
|
(coefficients[2] == 1 || coefficients[2] == -1)) {
|
|
|
|
|
AddConditionalSum3LowerOrEqual(
|
|
|
|
|
enforcement_literals,
|
|
|
|
|
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,
|
|
|
|
|
model);
|
|
|
|
|
return;
|
2022-09-23 18:09:18 +02:00
|
|
|
}
|
2024-03-26 12:35:12 +01:00
|
|
|
}
|
2022-09-23 18:09:18 +02:00
|
|
|
|
2024-03-26 12:35:12 +01:00
|
|
|
// If value == min(expression), then we can avoid creating the sum.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): Deal with the case with no enforcement literal, in case the
|
|
|
|
|
// presolve was turned off?
|
|
|
|
|
if (!enforcement_literals.empty()) {
|
2019-08-22 13:15:49 +02:00
|
|
|
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
|
2024-01-31 14:44:02 +01:00
|
|
|
? integer_trail->LevelZeroLowerBound(vars[i])
|
|
|
|
|
: integer_trail->LevelZeroUpperBound(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) {
|
2024-01-31 14:44:02 +01:00
|
|
|
const IntegerValue lb = integer_trail->LevelZeroLowerBound(vars[i]);
|
2020-11-25 22:38:26 +01:00
|
|
|
non_cached_min += coefficients[i] * lb;
|
2026-02-26 16:45:05 +01:00
|
|
|
AddImplication(enforcement_literals,
|
|
|
|
|
IntegerLiteral::LowerOrEqual(vars[i], lb), model);
|
2019-08-22 13:15:49 +02:00
|
|
|
} else if (coefficients[i] < 0) {
|
2024-01-31 14:44:02 +01:00
|
|
|
const IntegerValue ub = integer_trail->LevelZeroUpperBound(vars[i]);
|
2020-11-25 22:38:26 +01:00
|
|
|
non_cached_min += coefficients[i] * ub;
|
2026-02-26 16:45:05 +01:00
|
|
|
AddImplication(enforcement_literals,
|
|
|
|
|
IntegerLiteral::GreaterOrEqual(vars[i], ub), model);
|
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());
|
|
|
|
|
}
|
2026-02-26 16:45:05 +01:00
|
|
|
AddClauseConstraint(clause, model);
|
2020-11-25 22:38:26 +01:00
|
|
|
}
|
2024-03-26 12:35:12 +01:00
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (params.new_linear_propagation()) {
|
|
|
|
|
const bool ok = model->GetOrCreate<LinearPropagator>()->AddConstraint(
|
2025-10-16 13:28:10 +02:00
|
|
|
enforcement_literals, vars, coefficients, IntegerValue(upper_bound));
|
2024-03-26 12:35:12 +01:00
|
|
|
if (!ok) {
|
|
|
|
|
auto* sat_solver = model->GetOrCreate<SatSolver>();
|
|
|
|
|
if (sat_solver->CurrentDecisionLevel() == 0) {
|
|
|
|
|
sat_solver->NotifyThatModelIsUnsat();
|
2022-09-23 18:09:18 +02:00
|
|
|
} else {
|
2024-03-26 12:35:12 +01:00
|
|
|
LOG(FATAL) << "We currently do not support adding conflicting "
|
|
|
|
|
"constraint at positive level.";
|
2022-09-23 18:09:18 +02:00
|
|
|
}
|
2019-08-22 13:15:49 +02:00
|
|
|
}
|
2024-03-26 12:35:12 +01:00
|
|
|
} else {
|
2025-10-16 13:28:10 +02:00
|
|
|
IntegerSumLE* constraint =
|
|
|
|
|
new IntegerSumLE(enforcement_literals, vars, coefficients,
|
|
|
|
|
IntegerValue(upper_bound), model);
|
2024-03-26 12:35:12 +01:00
|
|
|
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
|
|
|
|
|
model->TakeOwnership(constraint);
|
|
|
|
|
}
|
2016-10-13 10:44:35 -07:00
|
|
|
}
|
|
|
|
|
|
2018-09-12 15:07:23 +02:00
|
|
|
// enforcement_literals => sum >= lower_bound
|
2024-03-26 12:35:12 +01:00
|
|
|
inline void AddWeightedSumGreaterOrEqual(
|
|
|
|
|
absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
absl::Span<const IntegerVariable> vars,
|
2025-10-16 13:28:10 +02:00
|
|
|
absl::Span<const IntegerValue> coefficients, int64_t lower_bound,
|
|
|
|
|
Model* model) {
|
2016-10-13 10:44:35 -07:00
|
|
|
// We just negate everything and use an <= constraint.
|
2025-10-16 13:28:10 +02:00
|
|
|
std::vector<IntegerValue> negated_coeffs(coefficients.begin(),
|
|
|
|
|
coefficients.end());
|
|
|
|
|
for (IntegerValue& ref : negated_coeffs) ref = -ref;
|
2024-03-26 12:35:12 +01:00
|
|
|
AddWeightedSumLowerOrEqual(enforcement_literals, vars, negated_coeffs,
|
|
|
|
|
-lower_bound, model);
|
2016-10-13 10:44:35 -07:00
|
|
|
}
|
|
|
|
|
|
2025-10-16 13:28:10 +02:00
|
|
|
// Weighted sum <= constant.
|
|
|
|
|
template <typename VectorInt>
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddWeightedSumLowerOrEqual(absl::Span<const IntegerVariable> vars,
|
|
|
|
|
const VectorInt& coefficients,
|
|
|
|
|
int64_t upper_bound, Model* model) {
|
|
|
|
|
std::vector<IntegerValue> local_coeffs(coefficients.begin(),
|
|
|
|
|
coefficients.end());
|
|
|
|
|
AddWeightedSumLowerOrEqual({}, vars, local_coeffs, upper_bound, model);
|
2025-10-16 13:28:10 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// Weighted sum >= constant.
|
|
|
|
|
template <typename VectorInt>
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddWeightedSumGreaterOrEqual(absl::Span<const IntegerVariable> vars,
|
|
|
|
|
const VectorInt& coefficients,
|
|
|
|
|
int64_t lower_bound, Model* model) {
|
2025-10-16 13:28:10 +02:00
|
|
|
// We just negate everything and use an <= constraints.
|
|
|
|
|
std::vector<IntegerValue> negated_coeffs(coefficients.begin(),
|
|
|
|
|
coefficients.end());
|
|
|
|
|
for (IntegerValue& ref : negated_coeffs) ref = -ref;
|
2026-02-26 16:45:05 +01:00
|
|
|
AddWeightedSumLowerOrEqual({}, vars, negated_coeffs, -lower_bound, model);
|
2025-10-16 13:28:10 +02:00
|
|
|
}
|
|
|
|
|
|
2026-02-26 16:45:05 +01:00
|
|
|
// Weighted sum == constant.
|
2025-10-16 13:28:10 +02:00
|
|
|
// Weighted sum == constant.
|
|
|
|
|
template <typename VectorInt>
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddFixedWeightedSum(absl::Span<const IntegerVariable> vars,
|
|
|
|
|
const VectorInt& coefficients, int64_t value,
|
|
|
|
|
Model* model) {
|
|
|
|
|
AddWeightedSumGreaterOrEqual(vars, coefficients, value, model);
|
|
|
|
|
AddWeightedSumLowerOrEqual(vars, coefficients, value, model);
|
2025-10-16 13:28:10 +02:00
|
|
|
}
|
|
|
|
|
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddConditionalWeightedSumLowerOrEqual(
|
2025-01-28 13:34:07 +01:00
|
|
|
absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
absl::Span<const IntegerVariable> vars,
|
2026-02-26 16:45:05 +01:00
|
|
|
absl::Span<const int64_t> coefficients, int64_t upper_bound, Model* model) {
|
|
|
|
|
std::vector<IntegerValue> local_coeffs(coefficients.begin(),
|
|
|
|
|
coefficients.end());
|
|
|
|
|
AddWeightedSumLowerOrEqual(enforcement_literals, vars, local_coeffs,
|
|
|
|
|
upper_bound, model);
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
2026-02-26 16:45:05 +01:00
|
|
|
|
|
|
|
|
inline void AddConditionalWeightedSumGreaterOrEqual(
|
2024-12-13 14:50:57 +01:00
|
|
|
absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
absl::Span<const IntegerVariable> vars,
|
2026-02-26 16:45:05 +01:00
|
|
|
absl::Span<const int64_t> coefficients, int64_t upper_bound, Model* model) {
|
|
|
|
|
std::vector<IntegerValue> local_coeffs(coefficients.begin(),
|
|
|
|
|
coefficients.end());
|
|
|
|
|
AddWeightedSumGreaterOrEqual(enforcement_literals, vars, local_coeffs,
|
|
|
|
|
upper_bound, model);
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
2020-02-03 16:21:57 +01:00
|
|
|
// LinearConstraint version.
|
|
|
|
|
inline void LoadConditionalLinearConstraint(
|
|
|
|
|
const absl::Span<const Literal> enforcement_literals,
|
2020-10-29 14:25:39 +01:00
|
|
|
const LinearConstraint& cst, Model* model) {
|
2024-01-10 16:42:04 +01:00
|
|
|
if (cst.num_terms == 0) {
|
2020-10-22 23:36:58 +02:00
|
|
|
if (cst.lb <= 0 && cst.ub >= 0) return;
|
2023-02-20 17:00:17 +01:00
|
|
|
|
|
|
|
|
// The enforcement literals cannot be all at true.
|
|
|
|
|
std::vector<Literal> clause;
|
|
|
|
|
for (const Literal lit : enforcement_literals) {
|
|
|
|
|
clause.push_back(lit.Negated());
|
|
|
|
|
}
|
2026-02-26 16:45:05 +01:00
|
|
|
return AddClauseConstraint(clause, model);
|
2020-02-03 16:21:57 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (cst.ub < kMaxIntegerValue) {
|
2025-10-16 13:28:10 +02:00
|
|
|
AddWeightedSumLowerOrEqual(enforcement_literals, cst.VarsAsSpan(),
|
|
|
|
|
cst.CoeffsAsSpan(), cst.ub.value(), model);
|
2020-02-03 16:21:57 +01:00
|
|
|
}
|
|
|
|
|
if (cst.lb > kMinIntegerValue) {
|
2025-10-16 13:28:10 +02:00
|
|
|
AddWeightedSumGreaterOrEqual(enforcement_literals, cst.VarsAsSpan(),
|
|
|
|
|
cst.CoeffsAsSpan(), cst.lb.value(), model);
|
2020-02-03 16:21:57 +01:00
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
2024-04-05 11:35:18 +02:00
|
|
|
inline void LoadLinearConstraint(const LinearConstraint& cst, Model* model) {
|
|
|
|
|
LoadConditionalLinearConstraint({}, cst, model);
|
|
|
|
|
}
|
|
|
|
|
|
2022-12-12 17:19:20 +01:00
|
|
|
inline void AddConditionalAffinePrecedence(
|
2024-04-05 11:35:18 +02:00
|
|
|
const absl::Span<const Literal> enforcement_literals, AffineExpression left,
|
2022-12-12 17:19:20 +01:00
|
|
|
AffineExpression right, Model* model) {
|
|
|
|
|
LinearConstraintBuilder builder(model, kMinIntegerValue, 0);
|
|
|
|
|
builder.AddTerm(left, 1);
|
|
|
|
|
builder.AddTerm(right, -1);
|
|
|
|
|
LoadConditionalLinearConstraint(enforcement_literals, builder.Build(), model);
|
|
|
|
|
}
|
|
|
|
|
|
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>
|
2026-02-26 16:45:05 +01:00
|
|
|
inline IntegerVariable AddNewWeightedSum(
|
|
|
|
|
const VectorInt& coefficients, const std::vector<IntegerVariable>& vars,
|
|
|
|
|
Model* model) {
|
|
|
|
|
std::vector<IntegerVariable> new_vars = vars;
|
|
|
|
|
// To avoid overflow in the FixedWeightedSum() constraint, we need to
|
|
|
|
|
// compute the basic bounds on the sum.
|
|
|
|
|
//
|
|
|
|
|
// TODO(user): deal with overflow here too!
|
|
|
|
|
int64_t sum_lb(0);
|
|
|
|
|
int64_t sum_ub(0);
|
|
|
|
|
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]));
|
2016-09-22 15:18:08 +02:00
|
|
|
}
|
2026-02-26 16:45:05 +01:00
|
|
|
}
|
2016-09-22 15:18:08 +02:00
|
|
|
|
2026-02-26 16:45:05 +01:00
|
|
|
const IntegerVariable sum = model->Add(NewIntegerVariable(sum_lb, sum_ub));
|
|
|
|
|
new_vars.push_back(sum);
|
|
|
|
|
std::vector<int64_t> new_coeffs(coefficients.begin(), coefficients.end());
|
|
|
|
|
new_coeffs.push_back(-1);
|
|
|
|
|
AddFixedWeightedSum(new_vars, new_coeffs, 0, model);
|
|
|
|
|
return sum;
|
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).
|
2025-08-31 14:07:56 +02:00
|
|
|
inline void AddIsEqualToMinOf(
|
|
|
|
|
const absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
const LinearExpression& min_expr, std::vector<LinearExpression> exprs,
|
|
|
|
|
Model* model) {
|
2024-12-13 13:10:35 +01:00
|
|
|
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
|
|
|
|
|
|
|
|
|
|
IntegerVariable min_var;
|
|
|
|
|
if (min_expr.vars.size() == 1 && std::abs(min_expr.coeffs[0].value()) == 1 &&
|
|
|
|
|
min_expr.offset == 0) {
|
|
|
|
|
if (min_expr.coeffs[0].value() == 1) {
|
|
|
|
|
min_var = min_expr.vars[0];
|
2019-12-16 12:34:56 +01:00
|
|
|
} else {
|
2024-12-13 13:10:35 +01:00
|
|
|
min_var = NegationOf(min_expr.vars[0]);
|
2019-12-16 12:34:56 +01:00
|
|
|
}
|
2024-12-13 13:10:35 +01:00
|
|
|
} else {
|
|
|
|
|
// Create a new variable if the expression is not just a single variable.
|
|
|
|
|
IntegerValue min_lb = min_expr.Min(*integer_trail);
|
|
|
|
|
IntegerValue min_ub = min_expr.Max(*integer_trail);
|
|
|
|
|
min_var = integer_trail->AddIntegerVariable(min_lb, min_ub);
|
|
|
|
|
|
|
|
|
|
// min_var = min_expr
|
|
|
|
|
LinearConstraintBuilder builder(0, 0);
|
|
|
|
|
builder.AddLinearExpression(min_expr, 1);
|
|
|
|
|
builder.AddTerm(min_var, -1);
|
|
|
|
|
LoadLinearConstraint(builder.Build(), model);
|
|
|
|
|
}
|
2024-12-16 14:09:39 +01:00
|
|
|
|
2025-08-31 14:07:56 +02:00
|
|
|
// Add for all i, enforcement_literals => min <= exprs[i].
|
2024-12-13 13:10:35 +01:00
|
|
|
for (const LinearExpression& expr : exprs) {
|
|
|
|
|
LinearConstraintBuilder builder(0, kMaxIntegerValue);
|
|
|
|
|
builder.AddLinearExpression(expr, 1);
|
|
|
|
|
builder.AddTerm(min_var, -1);
|
2025-08-31 14:07:56 +02:00
|
|
|
LoadConditionalLinearConstraint(enforcement_literals, builder.Build(),
|
|
|
|
|
model);
|
2024-12-13 13:10:35 +01:00
|
|
|
}
|
2019-12-16 12:34:56 +01:00
|
|
|
|
2025-08-31 14:07:56 +02:00
|
|
|
GreaterThanMinOfExprsPropagator* constraint =
|
|
|
|
|
new GreaterThanMinOfExprsPropagator(enforcement_literals,
|
|
|
|
|
std::move(exprs), min_var, model);
|
2024-12-13 13:10:35 +01:00
|
|
|
model->TakeOwnership(constraint);
|
2019-12-16 12:34:56 +01:00
|
|
|
}
|
|
|
|
|
|
2016-10-05 13:53:30 +02:00
|
|
|
// Adds the constraint: a * b = p.
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddProductConstraint(absl::Span<const Literal> enforcement_literals,
|
|
|
|
|
AffineExpression a, AffineExpression b,
|
|
|
|
|
AffineExpression p, Model* model) {
|
|
|
|
|
const IntegerTrail& integer_trail = *model->GetOrCreate<IntegerTrail>();
|
|
|
|
|
// TODO(user): return early if constraint is never enforced.
|
|
|
|
|
if (a == b) {
|
|
|
|
|
if (integer_trail.LowerBound(a) >= 0) {
|
|
|
|
|
model->TakeOwnership(
|
|
|
|
|
new SquarePropagator(enforcement_literals, a, p, model));
|
|
|
|
|
return;
|
2017-04-26 17:30:25 +02:00
|
|
|
}
|
2026-02-26 16:45:05 +01:00
|
|
|
if (integer_trail.UpperBound(a) <= 0) {
|
|
|
|
|
model->TakeOwnership(
|
|
|
|
|
new SquarePropagator(enforcement_literals, a.Negated(), p, model));
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
model->TakeOwnership(
|
|
|
|
|
new ProductPropagator(enforcement_literals, a, b, p, model));
|
2016-10-05 13:53:30 +02:00
|
|
|
}
|
|
|
|
|
|
2021-10-27 13:22:27 +02:00
|
|
|
// Adds the constraint: num / denom = div. (denom > 0).
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddDivisionConstraint(
|
2025-07-26 21:29:40 +02:00
|
|
|
absl::Span<const Literal> enforcement_literals, AffineExpression num,
|
2026-02-26 16:45:05 +01:00
|
|
|
AffineExpression denom, AffineExpression div, Model* model) {
|
|
|
|
|
const IntegerTrail& integer_trail = *model->GetOrCreate<IntegerTrail>();
|
|
|
|
|
// TODO(user): return early if constraint is never enforced.
|
|
|
|
|
DivisionPropagator* constraint;
|
|
|
|
|
if (integer_trail.UpperBound(denom) < 0) {
|
|
|
|
|
constraint = new DivisionPropagator(enforcement_literals, num.Negated(),
|
|
|
|
|
denom.Negated(), div, model);
|
|
|
|
|
} else {
|
|
|
|
|
constraint =
|
|
|
|
|
new DivisionPropagator(enforcement_literals, num, denom, div, model);
|
|
|
|
|
}
|
|
|
|
|
model->TakeOwnership(constraint);
|
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.
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddFixedDivisionConstraint(
|
2025-07-26 21:29:40 +02:00
|
|
|
absl::Span<const Literal> enforcement_literals, AffineExpression a,
|
2026-02-26 16:45:05 +01:00
|
|
|
IntegerValue b, AffineExpression c, Model* model) {
|
|
|
|
|
// TODO(user): return early if constraint is never enforced.
|
|
|
|
|
FixedDivisionPropagator* constraint =
|
|
|
|
|
b > 0 ? new FixedDivisionPropagator(enforcement_literals, a, b, c, model)
|
2025-07-26 21:29:40 +02:00
|
|
|
: new FixedDivisionPropagator(enforcement_literals, a.Negated(), -b,
|
|
|
|
|
c, model);
|
2026-02-26 16:45:05 +01:00
|
|
|
model->TakeOwnership(constraint);
|
2019-02-28 13:30:01 +01:00
|
|
|
}
|
|
|
|
|
|
2021-10-27 20:56:28 +02:00
|
|
|
// Adds the constraint: a % b = c where b is a constant.
|
2026-02-26 16:45:05 +01:00
|
|
|
inline void AddFixedModuloConstraint(
|
2025-07-26 21:29:40 +02:00
|
|
|
absl::Span<const Literal> enforcement_literals, AffineExpression a,
|
2026-02-26 16:45:05 +01:00
|
|
|
IntegerValue b, AffineExpression c, Model* model) {
|
|
|
|
|
model->TakeOwnership(
|
|
|
|
|
new FixedModuloPropagator(enforcement_literals, a, b, c, model));
|
2021-10-27 20:56:28 +02:00
|
|
|
}
|
|
|
|
|
|
2020-10-22 23:36:58 +02:00
|
|
|
} // namespace sat
|
|
|
|
|
} // namespace operations_research
|
2016-09-12 13:51:04 +02:00
|
|
|
|
2025-11-05 10:23:28 +01:00
|
|
|
#endif // ORTOOLS_SAT_INTEGER_EXPR_H_
|
