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.

翻译：图神经网络（GNN）作为布尔可满足性问题（SAT）的可学习求解器，在逻辑公式的图表示上运行时，已引起越来越多的关注。然而，其在更困难、约束更强的实例上性能急剧下降，引发了关于其架构局限性的疑问。本文从基于图里奇曲率（RC）的几何解释出发展开研究。我们证明了从随机k-SAT公式导出的二分图本质上是负曲率的，且该曲率随实例难度增加而减小。鉴于负的图RC意味着局部连接瓶颈，我们认为GNN求解器受到过度挤压效应的影响——即长程依赖关系无法被压缩到固定长度表示中的现象。我们在不同的SAT基准测试中实证验证了上述观点，并确认曲率既是问题复杂度的强指标，也可用于预测泛化误差。最后，我们将研究结果与现有求解器的设计联系起来，并展望了未来工作的潜在方向。