A novel approach of solving the CNF-SAT problem

TL;DR

This paper compares two algorithms, PL-Resolution and WalkSAT, for solving the NP-Complete CNF-SAT problem, highlighting their differences in certainty, speed, and practicality.

Contribution

It provides an analysis of the performance and trade-offs between a complete algorithm and a faster, incomplete heuristic for CNF-SAT.

Findings

PL-Resolution is sound and complete for CNF-SAT.

WalkSAT is faster but not guaranteed to find a solution.

WalkSAT performs acceptably on easier problems.

Abstract

In this paper, we discussed CNF-SAT problem (NP-Complete problem) and analysis two solutions that can solve the problem, the PL-Resolution algorithm and the WalkSAT algorithm. PL-Resolution is a sound and complete algorithm that can be used to determine satisfiability and unsatisfiability with certainty. WalkSAT can determine satisfiability if it finds a model, but it cannot guarantee to find a model even there exists one. However, WalkSAT is much faster than PL-Resolution, which makes WalkSAT more practical; and we have analysis the performance between these two algorithms, and the performance of WalkSAT is acceptable if the problem is not so hard.