An efficient algorithm for testing propositional formulas

Abstract

The determinant of the Boolean Formulae a = {C1,…,Cm} was introduced in [1]. The present paper gives an algorithm for testing satisfiably propositional formulas. The algorithm based on the enumeration of solutions for testing the satisfiability of propositional formulas has already been given by Kazuo Iwama [2]. The present paper is original by combining this algorithm  with other procedures, especially with the pure-literal rule and the one-literal rule, and also the one which consists in changing any formulas in bounded formulas. The algorithm based on the enumeration of the solution combined to these procedures is more efficient.