Conjunctive normal form
|
|
In Boolean logic, Conjunctive Normal Form (CNF) is a method of standardizing and normalizing logical formulas. As a normal form, it is useful in automated theorem proving. It is similar to the canonical sum of products form used in circuit theory. A logical formula is considered to be in CNF if and only if it is a single conjunction of one or more disjunctions of one or more literals. Thus all simple conjunctions are in CNF, but also all simple disjunctions are degenerately in CNF as they are a conjunction of a single clause. As in Disjunctive Normal Form, the only propositional operators in CNF are and, 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. For example, all of the following formulas are in CNF:
- <math>A \wedge B<math>
- <math>\neg A \wedge (B \vee C)<math>
- <math>(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)<math>
- <math>(\neg B \vee C).<math>
But the following are not:
- <math>\neg (B \vee C)<math>
- <math>(A \wedge B) \vee C<math>
- <math>A \wedge (B \vee (D \wedge E)).<math>
The above three formulas are respectively equivalent to the following three formulas that are in conjunctive normal form:
- <math>\neg B \wedge \neg C<math>
- <math>(A \vee C) \wedge (B \vee C)<math>
- <math>A \wedge (B \vee D) \wedge (B \vee E).<math>
Converting a formula to CNF involves using logical equivalences, such as the Double Negative Law, De Morgan's laws, and the Distributive Law. Note that all logical formulas can be converted into conjunctive normal form through repeated application of the distributive law of disjunction over conjunction, thus when making proofs on formulas or on the structure of formulas it is often convenient to assume that everything is in CNF. However, in some cases conversion to CNF can lead to an exponential explosion of the formula. For example, in CNF form, logical formulas of the following form have 2n terms:
- <math>(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n).<math>
Conjunctive normal form can be taken further to yield the clausal normal form of a logical formula, that is used to perform first-order resolution.
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. 3-SAT is the problem of finding a satisfying assignment to a boolean formula expressed in CNF such that each disjunction contains at most 3 variables. This has been shown to be NP-complete. The corresponding 2-SAT problem however can be solved in linear time.