A Survey of Average Time Analyses of Satisfiability Algorithms

Various algorithms for satisfiability problems require vastly different times to solve typical problems. The time taken to solve random problems is discussed for five algorithms, and the results from asymptotic analyses are surveyed. Plots of the average number of nodes per problem are given for random problems with 50variables. The plots give contours for the number of nodes as a function of the number of clauses and of the probability that a literal is in a clause. They show the strengths and weaknesses of each algorithm.