Implication graph

An implication graph representing the 2-satisfiability instance $\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 x_{5})\land (x_{1}\lor x_{5})\land (x_{2}\lor x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).$

In mathematical logic, 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 e(u, v) connecting vertex u and vertex v represents the implication "If the literal u is true then the literal v is also true". IGs were originally used for analyzing complex Boolean expressions.

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. The instance is satisfiable if and only if no literal and its negation belong to the same strongly connected component of the implication graph; this characterization can be used to solve 2-satisfiability instances in linear time.