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%。

NeuRes: 学习命题可满足性的证明

NeuRes: Learning Proofs of Propositional Satisfiability

This work, shows how propositional resolution can be generalized to obtain a
resolution proof system for constrained pseudo-propositional logic (CPPL),
which is an extension resulted from inserting the natural numbers with few
constraints symbols into the alphabet of propositional logic and adjusting the
underling language accordingly. Unlike the construction of CNF formulas which
are restricted to a finite set of clauses, the extended CPPL does not require
the corresponding set to be finite.
Although this restriction is made dispensable, this work presents a
constructive proof showing that the generalized resolution for CPPL is sound
and complete. As a marginal result, this implies that propositional resolution
is also sound and complete for formulas with even infinite set of clauses.

本研究展示了如何将命题演绎推广到受限伪命题逻辑（CPPL）中，这是将自然数与少量约束符号插入命题逻辑字母表并相应地调整底层语言所导致的扩展。虽然该限制被认为是不必要的，但本研究提供了一种建设性证明，证明了 CPPL 的广义演绎推理是正确而完整的。