On the Expressive Power of GNNs for Boolean Satisfiability

AI summary

Overview

• Research area: Machine learning for automated reasoning — specifically, the theory of graph neural networks (GNNs) applied to Boolean Satisfiability (SAT), analyzed through the Weisfeiler-Leman (WL) graph isomorphism test.
• Technical level: Advanced. The paper assumes familiarity with graph neural networks, message passing, the k-WL hierarchy, and SAT terminology, though the prose explains each concept.
• Scope: A combined theoretical and empirical study asking whether WL-bounded GNNs have enough expressive power to distinguish satisfiable from unsatisfiable Boolean formulas and to predict satisfying assignments.

What This Paper Is About

GNNs are the dominant architecture for learning-based SAT solving because Boolean formulas map naturally onto graphs, but GNNs can only distinguish graph structures that the Weisfeiler-Leman test can distinguish. This paper asks the fundamental question of whether that expressive ceiling is high enough to reason about satisfiability itself. It answers with a combination of impossibility proofs, positive results for special instance families, and experiments on benchmark SAT instances.

Key Contributions

1. An impossibility result at the top of the WL hierarchy. The authors construct pairs of 3-SAT formulas with O(n) variables and O(n) clauses that are indistinguishable by the n-WL test, even though one is satisfiable and the other is not (Theorem 5.3). The construction adapts the classic graph construction of Cai et al. (1992) into the domain of Boolean formulas, using formulas that encode the existence of an even orientation of a graph.

2. Transfer of the limitation to sequential solvers. Lemma 5.4 shows that for formulas whose LCNs are indistinguishable by k-WL (k ≥ 4), any partial assignment of at most ⌊k/2⌋ − 1 variables in one formula has a counterpart partial assignment in the other such that the residual formulas remain WL-indistinguishable. Corollary 5.5 concludes that WL-powerful GNNs cannot distinguish a satisfiable residual formula from an unsatisfiable one even with Θ(n) variable assignments.

3. A new NP-complete but WL-invisible family. The paper introduces 3-regular SAT (each literal appears in exactly k clauses, each clause has exactly k literals) and proves it is NP-complete (Theorem 5.1), while showing that the WL test does not distinguish any two 3-regular SAT formulas with the same number of variables (Observation 5.2).

4. Positive distinguishability results plus an empirical expressive-power test. PlanarSAT is shown to be fully identified by the 4-WL test (Theorem 6.1), and formulas extracted from uniformly random literal-incidence graphs are identified by WL with probability at least 1 − n^(−1/7) (Theorem 6.3). Experiments then measure which real instances are within WL's reach.

Main Findings

• The full WL hierarchy fails for SAT in general. There exist 3-SAT formula pairs with O(n) variables and O(n) clauses that are n-WL-indistinguishable, one satisfiable and one not. The paper notes an apparent connection between this construction and Tseitin formulas, which are hard for resolution refutation — both settings contain a global inconsistency invisible to purely local reasoning.

• Restarts and sequential variable assignment do not rescue WL-bounded solvers. Even with Θ(n) assignments, the satisfiability of the residual formula can remain undecidable for a WL-powerful architecture (Corollary 5.5), which the authors state applies to solvers that assign variables sequentially such as QuerySAT.

• 3-regular SAT is hard but invisible to WL. The class is NP-complete, yet all instances of the same size are indistinguishable, making WL-powerful GNNs essentially useless on it. The paper provides its own proof of NP-completeness since it could not find a formal proof of this specific variant.

• Planarity helps decisively. Every SAT formula has an equisatisfiable PlanarSAT equivalent with polynomially many variables and clauses, and the 4-WL test distinguishes it from any other formula. The catch is practical: the reduction replaces each edge crossing with a gadget adding 9 variables and 20 clauses, and there can be up to O(n²) crossings.

• Random formulas are largely within WL's reach. WL converges in about 3 or 4 rounds on random instances, and in roughly 40% of all formulas WL assigns every literal a unique identifier. Only a small fraction resisted: 2.0% of the k-clique family and 0.3% of the k-vercov family. The paper explains the 3-round pattern via the constant degree of 3-SAT clauses: iteration one reveals literal degrees, iteration two does not refine anything because clauses all have degree 3, and only iteration three lets literals observe other literals in shared clauses.

• Industrial and crafted instances often exceed WL's power. Out of 448 evaluated competition instances, only 234 could be solved within WL's expressive power, and across 69 instance families, 38 contained instances where WL is not expressive enough. Families such as heule-nol, a grid-coloring problem, resisted because their regular structure makes literals hard to distinguish.

• Round counts are much higher on competition data. Notable examples include cryptography instances (r_crit 15.74 ± 14.67, r_converged 17.63 ± 14.34, 41,510 ± 29,705 variables, 19 instances) versus random 3-SAT easy instances (r_crit 2.97 ± 0.18, r_converged 3.68 ± 0.47, 26 ± 9 variables). Several families, including circuit-multiplier, heule-folkman, and heule-nol, produced no satisfiable augmented formula at any round and are reported as "unsat."

• Two graph representations matter for the analysis. The literal-clause graph (LCG) connects literals to clauses, but the authors argue that literal-literal negation edges must be added — giving the literal-clause graph with negation connections (LCN) — because otherwise information is lost once node labels are removed for permutation invariance. They show an unlabeled LCN uniquely determines the SAT formula up to isomorphism (Observation 3.1), whereas the literal-incidence graph (LIG) and clause-incidence graph (CIG) are lossy and the variable-clause graph (VCG) is unsuitable because one formula can have non-isomorphic VCG representations.

