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 sy ...

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 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 position ...

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 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 ...

Applications

2-satisfiability In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case ...

instance in conjunctive normal form 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

(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 ...

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 procedure of automated theorem proving that can simplify a set of (usually propositional) clauses. Definition The procedure is based on unit claus ...

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