# 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): Most of the note below are done, but we currently only applies the reduction before the solve. We should consider doing more in-processing. The code could probably still be improved too.

Note(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. This is done by DetectEquivalences().

Note(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.

Note(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). This is done by ComputeTransitiveReduction().

Note(user): This class natively support at most one constraints. This is a way to reduced significantly the memory and size of some 2-SAT instances. However, it is not fully exploited for pure SAT problems. See TransformIntoMaxCliques().

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

References for most of the above 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=10.1.1.28.4911

- 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

Method | |
---|---|

`AddAtMostOne` | Return type: Arguments: 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. |

`AddBinaryClause` | Return type: Arguments: 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). |

`AddBinaryClauseDuringSearch` | Return type: Arguments: 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 false and do nothing if both a and b are currently false. |

`AddImplication` | Return type: Arguments: |

`BinaryImplicationGraph` | Return type: Arguments: |

`~BinaryImplicationGraph` | |

`ChangeReason` | Return type: Arguments: Changes the reason of the variable at trail index to a binary reason. Note that the implication "new_reason => trail_[trail_index]" should be part of the implication graph. |

`CleanupAllRemovedVariables` | Return type: TODO(user): consider at most ones. |

`ComputeTransitiveReduction` | Return type: Arguments: 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. Returns false if the model is detected to be UNSAT (this needs to call DetectEquivalences() if not already done). |

`DetectEquivalences` | Return type: Arguments: 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. |

`DirectImplications` | Return type: Arguments: The literals that are "directly" implied when literal is set to true. This is not a full "reachability". It includes at most ones propagation. The set of all direct implications is enough to describe the implications graph completely. When doing blocked clause elimination of bounded variable elimination, one only need to consider this list and not the full reachability. |

`DirectImplicationsEstimatedSize` | Return type: Arguments: A proxy for DirectImplications().size(), However we currently do not maintain it perfectly. It is exact each time DirectImplications() is called, and we update it in some situation but we don't deal with fixed variables, at_most ones and duplicates implications for now. |

`ExtractAllBinaryClauses` | Return type: Arguments: |

`FindFailedLiteralAroundVar` | Return type: Arguments: Variable elimination by replacing everything of the form a => var => b by a => b. We ignore any a => a so the number of new implications is not always just the product of the two direct implication list of var and not(var). However, if a => var => a, then a and var are equivalent, so this case will be removed if one run DetectEquivalences() before this. Similarly, if a => var => not(a) then a must be false and this is detected and dealt with by FindFailedLiteralAroundVar(). |

`Implications` | Return type: Arguments: Returns the list of literal "directly" implied by l. Beware that this can easily change behind your back if you modify the solver state. |

`IsDag` | Return type: Returns true if DetectEquivalences() has been called and no new binary clauses have been added since then. When this is true then there is no cycle in the binary implication graph (modulo the redundant literals that form a cycle with their representative). |

`IsEmpty` | Return type: Returns true if there is no constraints in this class. |

`IsRedundant` | Return type: Arguments: Returns true if this literal is fixed or is equivalent to another literal. This means that it can just be ignored in most situation. Note that the set (and thus number) of redundant literal can only grow over time. This is because we always use the lowest index as representative of an equivalent class, so a redundant literal will stay that way. |

`IsRemoved` | Return type: Arguments: |

`literal_size` | Return type: |

`MinimizeConflictExperimental` | Return type: Arguments: |

`MinimizeConflictFirst` | Return type: Arguments: |

`MinimizeConflictFirstWithTransitiveReduction` | Return type: Arguments: |

`MinimizeConflictWithReachability` | Return type: Arguments: 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. |

`num_implications` | Return type: Returns the number of current implications. Note that a => b and not(b) => not(a) are counted separately since they appear separately in our propagation lists. The number of size 2 clauses that represent the same thing is half this number. |

`num_inspections` | Return type: Number of literals inspected by this class during propagation. |

`num_literals_removed` | Return type: |

`num_minimization` | Return type: MinimizeClause() stats. |

`num_propagations` | Return type: Number of literal propagated by this class (including conflicts). |

`num_redundant_implications` | Return type: Number of implications removed by transitive reduction. |

`num_redundant_literals` | Return type: |

`NumImplicationOnVariableRemoval` | Return type: Arguments: |

`Propagate` | Return type: Arguments: SatPropagator interface. |

`Reason` | Return type: Arguments: |

`RemoveBooleanVariable` | Return type: Arguments: |

`RemoveFixedVariables` | Return type: 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. |

`RepresentativeOf` | Return type: Arguments: 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. |

`Resize` | Return type: Arguments: Resizes the data structure. |

`ReverseTopologicalOrder` | Return type: One must call DetectEquivalences() first, this is CHECKed. Returns a list so that if x => y, then x is after y. |

`SetDratProofHandler` | Return type: Arguments: |

`TransformIntoMaxCliques` | Return type: Arguments: 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. Returns false if the model is detected to be UNSAT (this needs to call DetectEquivalences() if not already done). |