  Training neural networks on NP-complete problems typically demands very large
amounts of training data and often needs to be coupled with computationally
expensive symbolic verifiers to ensure output correctness. In this paper, we
present NeuRes, a neuro-symbolic approach to address both challenges for
propositional satisfiability, being the quintessential NP-complete problem. By
combining certificate-driven training and expert iteration, our model learns
better representations than models trained for classification only, with a much
higher data efficiency -- requiring orders of magnitude less training data.
NeuRes employs propositional resolution as a proof system to generate proofs of
unsatisfiability and to accelerate the process of finding satisfying truth
assignments, exploring both possibilities in parallel. To realize this, we
propose an attention-based architecture that autoregressively selects pairs of
clauses from a dynamic formula embedding to derive new clauses. Furthermore, we
employ expert iteration whereby model-generated proofs progressively replace
longer teacher proofs as the new ground truth. This enables our model to reduce
a dataset of proofs generated by an advanced solver by ~32% after training on
it with no extra guidance. This shows that NeuRes is not limited by the
optimality of the teacher algorithm owing to its self-improving workflow. We
show that our model achieves far better performance than NeuroSAT in terms of
both correctly classified and proven instances.
