Conjunctive normal form
From Exampleproblems
In Boolean logic, a formula is in Conjunctive Normal Form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals. 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.
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 for the Disjunctive Normal Form, the only propositional connectives a formula in CNF can contain 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:
But the following are not:
The above three formulas are respectively equivalent to the following three formulas that are in conjunctive normal form:
Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: the Double Negative Law, the De Morgan's laws, and the Distributive Law.
Since all logical 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 formula in CNF produces a formula with 2n clauses:
Transformations of formulae in CNF form preserving satisfiability (rather than equivalence) and introducing new variables exist. These transformations are interesting because they are guaranteed not to produce an exponential blow-up.
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.
