Implication graph

An implication graph is a directed graph that represents consequences among logical assignments. The term has two closely related meanings in Boolean satisfiability. In the study of formulas in 2-conjunctive normal form, it denotes a static graph containing every implication encoded by the formula. In conflict-driven clause learning, it denotes a dynamic record of decisions, propagated assignments, and the dependencies that produced a conflict.

Both forms translate logical entailment into reachability, but they differ in scope. The graph associated with a 2-satisfiability instance describes all assignments permitted by its binary clauses, whereas the graph constructed by a solver describes only the portion of a search that has actually been explored. This distinction determines how vertices, edges, and graph decompositions are interpreted.

Static implication graphs

For a 2-conjunctive normal form formula, the vertices are the literals occurring in the formula. Every variable (x) therefore contributes two vertices, (x) and (\neg x). A binary clause

[ (a \lor b) ]

is logically equivalent to the pair of implications

[ \neg a \rightarrow b \qquad\text{and}\qquad \neg b \rightarrow a. ]

The implication graph consequently contains the directed edges ((\neg a,b)) and ((\neg b,a)). Because each clause produces both contrapositively related edges, reachability has a complementary symmetry: whenever a path leads from (u) to (v), a corresponding path leads from (\neg v) to (\neg u).

A formula is unsatisfiable exactly when some variable and its negation belong to the same strongly connected component. If (x) reaches (\neg x), assigning (x) to true forces it to false. If (\neg x) also reaches (x), the opposite assignment produces the complementary contradiction. Membership in one strongly connected component expresses both implications simultaneously.

When no such component exists, contracting every strongly connected component produces a directed acyclic graph. A satisfying assignment can then be characterized through an ordering of the contracted components that respects all graph edges. Complementary components occupy distinct positions in this ordering, allowing each variable to receive a value consistent with every implication.

The linear-time characterization of 2-satisfiability through strongly connected components was established by Bengt Aspvall, Michael Plass, and Robert Tarjan. Their formulation connected satisfiability testing with standard graph traversal and component-decomposition methods, yielding a running time linear in the size of the formula and its implication graph.

Dynamic implication graphs in satisfiability solving

In a solver based on the Davis–Putnam–Logemann–Loveland algorithm, an implication graph records assignments generated during one branch of the search. A vertex represents a literal that has become true under the current partial assignment. Decision literals have no incoming justification edges because their values were selected by the branching mechanism. Propagated literals have incoming edges determined by clauses that became unit clauses.

Suppose the solver contains the clause

[ (\neg p \lor \neg q \lor r) ]

and the current assignment makes both (p) and (q) true. The clause then forces (r) to become true. The graph contains edges from the vertices (p) and (q) to the vertex (r), expressing that the assignments to (p) and (q) jointly provided the antecedent for the propagation.

An edge does not ordinarily represent a complete material implication in isolation. In the preceding example, neither (p) nor (q) alone forces (r); the relevant implication is conjunctive:

[ p \land q \rightarrow r. ]

The ordinary directed graph records this hypergraph-like dependency by placing one edge from each antecedent into the propagated vertex. The associated clause, commonly called the reason clause or antecedent clause, preserves the full logical relation.

Assignments are organized into decision levels. The first branching assignment establishes a level, and every literal propagated from assignments at that level remains associated with it unless its reason depends entirely on earlier levels. A later branching decision establishes another level. The graph is acyclic when vertices are ordered by the time at which their assignments were made, because a propagation depends only on assignments already present.

Conflict representation

A conflict occurs when a clause becomes false under the current assignment. The implication graph represents this event with a distinguished conflict vertex, conventionally denoted by (\kappa) or (\bot). Incoming edges connect the assignments that falsified the conflicting clause to this vertex.

For example, if the clause

[ (\neg s \lor \neg t) ]

is falsified because (s) and (t) are both true, the graph contains edges from (s) and (t) to the conflict vertex. Paths ending at the conflict thereby expose the sequence of decisions and propagations responsible for the inconsistency. Portions of the current assignment that do not reach the conflict are irrelevant to that particular analysis.

The conflict graph is not normally materialized as a permanent graph data structure. Solver implementations retain a propagation trail, a decision level for each assignment, and a reference to the clause that implied each propagated literal. These records define the same graph implicitly and permit its relevant edges to be reconstructed during conflict analysis.

Cuts and learned clauses

