Английская Википедия:Implication graph

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Файл:Implication graph.svg

An implication graph representing the Шаблон:Nowrap instance <math>\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).</math>

In mathematical logic and graph theory, an implication graph is a skew-symmetric, directed graph Шаблон:Math composed of vertex set Шаблон:Mvar and directed edge set Шаблон:Mvar. Each vertex in Шаблон:Mvar represents the truth status of a Boolean literal, and each directed edge from vertex Шаблон:Mvar to vertex Шаблон:Mvar represents the material implication "If the literal Шаблон:Mvar is true then the literal Шаблон:Mvar is also true". Implication graphs were originally used for analyzing complex Boolean expressions.

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 <math>(x_0\lor x_1)</math> can be rewritten as the pair <math>(\neg x_0 \rightarrow x_1), (\neg x_1 \rightarrow x_0)</math>. 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 Шаблон:Nowrap instances in linear time.

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