Implication graph

From Wikipedia, the free encyclopedia

An implication graph representing the 2-satisfiability instance
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.[1]

[edit] References

  1. ^ Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979). "A linear-time algorithm for testing the truth of certain quantified boolean formulas". Information Processing Letters 8 (3): 121–123. doi:10.1016/0020-0190(79)90002-4. 
\lnot(p\land\lnot p)  This logic-related article is a stub. You can help by expanding it.