NationMaster - Encyclopedia: Conjunctive normal form

In boolean logic, a formula is in conjunctive normal form (CNF or 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 product of sums form used in circuit theory. Boolean logic is a complete system for logical operations. ... In mathematics and in the sciences, a formula (plural: formulae, formulÃ¦ or formulas) is a concise way of expressing information symbolically (as in a mathematical or chemical formula), or a general relationship between quantities. ... In logic and declarative programming, a clause is a disjunction of literals and can be interpreted as a (conditional) statement. ... OR logic gate. ... In mathematical logic, a literal is an atomic formula (atom) or its negation. ... The term normal form is used in a variety of contexts. ... Automated theorem proving (ATP) or automated deduction, currently the most well-developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. ... In a Boolean algebra, any Boolean function can be expressed in a canonical form using the dual concepts of minterms and maxterms. ...

All conjunctions of literals and all disjunctions of literals are in CNF, as they can be seen as conjunctions of one-literal clauses and disjunctions 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. In boolean logic, a disjunctive normal form (DNF) is a standardization (or normalization) of a logical formula which is a disjunction of conjunctive clauses. ... AND Logic Gate In logic and mathematics, logical conjunction (usual symbol and) is a two-place logical operation that results in a value of true if both of its operands are true, otherwise a value of false. ... OR logic gate. ... Negation, in its most basic sense, changes the truth value of a statement to its opposite. ... In mathematical logic, a propositional variable (also called a sentential variable) is a variable which can either be true or false. ...

1 Examples and counterexamples
2 Conversion into CNF
3 First-order logic
4 Computational complexity
5 Converting from first-order logic
6 See also
7 External links

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)$

$(neg B vee C)$

$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 formulas are respectively equivalent to the following three formulas that are in conjunctive normal form:

$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, the De Morgan's laws, and the distributive law. In logic, statements p and q are logically equivalent if they have the same logical content. ... In logic, statements p and q are logically equivalent if they have the same logical content. ... In logic and the propositional calculus, double negative elimination is a rule that states that double negatives can be removed from a proposition without changing its meaning: means the same as: Formally: Â¬ Â¬ A âˆ´ A The rule of double negative introduction states the converse, that double negatives can be added without... note that demorgans laws are also a big part in circut design. ... In mathematics, and in particular in abstract algebra, distributivity is a property of binary operations that generalises the distributive law from elementary algebra. ...

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 non-CNF formula in CNF produces a formula with $2 n$ 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)$

In words, this formula contains $2 n$ clauses: in each clause contains either $X i$ or $Y i$ for each $i$ .

Transformations of formulas in CNF preserving satisfiability rather than equivalence and not producing an exponential increase of size exist. These transformations are guaranteed to only linearly increase the size of the formula, but introduce new variables. For example, the above formula can be put in CNF by adding variables $Z_1,ldots,Z_n$ as follows: 3SAT redirects here. ...

$(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 $Z i$ , then both $X i$ and $Y i$ 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 $Z i$ is not mentioned in the original formula, their values is 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. In logic, statements p and q are logically equivalent if they have the same logical content. ...

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" $Z i$ 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. y this The clausal normal form is used in logic programming and many theorem proving systems. ... In mathematical logic and automated theorem proving, a branch of the traditional artificial intelligence (see GOFAI), resolution is a theorem-proving technique for sentences in propositional logic and first-order logic. ...

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 solution in polynomial time. Complexity theory is part of the theory of computation dealing with the resources required during computation to solve a given problem. ... 3SAT redirects here. ... In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use... 2-satisfiability (abbreviated as 2-SAT) is a special case of satisfiability if expressions are written in conjunctive normal form with 2 variables per clause (2-CNF). ... In computational complexity theory, polynomial time refers to the computation time of a problem where the time, m(n), is no greater than a polynomial function of the problem size, n. ...

Converting from first-order logic

To convert first-order logic to CNF:

Convert to Negation normal form. Eliminate implications: convert $x rightarrow y$ to $neg x vee y$
Move NOTs inwards
Standardize variables
Skolemize the statement
Drop universal quantifiers
Distribute ANDs over ORs.

(Artificial Intelligence: A modern Approach [1995...] Russel and Norvig) A logical formula is in negation normal form if negation occurs only immediately above elementary propositions. ...

External links

Scheme and Ocaml programs for converting propositional logic statements into CNF

Categories: Logic stubs | Logic | Boolean algebra

Results from FactBites:

PlanetMath: CNF (68 words)
	A propositional formula is a CNF formula, meaning Conjunctive Normal Form, if it is a conjunction of disjunction of literals (a literal is a propositional variable or its negation).
	Hence, a CNF is a formula of the form:
	This is version 4 of CNF, born on 2003-10-16, modified 2004-03-09.

More results at FactBites »

COMMENTARY

Share your thoughts, questions and commentary here

Want to know more?
Search encyclopedia, statistics and forums:

Feeds | Contact
The Wikipedia article included on this page is licensed under the GFDL.
Images may be subject to relevant owners' copyright.
All other elements are (c) copyright NationMaster.com 2003-5. All Rights Reserved.
Usage implies agreement with terms.

Contents

Examples and counterexamples GA_googleFillSlot("encyclopedia_square");