# Implication graph

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Implication_graph
> Markdown URL: https://mediated.wiki/source/Implication_graph.md
> Source: https://en.wikipedia.org/wiki/Implication_graph
> Source revision: 1344282808
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Directed graph representing a Boolean expression

An implication graph representing the [2-satisfiability](/source/2-satisfiability) instance

            (

              x

                0

            ∨

              x

                2

            )
            ∧
            (

              x

                0

            ∨
            ¬

              x

                3

            )
            ∧
            (

              x

                1

            ∨
            ¬

              x

                3

            )
            ∧
            (

              x

                1

            ∨
            ¬

              x

                4

            )
            ∧
            (

              x

                2

            ∨
            ¬

              x

                4

            )
            ∧

            (

              x

                0

            ∨
            ¬

              x

                5

            )
            ∧
            (

              x

                1

            ∨
            ¬

              x

                5

            )
            ∧
            (

              x

                2

            ∨
            ¬

              x

                5

            )
            ∧
            (

              x

                3

            ∨

              x

                6

            )
            ∧
            (

              x

                4

            ∨

              x

                6

            )
            ∧
            (

              x

                5

            ∨

              x

                6

            )
            .

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

In [mathematical logic](/source/Mathematical_logic) and [graph theory](/source/Graph_theory), an **implication graph** is a [skew-symmetric](/source/Skew-symmetric_graph), [directed graph](/source/Directed_graph) *G* = (*V*, *E*) composed of [vertex](/source/Vertex_(graph_theory)) set V and directed edge set E. Each vertex in V represents the truth status of a [Boolean literal](/source/Boolean_literal), and each directed edge from vertex u to vertex v represents the [material implication](/source/Material_conditional) "If the literal u is true then the literal v is also true". Implication graphs were originally used for analyzing complex [Boolean expressions](/source/Boolean_expression).

## Applications

A [2-satisfiability](/source/2-satisfiability) instance in [conjunctive normal form](/source/Conjunctive_normal_form) can be transformed into an implication graph by replacing each of its [disjunctions](/source/Disjunction) by a pair of implications. For example, the statement ( x 0 ∨ x 1 ) {\displaystyle (x_{0}\lor x_{1})} can be rewritten as ( ¬ x 0 → x 1 ) {\displaystyle (\neg x_{0}\rightarrow x_{1})} , but ( ¬ x 1 → x 0 ) {\displaystyle (\neg x_{1}\rightarrow x_{0})} also works. An instance is satisfiable [if and only if](/source/If_and_only_if) no literal and its [negation](/source/Negation) belong to the same [strongly connected component](/source/Strongly_connected_component) of its implication graph; this characterization can be used to solve 2-satisfiability instances in [linear time](/source/Linear_time).[1]

In [CDCL](/source/CDCL) [SAT](/source/Boolean_satisfiability_problem)-solvers, [unit propagation](/source/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

1. **[^](#cite_ref-1)** Aspvall, Bengt; [Plass, Michael F.](https://en.wikipedia.org/w/index.php?title=Michael_Plass&action=edit&redlink=1); [Tarjan, Robert E.](/source/Robert_Tarjan) (1979). "A linear-time algorithm for testing the truth of certain quantified boolean formulas". *Information Processing Letters*. **8** (3): 121–123. [doi](/source/Doi_(identifier)):[10.1016/0020-0190(79)90002-4](https://doi.org/10.1016%2F0020-0190%2879%2990002-4).

1. **[^](#cite_ref-2)** Paul Beame; Henry Kautz; Ashish Sabharwal (2003). [*Understanding the Power of Clause Learning*](https://www.cs.cornell.edu/~sabhar/publications/learnIJCAI03.pdf) (PDF). IJCAI. pp. 1194–1201.

---
Adapted from the Wikipedia article [Implication graph](https://en.wikipedia.org/wiki/Implication_graph) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Implication_graph?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.