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

Conference: ICLR 2026 arXiv: 2508.21513 Code: None Area: Graph Neural Networks / Theory Keywords: GNN, SAT solver, Ricci curvature, oversquashing, graph geometry

TL;DR¶

This paper proves, from the geometric perspective of graph Ricci curvature, that the bipartite graph representation of random k-SAT instances exhibits inherent negative curvature that decreases as problem difficulty increases. It establishes a theoretical connection between GNN oversquashing and SAT solving difficulty, and validates the theory through test-time graph rewiring.

Background & Motivation¶

Background: GNNs serve as learnable SAT solvers by performing message passing on the bipartite graph representation of logical formulas to solve Boolean satisfiability problems.

Limitations of Prior Work: GNN solvers suffer severe performance degradation on harder, more constrained SAT instances (e.g., as \(k\) increases), yet a theoretical explanation for this degradation has been lacking.

Key Challenge: The difficulty of SAT problems is closely tied to long-range dependencies (constraint relationships between distant variables), while the message-passing mechanism of GNNs is inherently limited by oversquashing when handling such dependencies—information from exponentially growing neighborhoods must be compressed into fixed-dimensional embeddings.

Goal: To provide a geometry-based theoretical explanation for why GNN-based SAT solvers underperform on difficult instances.

Key Insight: Balanced Forman Curvature (BFC) is employed as a graph-geometric tool to establish a theoretical chain linking SAT problem difficulty → graph curvature → GNN oversquashing.

Core Idea: The BFC of random k-SAT bipartite graphs converges in probability to \(2/k - 2\) (strongly negative curvature) in the hard limit (\(\alpha \to \infty\)), which directly induces GNN oversquashing and constitutes the geometric root cause of solver performance degradation.

Method¶

Overall Architecture¶

The paper follows a framework of theoretical analysis combined with experimental validation: (1) proving the behavior of BFC on the Literal-Clause bipartite graph of random k-SAT across different difficulty regimes; (2) establishing a theoretical connection to GNN oversquashing; and (3) validating the theory through test-time graph rewiring and generalization error prediction.

Key Designs¶

Probabilistic Characterization of BFC (Theoretical Core):
- Function: Precisely characterizes how the BFC of random k-SAT bipartite graphs evolves with problem difficulty.
- Mechanism: Modeling follows an Erdős-Rényi-type process where literal node degrees follow a Poisson distribution \(\lambda = \alpha k/2\). Three key results are proved: (a) as \(\alpha \to 0\), BFC \(\to 0\) (easy instances yield nearly flat graphs); (b) as \(\alpha \to \infty\), the lower bound of BFC \(\to 2/k - 2\); (c) BFC itself converges in probability to \(2/k - 2\) (Theorem 3.1), requiring analysis of 4-cycle structure behavior in the limit.
- Design Motivation: BFC is fully determined by endpoint degrees and neighborhood topology, admits closed-form computation, and has been shown to be directly related to GNN oversquashing.
Theoretical Connection to Oversquashing:
- Function: Links the BFC results to Topping et al.'s theorem on GNN oversquashing.
- Mechanism: When \(\kappa(i,j) \leq -2 + \delta\) (for arbitrarily small \(\delta > 0\)), the Jacobian of node representations near edge \(i \sim j\) decays exponentially under bounded message-passing gradients. For large \(k\) or large \(\alpha\), Theorem 3.1 guarantees the existence of such highly negative-curvature edges.
- Design Motivation: Establishes a complete causal chain: SAT difficulty → negative curvature → oversquashing → performance degradation.
Curvature-Based Hardness Heuristic (Practical Contribution):
- Function: Proposes BFC-based dataset hardness prediction metrics.
- Mechanism: \(\omega(G) = -\mathbb{E}[\kappa(i,j)] \cdot \mathbb{E}[\alpha]\) and \(\omega^*(G) = \omega(G) / \mathbb{V}[\kappa(i,j)]\); the former jointly accounts for curvature and density, while the latter further incorporates concentration (higher concentration implies greater difficulty).
- Design Motivation: Clause density \(\alpha\) alone is insufficient for judging difficulty—the CA dataset has large \(\alpha\) (9.73) but community structure reduces effective negative curvature. The Pearson correlation of \(\omega^*\) with generalization error reaches 0.98.

Loss & Training¶

Standard GNN solver training (NeuroSAT and GCN), 100 epochs, AdamW optimizer. The analytical focus is on theory and geometry rather than training procedures.

