OR-Tools  8.2
simplification.cc
Go to the documentation of this file.
1 // Copyright 2010-2018 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
15 
16 #include <algorithm>
17 #include <limits>
18 #include <set>
19 #include <utility>
20 
21 #include "absl/memory/memory.h"
24 #include "ortools/base/logging.h"
25 #include "ortools/base/random.h"
26 #include "ortools/base/stl_util.h"
28 #include "ortools/base/timer.h"
30 #include "ortools/sat/probing.h"
32 #include "ortools/sat/util.h"
34 
35 namespace operations_research {
36 namespace sat {
37 
38 SatPostsolver::SatPostsolver(int num_variables)
39  : initial_num_variables_(num_variables), num_variables_(num_variables) {
40  reverse_mapping_.resize(num_variables);
41  for (BooleanVariable var(0); var < num_variables; ++var) {
42  reverse_mapping_[var] = var;
43  }
44  assignment_.Resize(num_variables);
45 }
46 
47 void SatPostsolver::Add(Literal x, absl::Span<const Literal> clause) {
48  DCHECK(!clause.empty());
49  DCHECK(std::find(clause.begin(), clause.end(), x) != clause.end());
50  associated_literal_.push_back(ApplyReverseMapping(x));
51  clauses_start_.push_back(clauses_literals_.size());
52  for (const Literal& l : clause) {
53  clauses_literals_.push_back(ApplyReverseMapping(l));
54  }
55 }
56 
58  const Literal l = ApplyReverseMapping(x);
59  assignment_.AssignFromTrueLiteral(l);
60 }
61 
65  if (reverse_mapping_.size() < mapping.size()) {
66  // We have new variables.
67  while (reverse_mapping_.size() < mapping.size()) {
68  reverse_mapping_.push_back(BooleanVariable(num_variables_++));
69  }
70  assignment_.Resize(num_variables_);
71  }
72  for (BooleanVariable v(0); v < mapping.size(); ++v) {
73  const BooleanVariable image = mapping[v];
74  if (image != kNoBooleanVariable) {
75  if (image >= new_mapping.size()) {
76  new_mapping.resize(image.value() + 1, kNoBooleanVariable);
77  }
78  new_mapping[image] = reverse_mapping_[v];
79  DCHECK_NE(new_mapping[image], kNoBooleanVariable);
80  }
81  }
82  std::swap(new_mapping, reverse_mapping_);
83 }
84 
85 Literal SatPostsolver::ApplyReverseMapping(Literal l) {
86  if (l.Variable() >= reverse_mapping_.size()) {
87  // We have new variables.
88  while (l.Variable() >= reverse_mapping_.size()) {
89  reverse_mapping_.push_back(BooleanVariable(num_variables_++));
90  }
91  assignment_.Resize(num_variables_);
92  }
93  DCHECK_NE(reverse_mapping_[l.Variable()], kNoBooleanVariable);
94  const Literal result(reverse_mapping_[l.Variable()], l.IsPositive());
95  DCHECK(!assignment_.LiteralIsAssigned(result));
96  return result;
97 }
98 
99 void SatPostsolver::Postsolve(VariablesAssignment* assignment) const {
100  // First, we set all unassigned variable to true.
101  // This will be a valid assignment of the presolved problem.
102  for (BooleanVariable var(0); var < assignment->NumberOfVariables(); ++var) {
103  if (!assignment->VariableIsAssigned(var)) {
104  assignment->AssignFromTrueLiteral(Literal(var, true));
105  }
106  }
107 
108  int previous_start = clauses_literals_.size();
109  for (int i = static_cast<int>(clauses_start_.size()) - 1; i >= 0; --i) {
110  bool set_associated_var = true;
111  const int new_start = clauses_start_[i];
112  for (int j = new_start; j < previous_start; ++j) {
113  if (assignment->LiteralIsTrue(clauses_literals_[j])) {
114  set_associated_var = false;
115  break;
116  }
117  }
118  previous_start = new_start;
119  if (set_associated_var) {
120  assignment->UnassignLiteral(associated_literal_[i].Negated());
121  assignment->AssignFromTrueLiteral(associated_literal_[i]);
122  }
123  }
124 
125  // Ignore the value of any variables added by the presolve.
126  assignment->Resize(initial_num_variables_);
127 }
128 
130  const SatSolver& solver) {
131  std::vector<bool> solution(solver.NumVariables());
132  for (BooleanVariable var(0); var < solver.NumVariables(); ++var) {
134  solution[var.value()] =
135  solver.Assignment().LiteralIsTrue(Literal(var, true));
136  }
137  return PostsolveSolution(solution);
138 }
139 
141  const std::vector<bool>& solution) {
142  for (BooleanVariable var(0); var < solution.size(); ++var) {
143  DCHECK_LT(var, reverse_mapping_.size());
144  DCHECK_NE(reverse_mapping_[var], kNoBooleanVariable);
145  DCHECK(!assignment_.VariableIsAssigned(reverse_mapping_[var]));
146  assignment_.AssignFromTrueLiteral(
147  Literal(reverse_mapping_[var], solution[var.value()]));
148  }
149  Postsolve(&assignment_);
150  std::vector<bool> postsolved_solution;
151  postsolved_solution.reserve(initial_num_variables_);
152  for (int i = 0; i < initial_num_variables_; ++i) {
153  postsolved_solution.push_back(
154  assignment_.LiteralIsTrue(Literal(BooleanVariable(i), true)));
155  }
156  return postsolved_solution;
157 }
158 
160 
161 void SatPresolver::AddClause(absl::Span<const Literal> clause) {
162  DCHECK_GT(clause.size(), 0) << "Added an empty clause to the presolver";
163  const ClauseIndex ci(clauses_.size());
164  clauses_.push_back(std::vector<Literal>(clause.begin(), clause.end()));
165  in_clause_to_process_.push_back(true);
166  clause_to_process_.push_back(ci);
167 
168  bool changed = false;
169  std::vector<Literal>& clause_ref = clauses_.back();
170  if (!equiv_mapping_.empty()) {
171  for (int i = 0; i < clause_ref.size(); ++i) {
172  const Literal old_literal = clause_ref[i];
173  clause_ref[i] = Literal(equiv_mapping_[clause_ref[i].Index()]);
174  if (old_literal != clause_ref[i]) changed = true;
175  }
176  }
177  std::sort(clause_ref.begin(), clause_ref.end());
178  clause_ref.erase(std::unique(clause_ref.begin(), clause_ref.end()),
179  clause_ref.end());
180 
181  // Check for trivial clauses:
182  for (int i = 1; i < clause_ref.size(); ++i) {
183  if (clause_ref[i] == clause_ref[i - 1].Negated()) {
184  // The clause is trivial!
185  ++num_trivial_clauses_;
186  clause_to_process_.pop_back();
187  clauses_.pop_back();
188  in_clause_to_process_.pop_back();
189  return;
190  }
191  }
192 
193  // This needs to be done after the basic canonicalization above.
194  signatures_.push_back(ComputeSignatureOfClauseVariables(ci));
195  DCHECK_EQ(signatures_.size(), clauses_.size());
196 
197  if (drat_proof_handler_ != nullptr && changed) {
198  drat_proof_handler_->AddClause(clause_ref);
199  drat_proof_handler_->DeleteClause(clause);
200  }
201 
202  const Literal max_literal = clause_ref.back();
203  const int required_size = std::max(max_literal.Index().value(),
204  max_literal.NegatedIndex().value()) +
205  1;
206  if (required_size > literal_to_clauses_.size()) {
207  literal_to_clauses_.resize(required_size);
208  literal_to_clause_sizes_.resize(required_size);
209  }
210  for (Literal e : clause_ref) {
211  literal_to_clauses_[e.Index()].push_back(ci);
212  literal_to_clause_sizes_[e.Index()]++;
213  }
214 }
215 
216 void SatPresolver::SetNumVariables(int num_variables) {
217  const int required_size = 2 * num_variables;
218  if (required_size > literal_to_clauses_.size()) {
219  literal_to_clauses_.resize(required_size);
220  literal_to_clause_sizes_.resize(required_size);
221  }
222 }
223 
224 void SatPresolver::AddClauseInternal(std::vector<Literal>* clause) {
225  if (drat_proof_handler_ != nullptr) drat_proof_handler_->AddClause(*clause);
226 
227  DCHECK(std::is_sorted(clause->begin(), clause->end()));
228  DCHECK_GT(clause->size(), 0) << "TODO(fdid): Unsat during presolve?";
229  const ClauseIndex ci(clauses_.size());
230  clauses_.push_back(std::vector<Literal>());
231  clauses_.back().swap(*clause);
232  in_clause_to_process_.push_back(true);
233  clause_to_process_.push_back(ci);
234  for (const Literal e : clauses_.back()) {
235  literal_to_clauses_[e.Index()].push_back(ci);
236  literal_to_clause_sizes_[e.Index()]++;
237  UpdatePriorityQueue(e.Variable());
238  UpdateBvaPriorityQueue(e.Index());
239  }
240 
241  signatures_.push_back(ComputeSignatureOfClauseVariables(ci));
242  DCHECK_EQ(signatures_.size(), clauses_.size());
243 }
244 
248  BooleanVariable new_var(0);
249  for (BooleanVariable var(0); var < NumVariables(); ++var) {
250  if (literal_to_clause_sizes_[Literal(var, true).Index()] > 0 ||
251  literal_to_clause_sizes_[Literal(var, false).Index()] > 0) {
252  result.push_back(new_var);
253  ++new_var;
254  } else {
256  }
257  }
258  return result;
259 }
260 
262  // Cleanup some memory that is not needed anymore. Note that we do need
263  // literal_to_clause_sizes_ for VariableMapping() to work.
264  var_pq_.Clear();
265  var_pq_elements_.clear();
266  in_clause_to_process_.clear();
267  clause_to_process_.clear();
268  literal_to_clauses_.clear();
269  signatures_.clear();
270 
272  VariableMapping();
273  int new_size = 0;
274  for (BooleanVariable index : mapping) {
275  if (index != kNoBooleanVariable) ++new_size;
276  }
277 
278  std::vector<Literal> temp;
279  solver->SetNumVariables(new_size);
280  for (std::vector<Literal>& clause_ref : clauses_) {
281  temp.clear();
282  for (Literal l : clause_ref) {
283  DCHECK_NE(mapping[l.Variable()], kNoBooleanVariable);
284  temp.push_back(Literal(mapping[l.Variable()], l.IsPositive()));
285  }
286  if (!temp.empty()) solver->AddProblemClause(temp);
287  gtl::STLClearObject(&clause_ref);
288  }
289 }
290 
291 bool SatPresolver::ProcessAllClauses() {
292  int num_skipped_checks = 0;
293  const int kCheckFrequency = 1000;
294 
295  // Because on large problem we don't have a budget to process all clauses,
296  // lets start by the smallest ones first.
297  std::sort(clause_to_process_.begin(), clause_to_process_.end(),
298  [this](ClauseIndex c1, ClauseIndex c2) {
299  return clauses_[c1].size() < clauses_[c2].size();
300  });
301  while (!clause_to_process_.empty()) {
302  const ClauseIndex ci = clause_to_process_.front();
303  in_clause_to_process_[ci] = false;
304  clause_to_process_.pop_front();
305  if (!ProcessClauseToSimplifyOthers(ci)) return false;
306  if (++num_skipped_checks >= kCheckFrequency) {
307  if (num_inspected_signatures_ + num_inspected_literals_ > 1e9) {
308  VLOG(1) << "Aborting ProcessAllClauses() because work limit has been "
309  "reached";
310  return true;
311  }
312  if (time_limit_ != nullptr && time_limit_->LimitReached()) return true;
313  num_skipped_checks = 0;
314  }
315  }
316  return true;
317 }
318 
320  // This is slighlty inefficient, but the presolve algorithm is
321  // a lot more costly anyway.
322  std::vector<bool> can_be_removed(NumVariables(), true);
323  return Presolve(can_be_removed);
324 }
325 
326 bool SatPresolver::Presolve(const std::vector<bool>& can_be_removed,
327  bool log_info) {
328  log_info |= VLOG_IS_ON(1);
329 
330  WallTimer timer;
331  timer.Start();
332  if (log_info) {
333  int64 num_removable = 0;
334  for (const bool b : can_be_removed) {
335  if (b) ++num_removable;
336  }
337  LOG(INFO) << "num removable Booleans: " << num_removable << " / "
338  << can_be_removed.size();
339  LOG(INFO) << "num trivial clauses: " << num_trivial_clauses_;
340  DisplayStats(0);
341  }
342 
343  // TODO(user): When a clause is strengthened, add it to a queue so it can
344  // be processed again?
345  if (!ProcessAllClauses()) return false;
346  if (log_info) DisplayStats(timer.Get());
347 
348  if (time_limit_ != nullptr && time_limit_->LimitReached()) return true;
349  if (num_inspected_signatures_ + num_inspected_literals_ > 1e9) return true;
350 
351  InitializePriorityQueue();
352  while (var_pq_.Size() > 0) {
353  const BooleanVariable var = var_pq_.Top()->variable;
354  var_pq_.Pop();
355  if (!can_be_removed[var.value()]) continue;
356  if (CrossProduct(Literal(var, true))) {
357  if (!ProcessAllClauses()) return false;
358  }
359  if (time_limit_ != nullptr && time_limit_->LimitReached()) return true;
360  if (num_inspected_signatures_ + num_inspected_literals_ > 1e9) return true;
361  }
362  if (log_info) DisplayStats(timer.Get());
363 
364  // We apply BVA after a pass of the other algorithms.
365  if (parameters_.presolve_use_bva()) {
366  PresolveWithBva();
367  if (log_info) DisplayStats(timer.Get());
368  }
369 
370  return true;
371 }
372 
374  var_pq_elements_.clear(); // so we don't update it.
375  InitializeBvaPriorityQueue();
376  while (bva_pq_.Size() > 0) {
377  const LiteralIndex lit = bva_pq_.Top()->literal;
378  bva_pq_.Pop();
379  SimpleBva(lit);
380  }
381 }
382 
383 // We use the same notation as in the article mentionned in the .h
384 void SatPresolver::SimpleBva(LiteralIndex l) {
385  literal_to_p_size_.resize(literal_to_clauses_.size(), 0);
386  DCHECK(std::all_of(literal_to_p_size_.begin(), literal_to_p_size_.end(),
387  [](int v) { return v == 0; }));
388 
389  // We will try to add a literal to m_lit_ and take a subset of m_cls_ such
390  // that |m_lit_| * |m_cls_| - |m_lit_| - |m_cls_| is maximized.
391  m_lit_ = {l};
392  m_cls_ = literal_to_clauses_[l];
393 
394  int reduction = 0;
395  while (true) {
396  LiteralIndex lmax = kNoLiteralIndex;
397  int max_size = 0;
398 
399  flattened_p_.clear();
400  for (const ClauseIndex c : m_cls_) {
401  const std::vector<Literal>& clause = clauses_[c];
402  if (clause.empty()) continue; // It has been deleted.
403 
404  // Find a literal different from l that occur in the less number of
405  // clauses.
406  const LiteralIndex l_min =
407  FindLiteralWithShortestOccurrenceListExcluding(clause, Literal(l));
408  if (l_min == kNoLiteralIndex) continue;
409 
410  // Find all the clauses of the form "clause \ {l} + {l'}", for a literal
411  // l' that is not in the clause.
412  for (const ClauseIndex d : literal_to_clauses_[l_min]) {
413  if (clause.size() != clauses_[d].size()) continue;
414  const LiteralIndex l_diff =
415  DifferAtGivenLiteral(clause, clauses_[d], Literal(l));
416  if (l_diff == kNoLiteralIndex || m_lit_.count(l_diff) > 0) continue;
417  if (l_diff == Literal(l).NegatedIndex()) {
418  // Self-subsumbtion!
419  //
420  // TODO(user): Not sure this can happen after the presolve we did
421  // before calling SimpleBva().
422  VLOG(1) << "self-subsumbtion";
423  }
424 
425  flattened_p_.push_back({l_diff, c});
426  const int new_size = ++literal_to_p_size_[l_diff];
427  if (new_size > max_size) {
428  lmax = l_diff;
429  max_size = new_size;
430  }
431  }
432  }
433 
434  if (lmax == kNoLiteralIndex) break;
435  const int new_m_lit_size = m_lit_.size() + 1;
436  const int new_m_cls_size = max_size;
437  const int new_reduction =
438  new_m_lit_size * new_m_cls_size - new_m_cls_size - new_m_lit_size;
439 
440  if (new_reduction <= reduction) break;
441  DCHECK_NE(1, new_m_lit_size);
442  DCHECK_NE(1, new_m_cls_size);
443 
444  // TODO(user): Instead of looping and recomputing p_ again, we can instead
445  // simply intersect the clause indices in p_. This should be a lot faster.
446  // That said, we loop again only when we have a reduction, so this happens
447  // not that often compared to the initial computation of p.
448  reduction = new_reduction;
449  m_lit_.insert(lmax);
450 
451  // Set m_cls_ to p_[lmax].
452  m_cls_.clear();
453  for (const auto entry : flattened_p_) {
454  literal_to_p_size_[entry.first] = 0;
455  if (entry.first == lmax) m_cls_.push_back(entry.second);
456  }
457  flattened_p_.clear();
458  }
459 
460  // Make sure literal_to_p_size_ is all zero.
461  for (const auto entry : flattened_p_) literal_to_p_size_[entry.first] = 0;
462  flattened_p_.clear();
463 
464  // A strictly positive reduction means that applying the BVA transform will
465  // reduce the overall number of clauses by that much. Here we can control
466  // what kind of reduction we want to apply.
467  if (reduction <= parameters_.presolve_bva_threshold()) return;
468  DCHECK_GT(m_lit_.size(), 1);
469 
470  // Create a new variable.
471  const int old_size = literal_to_clauses_.size();
472  const LiteralIndex x_true = LiteralIndex(old_size);
473  const LiteralIndex x_false = LiteralIndex(old_size + 1);
474  literal_to_clauses_.resize(old_size + 2);
475  literal_to_clause_sizes_.resize(old_size + 2);
476  bva_pq_elements_.resize(old_size + 2);
477  bva_pq_elements_[x_true.value()].literal = x_true;
478  bva_pq_elements_[x_false.value()].literal = x_false;
479 
480  // Add the new clauses.
481  if (drat_proof_handler_ != nullptr) drat_proof_handler_->AddOneVariable();
482  for (const LiteralIndex lit : m_lit_) {
483  tmp_new_clause_ = {Literal(lit), Literal(x_true)};
484  AddClauseInternal(&tmp_new_clause_);
485  }
486  for (const ClauseIndex ci : m_cls_) {
487  tmp_new_clause_ = clauses_[ci];
488  DCHECK(!tmp_new_clause_.empty());
489  for (Literal& ref : tmp_new_clause_) {
490  if (ref.Index() == l) {
491  ref = Literal(x_false);
492  break;
493  }
494  }
495 
496  // TODO(user): we can be more efficient here since the clause used to
497  // derive this one is already sorted. We just need to insert x_false in
498  // the correct place and remove l.
499  std::sort(tmp_new_clause_.begin(), tmp_new_clause_.end());
500  AddClauseInternal(&tmp_new_clause_);
501  }
502 
503  // Delete the old clauses.
504  //
505  // TODO(user): do that more efficiently? we can simply store the clause d
506  // instead of finding it again. That said, this is executed only when a
507  // reduction occur, whereas the start of this function occur all the time, so
508  // we want it to be as fast as possible.
509  for (const ClauseIndex c : m_cls_) {
510  const std::vector<Literal>& clause = clauses_[c];
511  DCHECK(!clause.empty());
512  const LiteralIndex l_min =
513  FindLiteralWithShortestOccurrenceListExcluding(clause, Literal(l));
514  for (const LiteralIndex lit : m_lit_) {
515  if (lit == l) continue;
516  for (const ClauseIndex d : literal_to_clauses_[l_min]) {
517  if (clause.size() != clauses_[d].size()) continue;
518  const LiteralIndex l_diff =
519  DifferAtGivenLiteral(clause, clauses_[d], Literal(l));
520  if (l_diff == lit) {
521  Remove(d);
522  break;
523  }
524  }
525  }
526  Remove(c);
527  }
528 
529  // Add these elements to the priority queue.
530  //
531  // TODO(user): It seems some of the element already processed could benefit
532  // from being processed again by SimpleBva(). It is unclear if it is worth the
533  // extra time though.
534  AddToBvaPriorityQueue(x_true);
535  AddToBvaPriorityQueue(x_false);
536  AddToBvaPriorityQueue(l);
537 }
538 
539 uint64 SatPresolver::ComputeSignatureOfClauseVariables(ClauseIndex ci) {
540  uint64 signature = 0;
541  for (const Literal l : clauses_[ci]) {
542  signature |= (uint64{1} << (l.Variable().value() % 64));
543  }
544  DCHECK_EQ(signature == 0, clauses_[ci].empty());
545  return signature;
546 }
547 
548 // We are looking for clause that contains lit and contains a superset of the
549 // literals in clauses_[clauses_index] or a superset with just one literal of
550 // clauses_[clause_index] negated.
551 bool SatPresolver::ProcessClauseToSimplifyOthersUsingLiteral(
552  ClauseIndex clause_index, Literal lit) {
553  const std::vector<Literal>& clause = clauses_[clause_index];
554  const uint64 clause_signature = signatures_[clause_index];
555  LiteralIndex opposite_literal;
556 
557  // Try to simplify the clauses containing 'lit'. We take advantage of this
558  // loop to also detect if there is any empty clause, in which case we will
559  // trigger a "cleaning" below.
560  bool need_cleaning = false;
561  num_inspected_signatures_ += literal_to_clauses_[lit.Index()].size();
562  for (const ClauseIndex ci : literal_to_clauses_[lit.Index()]) {
563  const uint64 ci_signature = signatures_[ci];
564 
565  // This allows to check for empty clause without fetching the memory at
566  // clause_[ci]. It can have a huge time impact on large problems.
567  DCHECK_EQ(ci_signature, ComputeSignatureOfClauseVariables(ci));
568  if (ci_signature == 0) {
569  need_cleaning = true;
570  continue;
571  }
572 
573  // Note that SimplifyClause() can return true only if the variables in
574  // 'a' are a subset of the one in 'b'. We use the signatures to abort
575  // early as a speed optimization.
576  if (ci != clause_index && (clause_signature & ~ci_signature) == 0 &&
577  SimplifyClause(clause, &clauses_[ci], &opposite_literal,
578  &num_inspected_literals_)) {
579  if (opposite_literal == kNoLiteralIndex) {
580  need_cleaning = true;
581  Remove(ci);
582  continue;
583  } else {
584  DCHECK_NE(opposite_literal, lit.Index());
585  if (clauses_[ci].empty()) return false; // UNSAT.
586  if (drat_proof_handler_ != nullptr) {
587  // TODO(user): remove the old clauses_[ci] afterwards.
588  drat_proof_handler_->AddClause(clauses_[ci]);
589  }
590 
591  // Recompute signature.
592  signatures_[ci] = ComputeSignatureOfClauseVariables(ci);
593 
594  // Remove ci from the occurrence list. Note that opposite_literal
595  // cannot be literal or literal.Negated().
596  gtl::STLEraseAllFromSequence(&literal_to_clauses_[opposite_literal],
597  ci);
598  --literal_to_clause_sizes_[opposite_literal];
599  UpdatePriorityQueue(Literal(opposite_literal).Variable());
600 
601  if (!in_clause_to_process_[ci]) {
602  in_clause_to_process_[ci] = true;
603  clause_to_process_.push_back(ci);
604  }
605  }
606  }
607  }
608 
609  if (need_cleaning) {
610  int new_index = 0;
611  auto& occurrence_list_ref = literal_to_clauses_[lit.Index()];
612  for (const ClauseIndex ci : occurrence_list_ref) {
613  if (signatures_[ci] != 0) occurrence_list_ref[new_index++] = ci;
614  }
615  occurrence_list_ref.resize(new_index);
616  DCHECK_EQ(literal_to_clause_sizes_[lit.Index()], new_index);
617  }
618 
619  return true;
620 }
621 
622 // TODO(user): Binary clauses are really common, and we can probably do this
623 // more efficiently for them. For instance, we could just take the intersection
624 // of two sorted lists to get the simplified clauses.
626  const std::vector<Literal>& clause = clauses_[clause_index];
627  if (clause.empty()) return true;
628  DCHECK(std::is_sorted(clause.begin(), clause.end()));
629 
630  LiteralIndex opposite_literal;
631  const Literal lit = FindLiteralWithShortestOccurrenceList(clause);
632 
633  if (!ProcessClauseToSimplifyOthersUsingLiteral(clause_index, lit)) {
634  return false;
635  }
636 
637  // If there is another "short" occurrence list, use it. Otherwise use the
638  // one corresponding to the negation of lit.
639  const LiteralIndex other_lit_index =
640  FindLiteralWithShortestOccurrenceListExcluding(clause, lit);
641  if (other_lit_index != kNoLiteralIndex &&
642  literal_to_clause_sizes_[other_lit_index] <
643  literal_to_clause_sizes_[lit.NegatedIndex()]) {
644  return ProcessClauseToSimplifyOthersUsingLiteral(clause_index,
645  Literal(other_lit_index));
646  } else {
647  // Treat the clauses containing lit.Negated().
648  int new_index = 0;
649  bool something_removed = false;
650  auto& occurrence_list_ref = literal_to_clauses_[lit.NegatedIndex()];
651  const uint64 clause_signature = signatures_[clause_index];
652  for (const ClauseIndex ci : occurrence_list_ref) {
653  const uint64 ci_signature = signatures_[ci];
654  DCHECK_EQ(ci_signature, ComputeSignatureOfClauseVariables(ci));
655  if (ci_signature == 0) continue;
656 
657  // TODO(user): not super optimal since we could abort earlier if
658  // opposite_literal is not the negation of shortest_list. Note that this
659  // applies to the second call to
660  // ProcessClauseToSimplifyOthersUsingLiteral() above too.
661  if ((clause_signature & ~ci_signature) == 0 &&
662  SimplifyClause(clause, &clauses_[ci], &opposite_literal,
663  &num_inspected_literals_)) {
664  DCHECK_EQ(opposite_literal, lit.NegatedIndex());
665  if (clauses_[ci].empty()) return false; // UNSAT.
666  if (drat_proof_handler_ != nullptr) {
667  // TODO(user): remove the old clauses_[ci] afterwards.
668  drat_proof_handler_->AddClause(clauses_[ci]);
669  }
670 
671  // Recompute signature.
672  signatures_[ci] = ComputeSignatureOfClauseVariables(ci);
673 
674  if (!in_clause_to_process_[ci]) {
675  in_clause_to_process_[ci] = true;
676  clause_to_process_.push_back(ci);
677  }
678  something_removed = true;
679  continue;
680  }
681  occurrence_list_ref[new_index] = ci;
682  ++new_index;
683  }
684  occurrence_list_ref.resize(new_index);
685  literal_to_clause_sizes_[lit.NegatedIndex()] = new_index;
686  if (something_removed) {
687  UpdatePriorityQueue(Literal(lit.NegatedIndex()).Variable());
688  }
689  }
690  return true;
691 }
692 
693 void SatPresolver::RemoveAndRegisterForPostsolveAllClauseContaining(Literal x) {
694  for (ClauseIndex i : literal_to_clauses_[x.Index()]) {
695  if (!clauses_[i].empty()) RemoveAndRegisterForPostsolve(i, x);
696  }
697  gtl::STLClearObject(&literal_to_clauses_[x.Index()]);
698  literal_to_clause_sizes_[x.Index()] = 0;
699 }
700 
702  const int s1 = literal_to_clause_sizes_[x.Index()];
703  const int s2 = literal_to_clause_sizes_[x.NegatedIndex()];
704 
705  // Note that if s1 or s2 is equal to 0, this function will implicitely just
706  // fix the variable x.
707  if (s1 == 0 && s2 == 0) return false;
708 
709  // Heuristic. Abort if the work required to decide if x should be removed
710  // seems to big.
711  if (s1 > 1 && s2 > 1 && s1 * s2 > parameters_.presolve_bve_threshold()) {
712  return false;
713  }
714 
715  // Compute the threshold under which we don't remove x.Variable().
716  int threshold = 0;
717  const int clause_weight = parameters_.presolve_bve_clause_weight();
718  for (ClauseIndex i : literal_to_clauses_[x.Index()]) {
719  if (!clauses_[i].empty()) {
720  threshold += clause_weight + clauses_[i].size();
721  }
722  }
723  for (ClauseIndex i : literal_to_clauses_[x.NegatedIndex()]) {
724  if (!clauses_[i].empty()) {
725  threshold += clause_weight + clauses_[i].size();
726  }
727  }
728 
729  // For the BCE, we prefer s2 to be small.
730  if (s1 < s2) x = x.Negated();
731 
732  // Test whether we should remove the x.Variable().
733  int size = 0;
734  for (ClauseIndex i : literal_to_clauses_[x.Index()]) {
735  if (clauses_[i].empty()) continue;
736  bool no_resolvant = true;
737  for (ClauseIndex j : literal_to_clauses_[x.NegatedIndex()]) {
738  if (clauses_[j].empty()) continue;
739  const int rs = ComputeResolvantSize(x, clauses_[i], clauses_[j]);
740  if (rs >= 0) {
741  no_resolvant = false;
742  size += clause_weight + rs;
743 
744  // Abort early if the "size" become too big.
745  if (size > threshold) return false;
746  }
747  }
748  if (no_resolvant && parameters_.presolve_blocked_clause()) {
749  // This is an incomplete heuristic for blocked clause detection. Here,
750  // the clause i is "blocked", so we can remove it. Note that the code
751  // below already do that if we decide to eliminate x.
752  //
753  // For more details, see the paper "Blocked clause elimination", Matti
754  // Jarvisalo, Armin Biere, Marijn Heule. TACAS, volume 6015 of Lecture
755  // Notes in Computer Science, pages 129–144. Springer, 2010.
756  //
757  // TODO(user): Choose if we use x or x.Negated() depending on the list
758  // sizes? The function achieve the same if x = x.Negated(), however the
759  // loops are not done in the same order which may change this incomplete
760  // "blocked" clause detection.
761  RemoveAndRegisterForPostsolve(i, x);
762  }
763  }
764 
765  // Add all the resolvant clauses.
766  // Note that the variable priority queue will only be updated during the
767  // deletion.
768  std::vector<Literal> temp;
769  for (ClauseIndex i : literal_to_clauses_[x.Index()]) {
770  if (clauses_[i].empty()) continue;
771  for (ClauseIndex j : literal_to_clauses_[x.NegatedIndex()]) {
772  if (clauses_[j].empty()) continue;
773  if (ComputeResolvant(x, clauses_[i], clauses_[j], &temp)) {
774  AddClauseInternal(&temp);
775  }
776  }
777  }
778 
779  // Deletes the old clauses.
780  //
781  // TODO(user): We could only update the priority queue once for each variable
782  // instead of doing it many times.
783  RemoveAndRegisterForPostsolveAllClauseContaining(x);
784  RemoveAndRegisterForPostsolveAllClauseContaining(x.Negated());
785 
786  // TODO(user): At this point x.Variable() is added back to the priority queue.
787  // Avoid doing that.
788  return true;
789 }
790 
791 void SatPresolver::Remove(ClauseIndex ci) {
792  signatures_[ci] = 0;
793  for (Literal e : clauses_[ci]) {
794  literal_to_clause_sizes_[e.Index()]--;
795  UpdatePriorityQueue(e.Variable());
796  UpdateBvaPriorityQueue(Literal(e.Variable(), true).Index());
797  UpdateBvaPriorityQueue(Literal(e.Variable(), false).Index());
798  }
799  if (drat_proof_handler_ != nullptr) {
800  drat_proof_handler_->DeleteClause(clauses_[ci]);
801  }
802  gtl::STLClearObject(&clauses_[ci]);
803 }
804 
805 void SatPresolver::RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x) {
806  postsolver_->Add(x, clauses_[ci]);
807  Remove(ci);
808 }
809 
810 Literal SatPresolver::FindLiteralWithShortestOccurrenceList(
811  const std::vector<Literal>& clause) {
812  DCHECK(!clause.empty());
813  Literal result = clause.front();
814  int best_size = literal_to_clause_sizes_[result.Index()];
815  for (const Literal l : clause) {
816  const int size = literal_to_clause_sizes_[l.Index()];
817  if (size < best_size) {
818  result = l;
819  best_size = size;
820  }
821  }
822  return result;
823 }
824 
825 LiteralIndex SatPresolver::FindLiteralWithShortestOccurrenceListExcluding(
826  const std::vector<Literal>& clause, Literal to_exclude) {
827  DCHECK(!clause.empty());
828  LiteralIndex result = kNoLiteralIndex;
829  int num_occurrences = std::numeric_limits<int>::max();
830  for (const Literal l : clause) {
831  if (l == to_exclude) continue;
832  if (literal_to_clause_sizes_[l.Index()] < num_occurrences) {
833  result = l.Index();
834  num_occurrences = literal_to_clause_sizes_[l.Index()];
835  }
836  }
837  return result;
838 }
839 
840 void SatPresolver::UpdatePriorityQueue(BooleanVariable var) {
841  if (var_pq_elements_.empty()) return; // not initialized.
842  PQElement* element = &var_pq_elements_[var];
843  element->weight = literal_to_clause_sizes_[Literal(var, true).Index()] +
844  literal_to_clause_sizes_[Literal(var, false).Index()];
845  if (var_pq_.Contains(element)) {
846  var_pq_.NoteChangedPriority(element);
847  } else {
848  var_pq_.Add(element);
849  }
850 }
851 
852 void SatPresolver::InitializePriorityQueue() {
853  const int num_vars = NumVariables();
854  var_pq_elements_.resize(num_vars);
855  for (BooleanVariable var(0); var < num_vars; ++var) {
856  PQElement* element = &var_pq_elements_[var];
857  element->variable = var;
858  element->weight = literal_to_clause_sizes_[Literal(var, true).Index()] +
859  literal_to_clause_sizes_[Literal(var, false).Index()];
860  var_pq_.Add(element);
861  }
862 }
863 
864 void SatPresolver::UpdateBvaPriorityQueue(LiteralIndex lit) {
865  if (bva_pq_elements_.empty()) return; // not initialized.
866  DCHECK_LT(lit, bva_pq_elements_.size());
867  BvaPqElement* element = &bva_pq_elements_[lit.value()];
868  element->weight = literal_to_clause_sizes_[lit];
869  if (bva_pq_.Contains(element)) {
870  bva_pq_.NoteChangedPriority(element);
871  }
872 }
873 
874 void SatPresolver::AddToBvaPriorityQueue(LiteralIndex lit) {
875  if (bva_pq_elements_.empty()) return; // not initialized.
876  DCHECK_LT(lit, bva_pq_elements_.size());
877  BvaPqElement* element = &bva_pq_elements_[lit.value()];
878  element->weight = literal_to_clause_sizes_[lit];
879  DCHECK(!bva_pq_.Contains(element));
880  if (element->weight > 2) bva_pq_.Add(element);
881 }
882 
883 void SatPresolver::InitializeBvaPriorityQueue() {
884  const int num_literals = 2 * NumVariables();
885  bva_pq_.Clear();
886  bva_pq_elements_.assign(num_literals, BvaPqElement());
887  for (LiteralIndex lit(0); lit < num_literals; ++lit) {
888  BvaPqElement* element = &bva_pq_elements_[lit.value()];
889  element->literal = lit;
890  element->weight = literal_to_clause_sizes_[lit];
891 
892  // If a literal occur only in two clauses, then there is no point calling
893  // SimpleBva() on it.
894  if (element->weight > 2) bva_pq_.Add(element);
895  }
896 }
897 
898 void SatPresolver::DisplayStats(double elapsed_seconds) {
899  int num_literals = 0;
900  int num_clauses = 0;
901  int num_singleton_clauses = 0;
902  for (const std::vector<Literal>& c : clauses_) {
903  if (!c.empty()) {
904  if (c.size() == 1) ++num_singleton_clauses;
905  ++num_clauses;
906  num_literals += c.size();
907  }
908  }
909  int num_one_side = 0;
910  int num_simple_definition = 0;
911  int num_vars = 0;
912  for (BooleanVariable var(0); var < NumVariables(); ++var) {
913  const int s1 = literal_to_clause_sizes_[Literal(var, true).Index()];
914  const int s2 = literal_to_clause_sizes_[Literal(var, false).Index()];
915  if (s1 == 0 && s2 == 0) continue;
916 
917  ++num_vars;
918  if (s1 == 0 || s2 == 0) {
919  num_one_side++;
920  } else if (s1 == 1 || s2 == 1) {
921  num_simple_definition++;
922  }
923  }
924  LOG(INFO) << " [" << elapsed_seconds << "s]"
925  << " clauses:" << num_clauses << " literals:" << num_literals
926  << " vars:" << num_vars << " one_side_vars:" << num_one_side
927  << " simple_definition:" << num_simple_definition
928  << " singleton_clauses:" << num_singleton_clauses;
929 }
930 
931 bool SimplifyClause(const std::vector<Literal>& a, std::vector<Literal>* b,
932  LiteralIndex* opposite_literal,
933  int64* num_inspected_literals) {
934  if (b->size() < a.size()) return false;
935  DCHECK(std::is_sorted(a.begin(), a.end()));
936  DCHECK(std::is_sorted(b->begin(), b->end()));
937  if (num_inspected_literals != nullptr) {
938  *num_inspected_literals += a.size();
939  *num_inspected_literals += b->size();
940  }
941 
942  *opposite_literal = LiteralIndex(-1);
943 
944  int num_diff = 0;
945  std::vector<Literal>::const_iterator ia = a.begin();
946  std::vector<Literal>::const_iterator ib = b->begin();
947  std::vector<Literal>::const_iterator to_remove;
948 
949  // Because we abort early when size_diff becomes negative, the second test
950  // in the while loop is not needed.
951  int size_diff = b->size() - a.size();
952  while (ia != a.end() /* && ib != b->end() */) {
953  if (*ia == *ib) { // Same literal.
954  ++ia;
955  ++ib;
956  } else if (*ia == ib->Negated()) { // Opposite literal.
957  ++num_diff;
958  if (num_diff > 1) return false; // Too much difference.
959  to_remove = ib;
960  ++ia;
961  ++ib;
962  } else if (*ia < *ib) {
963  return false; // A literal of a is not in b.
964  } else { // *ia > *ib
965  ++ib;
966 
967  // A literal of b is not in a, we can abort early by comparing the sizes
968  // left.
969  if (--size_diff < 0) return false;
970  }
971  }
972  if (num_diff == 1) {
973  *opposite_literal = to_remove->Index();
974  b->erase(to_remove);
975  }
976  return true;
977 }
978 
979 LiteralIndex DifferAtGivenLiteral(const std::vector<Literal>& a,
980  const std::vector<Literal>& b, Literal l) {
981  DCHECK_EQ(b.size(), a.size());
982  DCHECK(std::is_sorted(a.begin(), a.end()));
983  DCHECK(std::is_sorted(b.begin(), b.end()));
984  LiteralIndex result = kNoLiteralIndex;
985  std::vector<Literal>::const_iterator ia = a.begin();
986  std::vector<Literal>::const_iterator ib = b.begin();
987  while (ia != a.end() && ib != b.end()) {
988  if (*ia == *ib) { // Same literal.
989  ++ia;
990  ++ib;
991  } else if (*ia < *ib) {
992  // A literal of a is not in b, it must be l.
993  // Note that this can only happen once.
994  if (*ia != l) return kNoLiteralIndex;
995  ++ia;
996  } else {
997  // A literal of b is not in a, save it.
998  // We abort if this happen twice.
999  if (result != kNoLiteralIndex) return kNoLiteralIndex;
1000  result = (*ib).Index();
1001  ++ib;
1002  }
1003  }
1004  // Check the corner case of the difference at the end.
1005  if (ia != a.end() && *ia != l) return kNoLiteralIndex;
1006  if (ib != b.end()) {
1007  if (result != kNoLiteralIndex) return kNoLiteralIndex;
1008  result = (*ib).Index();
1009  }
1010  return result;
1011 }
1012 
1013 bool ComputeResolvant(Literal x, const std::vector<Literal>& a,
1014  const std::vector<Literal>& b,
1015  std::vector<Literal>* out) {
1016  DCHECK(std::is_sorted(a.begin(), a.end()));
1017  DCHECK(std::is_sorted(b.begin(), b.end()));
1018 
1019  out->clear();
1020  std::vector<Literal>::const_iterator ia = a.begin();
1021  std::vector<Literal>::const_iterator ib = b.begin();
1022  while ((ia != a.end()) && (ib != b.end())) {
1023  if (*ia == *ib) {
1024  out->push_back(*ia);
1025  ++ia;
1026  ++ib;
1027  } else if (*ia == ib->Negated()) {
1028  if (*ia != x) return false; // Trivially true.
1029  DCHECK_EQ(*ib, x.Negated());
1030  ++ia;
1031  ++ib;
1032  } else if (*ia < *ib) {
1033  out->push_back(*ia);
1034  ++ia;
1035  } else { // *ia > *ib
1036  out->push_back(*ib);
1037  ++ib;
1038  }
1039  }
1040 
1041  // Copy remaining literals.
1042  out->insert(out->end(), ia, a.end());
1043  out->insert(out->end(), ib, b.end());
1044  return true;
1045 }
1046 
1047 // Note that this function takes a big chunk of the presolve running time.
1048 int ComputeResolvantSize(Literal x, const std::vector<Literal>& a,
1049  const std::vector<Literal>& b) {
1050  DCHECK(std::is_sorted(a.begin(), a.end()));
1051  DCHECK(std::is_sorted(b.begin(), b.end()));
1052 
1053  int size = static_cast<int>(a.size() + b.size()) - 2;
1054  std::vector<Literal>::const_iterator ia = a.begin();
1055  std::vector<Literal>::const_iterator ib = b.begin();
1056  while ((ia != a.end()) && (ib != b.end())) {
1057  if (*ia == *ib) {
1058  --size;
1059  ++ia;
1060  ++ib;
1061  } else if (*ia == ib->Negated()) {
1062  if (*ia != x) return -1; // Trivially true.
1063  DCHECK_EQ(*ib, x.Negated());
1064  ++ia;
1065  ++ib;
1066  } else if (*ia < *ib) {
1067  ++ia;
1068  } else { // *ia > *ib
1069  ++ib;
1070  }
1071  }
1072  DCHECK_GE(size, 0);
1073  return size;
1074 }
1075 
1076 // A simple graph where the nodes are the literals and the nodes adjacent to a
1077 // literal l are the propagated literal when l is assigned in the underlying
1078 // sat solver.
1079 //
1080 // This can be used to do a strong component analysis while probing all the
1081 // literals of a solver. Note that this can be expensive, hence the support
1082 // for a deterministic time limit.
1084  public:
1085  PropagationGraph(double deterministic_time_limit, SatSolver* solver)
1086  : solver_(solver),
1087  deterministic_time_limit(solver->deterministic_time() +
1088  deterministic_time_limit) {}
1089 
1090  // Returns the set of node adjacent to the given one.
1091  // Interface needed by FindStronglyConnectedComponents(), note that it needs
1092  // to be const.
1093  const std::vector<int32>& operator[](int32 index) const {
1094  scratchpad_.clear();
1095  solver_->Backtrack(0);
1096 
1097  // Note that when the time limit is reached, we just keep returning empty
1098  // adjacency list. This way, the SCC algorithm will terminate quickly and
1099  // the equivalent literals detection will be incomplete but correct. Note
1100  // also that thanks to the SCC algorithm, we will explore the connected
1101  // components first.
1102  if (solver_->deterministic_time() > deterministic_time_limit) {
1103  return scratchpad_;
1104  }
1105 
1106  const Literal l = Literal(LiteralIndex(index));
1107  if (!solver_->Assignment().LiteralIsAssigned(l)) {
1108  const int trail_index = solver_->LiteralTrail().Index();
1110  if (solver_->CurrentDecisionLevel() > 0) {
1111  // Note that the +1 is to avoid adding a => a.
1112  for (int i = trail_index + 1; i < solver_->LiteralTrail().Index();
1113  ++i) {
1114  scratchpad_.push_back(solver_->LiteralTrail()[i].Index().value());
1115  }
1116  }
1117  }
1118  return scratchpad_;
1119  }
1120 
1121  private:
1122  mutable std::vector<int32> scratchpad_;
1123  SatSolver* const solver_;
1124  const double deterministic_time_limit;
1125 
1126  DISALLOW_COPY_AND_ASSIGN(PropagationGraph);
1127 };
1128 
1130  SatSolver* solver, SatPostsolver* postsolver,
1131  DratProofHandler* drat_proof_handler,
1133  WallTimer timer;
1134  timer.Start();
1135 
1136  solver->Backtrack(0);
1137  mapping->clear();
1138  const int num_already_fixed_vars = solver->LiteralTrail().Index();
1139 
1140  PropagationGraph graph(
1141  solver->parameters().presolve_probing_deterministic_time_limit(), solver);
1142  const int32 size = solver->NumVariables() * 2;
1143  std::vector<std::vector<int32>> scc;
1144  FindStronglyConnectedComponents(size, graph, &scc);
1145 
1146  // We have no guarantee that the cycle of x and not(x) touch the same
1147  // variables. This is because we may have more info for the literal probed
1148  // later or the propagation may go only in one direction. For instance if we
1149  // have two clauses (not(x1) v x2) and (not(x1) v not(x2) v x3) then x1
1150  // implies x2 and x3 but not(x3) doesn't imply anything by unit propagation.
1151  //
1152  // TODO(user): Add some constraint so that it does?
1153  //
1154  // Because of this, we "merge" the cycles.
1155  MergingPartition partition(size);
1156  for (const std::vector<int32>& component : scc) {
1157  if (component.size() > 1) {
1158  if (mapping->empty()) mapping->resize(size, LiteralIndex(-1));
1159  const Literal representative((LiteralIndex(component[0])));
1160  for (int i = 1; i < component.size(); ++i) {
1161  const Literal l((LiteralIndex(component[i])));
1162  // TODO(user): check compatibility? if x ~ not(x) => unsat.
1163  // but probably, the solver would have found this too? not sure...
1164  partition.MergePartsOf(representative.Index().value(),
1165  l.Index().value());
1166  partition.MergePartsOf(representative.NegatedIndex().value(),
1167  l.NegatedIndex().value());
1168  }
1169 
1170  // We rely on the fact that the representative of a literal x and the one
1171  // of its negation are the same variable.
1172  DCHECK_EQ(Literal(LiteralIndex(partition.GetRootAndCompressPath(
1173  representative.Index().value()))),
1174  Literal(LiteralIndex(partition.GetRootAndCompressPath(
1175  representative.NegatedIndex().value())))
1176  .Negated());
1177  }
1178  }
1179 
1180  solver->Backtrack(0);
1181  int num_equiv = 0;
1182  if (!mapping->empty()) {
1183  // If a variable in a cycle is fixed. We want to fix all of them.
1184  //
1185  // We first fix all representative if one variable of the cycle is fixed. In
1186  // a second pass we fix all the variable of a cycle whose representative is
1187  // fixed.
1188  //
1189  // TODO(user): Fixing a variable might fix more of them by propagation, so
1190  // we might not fix everything possible with these loops.
1191  const VariablesAssignment& assignment = solver->Assignment();
1192  for (LiteralIndex i(0); i < size; ++i) {
1193  const LiteralIndex rep(partition.GetRootAndCompressPath(i.value()));
1194  if (assignment.LiteralIsAssigned(Literal(i)) &&
1195  !assignment.LiteralIsAssigned(Literal(rep))) {
1196  const Literal true_lit = assignment.LiteralIsTrue(Literal(i))
1197  ? Literal(rep)
1198  : Literal(rep).Negated();
1199  solver->AddUnitClause(true_lit);
1200  if (drat_proof_handler != nullptr) {
1201  drat_proof_handler->AddClause({true_lit});
1202  }
1203  }
1204  }
1205  for (LiteralIndex i(0); i < size; ++i) {
1206  const LiteralIndex rep(partition.GetRootAndCompressPath(i.value()));
1207  (*mapping)[i] = rep;
1208  if (assignment.LiteralIsAssigned(Literal(rep))) {
1209  if (!assignment.LiteralIsAssigned(Literal(i))) {
1210  const Literal true_lit = assignment.LiteralIsTrue(Literal(rep))
1211  ? Literal(i)
1212  : Literal(i).Negated();
1213  solver->AddUnitClause(true_lit);
1214  if (drat_proof_handler != nullptr) {
1215  drat_proof_handler->AddClause({true_lit});
1216  }
1217  }
1218  } else if (assignment.LiteralIsAssigned(Literal(i))) {
1219  if (!assignment.LiteralIsAssigned(Literal(rep))) {
1220  const Literal true_lit = assignment.LiteralIsTrue(Literal(i))
1221  ? Literal(rep)
1222  : Literal(rep).Negated();
1223  solver->AddUnitClause(true_lit);
1224  if (drat_proof_handler != nullptr) {
1225  drat_proof_handler->AddClause({true_lit});
1226  }
1227  }
1228  } else if (rep != i) {
1229  ++num_equiv;
1230  postsolver->Add(Literal(i), {Literal(i), Literal(rep).Negated()});
1231  if (drat_proof_handler != nullptr) {
1232  drat_proof_handler->AddClause({Literal(i), Literal(rep).Negated()});
1233  }
1234  }
1235  }
1236  }
1237 
1238  const bool log_info =
1239  solver->parameters().log_search_progress() || VLOG_IS_ON(1);
1240  LOG_IF(INFO, log_info) << "Probing. fixed " << num_already_fixed_vars << " + "
1241  << solver->LiteralTrail().Index() -
1242  num_already_fixed_vars
1243  << " equiv " << num_equiv / 2 << " total "
1244  << solver->NumVariables() << " wtime: " << timer.Get();
1245 }
1246 
1247 SatSolver::Status SolveWithPresolve(std::unique_ptr<SatSolver>* solver,
1249  std::vector<bool>* solution,
1250  DratProofHandler* drat_proof_handler) {
1251  // We save the initial parameters.
1252  const SatParameters parameters = (*solver)->parameters();
1253  SatPostsolver postsolver((*solver)->NumVariables());
1254 
1255  const bool log_info = parameters.log_search_progress() || VLOG_IS_ON(1);
1256 
1257  // Some problems are formulated in such a way that our SAT heuristics
1258  // simply works without conflict. Get them out of the way first because it
1259  // is possible that the presolve lose this "lucky" ordering. This is in
1260  // particular the case on the SAT14.crafted.complete-xxx-... problems.
1261  {
1262  Model* model = (*solver)->model();
1263  const double dtime = std::min(1.0, time_limit->GetDeterministicTimeLeft());
1264  if (!LookForTrivialSatSolution(dtime, model, log_info)) {
1265  VLOG(1) << "UNSAT during probing.";
1266  return SatSolver::INFEASIBLE;
1267  }
1268  const int num_variables = (*solver)->NumVariables();
1269  if ((*solver)->LiteralTrail().Index() == num_variables) {
1270  VLOG(1) << "Problem solved by trivial heuristic!";
1271  solution->clear();
1272  for (int i = 0; i < (*solver)->NumVariables(); ++i) {
1273  solution->push_back((*solver)->Assignment().LiteralIsTrue(
1274  Literal(BooleanVariable(i), true)));
1275  }
1276  return SatSolver::FEASIBLE;
1277  }
1278  }
1279 
1280  // We use a new block so the memory used by the presolver can be
1281  // reclaimed as soon as it is no longer needed.
1282  const int max_num_passes = 4;
1283  for (int i = 0; i < max_num_passes && !time_limit->LimitReached(); ++i) {
1284  const int saved_num_variables = (*solver)->NumVariables();
1285 
1286  // Run the new preprocessing code. Note that the probing that it does is
1287  // faster than the ProbeAndFindEquivalentLiteral() call below, but does not
1288  // do equivalence detection as completely, so we still apply the other
1289  // "probing" code afterwards even if it will not fix more literals, but it
1290  // will do one pass of proper equivalence detection.
1291  {
1292  Model* model = (*solver)->model();
1293  model->GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(time_limit);
1294  SatPresolveOptions options;
1295  options.log_info = log_info;
1296  options.extract_binary_clauses_in_probing = false;
1297  options.use_transitive_reduction = false;
1298  options.deterministic_time_limit =
1299  parameters.presolve_probing_deterministic_time_limit();
1300 
1301  if (!model->GetOrCreate<Inprocessing>()->PresolveLoop(options)) {
1302  VLOG(1) << "UNSAT during probing.";
1303  return SatSolver::INFEASIBLE;
1304  }
1305  for (const auto& c : model->GetOrCreate<PostsolveClauses>()->clauses) {
1306  postsolver.Add(c[0], c);
1307  }
1308  }
1309 
1310  // Probe + find equivalent literals.
1311  // TODO(user): Use a derived time limit in the probing phase.
1313  ProbeAndFindEquivalentLiteral((*solver).get(), &postsolver,
1314  drat_proof_handler, &equiv_map);
1315  if ((*solver)->IsModelUnsat()) {
1316  VLOG(1) << "UNSAT during probing.";
1317  return SatSolver::INFEASIBLE;
1318  }
1319 
1320  // The rest of the presolve only work on pure SAT problem.
1321  if (!(*solver)->ProblemIsPureSat()) {
1322  VLOG(1) << "The problem is not a pure SAT problem, skipping the SAT "
1323  "specific presolve.";
1324  break;
1325  }
1326 
1327  // Register the fixed variables with the postsolver.
1328  // TODO(user): Find a better place for this?
1329  (*solver)->Backtrack(0);
1330  for (int i = 0; i < (*solver)->LiteralTrail().Index(); ++i) {
1331  postsolver.FixVariable((*solver)->LiteralTrail()[i]);
1332  }
1333 
1334  // TODO(user): Pass the time_limit to the presolver.
1335  SatPresolver presolver(&postsolver);
1336  presolver.SetParameters(parameters);
1337  presolver.SetDratProofHandler(drat_proof_handler);
1338  presolver.SetEquivalentLiteralMapping(equiv_map);
1339  (*solver)->ExtractClauses(&presolver);
1340  (*solver)->AdvanceDeterministicTime(time_limit);
1341 
1342  // Tricky: the model local time limit is updated by the new functions, but
1343  // the old ones update time_limit directly.
1344  time_limit->AdvanceDeterministicTime((*solver)
1345  ->model()
1346  ->GetOrCreate<TimeLimit>()
1347  ->GetElapsedDeterministicTime());
1348 
1349  (*solver).reset(nullptr);
1350  std::vector<bool> can_be_removed(presolver.NumVariables(), true);
1351  if (!presolver.Presolve(can_be_removed, log_info)) {
1352  VLOG(1) << "UNSAT during presolve.";
1353 
1354  // This is just here to reset the SatSolver::Solve() satistics.
1355  (*solver) = absl::make_unique<SatSolver>();
1356  return SatSolver::INFEASIBLE;
1357  }
1358 
1359  postsolver.ApplyMapping(presolver.VariableMapping());
1360  if (drat_proof_handler != nullptr) {
1361  drat_proof_handler->ApplyMapping(presolver.VariableMapping());
1362  }
1363 
1364  // Load the presolved problem in a new solver.
1365  (*solver) = absl::make_unique<SatSolver>();
1366  (*solver)->SetDratProofHandler(drat_proof_handler);
1367  (*solver)->SetParameters(parameters);
1368  presolver.LoadProblemIntoSatSolver((*solver).get());
1369 
1370  // Stop if a fixed point has been reached.
1371  if ((*solver)->NumVariables() == saved_num_variables) break;
1372  }
1373 
1374  // Before solving, we use the new probing code that adds all new binary
1375  // implication it can find to the binary implication graph. This gives good
1376  // benefits. Note that we currently do not do it before presolve because then
1377  // the current presolve code does not work too well with the potential huge
1378  // number of binary clauses added.
1379  //
1380  // TODO(user): Revisit the situation when we simplify better all the clauses
1381  // using binary ones. Or if/when we support at most one better in pure SAT
1382  // solving and presolve.
1383  {
1384  Model* model = (*solver)->model();
1385  model->GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(time_limit);
1386  SatPresolveOptions options;
1387  options.log_info = log_info;
1388  options.use_transitive_reduction = true;
1389  options.extract_binary_clauses_in_probing = true;
1390  options.deterministic_time_limit =
1391  model->GetOrCreate<SatParameters>()
1392  ->presolve_probing_deterministic_time_limit();
1393  if (!model->GetOrCreate<Inprocessing>()->PresolveLoop(options)) {
1394  return SatSolver::INFEASIBLE;
1395  }
1396  for (const auto& c : model->GetOrCreate<PostsolveClauses>()->clauses) {
1397  postsolver.Add(c[0], c);
1398  }
1399  }
1400 
1401  // Solve.
1402  const SatSolver::Status result = (*solver)->SolveWithTimeLimit(time_limit);
1403  if (result == SatSolver::FEASIBLE) {
1404  *solution = postsolver.ExtractAndPostsolveSolution(**solver);
1405  }
1406  return result;
1407 }
1408 
1409 } // namespace sat
1410 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define LOG_IF(severity, condition)
Definition: base/logging.h:479
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
#define VLOG(verboselevel)
Definition: base/logging.h:978
bool Contains(const T *val) const
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)
int MergePartsOf(int node1, int node2)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
Definition: time_limit.h:532
void DeleteClause(absl::Span< const Literal > clause)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
void AddClause(absl::Span< const Literal > clause)
bool PresolveLoop(SatPresolveOptions options)
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
LiteralIndex Index() const
Definition: sat_base.h:84
BooleanVariable Variable() const
Definition: sat_base.h:80
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
const std::vector< int32 > & operator[](int32 index) const
PropagationGraph(double deterministic_time_limit, SatSolver *solver)
void Add(Literal x, const absl::Span< const Literal > clause)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
std::vector< bool > PostsolveSolution(const std::vector< bool > &solution)
std::vector< bool > ExtractAndPostsolveSolution(const SatSolver &solver)
void SetNumVariables(int num_variables)
void LoadProblemIntoSatSolver(SatSolver *solver)
void AddBinaryClause(Literal a, Literal b)
void SetEquivalentLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping)
void SetParameters(const SatParameters &params)
absl::StrongVector< BooleanVariable, BooleanVariable > VariableMapping() const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
void AddClause(absl::Span< const Literal > clause)
bool ProcessClauseToSimplifyOthers(ClauseIndex clause_index)
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
void SetNumVariables(int num_variables)
Definition: sat_solver.cc:64
const SatParameters & parameters() const
Definition: sat_solver.cc:110
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
Definition: sat_solver.cc:499
void Backtrack(int target_level)
Definition: sat_solver.cc:888
bool AddProblemClause(absl::Span< const Literal > literals)
Definition: sat_solver.cc:203
bool AddUnitClause(Literal true_literal)
Definition: sat_solver.cc:164
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
void AssignFromTrueLiteral(Literal literal)
Definition: sat_base.h:133
SatParameters parameters
SharedTimeLimit * time_limit
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
int64_t int64
uint64_t uint64
const int INFO
Definition: log_severity.h:31
void STLEraseAllFromSequence(T *v, const E &e)
Definition: stl_util.h:93
void STLClearObject(T *obj)
Definition: stl_util.h:123
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
Definition: probing.cc:270
int ComputeResolvantSize(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b)
const LiteralIndex kNoLiteralIndex(-1)
SatSolver::Status SolveWithPresolve(std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler)
LiteralIndex DifferAtGivenLiteral(const std::vector< Literal > &a, const std::vector< Literal > &b, Literal l)
bool ComputeResolvant(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b, std::vector< Literal > *out)
void ProbeAndFindEquivalentLiteral(SatSolver *solver, SatPostsolver *postsolver, DratProofHandler *drat_proof_handler, absl::StrongVector< LiteralIndex, LiteralIndex > *mapping)
const BooleanVariable kNoBooleanVariable(-1)
bool SimplifyClause(const std::vector< Literal > &a, std::vector< Literal > *b, LiteralIndex *opposite_literal, int64 *num_inspected_literals)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int index
Definition: pack.cc:508
ColIndex representative
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
std::deque< std::vector< Literal > > clauses
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41