A MATRIX-METHOD OF COMPUTATION OF PRIME IMPLICATES OF PROPOSITIONAL FORMULA IN CNF

摘要: AK SHINY, ARINDAMA SINGH, ARUN K. PUJARI School of Mathematics and Computer/Information Sciences, University of Hyderabad, Hyderabad-500 134, India Tel.: 253901, ext 4105, Telex: 425-2050, UHYD IN; Fax: 91-842-253145In this paper, an efficient recursive algorithm to compute the set of prime implicates of a propositional formula in Conjunctive Normal Form (CNF) is presented. Once a binary matrix representation of a formula is obtained, the algorithm finds the prime implicates as prime paths through the matrix. The proposed algorithm is easily adaptable to the case where an earlier formula is updated by a set of clauses, without recomputing prime paths for the updated formula.