×

Algorithms for selective enumeration of prime implicants. (English) Zbl 0996.68181

Summary: 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 \(\Psi'\) (not necessarily a prime one), and then generating a prime implicant implied by \(\Psi'\). 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
90C10 Integer programming

Keywords:

CNF formulae
PDF BibTeX XML Cite
Full Text: DOI