In
mathematical logic
Mathematical logic is the study of logic, 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 for ...
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 conne ...
, an implication graph is a
skew-symmetric,
directed graph
In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs.
Definition
In formal terms, a directed graph is an ordered pa ...
composed of
vertex
Vertex, vertices or vertexes may refer to:
Science and technology Mathematics and computer science
*Vertex (geometry), a point where two or more curves, lines, or edges meet
* Vertex (computer graphics), a data structure that describes the positio ...
set and directed edge set . Each vertex in represents the truth status of a
Boolean literal
In mathematical logic, a literal is an atomic formula (also known as an atom or prime formula) or its negation. The definition mostly appears in proof theory (of classical logic), e.g. in conjunctive normal form and the method of resolution.
Liter ...
, 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 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 composed of a combination of the Boolean con ...
s.
Applications
A
2-satisfiability instance in
conjunctive normal form
In Boolean logic, 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. As a can ...
can be transformed into an implication graph by replacing each of its
disjunction
In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor S ...
s 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
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
The SAT ( ) is a standardized test widely used for college admissions in the United States. Since its debut in 1926, its name and scoring have changed several times; originally called the Scholastic Aptitude Test, it was later called the Schol ...
-solvers,
unit propagation
Unit propagation (UP) or Boolean Constraint propagation (BCP) or the one-literal rule (OLR) is a Algorithm, procedure of automated theorem proving that can simplify a set of (usually propositional logic, propositional) Clause (logic), clauses.
Def ...
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