计算机科学 ›› 2023, Vol. 50 ›› Issue (7): 167-175.doi: 10.11896/jsjkx.221000251
黄沛1,3, 刘明昊1,3, 马菲菲2,3, 张健1,3
HUANG Pei1,3, LIU Minghao1,3, MA Feifei2,3, ZHANG Jian1,3
摘要: 自动推理是一种以符号演算的方式来自动模拟人类逻辑推理能力的技术,其总体目标是利用计算机构建一个将不同形式的推理机械化的系统。虽然该领域的理论框架尚未实现对人类全部推理能力的模拟,但该领域的发展已经可以帮助研究人员解决一些数学和逻辑领域的开放性问题,并提供了计算科学中的重要应用。文中简要回顾了利用自动推理技术处理组合数学开放性难题时的代表性方法,重点梳理了该领域的国内外最新进展,分析了各种方法的优势与不足,介绍了近年来出现的增强自动推理结果可信性的技术方法,并探讨了未来的研究方向和面临的挑战。
中图分类号:
[1]ROBINSON,ALAN J A,VORONKOV A,et al.Handbook of Automated Reasoning[M].Elsevier,2001:17-18. [2]TURING A M.On computable numbers,with an application to the Entscheidungsproblem[J].Journal of Mathematics,1936,42:230-265. [3]COOK S A.The complexity of theorem-proving procedures[C]//Proceedings of the Third Annual ACM Symposium on Theory of Computing.1971:151-158. [4]ARMIN B,HEULE M,MAREN H V,et al.Handbook of satisfiability[M].IOS Press,2009. [5]SMOLENSKY P.Connectionist AI,symbolic AI,and the brain[J].Artificial Intelligence Review,1987,1(2):95-109. [6]KROENING D,STRICHMAN O.Decision procedures[M].Ber-lin:Springer,2016. [7]LUCKHAM D,ROBINSON J A.A Machine-Oriented Logicbased on the Resolution Principle[J].Journal of Symbolic Lo-gic,1966,31(3):515. [8]MOSKEWICZ M W,MADIGAN C F,ZHAO Y,et al.Chaff:Engineering an efficient SAT solver[C]//Proceedings of the 38th annual Design Automation Conference.2001:530-535. [9]BONACINA M P,GRAHAM-LENGRAND S,SHANKAR N.Satisfiability modulo theories and assignments[C]//Interna-tional Conference on Automated Deduction.Cham:Springer,2017:42-59. [10]BOSE R C,SHRIKHANDE S,PARKER E T.Further resultson the construction of mutually orthogonal Latin squares and the falsify of the Euler’s conjecture[J].Canadian Journal of Mathematics,1960,12:189-203. [11]OSMUNDSEN J A.Major mathematical conjecture propounded 177 years ago is disproved:3 mathematicians solve old puzzle[J].The New York Times,1959,26:1. [12]ZHANG J.Constructing finite algebras with FALCON[J].Journal of automated reasoning,1996,17(1):1-22. [13]HASEGAWA R,FUJITA H,KOSHIMURA M,et al.A model generation-based theorem prover MGTP for first-order logic[M]//Computational Logic:Logic Programming and Beyond.Berlin:Springer,2002:178-213. [14]FUJITA M,SLANEY J,BENNETT F.Automatic generation of some results in finite algebra[C]//IJCAI.1993:52-57. [15]SLANEY J.FINDER:Finite domain enumerator system description[C]//International Conference on Automated Deduction.Berlin:Springer,1994:798-801. [16]ZHANG H,STICKEL M.Implementing the davis-putnam me-thod[J].Journal of Automated Reasoning,2000,24(1):277-296. [17]ZHANG H.SATO:An efficient propositional prover[C]//International Conference on Automated Deduction.Berlin:Sprin-ger,1997. [18]MCCUNE W.MACE 2.0 reference manual and guide[J].ar-Xiv:0106042,2001. [19]ZHANG J,ZHANG H.SEM:a system for enumerating models[C]//Proceedings of the 4th International Joint Conference on Artificial Intelligence.1995:298-303. [20]JIA X,ZHANG J.A powerful technique to eliminate isomorphism in finite model search[C]//International Joint Conference on Automated Reasoning.Berlin:Springer,2006:318-331. [21]MCCUNE W.Mace4 reference manual and guide[J].arXiv:0310055,2003. [22]EÉN N,SÖRENSSON N.An extensible SAT-solver[C]//International conference on theory and applications of satisfiability testing.Berlin:Springer,2003:502-518. [23]AUDEMARD G,SIMON L.Predicting learnt clauses quality in modern SAT solvers[C]//Twenty-first International Joint Conference on Artificial Intelligence.2009. [24]HEULE M J H,KULLMANN O,WIERINGA S,et al.Cube and conquer,Guiding CDCL SAT solvers by lookaheads[C]//Haifa Verification Conference.Berlin:Springer,2011:50-65. [25]LAMB E.Two-hundred-terabyte maths proof is largest ever[J].Nature,2016,534(7605). [26]HEULE M.Schur number five[C]//Proceedings of the AAAI Conference on Artificial Intelligence.2018. [27]BRAKENSIEK J,HEULE M,MACKEY J,et al.The Resolution of Keller’s Conjecture[C]//Automated Reasoning:10th International Joint Conference(IJCAR 2020).2020:48-65. [28]ZHANG J.Automatic symmetry breaking method combinedwith SAT[C]//Acm Symposium on Applied Computing.ACM,2001. [29]HUANG P,MA F,GE C,et al.Investigating the existence of large sets of idempotent quasigroups via satisfiability testing[C]//International Joint Conference on Automated Reasoning.Cham:Springer,2018:354-369. [30]CHAR B W,FEE G J,GEDDES K O,et al.A tutorial introduction to Maple[J].Journal of Symbolic Computation,1986,2(2):179-200. [31]WOLFRAM S.The Mathematica Book[M].Wolfram Research,Inc.,2003. [32]STEIN W.Sage:Open Source Mathematical Software[J/OL].The Cloud,2008.https://www.williamstein.org/talks/2010-01-14-ams/2010-01-14-ams-sage/sage-slides.pdf. [33]BOSMA W,CANNON J,PLAYOUST C.The Magma algebrasystem I:The user language[J].Journal of Symbolic Computation,1997,24(3/4):235-265. [34]BRIGHT C,GANESH V,HEINLE A,et al.MathCheck 2:A SAT+CAS verifier for combinatorial conjectures[C]//International Workshop on Computer Algebra in Scientific Computing.Cham:Springer,2016:117-133. [35]BRIGHT C,KOTSIREAS I,HEINLE A,et al.Enumeration of complex Golay pairs via programmatic SAT[C]//Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation.2018:111-118. [36]BRIGHT C,-DOKOVIĆD ,KOTSIREAS I,et al.A SAT+CAS approach to finding good matrices:New examples and counterexamples[C]//Proceedings of the AAAI Conference on Artificial Intelligence.2019:1435-1442. [37]BRIGHT C,CHEUNG K,STEVENS B,et al.UnsatisfiabilityProofs for Weight 16 Codewords in Lam’s Problem[C]//Twenty-Ninth International Joint Conference on Artificial Intelligence and Seventeenth Pacific Rim International Conference on Artificial Intelligence(IJCAI).2020. [38]HUANG P,LIU M,GE C,et al.Investigating the existence of orthogonal golf designs via satisfiability testing[C]//Procee-dings of the 2019 on International Symposium on Symbolic and Algebraic Computation.2019:203-210. [39]MA F F,ZHANG J.Finding orthogonal latin squares using finite model searching tools[J].Science China Information Sciences,2013,56(3):1-9. [40]JIN J,LV Y,GE C,et al.Investigating the existence of costaslatin squares via satisfiability testing[C]//International Confe-rence on Theory and Applications of Satisfiability Testing.Cham:Springer,2021:270-279. [41]DAVIES A,VELIĆKOVIĆ P,BUESING L,et al.Advancing mathematics by guiding human intuition with AI[J].Nature,2021,600(7887):70-74. [42]AOUCHICHE M,HANSEN P.A survey of automated conjectures in spectral graph theory[J].Linear Algebra and Its Applications,2010,432(9):2293-2322. [43]AOUCHICHE M,HANSEN P.Proximity,remoteness and distance eigenvalues of a graph[J].Discrete Applied Mathematics,2016,213:17-25. [44]COLLINS K L.On a conjecture of Graham and Lovász about distance matrices[J].Discrete applied mathematics,1989,25(1/2):27-35. [45]HOGBEN L,REINHART C.Spectra of variants of distance matrices of graphs and digraphs:a survey[J].La Matematica,2022,1(1):186-224. [46]AARONSON J,GROENLAND C,GRZESIK A,et al.Exact hyperplane covers for subsets of the hypercube[J].Discrete Mathe-matics,2021,344(9):112490. [47]APPEL K,HAKEN W.The four-color proof suffices[J].The Mathematical Intelligencer,1986,8(1):10-20. [48]BRUMMAYER R,LONSING F,BIERE A.Automated testing and debugging of SAT and QBF solvers[C]//International Conference on Theory and Applications of Satisfiability Testing.Berlin:Springer,2010:44-57. [49]ZHANG L,MALIK S.Validating SAT solvers using an inde-pendent resolution-based checker,Practical implementations and other applications[C]//2003 Design,Automation and Test in Europe Conference and Exhibition.IEEE,2003:880-885. [50]VAN GELDER A.Verifying RUP Proofs of Propositional Unsatisfiability[C]//International Symposium on Artificial Intelligence and Mathematics.Springer,2008. [51]MANTHEY N,HEULE M J H,BIERE A.Automated reenco-ding of boolean formulas[C]//Haifa Verification Conference.Berlin:Springer,2012:102-117. [52]JÄRVISALO M,HEULE M J H,BIERE A.Inprocessing rules[C]//International Joint Conference on Automated Reasoning.Berlin:Springer,2012:355-370. [53]AUDEMARD G,KATSIRELOS G,SIMON L.A restriction ofextended resolution for clause learning SAT solvers[C]//Twenty-Fourth AAAI Conference on Artificial Intelligence.2010. [54]KULLMANN O.On a generalization of extended resolution[J].Discrete Applied Mathematics,1999,96:149-176. [55]WETZLER N,HEULE M J H,HUNT W A.DRAT-trim:Efficient checking and trimming using expressive clausal proofs[C]//International Conference on Theory and Applications of Satisfiability Testing.Cham:Springer,2014:422-429. [56]SELSAM D,LAMM M,BENEDIKT B,et al.Learning a SAT Solver from Single-Bit Supervision[C]//International Confe-rence on Learning Representations.2018. [57]YOLCU E,PÓCZOS B.Learning local search heuristics forboolean satisfiability[C]//Proceedings of the 33rd International Conference on Neural Information Processing Systems.2019:7992-8003. |
|