摘要
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.
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.
