Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Expressive Power of GNNs for Boolean Satisfiability

Saku Peltonen, Roger Wattenhofer

TL;DR

This work establishes fundamental limits on the expressivity of GNNs for SAT solving by analyzing them through the Weisfeiler-Leman hierarchy, proving that the full WL framework cannot universally distinguish satisfiable from unsatisfiable formulas. It identifies both hard and easy subfamilies: 3-regular SAT and k-WL indistinguishable instances resist WL-based discrimination, while PlanarSAT is fully identified by 4-WL and random-SAT instances are largely WL-identifiable. The authors corroborate these findings experimentally on G4SAT and SAT Competition data, showing random instances are often distinguishable with few WL iterations, whereas industrial instances may require greater expressivity or remain unsolved by WL-bound architectures. The results bridge theory and practice, linking WL indistinguishability to sequential solving limitations and highlighting avenues for more expressive GNN designs or alternative strategies. Overall, the paper clarifies when WL-powered GNNs can be effective for SAT and where they fundamentally fail, guiding future architectural and dataset considerations for learning-based SAT solvers.

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.

On the Expressive Power of GNNs for Boolean Satisfiability

TL;DR

This work establishes fundamental limits on the expressivity of GNNs for SAT solving by analyzing them through the Weisfeiler-Leman hierarchy, proving that the full WL framework cannot universally distinguish satisfiable from unsatisfiable formulas. It identifies both hard and easy subfamilies: 3-regular SAT and k-WL indistinguishable instances resist WL-based discrimination, while PlanarSAT is fully identified by 4-WL and random-SAT instances are largely WL-identifiable. The authors corroborate these findings experimentally on G4SAT and SAT Competition data, showing random instances are often distinguishable with few WL iterations, whereas industrial instances may require greater expressivity or remain unsolved by WL-bound architectures. The results bridge theory and practice, linking WL indistinguishability to sequential solving limitations and highlighting avenues for more expressive GNN designs or alternative strategies. Overall, the paper clarifies when WL-powered GNNs can be effective for SAT and where they fundamentally fail, guiding future architectural and dataset considerations for learning-based SAT solvers.

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.
Paper Structure (32 sections, 21 theorems, 8 equations, 4 figures, 3 tables)

This paper contains 32 sections, 21 theorems, 8 equations, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Graph representations of SAT formulas
  4. Related work
  5. Indistinguishable families of SAT instances
  6. 3-regular SAT
  7. k-WL indistinguishable SAT instances
  8. Positive results for distinguishability
  9. Planar SAT
  10. Random SAT instances
  11. Experiments
  12. Setup
  13. Datasets
  14. Results
  15. SAT Competition Instances.
  16. ...and 17 more sections

Key Result

Theorem 5.1

3-regular SAT is NP-complete.

Figures (4)

  • Figure 1: Literal-clause graph with negation connections ($\mathrm{LCN}$) of a formula $f$. Removing the literal-literal edges represented by dashed lines gives the literal-clause graph ($\mathrm{LCG}$).
  • Figure 2: $\mathrm{LCN}$s of $f$ and $f'$. The difference between the formulas is highlighted in bold. Removing the literal-literal edges represented by the dashed lines gives the literal-clause graphs.
  • Figure 3: An $\mathrm{LCN}$ of the formula $X_3$, corresponding to the graph $X_3$ in the CFI construction. Literal nodes are circled. The clauses are connected to the literals by solid lines.
  • Figure 4: Constructions in the formula $f_G$ and $\tilde{f}_G$ for an edge $\{v,w\} \in E(G)$. The edges are represented vertically, with the top ellipse corresponding to $v$'s side and the bottom to $w$'s side of the edge. Solid lines connect clauses to their literals. Dashed lines connect literals and their negations.

Theorems & Definitions (41)

  • Definition 2.1: Weisfeiler-Leman algorithm
  • Definition 2.2: $k$-dimensional WL algorithm
  • Remark 2.3
  • Theorem 5.1
  • Theorem 5.3
  • Lemma 5.3
  • Corollary 5.3
  • Theorem 6.1
  • Lemma 6.2: LIGextraction
  • Theorem 6.3
  • ...and 31 more