Implication graph

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

gollark: I think the sides work too.

gollark: The reason for the first thing is that remote wrapping/peripheral listing/whatever else is actually implemented in Lua using modems' `callRemote` (and other things), and only descends the "peripheral tree" one level because that's all it has to in vanilla CC.

gollark: The only important constraints I know of is that the OC relay must be directly adjacent to the computer (unless you program around this) and that you can't connect to the top of the 3D printer.

gollark: I think it's just that you can't connect stuff to the top.

gollark: Move items in and out, yes.

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.