In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
and
graph theory
In mathematics and computer science, graph theory is the study of ''graph (discrete mathematics), graphs'', which are mathematical structures used to model pairwise relations between objects. A graph in this context is made up of ''Vertex (graph ...
, 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 expression
In computer science, a Boolean expression (also known as logical expression) is an expression used in programming languages that produces a Boolean value when evaluated. A Boolean value is either true or false. A Boolean expression may be compos ...
s.
Applications
A
2-satisfiability instance in
conjunctive normal form
In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.
In au ...
can be transformed into an implication graph by replacing each of its
disjunction
In logic, disjunction (also known as logical disjunction, logical or, logical addition, or inclusive disjunction) is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is ...
s by a pair of implications. For example, the statement
can be rewritten as the pair
. An instance is satisfiable
if and only if
In logic and related fields such as mathematics and philosophy, "if and only if" (often shortened as "iff") is paraphrased by the biconditional, a logical connective between statements. The biconditional is true in two cases, where either bo ...
no literal and its
negation
In logic, negation, also called the logical not or logical complement, is an operation (mathematics), operation that takes a Proposition (mathematics), proposition P to another proposition "not P", written \neg P, \mathord P, P^\prime or \over ...
belong to the same
strongly connected component
In the mathematics, mathematical theory of directed graphs, a graph is said to be strongly connected if every vertex is reachability, reachable from every other vertex. The strongly connected components of a directed graph form a partition of a s ...
of its implication graph; this characterization can be used to solve instances in
linear time
In theoretical computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations ...
.
In
CDCL SAT
The SAT ( ) is a standardized test widely used for college admissions in the United States. Since its debut in 1926, its name and Test score, scoring have changed several times. For much of its history, it was called the Scholastic Aptitude Test ...
-solvers,
unit propagation
Unit propagation (UP) or boolean constraint propagation (BCP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses.
Definition
The procedure is based on unit clause ...
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.
References
Boolean algebra
Application-specific graphs
Directed graphs
Graph families