Learning Better Representations From Less Data For Propositional Satisfiability
This addresses the data inefficiency and computational cost in neural approaches to NP-complete problems, offering a self-improving method for propositional satisfiability, though it is incremental as it builds on existing neuro-symbolic techniques.
The paper tackles the challenge of training neural networks for propositional satisfiability, which typically requires large datasets and symbolic verifiers, by introducing NeuRes, a neuro-symbolic approach that learns better representations with orders of magnitude less data and reduces proof dataset size by ~32% through self-improvement.
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.