Machine Learning Methods in Solving the Boolean Satisfiability Problem

Abstract

This paper reviews the recent literature on solving the Boolean satisfiability problem (SAT), an archetypal NP-complete problem, with the help of machine learning techniques. Despite the great success of modern SAT solvers to solve large industrial instances, the design of handcrafted heuristics is time-consuming and empirical. Under the circumstances, the flexible and expressive machine learning methods provide a proper alternative to solve this long-standing problem. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT, as well as recent progress on combinations of existing 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.

References in corpus (6)

• Semi-Supervised Classification with Graph Convolutional Networks
• On Joint Learning for Solving Placement and Routing in Chip Design
• Graph Neural Networks and Boolean Satisfiability
• Goal-Aware Neural SAT Solver
• Improve SAT-solving with Machine Learning
• Enhancing SAT solvers with glue variable predictions

Cited by in corpus (4)

• Deep Learning-based Software Engineering: Progress, Challenges, and Opportunities
• SATformer: Transformer-Based UNSAT Core Learning
• Identifying Protein Co-regulatory Network Logic by Solving B-SAT Problems through Gate-based Quantum Computing
• Using deep learning to construct stochastic local search SAT solvers with performance bounds