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