implication graph
{{short description|Directed graph representing a Boolean expression}}
Image:Implication graph.svg}} instance ]]
In mathematical logic and graph theory, an implication graph is a skew-symmetric, directed graph {{math|1=G = (V, E)}} composed of 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 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 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 can be rewritten as the pair . 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.{{cite journal|author1= Aspvall, Bengt |author2=Plass, Michael F. |author3=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}}
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,{{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}} which is then used for clause learning.