The satisfiability(SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient optimization algorithms for finding a solution for a satisfiable CNF ...The satisfiability(SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient optimization algorithms for finding a solution for a satisfiable CNF formula. A new formulation, the Universal SAT problem model, which transforms the SAT problem on Boofean space into an optimization problem on real space has been developed. Many optimization techniques, such as the steepest descent method, Newton's method, and the coordinate descent method, can be used to solve the Universal SAT 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 coordinate descent method is approximately (1-β/m) for the Universal SAT problem with m variables. An algorithm based on the coordinate descent method for the Universal SAT problem is also presented in this paper.展开更多
For the problem of propositional satisfiability a polynomial algorithm of limited propositional deduction is proposed which can be viewed as a sort of boolean constraint propagation mechanism. It can be embodied in a ...For the problem of propositional satisfiability a polynomial algorithm of limited propositional deduction is proposed which can be viewed as a sort of boolean constraint propagation mechanism. It can be embodied in a backtracking search program for propositional satisfiability problems to make search efficient. The efficiency is gained in two ways:One is to use the algorithm to derive literals so as to overcome the ambiguities in search. The other is to exploit the consequence sets of unbound atoms generated during limited deduction as a heuristic measure for possible choices. The experiments have shown remarkable improvement in reducing search space.展开更多
The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems. Different kinds of SAT algorithmsall have their own hard instances res...The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems. Different kinds of SAT algorithmsall have their own hard instances respectively. Therefore, to get the better performance onall kinds of problems, SAT solver should know how to select different algorithms according tothe feature of instances. In this paper the differences of several effective SAT algorithms areanalyzed and two new parameters gb and & are proposed to characterize the feature of SATinstances. Experiments are performed to study the relationship between SAT algorithms andsome statistical parameters including Φ, δ. Based on this analysis, a strategy is presented fordesigning a faster SAT tester by carefully combining some existing SAT algorithms. With thisstrategy, a faster SAT tester to solve many kinds of SAT problem is obtained.展开更多
基金NSERC Strategic Grant MEF0045793NSERC Research Grant OGP0046423.
文摘The satisfiability(SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient optimization algorithms for finding a solution for a satisfiable CNF formula. A new formulation, the Universal SAT problem model, which transforms the SAT problem on Boofean space into an optimization problem on real space has been developed. Many optimization techniques, such as the steepest descent method, Newton's method, and the coordinate descent method, can be used to solve the Universal SAT 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 coordinate descent method is approximately (1-β/m) for the Universal SAT problem with m variables. An algorithm based on the coordinate descent method for the Universal SAT problem is also presented in this paper.
基金Project supported by the "863" High-Tech Program of China.
文摘For the problem of propositional satisfiability a polynomial algorithm of limited propositional deduction is proposed which can be viewed as a sort of boolean constraint propagation mechanism. It can be embodied in a backtracking search program for propositional satisfiability problems to make search efficient. The efficiency is gained in two ways:One is to use the algorithm to derive literals so as to overcome the ambiguities in search. The other is to exploit the consequence sets of unbound atoms generated during limited deduction as a heuristic measure for possible choices. The experiments have shown remarkable improvement in reducing search space.
文摘The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems. Different kinds of SAT algorithmsall have their own hard instances respectively. Therefore, to get the better performance onall kinds of problems, SAT solver should know how to select different algorithms according tothe feature of instances. In this paper the differences of several effective SAT algorithms areanalyzed and two new parameters gb and & are proposed to characterize the feature of SATinstances. Experiments are performed to study the relationship between SAT algorithms andsome statistical parameters including Φ, δ. Based on this analysis, a strategy is presented fordesigning a faster SAT tester by carefully combining some existing SAT algorithms. With thisstrategy, a faster SAT tester to solve many kinds of SAT problem is obtained.
