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.

翻译：我们提出了NeuRes，一种基于神经符号的SAT求解器。与其它神经SAT求解方法不同，NeuRes不仅能预测不可满足性，更能证明其不可满足性。在设计上，NeuRes以证书驱动的方式运作，分别通过命题消解来证明不可满足性，并在处理不可满足公式和可满足公式时加速寻找满足真值赋值的过程。为实现这一目标，我们提出了一种新颖的架构，该架构结合了图神经网络和指针网络的元素，以自回归方式从动态图结构中选择节点对，这对生成消解证明至关重要。我们的模型在教师证明和真值赋值数据集上进行训练和评估，该数据集使用与NeuroSAT相同的随机公式分布编译而成。实验表明，在不同分布上，NeuRes求解的测试公式数量明显多于NeuroSAT，同时数据效率更高。此外，我们还证明了NeuRes能够大幅缩短教师证明的长度（可观的比例）。利用这一特性，我们设计了一种引导式训练流程，在无额外引导的情况下，该流程成功将高级求解器生成的证明数据集规模缩减了约23%。