CISPA
Browse

NeuRes: A Neural Resolution Prover of Unsatisfiability

Download (1.3 MB)
thesis
posted on 2024-10-01, 12:09 authored by Mohamed Abdelhamid GhanemMohamed Abdelhamid Ghanem
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.

History

Primary Research Area

  • Reliable Security Guarantees

Thesis Type

  • Master's Thesis

BibTeX

@masterthesis{Ghanem, title = "NeuRes: A Neural Resolution Prover of Unsatisfiability", author = "Ghanem, Mohamed Abdelhamid" }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC