Implication graph

{{short description|Directed graph representing a Boolean expression}} [[Image:Implication graph.svg|thumb|upright=1.35|An implication graph representing the {{nowrap|[[2-satisfiability]]}} 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 graph|skew-symmetric]], [[directed graph]] {{math|1=''G'' = (''V'', ''E'')}} composed of [[vertex (graph theory)|vertex]] set {{mvar|V}} and directed edge set {{mvar|E}}. Each vertex in {{mvar|V}} represents the truth status of a [[Boolean literal]], and each directed edge from vertex {{mvar|u}} to vertex {{mvar|v}} represents the [[material conditional|material implication]] "If the literal {{mvar|u}} is true then the literal {{mvar|v}} is also true". Implication graphs were originally used for analyzing complex [[Boolean expression]]s.

==Applications== A [[2-satisfiability]] instance in [[conjunctive normal form]] can be transformed into an implication graph by replacing each of its [[disjunction]]s by a pair of implications. For example, the statement <math>(x_0\lor x_1)</math> can be rewritten as <math>(\neg x_0 \rightarrow x_1)</math>, but <math> (\neg x_1 \rightarrow x_0)</math> also works. 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|2-satisfiability}} instances in [[linear time]].<ref>{{cite journal|author1= Aspvall, Bengt |author2=[[Michael Plass|Plass, Michael F.]] |author3=[[Robert Tarjan|Tarjan, Robert E.]] |title = A linear-time algorithm for testing the truth of certain quantified boolean formulas|journal = Information Processing Letters | volume = 8 | issue = 3 | pages = 121–123|year = 1979|doi = 10.1016/0020-0190(79)90002-4}}</ref>

In [[CDCL]] [[Boolean satisfiability problem|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,<ref>{{cite conference|author1=Paul Beame |author2=Henry Kautz |author3=Ashish Sabharwal |title = Understanding the Power of Clause Learning| conference = IJCAI | pages = 1194–1201|year = 2003|url=https://www.cs.cornell.edu/~sabhar/publications/learnIJCAI03.pdf}}</ref> which is then used for clause learning.

==References== <references/>

[[Category:Boolean algebra]] [[Category:Application-specific graphs]] [[Category:Directed graphs]] [[Category:Graph families]]