# G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

arXiv: https://arxiv.org/abs/2309.16941 · HTML: https://mlsanity.com/paper/2309.16941/

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 48 references that are in the map.
- First posted on arXiv 29 Sep 2023.

## Builds on (most cited first, 24 of 24)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [A Simple Framework for Contrastive Learning of Visual Representations](https://mlsanity.com/paper/2002.05709/) (2020)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Delving Deep into Rectifiers: Surpassing Human-Level Performance on ImageNet Classification](https://mlsanity.com/paper/1502.01852/) (2015)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Gated Graph Sequence Neural Networks](https://mlsanity.com/paper/1511.05493/) (2015)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [Augment with Care: Contrastive Learning for Combinatorial Problems](https://mlsanity.com/paper/2202.08396/) (2022)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [PDP: A General Neural Framework for Learning Constraint Satisfaction Solvers](https://mlsanity.com/paper/1903.01969/) (2019)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [Enhancing SAT solvers with glue variable predictions](https://mlsanity.com/paper/2007.02559/) (2020)
- [DeepSAT: An EDA-Driven Learning Framework for SAT](https://mlsanity.com/paper/2205.13745/) (2022)
- [Graph Neural Networks and Boolean Satisfiability](https://mlsanity.com/paper/1702.03592/) (2017)
- [Neural heuristics for SAT solving](https://mlsanity.com/paper/2005.13406/) (2020)
- [Addressing Variable Dependency in GNN-based SAT Solving](https://mlsanity.com/paper/2304.08738/) (2023)
- [Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability](https://mlsanity.com/paper/1909.11588/) (2019)

## Built on by (most cited first, 18 of 18)

- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [AutoSAT: Automatically Optimize SAT Solvers via Large Language Models](https://mlsanity.com/paper/2402.10705/) (2024)
- [Contrastive Representations for Temporal Reasoning](https://mlsanity.com/paper/2508.13113/) (2025)
- [Experience-Guided Reflective Co-Evolution of Prompts and Heuristics for Automatic Algorithm Design](https://mlsanity.com/paper/2509.24509/) (2025)
- [Neural Approaches to SAT Solving: Design Choices and Interpretability](https://mlsanity.com/paper/2504.01173/) (2025)
- [Graph Alignment for Benchmarking Graph Neural Networks and Learning Positional Encodings](https://mlsanity.com/paper/2505.13087/) (2025)
- [FORGE: Foundational Optimization Representations from Graph Embeddings](https://mlsanity.com/paper/2508.20330/) (2025)
- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)
- [Structure based SAT dataset for analysing GNN generalisation](https://mlsanity.com/paper/2502.11410/) (2025)
- [MILP-SAT-GNN: Yet Another Neural SAT Solver](https://mlsanity.com/paper/2507.01825/) (2025)
- [On the Expressive Power of GNNs for Boolean Satisfiability](https://mlsanity.com/paper/2602.08745/) (2026)
- [Learning to Rank the Initial Branching Order of SAT Solvers](https://mlsanity.com/paper/2603.07176/) (2026)
- [A Geometric Perspective on the Difficulties of Learning GNN-based SAT Solvers](https://mlsanity.com/paper/2508.21513/) (2025)
- [Boolean Satisfiability via Imitation Learning](https://mlsanity.com/paper/2509.25411/) (2025)
- [Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations](https://mlsanity.com/paper/2604.15448/) (2026)
- [Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs](https://mlsanity.com/paper/2605.04819/) (2026)
- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)
- [Tiny Recursive Message Passing](https://mlsanity.com/paper/2610.18649/) (2026)

## Abstract (arXiv)

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.