Algorithms for testing satisfiability formulas

The present paper presents algorithms for testing satisfiabily of clausal formulas in the propositional logic and the first-order logic. The algorithm based on the enumeration of solutions for testing the satisfiability of propositional formula, has already been given by K. Iwama, O. Dubois. The originality in this paper is to combine this algorithm to other procedures, especially with the pure-literal literal and the one-literal rule, and also the one which consists in changing any formulas in formulas bounded. The algorithm based on the enumeration of the solution combined to these procedures is more efficient. The algorithm based on the concept of resolutive derivation from Skolem normal form off formula alpha in first-order logic, has already been given. The idea in present's paper is to combined to this algorithm to process of elimination of tautological clauses and process of elimination of subsumed clauses.