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