Recognition: unknown
Graph Neural Networks and Boolean Satisfiability
read the original abstract
In this paper we explore whether or not deep neural architectures can learn to classify Boolean satisfiability (SAT). We devote considerable time to discussing the theoretical properties of SAT. Then, we define a graph representation for Boolean formulas in conjunctive normal form, and train neural classifiers over general graph structures called Graph Neural Networks, or GNNs, to recognize features of satisfiability. To the best of our knowledge this has never been tried before. Our preliminary findings are potentially profound. In a weakly-supervised setting, that is, without problem specific feature engineering, Graph Neural Networks can learn features of satisfiability.
This paper has not been read by Pith yet.
Forward citations
Cited by 2 Pith papers
-
Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs
A polarity-aware hypergraph GNN framework improves unsat core prediction in SAT by separating polarity-invariant and equivariant literal representations.
-
Hypergraph Neural Networks Accelerate MUS Enumeration
Hypergraph neural networks trained via reinforcement learning enumerate more minimal unsatisfiable subsets within a fixed budget of satisfiability checks than conventional methods.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.