A novel approach of solving the CNF-SAT problem

2013/07/24 by Xili Wang, Wang, Xili
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.AI #cs.LO

paper · pdf · doi:10.48550/arxiv.1307.6291

arxiv created 2013/07/24 · arxiv updated 2013/07/25

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.

Related

• SAT for pedestrians
• A new algorithm for Solving 3-CNF-SAT problem
• WalkSAT is linear on random 2-SAT
• Further Improvements for SAT in Terms of Formula Length
• An Improved Algorithm for Sparse Instances of SAT