Understanding GNNs for Boolean Satisfiability through Approximation Algorithms

TL;DR

This work investigates how Graph Neural Networks solve SAT by revealing connections between their message-passing dynamics and classical approximation algorithms, notably SDP relaxations and Belief Propagation. It introduces a curriculum-based training regime and sampling/decimation techniques that drastically speed up training and increase the fraction of solvable instances on synthetic distributions. Empirically, the embeddings in NeuroSAT evolve toward SDP-like vector configurations, and the proposed enhancements yield substantial speedups and better solving performance. The findings offer a framework for interpreting learned approximation algorithms in GNNs and suggest pathways to generalize these ideas to other combinatorial optimization domains.

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.

Figures (9)

• Figure 1: This figure shows how the embeddings of literals change during the MP process. We selected 3 different time steps from the 30 time steps used for this example. The 16-dimensional vectors are projected to 2D by UMAP algorithm. The colors correspond to the truth values of the final solution recovered for this formula. As can be seen, the literals progressively form two well-separated clusters of literals with the same truth value.
• Figure 2: A histogram of Euclidean distances to the average true vector and average false vector. 0 to 0 center are distances between embeddings of literals assigned to false to the average false vector, etc. The figure clearly demonstrates that literals that take the value false in the final assignment move to the same area of the vector space and the same is true for literals that take the value true.
• Figure 3: Validation accuracy during training. Our model with a curriculum achieves reaches 85% in approximately 30 minutes, whereas the original NeuroSAT implementation needs over 5 hours. For comparison, we also add our implementation trained on the same data, but without a curriculum. The training of each model stops once it achieves an accuracy of 85% on a validation set.
• Figure 4: A plot showing how the SDP objective value computed from the NeuroSAT embeddings (in blue) changes after each iteration of MP. The horizontal red line represents the value of the same objective obtained with an SDP solver.
• Figure 5: Lifting the variables to a higher dimension, demonstrated on variables $y_1, y_2, y_3$. Initially, only integer values of $-1$ and $1$ could be assigned to them (integer program). Next, constraints are relaxed, allowing variables to take any real value between $-1$ and $1$. Finally, it is permitted for them to be unit vectors in a high-dimensional space (here, 3 dimensions). The hyperplane in the last picture would be used for rounding the variables at the end. This hyperplane can be randomly selected, and truth values for variables $y_1, y_2, y_3$ are determined based on which side of the hyperplane they land after continuous optimization.