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

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, SparseBitset<BooleanVariable>* marked, 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.

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