Computer Science ›› 2019, Vol. 46 ›› Issue (11A): 19-22.
• Intelligent Computing • Previous Articles Next Articles
WANG Meng, HE Xing-xing
CLC Number:
[1]王国俊.数理逻辑引论与归结原理[M].北京:科学出版社,2007:23-24. [2]COOK S A.The complexity of theorem proving procedures[C]∥Proceedings of the ACM SymPosium on Theory of Computin.Shaker Heights,1971:151-158. [3]SILVA J P M,SAKALLAH K A.GRASP:a new search algorithm for satisfiability[C]∥Proceedings of the IEEE/ACM International Conference on Computer-Aided Design.Los Alamitos,2002:220-227. [4]JEROSLOW R G,WANG J.Solving propositional satisfiability problems[J].Annals of Mathematics and Artificial Intelligence,1990,1(1/2/3/4):167-187. [5]FREEMAN J W.Improvements to propositional satisfiability search algorithms[D].Philadelphia:University of Pennsylvania,1995. [6]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A new search algorithm for satisfiability[C]∥International Conference on Computer Aided Design.1996:220-227. [7]MOSKEWICZ M W,MADIGAN C F,ZHAO Y,et al.Chaff:engineering an efficient SAT solver[C]∥Proceedings of the 38th Design Automation Conference.New York:ACM,2001:530-535. [8]LIANG J H,GANESH V,POUPART P,et al.Learning rate based branching heuristic for SAT solvers[C]∥Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing(SAT 2016).2016:123-140. [9]AUDEMARD G,SIMON L.Predicting learnt clauses quality in modern SAT solvers[C]∥Proceedings of the 21st International Joint Conference on Artificial Intelligence(IJCAI 2009).2009:399-404. [10]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A search algorithm for propositional satisfiability[J].IEEETransactions on Computers,1999,48(5):506-521. [11]DAVIS M,LOGEMANN G,LOVELAND D.A machine program for theorem proving[J].Communications of the ACM,1962,59(5):394-397. [12]BURO M,KLEINE-BÜNING H.Report on a SAT competition[J].Bulletin of the European Association for Theoretical Computer Science,1993,5(2):49. [13]MALIK S,ZHAO Y,MADIGAN C F.Chaff:an efficient SAT solver[C]∥Proceedings of the Design Automation Conference.LasVegas,2001:530-535. [14]SELMAN B,KAUTZ H,MCALLESTER D.Ten challenges in propositional reasoning and search[C]∥Proceedings of the 15 the International Conference on Artificial Intelligence.Aichi,1997:50-54. [15]JEROSLOW R G,WANG J.Solving propositional satisfiabilityproblems[J].Annals of Mathematics & Artificial Intelligence,1990,1(1/2/3/4):167-187. [16]MARQUES-SILVA JP,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. [17]GOMES C P,SELMAN B,CRATO N.Heavy-tailed distributions in combinatorial search[C]∥Proceedings of the International Conference on Principles and Practice of Constraint Programming.Linz,1997:121-135. [18]EÉN N,SÖRENSSON N.An Extensible SAT-solver[M]∥Theory and Applications of Satisfiability Testing.Santa Margherita Ligure,2003:502-518. [19]BIERE A,FRÖHLICH A.Evaluating CDCL Variable ScoringSchemes[C]∥International Conference on Theory and Applications of Satisfiability Testing.Cham:Springer,2015:405-422. [20]ZHANG L,MADIGAN C,MOSKEWICZ M,et al.EfficientConflict Driven Lening in a Boolean Satisfiability Slover[C]∥International Conferenceon Computer Aided Sesign (ICCAD).SanJose CA,2001. |
[1] | 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. |
[2] | YANG Jin-cai,XIE Fang and HU Jin-zhu. Research on Rule Engine for Automatic Identification of Relational Words in Chinese Complex Sentences [J]. Computer Science, 2014, 41(Z11): 25-28. |
[3] | . Branch Predictor with TBHBP Based on Simultaneous Multithreaded Processors [J]. Computer Science, 2012, 39(9): 307-311. |
[4] | LI Lin, LU Xian-Liang. Test Pac(}ets Choice Algorithm Aiming at Filter Conflicts [J]. Computer Science, 2011, 38(9): 71-75. |
[5] | GUO Yu-tang. Automatic Image Annotation Method and Fast Solution Based on the Mutual K Nearest Neighbor Graph [J]. Computer Science, 2011, 38(2): 277-280. |
[6] | WU Hai, CHEN Wei, LU Yan-sheng (Computer College, Huazhong University of Science and Technology, Wuhan 430074, China). [J]. Computer Science, 2009, 36(2): 155-157. |
[7] | . [J]. Computer Science, 2008, 35(8): 101-103. |
[8] | GUAN Zhong (Guangzhou City Polytechnic, Guangzhou 510230). [J]. Computer Science, 2007, 34(6): 58-60. |
[9] | WANG Zhan ZHAO Yan-Li LIU Feng-Yu ZHANG Hong (Department of Computer, Nanjing University of Science and Technology, Nanjing 210094). [J]. Computer Science, 2007, 34(12): 265-267. |
[10] | WANG Zhan ,YOU Jing, ZHAO Yan-Li ,LIU Feng-Yu ,ZHANG Hong (Department of Computer, Nanjing University of Science and Technology,Nanjing 210094). [J]. Computer Science, 2006, 33(9): 274-277. |
|