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());
76 template <
class IntType>
78 return IntType(std::abs(t.value()));
81 inline IntegerValue
CeilRatio(IntegerValue dividend,
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))));
1586 inline std::function<std::vector<IntegerEncoder::ValueLiteralPair>(Model*)>
1602 std::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)
const InlinedIntegerLiteralVector & GetAllIntegerLiterals(Literal lit) const
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i, IntegerValue *bound) const
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
void FullyEncodeVariable(IntegerVariable var)
Literal GetFalseLiteral()
const IntegerVariable GetLiteralView(Literal lit) const
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
void DisableImplicationBetweenLiteral()
void ClearNewlyFixedIntegerLiterals()
const std::vector< IntegerLiteral > NewlyFixedIntegerLiterals() const
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
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
std::map< IntegerValue, Literal > PartialGreaterThanEncoding(IntegerVariable var) 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)
std::vector< Literal > * MutableConflict()
const VariablesAssignment & Assignment() const
bool LiteralIsTrue(Literal literal) const
static const int64 kint64max
static const int64 kint64min
absl::InlinedVector< IntegerLiteral, 2 > InlinedIntegerLiteralVector
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
bool AddProductTo(IntegerValue a, IntegerValue b, IntegerValue *result)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
IntType IntTypeAbs(IntType t)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
const LiteralIndex kNoLiteralIndex(-1)
std::function< IntegerVariable(Model *)> ConstantIntegerVariable(int64 value)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
std::function< int64(const Model &)> Value(IntegerVariable v)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >Model *)> FullyEncodeVariable(IntegerVariable var)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
std::function< void(Model *)> ImpliesInInterval(Literal in_interval, IntegerVariable v, int64 lb, int64 ub)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
IntegerVariable PositiveVariable(IntegerVariable i)
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
DEFINE_INT_TYPE(ClauseIndex, int)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
bool VariableIsPositive(IntegerVariable i)
double ToDouble(IntegerValue value)
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