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

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.

Key findings

• ▸Machine learning has been applied to SAT and QSAT problems, but its incorporation into solvers can be counterproductive due to sensitivity to implementation changes.
• ▸Better machine learning methods are needed to improve the performance of SAT and QSAT solvers.
• ▸The application of machine learning in this area is delicate and requires careful consideration of the trade-offs between learning and implementation.

Keywords

Identifiers

DOI

10.1561/2200000081

Journal

Foundations and Trends® in Machine Learning

Year

2020