计算机科学 ›› 2023, Vol. 50 ›› Issue (7): 167-175.doi: 10.11896/jsjkx.221000251

• 人工智能 • 上一篇    下一篇

自动推理技术在求解组合数学难题中的研究进展

黄沛1,3, 刘明昊1,3, 马菲菲2,3, 张健1,3   

  1. 1 中国科学院软件研究所计算机科学国家重点实验室 北京 100190
    2 中国科学院软件研究所并行软件与计算科学实验室 北京 100190
    3 中国科学院大学 北京 100049
  • 收稿日期:2022-10-31 修回日期:2023-03-26 出版日期:2023-07-15 发布日期:2023-07-05
  • 通讯作者: 张健(zj@ios.ac.cn)
  • 作者简介:(huangpei@ios.ac.cn)
  • 基金资助:
    国家自然科学基金(61972384,62132020)

Automated Reasoning Techniques for Solving Combinatorial Mathematical Problems:A Survey

HUANG Pei1,3, LIU Minghao1,3, MA Feifei2,3, ZHANG Jian1,3   

  1. 1 State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China
    2 Laboratory of Parallel Software and Computational Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China
    3 University of Chinese Academy of Sciences,Beijing 100049,China
  • Received:2022-10-31 Revised:2023-03-26 Online:2023-07-15 Published:2023-07-05
  • About author:HUANG Pei,born in 1992,Ph.D.His main research interests include automated reasoning and trustworthy AI.ZHANG Jian,born in 1969,Ph.D,professor,Ph.D supervisor,is a member of China Computer Federation.His main research interests include software engineering and automated reasoning.
  • Supported by:
    National Nature Science Foundation of China(61972384,62132020).

摘要: 自动推理是一种以符号演算的方式来自动模拟人类逻辑推理能力的技术,其总体目标是利用计算机构建一个将不同形式的推理机械化的系统。虽然该领域的理论框架尚未实现对人类全部推理能力的模拟,但该领域的发展已经可以帮助研究人员解决一些数学和逻辑领域的开放性问题,并提供了计算科学中的重要应用。文中简要回顾了利用自动推理技术处理组合数学开放性难题时的代表性方法,重点梳理了该领域的国内外最新进展,分析了各种方法的优势与不足,介绍了近年来出现的增强自动推理结果可信性的技术方法,并探讨了未来的研究方向和面临的挑战。

关键词: 自动推理, 组合数学, 计算逻辑, 人工智能, 符号演算

Abstract: Automated reasoning is a symbolic algorithmic technique that aims to simulate the logical reasoning ability of human.The overall goal is to mechanize different forms of reasoning with a computer system.Although the theoretical framework of the field has not yet supported the simulation of the full range of human reasoning capabilities,developments in the field have reached a point where automated reasoning programs are being used by researchers to attack open problems in mathematics and logic and provide important applications in computing science.This paper briefly reviews common approaches of automatic reasoning in dealing with open problems in combinatorial mathematics and highlights the latest developments in this field in China and abroad.Then the strengths and weaknesses of various approaches are analyzed,and reasoning strategies that have emerged in recent years to enhance the trustworthiness of automated reasoning results are introduced.Finally,future research directions and challenges are discussed.

Key words: Automated reasoning, Combinatorial mathematics, Computational logic, Artificial intelligence, Symbolic calculus

中图分类号: 

  • TP181
[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.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!