Conjunctive normal form

As a conjunctive normal form ( CNF short, Eng. CNF for conjunctive normal form) is in propositional logic a particular form of formulas called.

Definition

A formula of propositional logic is in conjunctive normal form if it is a conjunction of Disjunktionstermen. Disjunktionsterme are disjunctions of literals. Literals are nichtnegierte or negated variables. A formula in CNF thus has the form

Example:

Canonical conjunctive normal form

A canonical conjunctive normal form ( KKNF ) consists of pairwise distinct Maxtermen. In each of these maxterms every variable exactly once before. Every Boolean function has exactly one KKNF. The KKNF is also called full canonical normal form.

Education

Each formula of propositional logic can be transformed into conjunctive normal form, as well as any Boolean function can be represented by a CNF. It is sufficient to read the lines of its truth table. For each line that supplies a 0 as a result, a clause is formed, which links all the variables of the function disjunctive with the inverted occupancy. The resulting terms are maxterms. Their conjunctive link provides the canonical conjunctive normal form.

This is usually no minimum formula, that is, a formula with a minimum of clauses. If you want to form a minimal formula, so you can do this perhaps with the help of Karnaugh - Veitch - diagrams ( short Karnaugh maps ).

For example for the formation of

Wanted is a formula in CNF for the Boolean function with three variables x2, x1 and x0, the iff the truth value 1 (true) assumes when the binary number [ X2X1X0 ] 2 is a prime number.

The truth table for this function has the following form:

Note: The individual clauses are listed as maxterms. Moreover, one can easily see that each CNF has an equivalent DNF.

Decidability

The question of whether the variables of a propositional formula can be proven that the statement is true, is satisfiability ( SAT short ) called. SAT belongs to the class of NP -complete problems and thus is generally solvable difficult. This also applies to the formulas which are present in CNF; However, with the exception of Horn formulas, which are a special case of CNF - formulas and can be tested in polynomial time to satisfiability. There are basically two approaches, such as propositional logic expression can be checked for satisfiability: by testing all possible assignments of its variables (semantic approach ) or by the resolution calculus ( purely syntactic ).

Other normal forms

In addition to the conjunctive normal form of propositional logic, there are in more normal forms, such as the disjunctive normal form or the negation normal form.