Machine Learning Methods in Solving the Boolean Satisfiability Problem

This paper reviews the recent literature on solving the Boolean satisfiability problem (SAT), an archetypal NP-complete problem, with the aid of machine learning (ML) techniques. Over the last decade, the machine learning society advances rapidly and surpasses human performance on several tasks. This trend also inspires a number of works that apply machine learning methods for SAT solving. In this survey, we examine the evolving ML SAT solvers from naive classifiers with handcrafted features to emerging end-to-end SAT solvers, as well as recent progress on combinations of existing conflict-driven clause learning (CDCL) and local search solvers with machine learning methods. Overall, solving SAT with machine learning is a promising yet challenging research topic. We conclude the limitations of current works and suggest possible future directions. The collected paper list is available at https://github.com/ThinklabSJTU/awesome-ml4co.

Automated summary

This paper reviews recent literature on using machine learning techniques to solve the Boolean satisfiability problem (SAT), a classic NP-complete problem. The rapid advancements in the field of machine learning over the past decade have inspired many researchers to apply machine learning methods for SAT solving. The paper examines the evolution of ML SAT solvers, from naive classifiers with handcrafted features to emerging end-to-end SAT solvers, as well as recent progress in combining existing conflict-driven clause learning (CDCL) and local search solvers with machine learning methods. The paper concludes by addressing the limitations of current works and suggesting possible future directions. The collected paper list is available at https://github.com/ThinklabSJTU/awesome-ml4co.