Computer Science ›› 2020, Vol. 47 ›› Issue (7): 42-46.doi: 10.11896/jsjkx.190700191
• Computer Science Theory • Previous Articles Next Articles
SHEN Xue, CHEN Shu-wei, AI Sen-yang
CLC Number:
[1]COOK S.The Complexity of Theorem Proving Procedures[C]//Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing.New York,1971:151-158. [2]MARQUES-SILVA J.Practical Applications of Boolean Satisfi-ability[C]//9th International Workshop on Discrete Event Systems (WODES 2008).IEEE,2008:74-80. [3]XU L,YU J.Improved Bounded Model Checking on Verification of Valid ACTL Properties [J].Computer Science,2013,40(6):99-102. [4]DAVIS M,LOGEMANN G,LOVELAND D.A Machine Pro-gram for Theorem Proving [J].Communications of the ACM,1962,5(5):394-397. [5]MARQUES-SILVA J,LYNCE I,MALIK S.Conflict DrivenClause Learning SAT Solvers[M]//Handbook of Satisfiability.Amsterdam:IOS Press,2009:127-149. [6]MARQUES-SILVA J.The Impact of Branching Heuristics onPropositional Satisfiability Algorithms[C]//Portuguese Confe-rence on Artificial Intelligence.Heidelberg:Springer,1999:62-74. [7]MARQUES-SILVA J,SAKALLAH K.GRASP:A New Search Algorithm for Satisfiability[M]//The Best of ICCAD.New York:Springer,2003:73-89. [8]MALIK S,ZHAO Y,MADIGAN C.Chaff:Engineering an Efficient SAT Solver[C]//Proceedings of the 38th Annual Design Automation Conference.2001:530-535. [9]BIERE A.Adaptive Restart Strategies for Conflict Driven SAT Solvers[C]//Theory and Applications of Satisfiability Testing-SAT 2008.Heidelberg:Springer,2008:28-33. [10]EEN N,SORENSSON N.An Extensible SAT-solver[C]//Theo-ry and Applications of Satisfiability Testing-SAT 2003.Berlin:Springer,2003:502-518. [11]BIERE A,FROHLICH A.Evaluating CDCL Variable ScoringSchemes[C]//Theory and Applications of Satisfiability Testing-SAT 2015.Switzerland:Springer,2015:405-422. [12]王国俊.数理逻辑引论与归结原理[M].北京:科学出版社,2003. [13]张建.逻辑公式的可满足性判断——方法、工具及应用[M].北京:科学出版社,2000:3-28. [14]BIERE A.Lingeling,Plingrling and Treengeling Entering theSAT Competition 2013[C]//Proceedings of SAT Competition.2013:51-52. [15]AUDEMARD G,SIMON L.On the Glucose SAT Solver [J].International Journal on Artificial Intelligence Tools,2018,27(1):18400. [16]LIANG J,GANESH V,POUPAR P,et al.Exponential Recency Weighted Average Branching Heuristic for SAT Solvers[C]//Proceedings of the 13th AAAI Conference on Artificial Intelligence.AAAI Press,2016:3434-3440. [17]LIANG J,GANESH V,POUPAR P,et al.Learning Rate Based Branching Heuristic for SAT Solvers[C]//Theory and Applications of Satisfiability Testing-SAT 2016.Switzerland:Springer,2016:123-140. [18]LIANG J,GANESH V,POUPAR P,et al.An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate[C]//Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing.Melbourne,2017:119-135. [19]CHEN Q S,XU Y X,HE X.Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction [J].Journal of Southwest Jiaotong University,2017,52(6):1224-1232. [20]XIAO F,LI C,LUO M,et al.A Branching Heuristic for SAT Solvers Based on Complete Implication Graphs [J].Science China Information Sciences,2019,62(7):72103. |
[1] | 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. |
[2] | LIU Jiang, ZHOU Hong-hao. New Algebraic Logic Reduction Method for Boolean Formula [J]. Computer Science, 2020, 47(5): 32-37. |
[3] | 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. |
[4] | GUO Ying, ZHANG Chang-sheng and ZHANG Bin. Research Advance of SAT Solving Algorithm [J]. Computer Science, 2016, 43(3): 8-17. |
[5] | WANG Xiao-feng, LI Qiang and DING Hong-sheng. Convergence of Warning Propagation Algorithm for Regular Structure Instances [J]. Computer Science, 2015, 42(1): 279-284. |
[6] | LI Shen,CHANG Liang,MENG Yu and LI Feng-ying. Branching Temporal Description Logic ALC-CTL and its Satisfiability Decision [J]. Computer Science, 2014, 41(3): 205-211. |
[7] | CHANG Liang , WANG Juan,GU Tian-long,DONG Rong-sheng. Tableau Decision Algorithm for the Temporal Description Logic ALC-LTL [J]. Computer Science, 2011, 38(8): 150-154. |
[8] | GU Wen-xiang,HUANG Ping,ZHU Lei,YIN Ming-hao. Research of Phase Transition in Artificial Intelligence [J]. Computer Science, 2011, 38(5): 1-7. |
[9] | GU Wen-xiang,LI Shu-xia,YIN Ming-hao. Research and Development in Backdoor Set [J]. Computer Science, 2010, 37(3): 11-16. |
[10] | . [J]. Computer Science, 2008, 35(5): 220-222. |
|