This paper analyzes the causes of performance degradation in Boolean satisfiability problems (SAT) using graph neural networks (GNNs) from a geometric perspective. Specifically, we quantify local connectivity bottlenecks in graphs using graph richness curvature (RC). We demonstrate that bipartite graphs derived from difficult k-SAT problems exhibit negative curvature, and that curvature decreases with problem difficulty. This demonstrates that GNN-based SAT solvers struggle to compress long-range dependencies into fixed-length representations, leading to "oversquashing." Experimental results demonstrate that curvature can be used as an indicator of problem complexity and for performance prediction. We also present implications for existing solver design principles and suggest future research directions.
