Solving SAT problem by heuristic polarity decision-making algorithm

作     者：JING MingE ZHOU Dian TANG PuShan ZHOU XiaoFang ZHANG Hua 

作者机构：State Key Laboratory of ASIC & System Microelectronics Department Fudan University Shanghai201203 China E. E. Department the University of Texas at Dallas TX 75083 USA 

出 版 物：《Science in China(Series F)》 (中国科学（F辑英文版）)

年 卷 期：2007年第50卷第6期

页      面：915-925页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：the National Natural Science Foundation of China (Grant Nos. 90207002, 90307017, 60773125 and 60676018) National Science Foundation (Grant Nos. CCR-0306298) China Postdoctoral Science Foundation (Grant No. KLH1202005) the Natural Science Foundation of Shanghai City (Grant No. 06ZR14016) 

主　　题：SAT problem DPLL complete algorithm decision-making 

摘      要：This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability （SAT）. The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause recording, restarts, etc. In addition, a preconditioning step that calculates the polarities of variables according to the cover distribution of Karnaugh map is introduced into DPLL procedure, which greatly reduces the number of conflicts in the search process. The proposed approach is implemented as a SAT solver named DiffSat. Experiments show that DiffSat can solve many ＂real-life＂ instances in a reasonable time while the best existing SAT solvers, such as Zchaff and MiniSat, cannot. In particular, DiffSat can solve every instance of Bart benchmark suite in less than 0.03 s while Zchaff and MiniSat fail under a 900 s time limit. Furthermore, DiffSat even outperforms the outstanding incomplete algorithm DLM in some instances.