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