OR-Tools  8.2
sat_base.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// Basic types and classes used by the sat solver.
15
16#ifndef OR_TOOLS_SAT_SAT_BASE_H_
17#define OR_TOOLS_SAT_SAT_BASE_H_
18
19#include <algorithm>
20#include <deque>
21#include <memory>
22#include <string>
23#include <vector>
24
25#include "absl/strings/str_format.h"
26#include "absl/types/span.h"
30#include "ortools/base/macros.h"
32#include "ortools/sat/model.h"
33#include "ortools/util/bitset.h"
34
35namespace operations_research {
36namespace sat {
37
38// Index of a variable (>= 0).
39DEFINE_INT_TYPE(BooleanVariable, int);
40const BooleanVariable kNoBooleanVariable(-1);
41
42// Index of a literal (>= 0), see Literal below.
43DEFINE_INT_TYPE(LiteralIndex, int);
44const LiteralIndex kNoLiteralIndex(-1);
45
46// Special values used in some API to indicate a literal that is always true
47// or always false.
48const LiteralIndex kTrueLiteralIndex(-2);
49const LiteralIndex kFalseLiteralIndex(-3);
50
51// A literal is used to represent a variable or its negation. If it represents
52// the variable it is said to be positive. If it represent its negation, it is
53// said to be negative. We support two representations as an integer.
54//
55// The "signed" encoding of a literal is convenient for input/output and is used
56// in the cnf file format. For a 0-based variable index x, (x + 1) represent the
57// variable x and -(x + 1) represent its negation. The signed value 0 is an
58// undefined literal and this class can never contain it.
59//
60// The "index" encoding of a literal is convenient as an index to an array
61// and is the one used internally for efficiency. It is always positive or zero,
62// and for a 0-based variable index x, (x << 1) encode the variable x and the
63// same number XOR 1 encode its negation.
64class Literal {
65 public:
66 // Not explicit for tests so we can write:
67 // vector<literal> literal = {+1, -3, +4, -9};
68 Literal(int signed_value) // NOLINT
69 : index_(signed_value > 0 ? ((signed_value - 1) << 1)
70 : ((-signed_value - 1) << 1) ^ 1) {
71 CHECK_NE(signed_value, 0);
72 }
73
75 explicit Literal(LiteralIndex index) : index_(index.value()) {}
76 Literal(BooleanVariable variable, bool is_positive)
77 : index_(is_positive ? (variable.value() << 1)
78 : (variable.value() << 1) ^ 1) {}
79
80 BooleanVariable Variable() const { return BooleanVariable(index_ >> 1); }
81 bool IsPositive() const { return !(index_ & 1); }
82 bool IsNegative() const { return (index_ & 1); }
83
84 LiteralIndex Index() const { return LiteralIndex(index_); }
85 LiteralIndex NegatedIndex() const { return LiteralIndex(index_ ^ 1); }
86
87 int SignedValue() const {
88 return (index_ & 1) ? -((index_ >> 1) + 1) : ((index_ >> 1) + 1);
89 }
90
91 Literal Negated() const { return Literal(NegatedIndex()); }
92
93 std::string DebugString() const {
94 return absl::StrFormat("%+d", SignedValue());
95 }
96 bool operator==(Literal other) const { return index_ == other.index_; }
97 bool operator!=(Literal other) const { return index_ != other.index_; }
98
99 bool operator<(const Literal& literal) const {
100 return Index() < literal.Index();
101 }
102
103 private:
104 int index_;
105};
106
107inline std::ostream& operator<<(std::ostream& os, Literal literal) {
108 os << literal.DebugString();
109 return os;
110}
111
112inline std::ostream& operator<<(std::ostream& os,
113 absl::Span<const Literal> literals) {
114 for (const Literal literal : literals) {
115 os << literal.DebugString() << ",";
116 }
117 return os;
118}
119
120// Holds the current variable assignment of the solver.
121// Each variable can be unassigned or be assigned to true or false.
123 public:
125 explicit VariablesAssignment(int num_variables) { Resize(num_variables); }
126 void Resize(int num_variables) {
127 assignment_.Resize(LiteralIndex(num_variables << 1));
128 }
129
130 // Makes the given literal true by assigning its underlying variable to either
131 // true or false depending on the literal sign. This can only be called on an
132 // unassigned variable.
134 DCHECK(!VariableIsAssigned(literal.Variable()));
135 assignment_.Set(literal.Index());
136 }
137
138 // Unassign the variable corresponding to the given literal.
139 // This can only be called on an assigned variable.
141 DCHECK(VariableIsAssigned(literal.Variable()));
142 assignment_.ClearTwoBits(literal.Index());
143 }
144
145 // Literal getters. Note that both can be false, in which case the
146 // corresponding variable is not assigned.
148 return assignment_.IsSet(literal.NegatedIndex());
149 }
151 return assignment_.IsSet(literal.Index());
152 }
154 return assignment_.AreOneOfTwoBitsSet(literal.Index());
155 }
156
157 // Returns true iff the given variable is assigned.
158 bool VariableIsAssigned(BooleanVariable var) const {
159 return assignment_.AreOneOfTwoBitsSet(LiteralIndex(var.value() << 1));
160 }
161
162 // Returns the literal of the given variable that is assigned to true.
163 // That is, depending on the variable, it can be the positive literal or the
164 // negative one. Only call this on an assigned variable.
167 return Literal(var, assignment_.IsSet(LiteralIndex(var.value() << 1)));
168 }
169
170 int NumberOfVariables() const { return assignment_.size().value() / 2; }
171
172 private:
173 // The encoding is as follows:
174 // - assignment_.IsSet(literal.Index()) means literal is true.
175 // - assignment_.IsSet(literal.Index() ^ 1]) means literal is false.
176 // - If both are false, then the variable (and the literal) is unassigned.
177 Bitset64<LiteralIndex> assignment_;
178
179 DISALLOW_COPY_AND_ASSIGN(VariablesAssignment);
180};
181
182// Forward declaration.
183class SatClause;
184class SatPropagator;
185
186// Information about a variable assignment.
188 // The decision level at which this assignment was made. This starts at 0 and
189 // increases each time the solver takes a search decision.
190 //
191 // TODO(user): We may be able to get rid of that for faster enqueues. Most of
192 // the code only need to know if this is 0 or the highest level, and for the
193 // LBD computation, the literal of the conflict are already ordered by level,
194 // so we could do it fairly efficiently.
195 //
196 // TODO(user): We currently don't support more than 2^28 decision levels. That
197 // should be enough for most practical problem, but we should fail properly if
198 // this limit is reached.
200
201 // The type of assignment (see AssignmentType below).
202 //
203 // Note(user): We currently don't support more than 16 types of assignment.
204 // This is checked in RegisterPropagator().
205 mutable uint32 type : 4;
206
207 // The index of this assignment in the trail.
209
210 std::string DebugString() const {
211 return absl::StrFormat("level:%d type:%d trail_index:%d", level, type,
213 }
214};
215static_assert(sizeof(AssignmentInfo) == 8,
216 "ERROR_AssignmentInfo_is_not_well_compacted");
217
218// Each literal on the trail will have an associated propagation "type" which is
219// either one of these special types or the id of a propagator.
221 static constexpr int kCachedReason = 0;
222 static constexpr int kUnitReason = 1;
223 static constexpr int kSearchDecision = 2;
224 static constexpr int kSameReasonAs = 3;
225
226 // Propagator ids starts from there and are created dynamically.
227 static constexpr int kFirstFreePropagationId = 4;
228};
229
230// The solver trail stores the assignment made by the solver in order.
231// This class is responsible for maintaining the assignment of each variable
232// and the information of each assignment.
233class Trail {
234 public:
235 explicit Trail(Model* model) : Trail() {}
236
238 current_info_.trail_index = 0;
239 current_info_.level = 0;
240 }
241
242 void Resize(int num_variables);
243
244 // Registers a propagator. This assigns a unique id to this propagator and
245 // calls SetPropagatorId() on it.
246 void RegisterPropagator(SatPropagator* propagator);
247
248 // Enqueues the assignment that make the given literal true on the trail. This
249 // should only be called on unassigned variables.
250 void Enqueue(Literal true_literal, int propagator_id) {
251 DCHECK(!assignment_.VariableIsAssigned(true_literal.Variable()));
252 trail_[current_info_.trail_index] = true_literal;
253 current_info_.type = propagator_id;
254 info_[true_literal.Variable()] = current_info_;
255 assignment_.AssignFromTrueLiteral(true_literal);
256 ++current_info_.trail_index;
257 }
258
259 // Specific Enqueue() version for the search decision.
260 void EnqueueSearchDecision(Literal true_literal) {
262 }
263
264 // Specific Enqueue() version for a fixed variable.
265 void EnqueueWithUnitReason(Literal true_literal) {
267 }
268
269 // Some constraints propagate a lot of literals at once. In these cases, it is
270 // more efficient to have all the propagated literals except the first one
271 // referring to the reason of the first of them.
273 BooleanVariable reference_var) {
274 reference_var_with_same_reason_as_[true_literal.Variable()] = reference_var;
276 }
277
278 // Enqueues the given literal using the current content of
279 // GetEmptyVectorToStoreReason() as the reason. This API is a bit more
280 // leanient and does not require the literal to be unassigned. If it is
281 // already assigned to false, then MutableConflict() will be set appropriately
282 // and this will return false otherwise this will enqueue the literal and
283 // returns true.
284 ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason(Literal true_literal) {
285 if (assignment_.LiteralIsTrue(true_literal)) return true;
286 if (assignment_.LiteralIsFalse(true_literal)) {
287 *MutableConflict() = reasons_repository_[Index()];
288 MutableConflict()->push_back(true_literal);
289 return false;
290 }
291
293 const BooleanVariable var = true_literal.Variable();
294 reasons_[var] = reasons_repository_[info_[var].trail_index];
295 old_type_[var] = info_[var].type;
297 return true;
298 }
299
300 // Returns the reason why this variable was assigned.
301 //
302 // Note that this shouldn't be called on a variable at level zero, because we
303 // don't cleanup the reason data for these variables but the underlying
304 // clauses may have been deleted.
305 absl::Span<const Literal> Reason(BooleanVariable var) const;
306
307 // Returns the "type" of an assignment (see AssignmentType). Note that this
308 // function never returns kSameReasonAs or kCachedReason, it instead returns
309 // the initial type that caused this assignment. As such, it is different
310 // from Info(var).type and the latter should not be used outside this class.
311 int AssignmentType(BooleanVariable var) const;
312
313 // If a variable was propagated with EnqueueWithSameReasonAs(), returns its
314 // reference variable. Otherwise return the given variable.
315 BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const;
316
317 // This can be used to get a location at which the reason for the literal
318 // at trail_index on the trail can be stored. This clears the vector before
319 // returning it.
320 std::vector<Literal>* GetEmptyVectorToStoreReason(int trail_index) const {
321 if (trail_index >= reasons_repository_.size()) {
322 reasons_repository_.resize(trail_index + 1);
323 }
324 reasons_repository_[trail_index].clear();
325 return &reasons_repository_[trail_index];
326 }
327
328 // Shortcut for GetEmptyVectorToStoreReason(Index()).
329 std::vector<Literal>* GetEmptyVectorToStoreReason() const {
331 }
332
333 // Explicitly overwrite the reason so that the given propagator will be
334 // asked for it. This is currently only used by the BinaryImplicationGraph.
335 void ChangeReason(int trail_index, int propagator_id) {
336 const BooleanVariable var = trail_[trail_index].Variable();
337 info_[var].type = propagator_id;
338 old_type_[var] = propagator_id;
339 }
340
341 // Reverts the trail and underlying assignment to the given target trail
342 // index. Note that we do not touch the assignment info.
343 void Untrail(int target_trail_index) {
344 const int index = Index();
345 num_untrailed_enqueues_ += index - target_trail_index;
346 for (int i = target_trail_index; i < index; ++i) {
347 assignment_.UnassignLiteral(trail_[i]);
348 }
349 current_info_.trail_index = target_trail_index;
350 }
351 void Dequeue() { Untrail(Index() - 1); }
352
353 // Changes the decision level used by the next Enqueue().
354 void SetDecisionLevel(int level) { current_info_.level = level; }
355 int CurrentDecisionLevel() const { return current_info_.level; }
356
357 // Generic interface to set the current failing clause.
358 //
359 // Returns the address of a vector where a client can store the current
360 // conflict. This vector will be returned by the FailingClause() call.
361 std::vector<Literal>* MutableConflict() {
362 failing_sat_clause_ = nullptr;
363 return &conflict_;
364 }
365
366 // Returns the last conflict.
367 absl::Span<const Literal> FailingClause() const { return conflict_; }
368
369 // Specific SatClause interface so we can update the conflict clause activity.
370 // Note that MutableConflict() automatically sets this to nullptr, so we can
371 // know whether or not the last conflict was caused by a clause.
372 void SetFailingSatClause(SatClause* clause) { failing_sat_clause_ = clause; }
373 SatClause* FailingSatClause() const { return failing_sat_clause_; }
374
375 // Getters.
376 int NumVariables() const { return trail_.size(); }
377 int64 NumberOfEnqueues() const { return num_untrailed_enqueues_ + Index(); }
378 int Index() const { return current_info_.trail_index; }
379 const Literal& operator[](int index) const { return trail_[index]; }
380 const VariablesAssignment& Assignment() const { return assignment_; }
381 const AssignmentInfo& Info(BooleanVariable var) const {
382 DCHECK_GE(var, 0);
383 DCHECK_LT(var, info_.size());
384 return info_[var];
385 }
386
387 // Print the current literals on the trail.
388 std::string DebugString() {
389 std::string result;
390 for (int i = 0; i < current_info_.trail_index; ++i) {
391 if (!result.empty()) result += " ";
392 result += trail_[i].DebugString();
393 }
394 return result;
395 }
396
397 private:
398 int64 num_untrailed_enqueues_ = 0;
399 AssignmentInfo current_info_;
400 VariablesAssignment assignment_;
401 std::vector<Literal> trail_;
402 std::vector<Literal> conflict_;
404 SatClause* failing_sat_clause_;
405
406 // Data used by EnqueueWithSameReasonAs().
408 reference_var_with_same_reason_as_;
409
410 // Reason cache. Mutable since we want the API to be the same whether the
411 // reason are cached or not.
412 //
413 // When a reason is computed for the first time, we change the type of the
414 // variable assignment to kCachedReason so that we know that if it is needed
415 // again the reason can just be retrieved by a direct access to reasons_. The
416 // old type is saved in old_type_ and can be retrieved by
417 // AssignmentType().
418 //
419 // Note(user): Changing the type is not "clean" but it is efficient. The idea
420 // is that it is important to do as little as possible when pushing/popping
421 // literals on the trail. Computing the reason happens a lot less often, so it
422 // is okay to do slightly more work then. Note also, that we don't need to
423 // do anything on "untrail", the kCachedReason type will be overwritten when
424 // the same variable is assigned again.
425 //
426 // TODO(user): An alternative would be to change the sign of the type. This
427 // would remove the need for a separate old_type_ vector, but it requires
428 // more bits for the type filed in AssignmentInfo.
429 //
430 // Note that we use a deque for the reason repository so that if we add
431 // variables, the memory address of the vectors (kept in reasons_) are still
432 // valid.
433 mutable std::deque<std::vector<Literal>> reasons_repository_;
435 reasons_;
437
438 // This is used by RegisterPropagator() and Reason().
439 std::vector<SatPropagator*> propagators_;
440
441 DISALLOW_COPY_AND_ASSIGN(Trail);
442};
443
444// Base class for all the SAT constraints.
446 public:
447 explicit SatPropagator(const std::string& name)
449 virtual ~SatPropagator() {}
450
451 // Sets/Gets this propagator unique id.
452 void SetPropagatorId(int id) { propagator_id_ = id; }
453 int PropagatorId() const { return propagator_id_; }
454
455 // Inspects the trail from propagation_trail_index_ until at least one literal
456 // is propagated. Returns false iff a conflict is detected (in which case
457 // trail->SetFailingClause() must be called).
458 //
459 // This must update propagation_trail_index_ so that all the literals before
460 // it have been propagated. In particular, if nothing was propagated, then
461 // PropagationIsDone() must return true.
462 virtual bool Propagate(Trail* trail) = 0;
463
464 // Reverts the state so that all the literals with a trail index greater or
465 // equal to the given one are not processed for propagation. Note that the
466 // trail current decision level is already reverted before this is called.
467 //
468 // TODO(user): Currently this is called at each Backtrack(), but we could
469 // bundle the calls in case multiple conflict one after the other are detected
470 // even before the Propagate() call of a SatPropagator is called.
471 //
472 // TODO(user): It is not yet 100% the case, but this can be guaranteed to be
473 // called with a trail index that will always be the start of a new decision
474 // level.
475 virtual void Untrail(const Trail& trail, int trail_index) {
477 }
478
479 // Explains why the literal at given trail_index was propagated by returning a
480 // reason for this propagation. This will only be called for literals that are
481 // on the trail and were propagated by this class.
482 //
483 // The interpretation is that because all the literals of a reason were
484 // assigned to false, we could deduce the assignement of the given variable.
485 //
486 // The returned Span has to be valid until the literal is untrailed. A client
487 // can use trail_.GetEmptyVectorToStoreReason() if it doesn't have a memory
488 // location that already contains the reason.
489 virtual absl::Span<const Literal> Reason(const Trail& trail,
490 int trail_index) const {
491 LOG(FATAL) << "Not implemented.";
492 return {};
493 }
494
495 // Returns true if all the preconditions for Propagate() are satisfied.
496 // This is just meant to be used in a DCHECK.
497 bool PropagatePreconditionsAreSatisfied(const Trail& trail) const;
498
499 // Returns true iff all the trail was inspected by this propagator.
500 bool PropagationIsDone(const Trail& trail) const {
501 return propagation_trail_index_ == trail.Index();
502 }
503
504 protected:
505 const std::string name_;
508
509 private:
510 DISALLOW_COPY_AND_ASSIGN(SatPropagator);
511};
512
513// ######################## Implementations below ########################
514
515// TODO(user): A few of these method should be moved in a .cc
516
518 const Trail& trail) const {
519 if (propagation_trail_index_ > trail.Index()) {
520 LOG(INFO) << "Issue in '" << name_ << ":"
521 << " propagation_trail_index_=" << propagation_trail_index_
522 << " trail_.Index()=" << trail.Index();
523 return false;
524 }
525 if (propagation_trail_index_ < trail.Index() &&
526 trail.Info(trail[propagation_trail_index_].Variable()).level !=
527 trail.CurrentDecisionLevel()) {
528 LOG(INFO) << "Issue in '" << name_ << "':"
529 << " propagation_trail_index_=" << propagation_trail_index_
530 << " trail_.Index()=" << trail.Index()
531 << " level_at_propagation_index="
532 << trail.Info(trail[propagation_trail_index_].Variable()).level
533 << " current_decision_level=" << trail.CurrentDecisionLevel();
534 return false;
535 }
536 return true;
537}
538
539inline void Trail::Resize(int num_variables) {
540 assignment_.Resize(num_variables);
541 info_.resize(num_variables);
542 trail_.resize(num_variables);
543 reasons_.resize(num_variables);
544
545 // TODO(user): these vectors are not always used. Initialize them
546 // dynamically.
547 old_type_.resize(num_variables);
548 reference_var_with_same_reason_as_.resize(num_variables);
549}
550
551inline void Trail::RegisterPropagator(SatPropagator* propagator) {
552 if (propagators_.empty()) {
553 propagators_.resize(AssignmentType::kFirstFreePropagationId);
554 }
555 CHECK_LT(propagators_.size(), 16);
556 propagator->SetPropagatorId(propagators_.size());
557 propagators_.push_back(propagator);
558}
559
561 BooleanVariable var) const {
562 DCHECK(Assignment().VariableIsAssigned(var));
563 // Note that we don't use AssignmentType() here.
564 if (info_[var].type == AssignmentType::kSameReasonAs) {
565 var = reference_var_with_same_reason_as_[var];
566 DCHECK(Assignment().VariableIsAssigned(var));
568 }
569 return var;
570}
571
572inline int Trail::AssignmentType(BooleanVariable var) const {
573 if (info_[var].type == AssignmentType::kSameReasonAs) {
574 var = reference_var_with_same_reason_as_[var];
576 }
577 const int type = info_[var].type;
578 return type != AssignmentType::kCachedReason ? type : old_type_[var];
579}
580
581inline absl::Span<const Literal> Trail::Reason(BooleanVariable var) const {
582 // Special case for AssignmentType::kSameReasonAs to avoid a recursive call.
584
585 // Fast-track for cached reason.
586 if (info_[var].type == AssignmentType::kCachedReason) return reasons_[var];
587
588 const AssignmentInfo& info = info_[var];
589 if (info.type == AssignmentType::kUnitReason ||
591 reasons_[var] = {};
592 } else {
593 DCHECK_LT(info.type, propagators_.size());
594 DCHECK(propagators_[info.type] != nullptr) << info.type;
595 reasons_[var] = propagators_[info.type]->Reason(*this, info.trail_index);
596 }
597 old_type_[var] = info.type;
599 return reasons_[var];
600}
601
602} // namespace sat
603} // namespace operations_research
604
605#endif // OR_TOOLS_SAT_SAT_BASE_H_
int64 min
Definition: alldiff_cst.cc:138
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
void resize(size_type new_size)
IndexType size() const
Definition: bitset.h:419
void Set(IndexType i)
Definition: bitset.h:491
void Resize(IndexType size)
Definition: bitset.h:429
bool IsSet(IndexType i) const
Definition: bitset.h:481
void ClearTwoBits(IndexType i)
Definition: bitset.h:467
bool AreOneOfTwoBitsSet(IndexType i) const
Definition: bitset.h:474
Literal(int signed_value)
Definition: sat_base.h:68
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
LiteralIndex Index() const
Definition: sat_base.h:84
Literal(LiteralIndex index)
Definition: sat_base.h:75
Literal(BooleanVariable variable, bool is_positive)
Definition: sat_base.h:76
BooleanVariable Variable() const
Definition: sat_base.h:80
std::string DebugString() const
Definition: sat_base.h:93
bool operator==(Literal other) const
Definition: sat_base.h:96
bool operator!=(Literal other) const
Definition: sat_base.h:97
bool operator<(const Literal &literal) const
Definition: sat_base.h:99
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
virtual bool Propagate(Trail *trail)=0
SatPropagator(const std::string &name)
Definition: sat_base.h:447
bool PropagatePreconditionsAreSatisfied(const Trail &trail) const
Definition: sat_base.h:517
virtual void Untrail(const Trail &trail, int trail_index)
Definition: sat_base.h:475
virtual absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const
Definition: sat_base.h:489
bool PropagationIsDone(const Trail &trail) const
Definition: sat_base.h:500
void RegisterPropagator(SatPropagator *propagator)
Definition: sat_base.h:551
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
SatClause * FailingSatClause() const
Definition: sat_base.h:373
void ChangeReason(int trail_index, int propagator_id)
Definition: sat_base.h:335
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
Definition: sat_base.h:272
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
int AssignmentType(BooleanVariable var) const
Definition: sat_base.h:572
void SetFailingSatClause(SatClause *clause)
Definition: sat_base.h:372
absl::Span< const Literal > Reason(BooleanVariable var) const
Definition: sat_base.h:581
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const
Definition: sat_base.h:560
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason(Literal true_literal)
Definition: sat_base.h:284
void Untrail(int target_trail_index)
Definition: sat_base.h:343
int64 NumberOfEnqueues() const
Definition: sat_base.h:377
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
absl::Span< const Literal > FailingClause() const
Definition: sat_base.h:367
void SetDecisionLevel(int level)
Definition: sat_base.h:354
std::vector< Literal > * GetEmptyVectorToStoreReason() const
Definition: sat_base.h:329
const Literal & operator[](int index) const
Definition: sat_base.h:379
void Resize(int num_variables)
Definition: sat_base.h:539
void EnqueueWithUnitReason(Literal true_literal)
Definition: sat_base.h:265
void EnqueueSearchDecision(Literal true_literal)
Definition: sat_base.h:260
bool LiteralIsAssigned(Literal literal) const
Definition: sat_base.h:153
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
void AssignFromTrueLiteral(Literal literal)
Definition: sat_base.h:133
Literal GetTrueLiteralForAssignedVariable(BooleanVariable var) const
Definition: sat_base.h:165
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
const std::string name
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
unsigned int uint32
int int32
int64_t int64
const int INFO
Definition: log_severity.h:31
const int FATAL
Definition: log_severity.h:32
const LiteralIndex kFalseLiteralIndex(-3)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
Definition: cp_model.cc:65
const LiteralIndex kNoLiteralIndex(-1)
DEFINE_INT_TYPE(ClauseIndex, int)
const BooleanVariable kNoBooleanVariable(-1)
const LiteralIndex kTrueLiteralIndex(-2)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
static constexpr int kSameReasonAs
Definition: sat_base.h:224
static constexpr int kFirstFreePropagationId
Definition: sat_base.h:227
static constexpr int kSearchDecision
Definition: sat_base.h:223
static constexpr int kCachedReason
Definition: sat_base.h:221