Solving 3-SAT using constraint programming and fail detection

Propositional satisfiability problem (SAT) is a well-known NP-complete problem. It can be categorized as NP-complete because it has a phase transition point between satisfiable or unsatisfiable. Instances within the phase transition region are hard to solve. To reduce computation time in this region, we designed and implemented a Fail Detection (FD) technique in solving 3-SAT. To simplify implementation procedure, constraint programming is used as the core of the solver because a set of utility is already well developed. As we concern about the robustness of our technique, a large-scale experiment with wide spectrum of random generated 3-SAT instances as test cases is run. To figure out the efficiency of our technique, existing approaches such as Davis-Putnam procedure (DP) and Jeroslow-Wang heuristic used in Davis-Putnam procedure (DP+JW) are tested together with Fail Detection technique (i.e., DP+FD and DP+JW+FD) using the same set of random generated uniform 3-SAT instances. Statistical results show that our DP+JW+FD approach is able to gain up to 63% reduction in computation complexity compare with DP and the effect of hard problem in phase transition region is also significantly reduced.