C++ Reference: class BinaryImplicationGraph

Note: 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: 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.
AddBinaryClause	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).
AddBinaryClauseDuringSearch	Return type: bool Arguments: Literal a, Literal b 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: void Arguments: Literal a, Literal b
BinaryImplicationGraph	Return type: explicit Arguments: Model* model
~BinaryImplicationGraph
ChangeReason	Return type: void Arguments: int trail_index, Literal new_reason 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: void TODO(user): consider at most ones.
ComputeTransitiveReduction	Return type: bool Arguments: bool log_info = false 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: bool Arguments: bool log_info = false 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: const std::vector<Literal>& Arguments: Literal literal 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: int Arguments: Literal literal 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.
ExpandAtMostOneWithWeight	Return type: std::vector<Literal> Arguments: const absl::Span<const Literal> at_most_one, const absl::StrongVector<LiteralIndex, bool>& can_be_included, const absl::StrongVector<LiteralIndex, double>& expanded_lp_values
ExtractAllBinaryClauses	Return type: void Arguments: Output* out
FindFailedLiteralAroundVar	Return type: bool Arguments: BooleanVariable var, bool* is_unsat 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: const absl::InlinedVector<Literal, 6>& Arguments: Literal l 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: bool 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: bool Returns true if there is no constraints in this class.
IsRedundant	Return type: bool Arguments: Literal l 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: bool Arguments: Literal l
literal_size	Return type: int64_t
MinimizeConflictExperimental	Return type: void Arguments: const Trail& trail, std::vector<Literal>* c
MinimizeConflictFirst	Return type: void Arguments: const Trail& trail, std::vector<Literal>* c, SparseBitset<BooleanVariable>* marked
MinimizeConflictFirstWithTransitiveReduction	Return type: void Arguments: const Trail& trail, std::vector<Literal>* c, absl::BitGenRef random
MinimizeConflictWithReachability	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.
num_implications	Return type: int64_t 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: int64_t Number of literals inspected by this class during propagation.
num_literals_removed	Return type: int64_t
num_minimization	Return type: int64_t MinimizeClause() stats.
num_propagations	Return type: int64_t Number of literal propagated by this class (including conflicts).
num_redundant_implications	Return type: int64_t Number of implications removed by transitive reduction.
num_redundant_literals	Return type: int64_t
NumImplicationOnVariableRemoval	Return type: int64_t Arguments: BooleanVariable var
Propagate	Return type: bool Arguments: Trail* trail SatPropagator interface.
Reason	Return type: absl::Span<const Literal> Arguments: const Trail& trail, int trail_index
RemoveBooleanVariable	Return type: void Arguments: BooleanVariable var, std::deque<std::vector<Literal>>* postsolve_clauses
RemoveFixedVariables	Return type: void 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: 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.
ResetWorkDone	Return type: void ExpandAtMostOneWithWeight() will increase this, so a client can put a limit on this possibly expansive operation.
Resize	Return type: void Arguments: int num_variables Resizes the data structure.
ReverseTopologicalOrder	Return type: const std::vector<LiteralIndex>& One must call DetectEquivalences() first, this is CHECKed. Returns a list so that if x => y, then x is after y.
SetDratProofHandler	Return type: void Arguments: DratProofHandler* drat_proof_handler
TransformIntoMaxCliques	Return type: bool Arguments: std::vector<std::vector<Literal>>* at_most_ones, int64_t 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. Note that the order of constraints will be conserved. Returns false if the model is detected to be UNSAT (this needs to call DetectEquivalences() if not already done).
WorkDone	Return type: int64_t