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