从几何角度解释GNN求解SAT难题的瓶颈
A Geometric Perspective on the Difficulties of Learning GNN-based SAT Solvers
- 用图 Ricci 曲率分析SAT公式图的几何特性
- 发现实例越难，图曲率越负，导致信息压缩困难
- 为GNN求解器设计提供新思路，适合图学习研究者
图神经网络（GNN）作为可学习的布尔可满足性问题（SAT）求解器，近年来受到广泛关注，其在逻辑公式的图表示上运行。然而，其在更难、更受约束的实例上性能急剧下降，引发对架构局限性的质疑。本文从图Ricci曲率（RC）出发，提出几何解释：由随机k-SAT公式导出的二分图具有固有的负曲率，且曲率随实例难度增加而减小。负曲率表明局部连通性存在瓶颈，因此我们推断GNN求解器受‘过度挤压’（oversquashing）影响——长程依赖无法压缩进固定长度表征。我们在多个SAT基准上验证了该观点，确认曲率是问题复杂度的强指标，并可预测泛化误差。最后，我们将发现与现有求解器设计关联，提出未来改进方向。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。