Abstract

The decision problem for Boolean satisfiability, generally referred to as SAT, is the archetypal NP-complete problem, and encodings of many problems of practical interest exist allowing them to be treated as SAT problems. Its generalization to quantified SAT (QSAT) is PSPACE-complete, and is useful for the same reason. Despite the computational complexity of SAT and QSAT, methods have been developed allowing large instances to be solved within reasonable resource constraints. These techniques have largely exploited algorithmic developments; however machine learning also exerts a significant influence in the development of state-ofthe- art solvers. Here, the application of machine learning is delicate, as in many cases, even if a relevant learning problem can be solved, it may be that incorporating the result into a SAT or QSAT solver is counterproductive, because the run-time of such solvers can be sensitive to small implementation changes. The application of better machine learning methods in this area is thus an ongoing challenge, with characteristics unique to the field. This work provides a comprehensive review of the research to date on incorporating machine learning into SAT and QSAT solvers, as a resource for those interested in further advancing the field.

Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT

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.