Computation of prime implicants using matrix and paths
A. K. Shiny · Journal of Logic and Computation · 1998
In this paper, an efficient algorithm to compute the set of prime implicants of a propositional formula in Conjunctive Normal Form (CNF) is presented. The proposed algorithm uses a concept of representing the formula as a binary matrix and computing paths through the matrix as implicants. The algorithm finds the prime implicants as the prime paths using the divide-and-conquer technique. The proposed algorithm can be used for knowledge compilation, Clause Maintenance Systems where the knowledge base is propositional formulae. Moreover, the algorithm is easily adaptable to the incremental mode of computation where an earlier formula is updated by a set of clauses.