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

TL;DR

It is proved that bipartite graphs derived from random k-SAT formulas are inherently negatively curved, and that this curvature decreases with instance difficulty, and that curvature is both a strong indicator of problem complexity and can be used to predict generalization error.

Abstract

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.

Figures (7)

• Figure 1: (a) Average as a function of $\alpha$ for random 3-SAT problems with $N=256$. The color is used as a representation for the average solvability of the problems at a given $\alpha$ by the NeuroSAT model selsam_learning_2019, with a group labeled as solvable if 50% or more of the problems get a satisfying assignment. The vertical red line represents the analytical SAT-UNSAT critical threshold $\alpha_c \approx 4.267$MertensThresholds. The average drops monotonically with $\alpha$. The small plot in the bottom-left corner provides the model's solution probability curve in terms of $\alpha$, where it is possible to notice the algorithmic transition from satisfiable to unsatisfiable problems. (b) Probability of finding a satisfying assignment of the same problems as in (a) with NeuroSAT as a function of the variance and mean of the . Notice how as $\alpha$ grows, the average curvature not only gets more negative, but also concentrates. We can see from the empirical results in (a) that in this case, the model is unable to produce a satisying assignment. As $\alpha$ becomes smaller, the input graphs have less negative edges on average, the associated variance naturally grows, and so does the solving probability. Using the first two moments of the , we are able to observe a similar transition-like phenomenon as the small plot in the bottom-left corner of (a). Best viewed in color.
• Figure 2: Low dimensional visualization of the literal embeddings produced by NeuroSAT on random 4-SAT with (a) vanilla message passing and (b) Curvature Gate. Even though there is no major change in performance, the learned representations can be linearly separated into truth value assignments in the curvature-aware case, indicating promise for the inclusion of these principles in future -based solver design.
• Figure 3: Average graph Ricci Curvature lower bound (a) and Balanced Forman Curvature (b) as a function of $\alpha$ and $k$. Both quantities behave very similarly, both in terms of the smooth transition from flat to negative curvature and their magnitude, especially as $\alpha \to 0$ and $\alpha \to \infty$, in line with the developed theory. Best viewed in color.
• Figure 4: Visualization of an easy (in terms of clause density $\alpha$) random 3-SAT problem with 256 variables in (a) bipartite and (b) circular layouts. There is a very small number of long-range interactions, as can clearly be seen in (b). Furthermore, for such very small $\alpha$, the average approaches 0, in line with the developed theory.
• Figure 5: Visualization of a hard (in terms of clause density $\alpha$) random 3-SAT problem with 256 variables in (a) bipartite and (b) circular layouts. There is a very large number of long-range interactions, as can clearly be seen in (b). Furthermore, for such large $\alpha$, the average is strongly negative, in line with the developed theory.

Theorems & Definitions (10)

• Proposition 3.1: bounds on bipartite graphs
• Proposition 3.2
• Lemma 3.1
• Theorem 3.1
• Definition A.1: Ollivier-Ricci Curvature ollivier2009ricci
• Definition A.2: toppingunderstanding
• proof
• proof
• proof
• proof