Algorithms for selective enumeration of prime implicants

摘要

We present a new approach for selective enumeration of prime implicants of CNF formulae. The method uses a 0–1 programming schema, having feasible solutions corresponding to prime implicants. Prime implicants are generated one at a time, so that as many of them can be computed as needed by the specific application considered. Selective generation is also supported, whereby preferences on the structure of generated prime implicants can be specified. We present two algorithms for selective enumeration of prime implicants and discuss their properties. The former amounts to solving the basic 0–1 programming schema first, to obtain an implicant ψ′ (not necessarily a prime one), and then generating a prime implicant implied by ψ′. The latter is based on adding a suitable minimization function to the basic 0–1 programming schema so that finding optimal solutions corresponds one-to-one to generating prime implicants of the original theory. We show that the latter algorithm has wider applicability but is less efficient than the former one. Finally we present experimental results, which confirm the effectiveness of our approach in computing prime implicants of CNF formulae.