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