What would be a beautiful description for conversion to DNF?
The problem of converting a formula to DNF is easy to explain: Given a boolean formula, write it as a disjunction of conjunctions. For example, $(x \lor y) \land z$ may be rewritten, by distributivity, as $(x \land z) \lor (y \land z)$. The mechanism is also easy to describe: Push $\lnot$ down by de Morgan, then pull $\lor$ above $\land$ by distributivity.
How to turn this description into an algorithm?
I know a nice algorithm for the first half. Expressed in OCaml, it goes
like this: We want a function with the type
type f1 = [`Var of string | `Not of f1 | `And of f1 list | `Or of f1 list] type f2 = [`Pos of string | `Neg of string | `And of f2 list | `Or of f2 list]
The trick is to keep around a parity.
let rec pnd (p : bool) : f1 -> f2 = function | `Var x -> if p then `Pos x else `Neg x | `Not f -> pnd (not p) f | `And fs -> let fs = List.map (pnd p) fs in if p then `And fs else `Or fs | `Or fs -> let fs = List.map (pnd p) fs in if p then `Or fs else `And fs
This algorithm I use when I do boolean manipulations on paper. So I like it. The code is nice, rather than beautiful, because it has some repetition.
What would be a similarly nice solution for the second half—applying
distributivity? Expressed in OCaml, we want a function with the type
type dnf = [`Pos of string | `Neg of string] list list
Of course, I'm interested in solutions in any language.