OR-Tools  8.2
sat_inprocessing.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 "absl/container/inlined_vector.h"
17 #include "ortools/base/stl_util.h"
19 #include "ortools/base/timer.h"
20 #include "ortools/sat/probing.h"
22 
23 namespace operations_research {
24 namespace sat {
25 
27  Literal literal, absl::Span<const Literal> clause) {
28  bool found = false;
29  clauses.emplace_back(clause.begin(), clause.end());
30  for (int i = 0; i < clause.size(); ++i) {
31  if (clause[i] == literal) {
32  found = true;
33  std::swap(clauses.back()[0], clauses.back()[i]);
34  break;
35  }
36  }
37  CHECK(found);
38 }
39 
40 #define RETURN_IF_FALSE(f) \
41  if (!(f)) return false;
42 
45  wall_timer.Start();
46 
47  const bool log_info = options.log_info || VLOG_IS_ON(1);
48  const bool log_round_info = VLOG_IS_ON(1);
49 
50  // Mainly useful for development.
51  double probing_time = 0.0;
52 
53  // We currently do the transformations in a given order and restart each time
54  // we did something to make sure that the earlier step cannot srengthen more.
55  // This might not be the best, but it is really good during development phase
56  // to make sure each individual functions is as incremental and as fast as
57  // possible.
58  const double start_dtime = time_limit_->GetElapsedDeterministicTime();
59  const double stop_dtime = start_dtime + options.deterministic_time_limit;
60  while (!time_limit_->LimitReached() &&
61  time_limit_->GetElapsedDeterministicTime() <= stop_dtime) {
62  CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
63  if (!LevelZeroPropagate()) return false;
64 
65  // This one is fast since only newly fixed variables are considered.
66  implication_graph_->RemoveFixedVariables();
67 
68  // This also prepare the stamping below so that we do that on a DAG and do
69  // not consider potential new implications added by
70  // RemoveFixedAndEquivalentVariables().
72  log_round_info));
73 
74  // TODO(user): This should/could be integrated with the stamping since it
75  // seems better to do just one loop instead of two over all clauses. Because
76  // of memory access. it isn't that clear though.
78  RETURN_IF_FALSE(stamping_simplifier_->DoOneRound(log_round_info));
79 
80  // We wait for the fix-point to be reached before doing the other
81  // simplifications below.
83  !implication_graph_->IsDag()) {
84  continue;
85  }
86 
89  !implication_graph_->IsDag()) {
90  continue;
91  }
92 
93  // TODO(user): Combine the two? this way we don't create a full literal <->
94  // clause graph twice. It might make sense to reach the BCE fix point which
95  // is unique before each variable elimination.
96  blocked_clause_simplifier_->DoOneRound(log_round_info);
97  RETURN_IF_FALSE(bounded_variable_elimination_->DoOneRound(log_round_info));
99 
100  // Probing.
101  const double saved_wtime = wall_timer.Get();
102  const double time_left =
103  stop_dtime - time_limit_->GetElapsedDeterministicTime();
104  if (time_left <= 0) break;
105  ProbingOptions probing_options;
106  probing_options.log_info = log_round_info;
107  probing_options.deterministic_limit = time_left;
108  probing_options.extract_binary_clauses =
110  RETURN_IF_FALSE(FailedLiteralProbingRound(probing_options, model_));
111  probing_time += wall_timer.Get() - saved_wtime;
112 
114  !implication_graph_->IsDag()) {
115  continue;
116  }
117 
118  break;
119  }
120 
121  // TODO(user): Maintain the total number of literals in the watched clauses.
122  if (!LevelZeroPropagate()) return false;
123 
124  LOG_IF(INFO, log_info)
125  << "Presolve."
126  << " num_fixed: " << trail_->Index()
127  << " num_redundant: " << implication_graph_->num_redundant_literals() / 2
128  << "/" << sat_solver_->NumVariables()
129  << " num_implications: " << implication_graph_->num_implications()
130  << " num_watched_clauses: " << clause_manager_->num_watched_clauses()
131  << " dtime: " << time_limit_->GetElapsedDeterministicTime() - start_dtime
132  << "/" << options.deterministic_time_limit
133  << " wtime: " << wall_timer.Get()
134  << " non-probing time: " << (wall_timer.Get() - probing_time);
135  return true;
136 }
137 
140  wall_timer.Start();
141 
142  const bool log_info = true || VLOG_IS_ON(1);
143  const bool log_round_info = VLOG_IS_ON(1);
144 
145  // Mainly useful for development.
146  double probing_time = 0.0;
147  const double start_dtime = time_limit_->GetElapsedDeterministicTime();
148 
149  // Try to spend a given ratio of time in the inprocessing.
150  if (total_dtime_ > 0.1 * start_dtime) return true;
151 
152  // We make sure we do not "pollute" the current saved polarities. We will
153  // restore them at the end.
154  //
155  // TODO(user): We should probably also disable the variable/clauses activity
156  // updates.
157  decision_policy_->MaybeEnablePhaseSaving(/*save_phase=*/false);
158 
159  RETURN_IF_FALSE(DetectEquivalencesAndStamp(true, log_round_info));
162 
163  // Probing.
164  const double saved_wtime = wall_timer.Get();
165  ProbingOptions probing_options;
166  probing_options.log_info = log_round_info;
167  probing_options.deterministic_limit = 5;
168  probing_options.extract_binary_clauses = true;
169  RETURN_IF_FALSE(FailedLiteralProbingRound(probing_options, model_));
170  probing_time += wall_timer.Get() - saved_wtime;
171 
172  RETURN_IF_FALSE(DetectEquivalencesAndStamp(true, log_round_info));
175 
176  RETURN_IF_FALSE(stamping_simplifier_->DoOneRound(log_round_info));
178 
179  // TODO(user): Add a small wrapper function to time this.
181  sat_solver_->MinimizeSomeClauses(/*decisions_budget=*/1000);
183 
185 
187  blocked_clause_simplifier_->DoOneRound(log_round_info);
188  RETURN_IF_FALSE(bounded_variable_elimination_->DoOneRound(log_round_info));
190 
191  total_dtime_ += time_limit_->GetElapsedDeterministicTime() - start_dtime;
192  LOG_IF(INFO, log_info)
193  << "Presolve."
194  << " num_fixed: " << trail_->Index()
195  << " num_redundant: " << implication_graph_->num_redundant_literals() / 2
196  << "/" << sat_solver_->NumVariables()
197  << " num_implications: " << implication_graph_->num_implications()
198  << " num_watched_clauses: " << clause_manager_->num_watched_clauses()
199  << " dtime: " << time_limit_->GetElapsedDeterministicTime() - start_dtime
200  << " wtime: " << wall_timer.Get()
201  << " non-probing time: " << (wall_timer.Get() - probing_time);
202 
203  decision_policy_->MaybeEnablePhaseSaving(/*save_phase=*/true);
204  return true;
205 }
206 
207 #undef RETURN_IF_FALSE
208 
210  const int64 new_num_fixed_variables = trail_->Index();
211  return last_num_fixed_variables_ < new_num_fixed_variables;
212 }
213 
215  const int64 new_num_redundant_literals =
216  implication_graph_->num_redundant_literals();
217  return last_num_redundant_literals_ < new_num_redundant_literals;
218 }
219 
221  CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
222  clause_manager_->AttachAllClauses();
223  return sat_solver_->Propagate();
224 }
225 
226 // It make sense to do the pre-stamping right after the equivalence detection
227 // since it needs a DAG and can detect extra failed literal.
228 bool Inprocessing::DetectEquivalencesAndStamp(bool use_transitive_reduction,
229  bool log_info) {
230  if (!LevelZeroPropagate()) return false;
231  implication_graph_->RemoveFixedVariables();
232  if (!implication_graph_->IsDag()) {
233  // TODO(user): consider doing the transitive reduction after each SCC.
234  // It might be slow but we could try to make it more incremental to
235  // compensate and it should allow further reduction.
236  if (!implication_graph_->DetectEquivalences(log_info)) return false;
237  if (!LevelZeroPropagate()) return false;
238  if (use_transitive_reduction) {
239  if (!implication_graph_->ComputeTransitiveReduction(log_info)) {
240  return false;
241  }
242  if (!LevelZeroPropagate()) return false;
243  }
244  }
245 
246  if (!stamping_simplifier_->ComputeStampsForNextRound(log_info)) return false;
247  return LevelZeroPropagate();
248 }
249 
251  // Preconditions.
252  //
253  // TODO(user): The level zero is required because we remove fixed variables
254  // but if we split this into two functions, we could rewrite clause at any
255  // level.
256  CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
257  if (!LevelZeroPropagate()) return false;
258 
259  // Test if some work is needed.
260  //
261  // TODO(user): If only new fixed variables are there, we can use a faster
262  // function. We should also merge the code with the deletion code in
263  // sat_solver_.cc, but that require some refactoring of the dependence between
264  // files.
265  const int64 new_num_redundant_literals =
266  implication_graph_->num_redundant_literals();
267  const int64 new_num_fixed_variables = trail_->Index();
268  if (last_num_redundant_literals_ == new_num_redundant_literals &&
269  last_num_fixed_variables_ == new_num_fixed_variables) {
270  return true;
271  }
272  last_num_fixed_variables_ = new_num_fixed_variables;
273  last_num_redundant_literals_ = new_num_redundant_literals;
274 
275  // Start the round.
277  wall_timer.Start();
278 
279  int64 num_removed_literals = 0;
280  int64 num_inspected_literals = 0;
281 
282  // We need this temporary vector for the DRAT proof settings, otherwise
283  // we could just have done an in-place transformation.
284  std::vector<Literal> new_clause;
285 
286  // Used to mark clause literals.
287  const int num_literals(sat_solver_->NumVariables() * 2);
288  absl::StrongVector<LiteralIndex, bool> marked(num_literals, false);
289 
290  clause_manager_->DeleteRemovedClauses();
291  clause_manager_->DetachAllClauses();
292  for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) {
293  bool removed = false;
294  bool need_rewrite = false;
295 
296  // We first do a loop to see if there is anything to do.
297  for (const Literal l : clause->AsSpan()) {
298  if (assignment_.LiteralIsTrue(l)) {
299  // TODO(user): we should output literal to the proof right away,
300  // currently if we remove clauses before fixing literal the proof is
301  // wrong.
302  if (!clause_manager_->InprocessingFixLiteral(l)) return false;
303  clause_manager_->InprocessingRemoveClause(clause);
304  num_removed_literals += clause->size();
305  removed = true;
306  break;
307  }
308  if (assignment_.LiteralIsFalse(l) || implication_graph_->IsRedundant(l)) {
309  need_rewrite = true;
310  break;
311  }
312  }
313 
314  num_inspected_literals += clause->size();
315  if (removed || !need_rewrite) continue;
316  num_inspected_literals += clause->size();
317 
318  // Rewrite the clause.
319  new_clause.clear();
320  for (const Literal l : clause->AsSpan()) {
321  const Literal r = implication_graph_->RepresentativeOf(l);
322  if (marked[r.Index()] || assignment_.LiteralIsFalse(r)) {
323  continue;
324  }
325  if (marked[r.NegatedIndex()] || assignment_.LiteralIsTrue(r)) {
326  clause_manager_->InprocessingRemoveClause(clause);
327  num_removed_literals += clause->size();
328  removed = true;
329  break;
330  }
331  marked[r.Index()] = true;
332  new_clause.push_back(r);
333  }
334 
335  // Restore marked.
336  for (const Literal l : new_clause) marked[l.Index()] = false;
337  if (removed) continue;
338 
339  num_removed_literals += clause->size() - new_clause.size();
340  if (!clause_manager_->InprocessingRewriteClause(clause, new_clause)) {
341  return false;
342  }
343  }
344 
345  // TODO(user): find a way to auto-tune that after a run on borg...
346  const double dtime = static_cast<double>(num_inspected_literals) * 1e-8;
347  time_limit_->AdvanceDeterministicTime(dtime);
348  LOG_IF(INFO, log_info) << "Cleanup. num_removed_literals: "
349  << num_removed_literals << " dtime: " << dtime
350  << " wtime: " << wall_timer.Get();
351  return true;
352 }
353 
354 // TODO(user): Use better work limits, see SAT09.CRAFTED.ramseycube.Q3inK12
355 //
356 // TODO(user): Be more incremental, each time a clause is added/reduced track
357 // which literal are impacted? Also try to do orthogonal reductions from one
358 // round to the next.
361  wall_timer.Start();
362 
363  int64 num_subsumed_clauses = 0;
364  int64 num_removed_literals = 0;
365  int64 num_inspected_signatures = 0;
366  int64 num_inspected_literals = 0;
367 
368  // We need this temporary vector for the DRAT proof settings, otherwise
369  // we could just have done an in-place transformation.
370  std::vector<Literal> new_clause;
371 
372  // This function needs the watcher to be detached as we might remove some
373  // of the watched literals.
374  //
375  // TODO(user): We could do that only if we do some reduction, but this is
376  // quite fast though.
377  clause_manager_->DeleteRemovedClauses();
378  clause_manager_->DetachAllClauses();
379 
380  // Process clause by increasing sizes.
381  // TODO(user): probably faster without the size indirection.
382  std::vector<SatClause*> clauses =
383  clause_manager_->AllClausesInCreationOrder();
384  std::sort(clauses.begin(), clauses.end(),
385  [](SatClause* a, SatClause* b) { return a->size() < b->size(); });
386 
387  // Used to mark clause literals.
388  const LiteralIndex num_literals(sat_solver_->NumVariables() * 2);
389  SparseBitset<LiteralIndex> marked(num_literals);
390 
391  // Clause index in clauses.
392  // TODO(user): Storing signatures here might be faster?
394  num_literals.value());
395 
396  // Clause signatures in the same order as clauses.
397  std::vector<uint64> signatures(clauses.size());
398 
399  std::vector<Literal> candidates_for_removal;
400  for (int clause_index = 0; clause_index < clauses.size(); ++clause_index) {
401  SatClause* clause = clauses[clause_index];
402 
403  // TODO(user): Better abort limit. We could also limit the watcher sizes and
404  // never look at really long clauses. Note that for an easier
405  // incrementality, it is better to reach some kind of completion so we know
406  // what new stuff need to be done.
407  if (num_inspected_literals + num_inspected_signatures > 1e9) {
408  break;
409  }
410 
411  // Check for subsumption, note that this currently ignore all clauses in the
412  // binary implication graphs. Stamping is doing some of that (and some also
413  // happen during probing), but we could consider only direct implications
414  // here and be a bit more exhaustive than what stamping do with them (at
415  // least for node with many incoming and outgoing implications).
416  //
417  // TODO(user): Do some reduction using binary clauses. Note that only clause
418  // that never propagated since last round need to be checked for binary
419  // subsumption.
420 
421  // Compute hash and mark literals.
422  uint64 signature = 0;
423  marked.SparseClearAll();
424  for (const Literal l : clause->AsSpan()) {
425  marked.Set(l.Index());
426  signature |= (uint64{1} << (l.Variable().value() % 64));
427  }
428 
429  // Look for clause that subsumes this one. Note that because we inspect
430  // all one watcher lists for the literals of this clause, if a clause is
431  // included inside this one, it must appear in one of these lists.
432  bool removed = false;
433  candidates_for_removal.clear();
434  const uint64 mask = ~signature;
435  for (const Literal l : clause->AsSpan()) {
436  num_inspected_signatures += one_watcher[l.Index()].size();
437  for (const int i : one_watcher[l.Index()]) {
438  if ((mask & signatures[i]) != 0) continue;
439 
440  bool subsumed = true;
441  bool stengthen = true;
442  LiteralIndex to_remove = kNoLiteralIndex;
443  num_inspected_literals += clauses[i]->size();
444  for (const Literal o : clauses[i]->AsSpan()) {
445  if (!marked[o.Index()]) {
446  subsumed = false;
447  if (to_remove == kNoLiteralIndex && marked[o.NegatedIndex()]) {
448  to_remove = o.NegatedIndex();
449  } else {
450  stengthen = false;
451  break;
452  }
453  }
454  }
455  if (subsumed) {
456  ++num_subsumed_clauses;
457  num_removed_literals += clause->size();
458  clause_manager_->InprocessingRemoveClause(clause);
459  removed = true;
460  break;
461  }
462  if (stengthen) {
463  CHECK_NE(kNoLiteralIndex, to_remove);
464  candidates_for_removal.push_back(Literal(to_remove));
465  }
466  }
467  if (removed) break;
468  }
469  if (removed) continue;
470 
471  // For strengthenning we also need to check the negative watcher lists.
472  for (const Literal l : clause->AsSpan()) {
473  num_inspected_signatures += one_watcher[l.NegatedIndex()].size();
474  for (const int i : one_watcher[l.NegatedIndex()]) {
475  if ((mask & signatures[i]) != 0) continue;
476 
477  bool stengthen = true;
478  num_inspected_literals += clauses[i]->size();
479  for (const Literal o : clauses[i]->AsSpan()) {
480  if (o == l.Negated()) continue;
481  if (!marked[o.Index()]) {
482  stengthen = false;
483  break;
484  }
485  }
486  if (stengthen) {
487  candidates_for_removal.push_back(l);
488  }
489  }
490  }
491 
492  // Any literal here can be removed, but afterwards the other might not. For
493  // now we just remove the first one.
494  //
495  // TODO(user): remove first and see if other still removable. Alternatively
496  // use a "removed" marker and redo a check for each clause that simplifies
497  // this one? Or just remove the first one, and wait for next round.
498  if (!candidates_for_removal.empty()) {
499  new_clause.clear();
500  for (const Literal l : clause->AsSpan()) {
501  new_clause.push_back(l);
502  }
503 
504  int new_size = 0;
505  for (const Literal l : new_clause) {
506  if (l == candidates_for_removal[0]) continue;
507  new_clause[new_size++] = l;
508  }
509  CHECK_EQ(new_size + 1, new_clause.size());
510  new_clause.resize(new_size);
511 
512  num_removed_literals += clause->size() - new_clause.size();
513  if (!clause_manager_->InprocessingRewriteClause(clause, new_clause)) {
514  return false;
515  }
516  if (clause->size() == 0) continue;
517 
518  // Recompute signature.
519  signature = 0;
520  for (const Literal l : clause->AsSpan()) {
521  signature |= (uint64{1} << (l.Variable().value() % 64));
522  }
523  }
524 
525  // Register one literal to watch. Any literal works, but we choose the
526  // smallest list.
527  //
528  // TODO(user): No need to add this clause if we know it cannot subsume
529  // any new clause since last round. i.e. unchanged clause that do not
530  // contains any literals of newly added clause do not need to be added
531  // here. We can track two bitset in LiteralWatchers via a register
532  // mechanism:
533  // - literal of newly watched clauses since last clear.
534  // - literal of reduced clauses since last clear.
535  //
536  // Important: we can only use this clause to subsume/strenghten others if
537  // it cannot be deleted later.
538  if (!clause_manager_->IsRemovable(clause)) {
539  int min_size = kint32max;
540  LiteralIndex min_literal = kNoLiteralIndex;
541  for (const Literal l : clause->AsSpan()) {
542  if (one_watcher[l.Index()].size() < min_size) {
543  min_size = one_watcher[l.Index()].size();
544  min_literal = l.Index();
545  }
546  }
547 
548  // TODO(user): We could/should sort the literal in this clause by
549  // using literals that appear in a small number of clauses first so that
550  // we maximize the chance of early abort in the critical loops above.
551  //
552  // TODO(user): We could also move the watched literal first so we always
553  // skip it.
554  signatures[clause_index] = signature;
555  one_watcher[min_literal].push_back(clause_index);
556  }
557  }
558 
559  // We might have fixed variables, finish the propagation.
560  if (!LevelZeroPropagate()) return false;
561 
562  // TODO(user): tune the deterministic time.
563  const double dtime = static_cast<double>(num_inspected_signatures) * 1e-8 +
564  static_cast<double>(num_inspected_literals) * 5e-9;
565  time_limit_->AdvanceDeterministicTime(dtime);
566  LOG_IF(INFO, log_info) << "Subsume. num_removed_literals: "
567  << num_removed_literals
568  << " num_subsumed: " << num_subsumed_clauses
569  << " dtime: " << dtime
570  << " wtime: " << wall_timer.Get();
571  return true;
572 }
573 
574 bool StampingSimplifier::DoOneRound(bool log_info) {
576  wall_timer.Start();
577 
578  dtime_ = 0.0;
579  num_subsumed_clauses_ = 0;
580  num_removed_literals_ = 0;
581  num_fixed_ = 0;
582 
583  if (implication_graph_->literal_size() == 0) return true;
584  if (implication_graph_->num_implications() == 0) return true;
585 
586  if (!stamps_are_already_computed_) {
587  // We need a DAG so that we don't have cycle while we sample the tree.
588  // TODO(user): We could probably deal with it if needed so that we don't
589  // need to do equivalence detetion each time we want to run this.
590  implication_graph_->RemoveFixedVariables();
591  if (!implication_graph_->DetectEquivalences(log_info)) return true;
593  if (!ComputeStamps()) return false;
594  }
595  stamps_are_already_computed_ = false;
596  if (!ProcessClauses()) return false;
597 
598  // Note that num_removed_literals_ do not count the literals of the subsumed
599  // clauses.
600  time_limit_->AdvanceDeterministicTime(dtime_);
601  log_info |= VLOG_IS_ON(1);
602  LOG_IF(INFO, log_info) << "Stamping. num_removed_literals: "
603  << num_removed_literals_
604  << " num_subsumed: " << num_subsumed_clauses_
605  << " num_fixed: " << num_fixed_ << " dtime: " << dtime_
606  << " wtime: " << wall_timer.Get();
607  return true;
608 }
609 
612  wall_timer.Start();
613  dtime_ = 0.0;
614  num_fixed_ = 0;
615 
616  if (implication_graph_->literal_size() == 0) return true;
617  if (implication_graph_->num_implications() == 0) return true;
618 
619  implication_graph_->RemoveFixedVariables();
620  if (!implication_graph_->DetectEquivalences(log_info)) return true;
622  if (!ComputeStamps()) return false;
623  stamps_are_already_computed_ = true;
624 
625  // TODO(user): compute some dtime, it is always zero currently.
626  time_limit_->AdvanceDeterministicTime(dtime_);
627  log_info |= VLOG_IS_ON(1);
628  LOG_IF(INFO, log_info) << "Prestamping."
629  << " num_fixed: " << num_fixed_ << " dtime: " << dtime_
630  << " wtime: " << wall_timer.Get();
631  return true;
632 }
633 
635  const int size = implication_graph_->literal_size();
636  CHECK(implication_graph_->IsDag()); // so we don't have cycle.
637  parents_.resize(size);
638  for (LiteralIndex i(0); i < size; ++i) {
639  parents_[i] = i; // default.
640  if (implication_graph_->IsRedundant(Literal(i))) continue;
641  if (assignment_.LiteralIsAssigned(Literal(i))) continue;
642 
643  // TODO(user): Better algo to not select redundant parent.
644  //
645  // TODO(user): if parents_[x] = y, try not to have parents_[not(y)] = not(x)
646  // because this is not as useful for the simplification power.
647  //
648  // TODO(user): More generally, we could sample a parent while probing so
649  // that we consider all hyper binary implications (in the case we don't add
650  // them to the implication graph already).
651  const auto& children_of_not_l =
652  implication_graph_->DirectImplications(Literal(i).Negated());
653  if (children_of_not_l.empty()) continue;
654  for (int num_tries = 0; num_tries < 10; ++num_tries) {
655  const Literal candidate =
656  children_of_not_l[absl::Uniform<int>(*random_, 0,
657  children_of_not_l.size())]
658  .Negated();
659  if (implication_graph_->IsRedundant(candidate)) continue;
660  if (i == candidate.Index()) continue;
661 
662  // We found an interesting parent.
663  parents_[i] = candidate.Index();
664  break;
665  }
666  }
667 }
668 
670  const int size = implication_graph_->literal_size();
671 
672  // Compute sizes.
673  sizes_.assign(size, 0);
674  for (LiteralIndex i(0); i < size; ++i) {
675  if (parents_[i] == i) continue; // leaf.
676  sizes_[parents_[i]]++;
677  }
678 
679  // Compute starts in the children_ vector for each node.
680  starts_.resize(size + 1); // We use a sentinel.
681  starts_[LiteralIndex(0)] = 0;
682  for (LiteralIndex i(1); i <= size; ++i) {
683  starts_[i] = starts_[i - 1] + sizes_[i - 1];
684  }
685 
686  // Fill children. This messes up starts_.
687  children_.resize(size);
688  for (LiteralIndex i(0); i < size; ++i) {
689  if (parents_[i] == i) continue; // leaf.
690  children_[starts_[parents_[i]]++] = i;
691  }
692 
693  // Reset starts to correct value.
694  for (LiteralIndex i(0); i < size; ++i) {
695  starts_[i] -= sizes_[i];
696  }
697 
698  if (DEBUG_MODE) {
699  CHECK_EQ(starts_[LiteralIndex(0)], 0);
700  for (LiteralIndex i(1); i <= size; ++i) {
701  CHECK_EQ(starts_[i], starts_[i - 1] + sizes_[i - 1]);
702  }
703  }
704 
705  // Perform a DFS from each root to compute the stamps.
706  int64 stamp = 0;
707  first_stamps_.resize(size);
708  last_stamps_.resize(size);
709  marked_.assign(size, false);
710  for (LiteralIndex i(0); i < size; ++i) {
711  if (parents_[i] != i) continue; // Not a root.
712  DCHECK(!marked_[i]);
713  const LiteralIndex tree_root = i;
714  dfs_stack_.push_back(i);
715  while (!dfs_stack_.empty()) {
716  const LiteralIndex top = dfs_stack_.back();
717  if (marked_[top]) {
718  dfs_stack_.pop_back();
719  last_stamps_[top] = stamp++;
720  continue;
721  }
722  first_stamps_[top] = stamp++;
723  marked_[top] = true;
724 
725  // Failed literal detection. If the negation of top is in the same
726  // tree, we can fix the LCA of top and its negation to false.
727  if (marked_[Literal(top).NegatedIndex()] &&
728  first_stamps_[Literal(top).NegatedIndex()] >=
729  first_stamps_[tree_root]) {
730  // Find the LCA.
731  const int first_stamp = first_stamps_[Literal(top).NegatedIndex()];
732  LiteralIndex lca = top;
733  while (first_stamps_[lca] > first_stamp) {
734  lca = parents_[lca];
735  }
736  ++num_fixed_;
737  if (!clause_manager_->InprocessingFixLiteral(Literal(lca).Negated())) {
738  return false;
739  }
740  }
741 
742  const int end = starts_[top + 1]; // Ok with sentinel.
743  for (int j = starts_[top]; j < end; ++j) {
744  DCHECK_NE(top, children_[j]); // We removed leaf self-loop.
745  DCHECK(!marked_[children_[j]]); // This is a tree.
746  dfs_stack_.push_back(children_[j]);
747  }
748  }
749  }
750  DCHECK_EQ(stamp, 2 * size);
751  return true;
752 }
753 
755  struct Entry {
756  int i; // Index in the clause.
757  bool is_negated; // Correspond to clause[i] or clause[i].Negated();
758  int start; // Note that all start stamps are different.
759  int end;
760  bool operator<(const Entry& o) const { return start < o.start; }
761  };
762  std::vector<int> to_remove;
763  std::vector<Literal> new_clause;
764  std::vector<Entry> entries;
765  clause_manager_->DeleteRemovedClauses();
766  clause_manager_->DetachAllClauses();
767  for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) {
768  const auto span = clause->AsSpan();
769  if (span.empty()) continue;
770 
771  // Note that we might fix literal as we perform the loop here, so we do
772  // need to deal with them.
773  //
774  // For a and b in the clause, if not(a) => b is present, then the clause is
775  // subsumed. If a => b, then a can be removed, and if not(a) => not(b) then
776  // b can be removed. Nothing can be done if a => not(b).
777  entries.clear();
778  for (int i = 0; i < span.size(); ++i) {
779  if (assignment_.LiteralIsTrue(span[i])) {
780  clause_manager_->InprocessingRemoveClause(clause);
781  break;
782  }
783  if (assignment_.LiteralIsFalse(span[i])) continue;
784  entries.push_back({i, false, first_stamps_[span[i].Index()],
785  last_stamps_[span[i].Index()]});
786  entries.push_back({i, true, first_stamps_[span[i].NegatedIndex()],
787  last_stamps_[span[i].NegatedIndex()]});
788  }
789  if (clause->empty()) continue;
790 
791  // The sort should be dominant.
792  if (!entries.empty()) {
793  const double n = static_cast<double>(entries.size());
794  dtime_ += 1.5e-8 * n * std::log(n);
795  std::sort(entries.begin(), entries.end());
796  }
797 
798  Entry top_entry;
799  top_entry.end = -1; // Sentinel.
800  to_remove.clear();
801  for (const Entry& e : entries) {
802  if (e.end < top_entry.end) {
803  // We found an implication: top_entry => this entry.
804  const Literal lhs = top_entry.is_negated ? span[top_entry.i].Negated()
805  : span[top_entry.i];
806  const Literal rhs = e.is_negated ? span[e.i].Negated() : span[e.i];
807  DCHECK(ImplicationIsInTree(lhs, rhs));
808 
809  if (top_entry.is_negated != e.is_negated) {
810  // Failed literal?
811  if (top_entry.i == e.i) {
812  ++num_fixed_;
813  if (top_entry.is_negated) {
814  // not(span[i]) => span[i] so span[i] true.
815  // And the clause is satisfied (so we count as as subsumed).
816  if (!clause_manager_->InprocessingFixLiteral(span[top_entry.i])) {
817  return false;
818  }
819  } else {
820  // span[i] => not(span[i]) so span[i] false.
821  if (!clause_manager_->InprocessingFixLiteral(
822  span[top_entry.i].Negated())) {
823  return false;
824  }
825  to_remove.push_back(top_entry.i);
826  continue;
827  }
828  }
829 
830  // not(a) => b : subsumption.
831  // a => not(b), we cannot deduce anything, but it might make sense
832  // to see if not(b) implies anything instead of just keeping
833  // top_entry. See TODO below.
834  if (top_entry.is_negated) {
835  num_subsumed_clauses_++;
836  clause_manager_->InprocessingRemoveClause(clause);
837  break;
838  }
839  } else {
840  CHECK_NE(top_entry.i, e.i);
841  if (top_entry.is_negated) {
842  // not(a) => not(b), we can remove b.
843  to_remove.push_back(e.i);
844  } else {
845  // a => b, we can remove a.
846  //
847  // TODO(user): Note that it is okay to still use top_entry, but we
848  // might miss the removal of b if b => c. Also the paper do things
849  // differently. Make sure we don't miss any simplification
850  // opportunites by not changing top_entry. Same in the other
851  // branches.
852  to_remove.push_back(top_entry.i);
853  }
854  }
855  } else {
856  top_entry = e;
857  }
858  }
859 
860  if (clause->empty()) continue;
861 
862  // Strengthen the clause.
863  if (!to_remove.empty() || entries.size() < span.size()) {
864  new_clause.clear();
866  int to_remove_index = 0;
867  for (int i = 0; i < span.size(); ++i) {
868  if (to_remove_index < to_remove.size() &&
869  i == to_remove[to_remove_index]) {
870  ++to_remove_index;
871  continue;
872  }
873  if (assignment_.LiteralIsTrue(span[i])) {
874  clause_manager_->InprocessingRemoveClause(clause);
875  continue;
876  }
877  if (assignment_.LiteralIsFalse(span[i])) continue;
878  new_clause.push_back(span[i]);
879  }
880  num_removed_literals_ += span.size() - new_clause.size();
881  if (!clause_manager_->InprocessingRewriteClause(clause, new_clause)) {
882  return false;
883  }
884  }
885  }
886  return true;
887 }
888 
891  wall_timer.Start();
892 
893  dtime_ = 0.0;
894  num_blocked_clauses_ = 0;
895  num_inspected_literals_ = 0;
896 
897  InitializeForNewRound();
898 
899  while (!time_limit_->LimitReached() && !queue_.empty()) {
900  const Literal l = queue_.front();
901  in_queue_[l.Index()] = false;
902  queue_.pop_front();
903  ProcessLiteral(l);
904  }
905 
906  // Release some memory.
907  literal_to_clauses_.clear();
908 
909  dtime_ += 1e-8 * num_inspected_literals_;
910  time_limit_->AdvanceDeterministicTime(dtime_);
911  log_info |= VLOG_IS_ON(1);
912  LOG_IF(INFO, log_info) << "Blocked clause. num_blocked_clauses: "
913  << num_blocked_clauses_ << " dtime: " << dtime_
914  << " wtime: " << wall_timer.Get();
915 }
916 
917 void BlockedClauseSimplifier::InitializeForNewRound() {
918  clauses_.clear();
919  clause_manager_->DeleteRemovedClauses();
920  clause_manager_->DetachAllClauses();
921  for (SatClause* c : clause_manager_->AllClausesInCreationOrder()) {
922  // We ignore redundant clause. This shouldn't cause any validity issue.
923  if (clause_manager_->IsRemovable(c)) continue;
924 
925  clauses_.push_back(c);
926  }
927  const int num_literals = clause_manager_->literal_size();
928 
929  // TODO(user): process in order of increasing number of clause that contains
930  // not(l)?
931  in_queue_.assign(num_literals, true);
932  for (LiteralIndex l(0); l < num_literals; ++l) {
933  queue_.push_back(Literal(l));
934  }
935 
936  marked_.resize(num_literals);
937  DCHECK(
938  std::all_of(marked_.begin(), marked_.end(), [](bool b) { return !b; }));
939 
940  // TODO(user): because we don't create new clause here we can use a flat
941  // vector for literal_to_clauses_.
942  literal_to_clauses_.clear();
943  literal_to_clauses_.resize(num_literals);
944  for (ClauseIndex i(0); i < clauses_.size(); ++i) {
945  for (const Literal l : clauses_[i]->AsSpan()) {
946  literal_to_clauses_[l.Index()].push_back(i);
947  }
948  num_inspected_literals_ += clauses_[i]->size();
949  }
950 }
951 
952 void BlockedClauseSimplifier::ProcessLiteral(Literal current_literal) {
953  if (assignment_.LiteralIsAssigned(current_literal)) return;
954  if (implication_graph_->IsRemoved(current_literal)) return;
955 
956  // We want to check first that this clause will resolve to trivial clause with
957  // all binary containing not(current_literal). So mark all literal l so that
958  // current_literal => l.
959  //
960  // TODO(user): We do not need to redo that each time we reprocess
961  // current_literal.
962  //
963  // TODO(user): Ignore redundant literals. That might require pushing
964  // equivalence to the postsolve stack though. Better to simply remove
965  // these equivalence if we are allowed to and update the postsolve then.
966  //
967  // TODO(user): Make this work in the presence of at most ones.
968  int num_binary = 0;
969  const std::vector<Literal>& implications =
970  implication_graph_->DirectImplications(current_literal);
971  for (const Literal l : implications) {
972  if (l == current_literal) continue;
973  ++num_binary;
974  marked_[l.Index()] = true;
975  }
976 
977  // TODO(user): We could also mark a small clause containing
978  // current_literal.Negated(), and make sure we only include in
979  // clauses_to_process clauses that resolve trivially with that clause.
980  std::vector<ClauseIndex> clauses_to_process;
981  for (const ClauseIndex i : literal_to_clauses_[current_literal.Index()]) {
982  if (clauses_[i]->empty()) continue;
983 
984  // Blocked with respect to binary clause only? all marked binary should have
985  // their negation in clause.
986  //
987  // TODO(user): Abort if size left is too small.
988  if (num_binary > 0) {
989  if (clauses_[i]->size() <= num_binary) continue;
990  int num_with_negation_marked = 0;
991  for (const Literal l : clauses_[i]->AsSpan()) {
992  if (l == current_literal) continue;
993  if (marked_[l.NegatedIndex()]) {
994  ++num_with_negation_marked;
995  }
996  }
997  num_inspected_literals_ += clauses_[i]->size();
998  if (num_with_negation_marked < num_binary) continue;
999  }
1000  clauses_to_process.push_back(i);
1001  }
1002 
1003  // Clear marked.
1004  for (const Literal l : implications) {
1005  marked_[l.Index()] = false;
1006  }
1007 
1008  // TODO(user): There is a possible optimization: If we mark all literals of
1009  // all the clause to process, we can check that each clause containing
1010  // current_literal.Negated() contains at least one of these literal negated
1011  // other than current_literal. Otherwise none of the clause are blocked.
1012  //
1013  // TODO(user): If a clause cannot be blocked because of another clause, then
1014  // when we call ProcessLiteral(current_literal.Negated()) we can skip some
1015  // inspection.
1016  for (const ClauseIndex i : clauses_to_process) {
1017  const auto c = clauses_[i]->AsSpan();
1018  if (ClauseIsBlocked(current_literal, c)) {
1019  // Reprocess all clauses that have a negated literal in this one as
1020  // some might be blocked now.
1021  //
1022  // TODO(user): Maybe we can remember for which (literal, clause) pair this
1023  // was used as a certificate for "not-blocked" and just reprocess those,
1024  // but it might be memory intensive.
1025  for (const Literal l : c) {
1026  if (!in_queue_[l.NegatedIndex()]) {
1027  in_queue_[l.NegatedIndex()] = true;
1028  queue_.push_back(l.Negated());
1029  }
1030  }
1031 
1032  // Add the clause to the postsolving set.
1033  postsolve_->AddClauseWithSpecialLiteral(current_literal, c);
1034 
1035  // We can remove a blocked clause.
1036  ++num_blocked_clauses_;
1037  clause_manager_->InprocessingRemoveClause(clauses_[i]);
1038  }
1039  }
1040 }
1041 
1042 // Note that this assume that the binary clauses have already been checked.
1043 bool BlockedClauseSimplifier::ClauseIsBlocked(
1044  Literal current_literal, absl::Span<const Literal> clause) {
1045  bool is_blocked = true;
1046  for (const Literal l : clause) marked_[l.Index()] = true;
1047 
1048  // TODO(user): For faster reprocessing of the same literal, we should move
1049  // all clauses that are used in a non-blocked certificate first in the list.
1050  for (const ClauseIndex i :
1051  literal_to_clauses_[current_literal.NegatedIndex()]) {
1052  if (clauses_[i]->empty()) continue;
1053  bool some_marked = false;
1054  for (const Literal l : clauses_[i]->AsSpan()) {
1055  // TODO(user): we can be faster here by only updating it at the end?
1056  ++num_inspected_literals_;
1057 
1058  if (l == current_literal.Negated()) continue;
1059  if (marked_[l.NegatedIndex()]) {
1060  some_marked = true;
1061  break;
1062  }
1063  }
1064  if (!some_marked) {
1065  is_blocked = false;
1066  break;
1067  }
1068  }
1069 
1070  for (const Literal l : clause) marked_[l.Index()] = false;
1071  return is_blocked;
1072 }
1073 
1076  wall_timer.Start();
1077 
1078  dtime_ = 0.0;
1079  num_inspected_literals_ = 0;
1080  num_eliminated_variables_ = 0;
1081  num_literals_diff_ = 0;
1082  num_clauses_diff_ = 0;
1083  num_simplifications_ = 0;
1084  num_blocked_clauses_ = 0;
1085 
1086  clauses_.clear();
1087  clause_manager_->DeleteRemovedClauses();
1088  clause_manager_->DetachAllClauses();
1089  for (SatClause* c : clause_manager_->AllClausesInCreationOrder()) {
1090  // We ignore redundant clause. This shouldn't cause any validity issue.
1091  // TODO(user): but we shouldn't keep clauses containing removed literals.
1092  // It is still valid to do so, but it should be less efficient.
1093  if (clause_manager_->IsRemovable(c)) continue;
1094 
1095  clauses_.push_back(c);
1096  }
1097  const int num_literals = clause_manager_->literal_size();
1098  const int num_variables = num_literals / 2;
1099 
1100  literal_to_clauses_.clear();
1101  literal_to_clauses_.resize(num_literals);
1102  literal_to_num_clauses_.assign(num_literals, 0);
1103  for (ClauseIndex i(0); i < clauses_.size(); ++i) {
1104  for (const Literal l : clauses_[i]->AsSpan()) {
1105  literal_to_clauses_[l.Index()].push_back(i);
1106  literal_to_num_clauses_[l.Index()]++;
1107  }
1108  num_inspected_literals_ += clauses_[i]->size();
1109  }
1110 
1111  const int saved_trail_index = trail_->Index();
1112  propagation_index_ = trail_->Index();
1113 
1114  need_to_be_updated_.clear();
1115  in_need_to_be_updated_.resize(num_variables);
1116  queue_.Reserve(num_variables);
1117  for (BooleanVariable v(0); v < num_variables; ++v) {
1118  if (assignment_.VariableIsAssigned(v)) continue;
1119  if (implication_graph_->IsRemoved(Literal(v, true))) continue;
1120  UpdatePriorityQueue(v);
1121  }
1122 
1123  marked_.resize(num_literals);
1124  DCHECK(
1125  std::all_of(marked_.begin(), marked_.end(), [](bool b) { return !b; }));
1126 
1127  // TODO(user): add a local dtime limit for the corner case where this take too
1128  // much time. We can adapt the limit depending on how much we want to spend on
1129  // inprocessing.
1130  while (!time_limit_->LimitReached() && !queue_.IsEmpty()) {
1131  const BooleanVariable top = queue_.Top().var;
1132  queue_.Pop();
1133 
1134  // Make sure we fix variables first if needed. Note that because new binary
1135  // clause might appear when we fix variables, we need a loop here.
1136  //
1137  // TODO(user): we might also find new equivalent variable l => var => l
1138  // here, but for now we ignore those.
1139  bool is_unsat = false;
1140  if (!Propagate()) return false;
1141  while (implication_graph_->FindFailedLiteralAroundVar(top, &is_unsat)) {
1142  if (!Propagate()) return false;
1143  }
1144  if (is_unsat) return false;
1145 
1146  if (!CrossProduct(top)) return false;
1147 
1148  for (const BooleanVariable v : need_to_be_updated_) {
1149  in_need_to_be_updated_[v] = false;
1150 
1151  // Currently we never re-add top if we just processed it.
1152  if (v != top) UpdatePriorityQueue(v);
1153  }
1154  in_need_to_be_updated_.clear();
1155  need_to_be_updated_.clear();
1156  }
1157 
1158  implication_graph_->CleanupAllRemovedVariables();
1159 
1160  // Remove all redundant clause containing a removed literal. This avoid to
1161  // re-introduce a removed literal via conflict learning.
1162  for (SatClause* c : clause_manager_->AllClausesInCreationOrder()) {
1163  if (!clause_manager_->IsRemovable(c)) continue;
1164  bool remove = false;
1165  for (const Literal l : c->AsSpan()) {
1166  if (implication_graph_->IsRemoved(l)) {
1167  remove = true;
1168  break;
1169  }
1170  }
1171  if (remove) clause_manager_->InprocessingRemoveClause(c);
1172  }
1173 
1174  // Release some memory.
1175  literal_to_clauses_.clear();
1176  literal_to_num_clauses_.clear();
1177 
1178  dtime_ += 1e-8 * num_inspected_literals_;
1179  time_limit_->AdvanceDeterministicTime(dtime_);
1180  log_info |= VLOG_IS_ON(1);
1181  LOG_IF(INFO, log_info) << "BVE."
1182  << " num_fixed: "
1183  << trail_->Index() - saved_trail_index
1184  << " num_simplified_literals: " << num_simplifications_
1185  << " num_blocked_clauses_: " << num_blocked_clauses_
1186  << " num_eliminations: " << num_eliminated_variables_
1187  << " num_literals_diff: " << num_literals_diff_
1188  << " num_clause_diff: " << num_clauses_diff_
1189  << " dtime: " << dtime_
1190  << " wtime: " << wall_timer.Get();
1191  return true;
1192 }
1193 
1194 bool BoundedVariableElimination::RemoveLiteralFromClause(
1195  Literal lit, SatClause* sat_clause) {
1196  num_literals_diff_ -= sat_clause->size();
1197  resolvant_.clear();
1198  for (const Literal l : sat_clause->AsSpan()) {
1199  if (l == lit || assignment_.LiteralIsFalse(l)) {
1200  literal_to_num_clauses_[l.Index()]--;
1201  continue;
1202  }
1203  if (assignment_.LiteralIsTrue(l)) {
1204  num_clauses_diff_--;
1205  clause_manager_->InprocessingRemoveClause(sat_clause);
1206  return true;
1207  }
1208  resolvant_.push_back(l);
1209  }
1210  if (!clause_manager_->InprocessingRewriteClause(sat_clause, resolvant_)) {
1211  return false;
1212  }
1213  if (sat_clause->empty()) {
1214  --num_clauses_diff_;
1215  for (const Literal l : resolvant_) literal_to_num_clauses_[l.Index()]--;
1216  } else {
1217  num_literals_diff_ += sat_clause->size();
1218  }
1219  return true;
1220 }
1221 
1222 bool BoundedVariableElimination::Propagate() {
1223  for (; propagation_index_ < trail_->Index(); ++propagation_index_) {
1224  // Make sure we always propagate the binary clauses first.
1225  if (!implication_graph_->Propagate(trail_)) return false;
1226 
1227  const Literal l = (*trail_)[propagation_index_];
1228  for (const ClauseIndex index : literal_to_clauses_[l.Index()]) {
1229  if (clauses_[index]->empty()) continue;
1230  num_clauses_diff_--;
1231  num_literals_diff_ -= clauses_[index]->size();
1232  clause_manager_->InprocessingRemoveClause(clauses_[index]);
1233  }
1234  literal_to_clauses_[l.Index()].clear();
1235  for (const ClauseIndex index : literal_to_clauses_[l.NegatedIndex()]) {
1236  if (clauses_[index]->empty()) continue;
1237  if (!RemoveLiteralFromClause(l.Negated(), clauses_[index])) return false;
1238  }
1239  literal_to_clauses_[l.NegatedIndex()].clear();
1240  }
1241  return true;
1242 }
1243 
1244 // Note that we use the estimated size here to make it fast. It is okay if the
1245 // order of elimination is not perfect... We can improve on this later.
1246 int BoundedVariableElimination::NumClausesContaining(Literal l) {
1247  return literal_to_num_clauses_[l.Index()] +
1248  implication_graph_->DirectImplicationsEstimatedSize(l.Negated());
1249 }
1250 
1251 // TODO(user): Only enqueue variable that can be removed.
1252 void BoundedVariableElimination::UpdatePriorityQueue(BooleanVariable var) {
1253  if (assignment_.VariableIsAssigned(var)) return;
1254  const int priority = -NumClausesContaining(Literal(var, true)) -
1255  NumClausesContaining(Literal(var, false));
1256  if (queue_.Contains(var.value())) {
1257  queue_.ChangePriority({var, priority});
1258  } else {
1259  queue_.Add({var, priority});
1260  }
1261 }
1262 
1263 void BoundedVariableElimination::DeleteClause(SatClause* sat_clause) {
1264  const auto clause = sat_clause->AsSpan();
1265 
1266  num_clauses_diff_--;
1267  num_literals_diff_ -= clause.size();
1268 
1269  // Update literal <-> clause graph.
1270  for (const Literal l : clause) {
1271  literal_to_num_clauses_[l.Index()]--;
1272  if (!in_need_to_be_updated_[l.Variable()]) {
1273  in_need_to_be_updated_[l.Variable()] = true;
1274  need_to_be_updated_.push_back(l.Variable());
1275  }
1276  }
1277 
1278  // Lazy deletion of the clause.
1279  clause_manager_->InprocessingRemoveClause(sat_clause);
1280 }
1281 
1282 void BoundedVariableElimination::DeleteAllClausesContaining(Literal literal) {
1283  for (const ClauseIndex i : literal_to_clauses_[literal.Index()]) {
1284  const auto clause = clauses_[i]->AsSpan();
1285  if (clause.empty()) continue;
1286  postsolve_->AddClauseWithSpecialLiteral(literal, clause);
1287  DeleteClause(clauses_[i]);
1288  }
1289  literal_to_clauses_[literal.Index()].clear();
1290 }
1291 
1292 void BoundedVariableElimination::AddClause(absl::Span<const Literal> clause) {
1293  SatClause* pt = clause_manager_->InprocessingAddClause(clause);
1294  if (pt == nullptr) return;
1295 
1296  num_clauses_diff_++;
1297  num_literals_diff_ += clause.size();
1298 
1299  const ClauseIndex index(clauses_.size());
1300  clauses_.push_back(pt);
1301  for (const Literal l : clause) {
1302  literal_to_num_clauses_[l.Index()]++;
1303  literal_to_clauses_[l.Index()].push_back(index);
1304  if (!in_need_to_be_updated_[l.Variable()]) {
1305  in_need_to_be_updated_[l.Variable()] = true;
1306  need_to_be_updated_.push_back(l.Variable());
1307  }
1308  }
1309 }
1310 
1311 template <bool score_only, bool with_binary_only>
1312 bool BoundedVariableElimination::ResolveAllClauseContaining(Literal lit) {
1313  const int clause_weight = parameters_.presolve_bve_clause_weight();
1314 
1315  const std::vector<Literal>& implications =
1316  implication_graph_->DirectImplications(lit);
1317  auto& clause_containing_lit = literal_to_clauses_[lit.Index()];
1318  for (int i = 0; i < clause_containing_lit.size(); ++i) {
1319  const ClauseIndex clause_index = clause_containing_lit[i];
1320  const auto clause = clauses_[clause_index]->AsSpan();
1321  if (clause.empty()) continue;
1322 
1323  if (!score_only) resolvant_.clear();
1324  for (const Literal l : clause) {
1325  if (!score_only && l != lit) resolvant_.push_back(l);
1326  marked_[l.Index()] = true;
1327  }
1328  num_inspected_literals_ += clause.size() + implications.size();
1329 
1330  // If this is true, then "clause" is subsumed by one of its resolvant and we
1331  // can just remove lit from it. Then it doesn't need to be acounted at all.
1332  bool clause_can_be_simplified = false;
1333  const int64 saved_score = new_score_;
1334 
1335  // Resolution with binary clauses.
1336  for (const Literal l : implications) {
1337  CHECK_NE(l, lit);
1338  if (marked_[l.NegatedIndex()]) continue; // trivial.
1339  if (marked_[l.Index()]) {
1340  clause_can_be_simplified = true;
1341  break;
1342  } else {
1343  if (score_only) {
1344  new_score_ += clause_weight + clause.size();
1345  } else {
1346  resolvant_.push_back(l);
1347  AddClause(resolvant_);
1348  resolvant_.pop_back();
1349  }
1350  }
1351  }
1352 
1353  // Resolution with non-binary clauses.
1354  if (!with_binary_only && !clause_can_be_simplified) {
1355  auto& clause_containing_not_lit = literal_to_clauses_[lit.NegatedIndex()];
1356  for (int j = 0; j < clause_containing_not_lit.size(); ++j) {
1357  if (score_only && new_score_ > score_threshold_) break;
1358  const ClauseIndex other_index = clause_containing_not_lit[j];
1359  const auto other = clauses_[other_index]->AsSpan();
1360  if (other.empty()) continue;
1361  bool trivial = false;
1362  int extra_size = 0;
1363  for (const Literal l : other) {
1364  // TODO(user): we can optimize this by updating it outside the loop.
1365  ++num_inspected_literals_;
1366  if (l == lit.Negated()) continue;
1367  if (marked_[l.NegatedIndex()]) {
1368  trivial = true;
1369  break;
1370  }
1371  if (!marked_[l.Index()]) {
1372  ++extra_size;
1373  if (!score_only) resolvant_.push_back(l);
1374  }
1375  }
1376  if (trivial) {
1377  if (!score_only) resolvant_.resize(resolvant_.size() - extra_size);
1378  continue;
1379  }
1380 
1381  // If this is the case, the other clause is subsumed by the resolvant.
1382  // We can just remove not_lit from it and ignore it.
1383  if (score_only && clause.size() + extra_size <= other.size()) {
1384  CHECK_EQ(clause.size() + extra_size, other.size());
1385  ++num_simplifications_;
1386 
1387  // Note that we update the threshold since this clause was counted in
1388  // it.
1389  score_threshold_ -= clause_weight + other.size();
1390 
1391  if (extra_size == 0) {
1392  // We have a double self-subsumption. We can just remove this
1393  // clause since it will be subsumed by the clause created in the
1394  // "clause_can_be_simplified" case below.
1395  DeleteClause(clauses_[other_index]);
1396  } else {
1397  if (!RemoveLiteralFromClause(lit.Negated(),
1398  clauses_[other_index])) {
1399  return false;
1400  }
1401  std::swap(clause_containing_not_lit[j],
1402  clause_containing_not_lit.back());
1403  clause_containing_not_lit.pop_back();
1404  --j; // Reprocess the new position.
1405  continue;
1406  }
1407  }
1408 
1409  if (extra_size == 0) {
1410  clause_can_be_simplified = true;
1411  break;
1412  } else {
1413  if (score_only) {
1414  // Hack. We do not want to create long clauses during BVE.
1415  if (clause.size() - 1 + extra_size > 100) {
1416  new_score_ = score_threshold_ + 1;
1417  break;
1418  }
1419 
1420  new_score_ += clause_weight + clause.size() - 1 + extra_size;
1421  } else {
1422  AddClause(resolvant_);
1423  resolvant_.resize(resolvant_.size() - extra_size);
1424  }
1425  }
1426  }
1427  }
1428 
1429  // Note that we need to clear marked before aborting.
1430  for (const Literal l : clause) marked_[l.Index()] = false;
1431 
1432  // In this case, we simplify and remove the clause from here.
1433  if (clause_can_be_simplified) {
1434  ++num_simplifications_;
1435 
1436  // Note that we update the threshold as if this was simplified before.
1437  new_score_ = saved_score;
1438  score_threshold_ -= clause_weight + clause.size();
1439 
1440  if (!RemoveLiteralFromClause(lit, clauses_[clause_index])) return false;
1441  std::swap(clause_containing_lit[i], clause_containing_lit.back());
1442  clause_containing_lit.pop_back();
1443  --i; // Reprocess the new position.
1444  }
1445 
1446  if (score_only && new_score_ > score_threshold_) return true;
1447 
1448  // When this happen, then the clause is blocked (i.e. all its resolvant are
1449  // trivial). So even if we do not actually perform the variable elimination,
1450  // we can still remove this clause. Note that we treat the score as if the
1451  // clause was removed before.
1452  //
1453  // Tricky: The detection only work if we didn't abort the computation above,
1454  // so we do that after the score_threshold_ check.
1455  //
1456  // TODO(user): Also detect blocked clause for not(lit)? It is not as cheap
1457  // though and require more code.
1458  if (score_only && !with_binary_only && !clause_can_be_simplified &&
1459  new_score_ == saved_score) {
1460  ++num_blocked_clauses_;
1461  score_threshold_ -= clause_weight + clause.size();
1462  postsolve_->AddClauseWithSpecialLiteral(lit, clause);
1463  DeleteClause(clauses_[clause_index]);
1464  }
1465  }
1466  return true;
1467 }
1468 
1469 bool BoundedVariableElimination::CrossProduct(BooleanVariable var) {
1470  if (assignment_.VariableIsAssigned(var)) return true;
1471 
1472  const Literal lit(var, true);
1473  const Literal not_lit(var, false);
1474  {
1475  const int s1 = NumClausesContaining(lit);
1476  const int s2 = NumClausesContaining(not_lit);
1477  if (s1 == 0 && s2 == 0) return true;
1478  if (s1 > 0 && s2 == 0) {
1479  num_eliminated_variables_++;
1480  if (!clause_manager_->InprocessingFixLiteral(lit)) return false;
1481  DeleteAllClausesContaining(lit);
1482  return true;
1483  }
1484  if (s1 == 0 && s2 > 0) {
1485  num_eliminated_variables_++;
1486  if (!clause_manager_->InprocessingFixLiteral(not_lit)) return false;
1487  DeleteAllClausesContaining(not_lit);
1488  return true;
1489  }
1490  if (implication_graph_->IsRedundant(lit)) {
1491  // TODO(user): do that elsewhere?
1492  CHECK_EQ(s1, 1);
1493  CHECK_EQ(s2, 1);
1494  CHECK_EQ(implication_graph_->NumImplicationOnVariableRemoval(var), 0);
1495  num_eliminated_variables_++;
1496  implication_graph_->RemoveBooleanVariable(var, &postsolve_->clauses);
1497  return true;
1498  }
1499 
1500  // Heuristic. Abort if the work required to decide if var should be removed
1501  // seems to big.
1502  if (s1 > 1 && s2 > 1 && s1 * s2 > parameters_.presolve_bve_threshold()) {
1503  return true;
1504  }
1505  }
1506 
1507  // TODO(user): swap lit and not_lit for speed? it is unclear if we prefer
1508  // to minimize the number of clause containing lit or not_lit though. Also,
1509  // we might want to alternate since we also detect blocked clause containing
1510  // lit, but don't do it for not_lit.
1511 
1512  // Compute the current score.
1513  // TODO(user): cleanup the list lazily at the same time?
1514  int64 score = 0;
1515  const int clause_weight = parameters_.presolve_bve_clause_weight();
1516  score +=
1517  implication_graph_->DirectImplications(lit).size() * (clause_weight + 2);
1518  score += implication_graph_->DirectImplications(not_lit).size() *
1519  (clause_weight + 2);
1520  for (const ClauseIndex i : literal_to_clauses_[lit.Index()]) {
1521  const auto c = clauses_[i]->AsSpan();
1522  if (!c.empty()) score += clause_weight + c.size();
1523  }
1524  for (const ClauseIndex i : literal_to_clauses_[not_lit.Index()]) {
1525  const auto c = clauses_[i]->AsSpan();
1526  if (!c.empty()) score += clause_weight + c.size();
1527  }
1528 
1529  // Compute the new score after BVE.
1530  // Abort as soon as it crosses the threshold.
1531  //
1532  // TODO(user): Experiment with leaving the implications graph as is. This will
1533  // not remove the variable completely, but it seems interesting since after
1534  // equivalent variable removal and failed literal probing, the cross product
1535  // of the implication always add a quadratic number of implication, except if
1536  // the in (or out) degree is zero or one.
1537  score_threshold_ = score;
1538  new_score_ = implication_graph_->NumImplicationOnVariableRemoval(var) *
1539  (clause_weight + 2);
1540  if (new_score_ > score_threshold_) return true;
1541  if (!ResolveAllClauseContaining</*score_only=*/true,
1542  /*with_binary_only=*/true>(not_lit)) {
1543  return false;
1544  }
1545  if (new_score_ > score_threshold_) return true;
1546  if (!ResolveAllClauseContaining</*score_only=*/true,
1547  /*with_binary_only=*/false>(lit)) {
1548  return false;
1549  }
1550  if (new_score_ > score_threshold_) return true;
1551 
1552  // Perform BVE.
1553  if (new_score_ > 0) {
1554  if (!ResolveAllClauseContaining</*score_only=*/false,
1555  /*with_binary_only=*/false>(lit)) {
1556  return false;
1557  }
1558  if (!ResolveAllClauseContaining</*score_only=*/false,
1559  /*with_binary_only=*/true>(not_lit)) {
1560  return false;
1561  }
1562  }
1563 
1564  ++num_eliminated_variables_;
1565  implication_graph_->RemoveBooleanVariable(var, &postsolve_->clauses);
1566  DeleteAllClausesContaining(lit);
1567  DeleteAllClausesContaining(not_lit);
1568  return true;
1569 }
1570 
1571 } // namespace sat
1572 } // namespace operations_research
#define LOG_IF(severity, condition)
Definition: base/logging.h:479
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
void Start()
Definition: timer.h:31
double Get() const
Definition: timer.h:45
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
size_type size() const
void push_back(const value_type &x)
void Set(IntegerType index)
Definition: bitset.h:803
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
Definition: time_limit.h:532
double GetElapsedDeterministicTime() const
Returns the elapsed deterministic time since the construction of this object.
Definition: time_limit.h:260
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
Definition: time_limit.h:226
bool ComputeTransitiveReduction(bool log_info=false)
Definition: clause.cc:1311
Literal RepresentativeOf(Literal l) const
Definition: clause.h:561
const std::vector< Literal > & DirectImplications(Literal literal)
Definition: clause.cc:1799
bool DetectEquivalences(bool log_info=false)
Definition: clause.cc:1124
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
int DirectImplicationsEstimatedSize(Literal literal) const
Definition: clause.h:693
bool PresolveLoop(SatPresolveOptions options)
bool RemoveFixedAndEquivalentVariables(bool log_info)
bool DetectEquivalencesAndStamp(bool use_transitive_reduction, bool log_info)
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
LiteralIndex Index() const
Definition: sat_base.h:84
const std::vector< SatClause * > & AllClausesInCreationOrder() const
Definition: clause.h:211
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)
Definition: clause.cc:339
void InprocessingRemoveClause(SatClause *clause)
Definition: clause.cc:358
SatClause * InprocessingAddClause(absl::Span< const Literal > new_clause)
Definition: clause.cc:415
bool IsRemovable(SatClause *const clause) const
Definition: clause.h:219
ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(SatClause *clause, absl::Span< const Literal > new_clause)
Definition: clause.cc:367
absl::Span< const Literal > AsSpan() const
Definition: clause.h:90
void MaybeEnablePhaseSaving(bool save_phase)
Definition: sat_decision.h:85
void MinimizeSomeClauses(int decisions_budget)
Definition: sat_solver.cc:1247
bool ImplicationIsInTree(Literal a, Literal b) const
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
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
static const int32 kint32max
uint64_t uint64
const int INFO
Definition: log_severity.h:31
const bool DEBUG_MODE
Definition: macros.h:24
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
const LiteralIndex kNoLiteralIndex(-1)
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
Definition: probing.cc:350
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
#define RETURN_IF_FALSE(f)
std::deque< std::vector< Literal > > clauses
void AddClauseWithSpecialLiteral(Literal literal, absl::Span< const Literal > clause)
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41