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