1 // Copyright 2010-2021 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13
14 #ifndef OR_TOOLS_SAT_INTEGER_H_
15 #define OR_TOOLS_SAT_INTEGER_H_
16
17 #include <cstdint>
18 #include <deque>
19 #include <functional>
20 #include <limits>
21 #include <map>
22 #include <memory>
23 #include <string>
24 #include <utility>
25 #include <vector>
26
27 #include "absl/base/attributes.h"
28 #include "absl/container/flat_hash_map.h"
29 #include "absl/container/inlined_vector.h"
30 #include "absl/strings/str_cat.h"
31 #include "absl/types/span.h"
32 #include "ortools/base/hash.h"
33 #include "ortools/base/int_type.h"
34 #include "ortools/base/integral_types.h"
35 #include "ortools/base/logging.h"
36 #include "ortools/base/macros.h"
37 #include "ortools/base/map_util.h"
38 #include "ortools/base/strong_vector.h"
39 #include "ortools/graph/iterators.h"
40 #include "ortools/sat/model.h"
41 #include "ortools/sat/sat_base.h"
42 #include "ortools/sat/sat_solver.h"
43 #include "ortools/util/bitset.h"
44 #include "ortools/util/rev.h"
45 #include "ortools/util/saturated_arithmetic.h"
46 #include "ortools/util/sorted_interval_list.h"
47
48 namespace operations_research {
49 namespace sat {
50
51 // Value type of an integer variable. An integer variable is always bounded
52 // on both sides, and this type is also used to store the bounds [lb, ub] of the
53 // range of each integer variable.
54 //
55 // Note that both bounds are inclusive, which allows to write many propagation
56 // algorithms for just one of the bound and apply it to the negated variables to
57 // get the symmetric algorithm for the other bound.
58 DEFINE_INT_TYPE(IntegerValue, int64_t);
59
60 // The max range of an integer variable is [kMinIntegerValue, kMaxIntegerValue].
61 //
62 // It is symmetric so the set of possible ranges stays the same when we take the
63 // negation of a variable. Moreover, we need some IntegerValue that fall outside
64 // this range on both side so that we can usually take care of integer overflow
65 // by simply doing "saturated arithmetic" and if one of the bound overflow, the
66 // two bounds will "cross" each others and we will get an empty range.
67 constexpr IntegerValue kMaxIntegerValue(
68 std::numeric_limits<IntegerValue::ValueType>::max() - 1);
69 constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue);
70
ToDouble(IntegerValue value)71 inline double ToDouble(IntegerValue value) {
72 const double kInfinity = std::numeric_limits<double>::infinity();
73 if (value >= kMaxIntegerValue) return kInfinity;
74 if (value <= kMinIntegerValue) return -kInfinity;
75 return static_cast<double>(value.value());
76 }
77
78 template <class IntType>
IntTypeAbs(IntType t)79 inline IntType IntTypeAbs(IntType t) {
80 return IntType(std::abs(t.value()));
81 }
82
CeilRatio(IntegerValue dividend,IntegerValue positive_divisor)83 inline IntegerValue CeilRatio(IntegerValue dividend,
84 IntegerValue positive_divisor) {
85 DCHECK_GT(positive_divisor, 0);
86 const IntegerValue result = dividend / positive_divisor;
87 const IntegerValue adjust =
88 static_cast<IntegerValue>(result * positive_divisor < dividend);
89 return result + adjust;
90 }
91
FloorRatio(IntegerValue dividend,IntegerValue positive_divisor)92 inline IntegerValue FloorRatio(IntegerValue dividend,
93 IntegerValue positive_divisor) {
94 DCHECK_GT(positive_divisor, 0);
95 const IntegerValue result = dividend / positive_divisor;
96 const IntegerValue adjust =
97 static_cast<IntegerValue>(result * positive_divisor > dividend);
98 return result - adjust;
99 }
100
101 // Returns dividend - FloorRatio(dividend, divisor) * divisor;
102 //
103 // This function is around the same speed than the computation above, but it
104 // never causes integer overflow. Note also that when calling FloorRatio() then
105 // PositiveRemainder(), the compiler should optimize the modulo away and just
106 // reuse the one from the first integer division.
PositiveRemainder(IntegerValue dividend,IntegerValue positive_divisor)107 inline IntegerValue PositiveRemainder(IntegerValue dividend,
108 IntegerValue positive_divisor) {
109 DCHECK_GT(positive_divisor, 0);
110 const IntegerValue m = dividend % positive_divisor;
111 return m < 0 ? m + positive_divisor : m;
112 }
113
114 // Computes result += a * b, and return false iff there is an overflow.
AddProductTo(IntegerValue a,IntegerValue b,IntegerValue * result)115 inline bool AddProductTo(IntegerValue a, IntegerValue b, IntegerValue* result) {
116 const int64_t prod = CapProd(a.value(), b.value());
117 if (prod == std::numeric_limits<int64_t>::min() ||
118 prod == std::numeric_limits<int64_t>::max())
119 return false;
120 const int64_t add = CapAdd(prod, result->value());
121 if (add == std::numeric_limits<int64_t>::min() ||
122 add == std::numeric_limits<int64_t>::max())
123 return false;
124 *result = IntegerValue(add);
125 return true;
126 }
127
128 // Index of an IntegerVariable.
129 //
130 // Each time we create an IntegerVariable we also create its negation. This is
131 // done like that so internally we only stores and deal with lower bound. The
132 // upper bound beeing the lower bound of the negated variable.
133 DEFINE_INT_TYPE(IntegerVariable, int32_t);
134 const IntegerVariable kNoIntegerVariable(-1);
NegationOf(IntegerVariable i)135 inline IntegerVariable NegationOf(IntegerVariable i) {
136 return IntegerVariable(i.value() ^ 1);
137 }
138
VariableIsPositive(IntegerVariable i)139 inline bool VariableIsPositive(IntegerVariable i) {
140 return (i.value() & 1) == 0;
141 }
142
PositiveVariable(IntegerVariable i)143 inline IntegerVariable PositiveVariable(IntegerVariable i) {
144 return IntegerVariable(i.value() & (~1));
145 }
146
147 // Special type for storing only one thing for var and NegationOf(var).
148 DEFINE_INT_TYPE(PositiveOnlyIndex, int32_t);
GetPositiveOnlyIndex(IntegerVariable var)149 inline PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var) {
150 return PositiveOnlyIndex(var.value() / 2);
151 }
152
IntegerTermDebugString(IntegerVariable var,IntegerValue coeff)153 inline std::string IntegerTermDebugString(IntegerVariable var,
154 IntegerValue coeff) {
155 coeff = VariableIsPositive(var) ? coeff : -coeff;
156 return absl::StrCat(coeff.value(), "*X", var.value() / 2);
157 }
158
159 // Returns the vector of the negated variables.
160 std::vector<IntegerVariable> NegationOf(
161 const std::vector<IntegerVariable>& vars);
162
163 // The integer equivalent of a literal.
164 // It represents an IntegerVariable and an upper/lower bound on it.
165 //
166 // Overflow: all the bounds below kMinIntegerValue and kMaxIntegerValue are
167 // treated as kMinIntegerValue - 1 and kMaxIntegerValue + 1.
168 struct IntegerLiteral {
169 // Because IntegerLiteral should never be created at a bound less constrained
170 // than an existing IntegerVariable bound, we don't allow GreaterOrEqual() to
171 // have a bound lower than kMinIntegerValue, and LowerOrEqual() to have a
172 // bound greater than kMaxIntegerValue. The other side is not constrained
173 // to allow for a computed bound to overflow. Note that both the full initial
174 // domain and the empty domain can always be represented.
175 static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound);
176 static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound);
177
178 // These two static integer literals represent an always true and an always
179 // false condition.
180 static IntegerLiteral TrueLiteral();
181 static IntegerLiteral FalseLiteral();
182
183 // Clients should prefer the static construction methods above.
IntegerLiteralIntegerLiteral184 IntegerLiteral() : var(kNoIntegerVariable), bound(0) {}
IntegerLiteralIntegerLiteral185 IntegerLiteral(IntegerVariable v, IntegerValue b) : var(v), bound(b) {
186 DCHECK_GE(bound, kMinIntegerValue);
187 DCHECK_LE(bound, kMaxIntegerValue + 1);
188 }
189
IsValidIntegerLiteral190 bool IsValid() const { return var != kNoIntegerVariable; }
IsTrueLiteralIntegerLiteral191 bool IsTrueLiteral() const { return var == kNoIntegerVariable && bound <= 0; }
IsFalseLiteralIntegerLiteral192 bool IsFalseLiteral() const { return var == kNoIntegerVariable && bound > 0; }
193
194 // The negation of x >= bound is x <= bound - 1.
195 IntegerLiteral Negated() const;
196
197 bool operator==(IntegerLiteral o) const {
198 return var == o.var && bound == o.bound;
199 }
200 bool operator!=(IntegerLiteral o) const {
201 return var != o.var || bound != o.bound;
202 }
203
DebugStringIntegerLiteral204 std::string DebugString() const {
205 return VariableIsPositive(var)
206 ? absl::StrCat("I", var.value() / 2, ">=", bound.value())
207 : absl::StrCat("I", var.value() / 2, "<=", -bound.value());
208 }
209
210 // Note that bound should be in [kMinIntegerValue, kMaxIntegerValue + 1].
211 IntegerVariable var = kNoIntegerVariable;
212 IntegerValue bound = IntegerValue(0);
213 };
214
215 inline std::ostream& operator<<(std::ostream& os, IntegerLiteral i_lit) {
216 os << i_lit.DebugString();
217 return os;
218 }
219
220 using InlinedIntegerLiteralVector = absl::InlinedVector<IntegerLiteral, 2>;
221
222 // Represents [coeff * variable + constant] or just a [constant].
223 //
224 // In some places it is useful to manipulate such expression instead of having
225 // to create an extra integer variable. This is mainly used for scheduling
226 // related constraints.
227 struct AffineExpression {
228 // Helper to construct an AffineExpression.
AffineExpressionAffineExpression229 AffineExpression() {}
AffineExpressionAffineExpression230 AffineExpression(IntegerValue cst) // NOLINT(runtime/explicit)
231 : constant(cst) {}
AffineExpressionAffineExpression232 AffineExpression(IntegerVariable v) // NOLINT(runtime/explicit)
233 : var(v), coeff(1) {}
AffineExpressionAffineExpression234 AffineExpression(IntegerVariable v, IntegerValue c)
235 : var(c > 0 ? v : NegationOf(v)), coeff(IntTypeAbs(c)) {}
AffineExpressionAffineExpression236 AffineExpression(IntegerVariable v, IntegerValue c, IntegerValue cst)
237 : var(c > 0 ? v : NegationOf(v)), coeff(IntTypeAbs(c)), constant(cst) {}
238
239 // Returns the integer literal corresponding to expression >= value or
240 // expression <= value.
241 //
242 // On constant expressions, they will return IntegerLiteral::TrueLiteral()
243 // or IntegerLiteral::FalseLiteral().
244 IntegerLiteral GreaterOrEqual(IntegerValue bound) const;
245 IntegerLiteral LowerOrEqual(IntegerValue bound) const;
246
247 // It is safe to call these with non-typed constants.
248 // This simplify the code when we need GreaterOrEqual(0) for instance.
249 IntegerLiteral GreaterOrEqual(int64_t bound) const;
250 IntegerLiteral LowerOrEqual(int64_t bound) const;
251
NegatedAffineExpression252 AffineExpression Negated() const {
253 if (var == kNoIntegerVariable) return AffineExpression(-constant);
254 return AffineExpression(NegationOf(var), coeff, -constant);
255 }
256
MultipliedByAffineExpression257 AffineExpression MultipliedBy(IntegerValue multiplier) const {
258 // Note that this also works if multiplier is negative.
259 return AffineExpression(var, coeff * multiplier, constant * multiplier);
260 }
261
262 bool operator==(AffineExpression o) const {
263 return var == o.var && coeff == o.coeff && constant == o.constant;
264 }
265
266 // Returns the value of this affine expression given its variable value.
ValueAtAffineExpression267 IntegerValue ValueAt(IntegerValue var_value) const {
268 return coeff * var_value + constant;
269 }
270
271 // Returns the affine expression value under a given LP solution.
LpValueAffineExpression272 double LpValue(
273 const absl::StrongVector<IntegerVariable, double>& lp_values) const {
274 if (var == kNoIntegerVariable) return ToDouble(constant);
275 return ToDouble(coeff) * lp_values[var] + ToDouble(constant);
276 }
277
DebugStringAffineExpression278 const std::string DebugString() const {
279 if (var == kNoIntegerVariable) return absl::StrCat(constant.value());
280 if (constant == 0) {
281 return absl::StrCat("(", coeff.value(), " * X", var.value(), ")");
282 } else {
283 return absl::StrCat("(", coeff.value(), " * X", var.value(), " + ",
284 constant.value(), ")");
285 }
286 }
287
288 // The coefficient MUST be positive. Use NegationOf(var) if needed.
289 //
290 // TODO(user): Make this private to enforce the invariant that coeff cannot be
291 // negative.
292 IntegerVariable var = kNoIntegerVariable; // kNoIntegerVariable for constant.
293 IntegerValue coeff = IntegerValue(0); // Zero for constant.
294 IntegerValue constant = IntegerValue(0);
295 };
296
297 // A model singleton that holds the INITIAL integer variable domains.
298 struct IntegerDomains : public absl::StrongVector<IntegerVariable, Domain> {
IntegerDomainsIntegerDomains299 explicit IntegerDomains(Model* model) {}
300 };
301
302 // A model singleton used for debugging. If this is set in the model, then we
303 // can check that various derived constraint do not exclude this solution (if it
304 // is a known optimal solution for instance).
305 struct DebugSolution
306 : public absl::StrongVector<IntegerVariable, IntegerValue> {
DebugSolutionDebugSolution307 explicit DebugSolution(Model* model) {}
308 };
309
310 // A value and a literal.
311 struct ValueLiteralPair {
312 struct CompareByLiteral {
operatorValueLiteralPair::CompareByLiteral313 bool operator()(const ValueLiteralPair& a,
314 const ValueLiteralPair& b) const {
315 return a.literal < b.literal;
316 }
317 };
318 struct CompareByValue {
operatorValueLiteralPair::CompareByValue319 bool operator()(const ValueLiteralPair& a,
320 const ValueLiteralPair& b) const {
321 return (a.value < b.value) ||
322 (a.value == b.value && a.literal < b.literal);
323 }
324 };
325
326 bool operator==(const ValueLiteralPair& o) const {
327 return value == o.value && literal == o.literal;
328 }
329
330 std::string DebugString() const;
331
332 IntegerValue value = IntegerValue(0);
333 Literal literal = Literal(kNoLiteralIndex);
334 };
335
336 std::ostream& operator<<(std::ostream& os, const ValueLiteralPair& p);
337
338 // Each integer variable x will be associated with a set of literals encoding
339 // (x >= v) for some values of v. This class maintains the relationship between
340 // the integer variables and such literals which can be created by a call to
341 // CreateAssociatedLiteral().
342 //
343 // The advantage of creating such Boolean variables is that the SatSolver which
344 // is driving the search can then take this variable as a decision and maintain
345 // these variables activity and so on. These variables can also be propagated
346 // directly by the learned clauses.
347 //
348 // This class also support a non-lazy full domain encoding which will create one
349 // literal per possible value in the domain. See FullyEncodeVariable(). This is
350 // meant to be called by constraints that directly work on the variable values
351 // like a table constraint or an all-diff constraint.
352 //
353 // TODO(user): We could also lazily create precedences Booleans between two
354 // arbitrary IntegerVariable. This is better done in the PrecedencesPropagator
355 // though.
356 class IntegerEncoder {
357 public:
IntegerEncoder(Model * model)358 explicit IntegerEncoder(Model* model)
359 : sat_solver_(model->GetOrCreate<SatSolver>()),
360 domains_(model->GetOrCreate<IntegerDomains>()),
361 num_created_variables_(0) {}
362
~IntegerEncoder()363 ~IntegerEncoder() {
364 VLOG(1) << "#variables created = " << num_created_variables_;
365 }
366
367 // Fully encode a variable using its current initial domain.
368 // If the variable is already fully encoded, this does nothing.
369 //
370 // This creates new Booleans variables as needed:
371 // 1) num_values for the literals X == value. Except when there is just
372 // two value in which case only one variable is created.
373 // 2) num_values - 3 for the literals X >= value or X <= value (using their
374 // negation). The -3 comes from the fact that we can reuse the equality
375 // literals for the two extreme points.
376 //
377 // The encoding for NegationOf(var) is automatically created too. It reuses
378 // the same Boolean variable as the encoding of var.
379 //
380 // TODO(user): It is currently only possible to call that at the decision
381 // level zero because we cannot add ternary clause in the middle of the
382 // search (for now). This is Checked.
383 void FullyEncodeVariable(IntegerVariable var);
384
385 // Returns true if we know that PartialDomainEncoding(var) span the full
386 // domain of var. This is always true if FullyEncodeVariable(var) has been
387 // called.
388 bool VariableIsFullyEncoded(IntegerVariable var) const;
389
390 // Computes the full encoding of a variable on which FullyEncodeVariable() has
391 // been called. The returned elements are always sorted by increasing
392 // IntegerValue and we filter values associated to false literals.
393 //
394 // Performance note: This function is not particularly fast, however it should
395 // only be required during domain creation.
396 std::vector<ValueLiteralPair> FullDomainEncoding(IntegerVariable var) const;
397
398 // Same as FullDomainEncoding() but only returns the list of value that are
399 // currently associated to a literal. In particular this has no guarantee to
400 // span the full domain of the given variable (but it might).
401 std::vector<ValueLiteralPair> PartialDomainEncoding(
402 IntegerVariable var) const;
403
404 // Raw encoding. May be incomplete and is not sorted. Contains all literals,
405 // true or false.
406 std::vector<ValueLiteralPair> RawDomainEncoding(IntegerVariable var) const;
407
408 // Returns the "canonical" (i_lit, negation of i_lit) pair. This mainly
409 // deal with domain with initial hole like [1,2][5,6] so that if one ask
410 // for x <= 3, this get canonicalized in the pair (x <= 2, x >= 5).
411 //
412 // Note that it is an error to call this with a literal that is trivially true
413 // or trivially false according to the initial variable domain. This is
414 // CHECKed to make sure we don't create wasteful literal.
415 //
416 // TODO(user): This is linear in the domain "complexity", we can do better if
417 // needed.
418 std::pair<IntegerLiteral, IntegerLiteral> Canonicalize(
419 IntegerLiteral i_lit) const;
420
421 // Returns, after creating it if needed, a Boolean literal such that:
422 // - if true, then the IntegerLiteral is true.
423 // - if false, then the negated IntegerLiteral is true.
424 //
425 // Note that this "canonicalize" the given literal first.
426 //
427 // This add the proper implications with the two "neighbor" literals of this
428 // one if they exist. This is the "list encoding" in: Thibaut Feydy, Peter J.
429 // Stuckey, "Lazy Clause Generation Reengineered", CP 2009.
430 Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit);
431 Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var,
432 IntegerValue value);
433
434 // Associates the Boolean literal to (X >= bound) or (X == value). If a
435 // literal was already associated to this fact, this will add an equality
436 // constraints between both literals. If the fact is trivially true or false,
437 // this will fix the given literal.
438 void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit);
439 void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var,
440 IntegerValue value);
441
442 // Returns true iff the given integer literal is associated. The second
443 // version returns the associated literal or kNoLiteralIndex. Note that none
444 // of these function call Canonicalize() first for speed, so it is possible
445 // that this returns false even though GetOrCreateAssociatedLiteral() would
446 // not create a new literal.
447 bool LiteralIsAssociated(IntegerLiteral i_lit) const;
448 LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const;
449 LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var,
450 IntegerValue value) const;
451
452 // Advanced usage. It is more efficient to create the associated literals in
453 // order, but it might be anoying to do so. Instead, you can first call
454 // DisableImplicationBetweenLiteral() and when you are done creating all the
455 // associated literals, you can call (only at level zero)
456 // AddAllImplicationsBetweenAssociatedLiterals() which will also turn back on
457 // the implications between literals for the one that will be added
458 // afterwards.
DisableImplicationBetweenLiteral()459 void DisableImplicationBetweenLiteral() { add_implications_ = false; }
460 void AddAllImplicationsBetweenAssociatedLiterals();
461
462 // Returns the IntegerLiterals that were associated with the given Literal.
GetIntegerLiterals(Literal lit)463 const InlinedIntegerLiteralVector& GetIntegerLiterals(Literal lit) const {
464 if (lit.Index() >= reverse_encoding_.size()) {
465 return empty_integer_literal_vector_;
466 }
467 return reverse_encoding_[lit.Index()];
468 }
469
470 // Same as GetIntegerLiterals(), but in addition, if the literal was
471 // associated to an integer == value, then the returned list will contain both
472 // (integer >= value) and (integer <= value).
GetAllIntegerLiterals(Literal lit)473 const InlinedIntegerLiteralVector& GetAllIntegerLiterals(Literal lit) const {
474 if (lit.Index() >= full_reverse_encoding_.size()) {
475 return empty_integer_literal_vector_;
476 }
477 return full_reverse_encoding_[lit.Index()];
478 }
479
480 // This is part of a "hack" to deal with new association involving a fixed
481 // literal. Note that these are only allowed at the decision level zero.
NewlyFixedIntegerLiterals()482 const std::vector<IntegerLiteral> NewlyFixedIntegerLiterals() const {
483 return newly_fixed_integer_literals_;
484 }
ClearNewlyFixedIntegerLiterals()485 void ClearNewlyFixedIntegerLiterals() {
486 newly_fixed_integer_literals_.clear();
487 }
488
489 // If it exists, returns a [0,1] integer variable which is equal to 1 iff the
490 // given literal is true. Returns kNoIntegerVariable if such variable does not
491 // exist. Note that one can create one by creating a new IntegerVariable and
492 // calling AssociateToIntegerEqualValue().
GetLiteralView(Literal lit)493 const IntegerVariable GetLiteralView(Literal lit) const {
494 if (lit.Index() >= literal_view_.size()) return kNoIntegerVariable;
495 return literal_view_[lit.Index()];
496 }
497
498 // If this is true, then a literal can be linearized with an affine expression
499 // involving an integer variable.
LiteralOrNegationHasView(Literal lit)500 const bool LiteralOrNegationHasView(Literal lit) const {
501 return GetLiteralView(lit) != kNoIntegerVariable ||
502 GetLiteralView(lit.Negated()) != kNoIntegerVariable;
503 }
504
505 // Returns a Boolean literal associated with a bound lower than or equal to
506 // the one of the given IntegerLiteral. If the given IntegerLiteral is true,
507 // then the returned literal should be true too. Returns kNoLiteralIndex if no
508 // such literal was created.
509 //
510 // Ex: if 'i' is (x >= 4) and we already created a literal associated to
511 // (x >= 2) but not to (x >= 3), we will return the literal associated with
512 // (x >= 2).
513 LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i,
514 IntegerValue* bound) const;
515
516 // Gets the literal always set to true, make it if it does not exist.
GetTrueLiteral()517 Literal GetTrueLiteral() {
518 DCHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
519 if (literal_index_true_ == kNoLiteralIndex) {
520 const Literal literal_true =
521 Literal(sat_solver_->NewBooleanVariable(), true);
522 literal_index_true_ = literal_true.Index();
523 sat_solver_->AddUnitClause(literal_true);
524 }
525 return Literal(literal_index_true_);
526 }
GetFalseLiteral()527 Literal GetFalseLiteral() { return GetTrueLiteral().Negated(); }
528
529 // Returns the set of Literal associated to IntegerLiteral of the form var >=
530 // value. We make a copy, because this can be easily invalidated when calling
531 // any function of this class. So it is less efficient but safer.
PartialGreaterThanEncoding(IntegerVariable var)532 std::map<IntegerValue, Literal> PartialGreaterThanEncoding(
533 IntegerVariable var) const {
534 if (var >= encoding_by_var_.size()) {
535 return std::map<IntegerValue, Literal>();
536 }
537 return encoding_by_var_[var];
538 }
539
540 private:
541 // Only add the equivalence between i_lit and literal, if there is already an
542 // associated literal with i_lit, this make literal and this associated
543 // literal equivalent.
544 void HalfAssociateGivenLiteral(IntegerLiteral i_lit, Literal literal);
545
546 // Adds the implications:
547 // Literal(before) <= associated_lit <= Literal(after).
548 // Arguments:
549 // - map is just encoding_by_var_[associated_lit.var] and is passed as a
550 // slight optimization.
551 // - 'it' is the current position of associated_lit in map, i.e. we must have
552 // it->second == associated_lit.
553 void AddImplications(const std::map<IntegerValue, Literal>& map,
554 std::map<IntegerValue, Literal>::const_iterator it,
555 Literal associated_lit);
556
557 SatSolver* sat_solver_;
558 IntegerDomains* domains_;
559
560 bool add_implications_ = true;
561 int64_t num_created_variables_ = 0;
562
563 // We keep all the literals associated to an Integer variable in a map ordered
564 // by bound (so we can properly add implications between the literals
565 // corresponding to the same variable).
566 //
567 // TODO(user): Remove the entry no longer needed because of level zero
568 // propagations.
569 absl::StrongVector<IntegerVariable, std::map<IntegerValue, Literal>>
570 encoding_by_var_;
571
572 // Store for a given LiteralIndex the list of its associated IntegerLiterals.
573 const InlinedIntegerLiteralVector empty_integer_literal_vector_;
574 absl::StrongVector<LiteralIndex, InlinedIntegerLiteralVector>
575 reverse_encoding_;
576 absl::StrongVector<LiteralIndex, InlinedIntegerLiteralVector>
577 full_reverse_encoding_;
578 std::vector<IntegerLiteral> newly_fixed_integer_literals_;
579
580 // Store for a given LiteralIndex its IntegerVariable view or kNoLiteralIndex
581 // if there is none.
582 absl::StrongVector<LiteralIndex, IntegerVariable> literal_view_;
583
584 // Mapping (variable == value) -> associated literal. Note that even if
585 // there is more than one literal associated to the same fact, we just keep
586 // the first one that was added.
587 //
588 // Note that we only keep positive IntegerVariable here to reduce memory
589 // usage.
590 absl::flat_hash_map<std::pair<PositiveOnlyIndex, IntegerValue>, Literal>
591 equality_to_associated_literal_;
592
593 // Mutable because this is lazily cleaned-up by PartialDomainEncoding().
594 mutable absl::StrongVector<PositiveOnlyIndex, std::vector<ValueLiteralPair>>
595 equality_by_var_;
596
597 // Variables that are fully encoded.
598 mutable absl::StrongVector<PositiveOnlyIndex, bool> is_fully_encoded_;
599
600 // A literal that is always true, convenient to encode trivial domains.
601 // This will be lazily created when needed.
602 LiteralIndex literal_index_true_ = kNoLiteralIndex;
603
604 // Temporary memory used by FullyEncodeVariable().
605 std::vector<IntegerValue> tmp_values_;
606
607 DISALLOW_COPY_AND_ASSIGN(IntegerEncoder);
608 };
609
610 // This class maintains a set of integer variables with their current bounds.
611 // Bounds can be propagated from an external "source" and this class helps
612 // to maintain the reason for each propagation.
613 class IntegerTrail : public SatPropagator {
614 public:
IntegerTrail(Model * model)615 explicit IntegerTrail(Model* model)
616 : SatPropagator("IntegerTrail"),
617 domains_(model->GetOrCreate<IntegerDomains>()),
618 encoder_(model->GetOrCreate<IntegerEncoder>()),
619 trail_(model->GetOrCreate<Trail>()),
620 parameters_(*model->GetOrCreate<SatParameters>()) {
621 model->GetOrCreate<SatSolver>()->AddPropagator(this);
622 }
623 ~IntegerTrail() final;
624
625 // SatPropagator interface. These functions make sure the current bounds
626 // information is in sync with the current solver literal trail. Any
627 // class/propagator using this class must make sure it is synced to the
628 // correct state before calling any of its functions.
629 bool Propagate(Trail* trail) final;
630 void Untrail(const Trail& trail, int literal_trail_index) final;
631 absl::Span<const Literal> Reason(const Trail& trail,
632 int trail_index) const final;
633
634 // Returns the number of created integer variables.
635 //
636 // Note that this is twice the number of call to AddIntegerVariable() since
637 // we automatically create the NegationOf() variable too.
NumIntegerVariables()638 IntegerVariable NumIntegerVariables() const {
639 return IntegerVariable(vars_.size());
640 }
641
642 // Optimization: you can call this before calling AddIntegerVariable()
643 // num_vars time.
644 void ReserveSpaceForNumVariables(int num_vars);
645
646 // Adds a new integer variable. Adding integer variable can only be done when
647 // the decision level is zero (checked). The given bounds are INCLUSIVE and
648 // must not cross.
649 //
650 // Note on integer overflow: 'upper_bound - lower_bound' must fit on an
651 // int64_t, this is DCHECKed. More generally, depending on the constraints
652 // that are added, the bounds magnitude must be small enough to satisfy each
653 // constraint overflow precondition.
654 IntegerVariable AddIntegerVariable(IntegerValue lower_bound,
655 IntegerValue upper_bound);
656
657 // Same as above but for a more complex domain specified as a sorted list of
658 // disjoint intervals. See the Domain class.
659 IntegerVariable AddIntegerVariable(const Domain& domain);
660
661 // Returns the initial domain of the given variable. Note that the min/max
662 // are updated with level zero propagation, but not holes.
663 const Domain& InitialVariableDomain(IntegerVariable var) const;
664
665 // Takes the intersection with the current initial variable domain.
666 //
667 // TODO(user): There is some memory inefficiency if this is called many time
668 // because of the underlying data structure we use. In practice, when used
669 // with a presolve, this is not often used, so that is fine though.
670 bool UpdateInitialDomain(IntegerVariable var, Domain domain);
671
672 // Same as AddIntegerVariable(value, value), but this is a bit more efficient
673 // because it reuses another constant with the same value if its exist.
674 //
675 // Note(user): Creating constant integer variable is a bit wasteful, but not
676 // that much, and it allows to simplify a lot of constraints that do not need
677 // to handle this case any differently than the general one. Maybe there is a
678 // better solution, but this is not really high priority as of December 2016.
679 IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value);
680 int NumConstantVariables() const;
681
682 // Same as AddIntegerVariable() but uses the maximum possible range. Note
683 // that since we take negation of bounds in various places, we make sure that
684 // we don't have overflow when we take the negation of the lower bound or of
685 // the upper bound.
AddIntegerVariable()686 IntegerVariable AddIntegerVariable() {
687 return AddIntegerVariable(kMinIntegerValue, kMaxIntegerValue);
688 }
689
690 // For an optional variable, both its lb and ub must be valid bound assuming
691 // the fact that the variable is "present". However, the domain [lb, ub] is
692 // allowed to be empty (i.e. ub < lb) if the given is_ignored literal is true.
693 // Moreover, if is_ignored is true, then the bound of such variable should NOT
694 // impact any non-ignored variable in any way (but the reverse is not true).
IsOptional(IntegerVariable i)695 bool IsOptional(IntegerVariable i) const {
696 return is_ignored_literals_[i] != kNoLiteralIndex;
697 }
IsCurrentlyIgnored(IntegerVariable i)698 bool IsCurrentlyIgnored(IntegerVariable i) const {
699 const LiteralIndex is_ignored_literal = is_ignored_literals_[i];
700 return is_ignored_literal != kNoLiteralIndex &&
701 trail_->Assignment().LiteralIsTrue(Literal(is_ignored_literal));
702 }
IsIgnoredLiteral(IntegerVariable i)703 Literal IsIgnoredLiteral(IntegerVariable i) const {
704 DCHECK(IsOptional(i));
705 return Literal(is_ignored_literals_[i]);
706 }
OptionalLiteralIndex(IntegerVariable i)707 LiteralIndex OptionalLiteralIndex(IntegerVariable i) const {
708 return is_ignored_literals_[i] == kNoLiteralIndex
709 ? kNoLiteralIndex
710 : Literal(is_ignored_literals_[i]).NegatedIndex();
711 }
MarkIntegerVariableAsOptional(IntegerVariable i,Literal is_considered)712 void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered) {
713 DCHECK(is_ignored_literals_[i] == kNoLiteralIndex ||
714 is_ignored_literals_[i] == is_considered.NegatedIndex());
715 is_ignored_literals_[i] = is_considered.NegatedIndex();
716 is_ignored_literals_[NegationOf(i)] = is_considered.NegatedIndex();
717 }
718
719 // Returns the current lower/upper bound of the given integer variable.
720 IntegerValue LowerBound(IntegerVariable i) const;
721 IntegerValue UpperBound(IntegerVariable i) const;
722
723 // Checks if the variable is fixed.
724 bool IsFixed(IntegerVariable i) const;
725
726 // Checks that the variable is fixed and returns its value.
727 IntegerValue FixedValue(IntegerVariable i) const;
728
729 // Same as above for an affine expression.
730 IntegerValue LowerBound(AffineExpression expr) const;
731 IntegerValue UpperBound(AffineExpression expr) const;
732 bool IsFixed(AffineExpression expr) const;
733 IntegerValue FixedValue(AffineExpression expr) const;
734
735 // Returns the integer literal that represent the current lower/upper bound of
736 // the given integer variable.
737 IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const;
738 IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const;
739
740 // Returns the integer literal that represent the current lower/upper bound of
741 // the given affine expression. In case the expression is constant, it returns
742 // IntegerLiteral::TrueLiteral().
743 IntegerLiteral LowerBoundAsLiteral(AffineExpression expr) const;
744 IntegerLiteral UpperBoundAsLiteral(AffineExpression expr) const;
745
746 // Returns the current value (if known) of an IntegerLiteral.
747 bool IntegerLiteralIsTrue(IntegerLiteral l) const;
748 bool IntegerLiteralIsFalse(IntegerLiteral l) const;
749
750 // Returns globally valid lower/upper bound on the given integer variable.
751 IntegerValue LevelZeroLowerBound(IntegerVariable var) const;
752 IntegerValue LevelZeroUpperBound(IntegerVariable var) const;
753
754 // Returns globally valid lower/upper bound on the given affine expression.
755 IntegerValue LevelZeroLowerBound(AffineExpression exp) const;
756 IntegerValue LevelZeroUpperBound(AffineExpression exp) const;
757
758 // Returns true if the variable is fixed at level 0.
759 bool IsFixedAtLevelZero(IntegerVariable var) const;
760
761 // Returns true if the affine expression is fixed at level 0.
762 bool IsFixedAtLevelZero(AffineExpression expr) const;
763
764 // Advanced usage.
765 // Returns the current lower bound assuming the literal is true.
766 IntegerValue ConditionalLowerBound(Literal l, IntegerVariable i) const;
767 IntegerValue ConditionalLowerBound(Literal l, AffineExpression expr) const;
768
769 // Advanced usage. Given the reason for
770 // (Sum_i coeffs[i] * reason[i].var >= current_lb) initially in reason,
771 // this function relaxes the reason given that we only need the explanation of
772 // (Sum_i coeffs[i] * reason[i].var >= current_lb - slack).
773 //
774 // Preconditions:
775 // - coeffs must be of same size as reason, and all entry must be positive.
776 // - *reason must initially contains the trivial initial reason, that is
777 // the current lower-bound of each variables.
778 //
779 // TODO(user): Requiring all initial literal to be at their current bound is
780 // not really clean. Maybe we can change the API to only take IntegerVariable
781 // and produce the reason directly.
782 //
783 // TODO(user): change API so that this work is performed during the conflict
784 // analysis where we can be smarter in how we relax the reason. Note however
785 // that this function is mainly used when we have a conflict, so this is not
786 // really high priority.
787 //
788 // TODO(user): Test that the code work in the presence of integer overflow.
789 void RelaxLinearReason(IntegerValue slack,
790 absl::Span<const IntegerValue> coeffs,
791 std::vector<IntegerLiteral>* reason) const;
792
793 // Same as above but take in IntegerVariables instead of IntegerLiterals.
794 void AppendRelaxedLinearReason(IntegerValue slack,
795 absl::Span<const IntegerValue> coeffs,
796 absl::Span<const IntegerVariable> vars,
797 std::vector<IntegerLiteral>* reason) const;
798
799 // Same as above but relax the given trail indices.
800 void RelaxLinearReason(IntegerValue slack,
801 absl::Span<const IntegerValue> coeffs,
802 std::vector<int>* trail_indices) const;
803
804 // Removes from the reasons the literal that are always true.
805 // This is mainly useful for experiments/testing.
806 void RemoveLevelZeroBounds(std::vector<IntegerLiteral>* reason) const;
807
808 // Enqueue new information about a variable bound. Calling this with a less
809 // restrictive bound than the current one will have no effect.
810 //
811 // The reason for this "assignment" must be provided as:
812 // - A set of Literal currently beeing all false.
813 // - A set of IntegerLiteral currently beeing all true.
814 //
815 // IMPORTANT: Notice the inversed sign in the literal reason. This is a bit
816 // confusing but internally SAT use this direction for efficiency.
817 //
818 // Note(user): Duplicates Literal/IntegerLiteral are supported because we call
819 // STLSortAndRemoveDuplicates() in MergeReasonInto(), but maybe they shouldn't
820 // for efficiency reason.
821 //
822 // TODO(user): If the given bound is equal to the current bound, maybe the new
823 // reason is better? how to decide and what to do in this case? to think about
824 // it. Currently we simply don't do anything.
825 ABSL_MUST_USE_RESULT bool Enqueue(
826 IntegerLiteral i_lit, absl::Span<const Literal> literal_reason,
827 absl::Span<const IntegerLiteral> integer_reason);
828
829 // Enqueue new information about a variable bound. It has the same behavior
830 // as the Enqueue() method, except that it accepts true and false integer
831 // literals, both for i_lit, and for the integer reason.
832 //
833 // This method will do nothing if i_lit is a true literal. It will report a
834 // conflict if i_lit is a false literal, and enqueue i_lit normally otherwise.
835 // Furthemore, it will check that the integer reason does not contain any
836 // false literals, and will remove true literals before calling
837 // ReportConflict() or Enqueue().
838 ABSL_MUST_USE_RESULT bool SafeEnqueue(
839 IntegerLiteral i_lit, absl::Span<const IntegerLiteral> integer_reason);
840
841 // Pushes the given integer literal assuming that the Boolean literal is true.
842 // This can do a few things:
843 // - If lit it true, add it to the reason and push the integer bound.
844 // - If the bound is infeasible, push lit to false.
845 // - If the underlying variable is optional and also controlled by lit, push
846 // the bound even if lit is not assigned.
847 ABSL_MUST_USE_RESULT bool ConditionalEnqueue(
848 Literal lit, IntegerLiteral i_lit, std::vector<Literal>* literal_reason,
849 std::vector<IntegerLiteral>* integer_reason);
850
851 // Same as Enqueue(), but takes an extra argument which if smaller than
852 // integer_trail_.size() is interpreted as the trail index of an old Enqueue()
853 // that had the same reason as this one. Note that the given Span must still
854 // be valid as they are used in case of conflict.
855 //
856 // TODO(user): This currently cannot refer to a trail_index with a lazy
857 // reason. Fix or at least check that this is the case.
858 ABSL_MUST_USE_RESULT bool Enqueue(
859 IntegerLiteral i_lit, absl::Span<const Literal> literal_reason,
860 absl::Span<const IntegerLiteral> integer_reason,
861 int trail_index_with_same_reason);
862
863 // Lazy reason API.
864 //
865 // The function is provided with the IntegerLiteral to explain and its index
866 // in the integer trail. It must fill the two vectors so that literals
867 // contains any Literal part of the reason and dependencies contains the trail
868 // index of any IntegerLiteral that is also part of the reason.
869 //
870 // Remark: sometimes this is called to fill the conflict while the literal
871 // to explain is propagated. In this case, trail_index_of_literal will be
872 // the current trail index, and we cannot assume that there is anything filled
873 // yet in integer_literal[trail_index_of_literal].
874 using LazyReasonFunction = std::function<void(
875 IntegerLiteral literal_to_explain, int trail_index_of_literal,
876 std::vector<Literal>* literals, std::vector<int>* dependencies)>;
877 ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit,
878 LazyReasonFunction lazy_reason);
879
880 // Enqueues the given literal on the trail.
881 // See the comment of Enqueue() for the reason format.
882 void EnqueueLiteral(Literal literal, absl::Span<const Literal> literal_reason,
883 absl::Span<const IntegerLiteral> integer_reason);
884
885 // Returns the reason (as set of Literal currently false) for a given integer
886 // literal. Note that the bound must be less restrictive than the current
887 // bound (checked).
888 std::vector<Literal> ReasonFor(IntegerLiteral literal) const;
889
890 // Appends the reason for the given integer literals to the output and call
891 // STLSortAndRemoveDuplicates() on it.
892 void MergeReasonInto(absl::Span<const IntegerLiteral> literals,
893 std::vector<Literal>* output) const;
894
895 // Returns the number of enqueues that changed a variable bounds. We don't
896 // count enqueues called with a less restrictive bound than the current one.
897 //
898 // Note(user): this can be used to see if any of the bounds changed. Just
899 // looking at the integer trail index is not enough because at level zero it
900 // doesn't change since we directly update the "fixed" bounds.
num_enqueues()901 int64_t num_enqueues() const { return num_enqueues_; }
timestamp()902 int64_t timestamp() const { return num_enqueues_ + num_untrails_; }
903
904 // Same as num_enqueues but only count the level zero changes.
num_level_zero_enqueues()905 int64_t num_level_zero_enqueues() const { return num_level_zero_enqueues_; }
906
907 // All the registered bitsets will be set to one each time a LbVar is
908 // modified. It is up to the client to clear it if it wants to be notified
909 // with the newly modified variables.
RegisterWatcher(SparseBitset<IntegerVariable> * p)910 void RegisterWatcher(SparseBitset<IntegerVariable>* p) {
911 p->ClearAndResize(NumIntegerVariables());
912 watchers_.push_back(p);
913 }
914
915 // Helper functions to report a conflict. Always return false so a client can
916 // simply do: return integer_trail_->ReportConflict(...);
ReportConflict(absl::Span<const Literal> literal_reason,absl::Span<const IntegerLiteral> integer_reason)917 bool ReportConflict(absl::Span<const Literal> literal_reason,
918 absl::Span<const IntegerLiteral> integer_reason) {
919 DCHECK(ReasonIsValid(literal_reason, integer_reason));
920 std::vector<Literal>* conflict = trail_->MutableConflict();
921 conflict->assign(literal_reason.begin(), literal_reason.end());
922 MergeReasonInto(integer_reason, conflict);
923 return false;
924 }
ReportConflict(absl::Span<const IntegerLiteral> integer_reason)925 bool ReportConflict(absl::Span<const IntegerLiteral> integer_reason) {
926 DCHECK(ReasonIsValid({}, integer_reason));
927 std::vector<Literal>* conflict = trail_->MutableConflict();
928 conflict->clear();
929 MergeReasonInto(integer_reason, conflict);
930 return false;
931 }
932
933 // Returns true if the variable lower bound is still the one from level zero.
VariableLowerBoundIsFromLevelZero(IntegerVariable var)934 bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const {
935 return vars_[var].current_trail_index < vars_.size();
936 }
937
938 // Registers a reversible class. This class will always be synced with the
939 // correct decision level.
RegisterReversibleClass(ReversibleInterface * rev)940 void RegisterReversibleClass(ReversibleInterface* rev) {
941 reversible_classes_.push_back(rev);
942 }
943
Index()944 int Index() const { return integer_trail_.size(); }
945
946 // Inspects the trail and output all the non-level zero bounds (one per
947 // variables) to the output. The algo is sparse if there is only a few
948 // propagations on the trail.
949 void AppendNewBounds(std::vector<IntegerLiteral>* output) const;
950
951 // Returns the trail index < threshold of a TrailEntry about var. Returns -1
952 // if there is no such entry (at a positive decision level). This is basically
953 // the trail index of the lower bound of var at the time.
954 //
955 // Important: We do some optimization internally, so this should only be
956 // used from within a LazyReasonFunction().
957 int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const;
958
959 // Basic heuristic to detect when we are in a propagation loop, and suggest
960 // a good variable to branch on (taking the middle value) to get out of it.
961 bool InPropagationLoop() const;
962 IntegerVariable NextVariableToBranchOnInPropagationLoop() const;
963
964 // If we had an incomplete propagation, it is important to fix all the
965 // variables and not relly on the propagation to do so. This is related to the
966 // InPropagationLoop() code above.
967 bool CurrentBranchHadAnIncompletePropagation();
968 IntegerVariable FirstUnassignedVariable() const;
969
970 // Return true if we can fix new fact at level zero.
HasPendingRootLevelDeduction()971 bool HasPendingRootLevelDeduction() const {
972 return !literal_to_fix_.empty() || !integer_literal_to_fix_.empty();
973 }
974
975 private:
976 // Used for DHECKs to validate the reason given to the public functions above.
977 // Tests that all Literal are false. Tests that all IntegerLiteral are true.
978 bool ReasonIsValid(absl::Span<const Literal> literal_reason,
979 absl::Span<const IntegerLiteral> integer_reason);
980
981 // Called by the Enqueue() functions that detected a conflict. This does some
982 // common conflict initialization that must terminate by a call to
983 // MergeReasonIntoInternal(conflict) where conflict is the returned vector.
984 std::vector<Literal>* InitializeConflict(
985 IntegerLiteral integer_literal, const LazyReasonFunction& lazy_reason,
986 absl::Span<const Literal> literals_reason,
987 absl::Span<const IntegerLiteral> bounds_reason);
988
989 // Internal implementation of the different public Enqueue() functions.
990 ABSL_MUST_USE_RESULT bool EnqueueInternal(
991 IntegerLiteral i_lit, LazyReasonFunction lazy_reason,
992 absl::Span<const Literal> literal_reason,
993 absl::Span<const IntegerLiteral> integer_reason,
994 int trail_index_with_same_reason);
995
996 // Internal implementation of the EnqueueLiteral() functions.
997 void EnqueueLiteralInternal(Literal literal, LazyReasonFunction lazy_reason,
998 absl::Span<const Literal> literal_reason,
999 absl::Span<const IntegerLiteral> integer_reason);
1000
1001 // Same as EnqueueInternal() but for the case where we push an IntegerLiteral
1002 // because an associated Literal is true (and we know it). In this case, we
1003 // have less work to do, so this has the same effect but is faster.
1004 ABSL_MUST_USE_RESULT bool EnqueueAssociatedIntegerLiteral(
1005 IntegerLiteral i_lit, Literal literal_reason);
1006
1007 // Does the work of MergeReasonInto() when queue_ is already initialized.
1008 void MergeReasonIntoInternal(std::vector<Literal>* output) const;
1009
1010 // Returns the lowest trail index of a TrailEntry that can be used to explain
1011 // the given IntegerLiteral. The literal must be currently true (CHECKed).
1012 // Returns -1 if the explanation is trivial.
1013 int FindLowestTrailIndexThatExplainBound(IntegerLiteral i_lit) const;
1014
1015 // This must be called before Dependencies() or AppendLiteralsReason().
1016 //
1017 // TODO(user): Not really robust, try to find a better way.
1018 void ComputeLazyReasonIfNeeded(int trail_index) const;
1019
1020 // Helper function to return the "dependencies" of a bound assignment.
1021 // All the TrailEntry at these indices are part of the reason for this
1022 // assignment.
1023 //
1024 // Important: The returned Span is only valid up to the next call.
1025 absl::Span<const int> Dependencies(int trail_index) const;
1026
1027 // Helper function to append the Literal part of the reason for this bound
1028 // assignment. We use added_variables_ to not add the same literal twice.
1029 // Note that looking at literal.Variable() is enough since all the literals
1030 // of a reason must be false.
1031 void AppendLiteralsReason(int trail_index,
1032 std::vector<Literal>* output) const;
1033
1034 // Returns some debugging info.
1035 std::string DebugString();
1036
1037 // Information for each internal variable about its current bound.
1038 struct VarInfo {
1039 // The current bound on this variable.
1040 IntegerValue current_bound;
1041
1042 // Trail index of the last TrailEntry in the trail referring to this var.
1043 int current_trail_index;
1044 };
1045 absl::StrongVector<IntegerVariable, VarInfo> vars_;
1046
1047 // This is used by FindLowestTrailIndexThatExplainBound() and
1048 // FindTrailIndexOfVarBefore() to speed up the lookup. It keeps a trail index
1049 // for each variable that may or may not point to a TrailEntry regarding this
1050 // variable. The validity of the index is verified before beeing used.
1051 //
1052 // The cache will only be updated with trail_index >= threshold.
1053 mutable int var_trail_index_cache_threshold_ = 0;
1054 mutable absl::StrongVector<IntegerVariable, int> var_trail_index_cache_;
1055
1056 // Used by GetOrCreateConstantIntegerVariable() to return already created
1057 // constant variables that share the same value.
1058 absl::flat_hash_map<IntegerValue, IntegerVariable> constant_map_;
1059
1060 // The integer trail. It always start by num_vars sentinel values with the
1061 // level 0 bounds (in one to one correspondence with vars_).
1062 struct TrailEntry {
1063 IntegerValue bound;
1064 IntegerVariable var;
1065 int32_t prev_trail_index;
1066
1067 // Index in literals_reason_start_/bounds_reason_starts_ If this is -1, then
1068 // this was a propagation with a lazy reason, and the reason can be
1069 // re-created by calling the function lazy_reasons_[trail_index].
1070 int32_t reason_index;
1071 };
1072 std::vector<TrailEntry> integer_trail_;
1073 std::vector<LazyReasonFunction> lazy_reasons_;
1074
1075 // Start of each decision levels in integer_trail_.
1076 // TODO(user): use more general reversible mechanism?
1077 std::vector<int> integer_search_levels_;
1078
1079 // Buffer to store the reason of each trail entry.
1080 // Note that bounds_reason_buffer_ is an "union". It initially contains the
1081 // IntegerLiteral, and is lazily replaced by the result of
1082 // FindLowestTrailIndexThatExplainBound() applied to these literals. The
1083 // encoding is a bit hacky, see Dependencies().
1084 std::vector<int> reason_decision_levels_;
1085 std::vector<int> literals_reason_starts_;
1086 std::vector<int> bounds_reason_starts_;
1087 std::vector<Literal> literals_reason_buffer_;
1088
1089 // These two vectors are in one to one correspondence. Dependencies() will
1090 // "cache" the result of the conversion from IntegerLiteral to trail indices
1091 // in trail_index_reason_buffer_.
1092 std::vector<IntegerLiteral> bounds_reason_buffer_;
1093 mutable std::vector<int> trail_index_reason_buffer_;
1094
1095 // Temporary vector filled by calls to LazyReasonFunction().
1096 mutable std::vector<Literal> lazy_reason_literals_;
1097 mutable std::vector<int> lazy_reason_trail_indices_;
1098
1099 // The "is_ignored" literal of the optional variables or kNoLiteralIndex.
1100 absl::StrongVector<IntegerVariable, LiteralIndex> is_ignored_literals_;
1101
1102 // This is only filled for variables with a domain more complex than a single
1103 // interval of values. var_to_current_lb_interval_index_[var] stores the
1104 // intervals in (*domains_)[var] where the current lower-bound lies.
1105 //
1106 // TODO(user): Avoid using hash_map here, a simple vector should be more
1107 // efficient, but we need the "rev" aspect.
1108 RevMap<absl::flat_hash_map<IntegerVariable, int>>
1109 var_to_current_lb_interval_index_;
1110
1111 // Temporary data used by MergeReasonInto().
1112 mutable bool has_dependency_ = false;
1113 mutable std::vector<int> tmp_queue_;
1114 mutable std::vector<IntegerVariable> tmp_to_clear_;
1115 mutable absl::StrongVector<IntegerVariable, int>
1116 tmp_var_to_trail_index_in_queue_;
1117 mutable SparseBitset<BooleanVariable> added_variables_;
1118
1119 // Sometimes we propagate fact with no reason at a positive level, those
1120 // will automatically be fixed on the next restart.
1121 //
1122 // TODO(user): If we change the logic to not restart right away, we probably
1123 // need to not store duplicates bounds for the same variable.
1124 std::vector<Literal> literal_to_fix_;
1125 std::vector<IntegerLiteral> integer_literal_to_fix_;
1126
1127 // Temporary heap used by RelaxLinearReason();
1128 struct RelaxHeapEntry {
1129 int index;
1130 IntegerValue coeff;
1131 int64_t diff;
1132 bool operator<(const RelaxHeapEntry& o) const { return index < o.index; }
1133 };
1134 mutable std::vector<RelaxHeapEntry> relax_heap_;
1135 mutable std::vector<int> tmp_indices_;
1136
1137 // Temporary data used by AppendNewBounds().
1138 mutable SparseBitset<IntegerVariable> tmp_marked_;
1139
1140 // For EnqueueLiteral(), we store a special TrailEntry to recover the reason
1141 // lazily. This vector indicates the correspondence between a literal that
1142 // was pushed by this class at a given trail index, and the index of its
1143 // TrailEntry in integer_trail_.
1144 std::vector<int> boolean_trail_index_to_integer_one_;
1145
1146 // We need to know if we skipped some propagation in the current branch.
1147 // This is reverted as we backtrack over it.
1148 int first_level_without_full_propagation_ = -1;
1149
1150 int64_t num_enqueues_ = 0;
1151 int64_t num_untrails_ = 0;
1152 int64_t num_level_zero_enqueues_ = 0;
1153 mutable int64_t num_decisions_to_break_loop_ = 0;
1154
1155 std::vector<SparseBitset<IntegerVariable>*> watchers_;
1156 std::vector<ReversibleInterface*> reversible_classes_;
1157
1158 IntegerDomains* domains_;
1159 IntegerEncoder* encoder_;
1160 Trail* trail_;
1161 const SatParameters& parameters_;
1162
1163 // Temporary "hash" to keep track of all the conditional enqueue that were
1164 // done. Note that we currently do not keep any reason for them, and as such,
1165 // we can only use this in heuristics. See ConditionalLowerBound().
1166 absl::flat_hash_map<std::pair<LiteralIndex, IntegerVariable>, IntegerValue>
1167 conditional_lbs_;
1168
1169 DISALLOW_COPY_AND_ASSIGN(IntegerTrail);
1170 };
1171
1172 // Base class for CP like propagators.
1173 class PropagatorInterface {
1174 public:
PropagatorInterface()1175 PropagatorInterface() {}
~PropagatorInterface()1176 virtual ~PropagatorInterface() {}
1177
1178 // This will be called after one or more literals that are watched by this
1179 // propagator changed. It will also always be called on the first propagation
1180 // cycle after registration.
1181 virtual bool Propagate() = 0;
1182
1183 // This will only be called on a non-empty vector, otherwise Propagate() will
1184 // be called. The passed vector will contain the "watch index" of all the
1185 // literals that were given one at registration and that changed since the
1186 // last call to Propagate(). This is only true when going down in the search
1187 // tree, on backjump this list will be cleared.
1188 //
1189 // Notes:
1190 // - The indices may contain duplicates if the same integer variable as been
1191 // updated many times or if different watched literals have the same
1192 // watch_index.
1193 // - At level zero, it will not contain any indices associated with literals
1194 // that were already fixed when the propagator was registered. Only the
1195 // indices of the literals modified after the registration will be present.
IncrementalPropagate(const std::vector<int> & watch_indices)1196 virtual bool IncrementalPropagate(const std::vector<int>& watch_indices) {
1197 LOG(FATAL) << "Not implemented.";
1198 return false; // Remove warning in Windows
1199 }
1200 };
1201
1202 // Singleton for basic reversible types. We need the wrapper so that they can be
1203 // accessed with model->GetOrCreate<>() and properly registered at creation.
1204 class RevIntRepository : public RevRepository<int> {
1205 public:
RevIntRepository(Model * model)1206 explicit RevIntRepository(Model* model) {
1207 model->GetOrCreate<IntegerTrail>()->RegisterReversibleClass(this);
1208 }
1209 };
1210 class RevIntegerValueRepository : public RevRepository<IntegerValue> {
1211 public:
RevIntegerValueRepository(Model * model)1212 explicit RevIntegerValueRepository(Model* model) {
1213 model->GetOrCreate<IntegerTrail>()->RegisterReversibleClass(this);
1214 }
1215 };
1216
1217 // This class allows registering Propagator that will be called if a
1218 // watched Literal or LbVar changes.
1219 //
1220 // TODO(user): Move this to its own file. Add unit tests!
1221 class GenericLiteralWatcher : public SatPropagator {
1222 public:
1223 explicit GenericLiteralWatcher(Model* model);
~GenericLiteralWatcher()1224 ~GenericLiteralWatcher() final {}
1225
1226 // On propagate, the registered propagators will be called if they need to
1227 // until a fixed point is reached. Propagators with low ids will tend to be
1228 // called first, but it ultimately depends on their "waking" order.
1229 bool Propagate(Trail* trail) final;
1230 void Untrail(const Trail& trail, int literal_trail_index) final;
1231
1232 // Registers a propagator and returns its unique ids.
1233 int Register(PropagatorInterface* propagator);
1234
1235 // Changes the priority of the propagator with given id. The priority is a
1236 // non-negative integer. Propagators with a lower priority will always be
1237 // run before the ones with a higher one. The default priority is one.
1238 void SetPropagatorPriority(int id, int priority);
1239
1240 // The default behavior is to assume that a propagator does not need to be
1241 // called twice in a row. However, propagators on which this is called will be
1242 // called again if they change one of their own watched variables.
1243 void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id);
1244
1245 // Whether we call a propagator even if its watched variables didn't change.
1246 // This is only used when we are back to level zero. This was introduced for
1247 // the LP propagator where we might need to continue an interrupted solve or
1248 // add extra cuts at level zero.
1249 void AlwaysCallAtLevelZero(int id);
1250
1251 // Watches the corresponding quantity. The propagator with given id will be
1252 // called if it changes. Note that WatchLiteral() only trigger when the
1253 // literal becomes true.
1254 //
1255 // If watch_index is specified, it is associated with the watched literal.
1256 // Doing this will cause IncrementalPropagate() to be called (see the
1257 // documentation of this interface for more detail).
1258 void WatchLiteral(Literal l, int id, int watch_index = -1);
1259 void WatchLowerBound(IntegerVariable var, int id, int watch_index = -1);
1260 void WatchUpperBound(IntegerVariable var, int id, int watch_index = -1);
1261 void WatchIntegerVariable(IntegerVariable i, int id, int watch_index = -1);
1262
1263 // Because the coeff is always positive, whatching an affine expression is
1264 // the same as watching its var.
WatchLowerBound(AffineExpression e,int id)1265 void WatchLowerBound(AffineExpression e, int id) {
1266 WatchLowerBound(e.var, id);
1267 }
WatchUpperBound(AffineExpression e,int id)1268 void WatchUpperBound(AffineExpression e, int id) {
1269 WatchUpperBound(e.var, id);
1270 }
WatchAffineExpression(AffineExpression e,int id)1271 void WatchAffineExpression(AffineExpression e, int id) {
1272 WatchIntegerVariable(e.var, id);
1273 }
1274
1275 // No-op overload for "constant" IntegerVariable that are sometimes templated
1276 // as an IntegerValue.
WatchLowerBound(IntegerValue i,int id)1277 void WatchLowerBound(IntegerValue i, int id) {}
WatchUpperBound(IntegerValue i,int id)1278 void WatchUpperBound(IntegerValue i, int id) {}
WatchIntegerVariable(IntegerValue v,int id)1279 void WatchIntegerVariable(IntegerValue v, int id) {}
1280
1281 // Registers a reversible class with a given propagator. This class will be
1282 // changed to the correct state just before the propagator is called.
1283 //
1284 // Doing it just before should minimize cache-misses and bundle as much as
1285 // possible the "backtracking" together. Many propagators only watches a
1286 // few variables and will not be called at each decision levels.
1287 void RegisterReversibleClass(int id, ReversibleInterface* rev);
1288
1289 // Registers a reversible int with a given propagator. The int will be changed
1290 // to its correct value just before Propagate() is called.
1291 //
1292 // Note that this will work in O(num_rev_int_of_propagator_id) per call to
1293 // Propagate() and happens at most once per decision level. As such this is
1294 // meant for classes that have just a few reversible ints or that will have a
1295 // similar complexity anyway.
1296 //
1297 // Alternatively, one can directly get the underlying RevRepository<int> with
1298 // a call to model.Get<>(), and use SaveWithStamp() before each modification
1299 // to have just a slight overhead per int updates. This later option is what
1300 // is usually done in a CP solver at the cost of a sligthly more complex API.
1301 void RegisterReversibleInt(int id, int* rev);
1302
1303 // Returns the number of registered propagators.
NumPropagators()1304 int NumPropagators() const { return in_queue_.size(); }
1305
1306 // Set a callback for new variable bounds at level 0.
1307 //
1308 // This will be called (only at level zero) with the list of IntegerVariable
1309 // with changed lower bounds. Note that it might be called more than once
1310 // during the same propagation cycle if we fix variables in "stages".
1311 //
1312 // Also note that this will be called if some BooleanVariable where fixed even
1313 // if no IntegerVariable are changed, so the passed vector to the function
1314 // might be empty.
RegisterLevelZeroModifiedVariablesCallback(const std::function<void (const std::vector<IntegerVariable> &)> cb)1315 void RegisterLevelZeroModifiedVariablesCallback(
1316 const std::function<void(const std::vector<IntegerVariable>&)> cb) {
1317 level_zero_modified_variable_callback_.push_back(cb);
1318 }
1319
1320 // Returns the id of the propagator we are currently calling. This is meant
1321 // to be used from inside Propagate() in case a propagator was registered
1322 // more than once at different priority for instance.
GetCurrentId()1323 int GetCurrentId() const { return current_id_; }
1324
1325 private:
1326 // Updates queue_ and in_queue_ with the propagator ids that need to be
1327 // called.
1328 void UpdateCallingNeeds(Trail* trail);
1329
1330 TimeLimit* time_limit_;
1331 IntegerTrail* integer_trail_;
1332 RevIntRepository* rev_int_repository_;
1333
1334 struct WatchData {
1335 int id;
1336 int watch_index;
1337 bool operator==(const WatchData& o) const {
1338 return id == o.id && watch_index == o.watch_index;
1339 }
1340 };
1341 absl::StrongVector<LiteralIndex, std::vector<WatchData>> literal_to_watcher_;
1342 absl::StrongVector<IntegerVariable, std::vector<WatchData>> var_to_watcher_;
1343 std::vector<PropagatorInterface*> watchers_;
1344 SparseBitset<IntegerVariable> modified_vars_;
1345
1346 // Propagator ids that needs to be called. There is one queue per priority but
1347 // just one Boolean to indicate if a propagator is in one of them.
1348 std::vector<std::deque<int>> queue_by_priority_;
1349 std::vector<bool> in_queue_;
1350
1351 // Data for each propagator.
1352 DEFINE_INT_TYPE(IdType, int32_t);
1353 std::vector<int> id_to_level_at_last_call_;
1354 RevVector<IdType, int> id_to_greatest_common_level_since_last_call_;
1355 std::vector<std::vector<ReversibleInterface*>> id_to_reversible_classes_;
1356 std::vector<std::vector<int*>> id_to_reversible_ints_;
1357 std::vector<std::vector<int>> id_to_watch_indices_;
1358 std::vector<int> id_to_priority_;
1359 std::vector<int> id_to_idempotence_;
1360
1361 // Special propagators that needs to always be called at level zero.
1362 std::vector<int> propagator_ids_to_call_at_level_zero_;
1363
1364 // The id of the propagator we just called.
1365 int current_id_;
1366
1367 std::vector<std::function<void(const std::vector<IntegerVariable>&)>>
1368 level_zero_modified_variable_callback_;
1369
1370 DISALLOW_COPY_AND_ASSIGN(GenericLiteralWatcher);
1371 };
1372
1373 // ============================================================================
1374 // Implementation.
1375 // ============================================================================
1376
GreaterOrEqual(IntegerVariable i,IntegerValue bound)1377 inline IntegerLiteral IntegerLiteral::GreaterOrEqual(IntegerVariable i,
1378 IntegerValue bound) {
1379 return IntegerLiteral(
1380 i, bound > kMaxIntegerValue ? kMaxIntegerValue + 1 : bound);
1381 }
1382
LowerOrEqual(IntegerVariable i,IntegerValue bound)1383 inline IntegerLiteral IntegerLiteral::LowerOrEqual(IntegerVariable i,
1384 IntegerValue bound) {
1385 return IntegerLiteral(
1386 NegationOf(i), bound < kMinIntegerValue ? kMaxIntegerValue + 1 : -bound);
1387 }
1388
TrueLiteral()1389 inline IntegerLiteral IntegerLiteral::TrueLiteral() {
1390 return IntegerLiteral(kNoIntegerVariable, IntegerValue(-1));
1391 }
1392
FalseLiteral()1393 inline IntegerLiteral IntegerLiteral::FalseLiteral() {
1394 return IntegerLiteral(kNoIntegerVariable, IntegerValue(1));
1395 }
1396
Negated()1397 inline IntegerLiteral IntegerLiteral::Negated() const {
1398 // Note that bound >= kMinIntegerValue, so -bound + 1 will have the correct
1399 // capped value.
1400 return IntegerLiteral(
1401 NegationOf(IntegerVariable(var)),
1402 bound > kMaxIntegerValue ? kMinIntegerValue : -bound + 1);
1403 }
1404
1405 // var * coeff + constant >= bound.
GreaterOrEqual(IntegerValue bound)1406 inline IntegerLiteral AffineExpression::GreaterOrEqual(
1407 IntegerValue bound) const {
1408 if (var == kNoIntegerVariable) {
1409 return constant >= bound ? IntegerLiteral::TrueLiteral()
1410 : IntegerLiteral::FalseLiteral();
1411 }
1412 DCHECK_GT(coeff, 0);
1413 return IntegerLiteral::GreaterOrEqual(var,
1414 CeilRatio(bound - constant, coeff));
1415 }
1416
GreaterOrEqual(int64_t bound)1417 inline IntegerLiteral AffineExpression::GreaterOrEqual(int64_t bound) const {
1418 return GreaterOrEqual(IntegerValue(bound));
1419 }
1420
1421 // var * coeff + constant <= bound.
LowerOrEqual(IntegerValue bound)1422 inline IntegerLiteral AffineExpression::LowerOrEqual(IntegerValue bound) const {
1423 if (var == kNoIntegerVariable) {
1424 return constant <= bound ? IntegerLiteral::TrueLiteral()
1425 : IntegerLiteral::FalseLiteral();
1426 }
1427 DCHECK_GT(coeff, 0);
1428 return IntegerLiteral::LowerOrEqual(var, FloorRatio(bound - constant, coeff));
1429 }
1430
LowerOrEqual(int64_t bound)1431 inline IntegerLiteral AffineExpression::LowerOrEqual(int64_t bound) const {
1432 return LowerOrEqual(IntegerValue(bound));
1433 }
1434
LowerBound(IntegerVariable i)1435 inline IntegerValue IntegerTrail::LowerBound(IntegerVariable i) const {
1436 return vars_[i].current_bound;
1437 }
1438
UpperBound(IntegerVariable i)1439 inline IntegerValue IntegerTrail::UpperBound(IntegerVariable i) const {
1440 return -vars_[NegationOf(i)].current_bound;
1441 }
1442
IsFixed(IntegerVariable i)1443 inline bool IntegerTrail::IsFixed(IntegerVariable i) const {
1444 return vars_[i].current_bound == -vars_[NegationOf(i)].current_bound;
1445 }
1446
FixedValue(IntegerVariable i)1447 inline IntegerValue IntegerTrail::FixedValue(IntegerVariable i) const {
1448 DCHECK(IsFixed(i));
1449 return vars_[i].current_bound;
1450 }
1451
ConditionalLowerBound(Literal l,IntegerVariable i)1452 inline IntegerValue IntegerTrail::ConditionalLowerBound(
1453 Literal l, IntegerVariable i) const {
1454 const auto it = conditional_lbs_.find({l.Index(), i});
1455 if (it != conditional_lbs_.end()) {
1456 return std::max(vars_[i].current_bound, it->second);
1457 }
1458 return vars_[i].current_bound;
1459 }
1460
ConditionalLowerBound(Literal l,AffineExpression expr)1461 inline IntegerValue IntegerTrail::ConditionalLowerBound(
1462 Literal l, AffineExpression expr) const {
1463 if (expr.var == kNoIntegerVariable) return expr.constant;
1464 return ConditionalLowerBound(l, expr.var) * expr.coeff + expr.constant;
1465 }
1466
LowerBoundAsLiteral(IntegerVariable i)1467 inline IntegerLiteral IntegerTrail::LowerBoundAsLiteral(
1468 IntegerVariable i) const {
1469 return IntegerLiteral::GreaterOrEqual(i, LowerBound(i));
1470 }
1471
UpperBoundAsLiteral(IntegerVariable i)1472 inline IntegerLiteral IntegerTrail::UpperBoundAsLiteral(
1473 IntegerVariable i) const {
1474 return IntegerLiteral::LowerOrEqual(i, UpperBound(i));
1475 }
1476
LowerBound(AffineExpression expr)1477 inline IntegerValue IntegerTrail::LowerBound(AffineExpression expr) const {
1478 if (expr.var == kNoIntegerVariable) return expr.constant;
1479 return LowerBound(expr.var) * expr.coeff + expr.constant;
1480 }
1481
UpperBound(AffineExpression expr)1482 inline IntegerValue IntegerTrail::UpperBound(AffineExpression expr) const {
1483 if (expr.var == kNoIntegerVariable) return expr.constant;
1484 return UpperBound(expr.var) * expr.coeff + expr.constant;
1485 }
1486
IsFixed(AffineExpression expr)1487 inline bool IntegerTrail::IsFixed(AffineExpression expr) const {
1488 if (expr.var == kNoIntegerVariable) return true;
1489 return IsFixed(expr.var);
1490 }
1491
FixedValue(AffineExpression expr)1492 inline IntegerValue IntegerTrail::FixedValue(AffineExpression expr) const {
1493 if (expr.var == kNoIntegerVariable) return expr.constant;
1494 return FixedValue(expr.var) * expr.coeff + expr.constant;
1495 }
1496
LowerBoundAsLiteral(AffineExpression expr)1497 inline IntegerLiteral IntegerTrail::LowerBoundAsLiteral(
1498 AffineExpression expr) const {
1499 if (expr.var == kNoIntegerVariable) return IntegerLiteral::TrueLiteral();
1500 return IntegerLiteral::GreaterOrEqual(expr.var, LowerBound(expr.var));
1501 }
1502
UpperBoundAsLiteral(AffineExpression expr)1503 inline IntegerLiteral IntegerTrail::UpperBoundAsLiteral(
1504 AffineExpression expr) const {
1505 if (expr.var == kNoIntegerVariable) return IntegerLiteral::TrueLiteral();
1506 return IntegerLiteral::LowerOrEqual(expr.var, UpperBound(expr.var));
1507 }
1508
IntegerLiteralIsTrue(IntegerLiteral l)1509 inline bool IntegerTrail::IntegerLiteralIsTrue(IntegerLiteral l) const {
1510 return l.bound <= LowerBound(l.var);
1511 }
1512
IntegerLiteralIsFalse(IntegerLiteral l)1513 inline bool IntegerTrail::IntegerLiteralIsFalse(IntegerLiteral l) const {
1514 return l.bound > UpperBound(l.var);
1515 }
1516
1517 // The level zero bounds are stored at the beginning of the trail and they also
1518 // serves as sentinels. Their index match the variables index.
LevelZeroLowerBound(IntegerVariable var)1519 inline IntegerValue IntegerTrail::LevelZeroLowerBound(
1520 IntegerVariable var) const {
1521 return integer_trail_[var.value()].bound;
1522 }
1523
LevelZeroUpperBound(IntegerVariable var)1524 inline IntegerValue IntegerTrail::LevelZeroUpperBound(
1525 IntegerVariable var) const {
1526 return -integer_trail_[NegationOf(var).value()].bound;
1527 }
1528
IsFixedAtLevelZero(IntegerVariable var)1529 inline bool IntegerTrail::IsFixedAtLevelZero(IntegerVariable var) const {
1530 return integer_trail_[var.value()].bound ==
1531 -integer_trail_[NegationOf(var).value()].bound;
1532 }
1533
LevelZeroLowerBound(AffineExpression expr)1534 inline IntegerValue IntegerTrail::LevelZeroLowerBound(
1535 AffineExpression expr) const {
1536 if (expr.var == kNoIntegerVariable) return expr.constant;
1537 return expr.ValueAt(LevelZeroLowerBound(expr.var));
1538 }
1539
LevelZeroUpperBound(AffineExpression expr)1540 inline IntegerValue IntegerTrail::LevelZeroUpperBound(
1541 AffineExpression expr) const {
1542 if (expr.var == kNoIntegerVariable) return expr.constant;
1543 return expr.ValueAt(LevelZeroUpperBound(expr.var));
1544 }
1545
IsFixedAtLevelZero(AffineExpression expr)1546 inline bool IntegerTrail::IsFixedAtLevelZero(AffineExpression expr) const {
1547 if (expr.var == kNoIntegerVariable) return true;
1548 return IsFixedAtLevelZero(expr.var);
1549 }
1550
WatchLiteral(Literal l,int id,int watch_index)1551 inline void GenericLiteralWatcher::WatchLiteral(Literal l, int id,
1552 int watch_index) {
1553 if (l.Index() >= literal_to_watcher_.size()) {
1554 literal_to_watcher_.resize(l.Index().value() + 1);
1555 }
1556 literal_to_watcher_[l.Index()].push_back({id, watch_index});
1557 }
1558
WatchLowerBound(IntegerVariable var,int id,int watch_index)1559 inline void GenericLiteralWatcher::WatchLowerBound(IntegerVariable var, int id,
1560 int watch_index) {
1561 if (var == kNoIntegerVariable) return;
1562 if (var.value() >= var_to_watcher_.size()) {
1563 var_to_watcher_.resize(var.value() + 1);
1564 }
1565
1566 // Minor optim, so that we don't watch the same variable twice. Propagator
1567 // code is easier this way since for example when one wants to watch both
1568 // an interval start and interval end, both might have the same underlying
1569 // variable.
1570 const WatchData data = {id, watch_index};
1571 if (!var_to_watcher_[var].empty() && var_to_watcher_[var].back() == data) {
1572 return;
1573 }
1574 var_to_watcher_[var].push_back(data);
1575 }
1576
WatchUpperBound(IntegerVariable var,int id,int watch_index)1577 inline void GenericLiteralWatcher::WatchUpperBound(IntegerVariable var, int id,
1578 int watch_index) {
1579 if (var == kNoIntegerVariable) return;
1580 WatchLowerBound(NegationOf(var), id, watch_index);
1581 }
1582
WatchIntegerVariable(IntegerVariable i,int id,int watch_index)1583 inline void GenericLiteralWatcher::WatchIntegerVariable(IntegerVariable i,
1584 int id,
1585 int watch_index) {
1586 WatchLowerBound(i, id, watch_index);
1587 WatchUpperBound(i, id, watch_index);
1588 }
1589
1590 // ============================================================================
1591 // Model based functions.
1592 //
1593 // Note that in the model API, we simply use int64_t for the integer values, so
1594 // that it is nicer for the client. Internally these are converted to
1595 // IntegerValue which is typechecked.
1596 // ============================================================================
1597
NewBooleanVariable()1598 inline std::function<BooleanVariable(Model*)> NewBooleanVariable() {
1599 return [=](Model* model) {
1600 return model->GetOrCreate<SatSolver>()->NewBooleanVariable();
1601 };
1602 }
1603
ConstantIntegerVariable(int64_t value)1604 inline std::function<IntegerVariable(Model*)> ConstantIntegerVariable(
1605 int64_t value) {
1606 return [=](Model* model) {
1607 return model->GetOrCreate<IntegerTrail>()
1608 ->GetOrCreateConstantIntegerVariable(IntegerValue(value));
1609 };
1610 }
1611
NewIntegerVariable(int64_t lb,int64_t ub)1612 inline std::function<IntegerVariable(Model*)> NewIntegerVariable(int64_t lb,
1613 int64_t ub) {
1614 return [=](Model* model) {
1615 CHECK_LE(lb, ub);
1616 return model->GetOrCreate<IntegerTrail>()->AddIntegerVariable(
1617 IntegerValue(lb), IntegerValue(ub));
1618 };
1619 }
1620
NewIntegerVariable(const Domain & domain)1621 inline std::function<IntegerVariable(Model*)> NewIntegerVariable(
1622 const Domain& domain) {
1623 return [=](Model* model) {
1624 return model->GetOrCreate<IntegerTrail>()->AddIntegerVariable(domain);
1625 };
1626 }
1627
1628 // Creates a 0-1 integer variable "view" of the given literal. It will have a
1629 // value of 1 when the literal is true, and 0 when the literal is false.
NewIntegerVariableFromLiteral(Literal lit)1630 inline std::function<IntegerVariable(Model*)> NewIntegerVariableFromLiteral(
1631 Literal lit) {
1632 return [=](Model* model) {
1633 auto* encoder = model->GetOrCreate<IntegerEncoder>();
1634 const IntegerVariable candidate = encoder->GetLiteralView(lit);
1635 if (candidate != kNoIntegerVariable) return candidate;
1636
1637 IntegerVariable var;
1638 const auto& assignment = model->GetOrCreate<SatSolver>()->Assignment();
1639 if (assignment.LiteralIsTrue(lit)) {
1640 var = model->Add(ConstantIntegerVariable(1));
1641 } else if (assignment.LiteralIsFalse(lit)) {
1642 var = model->Add(ConstantIntegerVariable(0));
1643 } else {
1644 var = model->Add(NewIntegerVariable(0, 1));
1645 }
1646
1647 encoder->AssociateToIntegerEqualValue(lit, var, IntegerValue(1));
1648 DCHECK_NE(encoder->GetLiteralView(lit), kNoIntegerVariable);
1649 return var;
1650 };
1651 }
1652
LowerBound(IntegerVariable v)1653 inline std::function<int64_t(const Model&)> LowerBound(IntegerVariable v) {
1654 return [=](const Model& model) {
1655 return model.Get<IntegerTrail>()->LowerBound(v).value();
1656 };
1657 }
1658
UpperBound(IntegerVariable v)1659 inline std::function<int64_t(const Model&)> UpperBound(IntegerVariable v) {
1660 return [=](const Model& model) {
1661 return model.Get<IntegerTrail>()->UpperBound(v).value();
1662 };
1663 }
1664
IsFixed(IntegerVariable v)1665 inline std::function<bool(const Model&)> IsFixed(IntegerVariable v) {
1666 return [=](const Model& model) {
1667 const IntegerTrail* trail = model.Get<IntegerTrail>();
1668 return trail->LowerBound(v) == trail->UpperBound(v);
1669 };
1670 }
1671
1672 // This checks that the variable is fixed.
Value(IntegerVariable v)1673 inline std::function<int64_t(const Model&)> Value(IntegerVariable v) {
1674 return [=](const Model& model) {
1675 const IntegerTrail* trail = model.Get<IntegerTrail>();
1676 CHECK_EQ(trail->LowerBound(v), trail->UpperBound(v)) << v;
1677 return trail->LowerBound(v).value();
1678 };
1679 }
1680
GreaterOrEqual(IntegerVariable v,int64_t lb)1681 inline std::function<void(Model*)> GreaterOrEqual(IntegerVariable v,
1682 int64_t lb) {
1683 return [=](Model* model) {
1684 if (!model->GetOrCreate<IntegerTrail>()->Enqueue(
1685 IntegerLiteral::GreaterOrEqual(v, IntegerValue(lb)),
1686 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1687 model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1688 VLOG(1) << "Model trivially infeasible, variable " << v
1689 << " has upper bound " << model->Get(UpperBound(v))
1690 << " and GreaterOrEqual() was called with a lower bound of "
1691 << lb;
1692 }
1693 };
1694 }
1695
LowerOrEqual(IntegerVariable v,int64_t ub)1696 inline std::function<void(Model*)> LowerOrEqual(IntegerVariable v, int64_t ub) {
1697 return [=](Model* model) {
1698 if (!model->GetOrCreate<IntegerTrail>()->Enqueue(
1699 IntegerLiteral::LowerOrEqual(v, IntegerValue(ub)),
1700 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1701 model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1702 LOG(WARNING) << "Model trivially infeasible, variable " << v
1703 << " has lower bound " << model->Get(LowerBound(v))
1704 << " and LowerOrEqual() was called with an upper bound of "
1705 << ub;
1706 }
1707 };
1708 }
1709
1710 // Fix v to a given value.
Equality(IntegerVariable v,int64_t value)1711 inline std::function<void(Model*)> Equality(IntegerVariable v, int64_t value) {
1712 return [=](Model* model) {
1713 model->Add(LowerOrEqual(v, value));
1714 model->Add(GreaterOrEqual(v, value));
1715 };
1716 }
1717
1718 // TODO(user): This is one of the rare case where it is better to use Equality()
1719 // rather than two Implications(). Maybe we should modify our internal
1720 // implementation to use half-reified encoding? that is do not propagate the
1721 // direction integer-bound => literal, but just literal => integer-bound? This
1722 // is the same as using different underlying variable for an integer literal and
1723 // its negation.
Implication(const std::vector<Literal> & enforcement_literals,IntegerLiteral i)1724 inline std::function<void(Model*)> Implication(
1725 const std::vector<Literal>& enforcement_literals, IntegerLiteral i) {
1726 return [=](Model* model) {
1727 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
1728 if (i.bound <= integer_trail->LowerBound(i.var)) {
1729 // Always true! nothing to do.
1730 } else if (i.bound > integer_trail->UpperBound(i.var)) {
1731 // Always false.
1732 std::vector<Literal> clause;
1733 for (const Literal literal : enforcement_literals) {
1734 clause.push_back(literal.Negated());
1735 }
1736 model->Add(ClauseConstraint(clause));
1737 } else {
1738 // TODO(user): Double check what happen when we associate a trivially
1739 // true or false literal.
1740 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1741 std::vector<Literal> clause{encoder->GetOrCreateAssociatedLiteral(i)};
1742 for (const Literal literal : enforcement_literals) {
1743 clause.push_back(literal.Negated());
1744 }
1745 model->Add(ClauseConstraint(clause));
1746 }
1747 };
1748 }
1749
1750 // in_interval => v in [lb, ub].
ImpliesInInterval(Literal in_interval,IntegerVariable v,int64_t lb,int64_t ub)1751 inline std::function<void(Model*)> ImpliesInInterval(Literal in_interval,
1752 IntegerVariable v,
1753 int64_t lb, int64_t ub) {
1754 return [=](Model* model) {
1755 if (lb == ub) {
1756 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1757 model->Add(Implication({in_interval},
1758 encoder->GetOrCreateLiteralAssociatedToEquality(
1759 v, IntegerValue(lb))));
1760 return;
1761 }
1762 model->Add(Implication(
1763 {in_interval}, IntegerLiteral::GreaterOrEqual(v, IntegerValue(lb))));
1764 model->Add(Implication({in_interval},
1765 IntegerLiteral::LowerOrEqual(v, IntegerValue(ub))));
1766 };
1767 }
1768
1769 // Calling model.Add(FullyEncodeVariable(var)) will create one literal per value
1770 // in the domain of var (if not already done), and wire everything correctly.
1771 // This also returns the full encoding, see the FullDomainEncoding() method of
1772 // the IntegerEncoder class.
FullyEncodeVariable(IntegerVariable var)1773 inline std::function<std::vector<ValueLiteralPair>(Model*)> FullyEncodeVariable(
1774 IntegerVariable var) {
1775 return [=](Model* model) {
1776 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1777 if (!encoder->VariableIsFullyEncoded(var)) {
1778 encoder->FullyEncodeVariable(var);
1779 }
1780 return encoder->FullDomainEncoding(var);
1781 };
1782 }
1783
1784 // Same as ExcludeCurrentSolutionAndBacktrack() but this version works for an
1785 // integer problem with optional variables. The issue is that an optional
1786 // variable that is ignored can basically take any value, and we don't really
1787 // want to enumerate them. This function should exclude all solutions where
1788 // only the ignored variable values change.
1789 std::function<void(Model*)>
1790 ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack();
1791
1792 } // namespace sat
1793 } // namespace operations_research
1794
1795 #endif // OR_TOOLS_SAT_INTEGER_H_
1796