OR-Tools  8.2
clause.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
14#include "ortools/sat/clause.h"
15
16#include <algorithm>
17#include <functional>
18#include <memory>
19#include <string>
20#include <vector>
21
25#include "ortools/base/timer.h"
27
28namespace operations_research {
29namespace sat {
30
31namespace {
32
33// Returns true if the given watcher list contains the given clause.
34template <typename Watcher>
35bool WatcherListContains(const std::vector<Watcher>& list,
36 const SatClause& candidate) {
37 for (const Watcher& watcher : list) {
38 if (watcher.clause == &candidate) return true;
39 }
40 return false;
41}
42
43// A simple wrapper to simplify the erase(std::remove_if()) pattern.
44template <typename Container, typename Predicate>
45void RemoveIf(Container c, Predicate p) {
46 c->erase(std::remove_if(c->begin(), c->end(), p), c->end());
47}
48
49} // namespace
50
51// ----- LiteralWatchers -----
52
54 : SatPropagator("LiteralWatchers"),
55 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
56 trail_(model->GetOrCreate<Trail>()),
57 num_inspected_clauses_(0),
58 num_inspected_clause_literals_(0),
59 num_watched_clauses_(0),
60 stats_("LiteralWatchers") {
61 trail_->RegisterPropagator(this);
62}
63
65 gtl::STLDeleteElements(&clauses_);
66 IF_STATS_ENABLED(LOG(INFO) << stats_.StatString());
67}
68
69void LiteralWatchers::Resize(int num_variables) {
70 DCHECK(is_clean_);
71 watchers_on_false_.resize(num_variables << 1);
72 reasons_.resize(num_variables);
73 needs_cleaning_.Resize(LiteralIndex(num_variables << 1));
74}
75
76// Note that this is the only place where we add Watcher so the DCHECK
77// guarantees that there are no duplicates.
78void LiteralWatchers::AttachOnFalse(Literal literal, Literal blocking_literal,
79 SatClause* clause) {
80 SCOPED_TIME_STAT(&stats_);
81 DCHECK(is_clean_);
82 DCHECK(!WatcherListContains(watchers_on_false_[literal.Index()], *clause));
83 watchers_on_false_[literal.Index()].push_back(
84 Watcher(clause, blocking_literal));
85}
86
87bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) {
88 SCOPED_TIME_STAT(&stats_);
89 DCHECK(is_clean_);
90 std::vector<Watcher>& watchers = watchers_on_false_[false_literal.Index()];
91 const VariablesAssignment& assignment = trail->Assignment();
92
93 // Note(user): It sounds better to inspect the list in order, this is because
94 // small clauses like binary or ternary clauses will often propagate and thus
95 // stay at the beginning of the list.
96 auto new_it = watchers.begin();
97 const auto end = watchers.end();
98 while (new_it != end && assignment.LiteralIsTrue(new_it->blocking_literal)) {
99 ++new_it;
100 }
101 for (auto it = new_it; it != end; ++it) {
102 // Don't even look at the clause memory if the blocking literal is true.
103 if (assignment.LiteralIsTrue(it->blocking_literal)) {
104 *new_it++ = *it;
105 continue;
106 }
107 ++num_inspected_clauses_;
108
109 // If the other watched literal is true, just change the blocking literal.
110 // Note that we use the fact that the first two literals of the clause are
111 // the ones currently watched.
112 Literal* literals = it->clause->literals();
113 const Literal other_watched_literal(
114 LiteralIndex(literals[0].Index().value() ^ literals[1].Index().value() ^
115 false_literal.Index().value()));
116 if (assignment.LiteralIsTrue(other_watched_literal)) {
117 *new_it = *it;
118 new_it->blocking_literal = other_watched_literal;
119 ++new_it;
120 ++num_inspected_clause_literals_;
121 continue;
122 }
123
124 // Look for another literal to watch. We go through the list in a cyclic
125 // fashion from start. The first two literals can be ignored as they are the
126 // watched ones.
127 {
128 const int start = it->start_index;
129 const int size = it->clause->size();
130 DCHECK_GE(start, 2);
131
132 int i = start;
133 while (i < size && assignment.LiteralIsFalse(literals[i])) ++i;
134 num_inspected_clause_literals_ += i - start + 2;
135 if (i >= size) {
136 i = 2;
137 while (i < start && assignment.LiteralIsFalse(literals[i])) ++i;
138 num_inspected_clause_literals_ += i - 2;
139 if (i >= start) i = size;
140 }
141 if (i < size) {
142 // literal[i] is unassigned or true, it's now the new literal to watch.
143 // Note that by convention, we always keep the two watched literals at
144 // the beginning of the clause.
145 literals[0] = other_watched_literal;
146 literals[1] = literals[i];
147 literals[i] = false_literal;
148 watchers_on_false_[literals[1].Index()].emplace_back(
149 it->clause, other_watched_literal, i + 1);
150 continue;
151 }
152 }
153
154 // At this point other_watched_literal is either false or unassigned, all
155 // other literals are false.
156 if (assignment.LiteralIsFalse(other_watched_literal)) {
157 // Conflict: All literals of it->clause are false.
158 //
159 // Note(user): we could avoid a copy here, but the conflict analysis
160 // complexity will be a lot higher than this anyway.
161 trail->MutableConflict()->assign(it->clause->begin(), it->clause->end());
162 trail->SetFailingSatClause(it->clause);
163 num_inspected_clause_literals_ += it - watchers.begin() + 1;
164 watchers.erase(new_it, it);
165 return false;
166 } else {
167 // Propagation: other_watched_literal is unassigned, set it to true and
168 // put it at position 0. Note that the position 0 is important because
169 // we will need later to recover the literal that was propagated from the
170 // clause using this convention.
171 literals[0] = other_watched_literal;
172 literals[1] = false_literal;
173 reasons_[trail->Index()] = it->clause;
174 trail->Enqueue(other_watched_literal, propagator_id_);
175 *new_it++ = *it;
176 }
177 }
178 num_inspected_clause_literals_ += watchers.size(); // The blocking ones.
179 watchers.erase(new_it, end);
180 return true;
181}
182
184 const int old_index = trail->Index();
185 while (trail->Index() == old_index && propagation_trail_index_ < old_index) {
186 const Literal literal = (*trail)[propagation_trail_index_++];
187 if (!PropagateOnFalse(literal.Negated(), trail)) return false;
188 }
189 return true;
190}
191
192absl::Span<const Literal> LiteralWatchers::Reason(const Trail& trail,
193 int trail_index) const {
194 return reasons_[trail_index]->PropagationReason();
195}
196
198 return reasons_[trail_index];
199}
200
201bool LiteralWatchers::AddClause(absl::Span<const Literal> literals) {
202 return AddClause(literals, trail_);
203}
204
205bool LiteralWatchers::AddClause(absl::Span<const Literal> literals,
206 Trail* trail) {
207 SatClause* clause = SatClause::Create(literals);
208 clauses_.push_back(clause);
209 return AttachAndPropagate(clause, trail);
210}
211
213 const std::vector<Literal>& literals, Trail* trail) {
214 SatClause* clause = SatClause::Create(literals);
215 clauses_.push_back(clause);
216 CHECK(AttachAndPropagate(clause, trail));
217 return clause;
218}
219
220// Sets up the 2-watchers data structure. It selects two non-false literals
221// and attaches the clause to the event: one of the watched literals become
222// false. It returns false if the clause only contains literals assigned to
223// false. If only one literals is not false, it propagates it to true if it
224// is not already assigned.
225bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) {
226 SCOPED_TIME_STAT(&stats_);
227
228 const int size = clause->size();
229 Literal* literals = clause->literals();
230
231 // Select the first two literals that are not assigned to false and put them
232 // on position 0 and 1.
233 int num_literal_not_false = 0;
234 for (int i = 0; i < size; ++i) {
235 if (!trail->Assignment().LiteralIsFalse(literals[i])) {
236 std::swap(literals[i], literals[num_literal_not_false]);
237 ++num_literal_not_false;
238 if (num_literal_not_false == 2) {
239 break;
240 }
241 }
242 }
243
244 // Returns false if all the literals were false.
245 // This should only happen on an UNSAT problem, and there is no need to attach
246 // the clause in this case.
247 if (num_literal_not_false == 0) return false;
248
249 if (num_literal_not_false == 1) {
250 // To maintain the validity of the 2-watcher algorithm, we need to watch
251 // the false literal with the highest decision level.
252 int max_level = trail->Info(literals[1].Variable()).level;
253 for (int i = 2; i < size; ++i) {
254 const int level = trail->Info(literals[i].Variable()).level;
255 if (level > max_level) {
256 max_level = level;
257 std::swap(literals[1], literals[i]);
258 }
259 }
260
261 // Propagates literals[0] if it is unassigned.
262 if (!trail->Assignment().LiteralIsTrue(literals[0])) {
263 reasons_[trail->Index()] = clause;
264 trail->Enqueue(literals[0], propagator_id_);
265 }
266 }
267
268 ++num_watched_clauses_;
269 AttachOnFalse(literals[0], literals[1], clause);
270 AttachOnFalse(literals[1], literals[0], clause);
271 return true;
272}
273
275 Literal* literals = clause->literals();
276 CHECK(!trail->Assignment().LiteralIsAssigned(literals[0]));
277 CHECK(!trail->Assignment().LiteralIsAssigned(literals[1]));
278
279 ++num_watched_clauses_;
280 AttachOnFalse(literals[0], literals[1], clause);
281 AttachOnFalse(literals[1], literals[0], clause);
282}
283
284void LiteralWatchers::InternalDetach(SatClause* clause) {
285 --num_watched_clauses_;
286 const size_t size = clause->size();
287 if (drat_proof_handler_ != nullptr && size > 2) {
288 drat_proof_handler_->DeleteClause({clause->begin(), size});
289 }
290 clauses_info_.erase(clause);
291 clause->Clear();
292}
293
295 InternalDetach(clause);
296 is_clean_ = false;
297 needs_cleaning_.Set(clause->FirstLiteral().Index());
298 needs_cleaning_.Set(clause->SecondLiteral().Index());
299}
300
302 InternalDetach(clause);
303 for (const Literal l : {clause->FirstLiteral(), clause->SecondLiteral()}) {
304 needs_cleaning_.Clear(l.Index());
305 RemoveIf(&(watchers_on_false_[l.Index()]), [](const Watcher& watcher) {
306 return !watcher.clause->IsAttached();
307 });
308 }
309}
310
312 if (!all_clauses_are_attached_) return;
313 all_clauses_are_attached_ = false;
314
315 // This is easy, and this allows to reset memory if some watcher lists where
316 // really long at some point.
317 is_clean_ = true;
318 num_watched_clauses_ = 0;
319 watchers_on_false_.clear();
320}
321
323 if (all_clauses_are_attached_) return;
324 all_clauses_are_attached_ = true;
325
326 needs_cleaning_.ClearAll(); // This doesn't resize it.
327 watchers_on_false_.resize(needs_cleaning_.size().value());
328
330 for (SatClause* clause : clauses_) {
331 ++num_watched_clauses_;
332 CHECK_GE(clause->size(), 2);
333 AttachOnFalse(clause->FirstLiteral(), clause->SecondLiteral(), clause);
334 AttachOnFalse(clause->SecondLiteral(), clause->FirstLiteral(), clause);
335 }
336}
337
338// This one do not need the clause to be detached.
340 CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
341 if (drat_proof_handler_ != nullptr) {
342 drat_proof_handler_->AddClause({true_literal});
343 }
344 // TODO(user): remove the test when the DRAT issue with fixed literal is
345 // resolved.
346 if (!trail_->Assignment().LiteralIsTrue(true_literal)) {
347 trail_->EnqueueWithUnitReason(true_literal);
348
349 // Even when all clauses are detached, we can propagate the implication
350 // graph and we do that right away.
351 return implication_graph_->Propagate(trail_);
352 }
353 return true;
354}
355
356// TODO(user): We could do something slower if the clauses are attached like
357// we do for InprocessingRewriteClause().
359 CHECK(!all_clauses_are_attached_);
360 if (drat_proof_handler_ != nullptr) {
361 drat_proof_handler_->DeleteClause(clause->AsSpan());
362 }
363 clauses_info_.erase(clause);
364 clause->Clear();
365}
366
368 SatClause* clause, absl::Span<const Literal> new_clause) {
369 if (new_clause.empty()) return false; // UNSAT.
370
371 if (DEBUG_MODE) {
372 for (const Literal l : new_clause) {
373 CHECK(!trail_->Assignment().LiteralIsAssigned(l));
374 }
375 }
376
377 if (new_clause.size() == 1) {
378 if (!InprocessingFixLiteral(new_clause[0])) return false;
380 return true;
381 }
382
383 if (new_clause.size() == 2) {
384 implication_graph_->AddBinaryClause(new_clause[0], new_clause[1]);
386 return true;
387 }
388
389 if (drat_proof_handler_ != nullptr) {
390 // We must write the new clause before we delete the old one.
391 drat_proof_handler_->AddClause(new_clause);
392 drat_proof_handler_->DeleteClause(clause->AsSpan());
393 }
394
395 if (all_clauses_are_attached_) {
396 // We can still rewrite the clause, but it is inefficient. We first
397 // detach it in a non-lazy way.
398 --num_watched_clauses_;
399 clause->Clear();
400 for (const Literal l : {clause->FirstLiteral(), clause->SecondLiteral()}) {
401 needs_cleaning_.Clear(l.Index());
402 RemoveIf(&(watchers_on_false_[l.Index()]), [](const Watcher& watcher) {
403 return !watcher.clause->IsAttached();
404 });
405 }
406 }
407
408 clause->Rewrite(new_clause);
409
410 // And we re-attach it.
411 if (all_clauses_are_attached_) Attach(clause, trail_);
412 return true;
413}
414
416 absl::Span<const Literal> new_clause) {
417 CHECK(!new_clause.empty());
418 CHECK(!all_clauses_are_attached_);
419 if (DEBUG_MODE) {
420 for (const Literal l : new_clause) {
421 CHECK(!trail_->Assignment().LiteralIsAssigned(l));
422 }
423 }
424
425 if (new_clause.size() == 1) {
426 // TODO(user): We should return false...
427 if (!InprocessingFixLiteral(new_clause[0])) return nullptr;
428 return nullptr;
429 }
430
431 if (new_clause.size() == 2) {
432 implication_graph_->AddBinaryClause(new_clause[0], new_clause[1]);
433 return nullptr;
434 }
435
436 SatClause* clause = SatClause::Create(new_clause);
437 clauses_.push_back(clause);
438 return clause;
439}
440
442 SCOPED_TIME_STAT(&stats_);
443 for (LiteralIndex index : needs_cleaning_.PositionsSetAtLeastOnce()) {
444 DCHECK(needs_cleaning_[index]);
445 RemoveIf(&(watchers_on_false_[index]), [](const Watcher& watcher) {
446 return !watcher.clause->IsAttached();
447 });
448 needs_cleaning_.Clear(index);
449 }
450 needs_cleaning_.NotifyAllClear();
451 is_clean_ = true;
452}
453
455 DCHECK(is_clean_);
456
457 // Update to_minimize_index_.
458 if (to_minimize_index_ >= clauses_.size()) {
459 to_minimize_index_ = clauses_.size();
460 }
461 to_minimize_index_ =
462 std::stable_partition(clauses_.begin(),
463 clauses_.begin() + to_minimize_index_,
464 [](SatClause* a) { return a->IsAttached(); }) -
465 clauses_.begin();
466
467 // Do the proper deletion.
468 std::vector<SatClause*>::iterator iter =
469 std::stable_partition(clauses_.begin(), clauses_.end(),
470 [](SatClause* a) { return a->IsAttached(); });
471 gtl::STLDeleteContainerPointers(iter, clauses_.end());
472 clauses_.erase(iter, clauses_.end());
473}
474
475// ----- BinaryImplicationGraph -----
476
477void BinaryImplicationGraph::Resize(int num_variables) {
478 SCOPED_TIME_STAT(&stats_);
479 implications_.resize(num_variables << 1);
480 is_redundant_.resize(implications_.size(), false);
481 is_removed_.resize(implications_.size(), false);
482 estimated_sizes_.resize(implications_.size(), 0);
483 in_direct_implications_.resize(implications_.size(), false);
484 reasons_.resize(num_variables);
485}
486
487// TODO(user): Not all of the solver knows about representative literal, do
488// use them here and in AddBinaryClauseDuringSearch() to maintains invariant?
489// Explore this when we start cleaning our clauses using equivalence during
490// search. We can easily do it for every conflict we learn instead of here.
492 SCOPED_TIME_STAT(&stats_);
493 if (drat_proof_handler_ != nullptr) {
494 // TODO(user): Like this we will duplicate all binary clause from the
495 // problem. However this leads to a simpler API (since we don't need to
496 // special case the loading of the original clauses) and we mainly use drat
497 // proof for testing anyway.
498 drat_proof_handler_->AddClause({a, b});
499 }
500 estimated_sizes_[a.NegatedIndex()]++;
501 estimated_sizes_[b.NegatedIndex()]++;
502 implications_[a.NegatedIndex()].push_back(b);
503 implications_[b.NegatedIndex()].push_back(a);
504 is_dag_ = false;
505 num_implications_ += 2;
506}
507
509 SCOPED_TIME_STAT(&stats_);
510 if (num_implications_ == 0) propagation_trail_index_ = trail_->Index();
512
513 const auto& assignment = trail_->Assignment();
514 if (assignment.LiteralIsFalse(a)) {
515 if (assignment.LiteralIsAssigned(b)) {
516 if (assignment.LiteralIsFalse(b)) return false;
517 } else {
518 reasons_[trail_->Index()] = a;
519 trail_->Enqueue(b, propagator_id_);
520 }
521 } else if (assignment.LiteralIsFalse(b)) {
522 if (!assignment.LiteralIsAssigned(a)) {
523 reasons_[trail_->Index()] = b;
524 trail_->Enqueue(a, propagator_id_);
525 }
526 }
527 is_dag_ = false;
528 return true;
529}
530
532 absl::Span<const Literal> at_most_one) {
533 CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
534 if (at_most_one.size() <= 1) return true;
535
536 // Temporarily copy the at_most_one constraint at the end of
537 // at_most_one_buffer_. It will be cleaned up and added by
538 // CleanUpAndAddAtMostOnes().
539 const int base_index = at_most_one_buffer_.size();
540 at_most_one_buffer_.insert(at_most_one_buffer_.end(), at_most_one.begin(),
541 at_most_one.end());
542 at_most_one_buffer_.push_back(Literal(kNoLiteralIndex));
543
544 is_dag_ = false;
545 return CleanUpAndAddAtMostOnes(base_index);
546}
547
548// TODO(user): remove duplication with
549// LiteralWatchers::InprocessingFixLiteral();
550bool BinaryImplicationGraph::FixLiteral(Literal true_literal) {
551 if (trail_->Assignment().LiteralIsTrue(true_literal)) return true;
552 if (trail_->Assignment().LiteralIsFalse(true_literal)) return false;
553
554 if (drat_proof_handler_ != nullptr) {
555 drat_proof_handler_->AddClause({true_literal});
556 }
557
558 trail_->EnqueueWithUnitReason(true_literal);
559 return Propagate(trail_);
560}
561
562// This works by doing a linear scan on the at_most_one_buffer_ and
563// cleaning/copying the at most ones on the fly to the beginning of the same
564// buffer.
565bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(const int base_index) {
566 const VariablesAssignment& assignment = trail_->Assignment();
567 int local_end = base_index;
568 const int buffer_size = at_most_one_buffer_.size();
569 for (int i = base_index; i < buffer_size; ++i) {
570 if (at_most_one_buffer_[i].Index() == kNoLiteralIndex) continue;
571
572 // Process a new at most one.
573 // It will be copied into buffer[local_start, local_end].
574 const int local_start = local_end;
575 bool set_all_left_to_false = false;
576 for (;; ++i) {
577 const Literal l = at_most_one_buffer_[i];
578 if (l.Index() == kNoLiteralIndex) break;
579 if (assignment.LiteralIsFalse(l)) continue;
580 if (is_removed_[l.Index()]) continue;
581 if (!set_all_left_to_false && assignment.LiteralIsTrue(l)) {
582 set_all_left_to_false = true;
583 continue;
584 }
585 at_most_one_buffer_[local_end++] = RepresentativeOf(l);
586 }
587
588 // Deal with all false.
589 if (set_all_left_to_false) {
590 for (int j = local_start; j < local_end; ++j) {
591 const Literal l = at_most_one_buffer_[j];
592 if (assignment.LiteralIsFalse(l)) continue;
593 if (assignment.LiteralIsTrue(l)) return false;
594 if (!FixLiteral(l.Negated())) return false;
595 }
596 local_end = local_start;
597 continue;
598 }
599
600 // Deal with duplicates.
601 // Any duplicate in an "at most one" must be false.
602 {
603 int new_local_end = local_start;
604 std::sort(&at_most_one_buffer_[local_start],
605 &at_most_one_buffer_[local_end]);
606 for (int j = local_start; j < local_end; ++j) {
607 const Literal l = at_most_one_buffer_[j];
608 if (new_local_end > local_start &&
609 l == at_most_one_buffer_[new_local_end - 1]) {
610 if (assignment.LiteralIsTrue(l)) return false;
611 if (!assignment.LiteralIsFalse(l)) {
612 if (!FixLiteral(l.Negated())) return false;
613 }
614 --new_local_end;
615 continue;
616 }
617 at_most_one_buffer_[new_local_end++] = l;
618 }
619 local_end = new_local_end;
620 }
621
622 // Create a Span<> to simplify the code below.
623 const absl::Span<const Literal> at_most_one(
624 &at_most_one_buffer_[local_start], local_end - local_start);
625
626 // We expand small sizes into implications.
627 // TODO(user): Investigate what the best threshold is.
628 if (at_most_one.size() < 10) {
629 // Note that his automatically skip size 0 and 1.
630 for (const Literal a : at_most_one) {
631 for (const Literal b : at_most_one) {
632 if (a == b) continue;
633 implications_[a.Index()].push_back(b.Negated());
634 }
635 }
636 num_implications_ += at_most_one.size() * (at_most_one.size() - 1);
637
638 // This will erase the at_most_one from the buffer.
639 local_end = local_start;
640 continue;
641 }
642
643 // Index the new at most one.
644 for (const Literal l : at_most_one) {
645 if (l.Index() >= at_most_ones_.size()) {
646 at_most_ones_.resize(l.Index().value() + 1);
647 }
648 CHECK(!is_redundant_[l.Index()]);
649 at_most_ones_[l.Index()].push_back(local_start);
650 }
651
652 // Add sentinel.
653 at_most_one_buffer_[local_end++] = Literal(kNoLiteralIndex);
654 }
655
656 at_most_one_buffer_.resize(local_end);
657 return true;
658}
659
660bool BinaryImplicationGraph::PropagateOnTrue(Literal true_literal,
661 Trail* trail) {
662 SCOPED_TIME_STAT(&stats_);
663
664 const VariablesAssignment& assignment = trail->Assignment();
665 DCHECK(assignment.LiteralIsTrue(true_literal));
666
667 // Note(user): This update is not exactly correct because in case of conflict
668 // we don't inspect that much clauses. But doing ++num_inspections_ inside the
669 // loop does slow down the code by a few percent.
670 num_inspections_ += implications_[true_literal.Index()].size();
671
672 for (Literal literal : implications_[true_literal.Index()]) {
673 if (assignment.LiteralIsTrue(literal)) {
674 // Note(user): I tried to update the reason here if the literal was
675 // enqueued after the true_literal on the trail. This property is
676 // important for ComputeFirstUIPConflict() to work since it needs the
677 // trail order to be a topological order for the deduction graph.
678 // But the performance was not too good...
679 continue;
680 }
681
682 ++num_propagations_;
683 if (assignment.LiteralIsFalse(literal)) {
684 // Conflict.
685 *(trail->MutableConflict()) = {true_literal.Negated(), literal};
686 return false;
687 } else {
688 // Propagation.
689 reasons_[trail->Index()] = true_literal.Negated();
690 trail->Enqueue(literal, propagator_id_);
691 }
692 }
693
694 // Propagate the at_most_one constraints.
695 if (true_literal.Index() < at_most_ones_.size()) {
696 for (const int start : at_most_ones_[true_literal.Index()]) {
697 bool seen = false;
698 for (int i = start;; ++i) {
699 const Literal literal = at_most_one_buffer_[i];
700 if (literal.Index() == kNoLiteralIndex) break;
701
702 ++num_inspections_;
703 if (literal == true_literal) {
704 if (DEBUG_MODE) {
705 CHECK(!seen);
706 seen = true;
707 }
708 continue;
709 }
710 if (assignment.LiteralIsFalse(literal)) continue;
711
712 ++num_propagations_;
713 if (assignment.LiteralIsTrue(literal)) {
714 // Conflict.
715 *(trail->MutableConflict()) = {true_literal.Negated(),
716 literal.Negated()};
717 return false;
718 } else {
719 // Propagation.
720 reasons_[trail->Index()] = true_literal.Negated();
721 trail->Enqueue(literal.Negated(), propagator_id_);
722 }
723 }
724 }
725 }
726
727 return true;
728}
729
731 if (IsEmpty()) {
733 return true;
734 }
735 while (propagation_trail_index_ < trail->Index()) {
736 const Literal literal = (*trail)[propagation_trail_index_++];
737 if (!PropagateOnTrue(literal, trail)) return false;
738 }
739 return true;
740}
741
742absl::Span<const Literal> BinaryImplicationGraph::Reason(
743 const Trail& trail, int trail_index) const {
744 return {&reasons_[trail_index], 1};
745}
746
747// Here, we remove all the literal whose negation are implied by the negation of
748// the 1-UIP literal (which always appear first in the given conflict). Note
749// that this algorithm is "optimal" in the sense that it leads to a minimized
750// conflict with a backjump level as low as possible. However, not all possible
751// literals are removed.
752//
753// TODO(user): Also consider at most one?
755 std::vector<Literal>* conflict) {
756 SCOPED_TIME_STAT(&stats_);
757 dfs_stack_.clear();
758
759 // Compute the reachability from the literal "not(conflict->front())" using
760 // an iterative dfs.
761 const LiteralIndex root_literal_index = conflict->front().NegatedIndex();
762 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
763 is_marked_.Set(root_literal_index);
764
765 // TODO(user): This sounds like a good idea, but somehow it seems better not
766 // to do that even though it is almost for free. Investigate more.
767 //
768 // The idea here is that since we already compute the reachability from the
769 // root literal, we can use this computation to remove any implication
770 // root_literal => b if there is already root_literal => a and b is reachable
771 // from a.
772 const bool also_prune_direct_implication_list = false;
773
774 // We treat the direct implications differently so we can also remove the
775 // redundant implications from this list at the same time.
776 auto& direct_implications = implications_[root_literal_index];
777 for (const Literal l : direct_implications) {
778 if (is_marked_[l.Index()]) continue;
779 dfs_stack_.push_back(l);
780 while (!dfs_stack_.empty()) {
781 const LiteralIndex index = dfs_stack_.back().Index();
782 dfs_stack_.pop_back();
783 if (!is_marked_[index]) {
784 is_marked_.Set(index);
785 for (Literal implied : implications_[index]) {
786 if (!is_marked_[implied.Index()]) dfs_stack_.push_back(implied);
787 }
788 }
789 }
790
791 // The "trick" is to unmark 'l'. This way, if we explore it twice, it means
792 // that this l is reachable from some other 'l' from the direct implication
793 // list. Remarks:
794 // - We don't loose too much complexity when this happen since a literal
795 // can be unmarked only once, so in the worst case we loop twice over its
796 // children. Moreover, this literal will be pruned for later calls.
797 // - This is correct, i.e. we can't prune too many literals because of a
798 // strongly connected component. Proof by contradiction: If we take the
799 // first (in direct_implications) literal from a removed SCC, it must
800 // have marked all the others. But because they are marked, they will not
801 // be explored again and so can't mark the first literal.
802 if (also_prune_direct_implication_list) {
803 is_marked_.Clear(l.Index());
804 }
805 }
806
807 // Now we can prune the direct implications list and make sure are the
808 // literals there are marked.
809 if (also_prune_direct_implication_list) {
810 int new_size = 0;
811 for (const Literal l : direct_implications) {
812 if (!is_marked_[l.Index()]) {
813 is_marked_.Set(l.Index());
814 direct_implications[new_size] = l;
815 ++new_size;
816 }
817 }
818 if (new_size < direct_implications.size()) {
819 num_redundant_implications_ += direct_implications.size() - new_size;
820 direct_implications.resize(new_size);
821 }
822 }
823
824 RemoveRedundantLiterals(conflict);
825}
826
827// Same as MinimizeConflictWithReachability() but also mark (in the given
828// SparseBitset) the reachable literal already assigned to false. These literals
829// will be implied if the 1-UIP literal is assigned to false, and the classic
830// minimization algorithm can take advantage of that.
832 const Trail& trail, std::vector<Literal>* conflict,
834 SCOPED_TIME_STAT(&stats_);
835 CHECK(!conflict->empty());
836 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
837 MarkDescendants(conflict->front().Negated());
838 for (const LiteralIndex i : is_marked_.PositionsSetAtLeastOnce()) {
839 if (trail.Assignment().LiteralIsFalse(Literal(i))) {
840 marked->Set(Literal(i).Variable());
841 }
842 }
843 RemoveRedundantLiterals(conflict);
844}
845
846// Same as MinimizeConflictFirst() but take advantage of this reachability
847// computation to remove redundant implication in the implication list of the
848// first UIP conflict.
850 const Trail& trail, std::vector<Literal>* conflict,
851 SparseBitset<BooleanVariable>* marked, absl::BitGenRef random) {
852 SCOPED_TIME_STAT(&stats_);
853 const LiteralIndex root_literal_index = conflict->front().NegatedIndex();
854 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
855 is_marked_.Set(root_literal_index);
856
857 int new_size = 0;
858 auto& direct_implications = implications_[root_literal_index];
859
860 // The randomization allow to find more redundant implication since to find
861 // a => b and remove b, a must be before b in direct_implications. Note that
862 // a std::reverse() could work too. But randomization seems to work better.
863 // Probably because it has other impact on the search tree.
864 std::shuffle(direct_implications.begin(), direct_implications.end(), random);
865 dfs_stack_.clear();
866 for (const Literal l : direct_implications) {
867 if (is_marked_[l.Index()]) {
868 // The literal is already marked! so it must be implied by one of the
869 // previous literal in the direct_implications list. We can safely remove
870 // it.
871 continue;
872 }
873 direct_implications[new_size++] = l;
874 dfs_stack_.push_back(l);
875 while (!dfs_stack_.empty()) {
876 const LiteralIndex index = dfs_stack_.back().Index();
877 dfs_stack_.pop_back();
878 if (!is_marked_[index]) {
879 is_marked_.Set(index);
880 for (Literal implied : implications_[index]) {
881 if (!is_marked_[implied.Index()]) dfs_stack_.push_back(implied);
882 }
883 }
884 }
885 }
886 if (new_size < direct_implications.size()) {
887 num_redundant_implications_ += direct_implications.size() - new_size;
888 direct_implications.resize(new_size);
889 }
890 RemoveRedundantLiterals(conflict);
891}
892
893void BinaryImplicationGraph::RemoveRedundantLiterals(
894 std::vector<Literal>* conflict) {
895 SCOPED_TIME_STAT(&stats_);
896 int new_index = 1;
897 for (int i = 1; i < conflict->size(); ++i) {
898 if (!is_marked_[(*conflict)[i].NegatedIndex()]) {
899 (*conflict)[new_index] = (*conflict)[i];
900 ++new_index;
901 }
902 }
903 if (new_index < conflict->size()) {
904 ++num_minimization_;
905 num_literals_removed_ += conflict->size() - new_index;
906 conflict->resize(new_index);
907 }
908}
909
910// TODO(user): Also consider at most one?
912 const Trail& trail, std::vector<Literal>* conflict) {
913 SCOPED_TIME_STAT(&stats_);
914 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
915 is_simplified_.ClearAndResize(LiteralIndex(implications_.size()));
916 for (Literal lit : *conflict) {
917 is_marked_.Set(lit.Index());
918 }
919
920 // Identify and remove the redundant literals from the given conflict.
921 // 1/ If a -> b then a can be removed from the conflict clause.
922 // This is because not b -> not a.
923 // 2/ a -> b can only happen if level(a) <= level(b).
924 // 3/ Because of 2/, cycles can appear only at the same level.
925 // The vector is_simplified_ is used to avoid removing all elements of a
926 // cycle. Note that this is not optimal in the sense that we may not remove
927 // a literal that can be removed.
928 //
929 // Note that there is no need to explore the unique literal of the highest
930 // decision level since it can't be removed. Because this is a conflict, such
931 // literal is always at position 0, so we start directly at 1.
932 int index = 1;
933 for (int i = 1; i < conflict->size(); ++i) {
934 const Literal lit = (*conflict)[i];
935 const int lit_level = trail.Info(lit.Variable()).level;
936 bool keep_literal = true;
937 for (Literal implied : implications_[lit.Index()]) {
938 if (is_marked_[implied.Index()]) {
939 DCHECK_LE(lit_level, trail.Info(implied.Variable()).level);
940 if (lit_level == trail.Info(implied.Variable()).level &&
941 is_simplified_[implied.Index()]) {
942 continue;
943 }
944 keep_literal = false;
945 break;
946 }
947 }
948 if (keep_literal) {
949 (*conflict)[index] = lit;
950 ++index;
951 } else {
952 is_simplified_.Set(lit.Index());
953 }
954 }
955 if (index < conflict->size()) {
956 ++num_minimization_;
957 num_literals_removed_ += conflict->size() - index;
958 conflict->erase(conflict->begin() + index, conflict->end());
959 }
960}
961
963 SCOPED_TIME_STAT(&stats_);
964 CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
965
966 // Nothing to do if nothing changed since last call.
967 const int new_num_fixed = trail_->Index();
968 if (num_processed_fixed_variables_ == new_num_fixed) return;
969
970 const VariablesAssignment& assignment = trail_->Assignment();
971 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
972 for (; num_processed_fixed_variables_ < new_num_fixed;
973 ++num_processed_fixed_variables_) {
974 const Literal true_literal = (*trail_)[num_processed_fixed_variables_];
975 if (DEBUG_MODE) {
976 // The code assumes that everything is already propagated.
977 // Otherwise we will remove implications that didn't propagate yet!
978 for (const Literal lit : implications_[true_literal.Index()]) {
979 CHECK(trail_->Assignment().LiteralIsTrue(lit));
980 }
981 }
982
983 // If b is true and a -> b then because not b -> not a, all the
984 // implications list that contains b will be marked by this process.
985 // And the ones that contains not(b) should correspond to a false literal!
986 //
987 // TODO(user): This might not be true if we remove implication by
988 // transitive reduction and the process was aborted due to the computation
989 // limit. I think it will be good to maintain that invariant though,
990 // otherwise fixed literals might never be removed from these lists...
991 for (const Literal lit : implications_[true_literal.NegatedIndex()]) {
992 is_marked_.Set(lit.NegatedIndex());
993 }
994 gtl::STLClearObject(&(implications_[true_literal.Index()]));
995 gtl::STLClearObject(&(implications_[true_literal.NegatedIndex()]));
996
997 if (true_literal.Index() < at_most_ones_.size()) {
998 gtl::STLClearObject(&(at_most_ones_[true_literal.Index()]));
999 }
1000 if (true_literal.NegatedIndex() < at_most_ones_.size()) {
1001 gtl::STLClearObject(&(at_most_ones_[true_literal.NegatedIndex()]));
1002 }
1003 }
1004 for (const LiteralIndex i : is_marked_.PositionsSetAtLeastOnce()) {
1005 RemoveIf(&implications_[i], [&assignment](const Literal& lit) {
1006 return assignment.LiteralIsTrue(lit);
1007 });
1008 }
1009
1010 // TODO(user): This might be a bit slow. Do not call all the time if needed,
1011 // this shouldn't change the correctness of the code.
1012 at_most_ones_.clear();
1013 CleanUpAndAddAtMostOnes(/*base_index=*/0);
1014}
1015
1017 public:
1024 std::vector<std::vector<int32>>>;
1025
1026 explicit SccGraph(SccFinder* finder, Implication* graph,
1027 AtMostOne* at_most_ones,
1028 std::vector<Literal>* at_most_one_buffer)
1029 : finder_(*finder),
1030 implications_(*graph),
1031 at_most_ones_(*at_most_ones),
1032 at_most_one_buffer_(*at_most_one_buffer) {}
1033
1034 const std::vector<int32>& operator[](int32 node) const {
1035 tmp_.clear();
1036 for (const Literal l : implications_[LiteralIndex(node)]) {
1037 tmp_.push_back(l.Index().value());
1038 if (finder_.NodeIsInCurrentDfsPath(l.NegatedIndex().value())) {
1039 to_fix_.push_back(l);
1040 }
1041 }
1042 if (node < at_most_ones_.size()) {
1043 for (const int start : at_most_ones_[LiteralIndex(node)]) {
1044 if (start >= at_most_one_already_explored_.size()) {
1045 at_most_one_already_explored_.resize(start + 1, false);
1046 previous_node_to_explore_at_most_one_.resize(start + 1);
1047 }
1048
1049 // In the presence of at_most_ones_ contraints, expanding them
1050 // implicitely to implications in the SCC computation can result in a
1051 // quadratic complexity rather than a linear one in term of the input
1052 // data structure size. So this test here is critical on problem with
1053 // large at_most ones like the "ivu06-big.mps.gz" where without it, the
1054 // full FindStronglyConnectedComponents() take more than on hour instead
1055 // of less than a second!
1056 if (at_most_one_already_explored_[start]) {
1057 // We never expand a node twice.
1058 const int first_node = previous_node_to_explore_at_most_one_[start];
1059 CHECK_NE(node, first_node);
1060
1061 if (finder_.NodeIsInCurrentDfsPath(first_node)) {
1062 // If the first node is not settled, then we do explore the
1063 // at_most_one constraint again. In "Mixed-Integer-Programming:
1064 // Analyzing 12 years of progress", Tobias Achterberg and Roland
1065 // Wunderling explains that an at most one need to be looped over at
1066 // most twice. I am not sure exactly how that works, so for now we
1067 // are not fully linear, but on actual instances, we only rarely
1068 // run into this case.
1069 //
1070 // Note that we change the previous node to explore at most one
1071 // since the current node will be settled before the old ones.
1072 //
1073 // TODO(user): avoid looping more than twice on the same at most one
1074 // constraints? Note that the second time we loop we have x => y =>
1075 // not(x), so we can already detect that x must be false which we
1076 // detect below.
1077 previous_node_to_explore_at_most_one_[start] = node;
1078 } else {
1079 // The first node is already settled and so are all its child. Only
1080 // not(first_node) might still need exploring.
1081 tmp_.push_back(
1082 Literal(LiteralIndex(first_node)).NegatedIndex().value());
1083 continue;
1084 }
1085 } else {
1086 at_most_one_already_explored_[start] = true;
1087 previous_node_to_explore_at_most_one_[start] = node;
1088 }
1089
1090 for (int i = start;; ++i) {
1091 const Literal l = at_most_one_buffer_[i];
1092 if (l.Index() == kNoLiteralIndex) break;
1093 if (l.Index() == node) continue;
1094 tmp_.push_back(l.NegatedIndex().value());
1095 if (finder_.NodeIsInCurrentDfsPath(l.Index().value())) {
1096 to_fix_.push_back(l.Negated());
1097 }
1098 }
1099 }
1100 }
1101 work_done_ += tmp_.size();
1102 return tmp_;
1103 }
1104
1105 // All these literals where detected to be true during the SCC computation.
1106 mutable std::vector<Literal> to_fix_;
1107
1108 // For the deterministic time.
1109 mutable int64 work_done_ = 0;
1110
1111 private:
1112 const SccFinder& finder_;
1113 const Implication& implications_;
1114 const AtMostOne& at_most_ones_;
1115 const std::vector<Literal>& at_most_one_buffer_;
1116
1117 mutable std::vector<int32> tmp_;
1118
1119 // Used to get a non-quadratic complexity in the presence of at most ones.
1120 mutable std::vector<bool> at_most_one_already_explored_;
1121 mutable std::vector<int> previous_node_to_explore_at_most_one_;
1122};
1123
1125 // This was already called, and no new constraint where added. Note that new
1126 // fixed variable cannote create new equivalence, only new binary clauses do.
1127 if (is_dag_) return true;
1129 wall_timer.Start();
1130 log_info |= VLOG_IS_ON(1);
1131
1132 // Lets remove all fixed variables first.
1133 if (!Propagate(trail_)) return false;
1135 const VariablesAssignment& assignment = trail_->Assignment();
1136
1137 // TODO(user): We could just do it directly though.
1138 int num_fixed_during_scc = 0;
1139 const int32 size(implications_.size());
1140 std::vector<std::vector<int32>> scc;
1141 double dtime = 0.0;
1142 {
1143 SccGraph::SccFinder finder;
1144 SccGraph graph(&finder, &implications_, &at_most_ones_,
1145 &at_most_one_buffer_);
1146 finder.FindStronglyConnectedComponents(size, graph, &scc);
1147 dtime += 4e-8 * graph.work_done_;
1148
1149 for (const Literal l : graph.to_fix_) {
1150 if (assignment.LiteralIsFalse(l)) return false;
1151 if (assignment.LiteralIsTrue(l)) continue;
1152 ++num_fixed_during_scc;
1153 if (!FixLiteral(l)) return false;
1154 }
1155 }
1156
1157 // The old values will still be valid.
1158 representative_of_.resize(size, kNoLiteralIndex);
1159 is_redundant_.resize(size, false);
1160
1161 int num_equivalences = 0;
1162 reverse_topological_order_.clear();
1163 for (std::vector<int32>& component : scc) {
1164 // If one is fixed then all must be fixed. Note that the reason why the
1165 // propagation didn't already do that and we don't always get fixed
1166 // component of size 1 is because of the potential newly fixed literals
1167 // above.
1168 //
1169 // In any case, all fixed literals are marked as redundant.
1170 {
1171 bool all_fixed = false;
1172 bool all_true = false;
1173 for (const int32 i : component) {
1174 const Literal l = Literal(LiteralIndex(i));
1175 if (trail_->Assignment().LiteralIsAssigned(l)) {
1176 all_fixed = true;
1177 all_true = trail_->Assignment().LiteralIsTrue(l);
1178 break;
1179 }
1180 }
1181 if (all_fixed) {
1182 for (const int32 i : component) {
1183 const Literal l = Literal(LiteralIndex(i));
1184 if (!is_redundant_[l.Index()]) {
1185 ++num_redundant_literals_;
1186 is_redundant_[l.Index()] = true;
1187 }
1188 const Literal to_fix = all_true ? l : l.Negated();
1189 if (assignment.LiteralIsFalse(to_fix)) return false;
1190 if (assignment.LiteralIsTrue(to_fix)) continue;
1191 ++num_fixed_during_scc;
1192 if (!FixLiteral(l)) return false;
1193 }
1194
1195 // Next component.
1196 continue;
1197 }
1198 }
1199
1200 // We ignore variable that appear in no constraints.
1201 if (component.size() == 1 && is_removed_[LiteralIndex(component[0])]) {
1202 continue;
1203 }
1204
1205 // We always take the smallest literal index (which also corresponds to the
1206 // smallest BooleanVariable index) as a representative. This make sure that
1207 // the representative of a literal l and the one of not(l) will be the
1208 // negation of each other. There is also reason to think that it is
1209 // heuristically better to use a BooleanVariable that was created first.
1210 std::sort(component.begin(), component.end());
1211 const LiteralIndex representative(component[0]);
1212 reverse_topological_order_.push_back(representative);
1213
1214 if (component.size() == 1) {
1215 // Note that because we process list in reverse topological order, this
1216 // is only needed if there is any equivalence before this point.
1217 if (num_equivalences > 0) {
1218 auto& representative_list = implications_[representative];
1219 for (Literal& ref : representative_list) {
1220 const LiteralIndex rep = representative_of_[ref.Index()];
1221 if (rep == representative) continue;
1222 if (rep == kNoLiteralIndex) continue;
1223 ref = Literal(rep);
1224 }
1225 gtl::STLSortAndRemoveDuplicates(&representative_list);
1226 }
1227 continue;
1228 }
1229
1230 // Sets the representative.
1231 for (int i = 1; i < component.size(); ++i) {
1232 const Literal literal = Literal(LiteralIndex(component[i]));
1233 if (!is_redundant_[literal.Index()]) {
1234 ++num_redundant_literals_;
1235 is_redundant_[literal.Index()] = true;
1236 }
1237 representative_of_[literal.Index()] = representative;
1238
1239 // Detect if x <=> not(x) which means unsat. Note that we relly on the
1240 // fact that when sorted, they will both be consecutive in the list.
1241 if (Literal(LiteralIndex(component[i - 1])).Negated() == literal) {
1242 LOG_IF(INFO, log_info) << "Trivially UNSAT in DetectEquivalences()";
1243 return false;
1244 }
1245 }
1246
1247 // Merge all the lists in implications_[representative].
1248 // Note that we do not want representative in its own list.
1249 auto& representative_list = implications_[representative];
1250 int new_size = 0;
1251 for (const Literal l : representative_list) {
1252 const Literal rep = RepresentativeOf(l);
1253 if (rep.Index() == representative) continue;
1254 representative_list[new_size++] = rep;
1255 }
1256 representative_list.resize(new_size);
1257 for (int i = 1; i < component.size(); ++i) {
1258 const Literal literal = Literal(LiteralIndex(component[i]));
1259 auto& ref = implications_[literal.Index()];
1260 for (const Literal l : ref) {
1261 const Literal rep = RepresentativeOf(l);
1262 if (rep.Index() != representative) representative_list.push_back(rep);
1263 }
1264
1265 // Add representative <=> literal.
1266 //
1267 // Remark: this relation do not need to be added to a DRAT proof since
1268 // the redundant variables should never be used again for a pure SAT
1269 // problem.
1270 representative_list.push_back(literal);
1271 ref.clear();
1272 ref.push_back(Literal(representative));
1273 }
1274 gtl::STLSortAndRemoveDuplicates(&representative_list);
1275 num_equivalences += component.size() - 1;
1276 }
1277
1278 is_dag_ = true;
1279 if (num_equivalences != 0) {
1280 // Remap all at most ones. Remove fixed variables, process duplicates. Note
1281 // that this might result in more implications when we expand small at most
1282 // one.
1283 at_most_ones_.clear();
1284 CleanUpAndAddAtMostOnes(/*base_index=*/0);
1285
1286 num_implications_ = 0;
1287 for (LiteralIndex i(0); i < size; ++i) {
1288 num_implications_ += implications_[i].size();
1289 }
1290 dtime += 2e-8 * num_implications_;
1291 }
1292
1293 time_limit_->AdvanceDeterministicTime(dtime);
1294 LOG_IF(INFO, log_info) << "SCC. " << num_equivalences
1295 << " redundant equivalent literals. "
1296 << num_fixed_during_scc << " fixed. "
1297 << num_implications_ << " implications left. "
1298 << implications_.size() << " literals."
1299 << " size of at_most_one buffer = "
1300 << at_most_one_buffer_.size() << "."
1301 << " dtime: " << dtime
1302 << " wtime: " << wall_timer.Get();
1303 return true;
1304}
1305
1306// Note that as a side effect this also do a full "failed literal probing"
1307// using the binary implication graph only.
1308//
1309// TODO(user): Track which literal have new implications, and only process
1310// the antecedants of these.
1312 CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
1313 if (!DetectEquivalences()) return false;
1314
1315 // TODO(user): the situation with fixed variable is not really "clean".
1316 // Simplify the code so we are sure we don't run into issue or have to deal
1317 // with any of that here.
1318 if (!Propagate(trail_)) return false;
1320
1321 log_info |= VLOG_IS_ON(1);
1323 wall_timer.Start();
1324
1325 int64 num_fixed = 0;
1326 int64 num_new_redundant_implications = 0;
1327 bool aborted = false;
1328 work_done_in_mark_descendants_ = 0;
1329 int marked_index = 0;
1330
1331 // For each node we do a graph traversal and only keep the literals
1332 // at maximum distance 1. This only works because we have a DAG when ignoring
1333 // the "redundant" literal marked by DetectEquivalences(). Note that we also
1334 // need no duplicates in the implications list for correctness which is also
1335 // guaranteed by DetectEquivalences().
1336 //
1337 // TODO(user): We should be able to reuse some propagation like it is done for
1338 // tree-look. Once a node is processed, we just need to process a node that
1339 // implies it. Test if we can make this faster. Alternatively, only clear
1340 // a part of is_marked_ (after the first child of root in reverse topo order).
1341 //
1342 // TODO(user): Can we exploit the fact that the implication graph is a
1343 // skew-symmetric graph (isomorphic to its transposed) so that we do less
1344 // work? Also it would be nice to keep the property that even if we abort
1345 // during the algorithm, if a => b, then not(b) => not(a) is also present in
1346 // the other direct implication list.
1347 const LiteralIndex size(implications_.size());
1348 LiteralIndex previous = kNoLiteralIndex;
1349 for (const LiteralIndex root : reverse_topological_order_) {
1350 // In most situation reverse_topological_order_ contains no redundant, fixed
1351 // or removed variables. But the reverse_topological_order_ is only
1352 // recomputed when new binary are added to the graph, not when new variable
1353 // are fixed.
1354 if (is_redundant_[root]) continue;
1355 if (trail_->Assignment().LiteralIsAssigned(Literal(root))) continue;
1356
1357 auto& direct_implications = implications_[root];
1358 if (direct_implications.empty()) continue;
1359
1360 // This is a "poor" version of the tree look stuff, but it does show good
1361 // improvement. If we just processed one of the child of root, we don't
1362 // need to re-explore it.
1363 //
1364 // TODO(user): Another optim we can do is that we never need to expand
1365 // any node with a reverse topo order smaller or equal to the min of the
1366 // ones in this list.
1367 bool clear_previous_reachability = true;
1368 for (const Literal direct_child : direct_implications) {
1369 if (direct_child.Index() == previous) {
1370 clear_previous_reachability = false;
1371 is_marked_.Clear(previous);
1372 break;
1373 }
1374 }
1375 if (clear_previous_reachability) {
1376 is_marked_.ClearAndResize(size);
1377 marked_index = 0;
1378 }
1379 previous = root;
1380
1381 for (const Literal direct_child : direct_implications) {
1382 if (is_redundant_[direct_child.Index()]) continue;
1383 if (is_marked_[direct_child.Index()]) continue;
1384
1385 // This is a corner case where because of equivalent literal, root
1386 // appear in implications_[root], we will remove it below.
1387 if (direct_child.Index() == root) continue;
1388
1389 // When this happens, then root must be false, we handle this just after
1390 // the loop.
1391 if (direct_child.NegatedIndex() == root) {
1392 is_marked_.Set(direct_child.Index());
1393 break;
1394 }
1395
1396 MarkDescendants(direct_child);
1397
1398 // We have a DAG, so direct_child could only be marked first.
1399 is_marked_.Clear(direct_child.Index());
1400 }
1401 CHECK(!is_marked_[root])
1402 << "DetectEquivalences() should have removed cycles!";
1403 is_marked_.Set(root);
1404
1405 // Failed literal probing. If both x and not(x) are marked then root must be
1406 // false. Note that because we process "roots" in reverse topological order,
1407 // we will fix the LCA of x and not(x) first.
1408 const auto& marked_positions = is_marked_.PositionsSetAtLeastOnce();
1409 for (; marked_index < marked_positions.size(); ++marked_index) {
1410 const LiteralIndex i = marked_positions[marked_index];
1411 if (is_marked_[Literal(i).NegatedIndex()]) {
1412 // We tested that at the beginning.
1413 CHECK(!trail_->Assignment().LiteralIsAssigned(Literal(root)));
1414
1415 // We propagate right away the binary implications so that we do not
1416 // need to consider all antecedants of root in the transitive
1417 // reduction.
1418 ++num_fixed;
1419 if (!FixLiteral(Literal(root).Negated())) return false;
1420 break;
1421 }
1422 }
1423
1424 // Note that direct_implications will be cleared by
1425 // RemoveFixedVariables() that will need to inspect it to completely
1426 // remove Literal(root) from all lists.
1427 if (trail_->Assignment().LiteralIsAssigned(Literal(root))) continue;
1428
1429 // Only keep the non-marked literal (and the redundant one which are never
1430 // marked). We mark root to remove it in the corner case where it was
1431 // there.
1432 int new_size = 0;
1433 for (const Literal l : direct_implications) {
1434 if (!is_marked_[l.Index()]) {
1435 direct_implications[new_size++] = l;
1436 } else {
1437 CHECK(!is_redundant_[l.Index()]);
1438 }
1439 }
1440 const int diff = direct_implications.size() - new_size;
1441 direct_implications.resize(new_size);
1442 direct_implications.shrink_to_fit();
1443 num_new_redundant_implications += diff;
1444 num_implications_ -= diff;
1445
1446 // Abort if the computation involved is too big.
1447 if (work_done_in_mark_descendants_ > 1e8) {
1448 aborted = true;
1449 break;
1450 }
1451 }
1452
1453 is_marked_.ClearAndResize(size);
1454
1455 const double dtime = 1e-8 * work_done_in_mark_descendants_;
1456 time_limit_->AdvanceDeterministicTime(dtime);
1457 num_redundant_implications_ += num_new_redundant_implications;
1458 LOG_IF(INFO, log_info) << "Transitive reduction removed "
1459 << num_new_redundant_implications << " literals. "
1460 << num_fixed << " fixed. " << num_implications_
1461 << " implications left. " << implications_.size()
1462 << " literals."
1463 << " dtime: " << dtime
1464 << " wtime: " << wall_timer.Get()
1465 << (aborted ? " Aborted." : "");
1466 return true;
1467}
1468
1469namespace {
1470
1471bool IntersectionIsEmpty(const std::vector<int>& a, const std::vector<int>& b) {
1472 DCHECK(std::is_sorted(a.begin(), a.end()));
1473 DCHECK(std::is_sorted(b.begin(), b.end()));
1474 int i = 0;
1475 int j = 0;
1476 for (; i < a.size() && j < b.size();) {
1477 if (a[i] == b[j]) return false;
1478 if (a[i] < b[j]) {
1479 ++i;
1480 } else {
1481 ++j;
1482 }
1483 }
1484 return true;
1485}
1486
1487// Used by TransformIntoMaxCliques().
1488struct VectorHash {
1489 std::size_t operator()(const std::vector<Literal>& at_most_one) const {
1490 size_t hash = 0;
1491 for (Literal literal : at_most_one) {
1492 hash = util_hash::Hash(literal.Index().value(), hash);
1493 }
1494 return hash;
1495 }
1496};
1497
1498} // namespace
1499
1501 std::vector<std::vector<Literal>>* at_most_ones,
1502 int64 max_num_explored_nodes) {
1503 // The code below assumes a DAG.
1504 if (!DetectEquivalences()) return false;
1505 work_done_in_mark_descendants_ = 0;
1506
1507 int num_extended = 0;
1508 int num_removed = 0;
1509 int num_added = 0;
1510
1511 absl::flat_hash_set<std::vector<Literal>, VectorHash> max_cliques;
1513 implications_.size());
1514
1515 // We starts by processing larger constraints first.
1516 std::sort(at_most_ones->begin(), at_most_ones->end(),
1517 [](const std::vector<Literal> a, const std::vector<Literal> b) {
1518 return a.size() > b.size();
1519 });
1520 for (std::vector<Literal>& clique : *at_most_ones) {
1521 const int old_size = clique.size();
1522
1523 // Remap the clique to only use representative.
1524 //
1525 // Note(user): Because we always use literal with the smallest variable
1526 // indices as representative, this make sure that if possible, we express
1527 // the clique in term of user provided variable (that are always created
1528 // first).
1529 for (Literal& ref : clique) {
1530 DCHECK_LT(ref.Index(), representative_of_.size());
1531 const LiteralIndex rep = representative_of_[ref.Index()];
1532 if (rep == kNoLiteralIndex) continue;
1533 ref = Literal(rep);
1534 }
1535
1536 // Special case for clique of size 2, we don't expand them if they
1537 // are included in an already added clique.
1538 //
1539 // TODO(user): the second condition means the literal must be false!
1540 if (old_size == 2 && clique[0] != clique[1]) {
1541 if (!IntersectionIsEmpty(max_cliques_containing[clique[0].Index()],
1542 max_cliques_containing[clique[1].Index()])) {
1543 ++num_removed;
1544 clique.clear();
1545 continue;
1546 }
1547 }
1548
1549 // We only expand the clique as long as we didn't spend too much time.
1550 if (work_done_in_mark_descendants_ < max_num_explored_nodes) {
1551 clique = ExpandAtMostOne(clique);
1552 }
1553 std::sort(clique.begin(), clique.end());
1554 if (!gtl::InsertIfNotPresent(&max_cliques, clique)) {
1555 ++num_removed;
1556 clique.clear();
1557 continue;
1558 }
1559
1560 const int clique_index = max_cliques.size();
1561 for (const Literal l : clique) {
1562 max_cliques_containing[l.Index()].push_back(clique_index);
1563 }
1564 if (clique.size() > old_size) ++num_extended;
1565 ++num_added;
1566 }
1567
1568 if (num_extended > 0 || num_removed > 0 || num_added > 0) {
1569 VLOG(1) << "Clique Extended: " << num_extended
1570 << " Removed: " << num_removed << " Added: " << num_added
1571 << (work_done_in_mark_descendants_ > max_num_explored_nodes
1572 ? " (Aborted)"
1573 : "");
1574 }
1575 return true;
1576}
1577
1578std::vector<Literal> BinaryImplicationGraph::ExpandAtMostOneWithWeight(
1579 const absl::Span<const Literal> at_most_one,
1580 const absl::StrongVector<LiteralIndex, bool>& can_be_included,
1581 const absl::StrongVector<LiteralIndex, double>& expanded_lp_values) {
1582 std::vector<Literal> clique(at_most_one.begin(), at_most_one.end());
1583 std::vector<LiteralIndex> intersection;
1584 double clique_weight = 0.0;
1585 const int64 old_work = work_done_in_mark_descendants_;
1586 for (const Literal l : clique) clique_weight += expanded_lp_values[l.Index()];
1587 for (int i = 0; i < clique.size(); ++i) {
1588 // Do not spend too much time here.
1589 if (work_done_in_mark_descendants_ - old_work > 1e8) break;
1590
1591 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
1592 MarkDescendants(clique[i]);
1593 if (i == 0) {
1594 for (const LiteralIndex index : is_marked_.PositionsSetAtLeastOnce()) {
1595 if (can_be_included[index]) intersection.push_back(index);
1596 }
1597 for (const Literal l : clique) is_marked_.Clear(l.NegatedIndex());
1598 }
1599
1600 int new_size = 0;
1601 double intersection_weight = 0.0;
1602 is_marked_.Clear(clique[i].Index());
1603 is_marked_.Clear(clique[i].NegatedIndex());
1604 for (const LiteralIndex index : intersection) {
1605 if (!is_marked_[index]) continue;
1606 intersection[new_size++] = index;
1607 intersection_weight += expanded_lp_values[index];
1608 }
1609 intersection.resize(new_size);
1610 if (intersection.empty()) break;
1611
1612 // We can't generate a violated cut this way. This is because intersection
1613 // contains all the possible ways to extend the current clique.
1614 if (clique_weight + intersection_weight <= 1.0) {
1615 clique.clear();
1616 return clique;
1617 }
1618
1619 // Expand? The negation of any literal in the intersection is a valid way
1620 // to extend the clique.
1621 if (i + 1 == clique.size()) {
1622 // Heuristic: use literal with largest lp value. We randomize slightly.
1623 int index = -1;
1624 double max_lp = 0.0;
1625 for (int j = 0; j < intersection.size(); ++j) {
1626 const double lp = 1.0 - expanded_lp_values[intersection[j]] +
1627 absl::Uniform<double>(*random_, 0.0, 1e-4);
1628 if (index == -1 || lp > max_lp) {
1629 index = j;
1630 max_lp = lp;
1631 }
1632 }
1633 if (index != -1) {
1634 clique.push_back(Literal(intersection[index]).Negated());
1635 std::swap(intersection.back(), intersection[index]);
1636 intersection.pop_back();
1637 clique_weight += expanded_lp_values[clique.back().Index()];
1638 }
1639 }
1640 }
1641 return clique;
1642}
1643
1644const std::vector<std::vector<Literal>>&
1646 const std::vector<Literal>& literals,
1647 const std::vector<double>& lp_values) {
1648 // We only want to generate a cut with literals from the LP, not extra ones.
1649 const int num_literals = implications_.size();
1650 absl::StrongVector<LiteralIndex, bool> can_be_included(num_literals, false);
1651 absl::StrongVector<LiteralIndex, double> expanded_lp_values(num_literals,
1652 0.0);
1653 const int size = literals.size();
1654 for (int i = 0; i < size; ++i) {
1655 const Literal l = literals[i];
1656 can_be_included[l.Index()] = true;
1657 can_be_included[l.NegatedIndex()] = true;
1658
1659 const double value = lp_values[i];
1660 expanded_lp_values[l.Index()] = value;
1661 expanded_lp_values[l.NegatedIndex()] = 1.0 - value;
1662 }
1663
1664 // We want highest sum first.
1665 struct Candidate {
1666 Literal a;
1667 Literal b;
1668 double sum;
1669 bool operator<(const Candidate& other) const { return sum > other.sum; }
1670 };
1671 std::vector<Candidate> candidates;
1672
1673 // First heuristic. Currently we only consider violated at most one of size 2,
1674 // and extend them. Right now, the code is a bit slow to try too many at every
1675 // LP node so it is why we are defensive like this. Note also that because we
1676 // currently still statically add the initial implications, this will only add
1677 // cut based on newly learned binary clause. Or the one that were not added
1678 // to the relaxation in the first place.
1679 for (int i = 0; i < size; ++i) {
1680 Literal current_literal = literals[i];
1681 double current_value = lp_values[i];
1682 if (trail_->Assignment().LiteralIsAssigned(current_literal)) continue;
1683 if (is_redundant_[current_literal.Index()]) continue;
1684
1685 if (current_value < 0.5) {
1686 current_literal = current_literal.Negated();
1687 current_value = 1.0 - current_value;
1688 }
1689
1690 // We consider only one candidate for each current_literal.
1691 LiteralIndex best = kNoLiteralIndex;
1692 double best_value = 0.0;
1693 for (const Literal l : implications_[current_literal.Index()]) {
1694 if (!can_be_included[l.Index()]) continue;
1695 const double activity =
1696 current_value + expanded_lp_values[l.NegatedIndex()];
1697 if (activity <= 1.01) continue;
1698 const double v = activity + absl::Uniform<double>(*random_, 0.0, 1e-4);
1699 if (best == kNoLiteralIndex || v > best_value) {
1700 best_value = v;
1701 best = l.NegatedIndex();
1702 }
1703 }
1704 if (best != kNoLiteralIndex) {
1705 const double activity = current_value + expanded_lp_values[best];
1706 candidates.push_back({current_literal, Literal(best), activity});
1707 }
1708 }
1709
1710 // Do not genate too many cut at once.
1711 const int kMaxNumberOfCutPerCall = 50;
1712 std::sort(candidates.begin(), candidates.end());
1713 if (candidates.size() > kMaxNumberOfCutPerCall) {
1714 candidates.resize(kMaxNumberOfCutPerCall);
1715 }
1716
1717 // Expand to a maximal at most one each candidates before returning them.
1718 // Note that we only expand using literal from the LP.
1719 tmp_cuts_.clear();
1720 std::vector<Literal> at_most_one;
1721 for (const Candidate& candidate : candidates) {
1722 at_most_one = ExpandAtMostOneWithWeight(
1723 {candidate.a, candidate.b}, can_be_included, expanded_lp_values);
1724 if (!at_most_one.empty()) tmp_cuts_.push_back(at_most_one);
1725 }
1726 return tmp_cuts_;
1727}
1728
1729// We use dfs_stack_ but we actually do a BFS.
1730void BinaryImplicationGraph::MarkDescendants(Literal root) {
1731 dfs_stack_ = {root};
1732 is_marked_.Set(root.Index());
1733 if (is_redundant_[root.Index()]) return;
1734 for (int j = 0; j < dfs_stack_.size(); ++j) {
1735 const Literal current = dfs_stack_[j];
1736 for (const Literal l : implications_[current.Index()]) {
1737 if (!is_marked_[l.Index()] && !is_redundant_[l.Index()]) {
1738 dfs_stack_.push_back(l);
1739 is_marked_.Set(l.Index());
1740 }
1741 }
1742
1743 if (current.Index() >= at_most_ones_.size()) continue;
1744 for (const int start : at_most_ones_[current.Index()]) {
1745 for (int i = start;; ++i) {
1746 const Literal l = at_most_one_buffer_[i];
1747 if (l.Index() == kNoLiteralIndex) break;
1748 if (l == current) continue;
1749 if (!is_marked_[l.NegatedIndex()] && !is_redundant_[l.NegatedIndex()]) {
1750 dfs_stack_.push_back(l.Negated());
1751 is_marked_.Set(l.NegatedIndex());
1752 }
1753 }
1754 }
1755 }
1756 work_done_in_mark_descendants_ += dfs_stack_.size();
1757}
1758
1759std::vector<Literal> BinaryImplicationGraph::ExpandAtMostOne(
1760 const absl::Span<const Literal> at_most_one) {
1761 std::vector<Literal> clique(at_most_one.begin(), at_most_one.end());
1762
1763 // Optim.
1764 for (int i = 0; i < clique.size(); ++i) {
1765 if (implications_[clique[i].Index()].empty() ||
1766 is_redundant_[clique[i].Index()]) {
1767 return clique;
1768 }
1769 }
1770
1771 std::vector<LiteralIndex> intersection;
1772 for (int i = 0; i < clique.size(); ++i) {
1773 is_marked_.ClearAndResize(LiteralIndex(implications_.size()));
1774 MarkDescendants(clique[i]);
1775 if (i == 0) {
1776 intersection = is_marked_.PositionsSetAtLeastOnce();
1777 for (const Literal l : clique) is_marked_.Clear(l.NegatedIndex());
1778 }
1779
1780 int new_size = 0;
1781 is_marked_.Clear(clique[i].NegatedIndex()); // TODO(user): explain.
1782 for (const LiteralIndex index : intersection) {
1783 if (is_marked_[index]) intersection[new_size++] = index;
1784 }
1785 intersection.resize(new_size);
1786 if (intersection.empty()) break;
1787
1788 // Expand?
1789 if (i + 1 == clique.size()) {
1790 clique.push_back(Literal(intersection.back()).Negated());
1791 intersection.pop_back();
1792 }
1793 }
1794 return clique;
1795}
1796
1797// TODO(user): lazy cleanup the lists on is_removed_?
1798// TODO(user): Mark fixed variable as is_removed_ for faster iteration?
1800 Literal literal) {
1801 CHECK(!is_removed_[literal.Index()]);
1802
1803 // Clear old state.
1804 for (const Literal l : direct_implications_) {
1805 in_direct_implications_[l.Index()] = false;
1806 }
1807 direct_implications_.clear();
1808
1809 // Fill new state.
1810 const VariablesAssignment& assignment = trail_->Assignment();
1811 CHECK(!assignment.LiteralIsAssigned(literal));
1812 for (const Literal l : implications_[literal.Index()]) {
1813 if (l == literal) continue;
1814 if (assignment.LiteralIsAssigned(l)) continue;
1815 if (!is_removed_[l.Index()] && !in_direct_implications_[l.Index()]) {
1816 in_direct_implications_[l.Index()] = true;
1817 direct_implications_.push_back(l);
1818 }
1819 }
1820 if (literal.Index() < at_most_ones_.size()) {
1821 if (is_redundant_[literal.Index()]) {
1822 CHECK(at_most_ones_[literal.Index()].empty());
1823 }
1824 for (const int start : at_most_ones_[literal.Index()]) {
1825 for (int i = start;; ++i) {
1826 const Literal l = at_most_one_buffer_[i];
1827 if (l.Index() == kNoLiteralIndex) break;
1828 if (l == literal) continue;
1829 if (assignment.LiteralIsAssigned(l)) continue;
1830 if (!is_removed_[l.Index()] &&
1831 !in_direct_implications_[l.NegatedIndex()]) {
1832 in_direct_implications_[l.NegatedIndex()] = true;
1833 direct_implications_.push_back(l.Negated());
1834 }
1835 }
1836 }
1837 }
1838 estimated_sizes_[literal.Index()] = direct_implications_.size();
1839 return direct_implications_;
1840}
1841
1843 bool* is_unsat) {
1844 const int saved_index = propagation_trail_index_;
1845 CHECK_EQ(propagation_trail_index_, trail_->Index()); // Propagation done.
1846
1847 const VariablesAssignment& assignment = trail_->Assignment();
1848 if (assignment.VariableIsAssigned(var)) return false;
1849
1850 const Literal literal(var, true);
1851 direct_implications_of_negated_literal_ =
1852 DirectImplications(literal.Negated());
1853 DirectImplications(literal); // Fill in_direct_implications_.
1854 for (const Literal l : direct_implications_of_negated_literal_) {
1855 if (in_direct_implications_[l.Index()]) {
1856 // not(l) => literal => l.
1857 if (!FixLiteral(l)) {
1858 *is_unsat = true;
1859 return false;
1860 }
1861 }
1862 }
1863
1864 return propagation_trail_index_ > saved_index;
1865}
1866
1868 BooleanVariable var) {
1869 const Literal literal(var, true);
1870 int64 result = 0;
1871 direct_implications_of_negated_literal_ =
1872 DirectImplications(literal.Negated());
1873 const int64 s1 = DirectImplications(literal).size();
1874 for (const Literal l : direct_implications_of_negated_literal_) {
1875 result += s1;
1876
1877 // We should have dealt with that in FindFailedLiteralAroundVar().
1878 CHECK(!in_direct_implications_[l.Index()]);
1879
1880 // l => literal => l: equivalent variable!
1881 if (in_direct_implications_[l.NegatedIndex()]) result--;
1882 }
1883 return result;
1884}
1885
1886// For all possible a => var => b, add a => b.
1888 BooleanVariable var, std::deque<std::vector<Literal>>* postsolve_clauses) {
1889 const Literal literal(var, true);
1890 direct_implications_of_negated_literal_ =
1891 DirectImplications(literal.Negated());
1892 for (const Literal b : DirectImplications(literal)) {
1893 estimated_sizes_[b.NegatedIndex()]--;
1894 for (const Literal a_negated : direct_implications_of_negated_literal_) {
1895 if (a_negated.Negated() == b) continue;
1896 AddImplication(a_negated.Negated(), b);
1897 }
1898 }
1899 for (const Literal a_negated : direct_implications_of_negated_literal_) {
1900 estimated_sizes_[a_negated.NegatedIndex()]--;
1901 }
1902
1903 // Notify the deletion to the proof checker and the postsolve.
1904 // Note that we want var first in these clauses for the postsolve.
1905 for (const Literal b : direct_implications_) {
1906 if (drat_proof_handler_ != nullptr) {
1907 drat_proof_handler_->DeleteClause({Literal(var, false), b});
1908 }
1909 postsolve_clauses->push_back({Literal(var, false), b});
1910 }
1911 for (const Literal a_negated : direct_implications_of_negated_literal_) {
1912 if (drat_proof_handler_ != nullptr) {
1913 drat_proof_handler_->DeleteClause({Literal(var, true), a_negated});
1914 }
1915 postsolve_clauses->push_back({Literal(var, true), a_negated});
1916 }
1917
1918 // We need to remove any occurrence of var in our implication lists, this will
1919 // be delayed to the CleanupAllRemovedVariables() call.
1920 for (LiteralIndex index : {literal.Index(), literal.NegatedIndex()}) {
1921 is_removed_[index] = true;
1922 if (!is_redundant_[index]) {
1923 ++num_redundant_literals_;
1924 is_redundant_[index] = true;
1925 }
1926 implications_[index].clear();
1927 }
1928}
1929
1931 for (auto& implication : implications_) {
1932 int new_size = 0;
1933 for (const Literal l : implication) {
1934 if (!is_removed_[l.Index()]) implication[new_size++] = l;
1935 }
1936 implication.resize(new_size);
1937 }
1938
1939 // Clean-up at most ones.
1940 at_most_ones_.clear();
1941 CleanUpAndAddAtMostOnes(/*base_index=*/0);
1942}
1943
1944// ----- SatClause -----
1945
1946// static
1947SatClause* SatClause::Create(absl::Span<const Literal> literals) {
1948 CHECK_GE(literals.size(), 2);
1949 SatClause* clause = reinterpret_cast<SatClause*>(
1950 ::operator new(sizeof(SatClause) + literals.size() * sizeof(Literal)));
1951 clause->size_ = literals.size();
1952 for (int i = 0; i < literals.size(); ++i) {
1953 clause->literals_[i] = literals[i];
1954 }
1955 return clause;
1956}
1957
1958// Note that for an attached clause, removing fixed literal is okay because if
1959// any of the watched literal is assigned, then the clause is necessarily true.
1961 const VariablesAssignment& assignment) {
1962 DCHECK(IsAttached());
1963 if (assignment.VariableIsAssigned(literals_[0].Variable()) ||
1964 assignment.VariableIsAssigned(literals_[1].Variable())) {
1965 DCHECK(IsSatisfied(assignment));
1966 return true;
1967 }
1968 int j = 2;
1969 while (j < size_ && !assignment.VariableIsAssigned(literals_[j].Variable())) {
1970 ++j;
1971 }
1972 for (int i = j; i < size_; ++i) {
1973 if (assignment.VariableIsAssigned(literals_[i].Variable())) {
1974 if (assignment.LiteralIsTrue(literals_[i])) return true;
1975 } else {
1976 std::swap(literals_[j], literals_[i]);
1977 ++j;
1978 }
1979 }
1980 size_ = j;
1981 return false;
1982}
1983
1984bool SatClause::IsSatisfied(const VariablesAssignment& assignment) const {
1985 for (const Literal literal : *this) {
1986 if (assignment.LiteralIsTrue(literal)) return true;
1987 }
1988 return false;
1989}
1990
1991std::string SatClause::DebugString() const {
1992 std::string result;
1993 for (const Literal literal : *this) {
1994 if (!result.empty()) result.append(" ");
1995 result.append(literal.DebugString());
1996 }
1997 return result;
1998}
1999
2000} // namespace sat
2001} // namespace operations_research
#define LOG_IF(severity, condition)
Definition: base/logging.h:479
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
void Start()
Definition: timer.h:31
double Get() const
Definition: timer.h:45
void resize(size_type new_size)
size_type size() const
bool empty() const
void push_back(const value_type &x)
IntegerType size() const
Definition: bitset.h:769
void Set(IntegerType index)
Definition: bitset.h:803
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
void Clear(IntegerType index)
Definition: bitset.h:809
void Resize(IntegerType size)
Definition: bitset.h:789
void ClearAndResize(IntegerType size)
Definition: bitset.h:778
std::string StatString() const
Definition: stats.cc:71
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
Definition: time_limit.h:226
void AddBinaryClause(Literal a, Literal b)
Definition: clause.cc:491
bool ComputeTransitiveReduction(bool log_info=false)
Definition: clause.cc:1311
void MinimizeConflictWithReachability(std::vector< Literal > *c)
Definition: clause.cc:754
bool AddBinaryClauseDuringSearch(Literal a, Literal b)
Definition: clause.cc:508
const std::vector< std::vector< Literal > > & GenerateAtMostOnesWithLargeWeight(const std::vector< Literal > &literals, const std::vector< double > &lp_values)
Definition: clause.cc:1645
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: clause.cc:742
bool TransformIntoMaxCliques(std::vector< std::vector< Literal > > *at_most_ones, int64 max_num_explored_nodes=1e8)
Definition: clause.cc:1500
void RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
Definition: clause.cc:1887
void MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, absl::BitGenRef random)
Definition: clause.cc:849
Literal RepresentativeOf(Literal l) const
Definition: clause.h:561
const std::vector< Literal > & DirectImplications(Literal literal)
Definition: clause.cc:1799
void AddImplication(Literal a, Literal b)
Definition: clause.h:488
void MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked)
Definition: clause.cc:831
bool DetectEquivalences(bool log_info=false)
Definition: clause.cc:1124
bool FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat)
Definition: clause.cc:1842
int64 NumImplicationOnVariableRemoval(BooleanVariable var)
Definition: clause.cc:1867
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)
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
LiteralIndex Index() const
Definition: sat_base.h:84
BooleanVariable Variable() const
Definition: sat_base.h:80
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)
Definition: clause.cc:339
bool Propagate(Trail *trail) final
Definition: clause.cc:183
void InprocessingRemoveClause(SatClause *clause)
Definition: clause.cc:358
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: clause.cc:192
SatClause * AddRemovableClause(const std::vector< Literal > &literals, Trail *trail)
Definition: clause.cc:212
SatClause * InprocessingAddClause(absl::Span< const Literal > new_clause)
Definition: clause.cc:415
void Attach(SatClause *clause, Trail *trail)
Definition: clause.cc:274
bool AddClause(absl::Span< const Literal > literals, Trail *trail)
Definition: clause.cc:205
SatClause * ReasonClause(int trail_index) const
Definition: clause.cc:197
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
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
absl::Span< const Literal > AsSpan() const
Definition: clause.h:90
const Literal *const begin() const
Definition: clause.h:69
Literal SecondLiteral() const
Definition: clause.h:75
bool IsSatisfied(const VariablesAssignment &assignment) const
Definition: clause.cc:1984
bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment &assignment)
Definition: clause.cc:1960
std::string DebugString() const
Definition: clause.cc:1991
Literal FirstLiteral() const
Definition: clause.h:74
static SatClause * Create(absl::Span< const Literal > literals)
Definition: clause.cc:1947
SccGraph(SccFinder *finder, Implication *graph, AtMostOne *at_most_ones, std::vector< Literal > *at_most_one_buffer)
Definition: clause.cc:1026
std::vector< Literal > to_fix_
Definition: clause.cc:1106
const std::vector< int32 > & operator[](int32 node) const
Definition: clause.cc:1034
void RegisterPropagator(SatPropagator *propagator)
Definition: sat_base.h:551
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
void EnqueueWithUnitReason(Literal true_literal)
Definition: sat_base.h:265
bool LiteralIsAssigned(Literal literal) const
Definition: sat_base.h:153
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
WallTimer * wall_timer
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
int64_t int64
const int INFO
Definition: log_severity.h:31
const bool DEBUG_MODE
Definition: macros.h:24
int64 hash
Definition: matrix_utils.cc:60
bool InsertIfNotPresent(Collection *const collection, const typename Collection::value_type &value)
Definition: map_util.h:103
void STLClearObject(T *obj)
Definition: stl_util.h:123
void STLDeleteElements(T *container)
Definition: stl_util.h:372
void STLDeleteContainerPointers(ForwardIterator begin, ForwardIterator end)
Definition: stl_util.h:314
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
const LiteralIndex kNoLiteralIndex(-1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
uint64 Hash(uint64 num, uint64 c)
Definition: hash.h:150
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
ColIndex representative
#define IF_STATS_ENABLED(instructions)
Definition: stats.h:437
#define SCOPED_TIME_STAT(stats)
Definition: stats.h:438
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41