Understanding GNNs for Boolean Satisfiability through Approximation Algorithms

TL;DR

This paper explores the interpretability of Graph Neural Networks for Boolean Satisfiability by linking them to approximation algorithms, introducing curriculum training, and optimization techniques that improve training efficiency and problem-solving success.

Contribution

It uncovers connections between GNNs and approximation algorithms for SAT, and introduces curriculum training and optimization methods to enhance GNN performance.

Findings

Curriculum training reduces training time by over tenfold.

Decimation and sampling increase the percentage of solved problems.

Connections to Belief Propagation and Semidefinite Programming provide interpretability.

Abstract

The paper deals with the interpretability of Graph Neural Networks in the context of Boolean Satisfiability. The goal is to demystify the internal workings of these models and provide insightful perspectives into their decision-making processes. This is done by uncovering connections to two approximation algorithms studied in the domain of Boolean Satisfiability: Belief Propagation and Semidefinite Programming Relaxations. Revealing these connections has empowered us to introduce a suite of impactful enhancements. The first significant enhancement is a curriculum training procedure, which incrementally increases the problem complexity in the training set, together with increasing the number of message passing iterations of the Graph Neural Network. We show that the curriculum, together with several other optimizations, reduces the training time by more than an order of magnitude compared to the baseline without the curriculum. Furthermore, we apply decimation and sampling of initial embeddings, which significantly increase the percentage of solved problems.