In
Boolean logic
In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas ...
, a
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
is in conjunctive normal form (CNF) or clausal normal form if it is a
conjunction of one or more
clauses
In language, a clause is a constituent that comprises a semantic predicand (expressed or not) and a semantic predicate. A typical clause consists of a subject and a syntactic predicate, the latter typically a verb phrase composed of a verb with ...
, where a clause is a
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 ...
of
literal
Literal may refer to:
* Interpretation of legal concepts:
** Strict constructionism
** The plain meaning rule
The plain meaning rule, also known as the literal rule, is one of three rules of statutory construction traditionally applied by ...
s; otherwise put, it is a product of sums or an AND of ORs. As a
canonical normal form, it is useful in
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ...
and
circuit theory.
All conjunctions of literals and all disjunctions of literals are in CNF, as they can be seen as conjunctions of one-literal clauses and conjunctions of a single clause, respectively. As in the
disjunctive normal form (DNF), the only propositional connectives a formula in CNF can contain are
and
or AND may refer to:
Logic, grammar, and computing
* Conjunction (grammar), connecting two words, phrases, or clauses
* Logical conjunction in mathematical logic, notated as "∧", "⋅", "&", or simple juxtaposition
* Bitwise AND, a boolea ...
,
or, and
not. The not operator can only be used as part of a literal, which means that it can only precede a
propositional variable or a
predicate symbol.
In automated theorem proving, the notion "''clausal normal form''" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.
Examples and non-examples
All of the following formulas in the variables
, and
are in conjunctive normal form:
*
*
*
*
For clarity, the disjunctive clauses are written inside parentheses above. In
disjunctive normal form with parenthesized conjunctive clauses, the last case is the same, but the next to last is
. The constants ''true'' and ''false'' are denoted by the empty conjunct and one clause consisting of the empty disjunct, but are normally written explicitly.
The following formulas are not in conjunctive normal form:
*
, since an OR is nested within a NOT
*
*
, since an AND is nested within an OR
Every formula can be equivalently written as a formula in conjunctive normal form. The three non-examples in CNF are:
*
*
*
Conversion into CNF
Every
propositional formula can be converted into an
equivalent formula that is in CNF. This transformation is based on rules about
logical equivalence
In logic and mathematics, statements p and q are said to be logically equivalent if they have the same truth value in every model. The logical equivalence of p and q is sometimes expressed as p \equiv q, p :: q, \textsfpq, or p \iff q, depending o ...
s:
double negation elimination
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not ( ...
,
De Morgan's laws
In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British math ...
, and the
distributive law.
Since all propositional formulas can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF. However, in some cases this conversion to CNF can lead to an exponential explosion of the formula. For example, translating the following non-CNF formula into CNF produces a formula with
clauses:
:
In particular, the generated formula is:
:
This formula contains
clauses; each clause contains either
or
for each
.
There exist transformations into CNF that avoid an exponential increase in size by preserving
satisfiability rather than
equivalence. These transformations are guaranteed to only linearly increase the size of the formula, but introduce new variables. For example, the above formula can be transformed into CNF by adding variables
as follows:
:
An
interpretation
Interpretation may refer to:
Culture
* Aesthetic interpretation, an explanation of the meaning of a work of art
* Allegorical interpretation, an approach that assumes a text should not be interpreted literally
* Dramatic Interpretation, an event ...
satisfies this formula only if at least one of the new variables is true. If this variable is
, then both
and
are true as well. This means that every
model that satisfies this formula also satisfies the original one. On the other hand, only some of the models of the original formula satisfy this one: since the
are not mentioned in the original formula, their values are irrelevant to satisfaction of it, which is not the case in the last formula. This means that the original formula and the result of the translation are
equisatisfiable but not
equivalent.
An alternative translation, the
Tseitin transformation, includes also the clauses
. With these clauses, the formula implies
; this formula is often regarded to "define"
to be a name for
.
First-order logic
In first order logic, conjunctive normal form can be taken further to yield the clausal normal form of a logical formula, which can be then used to perform
first-order resolution.
In resolution-based automated theorem-proving, a CNF formula
See
below
Below may refer to:
*Earth
* Ground (disambiguation)
*Soil
*Floor
* Bottom (disambiguation)
*Less than
*Temperatures below freezing
*Hell or underworld
People with the surname
*Ernst von Below (1863–1955), German World War I general
*Fred Below ...
for an example.
Computational complexity
An important set of problems in
computational complexity
In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) ...
involves finding assignments to the variables of a boolean formula expressed in conjunctive normal form, such that the formula is true. The ''k''-SAT problem is the problem of finding a satisfying assignment to a boolean formula expressed in CNF in which each disjunction contains at most ''k'' variables.
3-SAT is
NP-complete (like any other ''k''-SAT problem with ''k''>2) while
2-SAT
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 Constraint (mathematics), constraints on pairs of variabl ...
is known to have solutions in
polynomial time
In 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 performed by ...
. As a consequence,
[since one way to check a CNF for satisfiability is to convert it into a DNF, the satisfiability of which can be checked in ]linear time
In 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 performed by ...
the task of converting a formula into a
DNF, preserving satisfiability, is
NP-hard
In computational complexity theory, NP-hardness ( non-deterministic polynomial-time hardness) is the defining property of a class of problems that are informally "at least as hard as the hardest problems in NP". A simple example of an NP-hard pr ...
;
dually, converting into CNF, preserving
validity, is also NP-hard; hence equivalence-preserving conversion into DNF or CNF is again NP-hard.
Typical problems in this case involve formulas in "3CNF": conjunctive normal form with no more than three variables per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts.
A formula in CNF can be converted into an equisatisfiable formula in "''k''CNF" (for ''k''≥3) by replacing each conjunct with more than ''k'' variables
by two conjuncts
and
with a new variable, and repeating as often as necessary.
Converting from first-order logic
To convert
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
to CNF:
[Artificial Intelligence: A modern Approach](_blank)
995...Russell and Norvig
#Convert to
negation normal form In mathematical logic, a formula is in negation normal form (NNF) if the negation operator (\lnot, ) is only applied to variables and the only other allowed Boolean operators are conjunction (\land, ) and disjunction (\lor, ).
Negation normal fo ...
.
## Eliminate implications and equivalences: repeatedly replace
with
; replace
with
. Eventually, this will eliminate all occurrences of
and
.
##Move NOTs inwards by repeatedly applying
De Morgan's law. Specifically, replace
with
; replace
with
; and replace
with
; replace
with
;
with
. After that, a
may occur only immediately before a predicate symbol.
#Standardize variables
##For sentences like
which use the same variable name twice, change the name of one of the variables. This avoids confusion later when dropping quantifiers. For example,