OR-Tools  8.2
clause.h
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
14// This file contains the solver internal representation of the clauses and the
15// classes used for their propagation.
16
17#ifndef OR_TOOLS_SAT_CLAUSE_H_
18#define OR_TOOLS_SAT_CLAUSE_H_
19
20#include <deque>
21#include <string>
22#include <utility>
23#include <vector>
24
25#include "absl/container/flat_hash_map.h"
26#include "absl/container/flat_hash_set.h"
27#include "absl/container/inlined_vector.h"
28#include "absl/random/bit_gen_ref.h"
29#include "absl/types/span.h"
30#include "ortools/base/hash.h"
33#include "ortools/base/macros.h"
36#include "ortools/sat/model.h"
38#include "ortools/sat/sat_parameters.pb.h"
39#include "ortools/sat/util.h"
40#include "ortools/util/bitset.h"
41#include "ortools/util/stats.h"
43
44namespace operations_research {
45namespace sat {
46
47// This is how the SatSolver stores a clause. A clause is just a disjunction of
48// literals. In many places, we just use vector<literal> to encode one. But in
49// the critical propagation code, we use this class to remove one memory
50// indirection.
51class SatClause {
52 public:
53 // Creates a sat clause. There must be at least 2 literals. Smaller clause are
54 // treated separatly and never constructed. In practice, we do use
55 // BinaryImplicationGraph for the clause of size 2, so this is mainly used for
56 // size at least 3.
57 static SatClause* Create(absl::Span<const Literal> literals);
58
59 // Non-sized delete because this is a tail-padded class.
60 void operator delete(void* p) {
61 ::operator delete(p); // non-sized delete
62 }
63
64 // Number of literals in the clause.
65 int size() const { return size_; }
66 int empty() const { return size_ == 0; }
67
68 // Allows for range based iteration: for (Literal literal : clause) {}.
69 const Literal* const begin() const { return &(literals_[0]); }
70 const Literal* const end() const { return &(literals_[size_]); }
71
72 // Returns the first and second literals. These are always the watched
73 // literals if the clause is attached in the LiteralWatchers.
74 Literal FirstLiteral() const { return literals_[0]; }
75 Literal SecondLiteral() const { return literals_[1]; }
76
77 // Returns the literal that was propagated to true. This only works for a
78 // clause that just propagated this literal. Otherwise, this will just returns
79 // a literal of the clause.
80 Literal PropagatedLiteral() const { return literals_[0]; }
81
82 // Returns the reason for the last unit propagation of this clause. The
83 // preconditions are the same as for PropagatedLiteral(). Note that we don't
84 // need to include the propagated literal.
85 absl::Span<const Literal> PropagationReason() const {
86 return absl::Span<const Literal>(&(literals_[1]), size_ - 1);
87 }
88
89 // Returns a Span<> representation of the clause.
90 absl::Span<const Literal> AsSpan() const {
91 return absl::Span<const Literal>(&(literals_[0]), size_);
92 }
93
94 // Removes literals that are fixed. This should only be called at level 0
95 // where a literal is fixed iff it is assigned. Aborts and returns true if
96 // they are not all false.
97 //
98 // Note that the removed literal can still be accessed in the portion [size,
99 // old_size) of literals().
101
102 // Returns true if the clause is satisfied for the given assignment. Note that
103 // the assignment may be partial, so false does not mean that the clause can't
104 // be satisfied by completing the assignment.
105 bool IsSatisfied(const VariablesAssignment& assignment) const;
106
107 // Returns true if the clause is attached to a LiteralWatchers.
108 bool IsAttached() const { return size_ > 0; }
109
110 std::string DebugString() const;
111
112 private:
113 // LiteralWatchers needs to permute the order of literals in the clause and
114 // call Clear()/Rewrite.
115 friend class LiteralWatchers;
116
117 Literal* literals() { return &(literals_[0]); }
118
119 // Marks the clause so that the next call to CleanUpWatchers() can identify it
120 // and actually detach it. We use size_ = 0 for this since the clause will
121 // never be used afterwards.
122 void Clear() { size_ = 0; }
123
124 // Rewrites a clause with another shorter one. Note that the clause shouldn't
125 // be attached when this is called.
126 void Rewrite(absl::Span<const Literal> new_clause) {
127 size_ = 0;
128 for (const Literal l : new_clause) literals_[size_++] = l;
129 }
130
131 int32 size_;
132
133 // This class store the literals inline, and literals_ mark the starts of the
134 // variable length portion.
135 Literal literals_[0];
136
137 DISALLOW_COPY_AND_ASSIGN(SatClause);
138};
139
140// Clause information used for the clause database management. Note that only
141// the clauses that can be removed have an info. The problem clauses and
142// the learned one that we wants to keep forever do not have one.
144 double activity = 0.0;
147};
148
150
151// Stores the 2-watched literals data structure. See
152// http://www.cs.berkeley.edu/~necula/autded/lecture24-sat.pdf for
153// detail.
154//
155// This class is also responsible for owning the clause memory and all related
156// information.
157//
158// TODO(user): Rename ClauseManager. This does more than just watching the
159// clauses and is the place where all the clauses are stored.
161 public:
162 explicit LiteralWatchers(Model* model);
163 ~LiteralWatchers() override;
164
165 // Must be called before adding clauses refering to such variables.
166 void Resize(int num_variables);
167
168 // SatPropagator API.
169 bool Propagate(Trail* trail) final;
170 absl::Span<const Literal> Reason(const Trail& trail,
171 int trail_index) const final;
172
173 // Returns the reason of the variable at given trail_index. This only works
174 // for variable propagated by this class and is almost the same as Reason()
175 // with a different return format.
176 SatClause* ReasonClause(int trail_index) const;
177
178 // Adds a new clause and perform initial propagation for this clause only.
179 bool AddClause(absl::Span<const Literal> literals, Trail* trail);
180 bool AddClause(absl::Span<const Literal> literals);
181
182 // Same as AddClause() for a removable clause. This is only called on learned
183 // conflict, so this should never have all its literal at false (CHECKED).
184 SatClause* AddRemovableClause(const std::vector<Literal>& literals,
185 Trail* trail);
186
187 // Lazily detach the given clause. The deletion will actually occur when
188 // CleanUpWatchers() is called. The later needs to be called before any other
189 // function in this class can be called. This is DCHECKed.
190 //
191 // Note that we remove the clause from clauses_info_ right away.
192 void LazyDetach(SatClause* clause);
193 void CleanUpWatchers();
194
195 // Detaches the given clause right away.
196 //
197 // TODO(user): It might be better to have a "slower" mode in
198 // PropagateOnFalse() that deal with detached clauses in the watcher list and
199 // is activated until the next CleanUpWatchers() calls.
200 void Detach(SatClause* clause);
201
202 // Attaches the given clause. The first two literal of the clause must
203 // be unassigned and the clause must not be already attached.
204 void Attach(SatClause* clause, Trail* trail);
205
206 // Reclaims the memory of the lazily removed clauses (their size was set to
207 // zero) and remove them from AllClausesInCreationOrder() this work in
208 // O(num_clauses()).
210 int64 num_clauses() const { return clauses_.size(); }
211 const std::vector<SatClause*>& AllClausesInCreationOrder() const {
212 return clauses_;
213 }
214
215 // True if removing this clause will not change the set of feasible solution.
216 // This is the case for clauses that were learned during search. Note however
217 // that some learned clause are kept forever (heuristics) and do not appear
218 // here.
219 bool IsRemovable(SatClause* const clause) const {
220 return gtl::ContainsKey(clauses_info_, clause);
221 }
222 int64 num_removable_clauses() const { return clauses_info_.size(); }
223 absl::flat_hash_map<SatClause*, ClauseInfo>* mutable_clauses_info() {
224 return &clauses_info_;
225 }
226
227 // Total number of clauses inspected during calls to PropagateOnFalse().
228 int64 num_inspected_clauses() const { return num_inspected_clauses_; }
230 return num_inspected_clause_literals_;
231 }
232
233 // The number of different literals (always twice the number of variables).
234 int64 literal_size() const { return needs_cleaning_.size().value(); }
235
236 // Number of clauses currently watched.
237 int64 num_watched_clauses() const { return num_watched_clauses_; }
238
239 void SetDratProofHandler(DratProofHandler* drat_proof_handler) {
240 drat_proof_handler_ = drat_proof_handler;
241 }
242
243 // Really basic algorithm to return a clause to try to minimize. We simply
244 // loop over the clause that we keep forever, in creation order. This starts
245 // by the problem clauses and then the learned one that we keep forever.
247 for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
248 if (!clauses_[to_minimize_index_]->IsAttached()) continue;
249 if (!IsRemovable(clauses_[to_minimize_index_])) {
250 return clauses_[to_minimize_index_++];
251 }
252 }
253 return nullptr;
254 }
255
256 // Restart the scan in NextClauseToMinimize() from the first problem clause.
257 void ResetToMinimizeIndex() { to_minimize_index_ = 0; }
258
259 // During an inprocessing phase, it is easier to detach all clause first,
260 // then simplify and then reattach them. Note however that during these
261 // two calls, it is not possible to use the solver unit-progation.
262 //
263 // Important: When reattach is called, we assume that none of their literal
264 // are fixed, so we don't do any special checks.
265 //
266 // These functions can be called multiple-time and do the right things. This
267 // way before doing something, you can call the corresponding function and be
268 // sure to be in a good state. I.e. always AttachAllClauses() before
269 // propagation and DetachAllClauses() before going to do an inprocessing pass
270 // that might transform them.
271 void DetachAllClauses();
272 void AttachAllClauses();
273
274 // These must only be called between [Detach/Attach]AllClauses() calls.
276 ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal);
277 ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(
278 SatClause* clause, absl::Span<const Literal> new_clause);
279
280 // This can return nullptr if new_clause was of size one or two as these are
281 // treated differently. Note that none of the variable should be fixed in the
282 // given new clause.
283 SatClause* InprocessingAddClause(absl::Span<const Literal> new_clause);
284
285 // Contains, for each literal, the list of clauses that need to be inspected
286 // when the corresponding literal becomes false.
287 struct Watcher {
289 Watcher(SatClause* c, Literal b, int i = 2)
291
292 // Optimization. A literal from the clause that sometimes allow to not even
293 // look at the clause memory when true.
295
296 // Optimization. An index in the clause. Instead of looking for another
297 // literal to watch from the start, we will start from here instead, and
298 // loop around if needed. This allows to avoid bad quadratric corner cases
299 // and lead to an "optimal" complexity. See "Optimal Implementation of
300 // Watched Literals and more General Techniques", Ian P. Gent.
301 //
302 // Note that ideally, this should be part of a SatClause, so it can be
303 // shared across watchers. However, since we have 32 bits for "free" here
304 // because of the struct alignment, we store it here instead.
306
308 };
309
310 // This is exposed since some inprocessing code can heuristically exploit the
311 // currently watched literal and blocking literal to do some simplification.
312 const std::vector<Watcher>& WatcherListOnFalse(Literal false_literal) const {
313 return watchers_on_false_[false_literal.Index()];
314 }
315
316 private:
317 // Attaches the given clause. This eventually propagates a literal which is
318 // enqueued on the trail. Returns false if a contradiction was encountered.
319 bool AttachAndPropagate(SatClause* clause, Trail* trail);
320
321 // Launches all propagation when the given literal becomes false.
322 // Returns false if a contradiction was encountered.
323 bool PropagateOnFalse(Literal false_literal, Trail* trail);
324
325 // Attaches the given clause to the event: the given literal becomes false.
326 // The blocking_literal can be any literal from the clause, it is used to
327 // speed up PropagateOnFalse() by skipping the clause if it is true.
328 void AttachOnFalse(Literal literal, Literal blocking_literal,
329 SatClause* clause);
330
331 // Common code between LazyDetach() and Detach().
332 void InternalDetach(SatClause* clause);
333
335
336 // SatClause reasons by trail_index.
337 std::vector<SatClause*> reasons_;
338
339 // Indicates if the corresponding watchers_on_false_ list need to be
340 // cleaned. The boolean is_clean_ is just used in DCHECKs.
341 SparseBitset<LiteralIndex> needs_cleaning_;
342 bool is_clean_ = true;
343
344 BinaryImplicationGraph* implication_graph_;
345 Trail* trail_;
346
347 int64 num_inspected_clauses_;
348 int64 num_inspected_clause_literals_;
349 int64 num_watched_clauses_;
350 mutable StatsGroup stats_;
351
352 // For DetachAllClauses()/AttachAllClauses().
353 bool all_clauses_are_attached_ = true;
354
355 // All the clauses currently in memory. This vector has ownership of the
356 // pointers. We currently do not use std::unique_ptr<SatClause> because it
357 // can't be used with some STL algorithms like std::partition.
358 //
359 // Note that the unit clauses are not kept here and if the parameter
360 // treat_binary_clauses_separately is true, the binary clause are not kept
361 // here either.
362 std::vector<SatClause*> clauses_;
363
364 int to_minimize_index_ = 0;
365
366 // Only contains removable clause.
367 absl::flat_hash_map<SatClause*, ClauseInfo> clauses_info_;
368
369 DratProofHandler* drat_proof_handler_ = nullptr;
370
371 DISALLOW_COPY_AND_ASSIGN(LiteralWatchers);
372};
373
374// A binary clause. This is used by BinaryClauseManager.
376 BinaryClause(Literal _a, Literal _b) : a(_a), b(_b) {}
377 bool operator==(BinaryClause o) const { return a == o.a && b == o.b; }
378 bool operator!=(BinaryClause o) const { return a != o.a || b != o.b; }
381};
382
383// A simple class to manage a set of binary clauses.
385 public:
387 int NumClauses() const { return set_.size(); }
388
389 // Adds a new binary clause to the manager and returns true if it wasn't
390 // already present.
392 std::pair<int, int> p(c.a.SignedValue(), c.b.SignedValue());
393 if (p.first > p.second) std::swap(p.first, p.second);
394 if (set_.find(p) == set_.end()) {
395 set_.insert(p);
396 newly_added_.push_back(c);
397 return true;
398 }
399 return false;
400 }
401
402 // Returns the newly added BinaryClause since the last ClearNewlyAdded() call.
403 const std::vector<BinaryClause>& newly_added() const { return newly_added_; }
404 void ClearNewlyAdded() { newly_added_.clear(); }
405
406 private:
407 absl::flat_hash_set<std::pair<int, int>> set_;
408 std::vector<BinaryClause> newly_added_;
409 DISALLOW_COPY_AND_ASSIGN(BinaryClauseManager);
410};
411
412// Special class to store and propagate clauses of size 2 (i.e. implication).
413// Such clauses are never deleted. Together, they represent the 2-SAT part of
414// the problem. Note that 2-SAT satisfiability is a polynomial problem, but
415// W2SAT (weighted 2-SAT) is NP-complete.
416//
417// TODO(user): Most of the note below are done, but we currently only applies
418// the reduction before the solve. We should consider doing more in-processing.
419// The code could probably still be improved too.
420//
421// Note(user): All the variables in a strongly connected component are
422// equivalent and can be thus merged as one. This is relatively cheap to compute
423// from time to time (linear complexity). We will also get contradiction (a <=>
424// not a) this way. This is done by DetectEquivalences().
425//
426// Note(user): An implication (a => not a) implies that a is false. I am not
427// sure it is worth detecting that because if the solver assign a to true, it
428// will learn that right away. I don't think we can do it faster.
429//
430// Note(user): The implication graph can be pruned. This is called the
431// transitive reduction of a graph. For instance If a => {b,c} and b => {c},
432// then there is no need to store a => {c}. The transitive reduction is unique
433// on an acyclic graph. Computing it will allow for a faster propagation and
434// memory reduction. It is however not cheap. Maybe simple lazy heuristics to
435// remove redundant arcs are better. Note that all the learned clauses we add
436// will never be redundant (but they could introduce cycles). This is done
437// by ComputeTransitiveReduction().
438//
439// Note(user): This class natively support at most one constraints. This is
440// a way to reduced significantly the memory and size of some 2-SAT instances.
441// However, it is not fully exploited for pure SAT problems. See
442// TransformIntoMaxCliques().
443//
444// Note(user): Add a preprocessor to remove duplicates in the implication lists.
445// Note that all the learned clauses we add will never create duplicates.
446//
447// References for most of the above and more:
448// - Brafman RI, "A simplifier for propositional formulas with many binary
449// clauses", IEEE Trans Syst Man Cybern B Cybern. 2004 Feb;34(1):52-9.
450// http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.4911
451// - Marijn J. H. Heule, Matti Järvisalo, Armin Biere, "Efficient CNF
452// Simplification Based on Binary Implication Graphs", Theory and Applications
453// of Satisfiability Testing - SAT 2011, Lecture Notes in Computer Science
454// Volume 6695, 2011, pp 201-215
455// http://www.cs.helsinki.fi/u/mjarvisa/papers/heule-jarvisalo-biere.sat11.pdf
457 public:
459 : SatPropagator("BinaryImplicationGraph"),
460 stats_("BinaryImplicationGraph"),
461 time_limit_(model->GetOrCreate<TimeLimit>()),
462 random_(model->GetOrCreate<ModelRandomGenerator>()),
463 trail_(model->GetOrCreate<Trail>()) {
464 trail_->RegisterPropagator(this);
465 }
466
469 LOG(INFO) << stats_.StatString();
470 LOG(INFO) << "num_redundant_implications " << num_redundant_implications_;
471 });
472 }
473
474 // SatPropagator interface.
475 bool Propagate(Trail* trail) final;
476 absl::Span<const Literal> Reason(const Trail& trail,
477 int trail_index) const final;
478
479 // Resizes the data structure.
480 void Resize(int num_variables);
481
482 // Returns true if there is no constraints in this class.
483 bool IsEmpty() { return num_implications_ == 0 && at_most_ones_.empty(); }
484
485 // Adds the binary clause (a OR b), which is the same as (not a => b).
486 // Note that it is also equivalent to (not b => a).
489 return AddBinaryClause(a.Negated(), b);
490 }
491
492 // Same as AddBinaryClause() but enqueues a possible unit propagation. Note
493 // that if the binary clause propagates, it must do so at the last level, this
494 // is DCHECKed.
495 //
496 // Return false and do nothing if both a and b are currently false.
498
499 // An at most one constraint of size n is a compact way to encode n * (n - 1)
500 // implications. This must only be called at level zero.
501 //
502 // Returns false if this creates a conflict. Currently this can only happens
503 // if there is duplicate literal already assigned to true in this constraint.
504 ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span<const Literal> at_most_one);
505
506 // Uses the binary implication graph to minimize the given conflict by
507 // removing literals that implies others. The idea is that if a and b are two
508 // literals from the given conflict and a => b (which is the same as not(b) =>
509 // not(a)) then a is redundant and can be removed.
510 //
511 // Note that removing as many literals as possible is too time consuming, so
512 // we use different heuristics/algorithms to do this minimization.
513 // See the binary_minimization_algorithm SAT parameter and the .cc for more
514 // details about the different algorithms.
515 void MinimizeConflictWithReachability(std::vector<Literal>* c);
516 void MinimizeConflictExperimental(const Trail& trail,
517 std::vector<Literal>* c);
518 void MinimizeConflictFirst(const Trail& trail, std::vector<Literal>* c,
521 const Trail& trail, std::vector<Literal>* c,
522 SparseBitset<BooleanVariable>* marked, absl::BitGenRef random);
523
524 // This must only be called at decision level 0 after all the possible
525 // propagations. It:
526 // - Removes the variable at true from the implications lists.
527 // - Frees the propagation list of the assigned literals.
529
530 // Returns false if the model is unsat, otherwise detects equivalent variable
531 // (with respect to the implications only) and reorganize the propagation
532 // lists accordingly.
533 //
534 // TODO(user): Completely get rid of such literal instead? it might not be
535 // reasonable code-wise to remap our literals in all of our constraints
536 // though.
537 bool DetectEquivalences(bool log_info = false);
538
539 // Returns true if DetectEquivalences() has been called and no new binary
540 // clauses have been added since then. When this is true then there is no
541 // cycle in the binary implication graph (modulo the redundant literals that
542 // form a cycle with their representative).
543 bool IsDag() const { return is_dag_; }
544
545 // One must call DetectEquivalences() first, this is CHECKed.
546 // Returns a list so that if x => y, then x is after y.
547 const std::vector<LiteralIndex>& ReverseTopologicalOrder() const {
548 CHECK(is_dag_);
549 return reverse_topological_order_;
550 }
551
552 // Returns the list of literal "directly" implied by l. Beware that this can
553 // easily change behind your back if you modify the solver state.
554 const absl::InlinedVector<Literal, 6>& Implications(Literal l) const {
555 return implications_[l.Index()];
556 }
557
558 // Returns the representative of the equivalence class of l (or l itself if it
559 // is on its own). Note that DetectEquivalences() should have been called to
560 // get any non-trival results.
562 if (l.Index() >= representative_of_.size()) return l;
563 if (representative_of_[l.Index()] == kNoLiteralIndex) return l;
564 return Literal(representative_of_[l.Index()]);
565 }
566
567 // Prunes the implication graph by calling first DetectEquivalences() to
568 // remove cycle and then by computing the transitive reduction of the
569 // remaining DAG.
570 //
571 // Note that this can be slow (num_literals graph traversals), so we abort
572 // early if we start doing too much work.
573 //
574 // Returns false if the model is detected to be UNSAT (this needs to call
575 // DetectEquivalences() if not already done).
576 bool ComputeTransitiveReduction(bool log_info = false);
577
578 // Another way of representing an implication graph is a list of maximal "at
579 // most one" constraints, each forming a max-clique in the incompatibility
580 // graph. This representation is useful for having a good linear relaxation.
581 //
582 // This function will transform each of the given constraint into a maximal
583 // one in the underlying implication graph. Constraints that are redundant
584 // after other have been expanded (i.e. included into) will be cleared.
585 //
586 // Returns false if the model is detected to be UNSAT (this needs to call
587 // DetectEquivalences() if not already done).
588 bool TransformIntoMaxCliques(std::vector<std::vector<Literal>>* at_most_ones,
589 int64 max_num_explored_nodes = 1e8);
590
591 // LP clique cut heuristic. Returns a set of "at most one" constraints on the
592 // given literals or their negation that are violated by the current LP
593 // solution. Note that this assumes that
594 // lp_value(lit) = 1 - lp_value(lit.Negated()).
595 //
596 // The literal and lp_values vector are in one to one correspondence. We will
597 // only generate clique with these literals or their negation.
598 //
599 // TODO(user): Refine the heuristic and unit test!
600 const std::vector<std::vector<Literal>>& GenerateAtMostOnesWithLargeWeight(
601 const std::vector<Literal>& literals,
602 const std::vector<double>& lp_values);
603
604 // Number of literal propagated by this class (including conflicts).
605 int64 num_propagations() const { return num_propagations_; }
606
607 // Number of literals inspected by this class during propagation.
608 int64 num_inspections() const { return num_inspections_; }
609
610 // MinimizeClause() stats.
611 int64 num_minimization() const { return num_minimization_; }
612 int64 num_literals_removed() const { return num_literals_removed_; }
613
614 // Returns true if this literal is fixed or is equivalent to another literal.
615 // This means that it can just be ignored in most situation.
616 //
617 // Note that the set (and thus number) of redundant literal can only grow over
618 // time. This is because we always use the lowest index as representative of
619 // an equivalent class, so a redundant literal will stay that way.
620 bool IsRedundant(Literal l) const { return is_redundant_[l.Index()]; }
622 CHECK_EQ(num_redundant_literals_ % 2, 0);
623 return num_redundant_literals_;
624 }
625
626 // Number of implications removed by transitive reduction.
628 return num_redundant_implications_;
629 }
630
631 // Returns the number of current implications. Note that a => b and not(b) =>
632 // not(a) are counted separately since they appear separately in our
633 // propagation lists. The number of size 2 clauses that represent the same
634 // thing is half this number.
635 int64 num_implications() const { return num_implications_; }
636 int64 literal_size() const { return implications_.size(); }
637
638 // Extract all the binary clauses managed by this class. The Output type must
639 // support an AddBinaryClause(Literal a, Literal b) function.
640 //
641 // Important: This currently does NOT include at most one constraints.
642 //
643 // TODO(user): When extracting to cp_model.proto we could be more efficient
644 // by extracting bool_and constraint with many lhs terms.
645 template <typename Output>
646 void ExtractAllBinaryClauses(Output* out) const {
647 // TODO(user): Ideally we should just never have duplicate clauses in this
648 // class. But it seems we do in some corner cases, so lets not output them
649 // twice.
650 absl::flat_hash_set<std::pair<LiteralIndex, LiteralIndex>>
651 duplicate_detection;
652 for (LiteralIndex i(0); i < implications_.size(); ++i) {
653 const Literal a = Literal(i).Negated();
654 for (const Literal b : implications_[i]) {
655 // Note(user): We almost always have both a => b and not(b) => not(a) in
656 // our implications_ database. Except if ComputeTransitiveReduction()
657 // was aborted early, but in this case, if only one is present, the
658 // other could be removed, so we shouldn't need to output it.
659 if (a < b &&
660 duplicate_detection.insert({a.Index(), b.Index()}).second) {
661 out->AddBinaryClause(a, b);
662 }
663 }
664 }
665 }
666
667 void SetDratProofHandler(DratProofHandler* drat_proof_handler) {
668 drat_proof_handler_ = drat_proof_handler;
669 }
670
671 // Changes the reason of the variable at trail index to a binary reason.
672 // Note that the implication "new_reason => trail_[trail_index]" should be
673 // part of the implication graph.
674 void ChangeReason(int trail_index, Literal new_reason) {
675 CHECK(trail_->Assignment().LiteralIsTrue(new_reason));
676 reasons_[trail_index] = new_reason.Negated();
677 trail_->ChangeReason(trail_index, propagator_id_);
678 }
679
680 // The literals that are "directly" implied when literal is set to true. This
681 // is not a full "reachability". It includes at most ones propagation. The set
682 // of all direct implications is enough to describe the implications graph
683 // completely.
684 //
685 // When doing blocked clause elimination of bounded variable elimination, one
686 // only need to consider this list and not the full reachability.
687 const std::vector<Literal>& DirectImplications(Literal literal);
688
689 // A proxy for DirectImplications().size(), However we currently do not
690 // maintain it perfectly. It is exact each time DirectImplications() is
691 // called, and we update it in some situation but we don't deal with fixed
692 // variables, at_most ones and duplicates implications for now.
694 return estimated_sizes_[literal.Index()];
695 }
696
697 // Variable elimination by replacing everything of the form a => var => b by a
698 // => b. We ignore any a => a so the number of new implications is not always
699 // just the product of the two direct implication list of var and not(var).
700 // However, if a => var => a, then a and var are equivalent, so this case will
701 // be removed if one run DetectEquivalences() before this. Similarly, if a =>
702 // var => not(a) then a must be false and this is detected and dealt with by
703 // FindFailedLiteralAroundVar().
704 bool FindFailedLiteralAroundVar(BooleanVariable var, bool* is_unsat);
707 BooleanVariable var, std::deque<std::vector<Literal>>* postsolve_clauses);
708 bool IsRemoved(Literal l) const { return is_removed_[l.Index()]; }
709
710 // TODO(user): consider at most ones.
712
713 private:
714 // Simple wrapper to not forget to output newly fixed variable to the DRAT
715 // proof if needed. This will propagate rigth away the implications.
716 bool FixLiteral(Literal true_literal);
717
718 // Propagates all the direct implications of the given literal becoming true.
719 // Returns false if a conflict was encountered, in which case
720 // trail->SetFailingClause() will be called with the correct size 2 clause.
721 // This calls trail->Enqueue() on the newly assigned literals.
722 bool PropagateOnTrue(Literal true_literal, Trail* trail);
723
724 // Remove any literal whose negation is marked (except the first one).
725 void RemoveRedundantLiterals(std::vector<Literal>* conflict);
726
727 // Fill is_marked_ with all the descendant of root.
728 // Note that this also use dfs_stack_.
729 void MarkDescendants(Literal root);
730
731 // Expands greedily the given at most one until we get a maximum clique in
732 // the underlying incompatibility graph. Note that there is no guarantee that
733 // if this is called with any sub-clique of the result we will get the same
734 // maximal clique.
735 std::vector<Literal> ExpandAtMostOne(
736 const absl::Span<const Literal> at_most_one);
737
738 // Same as ExpandAtMostOne() but try to maximize the weight in the clique.
739 std::vector<Literal> ExpandAtMostOneWithWeight(
740 const absl::Span<const Literal> at_most_one,
741 const absl::StrongVector<LiteralIndex, bool>& can_be_included,
742 const absl::StrongVector<LiteralIndex, double>& expanded_lp_values);
743
744 // Process all at most one constraints starting at or after base_index in
745 // at_most_one_buffer_. This replace literal by their representative, remove
746 // fixed literals and deal with duplicates. Return false iff the model is
747 // UNSAT.
748 bool CleanUpAndAddAtMostOnes(const int base_index);
749
750 mutable StatsGroup stats_;
751 TimeLimit* time_limit_;
752 ModelRandomGenerator* random_;
753 Trail* trail_;
754 DratProofHandler* drat_proof_handler_ = nullptr;
755
756 // Binary reasons by trail_index. We need a deque because we kept pointers to
757 // elements of this array and this can dynamically change size.
758 std::deque<Literal> reasons_;
759
760 // This is indexed by the Index() of a literal. Each list stores the
761 // literals that are implied if the index literal becomes true.
762 //
763 // Using InlinedVector helps quite a bit because on many problems, a literal
764 // only implies a few others. Note that on a 64 bits computer we get exactly
765 // 6 inlined int32 elements without extra space, and the size of the inlined
766 // vector is 4 times 64 bits.
767 //
768 // TODO(user): We could be even more efficient since a size of int32 is enough
769 // for us and we could store in common the inlined/not-inlined size.
771 implications_;
772 int64 num_implications_ = 0;
773
774 // Internal representation of at_most_one constraints. Each entry point to the
775 // start of a constraint in the buffer. Contraints are terminated by
776 // kNoLiteral. When LiteralIndex is true, then all entry in the at most one
777 // constraint must be false except the one refering to LiteralIndex.
778 //
779 // TODO(user): We could be more cache efficient by combining this with
780 // implications_ in some way. Do some propagation speed benchmark.
782 std::vector<Literal> at_most_one_buffer_;
783
784 // Used by GenerateAtMostOnesWithLargeWeight().
785 std::vector<std::vector<Literal>> tmp_cuts_;
786
787 // Some stats.
788 int64 num_propagations_ = 0;
789 int64 num_inspections_ = 0;
790 int64 num_minimization_ = 0;
791 int64 num_literals_removed_ = 0;
792 int64 num_redundant_implications_ = 0;
793 int64 num_redundant_literals_ = 0;
794
795 // Bitset used by MinimizeClause().
796 // TODO(user): use the same one as the one used in the classic minimization
797 // because they are already initialized. Moreover they contains more
798 // information.
800 SparseBitset<LiteralIndex> is_simplified_;
801
802 // Temporary stack used by MinimizeClauseWithReachability().
803 std::vector<Literal> dfs_stack_;
804
805 // Used to limit the work done by ComputeTransitiveReduction() and
806 // TransformIntoMaxCliques().
807 int64 work_done_in_mark_descendants_ = 0;
808
809 // Filled by DetectEquivalences().
810 bool is_dag_ = false;
811 std::vector<LiteralIndex> reverse_topological_order_;
814
815 // For in-processing and removing variables.
816 std::vector<Literal> direct_implications_;
817 std::vector<Literal> direct_implications_of_negated_literal_;
818 absl::StrongVector<LiteralIndex, bool> in_direct_implications_;
821
822 // For RemoveFixedVariables().
823 int num_processed_fixed_variables_ = 0;
824
825 DISALLOW_COPY_AND_ASSIGN(BinaryImplicationGraph);
826};
827
828} // namespace sat
829} // namespace operations_research
830
831#endif // OR_TOOLS_SAT_CLAUSE_H_
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define LOG(severity)
Definition: base/logging.h:420
size_type size() const
bool empty() const
IntegerType size() const
Definition: bitset.h:769
std::string StatString() const
Definition: stats.cc:71
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
const std::vector< BinaryClause > & newly_added() const
Definition: clause.h:403
void AddBinaryClause(Literal a, Literal b)
Definition: clause.cc:491
bool ComputeTransitiveReduction(bool log_info=false)
Definition: clause.cc:1311
void MinimizeConflictWithReachability(std::vector< Literal > *c)
Definition: clause.cc:754
const std::vector< LiteralIndex > & ReverseTopologicalOrder() const
Definition: clause.h:547
void ChangeReason(int trail_index, Literal new_reason)
Definition: clause.h:674
bool AddBinaryClauseDuringSearch(Literal a, Literal b)
Definition: clause.cc:508
const std::vector< std::vector< Literal > > & GenerateAtMostOnesWithLargeWeight(const std::vector< Literal > &literals, const std::vector< double > &lp_values)
Definition: clause.cc:1645
void ExtractAllBinaryClauses(Output *out) const
Definition: clause.h:646
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: clause.cc:742
const absl::InlinedVector< Literal, 6 > & Implications(Literal l) const
Definition: clause.h:554
bool TransformIntoMaxCliques(std::vector< std::vector< Literal > > *at_most_ones, int64 max_num_explored_nodes=1e8)
Definition: clause.cc:1500
void RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
Definition: clause.cc:1887
void MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, absl::BitGenRef random)
Definition: clause.cc:849
Literal RepresentativeOf(Literal l) const
Definition: clause.h:561
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
Definition: clause.h:667
const std::vector< Literal > & DirectImplications(Literal literal)
Definition: clause.cc:1799
void AddImplication(Literal a, Literal b)
Definition: clause.h:488
void MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked)
Definition: clause.cc:831
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
ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span< const Literal > at_most_one)
Definition: clause.cc:531
void MinimizeConflictExperimental(const Trail &trail, std::vector< Literal > *c)
Definition: clause.cc:911
int DirectImplicationsEstimatedSize(Literal literal) const
Definition: clause.h:693
LiteralIndex Index() const
Definition: sat_base.h:84
ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)
Definition: clause.cc:339
bool Propagate(Trail *trail) final
Definition: clause.cc:183
void InprocessingRemoveClause(SatClause *clause)
Definition: clause.cc:358
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: clause.cc:192
absl::flat_hash_map< SatClause *, ClauseInfo > * mutable_clauses_info()
Definition: clause.h:223
SatClause * AddRemovableClause(const std::vector< Literal > &literals, Trail *trail)
Definition: clause.cc:212
SatClause * InprocessingAddClause(absl::Span< const Literal > new_clause)
Definition: clause.cc:415
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
Definition: clause.h:239
void Attach(SatClause *clause, Trail *trail)
Definition: clause.cc:274
bool AddClause(absl::Span< const Literal > literals, Trail *trail)
Definition: clause.cc:205
SatClause * ReasonClause(int trail_index) const
Definition: clause.cc:197
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
void LazyDetach(SatClause *clause)
Definition: clause.cc:294
const std::vector< SatClause * > & AllClausesInCreationOrder() const
Definition: clause.h:211
const std::vector< Watcher > & WatcherListOnFalse(Literal false_literal) const
Definition: clause.h:312
void Detach(SatClause *clause)
Definition: clause.cc:301
void Resize(int num_variables)
Definition: clause.cc:69
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
absl::Span< const Literal > AsSpan() const
Definition: clause.h:90
const Literal *const begin() const
Definition: clause.h:69
absl::Span< const Literal > PropagationReason() const
Definition: clause.h:85
Literal SecondLiteral() const
Definition: clause.h:75
Literal PropagatedLiteral() const
Definition: clause.h:80
bool IsSatisfied(const VariablesAssignment &assignment) const
Definition: clause.cc:1984
bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment &assignment)
Definition: clause.cc:1960
std::string DebugString() const
Definition: clause.cc:1991
const Literal *const end() const
Definition: clause.h:70
Literal FirstLiteral() const
Definition: clause.h:74
static SatClause * Create(absl::Span< const Literal > literals)
Definition: clause.cc:1947
void RegisterPropagator(SatPropagator *propagator)
Definition: sat_base.h:551
void ChangeReason(int trail_index, int propagator_id)
Definition: sat_base.h:335
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
int64_t int64
const int INFO
Definition: log_severity.h:31
#define DISALLOW_COPY_AND_ASSIGN(TypeName)
Definition: macros.h:29
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
const LiteralIndex kNoLiteralIndex(-1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
#define IF_STATS_ENABLED(instructions)
Definition: stats.h:437
bool operator==(BinaryClause o) const
Definition: clause.h:377
bool operator!=(BinaryClause o) const
Definition: clause.h:378
BinaryClause(Literal _a, Literal _b)
Definition: clause.h:376
Watcher(SatClause *c, Literal b, int i=2)
Definition: clause.h:289