Minimization of Boolean functions Given a Boolean function represented in DNF, I am looking for a way to "minimize" its claues, in the sense that each clause contains only the variables it has to. For example, in
$$\phi = a + (b* \tilde a)$$
the second clause can be simply $b$. This is not a minimization in the "regular" sense (reducing the number of clauses). Are there any approaches on this problem?
 A: What you want is a prime cover of the function $\phi$ given a DNF for it.  That is, a cover made of prime implicants.
A classic reference for similar problems is Logic Minimization Algorithms for VLSI Synthesis by Brayton, Hachtel, McMullen, and Sangiovanni-Vincentelli, which deals with your problem as one of the steps in heuristic minimization of DNF (and CNF) covers.
In particular, what you want is to maximally expand each cube in the cover.  In its simplest form, the problem is solved by removing a literal from a term of the DNF and checking whether the result is equivalent to the original  formula, repeating the process until no further improvement is possible.  If there weren't more to the problem, there wouldn't be a book, of course.
The result is order dependent and may contain redundant terms, including duplicates.  From a prime cover one can select a prime and irredundant cover, which has several interesting properties, including the fact that the cheapest DNF cover for $\phi$ under very reasonable assumptions on cost, is a prime and irredundant cover.  (This was first observed by Quine.)
Since selecting a minimum cost set of prime implicants is as hard as minimum set covering, one seldom attempts to find a solution of the true minimum cost.  Prime and irredundant covers are much easier to come by.
For that reason, the local search approach I briefly mentioned above is often preferable to the generation of all prime implicants through some variant of iterated consensus.
At the other hand of the spectrum, CNF SAT solvers, which you can think of as DNF tautology checkers, often adopt a weakened form of simplification, which does not guarantee a prime and irredundant set of clauses, but is quickly applicable to large numbers (e.g., millions) of clauses.
