G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

TL;DR

G4SATBench presents a unified benchmark platform for assessing graph neural network approaches to SAT solving, addressing the lack of standardized datasets and fair evaluation. It curates seven diverse datasets from three generator families across three difficulty levels and re-implements a range of GNN baselines with unified interfaces to enable fair comparisons. Through extensive benchmarking and analysis, the study finds that GNNs can emulate greedy local search but struggle to learn backtracking-style CDCL search, with unsupervised training and clause-learning augmentation offering notable gains. The work provides insights into generalization across distributions, outlines limitations of current static GNNs, and points to future directions including neural-guided solving and dynamic graph models.

Abstract

Graph neural networks (GNNs) have recently emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT), offering potential alternatives to traditional backtracking or local search SAT solvers. However, despite the growing volume of literature in this field, there remains a notable absence of a unified dataset and a fair benchmark to evaluate and compare existing approaches. To address this crucial gap, we present G4SATBench, the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. In G4SATBench, we meticulously curate a large and diverse set of SAT datasets comprising 7 problems with 3 difficulty levels and benchmark a broad range of GNN models across various prediction tasks, training objectives, and inference algorithms. To explore the learning abilities and comprehend the strengths and limitations of GNN-based SAT solvers, we also compare their solving processes with the heuristics in search-based SAT solvers. Our empirical results provide valuable insights into the performance of GNN-based SAT solvers and further suggest that existing GNN models can effectively learn a solving strategy akin to greedy local search but struggle to learn backtracking search in the latent space. Our codebase is available at https://github.com/zhaoyu-li/G4SATBench.

Figures (12)

• Figure 1: Framework overview of G4SATBench.
• Figure 2: LCG* and VCG* of the CNF formula $(x_1 \lor \neg x_2) \land (x_1 \lor x_3) \land(\neg x_1 \lor x_2 \lor x_3)$.
• Figure 3: Classification accuracy of satisfiability across different datasets. The x-axis denotes testing datasets and the y-axis denotes training datasets.
• Figure 4: Classification accuracy of satisfiability across different difficulty levels. The x-axis denotes testing datasets and the y-axis denotes training datasets.
• Figure 5: Results on the predicted assignments with the increased message passing iteration $T$. NeuroSAT* refers to the model trained for satisfiability prediction.