Doesn't equivalence checking normally use BDDs, and SAT solving normally use separate AND, OR, and NOT? I mean the algorithm to reduce an expression to CNF is a pretty simple set of local rewrite rules with AND, OR, and NOT; I could be wrong but I feel like the NAND-based equivalent of CNF is quite a bit hairier.

As for minimizing combinational logic, don't you want to use the full set of gates available to you in that case, taking into account their cost, and maybe trying to minimize or at least limit circuit depth? It seems like just using NAND would be kind of a step backwards in that case. Karnaugh maps give you DNF; PALs/GALs want DNF; the fact that your DNF PAL circuit might just be two layers of NAND (equivalent to a layer of AND feeding into an OR layer) is kind of an implementation detail, isn't it? I mean you would configure the circuit in the exact same way if it were made out of physical AND and OR gates.