An implication graph representing the 2-satisfiability instance ( x 0 ∨ x 2 ) ∧ ( x 0 ∨ ¬ x 3 ) ∧ ( x 1 ∨ ¬ x 3 ) ∧ ( x 1 ∨ ¬ x 4 ) ∧ ( x 2 ∨ ¬ x 4 ) ∧ ( x 0 ∨ ¬ x 5 ) ∧ ( x 1 ∨ ¬ x 5 ) ∧ ( x 2 ∨ ¬ x 5 ) ∧ ( x 3 ∨ x 6 ) ∧ ( x 4 ∨ x 6 ) ∧ ( x 5 ∨ x 6 ) . {\displaystyle \scriptscriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad \scriptscriptstyle (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).}

In mathematical logic and graph theory, an implication graph is a skew-symmetric, directed graph G = (V, E) composed of vertex set V and directed edge set E. Each vertex in V represents the truth status of a Boolean literal, and each directed edge from vertex u to vertex v represents the material implication "If the literal u is true then the literal v is also true". Implication graphs were originally used for analyzing complex Boolean expressions.

Applications

A 2-satisfiability instance in conjunctive normal form can be transformed into an implication graph by replacing each of its disjunctions by a pair of implications. For example, the statement ( x 0 ∨ x 1 ) {\displaystyle (x_{0}\lor x_{1})} can be rewritten as ( ¬ x 0 → x 1 ) {\displaystyle (\neg x_{0}\rightarrow x_{1})}, but ( ¬ x 1 → x 0 ) {\displaystyle (\neg x_{1}\rightarrow x_{0})} also works. An instance is satisfiable if and only if no literal and its negation belong to the same strongly connected component of its implication graph; this characterization can be used to solve 2-satisfiability instances in linear time.

In CDCL SAT-solvers, unit propagation can be naturally associated with an implication graph that captures all possible ways of deriving all implied literals from decision literals, which is then used for clause learning.