Key Experimental Results¶

Main Results¶

Effect of Test-Time Graph Rewiring (accuracy gain after reducing negative curvature):

Dataset	NeuroSAT Original	NeuroSAT Rewired	GCN Original	GCN Rewired
3-SAT	0.690	0.820 (+0.130)	0.510	0.626 (+0.116)
4-SAT	0.436	0.686 (+0.250)	0.180	0.374 (+0.194)
SR (mixed k)	0.734	0.902 (+0.168)	0.470	0.696 (+0.226)
CA (industrial)	0.746	0.828 (+0.082)	0.650	0.670 (+0.020)

Ablation Study¶

Correlation between hardness heuristics and generalization error:

Heuristic	Pearson Correlation with Generalization Error
\(\bar{\alpha}\) (mean clause density)	0.32
\(\bar{\omega}\) (curvature × density)	0.86
\(\bar{\omega^*}\) (with concentration)	0.98

Key Findings¶

The mean BFC decreases monotonically with \(\alpha\) and begins to concentrate sharply near the dynamical transition threshold \(\alpha_d \approx 3.927\).
The rewiring improvement for 4-SAT (+0.250) is substantially larger than for 3-SAT (+0.130), confirming the theoretical prediction that larger \(k\) yields more negative curvature and more severe oversquashing.
The CA dataset has large \(\alpha\) (9.73) yet shows minimal improvement (+0.082), as its community structure reduces effective bottlenecks—the curvature is less negative than in random graphs.
Simple curvature-aware GNN processing indicators cannot consistently improve performance (BFC is too concentrated in the hard regime), indicating that more fundamental architectural changes are needed.

Highlights & Insights¶

Revelation of Dual Difficulty: GNN-based SAT solvers face two independent sources of difficulty—the algorithmic computational hardness of SAT and the oversquashing learning difficulty inherent to graph representations. The latter had not been theoretically explained before; this work fills that gap.
Interaction Between \(k\) and \(\alpha\): Larger \(k\) induces severe negative curvature even at "easy" \(\alpha\) settings, suggesting that oversquashing may limit GNN performance before algorithmic hardness even becomes a factor.
Persuasiveness of Rewiring Experiments: Large performance gains are obtained by reducing negative curvature at test time alone—without retraining—providing strong evidence for a causal argument rather than mere correlation.
Geometric Interpretation of Recurrence: NeuroSAT's recurrent message passing substantially outperforms GCN; the paper notes that recurrence has been shown to mitigate oversquashing, offering theoretical hindsight for existing architectural design choices.

Limitations & Future Work¶

Analysis is restricted to random k-SAT; real-world industrial SAT instances may have fundamentally different graph structures (e.g., community structure).
The identified message-passing bottleneck only provides new insight into BFC as a prior and does not yield improved model designs—simple curvature-aware GNNs fail to improve performance.
Theoretical analysis is limited to the thermodynamic limit (\(N \to \infty\)); finite-size effects are not thoroughly discussed.
The use of curvature information to guide training (e.g., curvature-weighted loss) or sampling strategies remains unexplored.

vs. Topping et al. 2022: This work instantiates their general theory of oversquashing and negative curvature specifically for SAT bipartite graphs, providing the first rigorous application of that theory to combinatorial optimization.
vs. NeuroSAT: NeuroSAT's recurrent design incidentally mitigates oversquashing; this paper offers a geometric theoretical explanation for that empirical observation.
vs. Statistical Physics of SAT: Classical approaches characterize SAT hardness via phase transitions in \(\alpha\); this work introduces the graph curvature dimension, capturing learning difficulty that \(\alpha\) alone cannot explain.

Rating¶

Novelty: ⭐⭐⭐⭐⭐ First theoretical characterization of GNN SAT solver limitations from a graph curvature perspective, with a complete and closed theoretical chain.
Experimental Thoroughness: ⭐⭐⭐⭐ Comprehensive coverage of theoretical validation, rewiring ablation, and heuristic evaluation, though large-scale industrial benchmarks are absent.
Writing Quality: ⭐⭐⭐⭐⭐ Rigorous and clear theoretical derivations, progressing systematically from simple propositions to the main theorem.
Value: ⭐⭐⭐⭐ Offers a novel geometric perspective for understanding and improving neural combinatorial solvers, though it has not yet translated into concrete architectural improvements.