Sometimes you'll see the form of CNF and DNF expressed in a notation with subscripts.

- DNF is
*∨*, where each clause_{i}ψ_{i}*φ*is_{i}*∧*, where each_{j}λ_{j}*λ*is a propositional variable (**Prop**), or a negation of one (¬**Prop**). - CNF is
*∧*, where each clause_{i}ψ_{i}*ψ*is_{i}*∨*, where each_{j}λ_{j}*λ*is again a propositional variable (**Prop**), or a negation of one (¬**Prop**).

For example, in the CNF formula (*a* ∨ *b*) ∧ (*¬a* ∨ *b* ∨ *c*) ∧ (*¬a* ∨*¬b*) we have *φ2* = *¬a* ∨ *b* ∨ *c*
within that clause we have *λ _{1}* =

*¬a*.

One question this notation brings up:

- What is the disjunction of a single clause? Well, it's reasonable to say that
*ψ ≡ ψ*. Note that this is also equivalent to*ψ*∨**false**. - What is the disjunction of zero clauses? Well, if we start with
*ψ ≡ ψ*∨**false**and remove the*ψ*, that leaves us with**false**! Alternately, imagine writing a function which takes a list of booleans, and returns the ∨ of all of them the natural base case for this recursive list-processing program turns out to be**false**. Indeed, this is the accepted defnition of the empty disjunction. It follows from false being the identity element for ∨. Correspondingly, a conjunction of zero clauses is true.

Actually, that subscript notation above isn't **quite** correct: it forces each clause to be the same length, which isn't actually required for CNF or DNF. For fun, you can think
about how to patch it up. (Hint: double-subscripting.)

Note that often one of these forms might be more concise than the other. Here are two equivalently verbose ways of encoding true, in CNF and DNF respectively: (*a* ∨*¬a*) ∧
(*b* ∨*¬b*) ∧ ... ∧ (*z* ∨*¬z*) is equivalent to (*a* ∧ *b* ∧ *c* ∧ ... ∧ *y* ∧ *z*) ∨ (*a* ∧ *b* ∧ *c* ∧ ...
∧ *y* ∧*¬z*) ∨ (*a* ∧ *b* ∧ *c* ∧ ... ∧*¬y* ∧ *z*) ∨ ... ∨ (*¬a* ∧*¬b* ∧ ... ∧*¬y* ∧*¬z*). The first version
corresponds to enumerating the choices for each location of a WaterWorld board; it has 26 two-variable clauses. This may seem like a lot, but compare it to the second version, which corresponds
to enumerating all possible WaterWorld boards explicitly: it has all possible 26-variable clauses; there are **2**^{26} ≈ 64
billion of them!

- 瀏覽次數：2255