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