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. This survey examines 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. It concludes the limitations of current works and suggest possible future directions. The collected paper list is available at https://github.com/Thinklab-SJTU.

From Springer

The Boolean satisfiability problem, often referred to as SAT, is the first proven NP-complete problem in the field of computational complexity. This hard combinatorial problem consistently attracts researchers′ attention for its wide application and for the variety of problems that can be reduced to SAT. For theoretical interests, numerous combinatorial problems can be expressed in propositional formulae and solved by running a SAT solver, e.g., graph coloring, vertex cover and clique detection. It also serves as a useful tool for automated theorem proving, one typical case of which is the resolution of Keller′s conjecture. Moreover, there are plenty of industrial applications of SAT solving, such as bounded model checking, configuration management, and equivalence checking in circuit design. It is a major component in logic synthesis, and many SAT solvers are designed specially for this task. Hence, SAT solving not only promotes research progress but also enables a more economical workflow.

Since the P versus NP problem remains unsettled, researchers respect the difficulty of the SAT problem and struggle to design efficient SAT solvers. Meanwhile, machine learning (ML), especially the surging deep learning techniques has advanced into the combinatorial optimization field and yielded a number of promising new avenues of research. Different areas such as graph matching and mixture integer programming, have been well studied in recent years, and the SAT community is no exception. As one of the most frontier events for SAT solvers, the past SAT competition has also witnessed several winning solvers featuring machine learning techniques, including Kissat_MAB (ranked first in SAT competition 2021) and MapleCOMSPS (ranked first in SAT competition 2016). In addition to the traditional solvers enhanced with machine learning components, end-to-end frameworks such as NeuroSAT seek integration of machine learning and SAT solving, which enables automatic and organic deduction and saves human labor.

There are a few previous surveys related to machine learning techniques in solving SAT and other hard problems. Specifically, Popescu et al. focused on a broader scope of constraint-solving problems. Another survey is the closest to this survey, where the author reviewed machine learning methods in solving SAT and quantified SAT (QSAT), especially for automated theorem proving. The reviewed methods in were categorized by the way of integration of machine learning into SAT solving. Based on its taxonomy, this survey discusses three primary patterns for this combination for SAT solving: 1) Standalone SAT solvers with pure machine learning methods; 2) Replacing some key components of existing conflict-driven clause learning (CDCL) solvers with learning-directed heuristics; 3) Modifying the local search solvers with learning-aided modules. In addition to solving the SAT problem itself with machine learning methods, it also provides a survey of instance generation for SAT with machine learning, which is an emerging yet promising topic in this field. Compared to, this survey focuses on more recent advancements and unfolds in a more compact and succinct way so that readers can be quickly informed of this rising area.

This survey encompasses directly optimizing SAT solving with the aid of machine learning techniques, e.g., multi-layer perceptron (MLP), naive Bayes, and neural networks, in the aforementioned three ways. Portfolio solvers and algorithm runtime prediction are not involved in this paper since it is a general technique applicable to other problems as well (see [Hutter et al.] for a survey). The extensions of SAT, e.g., maximum satisfiability problem (MAX-SAT), satisfiability modulo theories (SMT), and quantified Boolean formula problem (QBF), are also beyond the scope of this survey.

The rest of the paper is organized as follows. After giving some preliminaries in Section 2, it reviews three patterns of machine-learning-based SAT solving: Section 3.1 reviews standalone ML-SAT solvers, Section 3.2 discusses CDCL solvers enhanced with ML components, and Section 3.3 discusses learning-aided local search SAT solvers. In Section 4, machine learning methods for SAT instance generation are reviewed. Finally, it concludes in Section 5. An overview of this survey is illustrated in Fig. 1.

Overview of SAT solvers with ML techniques

Download full text：

Machine Learning Methods in Solving the Boolean Satisfiability Problem

Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, Junchi Yan

https://www.mi-research.net/en/article/doi/10.1007/s11633-022-1396-2

https://link.springer.com/article/10.1007/s11633-022-1396-2

@Article{MIR-2022-07-212,
author = {Wenxuan Guo and Hui-Ling Zhen and Xijun Li and Wanqian Luo and Mingxuan Yuan and Yaohui Jin and Junchi Yan},
journal = {Machine Intelligence Research},
title = {Machine Learning Methods in Solving the Boolean Satisfiability Problem},
year = {2023},
volume = {20},
number = {5},
pages = {640-655},
doi = {10.1007/s11633-022-1396-2}
}