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

Researchers explain why Graph Neural Networks (GNNs) struggle with complex Boolean Satisfiability Problems (SATs) through geometric analysis using graph Ricci Curvature. They prove that harder SAT instances have more negative curvature, creating connectivity bottlenecks that prevent GNNs from effectively processing long-range dependencies.

• →GNN-based SAT solvers experience sharp performance degradation on harder and more constrained problem instances.
• →Bipartite graphs from random k-SAT formulas are inherently negatively curved, with curvature decreasing as difficulty increases.
• →Negative graph Ricci Curvature indicates local connectivity bottlenecks that cause oversquashing in GNN solvers.
• →Curvature serves as both a strong indicator of problem complexity and a predictor of generalization error.
• →The findings provide geometric insights that could guide future improvements in GNN solver architecture design.