Graph Neural Networks and Boolean Satisfiability
This addresses the challenge of applying machine learning to logical reasoning problems like SAT, which is a fundamental NP-complete problem in computer science, but the work is preliminary and incremental as it explores a novel application rather than a breakthrough.
The paper tackles the problem of classifying Boolean satisfiability (SAT) using deep neural architectures, specifically Graph Neural Networks (GNNs), and finds that GNNs can learn features of satisfiability in a weakly-supervised setting without problem-specific feature engineering.
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.