Enumerating prime implicants of propositional formulae in conjunctive normal form

Abstract

In this paper, a new approach for enumerating the set prime implicants (PI) of a Boolean formula in conjunctive normal form (CNF) is proposed. It is based on an encoding of the input formula as a new one whose models correspond to the set of prime implicants of the original theory. This first PI enumeration approach is then enhanced by an original use of the boolean functions or gates usually involved in many CNF instances encoding real-world problems. Experimental evaluation on several classes of CNF instances shows the feasibility of our proposed framework.