We introduce NeuRes, a neuro-symbolic generative model for proving Boolean unsatisfiability using resolution. A resolution proof is a sequence of case distinctions ending in the empty clause (falsum). Similar propositional logic tasks have proven fertile grounds for neuro-symbolic methods such as NeuroSAT. However, these methods often lack easily verifiable certificates for unsatisfiability to support their predictions, whereby verifying their output effectively requires solving the satisfiability problem again. In contrast, resolution proofs produced by NeuRes provide an easily checkable certificate for unsatisfiability. We introduce a general architecture that adapts elements from Graph Neural Networks and Pointer Networks to autoregressively select pairs of nodes from a dynamic graph structure. Our model is trained and evaluated on a dataset of expert proofs that we compiled with the same formula distribution used by NeuroSAT. Compared to previous methods, we demonstrate NeuRes to be more data efficient, requiring only 8K training formulas to concisely prove unsatisfiability for 92.84% of unseen test formulas. In addition to the high success rate of our model, we further demonstrate its ability to largely shorten teacher proofs in a bootstrapped fashion with no extra guidance.
2024-01-24
2024-10-01