Canonical normal form

from Wikipedia, the free encyclopedia

A propositional formula is the canonical normal form ( CNF , not to be confused with " conjunctive normal form " (also CNF); English: canonical normal form ) to another propositional formula, if it

  • is a normal form of this propositional formula, d. H. a propositional formula equivalent to this formula, which is subject to certain syntactic restrictions and
  • is identical and unique for equivalent propositional formulas.

Examples

  • Disjunctive normal forms are generally not canonical, but the maximum or extended disjunctive normal form (a disjunctive normal form that only contains minterms in which all variables are present, each variable occurs exactly once and whose minterms are all different from one another) is canonical
  • Conjunctive normal forms are generally not canonical, but the maximum or extended conjunctive normal form (a conjunctive normal form that only contains maxterms in which all variables are present, each variable occurs exactly once and whose maxterms are all different from each other) is canonical
  • The all-round normal form (also called Reed-Muller normal form) is canonical
  • For a fixed order of variables, the reduced Shannon normal form is canonical (use of the Shannon decomposition for a fixed order of variables and subsequent elimination of redundant sub-formulas). This property is important, for example, in binary decision diagrams (BDDs), which are based on the Shannon decomposition: Boolean operations on reduced ordered BDDs (ROBDDs) always preserve the canonical normal form of such diagrams.

Possible applications

In order to show the equivalence of two propositional formulas and , both formulas can be evaluated with all possible interpretations ; if all interpretations deliver the same Boolean value for both formulas, both formulas are equivalent.

Alternatively, both formulas can also be transformed into canonical normal forms KNF ( ) and KNF ( ); Both formulas are equivalent if and only if KNF ( ) = KNF ( ).

In addition, questions regarding the satisfiability and general validity of a formula can be answered with the help of canonical normal forms: a propositional formula can be fulfilled if and only if CNF ( ) CNF (0) and is generally valid if and only if CNF ( ) = CNF (1).

Size of canonical normal forms

It is true that an exponential blow-up is inherent in canonical normal forms ; that is, a canonical normal form is generally exponentially larger than the propositional formula that is converted into such a form; This means the Aufzählungstheorem of Claude Shannon :

Let a (n) be the number of those propositional formulas with n variables whose canonical normal form is only polynomially larger, then this number is offset by the number of all possible Boolean functions B (n) with n variables, which is. Then: .

It follows that most canonical normal forms are exponentially longer than any propositional formula that is converted into one; In particular, the probability that a propositional formula can only be transformed into an exponentially longer canonical normal form increases with the number of variables involved; Because of this, it is also not possible to solve the satisfiability problem of propositional logic with the help of canonical normal forms deterministically with a polynomial expenditure of time.

Different canonical normal forms can behave differently in terms of their size for a certain propositional formula: For example, the canonical disjunctive normal form for the so-called parity function is exponentially longer than , whereas the length of the Reed-Muller normal form only increases polynomially as it increases n.