# A Geometric Perspective on the Difficulties of Learning GNN-based SAT Solvers

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 21 of its 52 references that are in the map.
- First posted on arXiv 29 Aug 2025.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [Deeper Insights into Graph Convolutional Networks for Semi-Supervised Learning](https://mlsanity.com/paper/1801.07606/) (2018)
- [Geometric deep learning: going beyond Euclidean data](https://mlsanity.com/paper/1611.08097/) (2016)
- [On the Bottleneck of Graph Neural Networks and its Practical Implications](https://mlsanity.com/paper/2006.05205/) (2020)
- [Understanding over-squashing and bottlenecks on graphs via curvature](https://mlsanity.com/paper/2111.14522/) (2021)
- [Combinatorial optimization and reasoning with graph neural networks](https://mlsanity.com/paper/2102.09544/) (2021)
- [GRAND: Graph Neural Diffusion](https://mlsanity.com/paper/2106.10934/) (2021)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Revisiting Over-smoothing and Over-squashing Using Ollivier-Ricci Curvature](https://mlsanity.com/paper/2211.15779/) (2022)
- [On Vanishing Gradients, Over-Smoothing, and Over-Squashing in GNNs: Bridging Recurrent and Graph Learning](https://mlsanity.com/paper/2502.10818/) (2025)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [From Continuous Dynamics to Graph Neural Networks: Neural Diffusion and Beyond](https://mlsanity.com/paper/2310.10121/) (2023)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [The backtracking survey propagation algorithm for solving random K-SAT problems](https://mlsanity.com/paper/1508.05117/) (2015)
- [Effective Structural Encodings via Local Curvature Profiles](https://mlsanity.com/paper/2311.14864/) (2023)
- [Monte Carlo algorithms are very effective in finding the largest independent set in sparse random graphs](https://mlsanity.com/paper/1904.02231/) (2019)
- [Denoising Diffusion for Sampling SAT Solutions](https://mlsanity.com/paper/2212.00121/) (2022)
- [Neural Approaches to SAT Solving: Design Choices and Interpretability](https://mlsanity.com/paper/2504.01173/) (2025)

## Abstract (arXiv)

Graph Neural Networks (GNNs) have gathered increasing interest as learnable solvers of Boolean Satisfiability Problems (SATs), operating on graph representations of logical formulas. However, their performance degrades sharply on harder and more constrained instances, raising questions about architectural limitations. In this paper, we work towards a geometric explanation built upon graph Ricci Curvature (RC). We prove that bipartite graphs derived from random k-SAT formulas are inherently negatively curved, and that this curvature decreases with instance difficulty. Given that negative graph RC indicates local connectivity bottlenecks, we argue that GNN solvers are affected by oversquashing, a phenomenon where long-range dependencies become impossible to compress into fixed-length representations. We validate our claims empirically across different SAT benchmarks and confirm that curvature is both a strong indicator of problem complexity and can be used to predict generalization error. Finally, we connect our findings to the design of existing solvers and outline promising directions for future work.
