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

## TL;DR

This paper provides a geometric explanation for the limitations of GNN-based SAT solvers, showing that negative graph Ricci Curvature correlates with problem difficulty and impacts the ability of GNNs to learn effectively.

## Contribution

It introduces a geometric perspective based on graph Ricci Curvature to explain GNN performance issues on complex SAT instances and validates this approach empirically.

## Key findings

- Negative graph Ricci Curvature characterizes harder SAT instances.
- Curvature serves as a predictor of problem complexity and generalization error.
- GNNs suffer from oversquashing in negatively curved graph regions.

## Abstract

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.