14#ifndef OR_TOOLS_SAT_INTEGER_H_
15#define OR_TOOLS_SAT_INTEGER_H_
26#include "absl/container/flat_hash_map.h"
27#include "absl/container/inlined_vector.h"
28#include "absl/strings/str_cat.h"
29#include "absl/types/span.h"
70 const double kInfinity = std::numeric_limits<double>::infinity();
73 return static_cast<double>(
value.value());
76template <
class IntType>
78 return IntType(std::abs(t.value()));
82 IntegerValue positive_divisor) {
84 const IntegerValue result = dividend / positive_divisor;
85 const IntegerValue adjust =
86 static_cast<IntegerValue
>(result * positive_divisor < dividend);
87 return result + adjust;
91 IntegerValue positive_divisor) {
93 const IntegerValue result = dividend / positive_divisor;
94 const IntegerValue adjust =
95 static_cast<IntegerValue
>(result * positive_divisor > dividend);
96 return result - adjust;
103 IntegerValue positive_divisor) {
105 const IntegerValue m = dividend % positive_divisor;
106 return m < 0 ? m + positive_divisor : m;
115 *result = IntegerValue(add);
127 return IntegerVariable(i.value() ^ 1);
131 return (i.value() & 1) == 0;
135 return IntegerVariable(i.value() & (~1));
141 return PositiveOnlyIndex(
var.value() / 2);
146 const std::vector<IntegerVariable>& vars);
184 ? absl::StrCat(
"I",
var.value() / 2,
">=",
bound.value())
185 : absl::StrCat(
"I",
var.value() / 2,
"<=", -
bound.value());
190 IntegerValue
bound = IntegerValue(0);
241 IntegerValue
coeff = IntegerValue(0);
281 num_created_variables_(0) {}
284 VLOG(1) <<
"#variables created = " << num_created_variables_;
333 IntegerVariable
var)
const;
377 IntegerValue
value)
const;
391 if (lit.
Index() >= reverse_encoding_.
size()) {
392 return empty_integer_literal_vector_;
394 return reverse_encoding_[lit.
Index()];
401 if (lit.
Index() >= full_reverse_encoding_.
size()) {
402 return empty_integer_literal_vector_;
404 return full_reverse_encoding_[lit.
Index()];
410 return newly_fixed_integer_literals_;
413 newly_fixed_integer_literals_.clear();
422 return literal_view_[lit.
Index()];
441 IntegerValue*
bound)
const;
449 literal_index_true_ = literal_true.
Index();
452 return Literal(literal_index_true_);
460 IntegerVariable
var)
const {
461 if (
var >= encoding_by_var_.size()) {
462 return std::map<IntegerValue, Literal>();
464 return encoding_by_var_[
var];
480 void AddImplications(
const std::map<IntegerValue, Literal>& map,
481 std::map<IntegerValue, Literal>::const_iterator it,
487 bool add_implications_ =
true;
488 int64 num_created_variables_ = 0;
504 full_reverse_encoding_;
505 std::vector<IntegerLiteral> newly_fixed_integer_literals_;
517 absl::flat_hash_map<std::pair<PositiveOnlyIndex, IntegerValue>,
Literal>
518 equality_to_associated_literal_;
532 std::vector<IntegerValue> tmp_values_;
547 parameters_(*
model->GetOrCreate<SatParameters>()) {
557 void Untrail(const
Trail& trail,
int literal_trail_index) final;
559 int trail_index) const final;
566 return IntegerVariable(vars_.
size());
582 IntegerValue upper_bound);
626 const LiteralIndex is_ignored_literal = is_ignored_literals_[i];
632 return Literal(is_ignored_literals_[i]);
641 is_ignored_literals_[i] == is_considered.
NegatedIndex());
647 IntegerValue
LowerBound(IntegerVariable i)
const;
648 IntegerValue
UpperBound(IntegerVariable i)
const;
651 bool IsFixed(IntegerVariable i)
const;
695 absl::Span<const IntegerValue> coeffs,
696 std::vector<IntegerLiteral>* reason)
const;
700 absl::Span<const IntegerValue> coeffs,
701 absl::Span<const IntegerVariable> vars,
702 std::vector<IntegerLiteral>* reason)
const;
706 absl::Span<const IntegerValue> coeffs,
707 std::vector<int>* trail_indices)
const;
730 ABSL_MUST_USE_RESULT
bool Enqueue(
732 absl::Span<const IntegerLiteral> integer_reason);
742 std::vector<IntegerLiteral>* integer_reason);
751 ABSL_MUST_USE_RESULT
bool Enqueue(
753 absl::Span<const IntegerLiteral> integer_reason,
754 int trail_index_with_same_reason);
769 std::vector<Literal>* literals, std::vector<int>* dependencies)>;
776 absl::Span<const IntegerLiteral> integer_reason);
786 std::vector<Literal>* output)
const;
805 watchers_.push_back(p);
811 absl::Span<const IntegerLiteral> integer_reason) {
812 DCHECK(ReasonIsValid(literal_reason, integer_reason));
814 conflict->assign(literal_reason.begin(), literal_reason.end());
819 DCHECK(ReasonIsValid({}, integer_reason));
828 return vars_[
var].current_trail_index < vars_.
size();
834 reversible_classes_.push_back(rev);
837 int Index()
const {
return integer_trail_.size(); }
865 return !literal_to_fix_.empty() || !integer_literal_to_fix_.empty();
871 bool ReasonIsValid(absl::Span<const Literal> literal_reason,
872 absl::Span<const IntegerLiteral> integer_reason);
877 std::vector<Literal>* InitializeConflict(
879 absl::Span<const Literal> literals_reason,
880 absl::Span<const IntegerLiteral> bounds_reason);
883 ABSL_MUST_USE_RESULT
bool EnqueueInternal(
885 absl::Span<const Literal> literal_reason,
886 absl::Span<const IntegerLiteral> integer_reason,
887 int trail_index_with_same_reason);
891 absl::Span<const Literal> literal_reason,
892 absl::Span<const IntegerLiteral> integer_reason);
897 ABSL_MUST_USE_RESULT
bool EnqueueAssociatedIntegerLiteral(
901 void MergeReasonIntoInternal(std::vector<Literal>* output)
const;
906 int FindLowestTrailIndexThatExplainBound(
IntegerLiteral i_lit)
const;
911 void ComputeLazyReasonIfNeeded(
int trail_index)
const;
918 absl::Span<const int> Dependencies(
int trail_index)
const;
924 void AppendLiteralsReason(
int trail_index,
925 std::vector<Literal>* output)
const;
928 std::string DebugString();
933 IntegerValue current_bound;
936 int current_trail_index;
946 mutable int var_trail_index_cache_threshold_ = 0;
951 absl::flat_hash_map<IntegerValue, IntegerVariable> constant_map_;
958 int32 prev_trail_index;
965 std::vector<TrailEntry> integer_trail_;
966 std::vector<LazyReasonFunction> lazy_reasons_;
970 std::vector<int> integer_search_levels_;
977 std::vector<int> reason_decision_levels_;
978 std::vector<int> literals_reason_starts_;
979 std::vector<int> bounds_reason_starts_;
980 std::vector<Literal> literals_reason_buffer_;
985 std::vector<IntegerLiteral> bounds_reason_buffer_;
986 mutable std::vector<int> trail_index_reason_buffer_;
989 mutable std::vector<Literal> lazy_reason_literals_;
990 mutable std::vector<int> lazy_reason_trail_indices_;
1001 RevMap<absl::flat_hash_map<IntegerVariable, int>>
1002 var_to_current_lb_interval_index_;
1005 mutable bool has_dependency_ =
false;
1006 mutable std::vector<int> tmp_queue_;
1007 mutable std::vector<IntegerVariable> tmp_to_clear_;
1009 tmp_var_to_trail_index_in_queue_;
1010 mutable SparseBitset<BooleanVariable> added_variables_;
1017 std::vector<Literal> literal_to_fix_;
1018 std::vector<IntegerLiteral> integer_literal_to_fix_;
1021 struct RelaxHeapEntry {
1025 bool operator<(
const RelaxHeapEntry& o)
const {
return index < o.index; }
1027 mutable std::vector<RelaxHeapEntry> relax_heap_;
1028 mutable std::vector<int> tmp_indices_;
1031 mutable SparseBitset<IntegerVariable> tmp_marked_;
1037 std::vector<int> boolean_trail_index_to_integer_one_;
1041 int first_level_without_full_propagation_ = -1;
1043 int64 num_enqueues_ = 0;
1044 int64 num_untrails_ = 0;
1045 int64 num_level_zero_enqueues_ = 0;
1046 mutable int64 num_decisions_to_break_loop_ = 0;
1048 std::vector<SparseBitset<IntegerVariable>*> watchers_;
1049 std::vector<ReversibleInterface*> reversible_classes_;
1051 IntegerDomains* domains_;
1052 IntegerEncoder* encoder_;
1054 const SatParameters& parameters_;
1117 void Untrail(
const Trail& trail,
int literal_trail_index)
final;
1203 const std::function<
void(
const std::vector<IntegerVariable>&)> cb) {
1204 level_zero_modified_variable_callback_.push_back(cb);
1215 void UpdateCallingNeeds(
Trail* trail);
1225 return id == o.id && watch_index == o.watch_index;
1230 std::vector<PropagatorInterface*> watchers_;
1231 SparseBitset<IntegerVariable> modified_vars_;
1235 std::vector<std::deque<int>> queue_by_priority_;
1236 std::vector<bool> in_queue_;
1239 DEFINE_INT_TYPE(IdType,
int32);
1240 std::vector<int> id_to_level_at_last_call_;
1241 RevVector<IdType, int> id_to_greatest_common_level_since_last_call_;
1242 std::vector<std::vector<ReversibleInterface*>> id_to_reversible_classes_;
1243 std::vector<std::vector<int*>> id_to_reversible_ints_;
1244 std::vector<std::vector<int>> id_to_watch_indices_;
1245 std::vector<int> id_to_priority_;
1246 std::vector<int> id_to_idempotence_;
1249 std::vector<int> propagator_ids_to_call_at_level_zero_;
1254 std::vector<std::function<void(
const std::vector<IntegerVariable>&)>>
1255 level_zero_modified_variable_callback_;
1265 IntegerValue
bound) {
1271 IntegerValue
bound) {
1286 IntegerValue
bound)
const {
1301 return vars_[i].current_bound;
1309 return vars_[i].current_bound == -vars_[
NegationOf(i)].current_bound;
1331 IntegerVariable i)
const {
1336 IntegerVariable i)
const {
1351 IntegerVariable
var)
const {
1352 return integer_trail_[
var.value()].bound;
1356 IntegerVariable
var)
const {
1361 return integer_trail_[
var.value()].bound ==
1367 if (l.
Index() >= literal_to_watcher_.
size()) {
1368 literal_to_watcher_.
resize(l.
Index().value() + 1);
1376 if (
var.value() >= var_to_watcher_.
size()) {
1377 var_to_watcher_.
resize(
var.value() + 1);
1384 const WatchData data = {id, watch_index};
1385 if (!var_to_watcher_[
var].empty() && var_to_watcher_[
var].back() == data) {
1422 ->GetOrCreateConstantIntegerVariable(IntegerValue(
value));
1431 IntegerValue(lb), IntegerValue(ub));
1451 IntegerVariable
var;
1453 if (assignment.LiteralIsTrue(lit)) {
1455 }
else if (assignment.LiteralIsFalse(lit)) {
1461 encoder->AssociateToIntegerEqualValue(lit,
var, IntegerValue(1));
1499 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1501 VLOG(1) <<
"Model trivially infeasible, variable " << v
1503 <<
" and GreaterOrEqual() was called with a lower bound of "
1513 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1515 LOG(
WARNING) <<
"Model trivially infeasible, variable " << v
1517 <<
" and LowerOrEqual() was called with an upper bound of "
1538 const std::vector<Literal>& enforcement_literals,
IntegerLiteral i) {
1545 std::vector<Literal> clause;
1572 v, IntegerValue(lb))));
1586inline std::function<std::vector<IntegerEncoder::ValueLiteralPair>(Model*)>
1602std::function<void(Model*)>
#define DCHECK_LE(val1, val2)
#define DCHECK_NE(val1, val2)
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK(condition)
#define CHECK_LE(val1, val2)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
void resize(size_type new_size)
void push_back(const value_type &x)
An Assignment is a variable -> domains mapping, used to report solutions to the user.
We call domain any subset of Int64 = [kint64min, kint64max].
void ClearAndResize(IntegerType size)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool Propagate(Trail *trail) final
void WatchLowerBound(IntegerValue i, int id)
void AlwaysCallAtLevelZero(int id)
void RegisterLevelZeroModifiedVariablesCallback(const std::function< void(const std::vector< IntegerVariable > &)> cb)
void WatchIntegerVariable(IntegerValue v, int id)
int NumPropagators() const
void WatchLowerBound(AffineExpression e, int id)
void WatchUpperBound(AffineExpression e, int id)
void RegisterReversibleInt(int id, int *rev)
void RegisterReversibleClass(int id, ReversibleInterface *rev)
void WatchLiteral(Literal l, int id, int watch_index=-1)
void WatchUpperBound(IntegerValue i, int id)
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
GenericLiteralWatcher(Model *model)
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
void WatchAffineExpression(AffineExpression e, int id)
~GenericLiteralWatcher() final
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
void SetPropagatorPriority(int id, int priority)
int Register(PropagatorInterface *propagator)
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
void Untrail(const Trail &trail, int literal_trail_index) final
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i, IntegerValue *bound) const
const std::vector< IntegerLiteral > NewlyFixedIntegerLiterals() const
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
void FullyEncodeVariable(IntegerVariable var)
std::map< IntegerValue, Literal > PartialGreaterThanEncoding(IntegerVariable var) const
Literal GetFalseLiteral()
const IntegerVariable GetLiteralView(Literal lit) const
const InlinedIntegerLiteralVector & GetAllIntegerLiterals(Literal lit) const
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
void DisableImplicationBetweenLiteral()
void ClearNewlyFixedIntegerLiterals()
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
bool LiteralIsAssociated(IntegerLiteral i_lit) const
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
std::vector< ValueLiteralPair > PartialDomainEncoding(IntegerVariable var) const
const bool LiteralOrNegationHasView(Literal lit) const
void AddAllImplicationsBetweenAssociatedLiterals()
bool VariableIsFullyEncoded(IntegerVariable var) const
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
IntegerEncoder(Model *model)
LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const
void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit)
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
IntegerVariable FirstUnassignedVariable() const
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value)
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
bool Propagate(Trail *trail) final
void ReserveSpaceForNumVariables(int num_vars)
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
bool IsCurrentlyIgnored(IntegerVariable i) const
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
bool ReportConflict(absl::Span< const IntegerLiteral > integer_reason)
std::function< void(IntegerLiteral literal_to_explain, int trail_index_of_literal, std::vector< Literal > *literals, std::vector< int > *dependencies)> LazyReasonFunction
bool IsFixed(IntegerVariable i) const
LiteralIndex OptionalLiteralIndex(IntegerVariable i) const
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool CurrentBranchHadAnIncompletePropagation()
bool InPropagationLoop() const
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerVariable NextVariableToBranchOnInPropagationLoop() const
IntegerValue UpperBound(IntegerVariable i) const
void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered)
int64 num_enqueues() const
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
bool IntegerLiteralIsTrue(IntegerLiteral l) const
IntegerValue LowerBound(IntegerVariable i) const
int64 num_level_zero_enqueues() const
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
bool HasPendingRootLevelDeduction() const
int NumConstantVariables() const
bool IsFixedAtLevelZero(IntegerVariable var) const
void MergeReasonInto(absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
Literal IsIgnoredLiteral(IntegerVariable i) const
bool IsOptional(IntegerVariable i) const
ABSL_MUST_USE_RESULT bool ConditionalEnqueue(Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
bool IntegerLiteralIsFalse(IntegerLiteral l) const
void RemoveLevelZeroBounds(std::vector< IntegerLiteral > *reason) const
IntegerVariable AddIntegerVariable()
void RegisterReversibleClass(ReversibleInterface *rev)
const Domain & InitialVariableDomain(IntegerVariable var) const
void Untrail(const Trail &trail, int literal_trail_index) final
IntegerVariable NumIntegerVariables() const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
IntegerTrail(Model *model)
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
virtual ~PropagatorInterface()
virtual bool Propagate()=0
virtual bool IncrementalPropagate(const std::vector< int > &watch_indices)
RevIntRepository(Model *model)
RevIntegerValueRepository(Model *model)
BooleanVariable NewBooleanVariable()
int CurrentDecisionLevel() const
bool AddUnitClause(Literal true_literal)
const VariablesAssignment & Assignment() const
std::vector< Literal > * MutableConflict()
bool LiteralIsTrue(Literal literal) const
static const int64 kint64max
static const int64 kint64min
absl::InlinedVector< IntegerLiteral, 2 > InlinedIntegerLiteralVector
bool VariableIsPositive(IntegerVariable i)
bool AddProductTo(IntegerValue a, IntegerValue b, IntegerValue *result)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
std::function< int64(const Model &)> Value(IntegerVariable v)
DEFINE_INT_TYPE(ClauseIndex, int)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
IntType IntTypeAbs(IntType t)
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
double ToDouble(IntegerValue value)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::function< IntegerVariable(Model *)> ConstantIntegerVariable(int64 value)
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
std::function< void(Model *)> ImpliesInInterval(Literal in_interval, IntegerVariable v, int64 lb, int64 ub)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapAdd(int64 x, int64 y)
int64 CapProd(int64 x, int64 y)
LinearRange operator==(const LinearExpr &lhs, const LinearExpr &rhs)
AffineExpression Negated() const
AffineExpression(IntegerVariable v, IntegerValue c, IntegerValue cst)
AffineExpression(IntegerValue cst)
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
IntegerLiteral LowerOrEqual(IntegerValue bound) const
double LpValue(const absl::StrongVector< IntegerVariable, double > &lp_values) const
AffineExpression(IntegerVariable v, IntegerValue c)
bool operator==(AffineExpression o) const
AffineExpression(IntegerVariable v)
DebugSolution(Model *model)
IntegerDomains(Model *model)
ValueLiteralPair(IntegerValue v, Literal l)
bool operator<(const ValueLiteralPair &o) const
bool operator==(const ValueLiteralPair &o) const
bool operator==(IntegerLiteral o) const
IntegerLiteral(IntegerVariable v, IntegerValue b)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::string DebugString() const
IntegerLiteral Negated() const
bool operator!=(IntegerLiteral o) const