OR-Tools  8.1
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"
31 #include "ortools/base/int_type.h"
33 #include "ortools/base/logging.h"
34 #include "ortools/base/macros.h"
35 #include "ortools/base/map_util.h"
38 #include "ortools/sat/model.h"
39 #include "ortools/sat/sat_base.h"
40 #include "ortools/sat/sat_solver.h"
41 #include "ortools/util/bitset.h"
42 #include "ortools/util/rev.h"
45 
46 namespace operations_research {
47 namespace 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.
56 DEFINE_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.
65 constexpr IntegerValue kMaxIntegerValue(
67 constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue);
68 
69 inline 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 
76 template <class IntType>
77 inline IntType IntTypeAbs(IntType t) {
78  return IntType(std::abs(t.value()));
79 }
80 
81 inline 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 
90 inline 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.
102 inline 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.
110 inline 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.
124 DEFINE_INT_TYPE(IntegerVariable, int32);
125 const IntegerVariable kNoIntegerVariable(-1);
126 inline IntegerVariable NegationOf(IntegerVariable i) {
127  return IntegerVariable(i.value() ^ 1);
128 }
129 
130 inline bool VariableIsPositive(IntegerVariable i) {
131  return (i.value() & 1) == 0;
132 }
133 
134 inline 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).
139 DEFINE_INT_TYPE(PositiveOnlyIndex, int32);
140 inline PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var) {
141  return PositiveOnlyIndex(var.value() / 2);
142 }
143 
144 // Returns the vector of the negated variables.
145 std::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 
175  bool operator==(IntegerLiteral o) const {
176  return var == o.var && bound == o.bound;
177  }
178  bool operator!=(IntegerLiteral o) const {
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 
193 inline std::ostream& operator<<(std::ostream& os, IntegerLiteral i_lit) {
194  os << i_lit.DebugString();
195  return os;
196 }
197 
198 using 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 
228  bool operator==(AffineExpression o) const {
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.
246 struct IntegerDomains : public absl::StrongVector<IntegerVariable, Domain> {
247  explicit IntegerDomains(Model* model) {}
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> {
255  explicit DebugSolution(Model* model) {}
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  // Returns a Boolean literal associated with a bound lower than or equal to
426  // the one of the given IntegerLiteral. If the given IntegerLiteral is true,
427  // then the returned literal should be true too. Returns kNoLiteralIndex if no
428  // such literal was created.
429  //
430  // Ex: if 'i' is (x >= 4) and we already created a literal associated to
431  // (x >= 2) but not to (x >= 3), we will return the literal associated with
432  // (x >= 2).
434  IntegerValue* bound) const;
435 
436  // Gets the literal always set to true, make it if it does not exist.
438  DCHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
439  if (literal_index_true_ == kNoLiteralIndex) {
440  const Literal literal_true =
441  Literal(sat_solver_->NewBooleanVariable(), true);
442  literal_index_true_ = literal_true.Index();
443  sat_solver_->AddUnitClause(literal_true);
444  }
445  return Literal(literal_index_true_);
446  }
448 
449  // Returns the set of Literal associated to IntegerLiteral of the form var >=
450  // value. We make a copy, because this can be easily invalidated when calling
451  // any function of this class. So it is less efficient but safer.
452  std::map<IntegerValue, Literal> PartialGreaterThanEncoding(
453  IntegerVariable var) const {
454  if (var >= encoding_by_var_.size()) {
455  return std::map<IntegerValue, Literal>();
456  }
457  return encoding_by_var_[var];
458  }
459 
460  private:
461  // Only add the equivalence between i_lit and literal, if there is already an
462  // associated literal with i_lit, this make literal and this associated
463  // literal equivalent.
464  void HalfAssociateGivenLiteral(IntegerLiteral i_lit, Literal literal);
465 
466  // Adds the implications:
467  // Literal(before) <= associated_lit <= Literal(after).
468  // Arguments:
469  // - map is just encoding_by_var_[associated_lit.var] and is passed as a
470  // slight optimization.
471  // - 'it' is the current position of associated_lit in map, i.e we must have
472  // it->second == associated_lit.
473  void AddImplications(const std::map<IntegerValue, Literal>& map,
474  std::map<IntegerValue, Literal>::const_iterator it,
475  Literal associated_lit);
476 
477  SatSolver* sat_solver_;
478  IntegerDomains* domains_;
479 
480  bool add_implications_ = true;
481  int64 num_created_variables_ = 0;
482 
483  // We keep all the literals associated to an Integer variable in a map ordered
484  // by bound (so we can properly add implications between the literals
485  // corresponding to the same variable).
486  //
487  // TODO(user): Remove the entry no longer needed because of level zero
488  // propagations.
490  encoding_by_var_;
491 
492  // Store for a given LiteralIndex the list of its associated IntegerLiterals.
493  const InlinedIntegerLiteralVector empty_integer_literal_vector_;
495  reverse_encoding_;
497  full_reverse_encoding_;
498  std::vector<IntegerLiteral> newly_fixed_integer_literals_;
499 
500  // Store for a given LiteralIndex its IntegerVariable view or kNoLiteralIndex
501  // if there is none.
503 
504  // Mapping (variable == value) -> associated literal. Note that even if
505  // there is more than one literal associated to the same fact, we just keep
506  // the first one that was added.
507  //
508  // Note that we only keep positive IntegerVariable here to reduce memory
509  // usage.
510  absl::flat_hash_map<std::pair<PositiveOnlyIndex, IntegerValue>, Literal>
511  equality_to_associated_literal_;
512 
513  // Mutable because this is lazily cleaned-up by PartialDomainEncoding().
515  equality_by_var_;
516 
517  // Variables that are fully encoded.
518  mutable absl::StrongVector<PositiveOnlyIndex, bool> is_fully_encoded_;
519 
520  // A literal that is always true, convenient to encode trivial domains.
521  // This will be lazily created when needed.
522  LiteralIndex literal_index_true_ = kNoLiteralIndex;
523 
524  // Temporary memory used by FullyEncodeVariable().
525  std::vector<IntegerValue> tmp_values_;
526 
527  DISALLOW_COPY_AND_ASSIGN(IntegerEncoder);
528 };
529 
530 // This class maintains a set of integer variables with their current bounds.
531 // Bounds can be propagated from an external "source" and this class helps
532 // to maintain the reason for each propagation.
533 class IntegerTrail : public SatPropagator {
534  public:
536  : SatPropagator("IntegerTrail"),
537  domains_(model->GetOrCreate<IntegerDomains>()),
538  encoder_(model->GetOrCreate<IntegerEncoder>()),
539  trail_(model->GetOrCreate<Trail>()),
540  parameters_(*model->GetOrCreate<SatParameters>()) {
541  model->GetOrCreate<SatSolver>()->AddPropagator(this);
542  }
543  ~IntegerTrail() final;
544 
545  // SatPropagator interface. These functions make sure the current bounds
546  // information is in sync with the current solver literal trail. Any
547  // class/propagator using this class must make sure it is synced to the
548  // correct state before calling any of its functions.
549  bool Propagate(Trail* trail) final;
550  void Untrail(const Trail& trail, int literal_trail_index) final;
551  absl::Span<const Literal> Reason(const Trail& trail,
552  int trail_index) const final;
553 
554  // Returns the number of created integer variables.
555  //
556  // Note that this is twice the number of call to AddIntegerVariable() since
557  // we automatically create the NegationOf() variable too.
558  IntegerVariable NumIntegerVariables() const {
559  return IntegerVariable(vars_.size());
560  }
561 
562  // Optimization: you can call this before calling AddIntegerVariable()
563  // num_vars time.
564  void ReserveSpaceForNumVariables(int num_vars);
565 
566  // Adds a new integer variable. Adding integer variable can only be done when
567  // the decision level is zero (checked). The given bounds are INCLUSIVE and
568  // must not cross.
569  //
570  // Note on integer overflow: 'upper_bound - lower_bound' must fit on an int64,
571  // this is DCHECKed. More generally, depending on the constraints that are
572  // added, the bounds magnitude must be small enough to satisfy each constraint
573  // overflow precondition.
574  IntegerVariable AddIntegerVariable(IntegerValue lower_bound,
575  IntegerValue upper_bound);
576 
577  // Same as above but for a more complex domain specified as a sorted list of
578  // disjoint intervals. See the Domain class.
579  IntegerVariable AddIntegerVariable(const Domain& domain);
580 
581  // Returns the initial domain of the given variable. Note that the min/max
582  // are updated with level zero propagation, but not holes.
583  const Domain& InitialVariableDomain(IntegerVariable var) const;
584 
585  // Takes the intersection with the current initial variable domain.
586  //
587  // TODO(user): There is some memory inefficiency if this is called many time
588  // because of the underlying data structure we use. In practice, when used
589  // with a presolve, this is not often used, so that is fine though.
590  bool UpdateInitialDomain(IntegerVariable var, Domain domain);
591 
592  // Same as AddIntegerVariable(value, value), but this is a bit more efficient
593  // because it reuses another constant with the same value if its exist.
594  //
595  // Note(user): Creating constant integer variable is a bit wasteful, but not
596  // that much, and it allows to simplify a lot of constraints that do not need
597  // to handle this case any differently than the general one. Maybe there is a
598  // better solution, but this is not really high priority as of December 2016.
599  IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value);
600  int NumConstantVariables() const;
601 
602  // Same as AddIntegerVariable() but uses the maximum possible range. Note
603  // that since we take negation of bounds in various places, we make sure that
604  // we don't have overflow when we take the negation of the lower bound or of
605  // the upper bound.
606  IntegerVariable AddIntegerVariable() {
608  }
609 
610  // For an optional variable, both its lb and ub must be valid bound assuming
611  // the fact that the variable is "present". However, the domain [lb, ub] is
612  // allowed to be empty (i.e. ub < lb) if the given is_ignored literal is true.
613  // Moreover, if is_ignored is true, then the bound of such variable should NOT
614  // impact any non-ignored variable in any way (but the reverse is not true).
615  bool IsOptional(IntegerVariable i) const {
616  return is_ignored_literals_[i] != kNoLiteralIndex;
617  }
618  bool IsCurrentlyIgnored(IntegerVariable i) const {
619  const LiteralIndex is_ignored_literal = is_ignored_literals_[i];
620  return is_ignored_literal != kNoLiteralIndex &&
621  trail_->Assignment().LiteralIsTrue(Literal(is_ignored_literal));
622  }
623  Literal IsIgnoredLiteral(IntegerVariable i) const {
624  DCHECK(IsOptional(i));
625  return Literal(is_ignored_literals_[i]);
626  }
627  LiteralIndex OptionalLiteralIndex(IntegerVariable i) const {
628  return is_ignored_literals_[i] == kNoLiteralIndex
630  : Literal(is_ignored_literals_[i]).NegatedIndex();
631  }
632  void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered) {
633  DCHECK(is_ignored_literals_[i] == kNoLiteralIndex ||
634  is_ignored_literals_[i] == is_considered.NegatedIndex());
635  is_ignored_literals_[i] = is_considered.NegatedIndex();
636  is_ignored_literals_[NegationOf(i)] = is_considered.NegatedIndex();
637  }
638 
639  // Returns the current lower/upper bound of the given integer variable.
640  IntegerValue LowerBound(IntegerVariable i) const;
641  IntegerValue UpperBound(IntegerVariable i) const;
642 
643  // Checks if the variable is fixed.
644  bool IsFixed(IntegerVariable i) const;
645 
646  // Same as above for an affine expression.
647  IntegerValue LowerBound(AffineExpression expr) const;
648  IntegerValue UpperBound(AffineExpression expr) const;
649  bool IsFixed(AffineExpression expr) const;
650 
651  // Returns the integer literal that represent the current lower/upper bound of
652  // the given integer variable.
653  IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const;
654  IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const;
655 
656  // Returns the current value (if known) of an IntegerLiteral.
657  bool IntegerLiteralIsTrue(IntegerLiteral l) const;
659 
660  // Returns globally valid lower/upper bound on the given integer variable.
661  IntegerValue LevelZeroLowerBound(IntegerVariable var) const;
662  IntegerValue LevelZeroUpperBound(IntegerVariable var) const;
663 
664  // Returns true if the variable is fixed at level 0.
665  bool IsFixedAtLevelZero(IntegerVariable var) const;
666 
667  // Advanced usage. Given the reason for
668  // (Sum_i coeffs[i] * reason[i].var >= current_lb) initially in reason,
669  // this function relaxes the reason given that we only need the explanation of
670  // (Sum_i coeffs[i] * reason[i].var >= current_lb - slack).
671  //
672  // Preconditions:
673  // - coeffs must be of same size as reason, and all entry must be positive.
674  // - *reason must initially contains the trivial initial reason, that is
675  // the current lower-bound of each variables.
676  //
677  // TODO(user): Requiring all initial literal to be at their current bound is
678  // not really clean. Maybe we can change the API to only take IntegerVariable
679  // and produce the reason directly.
680  //
681  // TODO(user): change API so that this work is performed during the conflict
682  // analysis where we can be smarter in how we relax the reason. Note however
683  // that this function is mainly used when we have a conflict, so this is not
684  // really high priority.
685  //
686  // TODO(user): Test that the code work in the presence of integer overflow.
687  void RelaxLinearReason(IntegerValue slack,
688  absl::Span<const IntegerValue> coeffs,
689  std::vector<IntegerLiteral>* reason) const;
690 
691  // Same as above but take in IntegerVariables instead of IntegerLiterals.
692  void AppendRelaxedLinearReason(IntegerValue slack,
693  absl::Span<const IntegerValue> coeffs,
694  absl::Span<const IntegerVariable> vars,
695  std::vector<IntegerLiteral>* reason) const;
696 
697  // Same as above but relax the given trail indices.
698  void RelaxLinearReason(IntegerValue slack,
699  absl::Span<const IntegerValue> coeffs,
700  std::vector<int>* trail_indices) const;
701 
702  // Removes from the reasons the literal that are always true.
703  // This is mainly useful for experiments/testing.
704  void RemoveLevelZeroBounds(std::vector<IntegerLiteral>* reason) const;
705 
706  // Enqueue new information about a variable bound. Calling this with a less
707  // restrictive bound than the current one will have no effect.
708  //
709  // The reason for this "assignment" must be provided as:
710  // - A set of Literal currently beeing all false.
711  // - A set of IntegerLiteral currently beeing all true.
712  //
713  // IMPORTANT: Notice the inversed sign in the literal reason. This is a bit
714  // confusing but internally SAT use this direction for efficiency.
715  //
716  // Note(user): Duplicates Literal/IntegerLiteral are supported because we call
717  // STLSortAndRemoveDuplicates() in MergeReasonInto(), but maybe they shouldn't
718  // for efficiency reason.
719  //
720  // TODO(user): If the given bound is equal to the current bound, maybe the new
721  // reason is better? how to decide and what to do in this case? to think about
722  // it. Currently we simply don't do anything.
723  ABSL_MUST_USE_RESULT bool Enqueue(
724  IntegerLiteral i_lit, absl::Span<const Literal> literal_reason,
725  absl::Span<const IntegerLiteral> integer_reason);
726 
727  // Same as Enqueue(), but takes an extra argument which if smaller than
728  // integer_trail_.size() is interpreted as the trail index of an old Enqueue()
729  // that had the same reason as this one. Note that the given Span must still
730  // be valid as they are used in case of conflict.
731  //
732  // TODO(user): This currently cannot refer to a trail_index with a lazy
733  // reason. Fix or at least check that this is the case.
734  ABSL_MUST_USE_RESULT bool Enqueue(
735  IntegerLiteral i_lit, absl::Span<const Literal> literal_reason,
736  absl::Span<const IntegerLiteral> integer_reason,
737  int trail_index_with_same_reason);
738 
739  // Lazy reason API.
740  //
741  // The function is provided with the IntegerLiteral to explain and its index
742  // in the integer trail. It must fill the two vectors so that literals
743  // contains any Literal part of the reason and dependencies contains the trail
744  // index of any IntegerLiteral that is also part of the reason.
745  //
746  // Remark: sometimes this is called to fill the conflict while the literal
747  // to explain is propagated. In this case, trail_index_of_literal will be
748  // the current trail index, and we cannot assume that there is anything filled
749  // yet in integer_literal[trail_index_of_literal].
750  using LazyReasonFunction = std::function<void(
751  IntegerLiteral literal_to_explain, int trail_index_of_literal,
752  std::vector<Literal>* literals, std::vector<int>* dependencies)>;
753  ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit,
754  LazyReasonFunction lazy_reason);
755 
756  // Enqueues the given literal on the trail.
757  // See the comment of Enqueue() for the reason format.
758  void EnqueueLiteral(Literal literal, absl::Span<const Literal> literal_reason,
759  absl::Span<const IntegerLiteral> integer_reason);
760 
761  // Returns the reason (as set of Literal currently false) for a given integer
762  // literal. Note that the bound must be less restrictive than the current
763  // bound (checked).
764  std::vector<Literal> ReasonFor(IntegerLiteral literal) const;
765 
766  // Appends the reason for the given integer literals to the output and call
767  // STLSortAndRemoveDuplicates() on it.
768  void MergeReasonInto(absl::Span<const IntegerLiteral> literals,
769  std::vector<Literal>* output) const;
770 
771  // Returns the number of enqueues that changed a variable bounds. We don't
772  // count enqueues called with a less restrictive bound than the current one.
773  //
774  // Note(user): this can be used to see if any of the bounds changed. Just
775  // looking at the integer trail index is not enough because at level zero it
776  // doesn't change since we directly update the "fixed" bounds.
777  int64 num_enqueues() const { return num_enqueues_; }
778  int64 timestamp() const { return num_enqueues_ + num_untrails_; }
779 
780  // Same as num_enqueues but only count the level zero changes.
781  int64 num_level_zero_enqueues() const { return num_level_zero_enqueues_; }
782 
783  // All the registered bitsets will be set to one each time a LbVar is
784  // modified. It is up to the client to clear it if it wants to be notified
785  // with the newly modified variables.
788  watchers_.push_back(p);
789  }
790 
791  // Helper functions to report a conflict. Always return false so a client can
792  // simply do: return integer_trail_->ReportConflict(...);
793  bool ReportConflict(absl::Span<const Literal> literal_reason,
794  absl::Span<const IntegerLiteral> integer_reason) {
795  DCHECK(ReasonIsValid(literal_reason, integer_reason));
796  std::vector<Literal>* conflict = trail_->MutableConflict();
797  conflict->assign(literal_reason.begin(), literal_reason.end());
798  MergeReasonInto(integer_reason, conflict);
799  return false;
800  }
801  bool ReportConflict(absl::Span<const IntegerLiteral> integer_reason) {
802  DCHECK(ReasonIsValid({}, integer_reason));
803  std::vector<Literal>* conflict = trail_->MutableConflict();
804  conflict->clear();
805  MergeReasonInto(integer_reason, conflict);
806  return false;
807  }
808 
809  // Returns true if the variable lower bound is still the one from level zero.
810  bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const {
811  return vars_[var].current_trail_index < vars_.size();
812  }
813 
814  // Registers a reversible class. This class will always be synced with the
815  // correct decision level.
817  reversible_classes_.push_back(rev);
818  }
819 
820  int Index() const { return integer_trail_.size(); }
821 
822  // Inspects the trail and output all the non-level zero bounds (one per
823  // variables) to the output. The algo is sparse if there is only a few
824  // propagations on the trail.
825  void AppendNewBounds(std::vector<IntegerLiteral>* output) const;
826 
827  // Returns the trail index < threshold of a TrailEntry about var. Returns -1
828  // if there is no such entry (at a positive decision level). This is basically
829  // the trail index of the lower bound of var at the time.
830  //
831  // Important: We do some optimization internally, so this should only be
832  // used from within a LazyReasonFunction().
833  int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const;
834 
835  // Basic heuristic to detect when we are in a propagation loop, and suggest
836  // a good variable to branch on (taking the middle value) to get out of it.
837  bool InPropagationLoop() const;
838  IntegerVariable NextVariableToBranchOnInPropagationLoop() const;
839 
840  // If we had an incomplete propagation, it is important to fix all the
841  // variables and not relly on the propagation to do so. This is related to the
842  // InPropagationLoop() code above.
844  IntegerVariable FirstUnassignedVariable() const;
845 
846  // Return true if we can fix new fact at level zero.
848  return !literal_to_fix_.empty() || !integer_literal_to_fix_.empty();
849  }
850 
851  private:
852  // Used for DHECKs to validate the reason given to the public functions above.
853  // Tests that all Literal are false. Tests that all IntegerLiteral are true.
854  bool ReasonIsValid(absl::Span<const Literal> literal_reason,
855  absl::Span<const IntegerLiteral> integer_reason);
856 
857  // Called by the Enqueue() functions that detected a conflict. This does some
858  // common conflict initialization that must terminate by a call to
859  // MergeReasonIntoInternal(conflict) where conflict is the returned vector.
860  std::vector<Literal>* InitializeConflict(
861  IntegerLiteral integer_literal, const LazyReasonFunction& lazy_reason,
862  absl::Span<const Literal> literals_reason,
863  absl::Span<const IntegerLiteral> bounds_reason);
864 
865  // Internal implementation of the different public Enqueue() functions.
866  ABSL_MUST_USE_RESULT bool EnqueueInternal(
867  IntegerLiteral i_lit, LazyReasonFunction lazy_reason,
868  absl::Span<const Literal> literal_reason,
869  absl::Span<const IntegerLiteral> integer_reason,
870  int trail_index_with_same_reason);
871 
872  // Internal implementation of the EnqueueLiteral() functions.
873  void EnqueueLiteralInternal(Literal literal, LazyReasonFunction lazy_reason,
874  absl::Span<const Literal> literal_reason,
875  absl::Span<const IntegerLiteral> integer_reason);
876 
877  // Same as EnqueueInternal() but for the case where we push an IntegerLiteral
878  // because an associated Literal is true (and we know it). In this case, we
879  // have less work to do, so this has the same effect but is faster.
880  ABSL_MUST_USE_RESULT bool EnqueueAssociatedIntegerLiteral(
881  IntegerLiteral i_lit, Literal literal_reason);
882 
883  // Does the work of MergeReasonInto() when queue_ is already initialized.
884  void MergeReasonIntoInternal(std::vector<Literal>* output) const;
885 
886  // Returns the lowest trail index of a TrailEntry that can be used to explain
887  // the given IntegerLiteral. The literal must be currently true (CHECKed).
888  // Returns -1 if the explanation is trivial.
889  int FindLowestTrailIndexThatExplainBound(IntegerLiteral i_lit) const;
890 
891  // This must be called before Dependencies() or AppendLiteralsReason().
892  //
893  // TODO(user): Not really robust, try to find a better way.
894  void ComputeLazyReasonIfNeeded(int trail_index) const;
895 
896  // Helper function to return the "dependencies" of a bound assignment.
897  // All the TrailEntry at these indices are part of the reason for this
898  // assignment.
899  //
900  // Important: The returned Span is only valid up to the next call.
901  absl::Span<const int> Dependencies(int trail_index) const;
902 
903  // Helper function to append the Literal part of the reason for this bound
904  // assignment. We use added_variables_ to not add the same literal twice.
905  // Note that looking at literal.Variable() is enough since all the literals
906  // of a reason must be false.
907  void AppendLiteralsReason(int trail_index,
908  std::vector<Literal>* output) const;
909 
910  // Returns some debugging info.
911  std::string DebugString();
912 
913  // Information for each internal variable about its current bound.
914  struct VarInfo {
915  // The current bound on this variable.
916  IntegerValue current_bound;
917 
918  // Trail index of the last TrailEntry in the trail refering to this var.
919  int current_trail_index;
920  };
922 
923  // This is used by FindLowestTrailIndexThatExplainBound() and
924  // FindTrailIndexOfVarBefore() to speed up the lookup. It keeps a trail index
925  // for each variable that may or may not point to a TrailEntry regarding this
926  // variable. The validity of the index is verified before beeing used.
927  //
928  // The cache will only be updated with trail_index >= threshold.
929  mutable int var_trail_index_cache_threshold_ = 0;
930  mutable absl::StrongVector<IntegerVariable, int> var_trail_index_cache_;
931 
932  // Used by GetOrCreateConstantIntegerVariable() to return already created
933  // constant variables that share the same value.
934  absl::flat_hash_map<IntegerValue, IntegerVariable> constant_map_;
935 
936  // The integer trail. It always start by num_vars sentinel values with the
937  // level 0 bounds (in one to one correspondence with vars_).
938  struct TrailEntry {
939  IntegerValue bound;
940  IntegerVariable var;
941  int32 prev_trail_index;
942 
943  // Index in literals_reason_start_/bounds_reason_starts_ If this is -1, then
944  // this was a propagation with a lazy reason, and the reason can be
945  // re-created by calling the function lazy_reasons_[trail_index].
946  int32 reason_index;
947  };
948  std::vector<TrailEntry> integer_trail_;
949  std::vector<LazyReasonFunction> lazy_reasons_;
950 
951  // Start of each decision levels in integer_trail_.
952  // TODO(user): use more general reversible mechanism?
953  std::vector<int> integer_search_levels_;
954 
955  // Buffer to store the reason of each trail entry.
956  // Note that bounds_reason_buffer_ is an "union". It initially contains the
957  // IntegerLiteral, and is lazily replaced by the result of
958  // FindLowestTrailIndexThatExplainBound() applied to these literals. The
959  // encoding is a bit hacky, see Dependencies().
960  std::vector<int> reason_decision_levels_;
961  std::vector<int> literals_reason_starts_;
962  std::vector<int> bounds_reason_starts_;
963  std::vector<Literal> literals_reason_buffer_;
964 
965  // These two vectors are in one to one correspondence. Dependencies() will
966  // "cache" the result of the conversion from IntegerLiteral to trail indices
967  // in trail_index_reason_buffer_.
968  std::vector<IntegerLiteral> bounds_reason_buffer_;
969  mutable std::vector<int> trail_index_reason_buffer_;
970 
971  // Temporary vector filled by calls to LazyReasonFunction().
972  mutable std::vector<Literal> lazy_reason_literals_;
973  mutable std::vector<int> lazy_reason_trail_indices_;
974 
975  // The "is_ignored" literal of the optional variables or kNoLiteralIndex.
977 
978  // This is only filled for variables with a domain more complex than a single
979  // interval of values. var_to_current_lb_interval_index_[var] stores the
980  // intervals in (*domains_)[var] where the current lower-bound lies.
981  //
982  // TODO(user): Avoid using hash_map here, a simple vector should be more
983  // efficient, but we need the "rev" aspect.
984  RevMap<absl::flat_hash_map<IntegerVariable, int>>
985  var_to_current_lb_interval_index_;
986 
987  // Temporary data used by MergeReasonInto().
988  mutable bool has_dependency_ = false;
989  mutable std::vector<int> tmp_queue_;
990  mutable std::vector<IntegerVariable> tmp_to_clear_;
992  tmp_var_to_trail_index_in_queue_;
993  mutable SparseBitset<BooleanVariable> added_variables_;
994 
995  // Sometimes we propagate fact with no reason at a positive level, those
996  // will automatically be fixed on the next restart.
997  //
998  // TODO(user): If we change the logic to not restart right away, we probably
999  // need to not store duplicates bounds for the same variable.
1000  std::vector<Literal> literal_to_fix_;
1001  std::vector<IntegerLiteral> integer_literal_to_fix_;
1002 
1003  // Temporary heap used by RelaxLinearReason();
1004  struct RelaxHeapEntry {
1005  int index;
1006  IntegerValue coeff;
1007  int64 diff;
1008  bool operator<(const RelaxHeapEntry& o) const { return index < o.index; }
1009  };
1010  mutable std::vector<RelaxHeapEntry> relax_heap_;
1011  mutable std::vector<int> tmp_indices_;
1012 
1013  // Temporary data used by AppendNewBounds().
1014  mutable SparseBitset<IntegerVariable> tmp_marked_;
1015 
1016  // For EnqueueLiteral(), we store a special TrailEntry to recover the reason
1017  // lazily. This vector indicates the correspondence between a literal that
1018  // was pushed by this class at a given trail index, and the index of its
1019  // TrailEntry in integer_trail_.
1020  std::vector<int> boolean_trail_index_to_integer_one_;
1021 
1022  // We need to know if we skipped some propagation in the current branch.
1023  // This is reverted as we backtrack over it.
1024  int first_level_without_full_propagation_ = -1;
1025 
1026  int64 num_enqueues_ = 0;
1027  int64 num_untrails_ = 0;
1028  int64 num_level_zero_enqueues_ = 0;
1029  mutable int64 num_decisions_to_break_loop_ = 0;
1030 
1031  std::vector<SparseBitset<IntegerVariable>*> watchers_;
1032  std::vector<ReversibleInterface*> reversible_classes_;
1033 
1034  IntegerDomains* domains_;
1035  IntegerEncoder* encoder_;
1036  Trail* trail_;
1037  const SatParameters& parameters_;
1038 
1039  DISALLOW_COPY_AND_ASSIGN(IntegerTrail);
1040 };
1041 
1042 // Base class for CP like propagators.
1044  public:
1047 
1048  // This will be called after one or more literals that are watched by this
1049  // propagator changed. It will also always be called on the first propagation
1050  // cycle after registration.
1051  virtual bool Propagate() = 0;
1052 
1053  // This will only be called on a non-empty vector, otherwise Propagate() will
1054  // be called. The passed vector will contain the "watch index" of all the
1055  // literals that were given one at registration and that changed since the
1056  // last call to Propagate(). This is only true when going down in the search
1057  // tree, on backjump this list will be cleared.
1058  //
1059  // Notes:
1060  // - The indices may contain duplicates if the same integer variable as been
1061  // updated many times or if different watched literals have the same
1062  // watch_index.
1063  // - At level zero, it will not contain any indices associated with literals
1064  // that were already fixed when the propagator was registered. Only the
1065  // indices of the literals modified after the registration will be present.
1066  virtual bool IncrementalPropagate(const std::vector<int>& watch_indices) {
1067  LOG(FATAL) << "Not implemented.";
1068  return false; // Remove warning in Windows
1069  }
1070 };
1071 
1072 // Singleton for basic reversible types. We need the wrapper so that they can be
1073 // accessed with model->GetOrCreate<>() and properly registered at creation.
1074 class RevIntRepository : public RevRepository<int> {
1075  public:
1077  model->GetOrCreate<IntegerTrail>()->RegisterReversibleClass(this);
1078  }
1079 };
1080 class RevIntegerValueRepository : public RevRepository<IntegerValue> {
1081  public:
1083  model->GetOrCreate<IntegerTrail>()->RegisterReversibleClass(this);
1084  }
1085 };
1086 
1087 // This class allows registering Propagator that will be called if a
1088 // watched Literal or LbVar changes.
1089 //
1090 // TODO(user): Move this to its own file. Add unit tests!
1092  public:
1093  explicit GenericLiteralWatcher(Model* model);
1095 
1096  // On propagate, the registered propagators will be called if they need to
1097  // until a fixed point is reached. Propagators with low ids will tend to be
1098  // called first, but it ultimately depends on their "waking" order.
1099  bool Propagate(Trail* trail) final;
1100  void Untrail(const Trail& trail, int literal_trail_index) final;
1101 
1102  // Registers a propagator and returns its unique ids.
1103  int Register(PropagatorInterface* propagator);
1104 
1105  // Changes the priority of the propagator with given id. The priority is a
1106  // non-negative integer. Propagators with a lower priority will always be
1107  // run before the ones with a higher one. The default priority is one.
1108  void SetPropagatorPriority(int id, int priority);
1109 
1110  // The default behavior is to assume that a propagator does not need to be
1111  // called twice in a row. However, propagators on which this is called will be
1112  // called again if they change one of their own watched variables.
1114 
1115  // Whether we call a propagator even if its watched variables didn't change.
1116  // This is only used when we are back to level zero. This was introduced for
1117  // the LP propagator where we might need to continue an interrupted solve or
1118  // add extra cuts at level zero.
1119  void AlwaysCallAtLevelZero(int id);
1120 
1121  // Watches the corresponding quantity. The propagator with given id will be
1122  // called if it changes. Note that WatchLiteral() only trigger when the
1123  // literal becomes true.
1124  //
1125  // If watch_index is specified, it is associated with the watched literal.
1126  // Doing this will cause IncrementalPropagate() to be called (see the
1127  // documentation of this interface for more detail).
1128  void WatchLiteral(Literal l, int id, int watch_index = -1);
1129  void WatchLowerBound(IntegerVariable var, int id, int watch_index = -1);
1130  void WatchUpperBound(IntegerVariable var, int id, int watch_index = -1);
1131  void WatchIntegerVariable(IntegerVariable i, int id, int watch_index = -1);
1132 
1133  // Because the coeff is always positive, whatching an affine expression is
1134  // the same as watching its var.
1136  WatchLowerBound(e.var, id);
1137  }
1139  WatchUpperBound(e.var, id);
1140  }
1142  WatchIntegerVariable(e.var, id);
1143  }
1144 
1145  // No-op overload for "constant" IntegerVariable that are sometimes templated
1146  // as an IntegerValue.
1147  void WatchLowerBound(IntegerValue i, int id) {}
1148  void WatchUpperBound(IntegerValue i, int id) {}
1149  void WatchIntegerVariable(IntegerValue v, int id) {}
1150 
1151  // Registers a reversible class with a given propagator. This class will be
1152  // changed to the correct state just before the propagator is called.
1153  //
1154  // Doing it just before should minimize cache-misses and bundle as much as
1155  // possible the "backtracking" together. Many propagators only watches a
1156  // few variables and will not be called at each decision levels.
1157  void RegisterReversibleClass(int id, ReversibleInterface* rev);
1158 
1159  // Registers a reversible int with a given propagator. The int will be changed
1160  // to its correct value just before Propagate() is called.
1161  //
1162  // Note that this will work in O(num_rev_int_of_propagator_id) per call to
1163  // Propagate() and happens at most once per decision level. As such this is
1164  // meant for classes that have just a few reversible ints or that will have a
1165  // similar complexity anyway.
1166  //
1167  // Alternatively, one can directly get the underlying RevRepository<int> with
1168  // a call to model.Get<>(), and use SaveWithStamp() before each modification
1169  // to have just a slight overhead per int updates. This later option is what
1170  // is usually done in a CP solver at the cost of a sligthly more complex API.
1171  void RegisterReversibleInt(int id, int* rev);
1172 
1173  // Returns the number of registered propagators.
1174  int NumPropagators() const { return in_queue_.size(); }
1175 
1176  // Set a callback for new variable bounds at level 0.
1177  //
1178  // This will be called (only at level zero) with the list of IntegerVariable
1179  // with changed lower bounds. Note that it might be called more than once
1180  // during the same propagation cycle if we fix variables in "stages".
1181  //
1182  // Also note that this will be called if some BooleanVariable where fixed even
1183  // if no IntegerVariable are changed, so the passed vector to the function
1184  // might be empty.
1186  const std::function<void(const std::vector<IntegerVariable>&)> cb) {
1187  level_zero_modified_variable_callback_.push_back(cb);
1188  }
1189 
1190  // Returns the id of the propagator we are currently calling. This is meant
1191  // to be used from inside Propagate() in case a propagator was registered
1192  // more than once at different priority for instance.
1193  int GetCurrentId() const { return current_id_; }
1194 
1195  private:
1196  // Updates queue_ and in_queue_ with the propagator ids that need to be
1197  // called.
1198  void UpdateCallingNeeds(Trail* trail);
1199 
1200  TimeLimit* time_limit_;
1201  IntegerTrail* integer_trail_;
1202  RevIntRepository* rev_int_repository_;
1203 
1204  struct WatchData {
1205  int id;
1206  int watch_index;
1207  bool operator==(const WatchData& o) const {
1208  return id == o.id && watch_index == o.watch_index;
1209  }
1210  };
1213  std::vector<PropagatorInterface*> watchers_;
1214  SparseBitset<IntegerVariable> modified_vars_;
1215 
1216  // Propagator ids that needs to be called. There is one queue per priority but
1217  // just one Boolean to indicate if a propagator is in one of them.
1218  std::vector<std::deque<int>> queue_by_priority_;
1219  std::vector<bool> in_queue_;
1220 
1221  // Data for each propagator.
1222  DEFINE_INT_TYPE(IdType, int32);
1223  std::vector<int> id_to_level_at_last_call_;
1224  RevVector<IdType, int> id_to_greatest_common_level_since_last_call_;
1225  std::vector<std::vector<ReversibleInterface*>> id_to_reversible_classes_;
1226  std::vector<std::vector<int*>> id_to_reversible_ints_;
1227  std::vector<std::vector<int>> id_to_watch_indices_;
1228  std::vector<int> id_to_priority_;
1229  std::vector<int> id_to_idempotence_;
1230 
1231  // Special propagators that needs to always be called at level zero.
1232  std::vector<int> propagator_ids_to_call_at_level_zero_;
1233 
1234  // The id of the propagator we just called.
1235  int current_id_;
1236 
1237  std::vector<std::function<void(const std::vector<IntegerVariable>&)>>
1238  level_zero_modified_variable_callback_;
1239 
1240  DISALLOW_COPY_AND_ASSIGN(GenericLiteralWatcher);
1241 };
1242 
1243 // ============================================================================
1244 // Implementation.
1245 // ============================================================================
1246 
1248  IntegerValue bound) {
1249  return IntegerLiteral(
1251 }
1252 
1254  IntegerValue bound) {
1255  return IntegerLiteral(
1257 }
1258 
1260  // Note that bound >= kMinIntegerValue, so -bound + 1 will have the correct
1261  // capped value.
1262  return IntegerLiteral(
1263  NegationOf(IntegerVariable(var)),
1265 }
1266 
1267 // var * coeff + constant >= bound.
1269  IntegerValue bound) const {
1271  DCHECK_GT(coeff, 0);
1274 }
1275 
1276 // var * coeff + constant <= bound.
1279  DCHECK_GT(coeff, 0);
1281 }
1282 
1283 inline IntegerValue IntegerTrail::LowerBound(IntegerVariable i) const {
1284  return vars_[i].current_bound;
1285 }
1286 
1287 inline IntegerValue IntegerTrail::UpperBound(IntegerVariable i) const {
1288  return -vars_[NegationOf(i)].current_bound;
1289 }
1290 
1291 inline bool IntegerTrail::IsFixed(IntegerVariable i) const {
1292  return vars_[i].current_bound == -vars_[NegationOf(i)].current_bound;
1293 }
1294 
1295 // TODO(user): Use capped arithmetic? It might be slow though and we better just
1296 // make sure there is no overflow at model creation.
1297 inline IntegerValue IntegerTrail::LowerBound(AffineExpression expr) const {
1298  if (expr.var == kNoIntegerVariable) return expr.constant;
1299  return LowerBound(expr.var) * expr.coeff + expr.constant;
1300 }
1301 
1302 // TODO(user): Use capped arithmetic? same remark as for LowerBound().
1303 inline IntegerValue IntegerTrail::UpperBound(AffineExpression expr) const {
1304  if (expr.var == kNoIntegerVariable) return expr.constant;
1305  return UpperBound(expr.var) * expr.coeff + expr.constant;
1306 }
1307 
1308 inline bool IntegerTrail::IsFixed(AffineExpression expr) const {
1309  if (expr.var == kNoIntegerVariable) return true;
1310  return IsFixed(expr.var);
1311 }
1312 
1314  IntegerVariable i) const {
1316 }
1317 
1319  IntegerVariable i) const {
1321 }
1322 
1324  return l.bound <= LowerBound(l.var);
1325 }
1326 
1328  return l.bound > UpperBound(l.var);
1329 }
1330 
1331 // The level zero bounds are stored at the beginning of the trail and they also
1332 // serves as sentinels. Their index match the variables index.
1334  IntegerVariable var) const {
1335  return integer_trail_[var.value()].bound;
1336 }
1337 
1339  IntegerVariable var) const {
1340  return -integer_trail_[NegationOf(var).value()].bound;
1341 }
1342 
1343 inline bool IntegerTrail::IsFixedAtLevelZero(IntegerVariable var) const {
1344  return integer_trail_[var.value()].bound ==
1345  -integer_trail_[NegationOf(var).value()].bound;
1346 }
1347 
1349  int watch_index) {
1350  if (l.Index() >= literal_to_watcher_.size()) {
1351  literal_to_watcher_.resize(l.Index().value() + 1);
1352  }
1353  literal_to_watcher_[l.Index()].push_back({id, watch_index});
1354 }
1355 
1356 inline void GenericLiteralWatcher::WatchLowerBound(IntegerVariable var, int id,
1357  int watch_index) {
1358  if (var == kNoIntegerVariable) return;
1359  if (var.value() >= var_to_watcher_.size()) {
1360  var_to_watcher_.resize(var.value() + 1);
1361  }
1362 
1363  // Minor optim, so that we don't watch the same variable twice. Propagator
1364  // code is easier this way since for example when one wants to watch both
1365  // an interval start and interval end, both might have the same underlying
1366  // variable.
1367  const WatchData data = {id, watch_index};
1368  if (!var_to_watcher_[var].empty() && var_to_watcher_[var].back() == data) {
1369  return;
1370  }
1371  var_to_watcher_[var].push_back(data);
1372 }
1373 
1374 inline void GenericLiteralWatcher::WatchUpperBound(IntegerVariable var, int id,
1375  int watch_index) {
1376  if (var == kNoIntegerVariable) return;
1377  WatchLowerBound(NegationOf(var), id, watch_index);
1378 }
1379 
1380 inline void GenericLiteralWatcher::WatchIntegerVariable(IntegerVariable i,
1381  int id,
1382  int watch_index) {
1383  WatchLowerBound(i, id, watch_index);
1384  WatchUpperBound(i, id, watch_index);
1385 }
1386 
1387 // ============================================================================
1388 // Model based functions.
1389 //
1390 // Note that in the model API, we simply use int64 for the integer values, so
1391 // that it is nicer for the client. Internally these are converted to
1392 // IntegerValue which is typechecked.
1393 // ============================================================================
1394 
1395 inline std::function<BooleanVariable(Model*)> NewBooleanVariable() {
1396  return [=](Model* model) {
1397  return model->GetOrCreate<SatSolver>()->NewBooleanVariable();
1398  };
1399 }
1400 
1401 inline std::function<IntegerVariable(Model*)> ConstantIntegerVariable(
1402  int64 value) {
1403  return [=](Model* model) {
1404  return model->GetOrCreate<IntegerTrail>()
1405  ->GetOrCreateConstantIntegerVariable(IntegerValue(value));
1406  };
1407 }
1408 
1409 inline std::function<IntegerVariable(Model*)> NewIntegerVariable(int64 lb,
1410  int64 ub) {
1411  return [=](Model* model) {
1412  CHECK_LE(lb, ub);
1413  return model->GetOrCreate<IntegerTrail>()->AddIntegerVariable(
1414  IntegerValue(lb), IntegerValue(ub));
1415  };
1416 }
1417 
1418 inline std::function<IntegerVariable(Model*)> NewIntegerVariable(
1419  const Domain& domain) {
1420  return [=](Model* model) {
1421  return model->GetOrCreate<IntegerTrail>()->AddIntegerVariable(domain);
1422  };
1423 }
1424 
1425 // Creates a 0-1 integer variable "view" of the given literal. It will have a
1426 // value of 1 when the literal is true, and 0 when the literal is false.
1427 inline std::function<IntegerVariable(Model*)> NewIntegerVariableFromLiteral(
1428  Literal lit) {
1429  return [=](Model* model) {
1430  auto* encoder = model->GetOrCreate<IntegerEncoder>();
1431  const IntegerVariable candidate = encoder->GetLiteralView(lit);
1432  if (candidate != kNoIntegerVariable) return candidate;
1433 
1434  IntegerVariable var;
1435  const auto& assignment = model->GetOrCreate<SatSolver>()->Assignment();
1436  if (assignment.LiteralIsTrue(lit)) {
1437  var = model->Add(ConstantIntegerVariable(1));
1438  } else if (assignment.LiteralIsFalse(lit)) {
1439  var = model->Add(ConstantIntegerVariable(0));
1440  } else {
1441  var = model->Add(NewIntegerVariable(0, 1));
1442  }
1443 
1444  encoder->AssociateToIntegerEqualValue(lit, var, IntegerValue(1));
1445  DCHECK_NE(encoder->GetLiteralView(lit), kNoIntegerVariable);
1446  return var;
1447  };
1448 }
1449 
1450 inline std::function<int64(const Model&)> LowerBound(IntegerVariable v) {
1451  return [=](const Model& model) {
1452  return model.Get<IntegerTrail>()->LowerBound(v).value();
1453  };
1454 }
1455 
1456 inline std::function<int64(const Model&)> UpperBound(IntegerVariable v) {
1457  return [=](const Model& model) {
1458  return model.Get<IntegerTrail>()->UpperBound(v).value();
1459  };
1460 }
1461 
1462 inline std::function<bool(const Model&)> IsFixed(IntegerVariable v) {
1463  return [=](const Model& model) {
1464  const IntegerTrail* trail = model.Get<IntegerTrail>();
1465  return trail->LowerBound(v) == trail->UpperBound(v);
1466  };
1467 }
1468 
1469 // This checks that the variable is fixed.
1470 inline std::function<int64(const Model&)> Value(IntegerVariable v) {
1471  return [=](const Model& model) {
1472  const IntegerTrail* trail = model.Get<IntegerTrail>();
1473  CHECK_EQ(trail->LowerBound(v), trail->UpperBound(v)) << v;
1474  return trail->LowerBound(v).value();
1475  };
1476 }
1477 
1478 inline std::function<void(Model*)> GreaterOrEqual(IntegerVariable v, int64 lb) {
1479  return [=](Model* model) {
1480  if (!model->GetOrCreate<IntegerTrail>()->Enqueue(
1481  IntegerLiteral::GreaterOrEqual(v, IntegerValue(lb)),
1482  std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1483  model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1484  VLOG(1) << "Model trivially infeasible, variable " << v
1485  << " has upper bound " << model->Get(UpperBound(v))
1486  << " and GreaterOrEqual() was called with a lower bound of "
1487  << lb;
1488  }
1489  };
1490 }
1491 
1492 inline std::function<void(Model*)> LowerOrEqual(IntegerVariable v, int64 ub) {
1493  return [=](Model* model) {
1494  if (!model->GetOrCreate<IntegerTrail>()->Enqueue(
1495  IntegerLiteral::LowerOrEqual(v, IntegerValue(ub)),
1496  std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1497  model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
1498  LOG(WARNING) << "Model trivially infeasible, variable " << v
1499  << " has lower bound " << model->Get(LowerBound(v))
1500  << " and LowerOrEqual() was called with an upper bound of "
1501  << ub;
1502  }
1503  };
1504 }
1505 
1506 // Fix v to a given value.
1507 inline std::function<void(Model*)> Equality(IntegerVariable v, int64 value) {
1508  return [=](Model* model) {
1509  model->Add(LowerOrEqual(v, value));
1510  model->Add(GreaterOrEqual(v, value));
1511  };
1512 }
1513 
1514 // TODO(user): This is one of the rare case where it is better to use Equality()
1515 // rather than two Implications(). Maybe we should modify our internal
1516 // implementation to use half-reified encoding? that is do not propagate the
1517 // direction integer-bound => literal, but just literal => integer-bound? This
1518 // is the same as using different underlying variable for an integer literal and
1519 // its negation.
1520 inline std::function<void(Model*)> Implication(
1521  const std::vector<Literal>& enforcement_literals, IntegerLiteral i) {
1522  return [=](Model* model) {
1523  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
1524  if (i.bound <= integer_trail->LowerBound(i.var)) {
1525  // Always true! nothing to do.
1526  } else if (i.bound > integer_trail->UpperBound(i.var)) {
1527  // Always false.
1528  std::vector<Literal> clause;
1529  for (const Literal literal : enforcement_literals) {
1530  clause.push_back(literal.Negated());
1531  }
1532  model->Add(ClauseConstraint(clause));
1533  } else {
1534  // TODO(user): Double check what happen when we associate a trivially
1535  // true or false literal.
1536  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1537  std::vector<Literal> clause{encoder->GetOrCreateAssociatedLiteral(i)};
1538  for (const Literal literal : enforcement_literals) {
1539  clause.push_back(literal.Negated());
1540  }
1541  model->Add(ClauseConstraint(clause));
1542  }
1543  };
1544 }
1545 
1546 // in_interval => v in [lb, ub].
1547 inline std::function<void(Model*)> ImpliesInInterval(Literal in_interval,
1548  IntegerVariable v,
1549  int64 lb, int64 ub) {
1550  return [=](Model* model) {
1551  if (lb == ub) {
1552  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1553  model->Add(Implication({in_interval},
1555  v, IntegerValue(lb))));
1556  return;
1557  }
1558  model->Add(Implication(
1559  {in_interval}, IntegerLiteral::GreaterOrEqual(v, IntegerValue(lb))));
1560  model->Add(Implication({in_interval},
1561  IntegerLiteral::LowerOrEqual(v, IntegerValue(ub))));
1562  };
1563 }
1564 
1565 // Calling model.Add(FullyEncodeVariable(var)) will create one literal per value
1566 // in the domain of var (if not already done), and wire everything correctly.
1567 // This also returns the full encoding, see the FullDomainEncoding() method of
1568 // the IntegerEncoder class.
1569 inline std::function<std::vector<IntegerEncoder::ValueLiteralPair>(Model*)>
1570 FullyEncodeVariable(IntegerVariable var) {
1571  return [=](Model* model) {
1572  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
1573  if (!encoder->VariableIsFullyEncoded(var)) {
1574  encoder->FullyEncodeVariable(var);
1575  }
1576  return encoder->FullDomainEncoding(var);
1577  };
1578 }
1579 
1580 // Same as ExcludeCurrentSolutionAndBacktrack() but this version works for an
1581 // integer problem with optional variables. The issue is that an optional
1582 // variable that is ignored can basically take any value, and we don't really
1583 // want to enumerate them. This function should exclude all solutions where
1584 // only the ignored variable values change.
1585 std::function<void(Model*)>
1587 
1588 } // namespace sat
1589 } // namespace operations_research
1590 
1591 #endif // OR_TOOLS_SAT_INTEGER_H_
operations_research::sat::IntegerTrail::IntegerTrail
IntegerTrail(Model *model)
Definition: integer.h:535
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::IntegerTrail::timestamp
int64 timestamp() const
Definition: integer.h:778
operations_research::sat::LowerBound
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1450
operations_research::sat::IntegerEncoder::ValueLiteralPair::literal
Literal literal
Definition: integer.h:325
operations_research::sat::RevIntegerValueRepository::RevIntegerValueRepository
RevIntegerValueRepository(Model *model)
Definition: integer.h:1082
operations_research::sat::IntegerEncoder::GetOrCreateAssociatedLiteral
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
Definition: integer.cc:202
operations_research::sat::IntegerLiteral::DebugString
std::string DebugString() const
Definition: integer.h:182
operations_research::sat::IntegerLiteral::Negated
IntegerLiteral Negated() const
Definition: integer.h:1259
operations_research::sat::AffineExpression::constant
IntegerValue constant
Definition: integer.h:242
operations_research::sat::GenericLiteralWatcher::Register
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1910
operations_research::sat::IntegerLiteral::IntegerLiteral
IntegerLiteral()
Definition: integer.h:164
operations_research::sat::IntegerEncoder::PartialDomainEncoding
std::vector< ValueLiteralPair > PartialDomainEncoding(IntegerVariable var) const
Definition: integer.cc:112
operations_research::sat::IntegerTrail::AppendNewBounds
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
Definition: integer.cc:1699
integral_types.h
operations_research::sat::AffineExpression
Definition: integer.h:205
map_util.h
operations_research::sat::IntegerTrail::~IntegerTrail
~IntegerTrail() final
Definition: integer.cc:473
operations_research::sat::IntegerTrail
Definition: integer.h:533
VLOG
#define VLOG(verboselevel)
Definition: base/logging.h:978
absl::StrongVector::push_back
void push_back(const value_type &x)
Definition: strong_vector.h:158
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
operations_research::sat::FloorRatio
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
operations_research::sat::VariableIsPositive
bool VariableIsPositive(IntegerVariable i)
Definition: integer.h:130
max
int64 max
Definition: alldiff_cst.cc:139
operations_research::sat::GenericLiteralWatcher::WatchLowerBound
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1356
operations_research::SparseBitset::ClearAndResize
void ClearAndResize(IntegerType size)
Definition: bitset.h:780
operations_research::operator==
LinearRange operator==(const LinearExpr &lhs, const LinearExpr &rhs)
Definition: linear_expr.cc:180
bound
int64 bound
Definition: routing_search.cc:971
operations_research::sat::IntegerEncoder::GetIntegerLiterals
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
Definition: integer.h:390
LOG
#define LOG(severity)
Definition: base/logging.h:420
operations_research::CapProd
int64 CapProd(int64 x, int64 y)
Definition: saturated_arithmetic.h:231
absl::StrongVector::size
size_type size() const
Definition: strong_vector.h:147
operations_research::sat::kNoLiteralIndex
const LiteralIndex kNoLiteralIndex(-1)
operations_research::sat::CeilRatio
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
operations_research::sat::ConstantIntegerVariable
std::function< IntegerVariable(Model *)> ConstantIntegerVariable(int64 value)
Definition: integer.h:1401
operations_research::sat::GetPositiveOnlyIndex
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
Definition: integer.h:140
operations_research::sat::DebugSolution::DebugSolution
DebugSolution(Model *model)
Definition: integer.h:255
FATAL
const int FATAL
Definition: log_severity.h:32
operations_research::sat::GenericLiteralWatcher::RegisterReversibleClass
void RegisterReversibleClass(int id, ReversibleInterface *rev)
Definition: integer.cc:1949
operations_research::sat::RevIntRepository
Definition: integer.h:1074
operations_research::sat::IntegerLiteral::operator==
bool operator==(IntegerLiteral o) const
Definition: integer.h:175
operations_research::sat::IntegerTrail::LevelZeroUpperBound
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition: integer.h:1338
operations_research::sat::IntegerTrail::LevelZeroLowerBound
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1333
operations_research::sat::IntegerEncoder::GetAllIntegerLiterals
const InlinedIntegerLiteralVector & GetAllIntegerLiterals(Literal lit) const
Definition: integer.h:400
operations_research::sat::IntegerTrail::VariableLowerBoundIsFromLevelZero
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const
Definition: integer.h:810
logging.h
operations_research::sat::PropagatorInterface
Definition: integer.h:1043
operations_research::sat::SatSolver
Definition: sat_solver.h:58
operations_research::sat::IntegerLiteral::IntegerLiteral
IntegerLiteral(IntegerVariable v, IntegerValue b)
Definition: integer.h:165
operations_research::sat::IntegerEncoder::ClearNewlyFixedIntegerLiterals
void ClearNewlyFixedIntegerLiterals()
Definition: integer.h:412
operations_research::sat::PropagatorInterface::IncrementalPropagate
virtual bool IncrementalPropagate(const std::vector< int > &watch_indices)
Definition: integer.h:1066
operations_research::sat::IntegerEncoder::ValueLiteralPair::operator==
bool operator==(const ValueLiteralPair &o) const
Definition: integer.h:320
operations_research::sat::IntegerEncoder::GetLiteralView
const IntegerVariable GetLiteralView(Literal lit) const
Definition: integer.h:420
operations_research::sat::GenericLiteralWatcher::RegisterReversibleInt
void RegisterReversibleInt(int id, int *rev)
Definition: integer.cc:1954
DCHECK_GT
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
operations_research::sat::AffineExpression::coeff
IntegerValue coeff
Definition: integer.h:241
value
int64 value
Definition: demon_profiler.cc:43
operations_research::sat::IntegerTrail::Propagate
bool Propagate(Trail *trail) final
Definition: integer.cc:480
operations_research::RevRepository
Definition: rev.h:47
model.h
operations_research::sat::IntegerEncoder::~IntegerEncoder
~IntegerEncoder()
Definition: integer.h:283
macros.h
operations_research::sat::GenericLiteralWatcher::WatchLowerBound
void WatchLowerBound(IntegerValue i, int id)
Definition: integer.h:1147
saturated_arithmetic.h
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::IntegerTrail::EnqueueLiteral
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1058
operations_research::sat::operator<<
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
Definition: cp_model.cc:65
operations_research::sat::NegationOf
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
operations_research::sat::VariablesAssignment::LiteralIsTrue
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
operations_research::sat::IntegerTrail::InPropagationLoop
bool InPropagationLoop() const
Definition: integer.cc:1118
operations_research::sat::IntegerTrail::OptionalLiteralIndex
LiteralIndex OptionalLiteralIndex(IntegerVariable i) const
Definition: integer.h:627
WARNING
const int WARNING
Definition: log_severity.h:31
operations_research::sat::AffineExpression::AffineExpression
AffineExpression(IntegerValue cst)
Definition: integer.h:208
kint64min
static const int64 kint64min
Definition: integral_types.h:60
operations_research::sat::IntegerLiteral::GreaterOrEqual
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1247
operations_research::sat::IntegerTrail::FirstUnassignedVariable
IntegerVariable FirstUnassignedVariable() const
Definition: integer.cc:1161
operations_research::sat::IntegerTrail::IntegerLiteralIsFalse
bool IntegerLiteralIsFalse(IntegerLiteral l) const
Definition: integer.h:1327
operations_research::sat::AffineExpression::LpValue
double LpValue(const absl::StrongVector< IntegerVariable, double > &lp_values) const
Definition: integer.h:233
operations_research::Domain
We call domain any subset of Int64 = [kint64min, kint64max].
Definition: sorted_interval_list.h:81
operations_research::sat::PositiveVariable
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
int64
int64_t int64
Definition: integral_types.h:34
operations_research::sat::Literal::Negated
Literal Negated() const
Definition: sat_base.h:91
operations_research::sat::PropagatorInterface::PropagatorInterface
PropagatorInterface()
Definition: integer.h:1045
operations_research::sat::Literal::NegatedIndex
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
sat_solver.h
operations_research::sat::AffineExpression::operator==
bool operator==(AffineExpression o) const
Definition: integer.h:228
operations_research::TimeLimit
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
operations_research::sat::IntegerTrail::Reason
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: integer.cc:1679
index
int index
Definition: pack.cc:508
sat_base.h
int32
int int32
Definition: integral_types.h:33
operations_research::sat::IntegerTrail::UpdateInitialDomain
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
operations_research::sat::DEFINE_INT_TYPE
DEFINE_INT_TYPE(ClauseIndex, int)
operations_research::sat::IntegerEncoder::DisableImplicationBetweenLiteral
void DisableImplicationBetweenLiteral()
Definition: integer.h:386
operations_research::sat::GenericLiteralWatcher::GenericLiteralWatcher
GenericLiteralWatcher(Model *model)
Definition: integer.cc:1714
operations_research::sat::IntegerTrail::MarkIntegerVariableAsOptional
void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered)
Definition: integer.h:632
operations_research::sat::IntegerEncoder::AddAllImplicationsBetweenAssociatedLiterals
void AddAllImplicationsBetweenAssociatedLiterals()
Definition: integer.cc:168
operations_research::sat::IntegerEncoder::ValueLiteralPair::ValueLiteralPair
ValueLiteralPair()
Definition: integer.h:317
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::IntegerTrail::NumIntegerVariables
IntegerVariable NumIntegerVariables() const
Definition: integer.h:558
operations_research::sat::IntegerEncoder::AssociateToIntegerLiteral
void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit)
Definition: integer.cc:282
DCHECK_NE
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
operations_research::sat::IntegerLiteral::var
IntegerVariable var
Definition: integer.h:189
operations_research::sat::SatSolver::CurrentDecisionLevel
int CurrentDecisionLevel() const
Definition: sat_solver.h:361
operations_research::sat::PositiveRemainder
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:102
operations_research::glop::kInfinity
const double kInfinity
Definition: lp_types.h:83
operations_research::sat::GenericLiteralWatcher::NumPropagators
int NumPropagators() const
Definition: integer.h:1174
a
int64 a
Definition: constraint_solver/table.cc:42
operations_research::sat::IntegerTrail::UpperBoundAsLiteral
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1318
operations_research::sat::SatSolver::AddUnitClause
bool AddUnitClause(Literal true_literal)
Definition: sat_solver.cc:164
operations_research::sat::IntegerTrail::AppendRelaxedLinearReason
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:807
operations_research::sat::NewBooleanVariable
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1395
operations_research::sat::AffineExpression::AffineExpression
AffineExpression()
Definition: integer.h:207
operations_research::SparseBitset< IntegerVariable >
operations_research::sat::NewIntegerVariable
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1409
operations_research::sat::GenericLiteralWatcher::~GenericLiteralWatcher
~GenericLiteralWatcher() final
Definition: integer.h:1094
operations_research::sat::IntTypeAbs
IntType IntTypeAbs(IntType t)
Definition: integer.h:77
operations_research::Assignment
An Assignment is a variable -> domains mapping, used to report solutions to the user.
Definition: constraint_solver.h:5033
operations_research::sat::IntegerEncoder::FullDomainEncoding
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
Definition: integer.cc:106
operations_research::sat::GenericLiteralWatcher::WatchAffineExpression
void WatchAffineExpression(AffineExpression e, int id)
Definition: integer.h:1141
operations_research::sat::GenericLiteralWatcher::SetPropagatorPriority
void SetPropagatorPriority(int id, int priority)
Definition: integer.cc:1933
operations_research::sat::IntegerTrail::RegisterWatcher
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
Definition: integer.h:786
operations_research::sat::IntegerTrail::UpperBound
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1287
operations_research::sat::IntegerTrail::Enqueue
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
operations_research::sat::IntegerEncoder::GetOrCreateLiteralAssociatedToEquality
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
Definition: integer.cc:248
operations_research::sat::AffineExpression::AffineExpression
AffineExpression(IntegerVariable v)
Definition: integer.h:210
operations_research::CapAdd
int64 CapAdd(int64 x, int64 y)
Definition: saturated_arithmetic.h:124
operations_research::sat::IntegerLiteral::operator!=
bool operator!=(IntegerLiteral o) const
Definition: integer.h:178
int_type.h
operations_research::sat::PropagatorInterface::~PropagatorInterface
virtual ~PropagatorInterface()
Definition: integer.h:1046
operations_research::sat::IntegerTrail::IntegerLiteralIsTrue
bool IntegerLiteralIsTrue(IntegerLiteral l) const
Definition: integer.h:1323
operations_research::sat::GenericLiteralWatcher::NotifyThatPropagatorMayNotReachFixedPointInOnePass
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
Definition: integer.cc:1940
operations_research::sat::IntegerTrail::InitialVariableDomain
const Domain & InitialVariableDomain(IntegerVariable var) const
Definition: integer.cc:644
operations_research::sat::kMaxIntegerValue
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
operations_research::sat::IntegerEncoder::Canonicalize
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
Definition: integer.cc:184
operations_research::sat::Trail::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
operations_research::sat::IntegerTrail::IsIgnoredLiteral
Literal IsIgnoredLiteral(IntegerVariable i) const
Definition: integer.h:623
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::NewIntegerVariableFromLiteral
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
Definition: integer.h:1427
operations_research::sat::IntegerDomains::IntegerDomains
IntegerDomains(Model *model)
Definition: integer.h:247
operations_research::sat::GenericLiteralWatcher::WatchLowerBound
void WatchLowerBound(AffineExpression e, int id)
Definition: integer.h:1135
operations_research::sat::IntegerEncoder::AssociateToIntegerEqualValue
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
Definition: integer.cc:308
operations_research::sat::IntegerEncoder::PartialGreaterThanEncoding
std::map< IntegerValue, Literal > PartialGreaterThanEncoding(IntegerVariable var) const
Definition: integer.h:452
operations_research::sat::Literal::Index
LiteralIndex Index() const
Definition: sat_base.h:84
operations_research::sat::IntegerTrail::RegisterReversibleClass
void RegisterReversibleClass(ReversibleInterface *rev)
Definition: integer.h:816
operations_research::sat::IntegerEncoder::IntegerEncoder
IntegerEncoder(Model *model)
Definition: integer.h:278
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::IntegerEncoder::GetAssociatedEqualityLiteral
LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const
Definition: integer.cc:238
operations_research::sat::IntegerLiteral::bound
IntegerValue bound
Definition: integer.h:190
operations_research::sat::IntegerTrail::ReserveSpaceForNumVariables
void ReserveSpaceForNumVariables(int num_vars)
Definition: integer.cc:592
operations_research::sat::IntegerTrail::ReasonFor
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
Definition: integer.cc:1533
operations_research::sat::IntegerEncoder::SearchForLiteralAtOrBefore
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i, IntegerValue *bound) const
Definition: integer.cc:460
operations_research::sat::IntegerTrail::LowerBoundAsLiteral
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1313
operations_research::sat::AddProductTo
bool AddProductTo(IntegerValue a, IntegerValue b, IntegerValue *result)
Definition: integer.h:110
operations_research::sat::AffineExpression::GreaterOrEqual
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
Definition: integer.h:1268
operations_research::sat::IntegerLiteral
Definition: integer.h:153
operations_research::sat::LowerOrEqual
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1492
operations_research::sat::Value
std::function< int64(const Model &)> Value(IntegerVariable v)
Definition: integer.h:1470
operations_research::sat::IntegerEncoder::ValueLiteralPair::ValueLiteralPair
ValueLiteralPair(IntegerValue v, Literal l)
Definition: integer.h:318
operations_research::sat::IntegerTrail::HasPendingRootLevelDeduction
bool HasPendingRootLevelDeduction() const
Definition: integer.h:847
operations_research::sat::GenericLiteralWatcher::WatchIntegerVariable
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
Definition: integer.h:1380
DCHECK
#define DCHECK(condition)
Definition: base/logging.h:884
operations_research::sat::AffineExpression::LowerOrEqual
IntegerLiteral LowerOrEqual(IntegerValue bound) const
Definition: integer.h:1277
operations_research::sat::IsFixed
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1462
operations_research::sat::IntegerLiteral::LowerOrEqual
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1253
CHECK_LE
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
rev.h
operations_research::sat::ImpliesInInterval
std::function< void(Model *)> ImpliesInInterval(Literal in_interval, IntegerVariable v, int64 lb, int64 ub)
Definition: integer.h:1547
operations_research::sat::ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
Definition: integer.cc:1960
sorted_interval_list.h
operations_research::sat::IntegerTrail::num_level_zero_enqueues
int64 num_level_zero_enqueues() const
Definition: integer.h:781
operations_research::sat::Trail::MutableConflict
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
operations_research::sat::IntegerTrail::Index
int Index() const
Definition: integer.h:820
operations_research::sat::ClauseConstraint
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:905
DCHECK_GE
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::sat::IntegerTrail::NumConstantVariables
int NumConstantVariables() const
Definition: integer.cc:710
operations_research::sat::RevIntegerValueRepository
Definition: integer.h:1080
operations_research::sat::IntegerTrail::RemoveLevelZeroBounds
void RemoveLevelZeroBounds(std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:919
operations_research::sat::ToDouble
double ToDouble(IntegerValue value)
Definition: integer.h:69
operations_research::sat::GenericLiteralWatcher::WatchIntegerVariable
void WatchIntegerVariable(IntegerValue v, int id)
Definition: integer.h:1149
absl::StrongVector< IntegerVariable, double >
operations_research::sat::IntegerTrail::NextVariableToBranchOnInPropagationLoop
IntegerVariable NextVariableToBranchOnInPropagationLoop() const
Definition: integer.cc:1128
operations_research::sat::IntegerEncoder::GetTrueLiteral
Literal GetTrueLiteral()
Definition: integer.h:437
operations_research::sat::GenericLiteralWatcher::WatchLiteral
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1348
operations_research::sat::IntegerEncoder::ValueLiteralPair
Definition: integer.h:316
operations_research::sat::IntegerTrail::ReportConflict
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.h:793
operations_research::ReversibleInterface
Definition: rev.h:29
operations_research::sat::kMinIntegerValue
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
iterators.h
operations_research::sat::GreaterOrEqual
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
Definition: integer.h:1478
operations_research::sat::IntegerTrail::Untrail
void Untrail(const Trail &trail, int literal_trail_index) final
Definition: integer.cc:543
operations_research::sat::AffineExpression::AffineExpression
AffineExpression(IntegerVariable v, IntegerValue c, IntegerValue cst)
Definition: integer.h:214
operations_research::sat::IntegerTrail::RelaxLinearReason
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:785
operations_research::sat::IntegerEncoder::LiteralIsAssociated
bool LiteralIsAssociated(IntegerLiteral i_lit) const
Definition: integer.cc:446
operations_research::sat::DebugSolution
Definition: integer.h:254
operations_research::sat::IntegerEncoder::ValueLiteralPair::value
IntegerValue value
Definition: integer.h:324
operations_research::sat::UpperBound
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1456
DCHECK_EQ
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
operations_research::sat::AffineExpression::AffineExpression
AffineExpression(IntegerVariable v, IntegerValue c)
Definition: integer.h:212
hash.h
operations_research::sat::GenericLiteralWatcher::Untrail
void Untrail(const Trail &trail, int literal_trail_index) final
Definition: integer.cc:1886
operations_research::sat::IntegerTrail::ReportConflict
bool ReportConflict(absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.h:801
operations_research::sat::IntegerTrail::FindTrailIndexOfVarBefore
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
Definition: integer.cc:716
operations_research::sat::IntegerTrail::GetOrCreateConstantIntegerVariable
IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value)
Definition: integer.cc:695
operations_research::sat::IntegerTrail::IsFixed
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1291
b
int64 b
Definition: constraint_solver/table.cc:43
absl::StrongVector::resize
void resize(size_type new_size)
Definition: strong_vector.h:150
operations_research::sat::GenericLiteralWatcher::AlwaysCallAtLevelZero
void AlwaysCallAtLevelZero(int id)
Definition: integer.cc:1945
operations_research::sat::IntegerDomains
Definition: integer.h:246
operations_research::sat::IntegerTrail::MergeReasonInto
void MergeReasonInto(absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
Definition: integer.cc:1541
strong_vector.h
operations_research::sat::Implication
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
Definition: integer.h:1520
operations_research::sat::Equality
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
Definition: integer.h:1507
operations_research::sat::AffineExpression::var
IntegerVariable var
Definition: integer.h:240
operations_research::sat::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::sat::IntegerEncoder::GetAssociatedLiteral
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
Definition: integer.cc:452
operations_research::sat::IntegerTrail::LazyReasonFunction
std::function< void(IntegerLiteral literal_to_explain, int trail_index_of_literal, std::vector< Literal > *literals, std::vector< int > *dependencies)> LazyReasonFunction
Definition: integer.h:752
operations_research::sat::GenericLiteralWatcher::WatchUpperBound
void WatchUpperBound(IntegerValue i, int id)
Definition: integer.h:1148
absl
Definition: cleanup.h:22
operations_research::sat::IntegerTrail::num_enqueues
int64 num_enqueues() const
Definition: integer.h:777
operations_research::sat::IntegerTrail::IsCurrentlyIgnored
bool IsCurrentlyIgnored(IntegerVariable i) const
Definition: integer.h:618
operations_research::sat::IntegerTrail::IsFixedAtLevelZero
bool IsFixedAtLevelZero(IntegerVariable var) const
Definition: integer.h:1343
literal
Literal literal
Definition: optimization.cc:84
operations_research::sat::GenericLiteralWatcher::Propagate
bool Propagate(Trail *trail) final
Definition: integer.cc:1772
DCHECK_LE
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
operations_research::sat::IntegerEncoder::GetFalseLiteral
Literal GetFalseLiteral()
Definition: integer.h:447
operations_research::sat::GenericLiteralWatcher::RegisterLevelZeroModifiedVariablesCallback
void RegisterLevelZeroModifiedVariablesCallback(const std::function< void(const std::vector< IntegerVariable > &)> cb)
Definition: integer.h:1185
operations_research::sat::IntegerEncoder::NewlyFixedIntegerLiterals
const std::vector< IntegerLiteral > NewlyFixedIntegerLiterals() const
Definition: integer.h:409
operations_research::sat::RevIntRepository::RevIntRepository
RevIntRepository(Model *model)
Definition: integer.h:1076
operations_research::sat::IntegerTrail::IsOptional
bool IsOptional(IntegerVariable i) const
Definition: integer.h:615
operations_research::sat::SatSolver::NewBooleanVariable
BooleanVariable NewBooleanVariable()
Definition: sat_solver.h:84
operations_research::sat::PropagatorInterface::Propagate
virtual bool Propagate()=0
operations_research::sat::GenericLiteralWatcher::GetCurrentId
int GetCurrentId() const
Definition: integer.h:1193
operations_research::sat::GenericLiteralWatcher::WatchUpperBound
void WatchUpperBound(AffineExpression e, int id)
Definition: integer.h:1138
operations_research::sat::SatPropagator
Definition: sat_base.h:445
operations_research::sat::InlinedIntegerLiteralVector
absl::InlinedVector< IntegerLiteral, 2 > InlinedIntegerLiteralVector
Definition: integer.h:198
operations_research::sat::FullyEncodeVariable
std::function< std::vector< IntegerEncoder::ValueLiteralPair >Model *)> FullyEncodeVariable(IntegerVariable var)
Definition: integer.h:1570
operations_research::sat::IntegerEncoder
Definition: integer.h:276
operations_research::sat::IntegerLiteral::IsValid
bool IsValid() const
Definition: integer.h:170
operations_research::sat::GenericLiteralWatcher::WatchUpperBound
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1374
operations_research::sat::IntegerTrail::AddIntegerVariable
IntegerVariable AddIntegerVariable()
Definition: integer.h:606
operations_research::sat::Trail
Definition: sat_base.h:233
operations_research::sat::IntegerEncoder::ValueLiteralPair::operator<
bool operator<(const ValueLiteralPair &o) const
Definition: integer.h:323
operations_research::sat::IntegerEncoder::FullyEncodeVariable
void FullyEncodeVariable(IntegerVariable var)
Definition: integer.cc:36
bitset.h
operations_research::sat::IntegerEncoder::VariableIsFullyEncoded
bool VariableIsFullyEncoded(IntegerVariable var) const
Definition: integer.cc:68
kint64max
static const int64 kint64max
Definition: integral_types.h:62
operations_research::sat::IntegerTrail::CurrentBranchHadAnIncompletePropagation
bool CurrentBranchHadAnIncompletePropagation()
Definition: integer.cc:1157
operations_research::sat::AffineExpression::Negated
AffineExpression Negated() const
Definition: integer.h:224