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

doi:10.11896/jsjkx.221000251

Abstract

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

CLC Number:

TP181

HUANG Pei, LIU Minghao, MA Feifei, ZHANG Jian. Automated Reasoning Techniques for Solving Combinatorial Mathematical Problems:A Survey[J].Computer Science, 2023, 50(7): 167-175.

References

[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.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

Comments

Recommended 0

No Suggested Reading articles found!

Automated Reasoning Techniques for Solving Combinatorial Mathematical Problems:A Survey

PDF (PC)

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 0

[1]	WANG Dongli, YANG Shan, OUYANG Wanli, LI Baopu, ZHOU Yan. Explainability of Artificial Intelligence:Development and Application [J]. Computer Science, 2023, 50(6A): 220600212-7.
[2]	WANG Zihan, TONG Xiangrong. Research Progress of Multi-agent Path Finding Based on Conflict-based Search Algorithms [J]. Computer Science, 2023, 50(6): 358-368.
[3]	XING Ying. Review of Software Engineering Techniques and Methods Based on Explainable Artificial Intelligence [J]. Computer Science, 2023, 50(5): 3-11.
[4]	ZHANG Qiyang, CHEN Xiliang, CAO Lei, LAI Jun, SHENG Lei. Survey on Knowledge Transfer Method in Deep Reinforcement Learning [J]. Computer Science, 2023, 50(5): 201-216.
[5]	ZHANG Qiyang, CHEN Xiliang, ZHANG Qiao. Sparse Reward Exploration Method Based on Trajectory Perception [J]. Computer Science, 2023, 50(1): 262-269.
[6]	LI Ye, CHEN Song-can. Physics-informed Neural Networks:Recent Advances and Prospects [J]. Computer Science, 2022, 49(4): 254-262.
[7]	LI Sun, CAO Feng, LIU Zi-shan. Study on Quality Evaluation Method of Speech Datasets for Algorithm Model [J]. Computer Science, 2022, 49(11A): 210800246-6.
[8]	ZHAO Hong, CHANG You-kang, WANG Wei-jie. Survey of Adversarial Attacks and Defense Methods for Deep Neural Networks [J]. Computer Science, 2022, 49(11A): 210900163-11.
[9]	WANG Lu, WEN Wu-song. Study on Distributed Intrusion Detection System Based on Artificial Intelligence [J]. Computer Science, 2022, 49(10): 353-357.
[10]	CHAO Le-men, YIN Xian-long. AI Governance and System:Current Situation and Trend [J]. Computer Science, 2021, 48(9): 1-8.
[11]	BAO Yu-xuan, LU Tian-liang, DU Yan-hui, SHI Da. Deepfake Videos Detection Method Based on i_ResNet34 Model and Data Augmentation [J]. Computer Science, 2021, 48(7): 77-85.
[12]	JING Hui-yun, WEI Wei, ZHOU Chuan, HE Xin. Artificial Intelligence Security Framework [J]. Computer Science, 2021, 48(7): 1-8.
[13]	XIE Chen-qi, ZHANG Bao-wen, YI Ping. Survey on Artificial Intelligence Model Watermarking [J]. Computer Science, 2021, 48(7): 9-16.
[14]	JING Hui-yun, ZHOU Chuan, HE Xin. Security Evaluation Method for Risk of Adversarial Attack on Face Detection [J]. Computer Science, 2021, 48(7): 17-24.
[15]	QIN Zhi-hui, LI Ning, LIU Xiao-tong, LIU Xiu-lei, TONG Qiang, LIU Xu-hong. Overview of Research on Model-free Reinforcement Learning [J]. Computer Science, 2021, 48(3): 180-187.