Computing prime implicants by integer programming

An enumerative approach for selective generation of prime implicants of a theory in conjunctive normal form is presented. The method is based on 0-1 programming. Optimal solutions of the integer linear program associated with the theory correspond to prime implicants. All prime implicants can be obtained by augmenting the integer program with new constraints which discard the already obtained solutions. The method allows to implement preference criteria in the choice of the prime implicants to find.