In
Boolean logic, a
formula is in conjunctive normal form (CNF) or clausal normal form if it is a
conjunction
Conjunction may refer to:
* Conjunction (grammar), a part of speech
* Logical conjunction, a mathematical operator
** Conjunction introduction, a rule of inference of propositional logic
* Conjunction (astronomy), in which two astronomical bodies ...
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 S ...
of
literals; otherwise put, it is a product of sums or an AND of ORs. As a
canonical normal form
In Boolean algebra, any Boolean function can be expressed in the canonical disjunctive normal form ( CDNF) or minterm canonical form and its dual canonical conjunctive normal form ( CCNF) or maxterm canonical form. Other canonical forms include ...
, 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 ma ...
and
circuit theory
Circuit may refer to:
Science and technology
Electrical engineering
* Electrical circuit, a complete electrical network with a closed-loop giving a return path for current
** Analog circuit, uses continuous signal levels
** Balanced circui ...
.
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
In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or (in philosophical logic) a ''cluster c ...
(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
In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building-blocks of proposit ...
or a
predicate symbol In mathematical logic, a predicate variable is a predicate letter which functions as a "placeholder" for a relation (between terms), but which has not been specifically assigned any particular relation (or meaning). Common symbols for denoting predi ...
.
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
In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or (in philosophical logic) a ''cluster c ...
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
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional for ...
can be converted into an
equivalent
Equivalence or Equivalent may refer to:
Arts and entertainment
*Album-equivalent unit, a measurement unit in the music industry
* Equivalence class (music)
*'' Equivalent VIII'', or ''The Bricks'', a minimalist sculpture by Carl Andre
*''Equiva ...
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 (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
In mathematics, the distributive property of binary operations generalizes the distributive law, which asserts that the equality
x \cdot (y + z) = x \cdot y + x \cdot z
is always true in elementary algebra.
For example, in elementary arithmetic, ...
.
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
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
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 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
A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure.
Models c ...
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
In Mathematical logic (a subtopic within the field of formal logic), two formulae are equisatisfiable if the first formula is satisfiable whenever the second is and vice versa; in other words, either both formulae are satisfiable or both are not. E ...
but not
equivalent
Equivalence or Equivalent may refer to:
Arts and entertainment
*Album-equivalent unit, a measurement unit in the music industry
* Equivalence class (music)
*'' Equivalent VIII'', or ''The Bricks'', a minimalist sculpture by Carl Andre
*''Equiva ...
.
An alternative translation, the
Tseitin transformation The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces a boolean formula in conjunctive normal form (CNF), which can be solved by a CNF-SAT solver. The leng ...
, 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 mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically ...
.
In resolution-based automated theorem-proving, a CNF formula
See
below for an example.
Computational complexity
An important set of problems in
computational complexity 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
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
is
NP-complete
In computational complexity theory, a problem is NP-complete when:
# it is a problem for which the correctness of each solution can be verified quickly (namely, in polynomial time) and a brute-force search algorithm can find a solution by trying ...
(like any other ''k''-SAT problem with ''k''>2) while
2-SAT is known to have solutions in
polynomial time. 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] the task of converting a formula into a
DNF, preserving satisfiability, is
NP-hard;
dually Dually may refer to:
*Dualla, County Tipperary, a village in Ireland
*A pickup truck with dual wheels on the rear axle
* DUALLy, s platform for architectural languages interoperability
* Dual-processor
See also
* Dual (disambiguation)
Dual or ...
, converting into CNF, preserving
validity
Validity or Valid may refer to:
Science/mathematics/statistics:
* Validity (logic), a property of a logical argument
* Scientific:
** Internal validity, the validity of causal inferences within scientific studies, usually based on experiments
** ...
, 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 for ...
.
## 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
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 mathem ...
. 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,