# 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=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. |

`BinaryImplicationGraph` | Return type: Arguments: |

`~BinaryImplicationGraph` | |

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

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

`ExtractAllBinaryClauses` | Return type: Arguments: |

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

`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_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. |

`NumberOfImplications` | Return type: Returns the number of current "half-implications". That is a => b and not(b) => not(a) are counted separately. |

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

`Reason` | Return type: Arguments: |

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

`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. |