交叉口(航空)
计算机科学
自动定理证明
启发式
可满足性
机器学习
领域(数学分析)
人工智能
算法
数学
数学分析
工程类
航空航天工程
标识
DOI:10.1561/9781680838992
摘要
Automated theorem proving represents a significant and long-standing area of research in computer science, with numerous applications. A large proportion of the methods developed to date for the implementation of automated theorem provers (ATPs) have been algorithmic, sharing a great deal in common with the wider study of heuristic search algorithms. However, in recent years researchers have begun to incorporate machine learning (ML) methods into ATPs in an effort to extract better performance. Propositional satisfiability (SAT) solving and machine learning are both large and longstanding areas of research, and each has a correspondingly large literature. In this book, the author presents the results of his thorough and systematic review of the research at the intersection of these two apparently rather unrelated fields. It focusses on the research that has appeared to date on incorporating ML methods into solvers for propositional satisfiability SAT problems, and also solvers for its immediate variants such as and quantified SAT (QSAT). The comprehensiveness of the coverage means that ML researchers gain an understanding of state-of-the-art SAT and QSAT solvers that is sufficient to make new opportunities for applying their own ML research to this domain clearly visible, while ATP researchers gain a clear appreciation of how state-of-the-art machine learning might help them to design better solvers. In presenting the material, the author concentrates on the learning methods used and the way in which they have been incorporated into solvers. This enables researchers and students in both Automated Theorem Proving and Machine Learning to a) know what has been tried and b) understand the often complex interaction between ATP and ML that is needed for success in these undeniably challenging applications.
科研通智能强力驱动
Strongly Powered by AbleSci AI