NeuRes: Learning Proofs of Propositional Satisfiability
Mohamed Ghanem Frederik Schmitt Julian Siber Bernd Finkbeiner
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.