Issue No.02 - February (1996 vol.45)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.485373
<p><b>Abstract</b>—The satisfiability (SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient algorithms to find a solution for a satisfiable conjunctive normal form (<it>CNF</it>) formula. A new formulation, the <it>Universal SAT</it> problem model, which transforms the SAT problem on Boolean space into an optimization problem on real space has been developed [<ref rid="bibt020927" type="bib">27</ref>], [<ref rid="bibt020928" type="bib">28</ref>], [<ref rid="bibt020930" type="bib">30</ref>]. Many optimization techniques, such as the steepest descent method, Newton's method, and the coordinate descent method, can be used to solve the <it>Universal SAT</it> problem. In this paper, we prove that, when the initial solution is sufficiently close to the optimal solution, the steepest descent method has a linear convergence ratio β < 1, Newton's method has a convergence ratio of order two, and the convergence ratio of the steepest descent method is approximately (1 −β/<it>m</it>) for the <it>Universal SAT</it> problem with <it>m</it> variables. An algorithm based on the coordinate descent method for the <it>Universal SAT</it> problem is also presented in this paper. Experimental results show that this algorithm is more efficient than some previous ones in finding a solution for certain classes of the satisfiable <it>CNF</it> formulas.</p>
Conjunctive normal form (CNF), satisfiability (SAT) problem, optimization algorithm, nonlinear programming, convergence ratio, time complexity.
Jun Gu, Qian-Ping Gu, Ding-Zhu Du, "Convergence Properties of Optimization Algorithms for the SAT Problem", IEEE Transactions on Computers, vol.45, no. 2, pp. 209-218, February 1996, doi:10.1109/12.485373