We introduce NeuRes, a neuro-symbolic proof-based SAT solver. Unlike other
neural SAT solving methods, NeuRes is capable of proving unsatisfiability as
opposed to merely predicting it. By design, NeuRes operates in a
certificate-driven fashion by employing propositional resolution to prove
unsatisfiability and to accelerate the process of finding satisfying truth
assignments in case of unsat and sat formulas, respectively. To realize this,
we propose a novel architecture that adapts elements from Graph Neural Networks
and Pointer Networks to autoregressively select pairs of nodes from a dynamic
graph structure, which is essential to the generation of resolution proofs. Our
model is trained and evaluated on a dataset of teacher proofs and truth
assignments that we compiled with the same random formula distribution used by
NeuroSAT. In our experiments, we show that NeuRes solves more test formulas
than NeuroSAT by a rather wide margin on different distributions while being
much more data-efficient. Furthermore, we show that NeuRes is capable of
largely shortening teacher proofs by notable proportions. We use this feature
to devise a bootstrapped training procedure that manages to reduce a dataset of
proofs generated by an advanced solver by ~23% after training on it with no
extra guidance.

我们介绍了一种神经符号证明型 SAT 求解器 NeuRes。与其他神经 SAT 求解方法不同，NeuRes 能够证明不可满足性而不仅仅是预测。通过使用命题证明来证明不可满足以及在不可满足和可满足公式的情况下加速找到满足真值分配的过程，NeuRes 以证书驱动的方式运行。为了实现这一点，我们提出了一种新颖的架构，该架构从图神经网络和指针网络中选择动态图结构的节点对，这对于生成解析证明至关重要。我们使用与 NeuroSAT 相同的随机公式分布编制了一组教师证明和真值分配的数据集，对我们的模型进行训练和评估。在实验中，我们展示了 NeuRes 在不同分布上比 NeuroSAT 解决更多的测试公式，而且数据效率更高。此外，我们还展示了 NeuRes 能够大大缩短教师证明的长度。我们利用这个特性设计了一种引导训练程序，在没有额外指导的情况下，成功将由高级求解器生成的证明数据集减少了约 23%。