Implication graph

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.

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 \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}).

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}\lor x_{1})$ can be rewritten as the pair $(\neg x_{0}\rightarrow x_{1}),(\neg x_{1}\rightarrow 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 2-satisfiability instances in linear time.[1]

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,[2] which is then used for clause learning.

References

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.
Paul Beame; Henry Kautz; Ashish Sabharwal (2003). Understanding the Power of Clause Learning (PDF). IJCAI. pp. 1194–1201.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[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.

[2] Paul Beame; Henry Kautz; Ashish Sabharwal (2003). Understanding the Power of Clause Learning (PDF). IJCAI. pp. 1194–1201.