Abstract
The satisfiability problem is a well known NP-complete problem. In artificial intelligence, solving the satisfiability problem is called mechanical theorem proving. One of those mechanical theorem proving methods is the resolution principle which was invented by J.R. Robinson. In this paper, we shall show how an algorithm based upon the resolution principle can be analyzed. Let n and r 0 denote the numbers of variables and input clauses respectively. Let P 0 denote the probability that a variable appears positively, or negatively, in a clause. Our analysis shows that the expected total number of clauses processed by our algorithm is O(n+r 0 ) if P 0 is a constant, r 0 is polynomially related with n, and n is large. © 1992 J.C. Baltzer A.G. Scientific Publishing Company.