Graph Neural Networks and Boolean Satisfiability

TL;DR

This paper investigates whether Graph Neural Networks can learn to classify Boolean satisfiability problems directly from graph representations without feature engineering, revealing promising initial results.

Contribution

It introduces a novel approach of applying GNNs to Boolean SAT classification and demonstrates their ability to learn satisfiability features in a weakly-supervised setting.

Findings

GNNs can learn features of satisfiability without explicit feature engineering

The approach is novel in applying GNNs to SAT classification

Preliminary results are promising for future research

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.