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"
19#include "ortools/base/timer.h"
20#include "ortools/sat/probing.h"
22
23namespace operations_research {
24namespace 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
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
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.
228bool 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.
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.
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
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
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
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
917void 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
952void 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.
1043bool 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
1194bool 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
1222bool 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.
1246int 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.
1252void 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
1263void 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
1282void 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
1292void 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
1311template <bool score_only, bool with_binary_only>
1312bool 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
1469bool 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
void RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
Definition: clause.cc:1887
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
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
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
const std::vector< SatClause * > & AllClausesInCreationOrder() const
Definition: clause.h:211
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