mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...

and

graph theory In mathematics, graph theory is the study of '' graphs'', which are mathematical structures used to model pairwise relations between objects. A graph in this context is made up of '' vertices'' (also called ''nodes'' or ''points'') which are conn ...

, an implication graph is a skew-symmetric, directed graph composed of vertex set and directed edge set . Each vertex in represents the truth status of a Boolean literal, and each directed edge from vertex to vertex represents the material implication "If the literal is true then the literal 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

(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 if and only if no literal and its negation belong to the same

strongly connected component In the mathematical theory of directed graphs, a graph is said to be strongly connected if every vertex is reachable from every other vertex. The strongly connected components of an arbitrary directed graph form a partition into subgraphs that a ...

of its implication graph; this characterization can be used to solve 2-satisfiability 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,{{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.rochester.edu/u/kautz/papers/learnIjcai.pdf which is then used for clause learning.

References

Boolean algebra Application-specific graphs Directed graphs Graph families