Implication graph

In

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

.

Applications

A

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

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

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.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Implication_graph&oldid=1212859793"

[1] :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.

[1]

[2]