An algorithm for the satisfiability problem
Robert Arlin Pilgrim · 1992
There is a wealth of information covering the class of problems known as non-deterministic polynomial-time (NP), most of which is concerned with theoretical issues of how to recognize when a problem is in the class NP or how to transform one NP problem into another. The issue of what to do when you must solve a problem which happens to be a member of the NP class, has not been addressed as completely. This work demonstrates a method of developing an algorithm to solve NP class problems within specified constraints of problem size and finite processing resources. The well-known NP-complete problem called the satisfiability (SAT) problem was selected for this study. A class of the SAT problems is introduced which is randomly generated under certain constraints to ensure a valid test set. A new algorithm called the Solution-Set-Enumeration (SSE) algorithm is introduced which is based on compact enumeration of the solution space. A proof is given for determining when particular SAT problems are members of the class solvable by SSE in polynomial time. Finally the performance of the SSE algorithm is compared with other SAT algorithm against random problems as described above and is shown to provide superior performance for a broader problem class than that covered by our proof.