Conjunctive normal form

Conjunctive normal form

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 product of sums 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 in the disjunctive normal form (DNF), 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.

Contents

Examples and counterexamples

All of the following formulas are in CNF:

\neg A \wedge (B \vee C)
(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)
A \or B
A \wedge B.

The last formula is in CNF because it can be seen as the conjunction of the two single-literal clauses A and B. Incidentally, this formula is also in disjunctive normal form. The following formulae are not in CNF:

\neg (B \vee C)
(A \wedge B) \vee C
A \wedge (B \vee (D \wedge E)).

The above three formulae are respectively equivalent to the following three formulas that are in CNF:

\neg B \wedge \neg C
(A \vee C) \wedge (B \vee C)
A \wedge (B \vee D) \wedge (B \vee E).

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 equivalences: the double negative law, De Morgan's laws, and the distributive law.

Since all logical formulae 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 2n clauses:

(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n).

In particular, the generated formula is:

(X_1 \vee \cdots \vee X_{n-1} \vee X_n) \wedge 
(X_1 \vee \cdots \vee X_{n-1} \vee Y_n) \wedge
\cdots \wedge
(Y_1 \vee \cdots \vee Y_{n-1} \vee Y_n).

This formula contains 2n clauses; each clause contains either Xi or Yi for each i.

There exist transformations into CNF that avoid an exponential increase in size by preserving satisfiability rather than equivalence.[1][2] 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 Z_1,\ldots,Z_n as follows:

(Z_1 \vee \cdots \vee Z_n) \wedge
(\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge
\cdots \wedge 
(\neg Z_n \vee X_n) \wedge (\neg Z_n \vee Y_n).

An interpretation satisfies this formula only if at least one of the new variables is true. If this variable is Zi, then both Xi and Yi 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 Zi 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 includes also the clauses Z_i \vee \neg X_i \vee \neg Y_i. With these clauses, the formula implies Z_i \equiv X_i \wedge Y_i; this formula is often regarded to "define" Zi to be a name for X_i \wedge Y_i.

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.

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 such that 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.

Typical problems in this case involve formulas in "3CNF" form: conjunctive normal form with no more than 3 variable per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts.

Converting from first-order logic

To convert first-order logic to CNF:[3]

  1. Convert to negation normal form.
    1. Eliminate implications: convert x \rightarrow  y to \neg x \vee y
    2. Move NOTs inwards by repeatedly applying DeMorgan's Law. Specifically, replace \neg (x \vee y) with (\neg x) \wedge (\neg y); replace \neg (x \wedge y) with (\neg x) \vee (\neg y); and replace \neg\neg x with x.
  2. Standardize variables
    1. For sentences like (∀x P(x)) ∨ (∃x Q(x)) which use the same variable name twice, change the name of one of the variables. This avoids confusion later when we drop the quantifiers.
    2. From ∀x [∃y Animal(y) ∧ ¬Loves(x, y)] ∨ [∃y Loves(y, x)]. we obtain: ∀x [∃y Animal(y) ∧ ¬Loves(x, y)] ∨ [∃z Loves(z,x)].
  3. Skolemize the statement
    1. ∃x P(x) into P(A), where A is a new constant (consult linked article for more details)
  4. Drop universal quantifiers
  5. Distribute ORs over ANDs.

Notes

  1. ^ Tseitin (1968)
  2. ^ Jackson and Sheridan (2004)
  3. ^ Artificial Intelligence: A modern Approach [1995...] Russel and Norvig

See also

References

  • Paul Jackson, Daniel Sheridan: Clause Form Conversions for Boolean Circuits. In: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, pp. 183–198
  • G.S. Tseitin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian), pp. 115–125. Steklov Mathematical Institute (1968)

External links


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • conjunctive normal form — noun The form of a boolean formula that the formula has if the formula is a conjunction of disjunctions of literals, such as (A or B or C) and (D or E or not F) …   Wiktionary

  • Normal form — may refer to: Normal form (abstract rewriting) Normal form (databases) Normal form (game theory) Normal form (mathematics) In formal language theory: Beta normal form Chomsky normal form Greibach normal form Kuroda normal form Normal form… …   Wikipedia

  • normal form — A well formed formula of the propositional calculus is in conjunctive normal form when it is of the form A & B &…where each of A, B…is a formula consisting of a disjunction of atomic propositions or negations of atomic propositions (e.g. p ∨q ∨ ¬ …   Philosophy dictionary

  • Disjunctive normal form — In boolean logic, a disjunctive normal form (DNF) is a standardization (or normalization) of a logical formula which is a disjunction of conjunctive clauses. As a normal form, it is useful in automated theorem proving. A logical formula is… …   Wikipedia

  • Clausal normal form — The clausal normal form (or clause normal form, conjunctive normal form, CNF) of a logical formula is used in logic programming and many theorem proving systems. A formula in clause normal form is a set of clauses, interpreted as a conjunction. A …   Wikipedia

  • Negation normal form — A logical formula is in negation normal form if negation occurs only immediately above elementary propositions, and { } are the only allowed Boolean connectives. In classical logic each formula can be brought into this form by replacing… …   Wikipedia

  • Algebraic normal form — In Boolean logic, the algebraic normal form (ANF) is a method of standardizing and normalizing logical formulas. As a normal form, it can be used in automated theorem proving (ATP), but is more commonly used in the design of cryptographic random… …   Wikipedia

  • Skolem normal form — A formula of first order logic is in Skolem normal form (named after Thoralf Skolem) if it is in conjunctive prenex normal form with only universal first order quantifiers. Every first order formula can be converted into Skolem normal form while… …   Wikipedia

  • Conjunctive query — In database theory, a conjunctive query is a restricted form of first order queries. A large part of queries issued on relational databases can be written as conjunctive queries, and large parts of other first order queries can be written as… …   Wikipedia

  • Canonical form (Boolean algebra) — In Boolean algebra, any Boolean function can be expressed in a canonical form using the dual concepts of minterms and maxterms. Minterms are called products because they are the logical AND of a set of variables, and maxterms are called sums… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”