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 
22 #include "ortools/base/logging.h"
23 #include "ortools/base/stl_util.h"
25 #include "ortools/base/timer.h"
27 
28 namespace operations_research {
29 namespace sat {
30 
31 namespace {
32 
33 // Returns true if the given watcher list contains the given clause.
34 template <typename Watcher>
35 bool 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.
44 template <typename Container, typename Predicate>
45 void 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 
69 void 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.
78 void 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 
87 bool 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 
192 absl::Span<const Literal> LiteralWatchers::Reason(const Trail& trail,
193  int trail_index) const {
194  return reasons_[trail_index]->PropagationReason();
195 }
196 
197 SatClause* LiteralWatchers::ReasonClause(int trail_index) const {
198  return reasons_[trail_index];
199 }
200 
201 bool LiteralWatchers::AddClause(absl::Span<const Literal> literals) {
202  return AddClause(literals, trail_);
203 }
204 
205 bool 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.
225 bool 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 
274 void LiteralWatchers::Attach(SatClause* clause, Trail* trail) {
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 
284 void 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;
379  InprocessingRemoveClause(clause);
380  return true;
381  }
382 
383  if (new_clause.size() == 2) {
384  implication_graph_->AddBinaryClause(new_clause[0], new_clause[1]);
385  InprocessingRemoveClause(clause);
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 
477 void 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();
511  AddBinaryClause(a, b);
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();
550 bool 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.
565 bool 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 
660 bool 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()) {
732  propagation_trail_index_ = trail->Index();
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 
742 absl::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 
893 void 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 
1016 class SccGraph {
1017  public:
1018  using Implication =
1020  using AtMostOne =
1022  using SccFinder =
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 
1469 namespace {
1470 
1471 bool 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().
1488 struct 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;
1512  absl::StrongVector<LiteralIndex, std::vector<int>> max_cliques_containing(
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 
1578 std::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 
1644 const 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.
1730 void 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 
1759 std::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
1947 SatClause* 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 
1984 bool 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 
1991 std::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)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
IntegerType size() const
Definition: bitset.h:769
void Set(IntegerType index)
Definition: bitset.h:803
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
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 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
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
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
const Literal *const begin() const
Definition: clause.h:69
SccGraph(SccFinder *finder, Implication *graph, AtMostOne *at_most_ones, std::vector< Literal > *at_most_one_buffer)
Definition: clause.cc:1026
const std::vector< int32 > & operator[](int32 node) const
Definition: clause.cc:1034
std::vector< Literal > to_fix_
Definition: clause.cc:1106
void RegisterPropagator(SatPropagator *propagator)
Definition: sat_base.h:551
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
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
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
bool InsertIfNotPresent(Collection *const collection, const typename Collection::value_type &value)
Definition: map_util.h:103
void STLDeleteElements(T *container)
Definition: stl_util.h:372
void STLDeleteContainerPointers(ForwardIterator begin, ForwardIterator end)
Definition: stl_util.h:314
void STLClearObject(T *obj)
Definition: stl_util.h:123
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