Implication graph

An implication graph representing the Template:Nowrap instance $\genfrac{}{}{0ex}{}{(x_0\vee x_2)\wedge (x_0\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_4)\wedge (x_2\vee \mathrm{\neg }{x}_4)\wedge }{(x_0\vee \mathrm{\neg }{x}_5)\wedge (x_1\vee \mathrm{\neg }{x}_5)\wedge (x_2\vee \mathrm{\neg }{x}_5)\wedge (x_3\vee x_6)\wedge (x_4\vee x_6)\wedge (x_5\vee x_6).}$

In mathematical logic and graph theory, an implication graph is a skew-symmetric, directed graph Template:Math composed of vertex set Template:Mvar and directed edge set Template:Mvar. Each vertex in Template:Mvar represents the truth status of a Boolean literal, and each directed edge from vertex Template:Mvar to vertex Template:Mvar represents the material implication "If the literal Template:Mvar is true then the literal Template:Mvar 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\vee x_1)$ can be rewritten as the pair $(\mathrm{\neg }{x}_0\to x_1),(\mathrm{\neg }{x}_1\to x_0)$. 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 Template:Nowrap 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.