A cut partitions the vertices involved in a conflict into a reason side and a conflict side. Decision assignments responsible for the conflict remain on the reason side, while the conflict vertex lies on the conflict side. Every edge crossing the cut identifies an assignment whose consequence enters the conflicting region.

The negations of the assignments at the boundary form a learned clause. If the boundary contains the true literals (a), (b), and (\neg c), the corresponding learned clause is

[ (\neg a \lor \neg b \lor c). ]

This clause excludes the combination of boundary assignments that reproduced the conflict. It is entailed by the original formula because conflict analysis derives it through repeated applications of resolution between the conflicting clause and the reason clauses of propagated literals.

Different cuts can produce different learned clauses. A cut positioned close to the original decisions generally contains more boundary literals, while a cut positioned close to the conflict generally reflects a narrower portion of the immediate causal structure. Logical validity does not depend on the cut position, although the resulting clause and its later behavior in the solver do.

During the mid-1990s, You Watanabe formulated the cut interpretation using a distinguished conflict sink and decision-level annotations, unifying the graphical account of propagation with resolution-based clause derivation. Her treatment identified dominator structure as the relevant criterion for selecting a canonical boundary in the current decision level. This formulation became part of the terminology used to describe implication-graph conflict analysis.

Unique implication points

A unique implication point, abbreviated UIP, is a vertex at the current decision level through which every directed path from the current decision literal to the conflict must pass. In graph-theoretic language, such a vertex dominates the conflict relative to the current decision.

The current decision literal is always a UIP whenever that decision contributes to the conflict. Additional UIPs can occur farther along the propagation structure. The first UIP is the one encountered nearest to the conflict when paths are examined backward, rather than the first assignment made at the decision level.

First-UIP analysis resolves away current-level literals until only one literal from the current decision level remains in the learned clause. The retained literal is the negation of the first UIP assignment. The learned clause then becomes unit after the solver returns to the greatest decision level represented by any of its other literals.

This destination is the clause’s assertion level. Returning directly to it is a form of non-chronological backtracking, because several intervening decisions can be discarded at once. The learned clause immediately propagates its remaining current-level literal, preventing reconstruction of the same conflict through the same boundary assignment.

The conflict-analysis framework was incorporated into the GRASP satisfiability architecture developed by João Marques-Silva and Karem Sakallah. Related clause-learning and relevance-based search mechanisms were developed by Robert Bayardo and Robert Schrag. These systems established implication graphs as the standard explanatory model for deriving learned clauses from unit propagation.

Relationship between the two meanings

The static and dynamic meanings of implication graph coincide most closely for formulas containing only binary clauses. A binary clause ((\neg a \lor b)) provides the fixed implication edge (a\rightarrow b). When a solver assigns (a) and propagates (b) from that clause, the same edge appears in the dynamic graph as an actual dependency.

For clauses containing more than two literals, the static binary-edge interpretation is insufficient because propagation depends on a conjunction of assignments. A clause

[ (\neg a_1 \lor \neg a_2 \lor \cdots \lor \neg a_k \lor b) ]

forces (b) only when every (a_i) is true. The dynamic graph records an incoming edge from each (a_i) to (b), while the reason clause preserves their collective significance. Consequently, reachability in a dynamic implication graph describes causal dependence within one partial assignment rather than unrestricted logical implication throughout the formula.

The two constructions nevertheless share a common invariant. A directed path represents a chain of consequences, and a cycle or converging path structure exposes a constraint that cannot be understood from one assignment in isolation. Strongly connected components capture global inconsistency in 2-satisfiability, whereas cuts and dominators capture the local structure of a conflict during clause-learning search.

Computational representation

An explicit implication graph could require storage proportional to the number of propagation dependencies generated during a search branch. Contemporary solver organization instead uses the assignment trail as a topological ordering of the implicit graph. Each propagated literal retains a reference to its reason clause, while each decision literal carries a null reason.

Conflict analysis traverses this representation in reverse trail order. Resolving on the most recently assigned current-level literal removes that literal from the working clause and replaces it with the earlier assignments appearing in its reason. The traversal reaches the first UIP when the working clause contains exactly one literal assigned at the current decision level.

This representation also supports clause-activity calculations and deletion policies without changing the logical interpretation of the graph. Learned clauses may later become reason clauses for new propagations, causing information derived from an earlier conflict to participate in subsequent implication graphs. The graph for an individual branch remains transient, while the learned clauses preserve selected consequences across the continuing search.