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

TL;DR
This paper provides a geometric explanation for the limitations of GNN-based SAT solvers, showing that negative graph Ricci Curvature correlates with problem difficulty and impacts the ability of GNNs to learn effectively.
Contribution
It introduces a geometric perspective based on graph Ricci Curvature to explain GNN performance issues on complex SAT instances and validates this approach empirically.
Findings
Negative graph Ricci Curvature characterizes harder SAT instances.
Curvature serves as a predictor of problem complexity and generalization error.
GNNs suffer from oversquashing in negatively curved graph regions.
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…
| Model | Variation | Datasets | |||
|---|---|---|---|---|---|
| 3-SAT | 4-SAT | SR | CA | ||
| GCN | No Rewiring | 0.510 0.012 | 0.180 0.048 | 0.470 0.031 | 0.650 0.016 |
| Test-time Rewiring | 0.626 0.021 (+0.116) | 0.374 0.045 (+0.194) | 0.696 0.035 (+0.226) | 0.670 0.048 (+0.020) | |
| NeuroSAT | No Rewiring | 0.690 0.022 | 0.436 0.032 | 0.734 0.017 | 0.746 0.018 |
| Test-time Rewiring | 0.820 0.030 (+0.130) | 0.686 0.029 (+0.250) | 0.902 0.004 (+0.168) | 0.828 0.029 (+0.082) | |
| Problem | Generalization Error | Hardness Heuristic | ||
|---|---|---|---|---|
| 3-SAT | 0.31 | 4.59 | 4.12 | 97.41 |
| 4-SAT | 0.56 | 9.08 | 9.81 | 612.32 |
| SR | 0.27 | 6.09 | 5.30 | 125.30 |
| CA | 0.25 | 9.73 | 6.30 | 123.27 |
| Model | Variation | Datasets | |||
|---|---|---|---|---|---|
| 3-SAT | 4-SAT | SR | CA | ||
| GCN | Vanilla | 0.510 0.012 | 0.180 0.048 | 0.470 0.031 | 0.650 0.016 |
| Curvature Gate | 0.514 0.018 | 0.154 0.017 | 0.422 0.013 | 0.664 0.042 | |
| Online LCP | 0.510 0.014 | 0.170 0.010 | 0.422 0.016 | 0.662 0.016 | |
| Both | 0.500 0.012 | 0.176 0.031 | 0.416 0.027 | 0.654 0.027 | |
| NeuroSAT | Vanilla | 0.690 0.022 | 0.436 0.032 | 0.734 0.017 | 0.746 0.018 |
| Curvature Gate | 0.682 0.030 | 0.436 0.015 | 0.742 0.027 | 0.758 0.016 | |
| Online LCP | 0.692 0.020 | 0.416 0.046 | 0.724 0.022 | 0.726 0.059 | |
| Both | 0.664 0.018 | 0.438 0.028 | 0.742 0.025 | 0.758 0.020 | |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Semantic Web and Ontologies · Mobile Agent-Based Network Management
A Geometric Perspective on the Difficulties of Learning GNN-based SAT Solvers
Geri Skenderi
Department of Computing Sciences, Bocconi University, Milan, Italy
Bocconi Institute for Data Science and Analytics (BIDSA)
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 -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.
1 Introduction
The Boolean Satisfiability Problem (SAT) is a cornerstone problem of theoretical computer science. It can be succinctly described as the problem of proving logical formulas, whether that consists in making a decision (is the formula satisfiable?) or providing an assignment (which is a bitstring that satisfies the formula?). SAT plays a foundational role in complexity theory as the first NP-Complete problem[cook1971complexity]. Furthermore, many real-world tasks such as circuit verification, automated planning, and software testing, are routinely cast into SAT form [bordeaux2006propositional, silva2008practicalSAT, biere2009handbook]. Beyond computer science, tools from statistical physics have been used to study typical-case theoretical properties [monasson1997statistical, krzakala2007gibbs, zdeborová2009statistical] and propose various solvers [BraunsteinSP, marino2016backtracking, angelini2019monte].
Recently, Graph Neural Networks (GNNs) [scarselli2008graph, gilmer2017neural] have emerged as a new paradigm in combinatorial problem solving by learning over the graph representations of these problems [cappart2023combinatorial]. This trend has been extended to learning SAT solvers [selsam_learning_2019, ozolins_goal-aware_2022, freivalds_denoising_2022, chang2025sat]. By representing logical formulas as bipartite graphs that connect variables to clauses, GNNs can be trained end-to-end on both decision and assignment scenarios. Despite their flexibility, these neural solvers remain fragile in practice. Their performance deteriorates on problems that are anecdotally or formally known to be of increasing (algorithmic) difficulty, e.g., at increasing values in random -SAT [skenderi2026benchmarking, lig4satbench].
In terms of representation learning, GNNs suffer from two prevalent issues: oversmoothing [li2018deeper] and oversquashing [alonbottleneck]. Oversmoothing refers to the idea that repeated aggregation causes node representations to become similar, eventually making them indistinguishable. This effect often imposes a practical upper bound on GNN depth. Oversquashing occurs when information from an exponentially expanding neighborhood must be compressed into finite-dimensional embeddings. This bottleneck severely restricts the ability of GNNs to model long-range dependencies. Oversquashing can, therefore, be thought of as a vanishing gradient problem. Given that the difficulty of SAT can actually be intuited as being directly related to the number of long-range dependencies between nodes, we question whether learning GNN-based solvers on these difficult problems is impacted by oversquashing.
Recent geometric analyses have showed that oversquashing is tightly tied to negative Ricci Curvature (RC) of the underlying graph [toppingunderstanding, nguyen2023revisiting]. These insights invite a fundamental question: Can graph RC serve as a predictive and constructive notion in unraveling limitations of GNN-based SAT solvers? In this work, we address this question by studying the behavior of the graph RC on random -SAT problems represented as bipartite graphs. We show that, with high probability, the edges become more negatively curved as problems get harder, and less negatively curved as they become easier. Finally, we derive an exact expression for the Balanced Forman Curvature (BFC) in the limit of unsolvable problems, from which we make a connection between curvature and oversquashing in GNNs-based SAT solvers, following the theory of toppingunderstanding. This is, to the best of our knowledge, the first successful attempt at a theoretical characterization of the limitations of GNN-based SAT solvers.
To validate our theory, we perform experiments on random 3- and 4- SAT problems following skenderi2026benchmarking, and also on different datasets from the recent benchmark of lig4satbench. Firstly, we observe a phase transition-like phenomenon in random 3-SAT solving probability as a function of the mean and variance of the BFC. We further affirm the aforementioned limitations by rewiring only the testing graphs of the benchmarks at test-time to increase their average BFC, and show that these rewired problems become much easier to solve. Finally, we find that heuristics based on the average BFC of a dataset correlate well with generalization error, unlike the average clause density, which is typically used to characterize the hardness of a single instance. Overall, our findings suggest that GNN-based SAT solvers suffer from two different types of hardness: the hardness of learning representations of inputs with high negative BFC, followed by the well-established algorithmic hardness of SAT. We conclude by relating our findings with modeling and design principles of existing approaches, as well as providing avenues for future research.
2 Background
This section is only intended to formally introduce the objects studied in the paper and render the material self-contained. We kindly ask the reader to tolerate the occasional whirlwind and abuse of notation, which will be formalized later in Section 3.
2.1 Random Boolean Satisfiability Problem
The random -SAT (assignment) problem, which is the central object of study in this work, is made up of variables that can take binary values . Using these variables, one constructs clauses containing a disjunction of variables or their negations (called literals). For example, a 3-SAT problem would have clauses of the form . The goal is to assign a value to all literals such that they satisfy the conjuction of all clauses, a logical formula posed in Conjunctive Normal Form (CNF). In the random formulation, it is possible to identify different phases of problem hardness based on the clause density parameter . This phenomenon has been actively researched in statistical physics due to the analogies between random -SAT and spin-glass models [mezard1987spin, mezard2009information]. Notable results[MezardSP, krzakala2007gibbs, zdeborová2009statistical] include the discovery of two transitions for typical instances at a given , based on the value of in the thermodynamic limit (): As increases, the measure over the space of possible solutions first decomposes into an exponential number of clusters at the dynamical transition and subsequently condensates over the largest such states at the critical transition . These phase transitions naturally affect the performances of many algorithms, e.g., when , solving beyond is almost impossible with existing algorithms.
2.2 Graph Neural Networks
GNNs are a subclass of Neural Networks (NNs) that learn representations of graph data by locally aggregating information[scarselli2008graph, gilmer2017neural]. The main goal of the architecture is to implement symmetries natural to graphs [bronstein2017geometric]. Consider, for simplicity, an unweighted and undirected graph with nodes, represented by a symmetric binary adjacency matrix . This setting can be easily extended to deal with more general connectivity structures [corso2024graph]. By associating a node signal to the graph, we can describe a GNNs as a learnable convolution of the node signal with as the shift operator. A generalization of this concept can be obtained by considering the message-passing framework:
[TABLE]
where denotes node features of node at layer , the (optional) edge features from node to node , the set of (1-hop) neighbor nodes, a differentiable, permutation invariant function, (e.g., sum, mean), and denote differentiable and (optionally) nonlinear functions such as Multi-Layer Perceptrons (MLPs).
A CNF formula can be readily translated into a bipartite graph [biere2009handbook], which can then be fed into a GNN-based solver. The particular bipartition we consider in this work is detailed later in Section 3. The application of the above message-passing scheme on SAT problems can be seen as using Equation1 for the clause and literal partitions [lig4satbench]. Let be a literal node and be a clause node, then:
[TABLE]
where the subscripts and refer to parameters specific to the clause and literal partitions respectively.
2.3 Ricci Curvature of Graphs
In Riemannian geometry, RC quantifies the local deviation of a manifold from flat Euclidean space based on (loosely speaking) volume change. Intuitively, RC captures how the neighborhoods of two adjacent points relate when moving from one point to the other by comparing how a small ball of mass around a point is distorted when transported along a geodesic to a neighboring point. Extending this notion to more general structures, such as metric spaces or combinatorial complexes, is an extremely active area of mathematical research, with the works of ollivier2009ricci and forman2003bochner standing out. In the case of graphs, we ask ourselves how local connectivity either concentrates or disperses. ollivier2009ricci implements this idea by comparing probability mass on local neighborhoods, i.e., a random walk distribution on the endpoints of an edge. Given these two distributions, one can compare the ratio between their Wasserstein and shortest path distance, serving as a direct and discrete analogue of geodesic transport. See Appendix A.1.1 for more details. The definition of forman2003bochner relies heavily on topology, and thus it takes a combinatorial form. Essentially, given a cell complex, the curvature of a p-cell depends only on the topological structures between the cell and its neighbors. This makes it quite simple to compute numerically. Given that RC is directly related to the structure of local neighborhoods, it has emerged as a powerful way of theoretically analyzing limitations of GNNs. In a seminal paper, toppingunderstanding provide both a balanced version of the Forman-Ricci Curvature (FC) curvature and show that the oversquashing problem [alonbottleneck] can be directly connected to edges with high negative curvature. This definition, namely the BFC, is central to this paper, therefore please consult Appendix A.1.2 for the definition and additional details. nguyen2023revisiting have shown that similar results can be derived using the Ollivier-Ricci Curvature (OC) curvature. It is worth noting that these notions of curvature are naturally correlated with one another, as shown empirically in a multitude of complex networks by samal2018comparative.
3 Curvature of Random k-SAT and Its Relationship with GNNs
Setting and Notation.
We consider random -SAT problems with variables and clauses, with and . The problems are represented as simple bipartite graphs , where the node set is a literal-clause bipartition , with and . The edge set takes the form . Given , we denote its degree by . The expected value of the random variable with probability distribution is denoted by , while is expectation over samples drawn from . Unless noted otherwise, when we refer to the expected value in simulations, we imply its estimate via the sample mean statistic. We denote by the convergence in probability of a sequence of random variables to a constant under a given limiting behavior Finally, we denote the BFC at an edge by . We remind the reader that we are going to analyze this variant of graph RC, defined in Appendix A.1.2.
Data Model.
Our bipartite formulation is a simplification of the input graphs considered in many GNN-based solvers [selsam_learning_2019, ozolins_goal-aware_2022]. Recent literature [lig4satbench] refers to this data structure as a Literal-Clause Graph (LCG). We consider an Erdős–Rényi-like procedure, where each clause is assigned distinct literals independently at random with probability . Assuming therefore that all literals are equally likely to appear in a given clause, we obtain the following degree distributions:
[TABLE]
where represents the delta function, the binomial coefficient, and . In the limit , we can approximate the Binomial form of the literal degree distribution with a Poisson distribution:
[TABLE]
with . We will be interested in using this approximation to analyze the graph BFC, which is an edge level property that is dependent on the degrees of the endpoints. Therefore we need to consider sampling on the edges of the graph. This fact has no implications on given its distribution, but it does imply that for our calculations, the literal degree should have zero mass on and be biased towards higher-degree literals under edge sampling. This line of reasoning naturally leads to the idea of considering a size-biased PMF [shanker2021generalization] as follows:
[TABLE]
which can easily be seen to be an equivalence in distribution as .
Characterizing curvature in easy and hard regimes.
We will now proceed by showing that the BFC of the above bipartite representation can be characterized in probability. This, in turn, will have implications for oversquashing. The proofs of all statements are deferred to Appendix A.2.
Proposition 3.1** (BFC bounds on bipartite graphs).**
Define the quantity
[TABLE]
For any edge in a simple, unweighted bipartite graph , we have that that .
Proposition 3.2**.**
Let be an edge from the LCG representation of a random k-SAT problem with variables and clauses, with degree distributions given by Equations 5 and 3. Then as .
Proposition 3.2 tells us that as problems become easier, their graph representations get (Ricci) flatter. This implies a relationship between trivial problems and their bipartite topology, which is that each clause is made of distinct, unique literals. In this scenario, producing a satisfying assignment becomes easy since assigning truth values to literals of one clause does not affect other clauses. This implication aligns well with common knowledge, therefore the next thing to check is the behavior when dealing with very difficult problems. This later case is important because it is close to the unsatisfiable phase where the faults of existing algorithms emerge [angelini2019monte]. We can formalize this intuition by first looking at the behavior of the lower bound in the limit of unsatisfiable when problems.
Lemma 3.1**.**
Let be an edge from the LCG representation of a random k-SAT problem with variables and clauses, with degree distributions given by Equations 5 and 3. Then as .
In the unsatisfiable limit, the lower bound of the graph BFC will tend to be maximally negative with high probability. Furthermore, Lemma 3.1 provides an interesting interplay between and in the aforementioned limit. We now show that this behavior holds in fact also for the BFC, and explore all the implications.
Theorem 3.1**.**
Let be an edge from the LCG representation of a random k-SAT problem with variables and clauses, with degree distributions given by Equations 5 and 3. Let be the neighbors of forming a 4-cycle based at , without diagonals inside. The BFC at is bounded from above by the quantity:
[TABLE]
Furthermore, in the limit , fixed, , and , .
Theorem 3.1 contains a crucial result in its probabilistic characterization of the BFC, which is that it is connected to both and in the same way as shown for above. As the problems get harder, the number of constraints becomes a decisive factor on the curvature. A larger value of implies more constraints and thus many long range interactions between the literals, and it also implies that edges tend to become more negatively curved. This phenomenon can be visually observed in Figure 3 (Appendix), where for smaller , larger values of are required to have highly negatively curved edges. This latter point is crucial in developing a more profound understanding of the limitations of GNN-based solvers, and we will expand upon it in the following discussion.
Message-Passing Bottlenecks and Downstream Performance.
The results presented in the previous section allow us to proceed with a principled way of understanding an important limitation for GNN-based SAT solvers. This is due to the direct connection between our result in Theorem 3.1 with Theorem 4 of toppingunderstanding, which establishes that "edges with high negative curvature are those causing the graph bottleneck and thus leading to the oversquashing phenomenon". This seminal result states that if the gradients of the message passing functions ( and in Equation 1) are bounded, and there exists a sufficiently negatively curved edge compared to the degrees of its endpoints, then the derivative of the learned node representations around that edge vanishes. Intuitively, this can be understood as a difficulty of propagating the information in nodes at a reachable distance due to the fact that the graph structure limits the pathways where information can travel: nodes in different neighborhoods need to pass all messages through the same edge. Formally, for larger values of , as the clause density , any infinitesimally small value could be used in Theorem 4 of toppingunderstanding such that , leading to an exponentially decaying Jacobian of the node representations around . This result leads us to the conclusion that GNN-based solvers are limited from two distinct hardness types: the algorithmic hardness inherent to SAT and the hardness of learning representations for long range communication. The interplay between and in Theorem 3.1 provides additional insights. Indeed, for problems with large values of or large values of , highly negatively curved edges are guaranteed to exist on average, and this quantity will concentrate. On the other hand, for large values of and relatively small values of , the latter becomes crucial in deciding how well a GNN-based solver will be able to learn, i.e., it should be easier to learn a solver for smaller values of . We confirm this fact empirically in Section 4.
The intuition we provide for a more complete understanding of the discussion above is the following: At increasing connectivity, literals become very distant on the interaction network, i.e., the number of long-range codependencies increases. In this scenario, a GNN will not be able to learn a fixed length representation that can "remember" the information of reachable, but not directly adjacent nodes. This means that the ability to learn a solver is compromised by an oversquashing phenomenon. For large values of , this problem becomes prevalent even before the hardness of exploring the solution space, due to the effect of on the BFC. Our theory motivates therefore how increasing values of in random -SAT would lead to worse oversquashing and performance, even for what would be considered simple problems in terms of . To visually see this, let us consult the level curves in Figure 3 (Appendix). As the value of grows, the gap between the flatter (yellow) and highly negatively curved problems (violet) gets smaller. The same holds for increasing values of , as expected. We provide more visual depictions of the additional implications of this phenomenon on the long-range codependencies in Appendix A.5, where we plot two input graphs for random 3-SAT at small (Figure 4) and large (Figure 5) . In the following section, we will empirically confirm our results for two different GNN-based solvers.
4 Experiments
Experimental Setting.
To validate our theory, we perform different experiments, the details of which will be provided in the respective subsections. We first explore the behavior of GNN-based solvers as a function of the input graph BFC. Based on these results, we then propose two heuristics to understand how hard a given SAT dataset will be to solve for a GNN-based solver. We focus on the assignment scenario, as it includes the decision scenario as well. Given that all the datasets we utilize do not come with node features, we use learnable embeddings in order to effectively explore oversquashing. The GNN-based solvers are implemented following the design of lig4satbench, using PyTorch [paszke2019pytorch], PyTorch-Geometric [fey2019pyg] and PyTorch Lightning [Falcon_PyTorch_Lightning_2019]. The networks were trained for 100 epochs using the AdamW optimizer [loshchilovdecoupled], with learning rate decaying by half after 50 epochs and the gradients clipped at unit norm, on NVIDIA Titan RTX GPUs.
4.1 The Relationship Between Curvature and Satisfiability
We start by using numerical simulations to verify the theoretical claims made in Section 3. To do so, we utilize the SAT benchmarks of skenderi2026benchmarking, which consist of random instances in Conjunctive Normal Form (CNF) implemented in the Julia language [bezanson2017julia]. The problems are generated with and , using steps of , thereby capturing both satisfiable and unsatisfiable regimes around the critical threshold [MertensThresholds]. Considering its widespread use and downstream performance, we train the NeuroSAT model [selsam_learning_2019] to produce a satisfying assignment, while scaling the number of message passing iterations by during evaluation, which has been shown to a good scaling regime to balance efficiency and accuracy [skenderi2026benchmarking]. We then analyze the performance of the model on problems with (for a better statistical correspondence to the theoretical setting), with the results being summarized in Figure 1. Our results show that by considering the probability of finding a solution at a given as a function of the first and second moments of the curvature, we can replicate a SAT/UNSAT phase-transition (Figure 1(b)). This result presents an important step forward in theoretically understanding the performance of GNN-based solvers. Similar results hold for random 4-SAT, and can be seen in Figures 6 and 7 in the Appendix. For this higher value of , we have more negatively curved edges which strongly impact the performance of GNN-based solvers, as will further confirmed in Section 4.2. An interesting observation is that for random 3-SAT, the curvature starts to become highly negative and concentrate close to the dynamical threshold [MertensThresholds].
Test-time Rewiring.
In order to obtain additional evidence about the previous observations, we put ourselves in a unique scenario: Suppose a GNN-based solver is trained on a dataset of SAT problems, and later tested on a separate testing partition. If we render the said testing partition less curved, would the model perform better without needing to retrain? The purpose behind this experiment is to gain a deeper understanding of the relationship between curvature and problem complexity. For this purpose, we use four different SAT benchmarks proposed by lig4satbench: Random 3 and 4 -SAT generated only near their (respective) critical thresholds , a random -SAT dataset consisting of mixed values (SR), and one that mimics the modularity and community structure of industrial problems (CA). The last two datasets are better representatives of real-world problems. We train both a Graph Convolutional Network (GCN) solver [kipf2016semi] and NeuroSAT on training partitions using the same protocol as before, while the testing partition is rewired using a stochastic discrete BFC flow [toppingunderstanding]. The idea behind the rewiring procedure is quite simple: we make the input graph less curved by stochastically deleting edges that have the highest negative curvature, while adding new edges that are less curved. We provide a more detailed explanation of this process, including a schematic algorithm in Appendix A.3. The results are reported in Table 1, where it can be observed that that the rewired problems become simpler to solve for both solvers at test-time. A noteworthy observation is that a large improvement happens on 4-SAT problems, while the modular CA dataset reports small improvements. Albeit already intuitive, we make a direct connection of this result with our theory in the following subsection.
4.2 A New Hardness Heuristic for GNN-Based Solvers
Based on the developed theory and the above observations, we provide, as a practical contribution, two different heuristics that reflect how hard it will be for a GNN-based solver to tackle a dataset. The main motivation behind these heuristics is that if we simply look at the average clause density of a dataset, we can miss out on direct implications of oversquashing. An example of this is the first dataset we presented for the random 3-SAT experiments discussed in Figure 1, which is build at increasing values of . Given an input graph , we define the heuristics as:
[TABLE]
with the expectations being taken over the edges . The averages of both heuristics, which we denote by and , can then be used to judge the hardness of a given dataset. Intuitively, we provide two non-negative numbers that reveal how dense and curved is on average () and how much this quantity concentrates (). Our theoretical insights tell us that these quantities should provide information into the hardness of learning a GNN-based solver. We report the generalization error (1 - testing accuracy) of NeuroSAT on the four previously mentioned benchmarks in Section 4.1, alongside the heuristics in Table 2. A (linear) correlation analysis between the error and the (normalized) heuristics reveals that our curvature-based approach serves as a better predictor of generalization: the respective correlation coefficients are , and .
These results allow us to formally motivate the performance gains during the test-time rewiring procedure discussed previously. What we observe, is that due to its community structure, the CA dataset has a large clause density, but its average curvature is much lower than that of random 4-SAT problems. This is natural, since a community structure is inherently linked with edges that act as less important bottlenecks for message passing [nguyen2023revisiting]. These results show that the ability of GNN-based solvers to learn representations for long range communication and generalize well is deeply connected with the curvature of the input data.
5 Conclusions
Practical Takeaways and Future Work.
In this paper, we have identified that the geometry of the input data is a plausible cause of deficiency in the performance of GNN-based SAT solvers, making connections to the oversquashing phenomenon. Tight relationships between data structure and learning are universally prevalent across all applications and as a result we have different modeling principles for different data. Our main takaway in this work is that a general purpose GNN architecture must be specialized in order to deal with SAT-specific issues, i.e., we cannot hope to learn faithful combinatorial solvers naively. What is quite fascinating is that most modern GNN-based SAT solvers implement some type of recurrence mechanism [selsam_learning_2019, ozolins_goal-aware_2022, lig4satbench, mojvzivsek2025neural], and this architectural component has been recently shown to be a great starting point to mitigate oversquashing [arroyo2025vanishing]. The effect of recurrence can be immediately noted by comparing the drop in performance between the GCN and NeuroSAT solvers in Table 1. A direct avenue for future work that we consider promising in this direction is the application of continuous graph diffusion dynamics for learning[chamberlain2021grand, han2024continuous], which can generalize the recurrence mechanism.
This above reflection leads us to conjecture that the relationship between input data and model performance is prevalent throughout Neural Combinatorial Optimization (NCO) [wang_neurocomb_2022], and different architectural designs are necessary for different problems. Furthermore, while we were able to identify a cause for the hardness of learning GNN-based SAT solvers and also provided heuristics to identify the hardness of a given dataset, we did not propose new modeling principles. One might intuitively suppose that using curvature-aware solvers [ye2019curvature, fessereffective] might provide advantages, but the concentration of the BFC would not make this conjecture plausible. We indeed verify this problem in Appendix A.4, where it can be seen that simple curvature-aware GNNs do not report consistent improvements. How to best inject curvature information in GNN-based solvers remains an open avenue for future work.
Closing Remarks.
In conclusion, our results highlight that the limitations of GNN-based SAT solvers cannot be fully understood without considering the geometric properties of the input. Our study presents, to the best of our knowledge, the first attempt at a theoretical understanding of these neural solvers, by establishing a direct connection between their negatively curved graph representations and oversquashing in GNNs. We provide empirical evidence of this connection and verify that it is prevalent on more constrained instances. Beyond SAT, we expect these insights to be valuable for other domains where graph representations of combinatorial problems are employed. Combinatorial Optimization (CO) provides an interesting venue to study the reasoning behavior of GNNs, and we hope that this paper makes a case for such studies. In conclusion, we hope that bridging concepts from deep learning, geometry, and physics, will pave the way for principled advances in the design of neural solvers.
Acknowledgements.
The author would like to thank the funding project Next Generation EU - MIUR PRIN PNRR 2022 Grant P20229PBZR provided by the European Union and MIUR. Furthermore, many thanks are due to several people that were kind enough to discuss the ideas of this work with the author, namely Dr. Sebastiano Ariosto, Dr. Enrico Ventura, and Prof. Carlo Lucibello. Finally, the views and opinions expressed are those of the author only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible.
References
Appendix A Appendix
In what follows, we provide supplementary material that complements the main manuscript. The appendix is organized as follows:
Appendix A.1 begins with background on graph Ricci Curvature (RC), where we review the Ollivier-Ricci Curvature (OC), Forman-Ricci Curvature (FC), and Balanced Forman Curvature (BFC) discretizations to give the reader an intuition for what graph RC describes. 2. 2.
In Appendix A.2, we provide the proofs of the formal statements regarding the characterization of the BFC in the easy and hard regimes of random -SAT problems. 3. 3.
Appendix A.3 describes the test-time graph rewiring procedure used in our experiments, including a full presentation of the stochastic curvature-guided algorithm. 4. 4.
In Appendix A.4, we outline preliminary ideas and implementations for curvature-aware solvers, along with empirical results that illustrate their shortcomings following the discussion in the main paper. 5. 5.
Finally, Appendix A.5 contains additional plots and visualizations that further augment the previously presented material.
A.1 Ricci curvature of graphs
In this section, we provide, for the sake of completeness, definitions and intuitive explanations of the two types of graph RC mentioned in this paper. The definitions are taken from bhattacharya2015exact and toppingunderstanding respectively, we simply report them here in a synthesized manner. We kindly refer the reader to the aforementioned works for more details.
A.1.1 Ollivier Ricci curvature (OC)
The formulation of ollivier2009ricci on graphs tries to mimic the intuition from differential geometry: we use a ratio between the amount of "mass" moved around of an edge neighborhood with the shortest path distance, i.e., the graph geodesic. We can see therefore that it is an edge-level, scalar-valued function. Edges with negative curvature act as structural bottlenecks, separating dense regions and limiting smooth information propagation. Edges with positive curvature in the other hand facilitate smooth information propagation and are indicators of community structure. Graph OC is very well studied and has being linked to properties of graph Laplacians and mixing times of Markov Chain Monte Carlo (MCMC) methods [paulin2016mixing, inagaki2025spectral]. Let us formalize this concept.
For two probability measures on a metric space , the the Wasserstein distance between them is defined as
[TABLE]
where is the collection of probability measures on with marginals and . The Wasserstein distance is the result of the solution to a famous problem called Optimal Transport [peyre2019computational]. Intuitively, this distance measures the optimal cost to move one pile of sand to another one with the same mass.
Let a metric measure space be a metric space , with a collection of probability measures indexed by the points of . The (coarse) Ricci curvature of a metric measure space is defined as follows:
Definition A.1** (Ollivier-Ricci Curvature [ollivier2009ricci]).**
Given the metric measure space , for any two distinct points , the (coarse) Ricci curvature of of is defined as:
[TABLE]
Extending this definition to graphs requires some additional steps. Consider a locally finite and possibly weighted simple graph , where each edge is assigned a positive weight . The graph is equipped with the standard shortest path graph distance , that is, for , is the length of the shortest path in connecting nodes and . For define the degree and the neighborhood . For each define a probability measure
[TABLE]
Note that these are just the transition probabilities of a weighted random walk on the vertices of . If , then considering the metric measure space , we can define the OC curvature for any edge as following Equation A.1 and discretizing Equation 9 on :
[TABLE]
denotes the set of all matrices with entries indexed by such that , , and , for all and . For a matrix , represents the mass moving from to . For this reason, the matrix is often called the transfer plan.
A.1.2 Balanced Forman curvature (BFC)
The FC is a discretization of Ricci curvature that holds for a broad class of topological objects, namely so called (regular) cellular (CW) complexes [samal2018comparative]. The original definition [forman2003bochner] is both extremely technical and out of the scope of this paper. Given that graphs edges are 1-dimensional cells (topologically), the definition simplifies greatly making use of very simple graph properties. Consider a simple, unweighted graph for simplicity, then the FC of edge is defined as . The main issue of this definition is that it ignores higher order correlations in terms of triangles and 4-cycles, which prove crucial to discriminate positively, flat, and negatively curved graphs. Inspired by these issues, toppingunderstanding propose an extension of the FC dubbed BFC, such that it is both fast to compute and encodes accurate curvature information.
Definition A.2** (toppingunderstanding).**
For any edge in a simple, unweighted graph with adjacency matrix let:
- •
be the set of 1-hop neighbors of .
- •
be the set of triangles based at .
- •
be the neighbors of forming a 4-cycle based at without diagonals inside.
- •
, with being the dot product and the elementwise product, be the maximal number of 4-cycles based at traversing a common node.
The BFC is 0 if and alternatively:
[TABLE]
A.2 Proofs
For the sake of clarity and exposition, we report here both the statements and their respective proofs.
Proposition 3.1
Define the quantity:
[TABLE]
For any edge in a simple, unweighted bipartite graph , we have that that .
Proof.
It is straightforward to see that as a direct consequence of the definition of the BFC (Def. A.2), . For the upper bound, we’ll have to consider the effects of each term in the definition. First, notice that notice that the BFC on an edge of takes a simpler form compared to the more general, original definition:
[TABLE]
This result follows from the fact that bipartite graphs have no triangles, i.e., . Our main focus for the upper bound becomes the rightmost term. Firstly note that this term is, by definition, non-negative. We can further simplify the definitions of the 4-cycle forming neighborhoods to match the bipartite topology of :
[TABLE]
By definition of it follows immediately that the cardinality of both sets is bounded above by the node degrees:
[TABLE]
Furthermore, we always have that , which gives us the upper bound:
[TABLE]
Let and such that w.l.o.g . We can then write:
[TABLE]
Note that , thus , which allows us to write . Finally, ignoring the trivial case for which by definition, we have that , which allows us to arrive at the conclusion , thereby:
[TABLE]
∎
Proposition 3.2
Let be an edge from the Literal-Clause Graph (LCG) representation of a random k-SAT problem with variables and clauses, with degree distributions given by Equations 5 and 3. Then as .
Proof.
We proceed by proving the stronger statement as , which automatically implies . A sufficient condition for proving the statement is then to show that as , given the definition of the BFC (Def. A.2). We can directly verify the probability of this event from the literal degree PMF (Eq. 5) in this limit:
[TABLE]
where , such that , which in turn implies that and as , and consequently . ∎
Lemma 3.1
Let be an edge from the LCG representation of a random k-SAT problem with variables and clauses, with degree distributions given by Equations 5 and 3. Then as .
Proof.
Ignoring the trivial case , as , we have that (see the proof of Proposition 3.2 above), therefore we can consider the lower bound as consisting only of .
Following the usual limit properties and the linearity of the expectation, we can write:
[TABLE]
By the sifting property of the delta function, we have that and therefore:
[TABLE]
The only term left in order to arrive at a conclusion is . By definition of the expectation over a PMF we can write:
[TABLE]
Letting , we have the equality , which then gives us:
[TABLE]
Note that for , we have that and , therefore by the Weierstrass M-test we have uniform convergence and thus the series can be integrated termwise, resulting in:
[TABLE]
This tell us that the expected value converges as . We now show that in the same limiting regime, the variance of the curvature lower bound vanishes, which is what we need to prove our statement. To start, notice that the variance depends entirely on the inverse literal degree term , as the others add no variance. Therefore we start from:
[TABLE]
Remember that the edge-sampled literal degree PMF allows us to see the latter as a variable which . Let us consider the expectation over two disjoint event collections: and . The idea behind this procedure is simply to analyze how the desired expectation behaves in a more "likely" scenario and in a tail scenario.
For , since , and , which finally implies . We can therefore write:
[TABLE]
where is an indicator function. 2. 2.
For , we can use the crude bound , wich implies that . Posed in this way, we can see that it is possible to apply a Chernoff bound on this probability, by letting and remembering that , to obtain:
[TABLE]
which implies that .
We can now separate the expectation, i.e., express it using partial expectations on or :
[TABLE]
from which it is straightforward too observe a convergence to 0 since variance is always non-negative and . We therefore have convergence at a finite expected value with the variance shrinking to 0, which implies that as .
∎
Theorem 3.1
Let be an edge from the LCG representation of a random k-SAT problem with variables and clauses, with degree distributions given by Equations 5 and 3. Let be the neighbors of forming a 4-cycle based at , without diagonals inside. The BFC at is bounded from above by the quantity:
[TABLE]
Furthermore, in the limit , fixed, , and , .
Proof.
We first prove the construction of the upper bound, which we can then use to prove the convergence via sandwiching upon the lower bound shown to converge in Lemma 3.1. We remind the reader that from the proof of Proposition 3.1 we have seen the term which constitutes the difference between and is:
[TABLE]
As another reminder, note that the definition of can also be simplified, always as a consequence of the topology of . Consider first the symmetric adjacency matrix of a bipartite graph, given by:
[TABLE]
where is an incidence matrix with if there if , and otherwise, is the transpose of (which ensures that is symmetric), and are zero blocks of size and corresponding to the absence of edges within the partitions. We can thus express as:
[TABLE]
since . The operation returns the number of common neighbors that nodes and have, with and being in the same partition. At this point, we can distinguish between two cases:
Case 1: No 4-cycles.
In this case, such that , therefore and by Lemma 3.1 we obtain as .
Case 2: Presence of 4-cycles.
Firstly, note that we can again use the crude bound of the form . Furthermore, since if , while . This gives us an upper bound on the four cycle correction term:
[TABLE]
which automatically provides We now inspect the final two terms separately. For the rightmost one, we have that
[TABLE]
due to the fact that as proved in Lemma 3.1. From the same previous result, given that , we have that the variance vanishes as . Therefore, as .
We are now left with the final term, for which we need to make some additional considerations. In particular, we’ll closely inspect the set and provide a combinatorial argument for its behavior. Let us start by asking what is the probability that a random clause containing shares at least one other literal with . For a given value of we will denote this by . For the edge with , there are candidate clauses that can belong in , which means can be any of these nodes. Then, the inclusion of in the set depends on whether there exists at least a literal which shares with that is not . Equivalently, we want to understand the probability of any of ’s other literals being among the remaining literals of .
Let us flip the problem and ask ourselves about the probability of no cycle overlap first: this implies that clause has to choose literals out of , given that out of the available literals, the present in clause must be ignored. On the other hand, given that each clause chooses distinct literals uniformly, there are literals, ignoring , that can be a part of out of total. Using the aforementioned logic, the probability of no overlap for any candidate clause can be written as:
[TABLE]
At this point, we can make a scaling argument by using the sparsity that the assumed asymptotic regime offers, given that we consider the graphs to have fixed while , such that . This allows us to consider and therefore .
Remember that for the edge with , there are candidate clauses that can belong in , therefore by conditioning and a simple counting argument we can write:
[TABLE]
Note that this bound is constant in , therefore by the law of total expectation we have that:
[TABLE]
Given that the quantity we can apply Markov’s inequality to obtain, for any :
[TABLE]
This result is particularly insightful, because it shows that the behavior of the term does not depend explicitly on , but it is in fact the appropriate scaling regime (i.e., the thermodynamic limit with k fixed) that induces sparsity and therefore diminishes the overlap probability. Nevertheless, given we work in this regime, we can overload notation somewhat and write that as .
Finally, because , and both and as , we can conclude that as .
∎
A.3 Details on Test-Time Rewiring
Graph rewiring is the process of modifying a graph’s connectivity by adding, removing, or re-weighting edges, typically to optimize information flow. In our case, we make use of the rewiring procedure presented by toppingunderstanding, which consists of a discrete and stochastic Ricci flow, guided by the BFC. At each iteration, the edge with the most negative curvature (i.e., the structurally most “strained” connection) is identified. Candidate rewiring edges are then generated between the neighborhoods of the two endpoints of this edge. A new edge is stochastically selected either at random (with probability ) or by maximizing the curvature improvement obtained from its addition. The selected edge is added to the graph and the corresponding curvature values are updated. By repeating this procedure for a fixed number of iterations, the algorithm progressively increases the average curvature of the graph, yielding a rewired version that contains information bottlenecks that are weaker compared to the input. Algorithm 1 contains the pseudocode for our rewiring algorithm. We would like to stress here that this modifies the constraints of the Boolean Satisfiability Problem (SAT) problem under consideration, but the goal of this procedure is to show that "flatter" problems will in fact be easier to solver for Graph Neural Network (GNN)-based solvers even without retraining.
A.4 Some initial ideas for curvature-aware solvers
As discussed during the conclusion, we showed that the graph BFC displays concentration to particular constants with high probability. This result makes it legitimate to conjecture that using a curvature-aware message passing procedure naively would not lead to stable performance benefits. In this section, we provide some starting points and experiments to confirm this conjecture. The goal of our implementations was to maintain efficiency and rely on straightforward ideas that could lead to performance improvements. For these purposes, we introduce two simple curvature-aware variants of message passing. The first is an adaptation of ye2019curvature, where the curvature of an edge is used to learn a gating mechanism that modulates message contributions. The second is a simple recurrent extension of fessereffective, where the statistics of the curvature around each node are used as additional features at each recurrent step. Our empirical findings reveal that naively injecting curvature into GNN-based solvers sometimes leads to improved performance, but it does not always provide clear advantages, as seen in Table 3. While we believe that both these implementations provide interesting starting points for future work and research, another direction is understanding how to effectively alter the curvature in data space, in a way that is compatible with SAT problems.
A.5 Additional plots
In this section we provide additional and miscellaneous plot that help with visualizing various concepts explained in the main manuscript, such as the relationship between curvature and hardness, as well as visualizations of easy and hard problems. More details can be found in Figures 3, 4, 5 and 6.
