Experimental Study on Strategy of CombiningSAT Algorithms

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 algorithms all have their own hard instances respectively.Therefore,to get the better performance on all kinds of problems,SAT solver should know how to select different algorithms according to the feature of instances.In this paper the differences of several effective SAT algorithms are analyzed and two new parameters φand δ are proposed to characterize the feature of SAT instances.Experiments are performed to study the relationship between SAT algorithms and some statistical parameters including φ，δ.Based on this analysis,a strategy is presented for designing a faster SAT tester by carefully combining some existing SAT algorithms.With this strategy,a faster SAT tester to solve many kinds of SAT problem is obtained.

Experimental study on strategy of combining SAT algorithms

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 algorithms all have their own hard instances respectively. Therefore, to get the better performance on all kinds of problems, SAT solver should know how to select different algorithms according to the feature of instances. In this paper the differences of several effective SAT algorithms are analyzed and two new parameters ϕ and δ are proposed to characterize the feature of SAT instances. Experiments are performed to study the relationship between SAT algorithms and some statistical parameters including ϕ, δ. Based on this analysis, a strategy is presented for designing a faster SAT tester by carefully combining some existing SAT algorithms. With this strategy, a faster SAT tester to solve many kinds of SAT problem is obtained. Lu Weifeng received the Ph.D. degree in computer science from Beijing University of Aeronautics and Astronautics. His SAT algorithm won the Silver Award of The Third International SAT Competition'96 in Beijing. His research interests are SAT algorithms, algorithm optimization, knowledgebase maintenance, and intelligent agents. Zhang Yuping is an Associate Professor. His research interests include mathematical logics, SAT algorithms, NP-hard problem, and approximation algorithms.