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.

本文综述了近期文献，重点介绍了利用机器学习技术来解决布尔可满足性问题（SAT）的方法，包括从基于手工特征的朴素分类器到最新的端到端 SAT 求解器 NeuroSAT，以及将现有的 CDCL 和本地搜索求解器与机器学习相结合的最新进展。总体而言，利用机器学习解决 SAT 是一个有前途但充满挑战的研究课题，文章指出了当前研究的局限性并提出了未来可能的方向。

解决布尔可满足性问题的机器学习方法

Machine Learning Methods in Solving the Boolean Satisfiability Problem

The NeuroSAT neural network architecture was recently introduced for
predicting properties of propositional formulae. When trained to predict the
satisfiability of toy problems, it was shown to find solutions and
unsatisfiable cores on its own. However, the authors saw "no obvious path" to
using the architecture to improve the state-of-the-art. In this work, we train
a simplified NeuroSAT architecture to directly predict the unsatisfiable cores
of real problems. We modify several high-performance SAT solvers to
periodically replace their variable activity scores with NeuroSAT's prediction
of how likely the variables are to appear in an unsatisfiable core. The
modified MiniSat solves 10% more problems on SAT-COMP 2018 within the standard
5,000 second timeout than the original does. The modified Glucose solves 11%
more problems than the original, while the modified Z3 solves 6% more. The
gains are even greater when the training is specialized for a specific
distribution of problems; on a benchmark of hard problems from a scheduling
domain, the modified Glucose solves 20% more problems than the original does
within a one-hour timeout. Our results demonstrate that NeuroSAT can provide
effective guidance to high-performance SAT solvers on real problems.

本文介绍了使用改进的 NeuroSAT 架构，通过训练简化的神经网络来直接预测实际问题的不可满足核，以提供有效的指导高性能 SAT 求解器在解决特定问题分布时的问题上的应用。

利用不可满足核心预测指导高性能 SAT 求解器

Guiding High-Performance SAT Solvers with Unsat-Core Predictions

We present NeuroSAT, a message passing neural network that learns to solve
SAT problems after only being trained as a classifier to predict
satisfiability. Although it is not competitive with state-of-the-art SAT
solvers, NeuroSAT can solve problems that are substantially larger and more
difficult than it ever saw during training by simply running for more
iterations. Moreover, NeuroSAT generalizes to novel distributions; after
training only on random SAT problems, at test time it can solve SAT problems
encoding graph coloring, clique detection, dominating set, and vertex cover
problems, all on a range of distributions over small random graphs.

NeuroSAT 是一种信息传递神经网络，通过分类器训练来预测可满足性，在解决图着色、团检测、支配集和顶点覆盖等问题上具有较好的泛化性能。