The satisfiability problem (SAT) is a fundamental problem in mathematical logic, constraint satisfaction, VLSI engineering, and computing theory. Methods to solve the satisfiability problem play an important role in the development of computing theory and systems. Traditional methods treat the SAT problem as a constrained decision problem. During past research, the number of unsatisfiable clauses as the value of an objective function was formulated. This transforms the SAT problem into a search problem-an unconstrained optimization problem to the objective function. A variety of iterative optimization techniques can be used to solve this optimization problem. In this paper, the author shows how to use the local search techniques to solve the satisfiability problem. The average time complexity analysis and numerous real algorithm executions were performed. They indicate that the local search algorithms are much more efficient than the existing SAT algorithms for certain classes of conjunctive normal form (CNF) formulas.
展开▼
