Computer Science ›› 2021, Vol. 48 ›› Issue (11): 294-299.doi: 10.11896/jsjkx.201000142
• Artificial Intelligence • Previous Articles Next Articles
WANG Yi-jie, XU Yang, WU Guan-feng
CLC Number:
[1]COOK S A.The complexity of Theorem-Proving Procedures[C]//Proceedings of the 3rd Annual ACM Symposium on Theo-ry of Computing.New York:ACM,1971:151-158. [2]KARP R M.Reducibility Among Combinatorial Problems[M]//Complexity of Computer Conputation.Berlin:Spring US,1972:85-103. [3]HOOS H H,STYUTZLE T.Stochastic Local Search:Foundations & Applications [M]//Access Online Via Elsecier.2004. [4]ROBINSON J A.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of the ACM (JACM),1965,12(1):23-41. [5]DAVIS M,PUTNAM H.A Computing Procedure for Quantification Theory[J].Journal of the ACM(JACM),1960,7(3):201-215. [6]DAVIS M,LOGEMANN G,LOVELAND D.A machine Pro-gram for Theorem Proving[J].Communication of the ACM,1962,5(7):394-397. [7]MARQUES-SILVA J,LYNCE I,MALIK S.Conflict-DrivenClause Learning SAT Solves [M].Amsterdam:IOS Press,2009:127-149. [8]MARQUES-SILVA J,SAKALLAH K.GRASP:A New Search Algorithm for Satisfiability [M]//The Best of ICCAD.New York:Springer,2003:73-89. [9]LUO M,LI C M,XIAO F,et al.An Effective Learnt Clause Mi-nimization Approach for CDCL SAT Solvers[C]//Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence.2017:703-711. [10]SIMON L,AUDEMARD G.Predicting Learnt Clauses in Mo-dern SAT Solver[C]//Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI'09).Menlo Park:AAAI Press,2009:399-404. [11]BIEKE A.Lingeling and Friends Entering the SAT Challenge 2012[C]//Proceedings of SAT Challenge.2012:33-34. [12]GLOUER F,KELLY J P,LAGUNA M.Genetic Algorithmsand Tabu Search:Hybrids for Optimization[J].Computer & Operations Research,1995,22(1):111-134. [13]BURO M,BÜNING H K.Report on a SAT Competition [M]//Fachbereich Math-Informatik.Univ.Gesamthochschule.West Germany,1992. [14]FREEMAN J W.Improvements to Propositional SatisfiabilitySearch Algorithms [D].Philadelphia:University of Pennsylvania,1995. [15]WEIDENBACH C,DIMOVA D,FIETZKE A,et al.SPASSVersion 3.5[C]//CADE.2009:140-145. [16]BIERE A,FROHLICH A.Evaluating CDCL Variable Scoring Schemes[C]//Theory and Applications of Satisfiability Testing-SAT 2015.Switzerland:Springer USA,2015:405-422. [17]RVAN L.Efficient Algorithms for Clause-Learning SAT Sol-vers [D].Vancouver:Simon Fraser University,2004. [18]CHANG W J.Study of Satisfiability Solving Systems and Application Based on Contradiction Separation Based Multiple Dynamic Automated Deduction[D].Chengdu:Southwest Jiaotong University,2019. [19]WANG G J.Introduction to Mathematical Logic and Resolution Principle[M].Beijing:Science Press,2003. [20]CHEN Q S,XU Y,HE X X.Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction[J].Journal of Southwest Jiaotong University,2017,52(6):1224-1232. [21]AUDEMAND G,SIMON L.Predicting Learnt Clauses Quality in Modern SAT Solvers[C]//Proceeding of the 21st International Joint Conference on Artificial.Intelligence.San Francisco,CA:Margan Kaufmann,2009:399-404. |
[1] | XIAO Zhi-hong, HAN Ye-tong, ZOU Yong-pan. Study on Activity Recognition Based on Multi-source Data and Logical Reasoning [J]. Computer Science, 2022, 49(6A): 397-406. |
[2] | XING Yun-bing, LONG Guang-yu, HU Chun-yu, HU Li-sha. Human Activity Recognition Method Based on Class Increment SVM [J]. Computer Science, 2022, 49(5): 78-83. |
[3] | SUN Shan-wu, WANG Nan. Subprocesses Discovery Based on Structure and Activity Semantics [J]. Computer Science, 2021, 48(11A): 659-665. |
[4] | SHEN Xue, CHEN Shu-wei, AI Sen-yang. Reward Mechanism Based Branching Strategy for SAT Solver [J]. Computer Science, 2020, 47(7): 42-46. |
[5] | LIU Jiang, ZHOU Hong-hao. New Algebraic Logic Reduction Method for Boolean Formula [J]. Computer Science, 2020, 47(5): 32-37. |
[6] | ZHANG Chun-xiang, ZHAO Chun-lei, CHEN Chao, LUO Hui. Review of Human Activity Recognition Based on Mobile Phone Sensors [J]. Computer Science, 2020, 47(10): 1-8. |
[7] | LI Juan,FANG Xian-wen,WANG Li-li,LIU Xiang-wei. Chaotic Activity Filter Method for Business Process Based on Log Automaton [J]. Computer Science, 2020, 47(1): 66-71. |
[8] | XU Min-min, KOU Guang-jie, MA Yun-yan, YUE Jun, JIA Shi-xiang, ZHANG Zhi-wang. Color Image Enhancement Algorithm Based on PCNN Internal Activities [J]. Computer Science, 2019, 46(6A): 259-262. |
[9] | CAO Yi-qin, CAO Ting, HUANG Xiao-sheng. Image Fusion Method Based on àtrous-NSCT Transform and Region Characteristic [J]. Computer Science, 2019, 46(6): 270-276. |
[10] | HOU Yu-chen, WU Wei. Design and Implementation of Crowdsourcing System for Still Image Activity Annotation [J]. Computer Science, 2019, 46(11A): 580-583. |
[11] | MAO Yi-ping, YU Lei, GUAN Ze-jin. Multi-focus Image Fusion Based on Fractional Differential [J]. Computer Science, 2019, 46(11A): 315-319. |
[12] | HUANG Jin-guo, LIU Tao, ZHOU Xian-chun, YAN Xi-jun. Detection for Group Riot Activity Based on Change Analysis of Group Motion Pattern [J]. Computer Science, 2018, 45(9): 314-319. |
[13] | YU Ya-xin and ZHANG Hai-jun. Activity Recommendation Algorithm Based on Latent Friendships in EBSN [J]. Computer Science, 2018, 45(3): 196-203. |
[14] | CHEN Qing-shan, XU Yang, WU Guan-feng. Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength [J]. Computer Science, 2018, 45(12): 137-141. |
[15] | WANG Zhong-min, ZHANG Shuang and HE Yan. Selective Ensemble Learning Human Activity Recognition Model Based on Diversity Measurement Cluster [J]. Computer Science, 2018, 45(1): 307-312. |
|