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 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.
As in disjunctive normal form (DNF), the only propositional operators in CNF are or (
The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.
are in conjunctive normal form: The following formulas are not in conjunctive normal form: In classical logic each propositional formula can be converted to an equivalent formula that is in CNF.
[1] This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.
The algorithm to compute a CNF-equivalent of a given propositional formula
in disjunctive normal form (DNF): step 1.
[1] Convert to CNF the propositional formula
Step 1: Convert its negation to disjunctive normal form.
inwards by applying the (generalized) De Morgan's equivalences until no longer possible.
Example Convert to CNF the propositional formula
A CNF equivalent of a formula can be derived from its truth table.
However, in some cases this conversion to CNF can lead to an exponential explosion of the formula.
There exist transformations into CNF that avoid an exponential increase in size by preserving satisfiability rather than equivalence.
[3][4] 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
An interpretation satisfies this formula only if at least one of the new variables is true.
On the other hand, only some of the models of the original formula satisfy this one: since the
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
disjunctions, one for each row of the truth table.In the example below they are underlined.
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 is NP-complete (like any other k-SAT problem with k>2) while 2-SAT is known to have solutions in polynomial time.
As a consequence,[f] the task of converting a formula into a DNF, preserving satisfiability, is NP-hard; 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.
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 for an example.
To convert first-order logic to CNF:[5] Example As an example, the formula saying "Anyone who loves all animals, is in turn loved by someone" is converted into CNF (and subsequently into clause form in the last line) as follows (highlighting replacement rule redexes in