# On the Expressive Power of GNNs for Boolean Satisfiability

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 52 references that are in the map.
- First posted on arXiv 9 Feb 2026.

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

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networks](https://mlsanity.com/paper/1810.02244/) (2018)
- [Provably Powerful Graph Networks](https://mlsanity.com/paper/1905.11136/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Identity-aware Graph Neural Networks](https://mlsanity.com/paper/2101.10320/) (2021)
- [Universal Invariant and Equivariant Graph Neural Networks](https://mlsanity.com/paper/1905.04943/) (2019)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [A Short Tutorial on The Weisfeiler-Lehman Test And Its Variants](https://mlsanity.com/paper/2201.07083/) (2022)
- [A Theoretical Comparison of Graph Neural Network Extensions](https://mlsanity.com/paper/2201.12884/) (2022)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [The Descriptive Complexity of Graph Neural Networks](https://mlsanity.com/paper/2303.04613/) (2023)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [SATformer: Transformer-Based UNSAT Core Learning](https://mlsanity.com/paper/2209.00953/) (2022)
- [The Weisfeiler-Leman Dimension of Planar Graphs is at most 3](https://mlsanity.com/paper/1708.07354/) (2017)
- [Improve SAT-solving with Machine Learning](https://mlsanity.com/paper/1710.11204/) (2017)

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

- [Target-Aware Data Augmentation for SAT Prediction](https://mlsanity.com/paper/2605.06931/) (2026)

## Abstract (arXiv)

Machine learning approaches to solving Boolean Satisfiability (SAT) aim to replace handcrafted heuristics with learning-based models. Graph Neural Networks have emerged as the main architecture for SAT solving, due to the natural graph representation of Boolean formulas. We analyze the expressive power of GNNs for SAT solving through the lens of the Weisfeiler-Leman (WL) test. As our main result, we prove that the full WL hierarchy cannot, in general, distinguish between satisfiable and unsatisfiable instances. We show that indistinguishability under higher-order WL carries over to practical limitations for WL-bounded solvers that set variables sequentially. We further study the expressivity required for several important families of SAT instances, including regular, random and planar instances. To quantify expressivity needs in practice, we conduct experiments on random instances from the G4SAT benchmark and industrial instances from the International SAT Competition. Our results suggest that while random instances are largely distinguishable, industrial instances often require more expressivity to predict a satisfying assignment.