Computer Science ›› 2018, Vol. 45 ›› Issue (12): 137-141.doi: 10.11896/j.issn.1002-137X.2018.12.021
• Artificial Intelligence • Previous Articles Next Articles
CHEN Qing-shan1,2, XU Yang2, WU Guan-feng1,2
CLC Number:
[1]COOK S A.The complexity of theorem-proving procedures [C]∥3rd Annual ACM Symposium on Theory of Computing.New York:ACM,1971:151-158. [2]BIERE A,HEULE M,VAN MAAREN H,et al.Conflict-driven clause learning SAT solvers [M]∥Handbook of Satisfiability,Frontiers in Artificial Intelligence and Applications.Amsterdam:IOS Press,2009:131-153. [3]VAN DER TAK P,RAMOS A,HEULE M.Reusing the assignment trail in cdcl solvers [J].Journal on Satisfiability,Boolean Modeling and Computation,2011,7(4):133-138. [4]SILVA J P M,SAKALLAH K A.GRASP—a new search algorithm for satisfiability [C]∥Proceedings of the 1996 IEEE/ACM International Conference on Computeraided Design.Los Alamitos:IEEE Computer Society Press,1996:220-227. [5]BAYARDO J R R J,SCHRAG R.Using CSP look-back techniques to solve real-world SAT instances [C]∥Proceedings of the 14th National Conference on Artificial Intelligence.Menlo Park:AAAI Press,1997:203-208. [6]MOSKEWICZ M W,MADIGAN C F,ZHAO Y.Chaff:Engi-neering an efficient SAT solver[C]∥Proceedings of the 38th Annual Design Automation Conference.New York:ACM,2001:530-535. [7]GOLDBERG E,NOVIKOV Y.BerkMin:A Fast and RobustSat-Solver [C]∥Proceedings of the Conference on Design,Automation and Test in Europe (DATE 2002).Los Alamitos:IEEE Computer Society Press,2002:142-149. [8]SÖRENSSONN,EÉN N.MiniSat v1.13-A SAT solver withconflict-clause minimization [C]∥Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing.Berlin:Springer,2005:502-518. [9]SIMON L,AUDEMARD G.Predicting learnt clauses quality in modern sat solver [C]∥Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09).Menlo Park:AAAI Press,2009:399-404. [10]AUDEMARD G,LAGNIEZ J-M,MAZURE B,et al.On free-zing and reactivating learnt clauses [C]∥Proceedings of the International Conference on Theory and Applications of Satisfia-bility Testing.Berlin:Springer,2011:188-200. [11]GUO L,JABBOUR S,LONLAC J,et al.Diversification by clauses deletion strategies in portfolio parallel SAT solving [C]∥Proceedings of 2014 IEEE 26th International Conference on Tools with Artificial Intelligence (ICTAI 2014).Los Alamitos:IEEE Computer Society Press,2014:701-708. [12]JABBOUR S,LONLAC J,SAIS L,et al.Revisiting the learned clauses database reduction strategies [OL]. [2016-10-20].https://arxiv.org/pdf/1402.1956. [13]ANSÓTEGUI C,GIRÁLDEZ-CRU J,LEVY J,et al.Usingcommunity structure to detect relevant learnt clauses [C]∥Proceedings of the International Conference on Theory and Applications of Satisfiability Testing.Switzerland:Springer,2015:238-254. [14]LONLAC J,NGUIFO E M.Towards Learned Clauses Database Reduction Strategies Based on Dominance Relationship[OL]. [2016-10-20].https://arxiv.org/pdf/1705.10898. [15]LUBY M,SINCLAIR A,ZUCKERMAN D.Optimal speedup of Las Vegas algorithms [J].Information Processing Letters,1993,47(4):173-180. |
[1] | LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112. |
[2] | WANG Yi-jie, XU Yang, WU Guan-feng. Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver [J]. Computer Science, 2021, 48(11): 294-299. |
[3] | TANG Lei-ming, BAI Mu-chen, HE Xing-xing, LI Xing-yu. Complete Contradiction and Smallest Contradiction Based on Propositional Logic [J]. Computer Science, 2020, 47(11A): 83-85. |
[4] | LIU Ting, XU Yang, CHEN Xiu-lan. Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic [J]. Computer Science, 2019, 46(8): 255-259. |
[5] | CHEN Cheng, PAN Zheng-hua and LV Yong-xi. Fuzzy Modal Propositional Logic with Three Kinds of Negation [J]. Computer Science, 2017, 44(4): 263-268. |
[6] | XU Wei, LI Xiao-fen and LIU Duan-yang. Propositional Logic-based Association-rule Mining Algorithm L-Eclat [J]. Computer Science, 2017, 44(12): 211-215. |
[7] | CHEN Qing-shan, XU Yang, WU Guan-feng and HE Xing-xing. Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver [J]. Computer Science, 2017, 44(11): 279-283. |
[8] | WU Xiao-gang and PAN Zheng-hua. Fuzzy Reasoning and its Application Based on Fuzzy Propositonal Logic [J]. Computer Science, 2015, 42(Z11): 100-103. |
[9] | LIU Yi, XU Yang and JIA Hai-rui. Notes on Multi-ary α-Resolution Principle Based on Lattice-valued Logical System LP(X) [J]. Computer Science, 2015, 42(4): 249-252. |
[10] | GHANG Jia-feng,XU Yang,HE Xing-xing. Lattice-valued Semantic Resolution Reasoning Method [J]. Computer Science, 2011, 38(9): 201-203. |
[11] | LIU Hong-lan,GAO Qing-sh,YANG Bing-ru. Set Algebra is Semantic Interpretation for Classical Formal System of Propositional Calculus [J]. Computer Science, 2010, 37(9): 194-197. |
[12] | TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing. Solving Einstein's Puzzle with SAT [J]. Computer Science, 2010, 37(5): 184-186. |
[13] | . [J]. Computer Science, 2008, 35(9): 230-232. |
|