Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
sat_solver.cc
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
15
16#include <algorithm>
17#include <cstddef>
18#include <cstdint>
19#include <limits>
20#include <memory>
21#include <string>
22#include <utility>
23#include <vector>
24
25#include "absl/base/attributes.h"
26#include "absl/container/btree_set.h"
27#include "absl/container/flat_hash_map.h"
28#include "absl/log/check.h"
29#include "absl/log/log.h"
30#include "absl/log/vlog_is_on.h"
31#include "absl/meta/type_traits.h"
32#include "absl/strings/str_cat.h"
33#include "absl/strings/str_format.h"
34#include "absl/types/span.h"
37#include "ortools/base/timer.h"
40#include "ortools/sat/clause.h"
42#include "ortools/sat/model.h"
44#include "ortools/sat/restart.h"
47#include "ortools/sat/sat_parameters.pb.h"
48#include "ortools/sat/util.h"
49#include "ortools/util/bitset.h"
52#include "ortools/util/stats.h"
55
56namespace operations_research {
57namespace sat {
58
60 owned_model_.reset(model_);
61 model_->Register<SatSolver>(this);
62}
63
65 : model_(model),
66 binary_implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
67 clauses_propagator_(model->GetOrCreate<ClauseManager>()),
68 pb_constraints_(model->GetOrCreate<PbConstraints>()),
69 track_binary_clauses_(false),
70 trail_(model->GetOrCreate<Trail>()),
71 time_limit_(model->GetOrCreate<TimeLimit>()),
72 parameters_(model->GetOrCreate<SatParameters>()),
73 restart_(model->GetOrCreate<RestartPolicy>()),
74 decision_policy_(model->GetOrCreate<SatDecisionPolicy>()),
75 logger_(model->GetOrCreate<SolverLogger>()),
76 clause_activity_increment_(1.0),
77 same_reason_identifier_(*trail_),
78 is_relevant_for_core_computation_(true),
79 drat_proof_handler_(nullptr),
80 stats_("SatSolver") {
81 InitializePropagators();
82}
83
84SatSolver::~SatSolver() { IF_STATS_ENABLED(LOG(INFO) << stats_.StatString()); }
85
86void SatSolver::SetNumVariables(int num_variables) {
87 SCOPED_TIME_STAT(&stats_);
88 CHECK_GE(num_variables, num_variables_);
89
90 num_variables_ = num_variables;
91 binary_implication_graph_->Resize(num_variables);
92 clauses_propagator_->Resize(num_variables);
93 trail_->Resize(num_variables);
94 decision_policy_->IncreaseNumVariables(num_variables);
95 pb_constraints_->Resize(num_variables);
96 same_reason_identifier_.Resize(num_variables);
97
98 // The +1 is a bit tricky, it is because in
99 // EnqueueDecisionAndBacktrackOnConflict() we artificially enqueue the
100 // decision before checking if it is not already assigned.
101 decisions_.resize(num_variables + 1);
102}
103
104int64_t SatSolver::num_branches() const { return counters_.num_branches; }
105
106int64_t SatSolver::num_failures() const { return counters_.num_failures; }
107
109 return trail_->NumberOfEnqueues() - counters_.num_branches;
110}
111
112int64_t SatSolver::num_backtracks() const { return counters_.num_backtracks; }
113
114int64_t SatSolver::num_restarts() const { return counters_.num_restarts; }
115
117 // Each of these counters mesure really basic operations. The weight are just
118 // an estimate of the operation complexity. Note that these counters are never
119 // reset to zero once a SatSolver is created.
120 //
121 // TODO(user): Find a better procedure to fix the weight than just educated
122 // guess.
123 return 1e-8 * (8.0 * trail_->NumberOfEnqueues() +
124 1.0 * binary_implication_graph_->num_inspections() +
125 4.0 * clauses_propagator_->num_inspected_clauses() +
126 1.0 * clauses_propagator_->num_inspected_clause_literals() +
127
128 // Here there is a factor 2 because of the untrail.
129 20.0 * pb_constraints_->num_constraint_lookups() +
130 2.0 * pb_constraints_->num_threshold_updates() +
131 1.0 * pb_constraints_->num_inspected_constraint_literals());
132}
133
134const SatParameters& SatSolver::parameters() const {
135 SCOPED_TIME_STAT(&stats_);
136 return *parameters_;
137}
138
139void SatSolver::SetParameters(const SatParameters& parameters) {
140 SCOPED_TIME_STAT(&stats_);
141 *parameters_ = parameters;
142 restart_->Reset();
143 time_limit_->ResetLimitFromParameters(parameters);
144 logger_->EnableLogging(parameters.log_search_progress() || VLOG_IS_ON(1));
145 logger_->SetLogToStdOut(parameters.log_to_stdout());
146}
147
148bool SatSolver::IsMemoryLimitReached() const {
149 const int64_t memory_usage =
151 const int64_t kMegaByte = 1024 * 1024;
152 return memory_usage > kMegaByte * parameters_->max_memory_in_mb();
153}
154
155bool SatSolver::SetModelUnsat() {
156 model_is_unsat_ = true;
157 return false;
158}
159
160bool SatSolver::AddClauseDuringSearch(absl::Span<const Literal> literals) {
161 if (model_is_unsat_) return false;
162
163 // Let filter clauses if we are at level zero
164 if (trail_->CurrentDecisionLevel() == 0) {
165 return AddProblemClause(literals);
166 }
167
168 const int index = trail_->Index();
169 if (literals.empty()) return SetModelUnsat();
170 if (literals.size() == 1) return AddUnitClause(literals[0]);
171 if (literals.size() == 2) {
172 // TODO(user): We generate in some corner cases clauses with
173 // literals[0].Variable() == literals[1].Variable(). Avoid doing that and
174 // adding such binary clauses to the graph?
175 if (!binary_implication_graph_->AddBinaryClause(literals[0], literals[1])) {
176 CHECK_EQ(CurrentDecisionLevel(), 0);
177 return SetModelUnsat();
178 }
179 } else {
180 if (!clauses_propagator_->AddClause(literals)) {
181 CHECK_EQ(CurrentDecisionLevel(), 0);
182 return SetModelUnsat();
183 }
184 }
185
186 // Tricky: Even if nothing new is propagated, calling Propagate() might, via
187 // the LP, deduce new things. This is problematic because some code assumes
188 // that when we create newly associated literals, nothing else changes.
189 if (trail_->Index() == index) return true;
190 return FinishPropagation();
191}
192
194 return AddProblemClause({true_literal});
195}
196
200
202 return AddProblemClause({a, b, c});
203}
204
205// Note that we will do a bit of presolve here, which might not always be
206// necessary if we know we are already adding a "clean" clause with no
207// duplicates or literal equivalent to others. However, we found that it is
208// better to make sure we always have "clean" clause in the solver rather than
209// to over-optimize this. In particular, presolve might be disabled or
210// incomplete, so such unclean clause might find their way here.
211bool SatSolver::AddProblemClause(absl::Span<const Literal> literals) {
212 SCOPED_TIME_STAT(&stats_);
213 DCHECK_EQ(CurrentDecisionLevel(), 0);
214 if (model_is_unsat_) return false;
215
216 // Filter already assigned literals. Note that we also remap literal in case
217 // we discovered equivalence later in the search.
218 literals_scratchpad_.clear();
219 for (Literal l : literals) {
220 l = binary_implication_graph_->RepresentativeOf(l);
221 if (trail_->Assignment().LiteralIsTrue(l)) return true;
222 if (trail_->Assignment().LiteralIsFalse(l)) continue;
223 literals_scratchpad_.push_back(l);
224 }
225
226 // A clause with l and not(l) is trivially true.
227 gtl::STLSortAndRemoveDuplicates(&literals_scratchpad_);
228 for (int i = 0; i + 1 < literals_scratchpad_.size(); ++i) {
229 if (literals_scratchpad_[i] == literals_scratchpad_[i + 1].Negated()) {
230 return true;
231 }
232 }
233
234 return AddProblemClauseInternal(literals_scratchpad_);
235}
236
237bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
238 SCOPED_TIME_STAT(&stats_);
239 if (DEBUG_MODE && CurrentDecisionLevel() == 0) {
240 for (const Literal l : literals) {
241 CHECK(!trail_->Assignment().LiteralIsAssigned(l));
242 }
243 }
244
245 if (literals.empty()) return SetModelUnsat();
246
247 if (literals.size() == 1) {
248 if (drat_proof_handler_ != nullptr) {
249 // Note that we will output problem unit clauses twice, but that is a
250 // small price to pay for having a single variable fixing API.
251 drat_proof_handler_->AddClause({literals[0]});
252 }
253 trail_->EnqueueWithUnitReason(literals[0]);
254 } else if (literals.size() == 2) {
255 // TODO(user): Make sure the presolve do not generate such clauses.
256 if (literals[0] == literals[1]) {
257 // Literal must be true.
258 trail_->EnqueueWithUnitReason(literals[0]);
259 } else if (literals[0] == literals[1].Negated()) {
260 // Always true.
261 return true;
262 } else {
263 AddBinaryClauseInternal(literals[0], literals[1]);
264 }
265 } else {
266 if (!clauses_propagator_->AddClause(literals, trail_, /*lbd=*/-1)) {
267 return SetModelUnsat();
268 }
269 }
270
271 // Tricky: The PropagationIsDone() condition shouldn't change anything for a
272 // pure SAT problem, however in the CP-SAT context, calling Propagate() can
273 // tigger computation (like the LP) even if no domain changed since the last
274 // call. We do not want to do that.
275 if (!PropagationIsDone() && !Propagate()) {
276 return SetModelUnsat();
277 }
278 return true;
279}
280
281bool SatSolver::AddLinearConstraintInternal(
282 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
283 Coefficient max_value) {
284 SCOPED_TIME_STAT(&stats_);
286 if (rhs < 0) return SetModelUnsat(); // Unsatisfiable constraint.
287 if (rhs >= max_value) return true; // Always satisfied constraint.
288
289 // Since the constraint is in canonical form, the coefficients are sorted.
290 const Coefficient min_coeff = cst.front().coefficient;
291 const Coefficient max_coeff = cst.back().coefficient;
292
293 // A linear upper bounded constraint is a clause if the only problematic
294 // assignment is the one where all the literals are true.
295 if (max_value - min_coeff <= rhs) {
296 // This constraint is actually a clause. It is faster to treat it as one.
297 literals_scratchpad_.clear();
298 for (const LiteralWithCoeff& term : cst) {
299 literals_scratchpad_.push_back(term.literal.Negated());
300 }
301 return AddProblemClauseInternal(literals_scratchpad_);
302 }
303
304 // Detect at most one constraints. Note that this use the fact that the
305 // coefficient are sorted.
306 if (!parameters_->use_pb_resolution() && max_coeff <= rhs &&
307 2 * min_coeff > rhs) {
308 literals_scratchpad_.clear();
309 for (const LiteralWithCoeff& term : cst) {
310 literals_scratchpad_.push_back(term.literal);
311 }
312 if (!binary_implication_graph_->AddAtMostOne(literals_scratchpad_)) {
313 return SetModelUnsat();
314 }
315 return true;
316 }
317
318 // TODO(user): If this constraint forces all its literal to false (when rhs is
319 // zero for instance), we still add it. Optimize this?
320 return pb_constraints_->AddConstraint(cst, rhs, trail_);
321}
322
323void SatSolver::CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
324 Coefficient* bound_shift,
325 Coefficient* max_value) {
326 // This block removes assigned literals from the constraint.
327 Coefficient fixed_variable_shift(0);
328 {
329 int index = 0;
330 for (const LiteralWithCoeff& term : *cst) {
331 if (trail_->Assignment().LiteralIsFalse(term.literal)) continue;
332 if (trail_->Assignment().LiteralIsTrue(term.literal)) {
333 CHECK(SafeAddInto(-term.coefficient, &fixed_variable_shift));
334 continue;
335 }
336 (*cst)[index] = term;
337 ++index;
338 }
339 cst->resize(index);
340 }
341
342 // Now we canonicalize.
343 // TODO(user): fix variables that must be true/false and remove them.
344 Coefficient bound_delta(0);
345 CHECK(ComputeBooleanLinearExpressionCanonicalForm(cst, &bound_delta,
346 max_value));
347
348 CHECK(SafeAddInto(bound_delta, bound_shift));
349 CHECK(SafeAddInto(fixed_variable_shift, bound_shift));
350}
351
352bool SatSolver::AddLinearConstraint(bool use_lower_bound,
353 Coefficient lower_bound,
354 bool use_upper_bound,
355 Coefficient upper_bound,
356 std::vector<LiteralWithCoeff>* cst) {
357 SCOPED_TIME_STAT(&stats_);
358 CHECK_EQ(CurrentDecisionLevel(), 0);
359 if (model_is_unsat_) return false;
360
361 Coefficient bound_shift(0);
362
363 if (use_upper_bound) {
364 Coefficient max_value(0);
365 CanonicalizeLinear(cst, &bound_shift, &max_value);
366 const Coefficient rhs =
367 ComputeCanonicalRhs(upper_bound, bound_shift, max_value);
368 if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
369 return SetModelUnsat();
370 }
371 }
372
373 if (use_lower_bound) {
374 // We need to "re-canonicalize" in case some literal were fixed while we
375 // processed one direction.
376 Coefficient max_value(0);
377 CanonicalizeLinear(cst, &bound_shift, &max_value);
378
379 // We transform the constraint into an upper-bounded one.
380 for (int i = 0; i < cst->size(); ++i) {
381 (*cst)[i].literal = (*cst)[i].literal.Negated();
382 }
383 const Coefficient rhs =
384 ComputeNegatedCanonicalRhs(lower_bound, bound_shift, max_value);
385 if (!AddLinearConstraintInternal(*cst, rhs, max_value)) {
386 return SetModelUnsat();
387 }
388 }
389
390 // Tricky: The PropagationIsDone() condition shouldn't change anything for a
391 // pure SAT problem, however in the CP-SAT context, calling Propagate() can
392 // tigger computation (like the LP) even if no domain changed since the last
393 // call. We do not want to do that.
394 if (!PropagationIsDone() && !Propagate()) {
395 return SetModelUnsat();
396 }
397 return true;
398}
399
400int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
401 const std::vector<Literal>& literals, bool is_redundant) {
402 SCOPED_TIME_STAT(&stats_);
403
404 if (literals.size() == 1) {
405 // A length 1 clause fix a literal for all the search.
406 // ComputeBacktrackLevel() should have returned 0.
407 CHECK_EQ(CurrentDecisionLevel(), 0);
408 trail_->EnqueueWithUnitReason(literals[0]);
409 return /*lbd=*/1;
410 }
411
412 if (literals.size() == 2) {
413 if (track_binary_clauses_) {
414 // This clause MUST be knew, otherwise something is wrong.
415 CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1])));
416 }
417 CHECK(binary_implication_graph_->AddBinaryClause(literals[0], literals[1]));
418 return /*lbd=*/2;
419 }
420
421 CleanClauseDatabaseIfNeeded();
422
423 // Important: Even though the only literal at the last decision level has
424 // been unassigned, its level was not modified, so ComputeLbd() works.
425 const int lbd = ComputeLbd(literals);
426 if (is_redundant && lbd > parameters_->clause_cleanup_lbd_bound()) {
427 --num_learned_clause_before_cleanup_;
428
429 SatClause* clause =
430 clauses_propagator_->AddRemovableClause(literals, trail_, lbd);
431
432 // BumpClauseActivity() must be called after clauses_info_[clause] has
433 // been created or it will have no effect.
434 (*clauses_propagator_->mutable_clauses_info())[clause].lbd = lbd;
435 BumpClauseActivity(clause);
436 } else {
437 CHECK(clauses_propagator_->AddClause(literals, trail_, lbd));
438 }
439 return lbd;
440}
441
443 CHECK_EQ(CurrentDecisionLevel(), 0);
444 trail_->RegisterPropagator(propagator);
445 external_propagators_.push_back(propagator);
446 InitializePropagators();
447}
448
450 CHECK_EQ(CurrentDecisionLevel(), 0);
451 CHECK(last_propagator_ == nullptr);
452 trail_->RegisterPropagator(propagator);
453 last_propagator_ = propagator;
454 InitializePropagators();
455}
456
457UpperBoundedLinearConstraint* SatSolver::ReasonPbConstraintOrNull(
458 BooleanVariable var) const {
459 // It is important to deal properly with "SameReasonAs" variables here.
460 var = trail_->ReferenceVarWithSameReason(var);
461 const AssignmentInfo& info = trail_->Info(var);
462 if (trail_->AssignmentType(var) == pb_constraints_->PropagatorId()) {
463 return pb_constraints_->ReasonPbConstraint(info.trail_index);
464 }
465 return nullptr;
466}
467
468SatClause* SatSolver::ReasonClauseOrNull(BooleanVariable var) const {
469 DCHECK(trail_->Assignment().VariableIsAssigned(var));
470 const AssignmentInfo& info = trail_->Info(var);
471 if (trail_->AssignmentType(var) == clauses_propagator_->PropagatorId()) {
472 return clauses_propagator_->ReasonClause(info.trail_index);
473 }
474 return nullptr;
475}
476
478 debug_assignment_.Resize(num_variables_.value());
479 for (BooleanVariable i(0); i < num_variables_; ++i) {
480 debug_assignment_.AssignFromTrueLiteral(
481 trail_->Assignment().GetTrueLiteralForAssignedVariable(i));
482 }
483}
484
485void SatSolver::LoadDebugSolution(absl::Span<const Literal> solution) {
486 debug_assignment_.Resize(num_variables_.value());
487 for (BooleanVariable var(0); var < num_variables_; ++var) {
488 if (!debug_assignment_.VariableIsAssigned(var)) continue;
489 debug_assignment_.UnassignLiteral(Literal(var, true));
490 }
491 for (const Literal l : solution) {
492 debug_assignment_.AssignFromTrueLiteral(l);
493 }
494
495 // We should only call this with complete solution.
496 for (BooleanVariable var(0); var < num_variables_; ++var) {
497 CHECK(debug_assignment_.VariableIsAssigned(var));
498 }
499}
500
501void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) {
502 if (track_binary_clauses_) {
503 // Abort if this clause was already added.
504 if (!binary_clauses_.Add(BinaryClause(a, b))) return;
505 }
506
507 if (!binary_implication_graph_->AddBinaryClause(a, b)) {
508 CHECK_EQ(CurrentDecisionLevel(), 0);
509 SetModelUnsat();
510 }
511}
512
513bool SatSolver::ClauseIsValidUnderDebugAssignment(
514 absl::Span<const Literal> clause) const {
515 if (debug_assignment_.NumberOfVariables() == 0) return true;
516 for (Literal l : clause) {
517 if (l.Variable() >= debug_assignment_.NumberOfVariables() ||
518 debug_assignment_.LiteralIsTrue(l)) {
519 return true;
520 }
521 }
522 return false;
523}
524
525bool SatSolver::PBConstraintIsValidUnderDebugAssignment(
526 absl::Span<const LiteralWithCoeff> cst, const Coefficient rhs) const {
527 Coefficient sum(0.0);
528 for (LiteralWithCoeff term : cst) {
529 if (term.literal.Variable() >= debug_assignment_.NumberOfVariables()) {
530 continue;
531 }
532 if (debug_assignment_.LiteralIsTrue(term.literal)) {
533 sum += term.coefficient;
534 }
535 }
536 return sum <= rhs;
537}
538
539namespace {
540
541// Returns true iff 'b' is subsumed by 'a' (i.e 'a' is included in 'b').
542// This is slow and only meant to be used in DCHECKs.
543bool ClauseSubsumption(absl::Span<const Literal> a, SatClause* b) {
544 std::vector<Literal> superset(b->begin(), b->end());
545 std::vector<Literal> subset(a.begin(), a.end());
546 std::sort(superset.begin(), superset.end());
547 std::sort(subset.begin(), subset.end());
548 return std::includes(superset.begin(), superset.end(), subset.begin(),
549 subset.end());
550}
551
552} // namespace
553
555 SCOPED_TIME_STAT(&stats_);
556 if (model_is_unsat_) return kUnsatTrailIndex;
557 DCHECK(PropagationIsDone());
558
559 // We should never enqueue before the assumptions_.
560 if (DEBUG_MODE && !assumptions_.empty()) {
561 CHECK_GE(current_decision_level_, assumption_level_);
562 }
563
564 EnqueueNewDecision(true_literal);
565 if (!FinishPropagation()) return kUnsatTrailIndex;
566 return last_decision_or_backtrack_trail_index_;
567}
568
570 if (model_is_unsat_) return false;
571 if (CurrentDecisionLevel() > assumption_level_) {
572 Backtrack(assumption_level_);
573 return true;
574 }
575 if (!FinishPropagation()) return false;
577}
578
580 if (model_is_unsat_) return false;
581 int num_loop = 0;
582 while (true) {
583 const int old_decision_level = current_decision_level_;
584 if (!Propagate()) {
586 if (model_is_unsat_) return false;
587 if (current_decision_level_ == old_decision_level) {
588 CHECK(!assumptions_.empty());
589 return false;
590 }
591
592 if (++num_loop % 16 == 0 && time_limit_->LimitReached()) {
593 // TODO(user): Exiting like this might cause issue since the propagation
594 // is not "finished" but some code might assume it is. However since we
595 // already might repropagate in the LP constraint, most of the code
596 // should support "not finished propagation".
597 return true;
598 }
599 continue;
600 }
601 break;
602 }
603 DCHECK(PropagationIsDone());
604 return true;
605}
606
608 if (model_is_unsat_) return false;
609 assumption_level_ = 0;
610 assumptions_.clear();
611 Backtrack(0);
612 return FinishPropagation();
613}
614
616 const std::vector<Literal>& assumptions) {
617 if (!ResetToLevelZero()) return false;
618 if (assumptions.empty()) return true;
619
620 // For assumptions and core-based search, it is really important to add as
621 // many binary clauses as possible. This is because we do not wan to miss any
622 // early core of size 2.
624
625 DCHECK(assumptions_.empty());
626 assumption_level_ = 1;
627 assumptions_ = assumptions;
629}
630
631// Note that we do not count these as "branches" for a reporting purpose.
633 if (model_is_unsat_) return false;
634 if (CurrentDecisionLevel() >= assumption_level_) return true;
635
636 if (CurrentDecisionLevel() == 0 && !assumptions_.empty()) {
637 // When assumptions_ is not empty, the first "decision" actually contains
638 // multiple one, and we should never use its literal.
639 CHECK_EQ(current_decision_level_, 0);
640 last_decision_or_backtrack_trail_index_ = trail_->Index();
641 decisions_[0] = Decision(trail_->Index(), Literal());
642
643 ++current_decision_level_;
644 trail_->SetDecisionLevel(current_decision_level_);
645
646 // We enqueue all assumptions at once at decision level 1.
647 int num_decisions = 0;
648 for (const Literal lit : assumptions_) {
649 if (Assignment().LiteralIsTrue(lit)) continue;
650 if (Assignment().LiteralIsFalse(lit)) {
651 // See GetLastIncompatibleDecisions().
652 *trail_->MutableConflict() = {lit.Negated(), lit};
653 if (num_decisions == 0) {
654 // This is needed to avoid an empty level that cause some CHECK fail.
655 current_decision_level_ = 0;
656 trail_->SetDecisionLevel(0);
657 }
658 return false;
659 }
660 ++num_decisions;
661 trail_->EnqueueSearchDecision(lit);
662 }
663
664 // Corner case: all assumptions are fixed at level zero, we ignore them.
665 if (num_decisions == 0) {
666 current_decision_level_ = 0;
667 trail_->SetDecisionLevel(0);
668 return ResetToLevelZero();
669 }
670
671 // Now that everything is enqueued, we propagate.
672 return FinishPropagation();
673 }
674
675 DCHECK(assumptions_.empty());
676 const int64_t old_num_branches = counters_.num_branches;
677 const SatSolver::Status status = ReapplyDecisionsUpTo(assumption_level_ - 1);
678 counters_.num_branches = old_num_branches;
679 assumption_level_ = CurrentDecisionLevel();
680 return (status == SatSolver::FEASIBLE);
681}
682
684 SCOPED_TIME_STAT(&stats_);
685 if (model_is_unsat_) return;
686
687 ++counters_.num_failures;
688 const int conflict_trail_index = trail_->Index();
689 const int conflict_decision_level = current_decision_level_;
690
691 // A conflict occurred, compute a nice reason for this failure.
692 same_reason_identifier_.Clear();
693 const int max_trail_index = ComputeMaxTrailIndex(trail_->FailingClause());
694 if (!assumptions_.empty() && !trail_->FailingClause().empty()) {
695 // If the failing clause only contains literal at the assumptions level,
696 // we cannot use the ComputeFirstUIPConflict() code as we might have more
697 // than one decision.
698 //
699 // TODO(user): We might still want to "learn" the clause, especially if
700 // it reduces to only one literal in which case we can just fix it.
701 const int highest_level =
702 DecisionLevel((*trail_)[max_trail_index].Variable());
703 if (highest_level == 1) return;
704 }
705
706 ComputeFirstUIPConflict(max_trail_index, &learned_conflict_,
707 &reason_used_to_infer_the_conflict_,
708 &subsumed_clauses_);
709
710 // An empty conflict means that the problem is UNSAT.
711 if (learned_conflict_.empty()) return (void)SetModelUnsat();
712 DCHECK(IsConflictValid(learned_conflict_));
713 DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
714
715 // Update the activity of all the variables in the first UIP clause.
716 // Also update the activity of the last level variables expanded (and
717 // thus discarded) during the first UIP computation. Note that both
718 // sets are disjoint.
719 decision_policy_->BumpVariableActivities(learned_conflict_);
720 decision_policy_->BumpVariableActivities(reason_used_to_infer_the_conflict_);
721 if (parameters_->also_bump_variables_in_conflict_reasons()) {
722 ComputeUnionOfReasons(learned_conflict_, &extra_reason_literals_);
723 decision_policy_->BumpVariableActivities(extra_reason_literals_);
724 }
725
726 // Bump the clause activities.
727 // Note that the activity of the learned clause will be bumped too
728 // by AddLearnedClauseAndEnqueueUnitPropagation().
729 if (trail_->FailingSatClause() != nullptr) {
730 BumpClauseActivity(trail_->FailingSatClause());
731 }
732 BumpReasonActivities(reason_used_to_infer_the_conflict_);
733
734 // Decay the activities.
735 decision_policy_->UpdateVariableActivityIncrement();
736 UpdateClauseActivityIncrement();
737 pb_constraints_->UpdateActivityIncrement();
738
739 // Hack from Glucose that seems to perform well.
740 const int period = parameters_->glucose_decay_increment_period();
741 const double max_decay = parameters_->glucose_max_decay();
742 if (counters_.num_failures % period == 0 &&
743 parameters_->variable_activity_decay() < max_decay) {
744 parameters_->set_variable_activity_decay(
745 parameters_->variable_activity_decay() +
746 parameters_->glucose_decay_increment());
747 }
748
749 // PB resolution.
750 // There is no point using this if the conflict and all the reasons involved
751 // in its resolution were clauses.
752 bool compute_pb_conflict = false;
753 if (parameters_->use_pb_resolution()) {
754 compute_pb_conflict = (pb_constraints_->ConflictingConstraint() != nullptr);
755 if (!compute_pb_conflict) {
756 for (Literal lit : reason_used_to_infer_the_conflict_) {
757 if (ReasonPbConstraintOrNull(lit.Variable()) != nullptr) {
758 compute_pb_conflict = true;
759 break;
760 }
761 }
762 }
763 }
764
765 // TODO(user): Note that we use the clause above to update the variable
766 // activities and not the pb conflict. Experiment.
767 if (compute_pb_conflict) {
768 pb_conflict_.ClearAndResize(num_variables_.value());
769 Coefficient initial_slack(-1);
770 if (pb_constraints_->ConflictingConstraint() == nullptr) {
771 // Generic clause case.
772 Coefficient num_literals(0);
773 for (Literal literal : trail_->FailingClause()) {
774 pb_conflict_.AddTerm(literal.Negated(), Coefficient(1.0));
775 ++num_literals;
776 }
777 pb_conflict_.AddToRhs(num_literals - 1);
778 } else {
779 // We have a pseudo-Boolean conflict, so we start from there.
780 pb_constraints_->ConflictingConstraint()->AddToConflict(&pb_conflict_);
781 pb_constraints_->ClearConflictingConstraint();
782 initial_slack =
783 pb_conflict_.ComputeSlackForTrailPrefix(*trail_, max_trail_index + 1);
784 }
785
786 int pb_backjump_level;
787 ComputePBConflict(max_trail_index, initial_slack, &pb_conflict_,
788 &pb_backjump_level);
789 if (pb_backjump_level == -1) return (void)SetModelUnsat();
790
791 // Convert the conflict into the vector<LiteralWithCoeff> form.
792 std::vector<LiteralWithCoeff> cst;
793 pb_conflict_.CopyIntoVector(&cst);
794 DCHECK(PBConstraintIsValidUnderDebugAssignment(cst, pb_conflict_.Rhs()));
795
796 // Check if the learned PB conflict is just a clause:
797 // all its coefficient must be 1, and the rhs must be its size minus 1.
798 bool conflict_is_a_clause = (pb_conflict_.Rhs() == cst.size() - 1);
799 if (conflict_is_a_clause) {
800 for (LiteralWithCoeff term : cst) {
801 if (term.coefficient != Coefficient(1)) {
802 conflict_is_a_clause = false;
803 break;
804 }
805 }
806 }
807
808 if (!conflict_is_a_clause) {
809 // Use the PB conflict.
810 DCHECK_GT(pb_constraints_->NumberOfConstraints(), 0);
811 CHECK_LT(pb_backjump_level, CurrentDecisionLevel());
812 Backtrack(pb_backjump_level);
813 CHECK(pb_constraints_->AddLearnedConstraint(cst, pb_conflict_.Rhs(),
814 trail_));
815 CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_);
816 counters_.num_learned_pb_literals += cst.size();
817 return;
818 }
819
820 // Continue with the normal clause flow, but use the PB conflict clause
821 // if it has a lower backjump level.
822 if (pb_backjump_level < ComputeBacktrackLevel(learned_conflict_)) {
823 subsumed_clauses_.clear(); // Because the conflict changes.
824 learned_conflict_.clear();
825 is_marked_.ClearAndResize(num_variables_);
826 int max_level = 0;
827 int max_index = 0;
828 for (LiteralWithCoeff term : cst) {
829 DCHECK(Assignment().LiteralIsTrue(term.literal));
830 DCHECK_EQ(term.coefficient, 1);
831 const int level = trail_->Info(term.literal.Variable()).level;
832 if (level == 0) continue;
833 if (level > max_level) {
834 max_level = level;
835 max_index = learned_conflict_.size();
836 }
837 learned_conflict_.push_back(term.literal.Negated());
838
839 // The minimization functions below expect the conflict to be marked!
840 // TODO(user): This is error prone, find a better way?
841 is_marked_.Set(term.literal.Variable());
842 }
843 CHECK(!learned_conflict_.empty());
844 std::swap(learned_conflict_.front(), learned_conflict_[max_index]);
845 DCHECK(IsConflictValid(learned_conflict_));
846 }
847 }
848
849 // Minimizing the conflict with binary clauses first has two advantages.
850 // First, there is no need to compute a reason for the variables eliminated
851 // this way. Second, more variables may be marked (in is_marked_) and
852 // MinimizeConflict() can take advantage of that. Because of this, the
853 // LBD of the learned conflict can change.
854 DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
855 if (!binary_implication_graph_->IsEmpty()) {
856 if (parameters_->binary_minimization_algorithm() ==
857 SatParameters::BINARY_MINIMIZATION_FIRST) {
858 binary_implication_graph_->MinimizeConflictFirst(
859 *trail_, &learned_conflict_, &is_marked_);
860 } else if (parameters_->binary_minimization_algorithm() ==
861 SatParameters::
862 BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION) {
863 binary_implication_graph_->MinimizeConflictFirstWithTransitiveReduction(
864 *trail_, &learned_conflict_,
865 *model_->GetOrCreate<ModelRandomGenerator>());
866 }
867 DCHECK(IsConflictValid(learned_conflict_));
868 }
869
870 // Minimize the learned conflict.
871 MinimizeConflict(&learned_conflict_);
872
873 // Minimize it further with binary clauses?
874 if (!binary_implication_graph_->IsEmpty()) {
875 // Note that on the contrary to the MinimizeConflict() above that
876 // just uses the reason graph, this minimization can change the
877 // clause LBD and even the backtracking level.
878 switch (parameters_->binary_minimization_algorithm()) {
879 case SatParameters::NO_BINARY_MINIMIZATION:
880 ABSL_FALLTHROUGH_INTENDED;
881 case SatParameters::BINARY_MINIMIZATION_FIRST:
882 ABSL_FALLTHROUGH_INTENDED;
883 case SatParameters::BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION:
884 break;
885 case SatParameters::BINARY_MINIMIZATION_WITH_REACHABILITY:
886 binary_implication_graph_->MinimizeConflictWithReachability(
887 &learned_conflict_);
888 break;
889 case SatParameters::EXPERIMENTAL_BINARY_MINIMIZATION:
890 binary_implication_graph_->MinimizeConflictExperimental(
891 *trail_, &learned_conflict_);
892 break;
893 }
894 DCHECK(IsConflictValid(learned_conflict_));
895 }
896
897 // We notify the decision before backtracking so that we can save the phase.
898 // The current heuristic is to try to take a trail prefix for which there is
899 // currently no conflict (hence just before the last decision was taken).
900 //
901 // TODO(user): It is unclear what the best heuristic is here. Both the current
902 // trail index or the trail before the current decision perform well, but
903 // using the full trail seems slightly better even though it will contain the
904 // current conflicting literal.
905 decision_policy_->BeforeConflict(trail_->Index());
906
907 // Backtrack and add the reason to the set of learned clause.
908 counters_.num_literals_learned += learned_conflict_.size();
909 Backtrack(ComputeBacktrackLevel(learned_conflict_));
910 DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
911
912 // Note that we need to output the learned clause before cleaning the clause
913 // database. This is because we already backtracked and some of the clauses
914 // that were needed to infer the conflict may not be "reasons" anymore and
915 // may be deleted.
916 if (drat_proof_handler_ != nullptr) {
917 drat_proof_handler_->AddClause(learned_conflict_);
918 }
919
920 // Because we might change the conflict with this minimization algorithm, we
921 // cannot just subsume clauses with it blindly.
922 //
923 // TODO(user): Either remove that algorithm or support subsumption by just
924 // checking if it is okay to do so, or doing it on the fly while computing the
925 // first UIP.
926 if (parameters_->minimization_algorithm() == SatParameters::EXPERIMENTAL) {
927 subsumed_clauses_.clear();
928 }
929
930 // Detach any subsumed clause. They will actually be deleted on the next
931 // clause cleanup phase.
932 bool is_redundant = true;
933 if (!subsumed_clauses_.empty() &&
934 parameters_->subsumption_during_conflict_analysis()) {
935 for (SatClause* clause : subsumed_clauses_) {
936 DCHECK(ClauseSubsumption(learned_conflict_, clause));
937 if (!clauses_propagator_->IsRemovable(clause)) {
938 is_redundant = false;
939 }
940 clauses_propagator_->LazyDetach(clause);
941 }
942 clauses_propagator_->CleanUpWatchers();
943 counters_.num_subsumed_clauses += subsumed_clauses_.size();
944 }
945
946 // Create and attach the new learned clause.
947 const int conflict_lbd = AddLearnedClauseAndEnqueueUnitPropagation(
948 learned_conflict_, is_redundant);
949 restart_->OnConflict(conflict_trail_index, conflict_decision_level,
950 conflict_lbd);
951}
952
953SatSolver::Status SatSolver::ReapplyDecisionsUpTo(
954 int max_level, int* first_propagation_index) {
955 SCOPED_TIME_STAT(&stats_);
956 DCHECK(assumptions_.empty());
957 int decision_index = current_decision_level_;
958 while (decision_index <= max_level) {
959 DCHECK_GE(decision_index, current_decision_level_);
960 const Literal previous_decision = decisions_[decision_index].literal;
961 ++decision_index;
962 if (Assignment().LiteralIsTrue(previous_decision)) {
963 // Note that this particular position in decisions_ will be overridden,
964 // but that is fine since this is a consequence of the previous decision,
965 // so we will never need to take it into account again.
966 continue;
967 }
968 if (Assignment().LiteralIsFalse(previous_decision)) {
969 // See GetLastIncompatibleDecisions().
970 *trail_->MutableConflict() = {previous_decision.Negated(),
971 previous_decision};
972 return ASSUMPTIONS_UNSAT;
973 }
974
975 // Not assigned, we try to take it.
976 const int old_level = current_decision_level_;
977 const int index = EnqueueDecisionAndBackjumpOnConflict(previous_decision);
978 if (first_propagation_index != nullptr) {
979 *first_propagation_index = std::min(*first_propagation_index, index);
980 }
981 if (index == kUnsatTrailIndex) return INFEASIBLE;
982 if (current_decision_level_ <= old_level) {
983 // A conflict occurred which backjumped to an earlier decision level.
984 // We potentially backjumped over some valid decisions, so we need to
985 // continue the loop and try to re-enqueue them.
986 //
987 // Note that there is no need to update max_level, because when we will
988 // try to reapply the current "previous_decision" it will result in a
989 // conflict. IMPORTANT: we can't actually optimize this and abort the loop
990 // earlier though, because we need to check that it is conflicting because
991 // it is already propagated to false. There is no guarantee of this
992 // because we learn the first-UIP conflict. If it is not the case, we will
993 // then learn a new conflict, backjump, and continue the loop.
994 decision_index = current_decision_level_;
995 }
996 }
997 return FEASIBLE;
998}
999
1001 Literal true_literal, int* first_propagation_index) {
1002 SCOPED_TIME_STAT(&stats_);
1003 CHECK(PropagationIsDone());
1004 CHECK(assumptions_.empty());
1005 if (model_is_unsat_) return SatSolver::INFEASIBLE;
1006 DCHECK_LT(CurrentDecisionLevel(), decisions_.size());
1007 decisions_[CurrentDecisionLevel()].literal = true_literal;
1008 if (first_propagation_index != nullptr) {
1009 *first_propagation_index = trail_->Index();
1010 }
1011 return ReapplyDecisionsUpTo(CurrentDecisionLevel(), first_propagation_index);
1012}
1013
1015 SCOPED_TIME_STAT(&stats_);
1016 DCHECK(PropagationIsDone());
1017
1018 if (model_is_unsat_) return kUnsatTrailIndex;
1019 const int current_level = CurrentDecisionLevel();
1020 EnqueueNewDecision(true_literal);
1021 if (Propagate()) {
1022 return true;
1023 } else {
1024 Backtrack(current_level);
1025 return false;
1026 }
1027}
1028
1029void SatSolver::Backtrack(int target_level) {
1030 SCOPED_TIME_STAT(&stats_);
1031 // TODO(user): The backtrack method should not be called when the model is
1032 // unsat. Add a DCHECK to prevent that, but before fix the
1033 // bop::BopOptimizerBase architecture.
1034
1035 // Do nothing if the CurrentDecisionLevel() is already correct.
1036 // This is needed, otherwise target_trail_index below will remain at zero and
1037 // that will cause some problems. Note that we could forbid a user to call
1038 // Backtrack() with the current level, but that is annoying when you just
1039 // want to reset the solver with Backtrack(0).
1040 DCHECK(target_level == 0 || !Decisions().empty());
1041 if (CurrentDecisionLevel() == target_level || Decisions().empty()) return;
1042 DCHECK_GE(target_level, 0);
1043 DCHECK_LE(target_level, CurrentDecisionLevel());
1044
1045 // Any backtrack to the root from a positive one is counted as a restart.
1046 counters_.num_backtracks++;
1047 if (target_level == 0) counters_.num_restarts++;
1048
1049 // Per the SatPropagator interface, this is needed before calling Untrail.
1050 trail_->SetDecisionLevel(target_level);
1051
1052 current_decision_level_ = target_level;
1053 const int target_trail_index =
1054 decisions_[current_decision_level_].trail_index;
1055
1056 DCHECK_LT(target_trail_index, trail_->Index());
1057 for (SatPropagator* propagator : propagators_) {
1058 if (propagator->IsEmpty()) continue;
1059 propagator->Untrail(*trail_, target_trail_index);
1060 }
1061 decision_policy_->Untrail(target_trail_index);
1062 trail_->Untrail(target_trail_index);
1063
1064 last_decision_or_backtrack_trail_index_ = trail_->Index();
1065}
1066
1067bool SatSolver::AddBinaryClauses(absl::Span<const BinaryClause> clauses) {
1068 SCOPED_TIME_STAT(&stats_);
1069 CHECK_EQ(CurrentDecisionLevel(), 0);
1070 for (const BinaryClause c : clauses) {
1071 if (!AddBinaryClause(c.a, c.b)) return false;
1072 }
1073 if (!Propagate()) return SetModelUnsat();
1074 return true;
1075}
1076
1077const std::vector<BinaryClause>& SatSolver::NewlyAddedBinaryClauses() {
1078 return binary_clauses_.newly_added();
1079}
1080
1082 binary_clauses_.ClearNewlyAdded();
1083}
1084
1085namespace {
1086// Return the next value that is a multiple of interval.
1087int64_t NextMultipleOf(int64_t value, int64_t interval) {
1088 return interval * (1 + value / interval);
1089}
1090} // namespace
1091
1093 const std::vector<Literal>& assumptions, int64_t max_number_of_conflicts) {
1094 SCOPED_TIME_STAT(&stats_);
1095 if (!ResetWithGivenAssumptions(assumptions)) return UnsatStatus();
1096 return SolveInternal(time_limit_,
1097 max_number_of_conflicts >= 0
1098 ? max_number_of_conflicts
1099 : parameters_->max_number_of_conflicts());
1100}
1101
1102SatSolver::Status SatSolver::StatusWithLog(Status status) {
1103 SOLVER_LOG(logger_, RunningStatisticsString());
1104 SOLVER_LOG(logger_, StatusString(status));
1105 return status;
1106}
1107
1108void SatSolver::SetAssumptionLevel(int assumption_level) {
1109 CHECK_GE(assumption_level, 0);
1110 CHECK_LE(assumption_level, CurrentDecisionLevel());
1111 assumption_level_ = assumption_level;
1112
1113 // New assumption code.
1114 if (!assumptions_.empty()) {
1115 CHECK_EQ(assumption_level, 0);
1116 assumptions_.clear();
1117 }
1118}
1119
1121 return SolveInternal(time_limit == nullptr ? time_limit_ : time_limit,
1122 parameters_->max_number_of_conflicts());
1123}
1124
1126 return SolveInternal(time_limit_, parameters_->max_number_of_conflicts());
1127}
1128
1129void SatSolver::KeepAllClausesUsedToInfer(BooleanVariable variable) {
1130 CHECK(Assignment().VariableIsAssigned(variable));
1131 if (trail_->Info(variable).level == 0) return;
1132 int trail_index = trail_->Info(variable).trail_index;
1133 std::vector<bool> is_marked(trail_index + 1, false); // move to local member.
1134 is_marked[trail_index] = true;
1135 int num = 1;
1136 for (; num > 0 && trail_index >= 0; --trail_index) {
1137 if (!is_marked[trail_index]) continue;
1138 is_marked[trail_index] = false;
1139 --num;
1140
1141 const BooleanVariable var = (*trail_)[trail_index].Variable();
1142 SatClause* clause = ReasonClauseOrNull(var);
1143 if (clause != nullptr) {
1144 // Keep this clause.
1145 clauses_propagator_->mutable_clauses_info()->erase(clause);
1146 }
1147 if (trail_->AssignmentType(var) == AssignmentType::kSearchDecision) {
1148 continue;
1149 }
1150 for (const Literal l : trail_->Reason(var)) {
1151 const AssignmentInfo& info = trail_->Info(l.Variable());
1152 if (info.level == 0) continue;
1153 if (!is_marked[info.trail_index]) {
1154 is_marked[info.trail_index] = true;
1155 ++num;
1156 }
1157 }
1158 }
1159}
1160
1161bool SatSolver::SubsumptionIsInteresting(BooleanVariable variable,
1162 int max_size) {
1163 // TODO(user): other id should probably be safe as long as we do not delete
1164 // the propagators. Note that symmetry is tricky since we would need to keep
1165 // the symmetric clause around in KeepAllClauseUsedToInfer().
1166 const int binary_id = binary_implication_graph_->PropagatorId();
1167 const int clause_id = clauses_propagator_->PropagatorId();
1168
1169 CHECK(Assignment().VariableIsAssigned(variable));
1170 if (trail_->Info(variable).level == 0) return true;
1171 int trail_index = trail_->Info(variable).trail_index;
1172 std::vector<bool> is_marked(trail_index + 1, false); // move to local member.
1173 is_marked[trail_index] = true;
1174 int num = 1;
1175 int num_clause_to_mark_as_non_deletable = 0;
1176 for (; num > 0 && trail_index >= 0; --trail_index) {
1177 if (!is_marked[trail_index]) continue;
1178 is_marked[trail_index] = false;
1179 --num;
1180
1181 const BooleanVariable var = (*trail_)[trail_index].Variable();
1182 const int type = trail_->AssignmentType(var);
1183 if (type == AssignmentType::kSearchDecision) continue;
1184 if (type != binary_id && type != clause_id) return false;
1185 SatClause* clause = ReasonClauseOrNull(var);
1186 if (clause != nullptr && clauses_propagator_->IsRemovable(clause)) {
1187 if (clause->size() > max_size) {
1188 return false;
1189 }
1190 if (++num_clause_to_mark_as_non_deletable > 1) return false;
1191 }
1192 for (const Literal l : trail_->Reason(var)) {
1193 const AssignmentInfo& info = trail_->Info(l.Variable());
1194 if (info.level == 0) continue;
1195 if (!is_marked[info.trail_index]) {
1196 is_marked[info.trail_index] = true;
1197 ++num;
1198 }
1199 }
1200 }
1201 return num_clause_to_mark_as_non_deletable <= 1;
1202}
1203
1204// TODO(user): this is really an in-processing stuff and should be moved out
1205// of here. Ideally this should be scheduled after other faster in-processing
1206// techniques. This implements "vivification" as described in
1207// https://doi.org/10.1016/j.artint.2019.103197, with one significant tweak:
1208// we sort each clause by current trail index before trying to minimize it so
1209// that we can reuse the trail from previous calls in case there are overlaps.
1210void SatSolver::TryToMinimizeClause(SatClause* clause) {
1211 CHECK(clause != nullptr);
1212 ++counters_.minimization_num_clauses;
1213
1214 std::vector<Literal> candidate;
1215 candidate.reserve(clause->size());
1216
1217 // Note that CP-SAT presolve detects clauses that share n-1 literals and
1218 // transforms them into (n-1 enforcement) => (1 literal per clause). We
1219 // currently do not support that internally, but these clauses will still
1220 // likely be loaded one after the other, so there is a high chance that if we
1221 // call TryToMinimizeClause() on consecutive clauses, there will be a long
1222 // prefix in common!
1223 //
1224 // TODO(user): Exploit this more by choosing a good minimization order?
1225 int longest_valid_prefix = 0;
1226 if (CurrentDecisionLevel() > 0) {
1227 candidate.resize(clause->size());
1228 // Insert any compatible decisions into their correct place in candidate
1229 for (Literal lit : *clause) {
1230 if (!Assignment().LiteralIsFalse(lit)) continue;
1231 const AssignmentInfo& info = trail_->Info(lit.Variable());
1232 if (info.level <= 0 || info.level > clause->size()) continue;
1233 if (decisions_[info.level - 1].literal == lit.Negated()) {
1234 candidate[info.level - 1] = lit;
1235 }
1236 }
1237 // Then compute the matching prefix and discard the rest
1238 for (int i = 0; i < candidate.size(); ++i) {
1239 if (candidate[i] != Literal()) {
1240 ++longest_valid_prefix;
1241 } else {
1242 break;
1243 }
1244 }
1245 counters_.minimization_num_reused += longest_valid_prefix;
1246 candidate.resize(longest_valid_prefix);
1247 }
1248 // Then do a second pass to add the remaining literals in order.
1249 for (Literal lit : *clause) {
1250 const AssignmentInfo& info = trail_->Info(lit.Variable());
1251 // Skip if this literal is already in the prefix.
1252 if (info.level >= 1 && info.level <= longest_valid_prefix &&
1253 candidate[info.level - 1] == lit) {
1254 continue;
1255 }
1256 candidate.push_back(lit);
1257 }
1258 CHECK_EQ(candidate.size(), clause->size());
1259
1260 Backtrack(longest_valid_prefix);
1261 absl::btree_set<LiteralIndex> moved_last;
1262 while (!model_is_unsat_) {
1263 // We want each literal in candidate to appear last once in our propagation
1264 // order. We want to do that while maximizing the reutilization of the
1265 // current assignment prefix, that is minimizing the number of
1266 // decision/progagation we need to perform.
1267 const int target_level = MoveOneUnprocessedLiteralLast(
1268 moved_last, CurrentDecisionLevel(), &candidate);
1269 if (target_level == -1) break;
1270 Backtrack(target_level);
1271
1272 while (CurrentDecisionLevel() < candidate.size()) {
1273 if (time_limit_->LimitReached()) return;
1274 const int level = CurrentDecisionLevel();
1275 const Literal literal = candidate[level];
1276 // Remove false literals
1277 if (Assignment().LiteralIsFalse(literal)) {
1278 candidate[level] = candidate.back();
1279 candidate.pop_back();
1280 continue;
1281 } else if (Assignment().LiteralIsTrue(literal)) {
1282 const int variable_level =
1283 LiteralTrail().Info(literal.Variable()).level;
1284 if (variable_level == 0) {
1285 ProcessNewlyFixedVariablesForDratProof();
1286 counters_.minimization_num_true++;
1287 counters_.minimization_num_removed_literals += clause->size();
1288 Backtrack(0);
1289 clauses_propagator_->Detach(clause);
1290 return;
1291 }
1292
1293 if (parameters_->inprocessing_minimization_use_conflict_analysis()) {
1294 // Replace the clause with the reason for the literal being true, plus
1295 // the literal itself.
1296 candidate.clear();
1297 for (Literal lit :
1298 GetDecisionsFixing(trail_->Reason(literal.Variable()))) {
1299 candidate.push_back(lit.Negated());
1300 }
1301 } else {
1302 candidate.resize(variable_level);
1303 }
1304 candidate.push_back(literal);
1305
1306 // If a (true) literal wasn't propagated by this clause, then we know
1307 // that this clause is subsumed by other clauses in the database, so we
1308 // can remove it so long as the subsumption is due to non-removable
1309 // clauses. If we can subsume this clause by making only 1 additional
1310 // clause permanent and that clause is no longer than this one, we will
1311 // do so.
1312 if (ReasonClauseOrNull(literal.Variable()) != clause &&
1313 SubsumptionIsInteresting(literal.Variable(), candidate.size())) {
1314 counters_.minimization_num_subsumed++;
1315 counters_.minimization_num_removed_literals += clause->size();
1316 KeepAllClausesUsedToInfer(literal.Variable());
1317 Backtrack(0);
1318 clauses_propagator_->Detach(clause);
1319 return;
1320 }
1321
1322 break;
1323 } else {
1324 ++counters_.minimization_num_decisions;
1325 EnqueueDecisionAndBackjumpOnConflict(literal.Negated());
1326 if (clause->IsRemoved()) {
1327 Backtrack(0);
1328 return;
1329 }
1330 if (model_is_unsat_) return;
1331 if (CurrentDecisionLevel() < level) {
1332 // There was a conflict, consider the conflicting literal next so we
1333 // should be able to exploit the conflict in the next iteration.
1334 // TODO(user): I *think* this is sufficient to ensure pushing
1335 // the same literal to the new trail fails, immediately on the next
1336 // iteration, if not we may be able to analyse the last failure and
1337 // skip some propagation steps?
1338 std::swap(candidate[level], candidate[CurrentDecisionLevel()]);
1339 }
1340 }
1341 }
1342 if (candidate.empty()) {
1343 model_is_unsat_ = true;
1344 return;
1345 }
1346 if (!parameters_->inprocessing_minimization_use_all_orderings()) break;
1347 moved_last.insert(candidate.back().Index());
1348 }
1349
1350 if (candidate.empty()) {
1351 model_is_unsat_ = true;
1352 return;
1353 }
1354
1355 // Returns if we don't have any minimization.
1356 if (candidate.size() == clause->size()) return;
1357 Backtrack(0);
1358
1359 if (candidate.size() == 1) {
1360 if (drat_proof_handler_ != nullptr) {
1361 drat_proof_handler_->AddClause(candidate);
1362 }
1363 if (!Assignment().VariableIsAssigned(candidate[0].Variable())) {
1364 counters_.minimization_num_removed_literals += clause->size();
1365 trail_->EnqueueWithUnitReason(candidate[0]);
1366 return (void)FinishPropagation();
1367 }
1368 return;
1369 }
1370
1371 if (candidate.size() == 2) {
1372 counters_.minimization_num_removed_literals += clause->size() - 2;
1373
1374 // The order is important for the drat proof.
1375 AddBinaryClauseInternal(candidate[0], candidate[1]);
1376 clauses_propagator_->Detach(clause);
1377
1378 // This is needed in the corner case where this was the first binary clause
1379 // of the problem so that PropagationIsDone() returns true on the newly
1380 // created BinaryImplicationGraph.
1381 return (void)FinishPropagation();
1382 }
1383
1384 counters_.minimization_num_removed_literals +=
1385 clause->size() - candidate.size();
1386
1387 // TODO(user): If the watched literal didn't change, we could just rewrite
1388 // the clause while keeping the two watched literals at the beginning.
1389 if (!clauses_propagator_->InprocessingRewriteClause(clause, candidate)) {
1390 model_is_unsat_ = true;
1391 }
1392}
1393
1394SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit,
1395 int64_t max_number_of_conflicts) {
1396 SCOPED_TIME_STAT(&stats_);
1397 if (model_is_unsat_) return INFEASIBLE;
1398
1399 // TODO(user): Because the counter are not reset to zero, this cause the
1400 // metrics / sec to be completely broken except when the solver is used
1401 // for exactly one Solve().
1402 timer_.Restart();
1403
1404 // Display initial statistics.
1405 if (logger_->LoggingIsEnabled()) {
1406 SOLVER_LOG(logger_, "Initial memory usage: ", MemoryUsage());
1407 SOLVER_LOG(logger_, "Number of variables: ", num_variables_.value());
1408 SOLVER_LOG(logger_, "Number of clauses (size > 2): ",
1409 clauses_propagator_->num_clauses());
1410 SOLVER_LOG(logger_, "Number of binary clauses: ",
1411 binary_implication_graph_->ComputeNumImplicationsForLog());
1412 SOLVER_LOG(logger_, "Number of linear constraints: ",
1413 pb_constraints_->NumberOfConstraints());
1414 SOLVER_LOG(logger_, "Number of fixed variables: ", trail_->Index());
1415 SOLVER_LOG(logger_, "Number of watched clauses: ",
1416 clauses_propagator_->num_watched_clauses());
1417 SOLVER_LOG(logger_, "Parameters: ", ProtobufShortDebugString(*parameters_));
1418 }
1419
1420 // Variables used to show the search progress.
1421 const int64_t kDisplayFrequency = 10000;
1422 int64_t next_display = parameters_->log_search_progress()
1423 ? NextMultipleOf(num_failures(), kDisplayFrequency)
1424 : std::numeric_limits<int64_t>::max();
1425
1426 // Variables used to check the memory limit every kMemoryCheckFrequency.
1427 const int64_t kMemoryCheckFrequency = 10000;
1428 int64_t next_memory_check =
1429 NextMultipleOf(num_failures(), kMemoryCheckFrequency);
1430
1431 // The max_number_of_conflicts is per solve but the counter is for the whole
1432 // solver.
1433 const int64_t kFailureLimit =
1434 max_number_of_conflicts == std::numeric_limits<int64_t>::max()
1435 ? std::numeric_limits<int64_t>::max()
1436 : counters_.num_failures + max_number_of_conflicts;
1437
1438 // Starts search.
1439 for (;;) {
1440 // Test if a limit is reached.
1441 if (time_limit != nullptr) {
1443 if (time_limit->LimitReached()) {
1444 SOLVER_LOG(logger_, "The time limit has been reached. Aborting.");
1445 return StatusWithLog(LIMIT_REACHED);
1446 }
1447 }
1448 if (num_failures() >= kFailureLimit) {
1449 SOLVER_LOG(logger_, "The conflict limit has been reached. Aborting.");
1450 return StatusWithLog(LIMIT_REACHED);
1451 }
1452
1453 // The current memory checking takes time, so we only execute it every
1454 // kMemoryCheckFrequency conflict. We use >= because counters_.num_failures
1455 // may augment by more than one at each iteration.
1456 //
1457 // TODO(user): Find a better way.
1458 if (counters_.num_failures >= next_memory_check) {
1459 next_memory_check = NextMultipleOf(num_failures(), kMemoryCheckFrequency);
1460 if (IsMemoryLimitReached()) {
1461 SOLVER_LOG(logger_, "The memory limit has been reached. Aborting.");
1462 return StatusWithLog(LIMIT_REACHED);
1463 }
1464 }
1465
1466 // Display search progression. We use >= because counters_.num_failures may
1467 // augment by more than one at each iteration.
1468 if (counters_.num_failures >= next_display) {
1469 SOLVER_LOG(logger_, RunningStatisticsString());
1470 next_display = NextMultipleOf(num_failures(), kDisplayFrequency);
1471 }
1472
1473 const int old_level = current_decision_level_;
1474 if (!Propagate()) {
1475 // A conflict occurred, continue the loop.
1477 if (model_is_unsat_) return StatusWithLog(INFEASIBLE);
1478 if (old_level == current_decision_level_) {
1479 CHECK(!assumptions_.empty());
1480 return StatusWithLog(ASSUMPTIONS_UNSAT);
1481 }
1482 } else {
1483 // We need to reapply any assumptions that are not currently applied.
1484 if (!ReapplyAssumptionsIfNeeded()) return StatusWithLog(UnsatStatus());
1485
1486 // At a leaf?
1487 if (trail_->Index() == num_variables_.value()) {
1488 return StatusWithLog(FEASIBLE);
1489 }
1490
1491 if (restart_->ShouldRestart()) {
1492 Backtrack(assumption_level_);
1493 }
1494
1495 DCHECK_GE(CurrentDecisionLevel(), assumption_level_);
1496 EnqueueNewDecision(decision_policy_->NextBranch());
1497 }
1498 }
1499}
1500
1502 bool minimize_new_clauses_only) {
1503 CHECK(time_limit_ != nullptr);
1504 AdvanceDeterministicTime(time_limit_);
1505 const double threshold = time_limit_->GetElapsedDeterministicTime() + dtime;
1506
1507 // Tricky: we don't want TryToMinimizeClause() to delete to_minimize
1508 // while we are processing it.
1509 block_clause_deletion_ = true;
1510
1511 int num_resets = 0;
1512 while (!time_limit_->LimitReached() &&
1513 time_limit_->GetElapsedDeterministicTime() < threshold) {
1514 SatClause* to_minimize = clauses_propagator_->NextNewClauseToMinimize();
1515 if (!minimize_new_clauses_only && to_minimize == nullptr) {
1516 to_minimize = clauses_propagator_->NextClauseToMinimize();
1517 }
1518
1519 if (to_minimize != nullptr) {
1520 TryToMinimizeClause(to_minimize);
1521 if (model_is_unsat_) return false;
1522 } else if (minimize_new_clauses_only) {
1523 break;
1524 } else {
1525 ++num_resets;
1526 VLOG(1) << "Minimized all clauses, restarting from first one.";
1527 clauses_propagator_->ResetToMinimizeIndex();
1528 if (num_resets > 1) break;
1529 }
1530
1531 AdvanceDeterministicTime(time_limit_);
1532 }
1533
1534 // Note(user): In some corner cases, the function above might find a
1535 // feasible assignment. I think it is okay to ignore this special case
1536 // that should only happen on trivial problems and just reset the solver.
1537 const bool result = ResetToLevelZero();
1538
1539 block_clause_deletion_ = false;
1540 clauses_propagator_->DeleteRemovedClauses();
1541 return result;
1542}
1543
1545 std::vector<Literal>* clause = trail_->MutableConflict();
1546 int num_true = 0;
1547 for (int i = 0; i < clause->size(); ++i) {
1548 const Literal literal = (*clause)[i];
1549 if (Assignment().LiteralIsTrue(literal)) {
1550 // literal at true in the conflict must be the last decision/assumption
1551 // that could not be taken. Put it at the front to add to the result
1552 // later.
1553 std::swap((*clause)[i], (*clause)[num_true++]);
1554 }
1555 }
1556 CHECK_LE(num_true, 1);
1557 std::vector<Literal> result =
1558 GetDecisionsFixing(absl::MakeConstSpan(*clause).subspan(num_true));
1559 for (int i = 0; i < num_true; ++i) {
1560 result.push_back((*clause)[i].Negated());
1561 }
1562 return result;
1563}
1564
1566 absl::Span<const Literal> literals) {
1567 SCOPED_TIME_STAT(&stats_);
1568 std::vector<Literal> unsat_assumptions;
1569
1570 is_marked_.ClearAndResize(num_variables_);
1571
1572 int trail_index = 0;
1573 for (const Literal lit : literals) {
1574 CHECK(Assignment().LiteralIsAssigned(lit));
1575 trail_index =
1576 std::max(trail_index, trail_->Info(lit.Variable()).trail_index);
1577 is_marked_.Set(lit.Variable());
1578 }
1579
1580 // We just expand the conflict until we only have decisions.
1581 const int limit =
1582 CurrentDecisionLevel() > 0 ? decisions_[0].trail_index : trail_->Index();
1583 CHECK_LT(trail_index, trail_->Index());
1584 while (true) {
1585 // Find next marked literal to expand from the trail.
1586 while (trail_index >= limit &&
1587 !is_marked_[(*trail_)[trail_index].Variable()]) {
1588 --trail_index;
1589 }
1590 if (trail_index < limit) break;
1591 const Literal marked_literal = (*trail_)[trail_index];
1592 --trail_index;
1593
1594 if (trail_->AssignmentType(marked_literal.Variable()) ==
1596 unsat_assumptions.push_back(marked_literal);
1597 } else {
1598 // Marks all the literals of its reason.
1599 for (const Literal literal : trail_->Reason(marked_literal.Variable())) {
1600 const BooleanVariable var = literal.Variable();
1601 const int level = DecisionLevel(var);
1602 if (level > 0 && !is_marked_[var]) is_marked_.Set(var);
1603 }
1604 }
1605 }
1606
1607 // We reverse the assumptions so they are in the same order as the one in
1608 // which the decision were made.
1609 std::reverse(unsat_assumptions.begin(), unsat_assumptions.end());
1610 return unsat_assumptions;
1611}
1612
1613void SatSolver::BumpReasonActivities(absl::Span<const Literal> literals) {
1614 SCOPED_TIME_STAT(&stats_);
1615 for (const Literal literal : literals) {
1616 const BooleanVariable var = literal.Variable();
1617 if (DecisionLevel(var) > 0) {
1618 SatClause* clause = ReasonClauseOrNull(var);
1619 if (clause != nullptr) {
1620 BumpClauseActivity(clause);
1621 } else {
1622 UpperBoundedLinearConstraint* pb_constraint =
1623 ReasonPbConstraintOrNull(var);
1624 if (pb_constraint != nullptr) {
1625 // TODO(user): Because one pb constraint may propagate many literals,
1626 // this may bias the constraint activity... investigate other policy.
1627 pb_constraints_->BumpActivity(pb_constraint);
1628 }
1629 }
1630 }
1631 }
1632}
1633
1634void SatSolver::BumpClauseActivity(SatClause* clause) {
1635 // We only bump the activity of the clauses that have some info. So if we know
1636 // that we will keep a clause forever, we don't need to create its Info. More
1637 // than the speed, this allows to limit as much as possible the activity
1638 // rescaling.
1639 auto it = clauses_propagator_->mutable_clauses_info()->find(clause);
1640 if (it == clauses_propagator_->mutable_clauses_info()->end()) return;
1641
1642 // Check if the new clause LBD is below our threshold to keep this clause
1643 // indefinitely. Note that we use a +1 here because the LBD of a newly learned
1644 // clause decrease by 1 just after the backjump.
1645 const int new_lbd = ComputeLbd(*clause);
1646 if (new_lbd + 1 <= parameters_->clause_cleanup_lbd_bound()) {
1647 clauses_propagator_->mutable_clauses_info()->erase(clause);
1648 return;
1649 }
1650
1651 // Eventually protect this clause for the next cleanup phase.
1652 switch (parameters_->clause_cleanup_protection()) {
1653 case SatParameters::PROTECTION_NONE:
1654 break;
1655 case SatParameters::PROTECTION_ALWAYS:
1656 it->second.protected_during_next_cleanup = true;
1657 break;
1658 case SatParameters::PROTECTION_LBD:
1659 // This one is similar to the one used by the Glucose SAT solver.
1660 //
1661 // TODO(user): why the +1? one reason may be that the LBD of a conflict
1662 // decrease by 1 just after the backjump...
1663 if (new_lbd + 1 < it->second.lbd) {
1664 it->second.protected_during_next_cleanup = true;
1665 it->second.lbd = new_lbd;
1666 }
1667 }
1668
1669 // Increase the activity.
1670 const double activity = it->second.activity += clause_activity_increment_;
1671 if (activity > parameters_->max_clause_activity_value()) {
1672 RescaleClauseActivities(1.0 / parameters_->max_clause_activity_value());
1673 }
1674}
1675
1676void SatSolver::RescaleClauseActivities(double scaling_factor) {
1677 SCOPED_TIME_STAT(&stats_);
1678 clause_activity_increment_ *= scaling_factor;
1679 for (auto& entry : *clauses_propagator_->mutable_clauses_info()) {
1680 entry.second.activity *= scaling_factor;
1681 }
1682}
1683
1684void SatSolver::UpdateClauseActivityIncrement() {
1685 SCOPED_TIME_STAT(&stats_);
1686 clause_activity_increment_ *= 1.0 / parameters_->clause_activity_decay();
1687}
1688
1689bool SatSolver::IsConflictValid(absl::Span<const Literal> literals) {
1690 SCOPED_TIME_STAT(&stats_);
1691 if (literals.empty()) return false;
1692 const int highest_level = DecisionLevel(literals[0].Variable());
1693 for (int i = 1; i < literals.size(); ++i) {
1694 const int level = DecisionLevel(literals[i].Variable());
1695 if (level <= 0 || level >= highest_level) return false;
1696 }
1697 return true;
1698}
1699
1700int SatSolver::ComputeBacktrackLevel(absl::Span<const Literal> literals) {
1701 SCOPED_TIME_STAT(&stats_);
1702 DCHECK_GT(CurrentDecisionLevel(), 0);
1703
1704 // We want the highest decision level among literals other than the first one.
1705 // Note that this level will always be smaller than that of the first literal.
1706 //
1707 // Note(user): if the learned clause is of size 1, we backtrack all the way to
1708 // the beginning. It may be possible to follow another behavior, but then the
1709 // code require some special cases in
1710 // AddLearnedClauseAndEnqueueUnitPropagation() to fix the literal and not
1711 // backtrack over it. Also, subsequent propagated variables may not have a
1712 // correct level in this case.
1713 int backtrack_level = 0;
1714 for (int i = 1; i < literals.size(); ++i) {
1715 const int level = DecisionLevel(literals[i].Variable());
1716 backtrack_level = std::max(backtrack_level, level);
1717 }
1718 DCHECK_LT(backtrack_level, DecisionLevel(literals[0].Variable()));
1719 DCHECK_LE(DecisionLevel(literals[0].Variable()), CurrentDecisionLevel());
1720 return backtrack_level;
1721}
1722
1723template <typename LiteralList>
1724int SatSolver::ComputeLbd(const LiteralList& literals) {
1725 SCOPED_TIME_STAT(&stats_);
1726 const int limit =
1727 parameters_->count_assumption_levels_in_lbd() ? 0 : assumption_level_;
1728
1729 // We know that the first literal is always of the highest level.
1730 is_level_marked_.ClearAndResize(
1731 SatDecisionLevel(DecisionLevel(literals.begin()->Variable()) + 1));
1732 for (const Literal literal : literals) {
1733 const SatDecisionLevel level(DecisionLevel(literal.Variable()));
1734 DCHECK_GE(level, 0);
1735 if (level > limit && !is_level_marked_[level]) {
1736 is_level_marked_.Set(level);
1737 }
1738 }
1739 return is_level_marked_.NumberOfSetCallsWithDifferentArguments();
1740}
1741
1742std::string SatSolver::StatusString(Status status) const {
1743 const double time_in_s = timer_.Get();
1744 return absl::StrFormat("\n status: %s\n", SatStatusString(status)) +
1745 absl::StrFormat(" time: %fs\n", time_in_s) +
1746 absl::StrFormat(" memory: %s\n", MemoryUsage()) +
1747 absl::StrFormat(
1748 " num failures: %d (%.0f /sec)\n", counters_.num_failures,
1749 static_cast<double>(counters_.num_failures) / time_in_s) +
1750 absl::StrFormat(
1751 " num branches: %d (%.0f /sec)\n", counters_.num_branches,
1752 static_cast<double>(counters_.num_branches) / time_in_s) +
1753 absl::StrFormat(" num propagations: %d (%.0f /sec)\n",
1755 static_cast<double>(num_propagations()) / time_in_s) +
1756 absl::StrFormat(" num binary propagations: %d\n",
1757 binary_implication_graph_->num_propagations()) +
1758 absl::StrFormat(" num binary inspections: %d\n",
1759 binary_implication_graph_->num_inspections()) +
1760 absl::StrFormat(
1761 " num binary redundant implications: %d\n",
1762 binary_implication_graph_->num_redundant_implications()) +
1763 absl::StrFormat(
1764 " num classic minimizations: %d"
1765 " (literals removed: %d)\n",
1766 counters_.num_minimizations, counters_.num_literals_removed) +
1767 absl::StrFormat(
1768 " num binary minimizations: %d"
1769 " (literals removed: %d)\n",
1770 binary_implication_graph_->num_minimization(),
1771 binary_implication_graph_->num_literals_removed()) +
1772 absl::StrFormat(" num inspected clauses: %d\n",
1773 clauses_propagator_->num_inspected_clauses()) +
1774 absl::StrFormat(" num inspected clause_literals: %d\n",
1775 clauses_propagator_->num_inspected_clause_literals()) +
1776 absl::StrFormat(
1777 " num learned literals: %d (avg: %.1f /clause)\n",
1778 counters_.num_literals_learned,
1779 1.0 * counters_.num_literals_learned / counters_.num_failures) +
1780 absl::StrFormat(
1781 " num learned PB literals: %d (avg: %.1f /clause)\n",
1782 counters_.num_learned_pb_literals,
1783 1.0 * counters_.num_learned_pb_literals / counters_.num_failures) +
1784 absl::StrFormat(" num subsumed clauses: %d\n",
1785 counters_.num_subsumed_clauses) +
1786 absl::StrFormat(" minimization_num_clauses: %d\n",
1787 counters_.minimization_num_clauses) +
1788 absl::StrFormat(" minimization_num_decisions: %d\n",
1789 counters_.minimization_num_decisions) +
1790 absl::StrFormat(" minimization_num_true: %d\n",
1791 counters_.minimization_num_true) +
1792 absl::StrFormat(" minimization_num_subsumed: %d\n",
1793 counters_.minimization_num_subsumed) +
1794 absl::StrFormat(" minimization_num_removed_literals: %d\n",
1795 counters_.minimization_num_removed_literals) +
1796 absl::StrFormat(" pb num threshold updates: %d\n",
1797 pb_constraints_->num_threshold_updates()) +
1798 absl::StrFormat(" pb num constraint lookups: %d\n",
1799 pb_constraints_->num_constraint_lookups()) +
1800 absl::StrFormat(" pb num inspected constraint literals: %d\n",
1801 pb_constraints_->num_inspected_constraint_literals()) +
1802 restart_->InfoString() +
1803 absl::StrFormat(" deterministic time: %f\n", deterministic_time());
1804}
1805
1806std::string SatSolver::RunningStatisticsString() const {
1807 const double time_in_s = timer_.Get();
1808 return absl::StrFormat(
1809 "%6.2fs, mem:%s, fails:%d, depth:%d, clauses:%d, tmp:%d, bin:%u, "
1810 "restarts:%d, vars:%d",
1811 time_in_s, MemoryUsage(), counters_.num_failures, CurrentDecisionLevel(),
1812 clauses_propagator_->num_clauses() -
1813 clauses_propagator_->num_removable_clauses(),
1814 clauses_propagator_->num_removable_clauses(),
1815 binary_implication_graph_->ComputeNumImplicationsForLog(),
1816 restart_->NumRestarts(),
1817 num_variables_.value() - num_processed_fixed_variables_);
1818}
1819
1820void SatSolver::ProcessNewlyFixedVariablesForDratProof() {
1821 if (drat_proof_handler_ == nullptr) return;
1822 if (CurrentDecisionLevel() != 0) return;
1823
1824 // We need to output the literals that are fixed so we can remove all
1825 // clauses that contains them. Note that this doesn't seems to be needed
1826 // for drat-trim.
1827 //
1828 // TODO(user): Ideally we could output such literal as soon as they are fixed,
1829 // but this is not that easy to do. Spend some time to find a cleaner
1830 // alternative? Currently this works, but:
1831 // - We will output some fixed literals twice since we already output learnt
1832 // clauses of size one.
1833 // - We need to call this function when needed.
1834 Literal temp;
1835 for (; drat_num_processed_fixed_variables_ < trail_->Index();
1836 ++drat_num_processed_fixed_variables_) {
1837 temp = (*trail_)[drat_num_processed_fixed_variables_];
1838 drat_proof_handler_->AddClause({&temp, 1});
1839 }
1840}
1841
1843 SCOPED_TIME_STAT(&stats_);
1844 DCHECK_EQ(CurrentDecisionLevel(), 0);
1845 int num_detached_clauses = 0;
1846 int num_binary = 0;
1847
1848 ProcessNewlyFixedVariablesForDratProof();
1849
1850 // We remove the clauses that are always true and the fixed literals from the
1851 // others. Note that none of the clause should be all false because we should
1852 // have detected a conflict before this is called.
1853 const int saved_index = trail_->Index();
1854 for (SatClause* clause : clauses_propagator_->AllClausesInCreationOrder()) {
1855 if (clause->IsRemoved()) continue;
1856
1857 const size_t old_size = clause->size();
1858 if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->Assignment())) {
1859 // The clause is always true, detach it.
1860 clauses_propagator_->LazyDetach(clause);
1861 ++num_detached_clauses;
1862 continue;
1863 }
1864
1865 const size_t new_size = clause->size();
1866 if (new_size == old_size) continue;
1867
1868 if (drat_proof_handler_ != nullptr) {
1869 CHECK_GT(new_size, 0);
1870 drat_proof_handler_->AddClause({clause->begin(), new_size});
1871 drat_proof_handler_->DeleteClause({clause->begin(), old_size});
1872 }
1873
1874 if (new_size == 2) {
1875 // This clause is now a binary clause, treat it separately. Note that
1876 // it is safe to do that because this clause can't be used as a reason
1877 // since we are at level zero and the clause is not satisfied.
1878 AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
1879 clauses_propagator_->LazyDetach(clause);
1880 ++num_binary;
1881
1882 // Tricky: AddBinaryClauseInternal() might fix literal if there is some
1883 // unprocessed equivalent literal, and the binary clause turn out to be
1884 // unary. This shouldn't happen otherwise the logic of
1885 // RemoveFixedLiteralsAndTestIfTrue() might fail.
1886 //
1887 // TODO(user): This still happen in SAT22.Carry_Save_Fast_1.cnf.cnf.xz,
1888 // it might not directly lead to a bug, but should still be fixed.
1889 DCHECK_EQ(trail_->Index(), saved_index);
1890 continue;
1891 }
1892 }
1893
1894 // Note that we will only delete the clauses during the next database cleanup.
1895 clauses_propagator_->CleanUpWatchers();
1896 if (num_detached_clauses > 0 || num_binary > 0) {
1897 VLOG(1) << trail_->Index() << " fixed variables at level 0. " << "Detached "
1898 << num_detached_clauses << " clauses. " << num_binary
1899 << " converted to binary.";
1900 }
1901
1902 // We also clean the binary implication graph.
1903 // Tricky: If we added the first binary clauses above, the binary graph
1904 // is not in "propagated" state as it should be, so we call Propagate() so
1905 // all the checks are happy.
1906 CHECK(binary_implication_graph_->Propagate(trail_));
1907 binary_implication_graph_->RemoveFixedVariables();
1908 num_processed_fixed_variables_ = trail_->Index();
1909 deterministic_time_of_last_fixed_variables_cleanup_ = deterministic_time();
1910}
1911
1912bool SatSolver::PropagationIsDone() const {
1913 for (SatPropagator* propagator : propagators_) {
1914 if (propagator->IsEmpty()) continue;
1915 if (!propagator->PropagationIsDone(*trail_)) return false;
1916 }
1917 return true;
1918}
1919
1920// TODO(user): Support propagating only the "first" propagators. That can
1921// be useful for probing/in-processing, so we can control if we do only the SAT
1922// part or the full integer part...
1924 SCOPED_TIME_STAT(&stats_);
1925 DCHECK(!ModelIsUnsat());
1926
1927 while (true) {
1928 // Because we might potentially iterate often on this list below, we remove
1929 // empty propagators.
1930 //
1931 // TODO(user): This might not really be needed.
1932 non_empty_propagators_.clear();
1933 for (SatPropagator* propagator : propagators_) {
1934 if (!propagator->IsEmpty()) {
1935 non_empty_propagators_.push_back(propagator);
1936 }
1937 }
1938
1939 while (true) {
1940 // The idea here is to abort the inspection as soon as at least one
1941 // propagation occurs so we can loop over and test again the highest
1942 // priority constraint types using the new information.
1943 //
1944 // Note that the first propagators_ should be the
1945 // binary_implication_graph_ and that its Propagate() functions will not
1946 // abort on the first propagation to be slightly more efficient.
1947 const int old_index = trail_->Index();
1948 for (SatPropagator* propagator : non_empty_propagators_) {
1949 DCHECK(propagator->PropagatePreconditionsAreSatisfied(*trail_));
1950 if (!propagator->Propagate(trail_)) return false;
1951 if (trail_->Index() > old_index) break;
1952 }
1953 if (trail_->Index() == old_index) break;
1954 }
1955
1956 // In some corner cases, we might add new constraint during propagation,
1957 // which might trigger new propagator addition or some propagator to become
1958 // non-empty() now.
1959 if (PropagationIsDone()) return true;
1960 }
1961 return true;
1962}
1963
1964void SatSolver::InitializePropagators() {
1965 propagators_.clear();
1966 propagators_.push_back(binary_implication_graph_);
1967 propagators_.push_back(clauses_propagator_);
1968 propagators_.push_back(pb_constraints_);
1969 for (int i = 0; i < external_propagators_.size(); ++i) {
1970 propagators_.push_back(external_propagators_[i]);
1971 }
1972 if (last_propagator_ != nullptr) {
1973 propagators_.push_back(last_propagator_);
1974 }
1975}
1976
1977bool SatSolver::ResolvePBConflict(BooleanVariable var,
1979 Coefficient* slack) {
1980 const int trail_index = trail_->Info(var).trail_index;
1981
1982 // This is the slack of the conflict < trail_index
1983 DCHECK_EQ(*slack, conflict->ComputeSlackForTrailPrefix(*trail_, trail_index));
1984
1985 // Pseudo-Boolean case.
1986 UpperBoundedLinearConstraint* pb_reason = ReasonPbConstraintOrNull(var);
1987 if (pb_reason != nullptr) {
1988 pb_reason->ResolvePBConflict(*trail_, var, conflict, slack);
1989 return false;
1990 }
1991
1992 // Generic clause case.
1993 Coefficient multiplier(1);
1994
1995 // TODO(user): experiment and choose the "best" algo.
1996 const int algorithm = 1;
1997 switch (algorithm) {
1998 case 1:
1999 // We reduce the conflict slack to 0 before adding the clause.
2000 // The advantage of this method is that the coefficients stay small.
2001 conflict->ReduceSlackTo(*trail_, trail_index, *slack, Coefficient(0));
2002 break;
2003 case 2:
2004 // No reduction, we add the lower possible multiple.
2005 multiplier = *slack + 1;
2006 break;
2007 default:
2008 // No reduction, the multiple is chosen to cancel var.
2009 multiplier = conflict->GetCoefficient(var);
2010 }
2011
2012 Coefficient num_literals(1);
2013 conflict->AddTerm(
2014 trail_->Assignment().GetTrueLiteralForAssignedVariable(var).Negated(),
2015 multiplier);
2016 for (Literal literal : trail_->Reason(var)) {
2017 DCHECK_NE(literal.Variable(), var);
2018 DCHECK(Assignment().LiteralIsFalse(literal));
2019 conflict->AddTerm(literal.Negated(), multiplier);
2020 ++num_literals;
2021 }
2022 conflict->AddToRhs((num_literals - 1) * multiplier);
2023
2024 // All the algorithms above result in a new slack of -1.
2025 *slack = -1;
2026 DCHECK_EQ(*slack, conflict->ComputeSlackForTrailPrefix(*trail_, trail_index));
2027 return true;
2028}
2029
2030void SatSolver::EnqueueNewDecision(Literal literal) {
2031 SCOPED_TIME_STAT(&stats_);
2032 CHECK(!Assignment().VariableIsAssigned(literal.Variable()));
2033
2034 // We are back at level 0. This can happen because of a restart, or because
2035 // we proved that some variables must take a given value in any satisfiable
2036 // assignment. Trigger a simplification of the clauses if there is new fixed
2037 // variables. Note that for efficiency reason, we don't do that too often.
2038 //
2039 // TODO(user): Do more advanced preprocessing?
2040 if (CurrentDecisionLevel() == 0) {
2041 const double kMinDeterministicTimeBetweenCleanups = 1.0;
2042 if (num_processed_fixed_variables_ < trail_->Index() &&
2044 deterministic_time_of_last_fixed_variables_cleanup_ +
2045 kMinDeterministicTimeBetweenCleanups) {
2047 }
2048 }
2049
2050 counters_.num_branches++;
2051 last_decision_or_backtrack_trail_index_ = trail_->Index();
2052 decisions_[current_decision_level_] = Decision(trail_->Index(), literal);
2053 ++current_decision_level_;
2054 trail_->SetDecisionLevel(current_decision_level_);
2055 trail_->EnqueueSearchDecision(literal);
2056}
2057
2058std::string SatSolver::DebugString(const SatClause& clause) const {
2059 std::string result;
2060 for (const Literal literal : clause) {
2061 if (!result.empty()) {
2062 result.append(" || ");
2063 }
2064 const std::string value =
2065 trail_->Assignment().LiteralIsTrue(literal)
2066 ? "true"
2067 : (trail_->Assignment().LiteralIsFalse(literal) ? "false"
2068 : "undef");
2069 result.append(absl::StrFormat("%s(%s)", literal.DebugString(), value));
2070 }
2071 return result;
2072}
2073
2074int SatSolver::ComputeMaxTrailIndex(absl::Span<const Literal> clause) const {
2075 SCOPED_TIME_STAT(&stats_);
2076 int trail_index = -1;
2077 for (const Literal literal : clause) {
2078 trail_index =
2079 std::max(trail_index, trail_->Info(literal.Variable()).trail_index);
2080 }
2081 return trail_index;
2082}
2083
2084// This method will compute a first UIP conflict
2085// http://www.cs.tau.ac.il/~msagiv/courses/ATP/iccad2001_final.pdf
2086// http://gauss.ececs.uc.edu/SAT/articles/FAIA185-0131.pdf
2087void SatSolver::ComputeFirstUIPConflict(
2088 int max_trail_index, std::vector<Literal>* conflict,
2089 std::vector<Literal>* reason_used_to_infer_the_conflict,
2090 std::vector<SatClause*>* subsumed_clauses) {
2091 SCOPED_TIME_STAT(&stats_);
2092 const int64_t conflict_id = counters_.num_failures;
2093
2094 // This will be used to mark all the literals inspected while we process the
2095 // conflict and the reasons behind each of its variable assignments.
2096 is_marked_.ClearAndResize(num_variables_);
2097
2098 conflict->clear();
2099 reason_used_to_infer_the_conflict->clear();
2100 subsumed_clauses->clear();
2101 if (max_trail_index == -1) return;
2102
2103 // max_trail_index is the maximum trail index appearing in the failing_clause
2104 // and its level (Which is almost always equals to the CurrentDecisionLevel(),
2105 // except for symmetry propagation).
2106 DCHECK_EQ(max_trail_index, ComputeMaxTrailIndex(trail_->FailingClause()));
2107 int trail_index = max_trail_index;
2108 const int highest_level = DecisionLevel((*trail_)[trail_index].Variable());
2109 if (highest_level == 0) return;
2110
2111 // To find the 1-UIP conflict clause, we start by the failing_clause, and
2112 // expand each of its literal using the reason for this literal assignment to
2113 // false. The is_marked_ set allow us to never expand the same literal twice.
2114 //
2115 // The expansion is not done (i.e. stop) for literals that were assigned at a
2116 // decision level below the current one. If the level of such literal is not
2117 // zero, it is added to the conflict clause.
2118 //
2119 // Now, the trick is that we use the trail to expand the literal of the
2120 // current level in a very specific order. Namely the reverse order of the one
2121 // in which they were inferred. We stop as soon as
2122 // num_literal_at_highest_level_that_needs_to_be_processed is exactly one.
2123 //
2124 // This last literal will be the first UIP because by definition all the
2125 // propagation done at the current level will pass though it at some point.
2126 absl::Span<const Literal> clause_to_expand = trail_->FailingClause();
2127 SatClause* sat_clause = trail_->FailingSatClause();
2128 DCHECK(!clause_to_expand.empty());
2129 int num_literal_at_highest_level_that_needs_to_be_processed = 0;
2130 while (true) {
2131 int num_new_vars_at_positive_level = 0;
2132 int num_vars_at_positive_level_in_clause_to_expand = 0;
2133 for (const Literal literal : clause_to_expand) {
2134 const BooleanVariable var = literal.Variable();
2135 const int level = DecisionLevel(var);
2136 if (level == 0) continue;
2137 ++num_vars_at_positive_level_in_clause_to_expand;
2138 if (!is_marked_[var]) {
2139 is_marked_.Set(var);
2140 ++num_new_vars_at_positive_level;
2141 if (level == highest_level) {
2142 ++num_literal_at_highest_level_that_needs_to_be_processed;
2143 } else {
2144 // Note that all these literals are currently false since the clause
2145 // to expand was used to infer the value of a literal at this level.
2146 DCHECK(trail_->Assignment().LiteralIsFalse(literal));
2147 conflict->push_back(literal);
2148 }
2149 }
2150 }
2151
2152 // If there is new variables, then all the previously subsumed clauses are
2153 // not subsumed anymore.
2154 if (num_new_vars_at_positive_level > 0) {
2155 // TODO(user): We could still replace all these clauses with the current
2156 // conflict.
2157 subsumed_clauses->clear();
2158 }
2159
2160 // This check if the new conflict is exactly equal to clause_to_expand.
2161 // Since we just performed an union, comparing the size is enough. When this
2162 // is true, then the current conflict subsumes the reason whose underlying
2163 // clause is given by sat_clause.
2164 if (sat_clause != nullptr &&
2165 num_vars_at_positive_level_in_clause_to_expand ==
2166 conflict->size() +
2167 num_literal_at_highest_level_that_needs_to_be_processed) {
2168 subsumed_clauses->push_back(sat_clause);
2169 }
2170
2171 // Find next marked literal to expand from the trail.
2172 DCHECK_GT(num_literal_at_highest_level_that_needs_to_be_processed, 0);
2173 while (!is_marked_[(*trail_)[trail_index].Variable()]) {
2174 --trail_index;
2175 DCHECK_GE(trail_index, 0);
2176 DCHECK_EQ(DecisionLevel((*trail_)[trail_index].Variable()),
2177 highest_level);
2178 }
2179
2180 if (num_literal_at_highest_level_that_needs_to_be_processed == 1) {
2181 // We have the first UIP. Add its negation to the conflict clause.
2182 // This way, after backtracking to the proper level, the conflict clause
2183 // will be unit, and infer the negation of the UIP that caused the fail.
2184 conflict->push_back((*trail_)[trail_index].Negated());
2185
2186 // To respect the function API move the first UIP in the first position.
2187 std::swap(conflict->back(), conflict->front());
2188 break;
2189 }
2190
2191 const Literal literal = (*trail_)[trail_index];
2192 reason_used_to_infer_the_conflict->push_back(literal);
2193
2194 // If we already encountered the same reason, we can just skip this literal
2195 // which is what setting clause_to_expand to the empty clause do.
2196 if (same_reason_identifier_.FirstVariableWithSameReason(
2197 literal.Variable()) != literal.Variable()) {
2198 clause_to_expand = {};
2199 } else {
2200 clause_to_expand = trail_->Reason(literal.Variable(), conflict_id);
2201 }
2202 sat_clause = ReasonClauseOrNull(literal.Variable());
2203
2204 --num_literal_at_highest_level_that_needs_to_be_processed;
2205 --trail_index;
2206 }
2207}
2208
2209void SatSolver::ComputeUnionOfReasons(absl::Span<const Literal> input,
2210 std::vector<Literal>* literals) {
2211 tmp_mark_.ClearAndResize(num_variables_);
2212 literals->clear();
2213 for (const Literal l : input) tmp_mark_.Set(l.Variable());
2214 for (const Literal l : input) {
2215 for (const Literal r : trail_->Reason(l.Variable())) {
2216 if (!tmp_mark_[r.Variable()]) {
2217 tmp_mark_.Set(r.Variable());
2218 literals->push_back(r);
2219 }
2220 }
2221 }
2222 for (const Literal l : input) tmp_mark_.Clear(l.Variable());
2223 for (const Literal l : *literals) tmp_mark_.Clear(l.Variable());
2224}
2225
2226// TODO(user): Remove the literals assigned at level 0.
2227void SatSolver::ComputePBConflict(int max_trail_index,
2228 Coefficient initial_slack,
2230 int* pb_backjump_level) {
2231 SCOPED_TIME_STAT(&stats_);
2232 int trail_index = max_trail_index;
2233
2234 // First compute the slack of the current conflict for the assignment up to
2235 // trail_index. It must be negative since this is a conflict.
2236 Coefficient slack = initial_slack;
2237 DCHECK_EQ(slack,
2238 conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1));
2239 CHECK_LT(slack, 0) << "We don't have a conflict!";
2240
2241 // Iterate backward over the trail.
2242 int backjump_level = 0;
2243 while (true) {
2244 const BooleanVariable var = (*trail_)[trail_index].Variable();
2245 --trail_index;
2246
2247 if (conflict->GetCoefficient(var) > 0 &&
2248 trail_->Assignment().LiteralIsTrue(conflict->GetLiteral(var))) {
2249 if (parameters_->minimize_reduction_during_pb_resolution()) {
2250 // When this parameter is true, we don't call ReduceCoefficients() at
2251 // every loop. However, it is still important to reduce the "current"
2252 // variable coefficient, because this can impact the value of the new
2253 // slack below.
2254 conflict->ReduceGivenCoefficient(var);
2255 }
2256
2257 // This is the slack one level before (< Info(var).trail_index).
2258 slack += conflict->GetCoefficient(var);
2259
2260 // This can't happen at the beginning, but may happen later.
2261 // It means that even without var assigned, we still have a conflict.
2262 if (slack < 0) continue;
2263
2264 // At this point, just removing the last assignment lift the conflict.
2265 // So we can abort if the true assignment before that is at a lower level
2266 // TODO(user): Somewhat inefficient.
2267 // TODO(user): We could abort earlier...
2268 const int current_level = DecisionLevel(var);
2269 int i = trail_index;
2270 while (i >= 0) {
2271 const BooleanVariable previous_var = (*trail_)[i].Variable();
2272 if (conflict->GetCoefficient(previous_var) > 0 &&
2273 trail_->Assignment().LiteralIsTrue(
2274 conflict->GetLiteral(previous_var))) {
2275 break;
2276 }
2277 --i;
2278 }
2279 if (i < 0 || DecisionLevel((*trail_)[i].Variable()) < current_level) {
2280 backjump_level = i < 0 ? 0 : DecisionLevel((*trail_)[i].Variable());
2281 break;
2282 }
2283
2284 // We can't abort, So resolve the current variable.
2285 DCHECK_NE(trail_->AssignmentType(var), AssignmentType::kSearchDecision);
2286 const bool clause_used = ResolvePBConflict(var, conflict, &slack);
2287
2288 // At this point, we have a negative slack. Note that ReduceCoefficients()
2289 // will not change it. However it may change the slack value of the next
2290 // iteration (when we will no longer take into account the true literal
2291 // with highest trail index).
2292 //
2293 // Note that the trail_index has already been decremented, it is why
2294 // we need the +1 in the slack computation.
2295 const Coefficient slack_only_for_debug =
2297 ? conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1)
2298 : Coefficient(0);
2299
2300 if (clause_used) {
2301 // If a clause was used, we know that slack has the correct value.
2302 if (!parameters_->minimize_reduction_during_pb_resolution()) {
2303 conflict->ReduceCoefficients();
2304 }
2305 } else {
2306 // TODO(user): The function below can take most of the running time on
2307 // some instances. The goal is to have slack updated to its new value
2308 // incrementally, but we are not here yet.
2309 if (parameters_->minimize_reduction_during_pb_resolution()) {
2310 slack =
2311 conflict->ComputeSlackForTrailPrefix(*trail_, trail_index + 1);
2312 } else {
2313 slack = conflict->ReduceCoefficientsAndComputeSlackForTrailPrefix(
2314 *trail_, trail_index + 1);
2315 }
2316 }
2317 DCHECK_EQ(slack, slack_only_for_debug);
2318 CHECK_LT(slack, 0);
2319 if (conflict->Rhs() < 0) {
2320 *pb_backjump_level = -1;
2321 return;
2322 }
2323 }
2324 }
2325
2326 // Reduce the conflit coefficients if it is not already done.
2327 // This is important to avoid integer overflow.
2328 if (!parameters_->minimize_reduction_during_pb_resolution()) {
2329 conflict->ReduceCoefficients();
2330 }
2331
2332 // Double check.
2333 // The sum of the literal with level <= backjump_level must propagate.
2334 std::vector<Coefficient> sum_for_le_level(backjump_level + 2, Coefficient(0));
2335 std::vector<Coefficient> max_coeff_for_ge_level(backjump_level + 2,
2336 Coefficient(0));
2337 int size = 0;
2338 Coefficient max_sum(0);
2339 for (BooleanVariable var : conflict->PossibleNonZeros()) {
2340 const Coefficient coeff = conflict->GetCoefficient(var);
2341 if (coeff == 0) continue;
2342 max_sum += coeff;
2343 ++size;
2344 if (!trail_->Assignment().VariableIsAssigned(var) ||
2345 DecisionLevel(var) > backjump_level) {
2346 max_coeff_for_ge_level[backjump_level + 1] =
2347 std::max(max_coeff_for_ge_level[backjump_level + 1], coeff);
2348 } else {
2349 const int level = DecisionLevel(var);
2350 if (trail_->Assignment().LiteralIsTrue(conflict->GetLiteral(var))) {
2351 sum_for_le_level[level] += coeff;
2352 }
2353 max_coeff_for_ge_level[level] =
2354 std::max(max_coeff_for_ge_level[level], coeff);
2355 }
2356 }
2357
2358 // Compute the cumulative version.
2359 for (int i = 1; i < sum_for_le_level.size(); ++i) {
2360 sum_for_le_level[i] += sum_for_le_level[i - 1];
2361 }
2362 for (int i = max_coeff_for_ge_level.size() - 2; i >= 0; --i) {
2363 max_coeff_for_ge_level[i] =
2364 std::max(max_coeff_for_ge_level[i], max_coeff_for_ge_level[i + 1]);
2365 }
2366
2367 // Compute first propagation level. -1 means that the problem is UNSAT.
2368 // Note that the first propagation level may be < backjump_level!
2369 if (sum_for_le_level[0] > conflict->Rhs()) {
2370 *pb_backjump_level = -1;
2371 return;
2372 }
2373 for (int i = 0; i <= backjump_level; ++i) {
2374 const Coefficient level_sum = sum_for_le_level[i];
2375 CHECK_LE(level_sum, conflict->Rhs());
2376 if (conflict->Rhs() - level_sum < max_coeff_for_ge_level[i + 1]) {
2377 *pb_backjump_level = i;
2378 return;
2379 }
2380 }
2381 LOG(FATAL) << "The code should never reach here.";
2382}
2383
2384void SatSolver::MinimizeConflict(std::vector<Literal>* conflict) {
2385 SCOPED_TIME_STAT(&stats_);
2386
2387 const int old_size = conflict->size();
2388 switch (parameters_->minimization_algorithm()) {
2389 case SatParameters::NONE:
2390 return;
2391 case SatParameters::SIMPLE: {
2392 MinimizeConflictSimple(conflict);
2393 break;
2394 }
2395 case SatParameters::RECURSIVE: {
2396 MinimizeConflictRecursively(conflict);
2397 break;
2398 }
2399 case SatParameters::EXPERIMENTAL: {
2400 MinimizeConflictExperimental(conflict);
2401 break;
2402 }
2403 }
2404 if (conflict->size() < old_size) {
2405 ++counters_.num_minimizations;
2406 counters_.num_literals_removed += old_size - conflict->size();
2407 }
2408}
2409
2410// This simple version just looks for any literal that is directly infered by
2411// other literals of the conflict. It is directly infered if the literals of its
2412// reason clause are either from level 0 or from the conflict itself.
2413//
2414// Note that because of the assignment structure, there is no need to process
2415// the literals of the conflict in order. While exploring the reason for a
2416// literal assignment, there will be no cycles.
2417void SatSolver::MinimizeConflictSimple(std::vector<Literal>* conflict) {
2418 SCOPED_TIME_STAT(&stats_);
2419 const int current_level = CurrentDecisionLevel();
2420
2421 // Note that is_marked_ is already initialized and that we can start at 1
2422 // since the first literal of the conflict is the 1-UIP literal.
2423 int index = 1;
2424 for (int i = 1; i < conflict->size(); ++i) {
2425 const BooleanVariable var = (*conflict)[i].Variable();
2426 bool can_be_removed = false;
2427 if (DecisionLevel(var) != current_level) {
2428 // It is important not to call Reason(var) when it can be avoided.
2429 const absl::Span<const Literal> reason = trail_->Reason(var);
2430 if (!reason.empty()) {
2431 can_be_removed = true;
2432 for (Literal literal : reason) {
2433 if (DecisionLevel(literal.Variable()) == 0) continue;
2434 if (!is_marked_[literal.Variable()]) {
2435 can_be_removed = false;
2436 break;
2437 }
2438 }
2439 }
2440 }
2441 if (!can_be_removed) {
2442 (*conflict)[index] = (*conflict)[i];
2443 ++index;
2444 }
2445 }
2446 conflict->erase(conflict->begin() + index, conflict->end());
2447}
2448
2449// This is similar to MinimizeConflictSimple() except that for each literal of
2450// the conflict, the literals of its reason are recursively expanded using their
2451// reason and so on. The recursion loops until we show that the initial literal
2452// can be infered from the conflict variables alone, or if we show that this is
2453// not the case. The result of any variable expansion will be cached in order
2454// not to be expended again.
2455void SatSolver::MinimizeConflictRecursively(std::vector<Literal>* conflict) {
2456 SCOPED_TIME_STAT(&stats_);
2457
2458 // is_marked_ will contains all the conflict literals plus the literals that
2459 // have been shown to depends only on the conflict literals. is_independent_
2460 // will contains the literals that have been shown NOT to depends only on the
2461 // conflict literals. The too set are exclusive for non-conflict literals, but
2462 // a conflict literal (which is always marked) can be independent if we showed
2463 // that it can't be removed from the clause.
2464 //
2465 // Optimization: There is no need to call is_marked_.ClearAndResize() or to
2466 // mark the conflict literals since this was already done by
2467 // ComputeFirstUIPConflict().
2468 is_independent_.ClearAndResize(num_variables_);
2469
2470 // min_trail_index_per_level_ will always be reset to all
2471 // std::numeric_limits<int>::max() at the end. This is used to prune the
2472 // search because any literal at a given level with an index smaller or equal
2473 // to min_trail_index_per_level_[level] can't be redundant.
2474 if (CurrentDecisionLevel() >= min_trail_index_per_level_.size()) {
2475 min_trail_index_per_level_.resize(CurrentDecisionLevel() + 1,
2476 std::numeric_limits<int>::max());
2477 }
2478
2479 // Compute the number of variable at each decision levels. This will be used
2480 // to pruned the DFS because we know that the minimized conflict will have at
2481 // least one variable of each decision levels. Because such variable can't be
2482 // eliminated using lower decision levels variable otherwise it will have been
2483 // propagated.
2484 //
2485 // Note(user): Because is_marked_ may actually contains literals that are
2486 // implied if the 1-UIP literal is false, we can't just iterate on the
2487 // variables of the conflict here.
2488 for (BooleanVariable var : is_marked_.PositionsSetAtLeastOnce()) {
2489 const int level = DecisionLevel(var);
2490 min_trail_index_per_level_[level] = std::min(
2491 min_trail_index_per_level_[level], trail_->Info(var).trail_index);
2492 }
2493
2494 // Remove the redundant variable from the conflict. That is the ones that can
2495 // be infered by some other variables in the conflict.
2496 // Note that we can skip the first position since this is the 1-UIP.
2497 int index = 1;
2498 TimeLimitCheckEveryNCalls time_limit_check(100, time_limit_);
2499 for (int i = 1; i < conflict->size(); ++i) {
2500 const BooleanVariable var = (*conflict)[i].Variable();
2501 const AssignmentInfo& info = trail_->Info(var);
2502 if (time_limit_check.LimitReached() ||
2503 info.type == AssignmentType::kSearchDecision ||
2504 info.trail_index <= min_trail_index_per_level_[info.level] ||
2505 !CanBeInferedFromConflictVariables(var)) {
2506 // Mark the conflict variable as independent. Note that is_marked_[var]
2507 // will still be true.
2508 is_independent_.Set(var);
2509 (*conflict)[index] = (*conflict)[i];
2510 ++index;
2511 }
2512 }
2513 conflict->resize(index);
2514
2515 // Reset min_trail_index_per_level_. We use the sparse version only if it
2516 // involves less than half the size of min_trail_index_per_level_.
2517 const int threshold = min_trail_index_per_level_.size() / 2;
2518 if (is_marked_.PositionsSetAtLeastOnce().size() < threshold) {
2519 for (BooleanVariable var : is_marked_.PositionsSetAtLeastOnce()) {
2520 min_trail_index_per_level_[DecisionLevel(var)] =
2521 std::numeric_limits<int>::max();
2522 }
2523 } else {
2524 min_trail_index_per_level_.clear();
2525 }
2526}
2527
2528bool SatSolver::CanBeInferedFromConflictVariables(BooleanVariable variable) {
2529 // Test for an already processed variable with the same reason.
2530 {
2531 DCHECK(is_marked_[variable]);
2532 const BooleanVariable v =
2533 same_reason_identifier_.FirstVariableWithSameReason(variable);
2534 if (v != variable) return !is_independent_[v];
2535 }
2536
2537 // This function implement an iterative DFS from the given variable. It uses
2538 // the reason clause as adjacency lists. dfs_stack_ can be seens as the
2539 // recursive call stack of the variable we are currently processing. All its
2540 // adjacent variable will be pushed into variable_to_process_, and we will
2541 // then dequeue them one by one and process them.
2542 //
2543 // Note(user): As of 03/2014, --cpu_profile seems to indicate that using
2544 // dfs_stack_.assign(1, variable) is slower. My explanation is that the
2545 // function call is not inlined.
2546 dfs_stack_.clear();
2547 dfs_stack_.push_back(variable);
2548 variable_to_process_.clear();
2549 variable_to_process_.push_back(variable);
2550
2551 // First we expand the reason for the given variable.
2552 for (const Literal literal : trail_->Reason(variable)) {
2553 const BooleanVariable var = literal.Variable();
2554 DCHECK_NE(var, variable);
2555 if (is_marked_[var]) continue;
2556 const AssignmentInfo& info = trail_->Info(var);
2557 if (info.level == 0) {
2558 // Note that this is not needed if the solver is not configured to produce
2559 // an unsat proof. However, the (level == 0) test should always be false
2560 // in this case because there will never be literals of level zero in any
2561 // reason when we don't want a proof.
2562 is_marked_.Set(var);
2563 continue;
2564 }
2565 if (info.trail_index <= min_trail_index_per_level_[info.level] ||
2566 info.type == AssignmentType::kSearchDecision || is_independent_[var]) {
2567 return false;
2568 }
2569 variable_to_process_.push_back(var);
2570 }
2571
2572 // Then we start the DFS.
2573 while (!variable_to_process_.empty()) {
2574 const BooleanVariable current_var = variable_to_process_.back();
2575 if (current_var == dfs_stack_.back()) {
2576 // We finished the DFS of the variable dfs_stack_.back(), this can be seen
2577 // as a recursive call terminating.
2578 if (dfs_stack_.size() > 1) {
2579 DCHECK(!is_marked_[current_var]);
2580 is_marked_.Set(current_var);
2581 }
2582 variable_to_process_.pop_back();
2583 dfs_stack_.pop_back();
2584 continue;
2585 }
2586
2587 // If this variable became marked since the we pushed it, we can skip it.
2588 if (is_marked_[current_var]) {
2589 variable_to_process_.pop_back();
2590 continue;
2591 }
2592
2593 // This case will never be encountered since we abort right away as soon
2594 // as an independent variable is found.
2595 DCHECK(!is_independent_[current_var]);
2596
2597 // Test for an already processed variable with the same reason.
2598 {
2599 const BooleanVariable v =
2600 same_reason_identifier_.FirstVariableWithSameReason(current_var);
2601 if (v != current_var) {
2602 if (is_independent_[v]) break;
2603 DCHECK(is_marked_[v]);
2604 variable_to_process_.pop_back();
2605 continue;
2606 }
2607 }
2608
2609 // Expand the variable. This can be seen as making a recursive call.
2610 dfs_stack_.push_back(current_var);
2611 bool abort_early = false;
2612 for (Literal literal : trail_->Reason(current_var)) {
2613 const BooleanVariable var = literal.Variable();
2614 DCHECK_NE(var, current_var);
2615 const AssignmentInfo& info = trail_->Info(var);
2616 if (info.level == 0 || is_marked_[var]) continue;
2617 if (info.trail_index <= min_trail_index_per_level_[info.level] ||
2618 info.type == AssignmentType::kSearchDecision ||
2619 is_independent_[var]) {
2620 abort_early = true;
2621 break;
2622 }
2623 variable_to_process_.push_back(var);
2624 }
2625 if (abort_early) break;
2626 }
2627
2628 // All the variable left on the dfs_stack_ are independent.
2629 for (const BooleanVariable var : dfs_stack_) {
2630 is_independent_.Set(var);
2631 }
2632 return dfs_stack_.empty();
2633}
2634
2635namespace {
2636
2637struct WeightedVariable {
2638 WeightedVariable(BooleanVariable v, int w) : var(v), weight(w) {}
2639
2640 BooleanVariable var;
2641 int weight;
2642};
2643
2644// Lexical order, by larger weight, then by smaller variable number
2645// to break ties
2646struct VariableWithLargerWeightFirst {
2647 bool operator()(const WeightedVariable& wv1,
2648 const WeightedVariable& wv2) const {
2649 return (wv1.weight > wv2.weight ||
2650 (wv1.weight == wv2.weight && wv1.var < wv2.var));
2651 }
2652};
2653} // namespace.
2654
2655// This function allows a conflict variable to be replaced by another variable
2656// not originally in the conflict. Greater reduction and backtracking can be
2657// achieved this way, but the effect of this is not clear.
2658//
2659// TODO(user): More investigation needed. This seems to help on the Hanoi
2660// problems, but degrades performance on others.
2661//
2662// TODO(user): Find a reference for this? neither minisat nor glucose do that,
2663// they just do MinimizeConflictRecursively() with a different implementation.
2664// Note that their behavior also make more sense with the way they (and we) bump
2665// the variable activities.
2666void SatSolver::MinimizeConflictExperimental(std::vector<Literal>* conflict) {
2667 SCOPED_TIME_STAT(&stats_);
2668
2669 // First, sort the variables in the conflict by decreasing decision levels.
2670 // Also initialize is_marked_ to true for all conflict variables.
2671 is_marked_.ClearAndResize(num_variables_);
2672 const int current_level = CurrentDecisionLevel();
2673 std::vector<WeightedVariable> variables_sorted_by_level;
2674 for (Literal literal : *conflict) {
2675 const BooleanVariable var = literal.Variable();
2676 is_marked_.Set(var);
2677 const int level = DecisionLevel(var);
2678 if (level < current_level) {
2679 variables_sorted_by_level.push_back(WeightedVariable(var, level));
2680 }
2681 }
2682 std::sort(variables_sorted_by_level.begin(), variables_sorted_by_level.end(),
2683 VariableWithLargerWeightFirst());
2684
2685 // Then process the reason of the variable with highest level first.
2686 std::vector<BooleanVariable> to_remove;
2687 for (WeightedVariable weighted_var : variables_sorted_by_level) {
2688 const BooleanVariable var = weighted_var.var;
2689
2690 // A nullptr reason means that this was a decision variable from the
2691 // previous levels.
2692 const absl::Span<const Literal> reason = trail_->Reason(var);
2693 if (reason.empty()) continue;
2694
2695 // Compute how many and which literals from the current reason do not appear
2696 // in the current conflict. Level 0 literals are ignored.
2697 std::vector<Literal> not_contained_literals;
2698 for (const Literal reason_literal : reason) {
2699 const BooleanVariable reason_var = reason_literal.Variable();
2700
2701 // We ignore level 0 variables.
2702 if (DecisionLevel(reason_var) == 0) continue;
2703
2704 // We have a reason literal whose variable is not yet seen.
2705 // If there is more than one, break right away, we will not minimize the
2706 // current conflict with this variable.
2707 if (!is_marked_[reason_var]) {
2708 not_contained_literals.push_back(reason_literal);
2709 if (not_contained_literals.size() > 1) break;
2710 }
2711 }
2712 if (not_contained_literals.empty()) {
2713 // This variable will be deleted from the conflict. Note that we don't
2714 // unmark it. This is because this variable can be infered from the other
2715 // variables in the conflict, so it is okay to skip it when processing the
2716 // reasons of other variables.
2717 to_remove.push_back(var);
2718 } else if (not_contained_literals.size() == 1) {
2719 // Replace the literal from variable var with the only
2720 // not_contained_literals from the current reason.
2721 to_remove.push_back(var);
2722 is_marked_.Set(not_contained_literals.front().Variable());
2723 conflict->push_back(not_contained_literals.front());
2724 }
2725 }
2726
2727 // Unmark the variable that should be removed from the conflict.
2728 for (BooleanVariable var : to_remove) {
2729 is_marked_.Clear(var);
2730 }
2731
2732 // Remove the now unmarked literals from the conflict.
2733 int index = 0;
2734 for (int i = 0; i < conflict->size(); ++i) {
2735 const Literal literal = (*conflict)[i];
2736 if (is_marked_[literal.Variable()]) {
2737 (*conflict)[index] = literal;
2738 ++index;
2739 }
2740 }
2741 conflict->erase(conflict->begin() + index, conflict->end());
2742}
2743
2744void SatSolver::CleanClauseDatabaseIfNeeded() {
2745 if (num_learned_clause_before_cleanup_ > 0) return;
2746 SCOPED_TIME_STAT(&stats_);
2747
2748 // Creates a list of clauses that can be deleted. Note that only the clauses
2749 // that appear in clauses_info can potentially be removed.
2750 typedef std::pair<SatClause*, ClauseInfo> Entry;
2751 std::vector<Entry> entries;
2752 auto& clauses_info = *(clauses_propagator_->mutable_clauses_info());
2753 for (auto& entry : clauses_info) {
2754 if (ClauseIsUsedAsReason(entry.first)) continue;
2755 if (entry.second.protected_during_next_cleanup) {
2756 entry.second.protected_during_next_cleanup = false;
2757 continue;
2758 }
2759 entries.push_back(entry);
2760 }
2761 const int num_protected_clauses = clauses_info.size() - entries.size();
2762
2763 if (parameters_->clause_cleanup_ordering() == SatParameters::CLAUSE_LBD) {
2764 // Order the clauses by decreasing LBD and then increasing activity.
2765 std::sort(entries.begin(), entries.end(),
2766 [](const Entry& a, const Entry& b) {
2767 if (a.second.lbd == b.second.lbd) {
2768 return a.second.activity < b.second.activity;
2769 }
2770 return a.second.lbd > b.second.lbd;
2771 });
2772 } else {
2773 // Order the clauses by increasing activity and then decreasing LBD.
2774 std::sort(entries.begin(), entries.end(),
2775 [](const Entry& a, const Entry& b) {
2776 if (a.second.activity == b.second.activity) {
2777 return a.second.lbd > b.second.lbd;
2778 }
2779 return a.second.activity < b.second.activity;
2780 });
2781 }
2782
2783 // The clause we want to keep are at the end of the vector.
2784 int num_kept_clauses =
2785 (parameters_->clause_cleanup_target() > 0)
2786 ? std::min(static_cast<int>(entries.size()),
2787 parameters_->clause_cleanup_target())
2788 : static_cast<int>(parameters_->clause_cleanup_ratio() *
2789 static_cast<double>(entries.size()));
2790
2791 int num_deleted_clauses = entries.size() - num_kept_clauses;
2792
2793 // Tricky: Because the order of the clauses_info iteration is NOT
2794 // deterministic (pointer keys), we also keep all the clauses which have the
2795 // same LBD and activity as the last one so the behavior is deterministic.
2796 if (num_kept_clauses > 0) {
2797 while (num_deleted_clauses > 0) {
2798 const ClauseInfo& a = entries[num_deleted_clauses].second;
2799 const ClauseInfo& b = entries[num_deleted_clauses - 1].second;
2800 if (a.activity != b.activity || a.lbd != b.lbd) break;
2801 --num_deleted_clauses;
2802 ++num_kept_clauses;
2803 }
2804 }
2805 if (num_deleted_clauses > 0) {
2806 entries.resize(num_deleted_clauses);
2807 for (const Entry& entry : entries) {
2808 SatClause* clause = entry.first;
2809 counters_.num_literals_forgotten += clause->size();
2810 clauses_propagator_->LazyDetach(clause);
2811 }
2812 clauses_propagator_->CleanUpWatchers();
2813
2814 // TODO(user): If the need arise, we could avoid this linear scan on the
2815 // full list of clauses by not keeping the clauses from clauses_info there.
2816 if (!block_clause_deletion_) {
2817 clauses_propagator_->DeleteRemovedClauses();
2818 }
2819 }
2820
2821 num_learned_clause_before_cleanup_ = parameters_->clause_cleanup_period();
2822 VLOG(1) << "Database cleanup, #protected:" << num_protected_clauses
2823 << " #kept:" << num_kept_clauses
2824 << " #deleted:" << num_deleted_clauses;
2825}
2826
2828 switch (status) {
2830 return "ASSUMPTIONS_UNSAT";
2832 return "INFEASIBLE";
2834 return "FEASIBLE";
2836 return "LIMIT_REACHED";
2837 }
2838 // Fallback. We don't use "default:" so the compiler will return an error
2839 // if we forgot one enum case above.
2840 LOG(DFATAL) << "Invalid SatSolver::Status " << status;
2841 return "UNKNOWN";
2842}
2843
2844void MinimizeCore(SatSolver* solver, std::vector<Literal>* core) {
2845 std::vector<Literal> result;
2846 if (!solver->ResetToLevelZero()) return;
2847 for (const Literal lit : *core) {
2848 if (solver->Assignment().LiteralIsTrue(lit)) continue;
2849 result.push_back(lit);
2850 if (solver->Assignment().LiteralIsFalse(lit)) break;
2851 if (!solver->EnqueueDecisionIfNotConflicting(lit)) break;
2852 }
2853 if (result.size() < core->size()) {
2854 VLOG(1) << "minimization " << core->size() << " -> " << result.size();
2855 *core = result;
2856 }
2857}
2858
2859} // namespace sat
2860} // namespace operations_research
bool AddBinaryClause(Literal a, Literal b)
Definition clause.cc:572
SatClause * ReasonClause(int trail_index) const
Definition clause.cc:219
absl::flat_hash_map< SatClause *, ClauseInfo > * mutable_clauses_info()
Definition clause.h:229
void AddClause(absl::Span< const Literal > clause)
BooleanVariable Variable() const
Definition sat_base.h:87
UpperBoundedLinearConstraint * ReasonPbConstraint(int trail_index) const
void BumpActivity(UpperBoundedLinearConstraint *constraint)
Contain the logic to decide when to restart a SAT tree search.
Definition restart.h:32
Base class for all the SAT constraints.
Definition sat_base.h:533
Status EnqueueDecisionAndBacktrackOnConflict(Literal true_literal, int *first_propagation_index=nullptr)
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
void LoadDebugSolution(absl::Span< const Literal > solution)
Status SolveWithTimeLimit(TimeLimit *time_limit)
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
bool MinimizeByPropagation(double dtime, bool minimize_new_clauses_only=false)
bool AddBinaryClauses(absl::Span< const BinaryClause > clauses)
void ProcessNewlyFixedVariables()
Simplifies the problem when new variables are assigned at level 0.
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
int64_t num_branches() const
Some statistics since the creation of the solver.
bool AddProblemClause(absl::Span< const Literal > literals)
std::vector< Literal > GetLastIncompatibleDecisions()
bool AddBinaryClause(Literal a, Literal b)
Same as AddProblemClause() below, but for small clauses.
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void Backtrack(int target_level)
const SatParameters & parameters() const
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
ABSL_MUST_USE_RESULT bool Propagate()
std::vector< Literal > GetDecisionsFixing(absl::Span< const Literal > literals)
void SetAssumptionLevel(int assumption_level)
ABSL_MUST_USE_RESULT bool AddUnitClause(Literal true_literal)
bool AddTernaryClause(Literal a, Literal b, Literal c)
void AdvanceDeterministicTime(TimeLimit *limit)
Definition sat_solver.h:478
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions, int64_t max_number_of_conflicts=-1)
const VariablesAssignment & Assignment() const
Definition sat_solver.h:390
ABSL_MUST_USE_RESULT bool ResetToLevelZero()
void AddLastPropagator(SatPropagator *propagator)
const std::vector< Decision > & Decisions() const
Definition sat_solver.h:387
ABSL_MUST_USE_RESULT bool FinishPropagation()
const Trail & LiteralTrail() const
Definition sat_solver.h:389
void SetNumVariables(int num_variables)
Definition sat_solver.cc:86
void AddPropagator(SatPropagator *propagator)
void SetParameters(const SatParameters &parameters)
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const
Definition sat_base.h:660
std::vector< Literal > * MutableConflict()
Definition sat_base.h:433
int AssignmentType(BooleanVariable var) const
Definition sat_base.h:672
absl::Span< const Literal > Reason(BooleanVariable var, int64_t conflict_id=-1) const
Definition sat_base.h:681
void EnqueueWithUnitReason(Literal true_literal)
Specific Enqueue() version for a fixed variable.
Definition sat_base.h:328
const AssignmentInfo & Info(BooleanVariable var) const
Definition sat_base.h:463
const VariablesAssignment & Assignment() const
Definition sat_base.h:462
bool VariableIsAssigned(BooleanVariable var) const
Returns true iff the given variable is assigned.
Definition sat_base.h:196
bool LiteralIsAssigned(Literal literal) const
Definition sat_base.h:191
bool LiteralIsFalse(Literal literal) const
Definition sat_base.h:185
bool LiteralIsTrue(Literal literal) const
Definition sat_base.h:188
time_limit
Definition solve.cc:22
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:55
std::string SatStatusString(SatSolver::Status status)
Returns a string representation of a SatSolver::Status.
Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound, Coefficient bound_shift, Coefficient max_value)
bool BooleanLinearExpressionIsCanonical(absl::Span< const LiteralWithCoeff > cst)
Returns true iff the Boolean linear expression is in canonical form.
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
Definition sat_solver.h:54
int MoveOneUnprocessedLiteralLast(const absl::btree_set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
Definition util.cc:388
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
In SWIG mode, we don't want anything besides these top-level includes.
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
const bool DEBUG_MODE
Definition radix_sort.h:266
std::string ProtobufShortDebugString(const P &message)
Definition proto_utils.h:46
std::string MemoryUsage()
Returns the current thread's total memory usage in an human-readable string.
Definition stats.cc:33
bool SafeAddInto(IntegerType a, IntegerType *b)
trees with all degrees equal w the current value of w
static int input(yyscan_t yyscanner)
#define IF_STATS_ENABLED(instructions)
Definition stats.h:414
#define SCOPED_TIME_STAT(stats)
Definition stats.h:421
Information about a variable assignment.
Definition sat_base.h:242
int32_t trail_index
The index of this assignment in the trail.
Definition sat_base.h:263
A binary clause. This is used by BinaryClauseManager.
Definition clause.h:405
Represents a term in a pseudo-Boolean formula.
#define SOLVER_LOG(logger,...)
Definition logging.h:110