C++ Reference: class BinaryImplicationGraph

This documentation is automatically generated.

Special class to store and propagate clauses of size 2 (i.e. implication). Such clauses are never deleted. Together, they represent the 2-SAT part of the problem. Note that 2-SAT satisfiability is a polynomial problem, but W2SAT (weighted 2-SAT) is NP-complete.

TODO(user): All the variables in a strongly connected component are equivalent and can be thus merged as one. This is relatively cheap to compute from time to time (linear complexity). We will also get contradiction (a <=> not a) this way.

TODO(user): An implication (a => not a) implies that a is false. I am not sure it is worth detecting that because if the solver assign a to true, it will learn that right away. I don't think we can do it faster.

TODO(user): The implication graph can be pruned. This is called the transitive reduction of a graph. For instance If a => {b,c} and b => {c}, then there is no need to store a => {c}. The transitive reduction is unique on an acyclic graph. Computing it will allow for a faster propagation and memory reduction. It is however not cheap. Maybe simple lazy heuristics to remove redundant arcs are better. Note that all the learned clauses we add will never be redundant (but they could introduce cycles).

TODO(user): Add a preprocessor to remove duplicates in the implication lists. Note that all the learned clauses we had will never create duplicates.

References for most of the above TODO and more:
   - Brafman RI, "A simplifier for propositional formulas with many binary clauses", IEEE Trans Syst Man Cybern B Cybern. 2004 Feb;34(1):52-9. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=
   - Marijn J. H. Heule, Matti Järvisalo, Armin Biere, "Efficient CNF Simplification Based on Binary Implication Graphs", Theory and Applications of Satisfiability Testing - SAT 2011, Lecture Notes in Computer Science Volume 6695, 2011, pp 201-215 http://www.cs.helsinki.fi/u/mjarvisa/papers/heule-jarvisalo-biere.sat11.pdf

Return type: ABSL_MUST_USE_RESULT bool

Arguments: absl::Span<const Literal> at_most_one

An at most one constraint of size n is a compact way to encode n * (n - 1) implications. This must only be called at level zero. Returns false if this creates a conflict. Currently this can only happens if there is duplicate literal already assigned to true in this constraint.


Return type: void

Arguments: Literal a, Literal b

Adds the binary clause (a OR b), which is the same as (not a => b). Note that it is also equivalent to (not b => a).


Return type: void

Arguments: Literal a, Literal b, Trail* trail

Same as AddBinaryClause() but enqueues a possible unit propagation. Note that if the binary clause propagates, it must do so at the last level, this is DCHECKed.


Return type: explicit

Arguments: Model* model



Return type: bool

Prunes the implication graph by calling first DetectEquivalences() to remove cycle and then by computing the transitive reduction of the remaining DAG. Note that this can be slow (num_literals graph traversals), so we abort early if we start doing too much work.


Return type: bool

Returns false if the model is unsat, otherwise detects equivalent variable (with respect to the implications only) and reorganize the propagation lists accordingly. TODO(user): Completely get rid of such literal instead? it might not be reasonable code-wise to remap our literals in all of our constraints though.


Return type: void

Arguments: Output* out


Return type: bool

Returns true if there is no constraints in this class.


Return type: void

Arguments: const Trail& trail, std::vector<Literal>* c


Return type: void

Arguments: const Trail& trail, std::vector<Literal>* c, SparseBitset<BooleanVariable>* marked


Return type: void

Arguments: const Trail& trail, std::vector<Literal>* c, SparseBitset<BooleanVariable>* marked, random_engine_t* random


Return type: void

Arguments: std::vector<Literal>* c

Uses the binary implication graph to minimize the given conflict by removing literals that implies others. The idea is that if a and b are two literals from the given conflict and a => b (which is the same as not(b) => not(a)) then a is redundant and can be removed. Note that removing as many literals as possible is too time consuming, so we use different heuristics/algorithms to do this minimization. See the binary_minimization_algorithm SAT parameter and the .cc for more details about the different algorithms.


Return type: int64

Number of literals inspected by this class during propagation.


Return type: int64


Return type: int64

MinimizeClause() stats.


Return type: int64

Number of literal propagated by this class (including conflicts).


Return type: int64

Number of implications removed by transitive reduction.


Return type: int64

Returns the number of current "half-implications". That is a => b and not(b) => not(a) are counted separately.


Return type: bool

Arguments: Trail* trail

SatPropagator interface.


Return type: absl::Span<const Literal>

Arguments: const Trail& trail, int trail_index


Return type: void

Arguments: int first_unprocessed_trail_index, const Trail& trail

This must only be called at decision level 0 after all the possible propagations. It: - Removes the variable at true from the implications lists. - Frees the propagation list of the assigned literals.


Return type: Literal

Arguments: Literal l

Returns the representative of the equivalence class of l (or l itself if it is on its own). Note that DetectEquivalences() should have been called to get any non-trival results.


Return type: void

Arguments: int num_variables

Resizes the data structure.


Return type: void

Arguments: std::vector<std::vector<Literal>>* at_most_ones, int64 max_num_explored_nodes = 1e8

Another way of representing an implication graph is a list of maximal "at most one" constraints, each forming a max-clique in the incompatibility graph. This representation is useful for having a good linear relaxation. This function will transform each of the given constraint into a maximal one in the underlying implication graph. Constraints that are redundant after other have been expanded (i.e. included into) will be cleared.