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