On the Expressive Power of GNNs for Boolean Satisfiability

• URL: http://arxiv.org/abs/2602.08745v1
• Date: Mon, 09 Feb 2026 14:48:16 GMT
• Title: On the Expressive Power of GNNs for Boolean Satisfiability
• Authors: Saku Peltonen, Roger Wattenhofer,
• Abstract summary: We analyze the expressive power of Graph Neural Networks for solving Boolean Satisfiability (SAT)<n>We show that indistinguishability under higher-order WL carries over to practical limitations for WL-bounded solvers that set variables sequentially.<n>Our results suggest that while random instances are largely distinguishable, industrial instances often require more expressivity to predict a satisfying assignment.
• Score: 34.662213518530315
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  We present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances. We enrich the graph representation with domain-specific decisions, such as novel node feature design. We demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime.
  arXiv  Detail & Related papers  (2024-05-17T18:00:50Z)
• Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
  We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments. Experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.
  arXiv  Detail & Related papers  (2023-04-18T05:33:33Z)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  W2SAT is a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances. We introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability. Decoding from WLIG into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method.
  arXiv  Detail & Related papers  (2023-02-01T06:30:41Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem. DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions.
  arXiv  Detail & Related papers  (2022-05-27T03:20:42Z)
• Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness [68.97830259849086]
  Most datasets only capture a simpler subproblem and likely suffer from spurious features. We study adversarial robustness - a local generalization property - to reveal hard, model-specific instances and spurious features. Unlike in other applications, where perturbation models are designed around subjective notions of imperceptibility, our perturbation models are efficient and sound. Surprisingly, with such perturbations, a sufficiently expressive neural solver does not suffer from the limitations of the accuracy-robustness trade-off common in supervised learning.
  arXiv  Detail & Related papers  (2021-10-21T07:28:11Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Improving Graph Neural Network Expressivity via Subgraph Isomorphism Counting [63.04999833264299]
  "Graph Substructure Networks" (GSN) is a topologically-aware message passing scheme based on substructure encoding. We show that it is strictly more expressive than the Weisfeiler-Leman (WL) graph isomorphism test. We perform an extensive evaluation on graph classification and regression tasks and obtain state-of-the-art results in diverse real-world settings.
  arXiv  Detail & Related papers  (2020-06-16T15:30:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.