On the Hardness of Learning GNN-based SAT Solvers: The Role of Graph Ricci Curvature
This addresses the fundamental limitations of GNN-based SAT solvers for AI and combinatorial optimization, providing a geometric explanation for performance drops.
The paper tackles the performance degradation of Graph Neural Networks (GNNs) on harder Boolean Satisfiability Problems (SATs) by linking it to graph Ricci Curvature, showing that negative curvature increases with difficulty and causes oversquashing, with empirical validation across benchmarks.
Graph Neural Networks (GNNs) have recently shown promise as solvers for Boolean Satisfiability Problems (SATs) by operating on graph representations of logical formulas. However, their performance degrades sharply on harder instances, raising the question of whether this reflects fundamental architectural limitations. In this work, we provide a geometric explanation through the lens of graph Ricci Curvature (RC), which quantifies local connectivity bottlenecks. We prove that bipartite graphs derived from random k-SAT formulas are inherently negatively curved, and that this curvature decreases with instance difficulty. Building on this, we show that GNN-based SAT 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 performance. Finally, we connect our findings to design principles of existing solvers and outline promising directions for future work.