Sometimes you'll see the form of CNF and DNF expressed in a notation with subscripts.
- DNF is ∨iψi, where each clause φi is ∧j λj , where each λ is a propositional variable (Prop), or a negation of one (¬Prop).
- CNF is ∧iψi, where each clause ψi is ∨jλj , where each λ 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 226 ≈ 64 billion of them!
- 2212 reads
