Repository logo
 

Machine learning for automated theorem proving: Learning to solve SAT and QSAT

Accepted version
Peer-reviewed

Type

Article

Change log

Authors

Holden, SB 

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-of-the-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.

Description

Keywords

46 Information and Computing Sciences, 4602 Artificial Intelligence

Journal Title

Foundations and Trends in Machine Learning

Conference Name

Journal ISSN

1935-8237
1935-8245

Volume Title

Publisher

Now Publishers