We present DeepSAT, a novel end-to-end learning framework for the Boolean
satisfiability (SAT) problem. Unlike existing solutions trained on random SAT
instances with relatively weak supervision, we propose applying the knowledge
of the well-developed electronic design automation (EDA) field for SAT solving.
Specifically, we first resort to logic synthesis algorithms to pre-process SAT
instances into optimized and-inverter graphs (AIGs). By doing so, the
distribution diversity among various SAT instances can be dramatically reduced,
which facilitates improving the generalization capability of the learned model.
Next, we regard the distribution of SAT solutions being a product of
conditional Bernoulli distributions. Based on this observation, we approximate
the SAT solving procedure with a conditional generative model, leveraging a
novel directed acyclic graph neural network (DAGNN) with two polarity
prototypes for conditional SAT modeling. To effectively train the generative
model, with the help of logic simulation tools, we obtain the probabilities of
nodes in the AIG being logic `1' as rich supervision. We conduct comprehensive
experiments on various SAT problems. Our results show that, DeepSAT achieves
significant accuracy improvements over state-of-the-art learning-based SAT
solutions, especially when generalized to SAT instances that are relatively
large or with diverse distributions.

提出了 DeepSAT 框架，使用 EDA 领域的知识来解决布尔可满足性问题（Boolean satisfiability），通过逻辑合成算法将 SAT 实例预处理为优化的与非图（AIGs），并利用 DAGNN 训练条件生成模型，在各种 SAT 实例上实现了显著的准确度提高。