AN EFFICIENT ALGORITHM FOR TESTING PROPOSITIONAL FORMULAS

The determinant of the Boolean Formulae alpha = {C-1, ..., C-m} was in troduced in [1]. The present paper gives an algorithm for testing sati sfiably proposition at formulas. The algorithm based on the enumeratio n of solutions for testing the satisfiability of propositional formula s has already been given by Kazuo Iwama [2]. The present paper is orig inal by combining this algorithm with other procedures, especially wit h the pure-literal rule and the one-literal rule, and also the one whi ch consists in changing any formulas in bounded formulas. The algorith m based on the enumeration of the solution combined to these procedure s is more efficient.