A randomized algorithm for solving the satisfiability problem

Abstract

In spite of the NP-completeness of the satisfiability decision problem (SAT problem), many researchers have been attracted by it because SAT has many applications in Artificial Intelligence. This paper presents a randomized David-Putnam based algorithm (RSAT) which solves this problem. Instead of selecting the next literal to be set true or false through a heuristic selection rule, RSAT does it through a random algorithm. RSAT not only improves the well-know Davis-Putnam Procedure that has been implemented with a heuristic selection rule, but avoids the incompleteness problem of the local search algorithms as well. RSAT is described in detail and it is compared with the heuristic based Davis-Putnam algorithm HDPP. We discuss the main features of the RSAT implementation and we especially analyze the random number generator features. Although the scope of the experiment is bound by the number of variables, our results indicate that the heuristic can be guessed by a random number generator and even improved. Empirical analysis that support the final conclusions are shown.