Methodology in Plain English

The authors split the work into theory and experiment.

For the theory, they formalize how a Boolean formula becomes a graph (the LCN representation) so that two formulas can be called "isomorphic" only when the mapping preserves clauses and the literal-negation pairing. They then borrow a known pair of graphs that the n-WL test cannot tell apart and translate those graphs into Boolean formulas by making variables encode edge orientations, so that satisfying assignments correspond to even orientations. Depending on a parity condition, one formula of the pair is satisfiable and the other is not. Further proofs handle the sequential-assignment case, prove hardness of the 3-regular family, and import known results on planar and random graphs.

For the experiments, they use a clean operational proxy for expressive power. If a GNN predicts a value per literal, then literals that WL cannot tell apart must receive the same predicted value. So for each satisfiable formula they run WL for r rounds, group literals into WL-equivalence classes, and add clauses forcing all literals in a class to be equal. The augmented formula can still be satisfiable only if a WL-bounded model could in principle output a satisfying assignment within r rounds. They sweep r from 1 to the round at which WL converges and record the smallest r where the augmented formula is satisfiable, labeling it r_crit; if no such r exists, they conclude WL is not powerful enough for that instance. They ran this on random instances from the G4SAT benchmark and on industrial and crafted instances from the International SAT Competition from 2020 to 2025, filtering to instances under 10 MB because competition instances range from a few hundred to 50 million variables.

Why This Matters

The paper draws a sharp line between what is achievable with WL-bounded architectures and what is not, and it does so at the level of the full WL hierarchy rather than a fixed k. This matters for research because it separates two things that are often conflated: computational hardness (SAT is NP-complete) and expressivity limits. The authors explicitly call out that conflating them is a misconception, noting that PlanarSAT is NP-complete yet fully distinguishable by 4-WL. The result also forges a link to proof complexity, connecting the Cai et al. construction to Tseitin formulas as instances with global inconsistencies that local reasoning cannot detect.

Real-world applications that depend on the reasoning about satisfiability:

• Hardware design and equivalence checking, which appears among the competition instance families evaluated (circuit-multiplier).
• Scheduling, listed as one of the applications represented in the competition datasets.
• Cryptography, whose instances proved among the hardest for WL in the experiments.
• Automated reasoning pipelines and verification tooling, where learned heuristics such as branching, restarts, and clause deletion are increasingly considered.

Industry relevance: the experiments show that the instance distributions most common in practice — industrial and crafted formulas — are exactly the ones where WL-bounded GNNs frequently lack the expressive power to even represent a satisfying assignment. The finding that random instances are largely distinguishable while industrial ones often are not is a caution for the common practice of training learning-based SAT solvers on random formulas because they are easy to generate.

Future Directions

1. Apply GNNs to industrial instances. The authors explicitly hope for this, while acknowledging the obstacles: a lack of scalable generators and the large size of many industrial instances. They argue these instances would be a structurally richer testbed that could reveal generalization behavior hidden by random distributions.

2. Close the gap between necessary and sufficient expressive power. The experimental setup tests only whether WL has the necessary expressivity to represent a satisfying assignment; it does not test whether that expressivity is sufficient for generalizable learning. Even on random formulas, better generalization may require higher-order GNNs or symmetry-breaking techniques.

3. Handle families where WL provably fails. Instance families like 3-regular SAT and the k-clique and k-vercov cases with unresolvable symmetries are outside the reach of WL-bounded models; mechanisms to break these symmetries or higher-order architectures remain open.

4. Revisit practical reductions such as PlanarSAT. The planarity result gives full expressivity at 4-WL, but the reduction's cost (9 variables and 20 clauses per crossing gadget, up to O(n²) crossings) makes it impractical and leaves room for more efficient encodings.

Target Audience

Researchers working at the intersection of graph representation learning and automated reasoning, especially those designing GNN-based SAT solvers or evaluating learned heuristics for CDCL-style solvers. It is also useful for theoreticians interested in the Weisfeiler-Leman hierarchy, finite model theory, or the links between graph isomorphism testing and proof complexity. Practitioners applying learned models to industrial verification, scheduling, or cryptographic instances will find the empirical results directly relevant, though they should expect to engage with the theory given the paper's level of formalism.

Authors’ abstract

Machine learning approaches to solving Boolean Satisfiability (SAT) aim to replace handcrafted heuristics with learning-based models. Graph Neural Networks have emerged as the main architecture for SAT solving, due to the natural graph representation of Boolean formulas. We analyze the expressive power of GNNs for SAT solving through the lens of the Weisfeiler-Leman (WL) test. As our main result, we prove that the full WL hierarchy cannot, in general, distinguish between satisfiable and unsatisfiable instances. We show that indistinguishability under higher-order WL carries over to practical limitations for WL-bounded solvers that set variables sequentially. We further study the expressivity required for several important families of SAT instances, including regular, random and planar instances. To quantify expressivity needs in practice, we conduct experiments on random instances from the G4SAT benchmark and industrial instances from the International SAT Competition. Our results suggest that while random instances are largely distinguishable, industrial instances often require more expressivity to predict a satisfying assignment.