On the Expressive Power of GNNs for Boolean Satisfiability
Authors: Saku Peltonen
Roger Wattenhofer
Venue: ICLR 2026 Poster (2026)
Keywords: SAT
GNN
Weisfeiler-Leman
expressivity
Primary area: learning on graphs and other geometries & topologies
TL;DR: We study the expressive power of GNNs for SAT solving, showing that even the full Weisfeiler-Leman hierarchy cannot distinguish satisfiable instances from unsatisfiable, and that industrial instances often require more expressivity than random ones.

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 2024 SAT competition. Our results suggest that while random instances are largely distinguishable, industrial instances often require more expressivity to predict a satisfying assignment.

Published as a conference paper at ICLR 2026
ON THE EXPRESSIVE POWER OF GNNS FOR BOOLEAN SATISHIABILITY
Saku Peltonen
Roger Wattenhofer
ETH Zürich
ETH Zürich
Zürich, Switzerland spelttoeenetth.cd
Zürich, Switzerland
wettenhoofer@eth...
ABSTRACT
Machine learning approaches to solving Boolean Satisfiability (SAT) aim to re- place 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 Weiseeiler-Leman (WL) test. As our main result, we prove that full WI. hierarchy cannot, in general, distinguish between satisfiable and unsatisfiable instances. We show that indistinguishabiliy 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 in- stances. To quantify expressivity needs in practice, conduct experiments 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 satisfying assignment.
INTRODUCTION
Boolean Satisfiability (SAT) is a central reasoning problem in computer science and one of the canonical NP-complete problems. Classic SAT solvers are highly optimized and can handle stances with millions of variables (Heule et al., 2024). Part of their success comes from carefully engineered heuristics, such as branching and restart strategies (Moskewicz et al. 2001 Biere 2008), conflict-driven clause learning (CDCL) (Silva & Sakallah 1996), and learned clause management (Audemard Simon 2009). These heuristics are based on recurring patterns that differ across distributions: CDCL solvers effective on industrial instances with strong community structure (Ansótegui et al. 2012), whereas look-ahead solvers are better suited for random instances (Alyahya al. 2022). However, designing distributtoon-specifee heuristics is time-consuming and requires pertise in the field.
Machine learning offers a promising alternative, where heuristics can be learned from data. Graph Neural Networks (GNNs) (Scarselli et al. 2008 Kipi 2016 Xu et al. 2018) have become the main architecture for learning-basee SAT solving (Guo al.) (023), since formulas can be naturally ex- pressed as graphs. A common choice is the Literal Clause Graph (LCG), where literals are connected clauses bipartite graph (see Figure 2 for an example). Existing GNN methods range from
end-to-end SAT solvers, such as NeuroS AT (Selsam et al.] 2019) and QuerySAT (Ozolins et al.
2022.. to hybrid approaches that augment components classic solvers (Wang et al., 2024 Guo
al. 2023).
However, GNNs are inherently limited in their expressive power (Xu et al. 2019 that is, their ability to distinguish different graph structures. The expressive power of GNNs is characterized by the Weisfeiler-Lemar (WL) test (Weisfeiler & Lehman, 1968), and the extended k-WL hierarchy Immerman & Lander 1990). which provide universal limits which graphs GNNs can distin- guish. In particular, any GNN bounded by the WL hierarchy produces identical outputs on graphs that are WL--equivalent (Xu et al. 2019). This poses a concrete limitation in the context of SAT,

---

Published as a conference paper at ICLR 2026
C6
12
Tt
f = A (a) x2) (~r, -x2) (a2 V za) (~x2 -zx) A (2) V-ra)
Figure 1: Literal-clause graph with negation connections (LCN) of formula f. Removing the
literal-literal edges represented by dashed lines gives the literal-clause graph (LCG).
where solving relies uncovering structural patterns in graphs representing formulas. This raises a fundamental question: Are GNNs expressive enough to reason about satisfiability?
Our main result shows that even the full Weisfeiler-Leman hierarchy cannot, in general, distinguish satisfiable from unsatisfiable formulas. Specifically, we construct pairs of 3-SAT instances with O(n) variables indistinguishable under the n-WL despite one being satisfiable and the other unsatisfiable (Theorem 5.3 This result mirrors the classic construction of Cai et al. (1992) in the context of boolean formulas, demonstrating that indistinguishable formulas may also differ in satisfiability. This has practical implications for solvers that assign variables sequentially, such as QuerySAT (Ozolins et 2022). Even with ((n) variable assignments, satisfiability the residual formula may remain undecidable with a WL-powerful architecture? (Lemma [5.4 Corollary 5.5 This result notable because transfers a theoretical limitation (k-WL indistinguishabiliyy to realistic computational setting.
We analyze regular, planar, and random SAT instances to examine how expressivity requirements vary across familics. In RegularSAT family which introduce and show is NP NP-complete aal instances of the same size are indistinguishable, making WL-powerful GNNs essentially useless. In contrast, PlanarSAT is fully identified by the 4-WL test (Theorem 6.1..
Similarly, we argue that random SAT instances are largely distinguishable by the WL test, mirror- ing behavior observed in graph isomorphism testing (Babai et al. 1980). We prove this formally Interestingly, for formulas generated using the method of Wu & Ramanujan (2021) (Lemma
learning-based SAT solvers are often trained random instances, primarily because they are easy to generate (Li et al. 2024). While both random and industrial instances can be hard in the tradi- tional sense, they differ significantly in structure (Alyahya al., 2022]. Our results show that these instance families also differ in the level of expressivity required to solve them.
We quantify this difference experimentally. We test whether WL-powerful GNNs can theoretically distinguish literals sufficiently to predict satisfying assignment. For datasets, we use random in- stances from the G4SAT benehmark (Li et al., 2024) as well industrial and crafted instances from the International SAT competition (Heule et al. 2024). In general, literals in random instances are quickly distinguished. In contrast, competition instances often require more iterations, and some- times WI--powerful GNNs are simply not expressive enough to predict satisfying assignment. This confirms that industrial and crafted instances pose greater challenge from the perspective of expressivity.
2 PRELIMINARIES
Boolean satistiability. Let 2 . denote variables in a propositional logic. A literal & is vari- able x or its negation -r. A clause e (fi....,ee } is a set of literals, representing the disjunction l V... V lg. A formula ff in Conjunetive Normal Form (CNF) is set of clauses {ci,.... Cm }. representing the conjunction e A sets, depending on the context. Let L(f) = Uces Lite be the set of all literals in formula. The Boolean Satisfiability Problem (SAT) is defined follows: given formula f. check whether is
Cm- We write f as a logical formula Nces Viee l or as
common misconception that such indistinguishable instances must exist, because SAT is NP-hard. Appendix[iexplains why expressivity and computational hardness are unrelated in this way. GGNNs with expressive power matching the Weisfeiler-L.cme test, such (Xu al. 2019
2

---

Published as a conference paper at ICLR 2026
satisfiable. 3-SAT is the SAT problem where each formula is in CNF and each clause consists of most 3 literals.
Graph Notation. A graph G' is a tuple (V, E). If the graph is not clear from context. we write ((G) and E(G). All graphs are undirected unless otherwise specified. N (o) denotes the set of neighbors of node and d((u) = [N)) is the degree of v. On a directed graph d denotes the outdegree of a node. A node coloring is a function Av V + C where C is a set of colors. Similarly, an edge coloring is function λœ= E + C. On edge-colored graphs we write Ne(v) = {w E V(G): Hv, w/ E E(G) s.t. AE([v, w)) c} for the neighbors of through edges of color c.
Isomorphism. Two graphs G and H are isomorphic if there exists bijection : V(GG) V(H) such that {u, w E E(G) iff (w)) E E(H). On graphs with a node-coloring (cg. Cи for G, H, respectively) we also require that ca(o) extended for edge-colored graphs in the natural way.
for all v E V(G). The definition is
Two CNF formulas f.g are isomorphic there are bijections dg : L(f) + L(g) and oe : f g such that (1.) [z(= (() for all & E L(f), i.. TL preserves the relationship between literal and its negation, and (2.) (c(c) = (f) EE c} for all f.
Graph Neural Networks. We focus on Message Passing Neural Networks (MPNNs) which encap- sulate the majority of GNN architectures. Nodes have some initial features s E Rd. An MPNN operates in synchronous rounds, which are typically structured as follows. In each round 1 I E S I, every node aggregates the states of its neighbors, a' = agg( ((s : w E (())))) where {(-}] de- notes multiset. The nodes update their state using their previous state and the aggregated messages: sf = upd(s" !-1 a.). The functions agg and upd are differentiable functions typically parameterized by neural networks. The final representations s/ can be used for node-level prediction tasks, or they can be aggregated into a graph-level representation.
Weisfeiler-Leman Test. The expressive power of MPNNs is bounded by the Weisfeiler-Leman (WL) algorithm, also known as color refinement:
algorithm). Let \v : V(G) + be a vertex coloring. The WL algorithm computes new colorings of the graph iteratively. The initial coloring is given by x ;= Av. For e E N, a new coloring x" is defined as ('()) := (x" (w). Uxx 1 (w) : w E (v)))). The color refinement is continued until the partition of nodes given by X equals the partition given by x f+1, The output of the WL algorithm is the stable coloring x
Definition 2.1 (Weisfeiler-
The WL algorithm can be generalized to also an edge-coloring dE E(G) + Cg. The update considers each color class of edges separately: (") == (x' (v). (IxN. : c E Cx where XN. = ((xx-1(w) w Ne(v)] are the colors of neighbors through edges of color c.
separateee
In the Weisfeiler-Leman test, the WL algorithm is applied to the disjoint union of G and G". The WL test distinguishes G and G' if there is a color e such that the sets {u : v E V(G), x(v) = c), {o E VVG"), x(v) c} have different cardinalities. We say that graph G is identified by WL is distinguished from every other non-isomorphic graph H. A class of graphs K is identified if every graph in IC is distinguished from every other non-isomorphic graph H (possibly H of K).
k- Weisfeiler Leman Test. Let & 2 2 be an integer. The atomic type of tuple T E (G) encodes all facts about edge connections and colors within the tuple. Two tuples e E V(G)*, u E V(G')* have the same atomic type and only if the mapping U; + us is an isomorphism of the induced colored subgraph Gl[vi,..., ux]] G[[ui,..,, J.
Definition 2.2 (A-dimensional WL algorithm). The k- WWiisfeiler-Lemaa (k-WL) algorithm ini- tializes x (T) as the atomic type of V for each T E V(G)* For i E N, a new col- (v), xf-'(()) where x = oring x" is defined as (T) = (T), ( (v). Xe (x).xe
(x Ui-1, u, U1-12..... U&) u E V(G)). The color refinement is continued until the partition of tuples given by x equals the partition given by x(+1. The output of the WI algorithm is the stable coloring x The k-dimensional WL test is defined analogously to the WL test. We say that G and G' are distinguished if there exists color e such that the sets {U: U V(G)* x(T) = c) and {ū: T E (G"),x(() = c} have different cardinalities.
Remark 2.3. There are two algorithms and naming conventions in the literature. This version of the k- algorithm is most common in machine learning literature. Through connections to counting
3

---

Published as a conference paper at ICLR 2026
logic, it can be shown (Groh 2017 to be equivalent (k - 1)-WL, as defined in for example CCai et al. 1992.
Kiefer et al. 2019). See (Huang & Villar 2021 for an overview.
GRAPH REPRESENTATIONS OF SAT FORMULAS
standard way represent SAT formulas as graphs is the literal-clause graph (LCG). The LCG is bipartite graph with literals on one side and clauses on the other. Edges connect literals to clauses where they appear. See Figure for an example.
In GNNs, node labels of graph are omitted to preserve permutation invariance. To avoid informa- tion loss, it is essential to include edges between literals and their negations We call the extended representation the literal-clause graph with negation connections (LCN). It is defined the LCG with additional edges connecting each variable to its negation. The literal-literal edges are assigned distinet color from the literal-clause edges. The LCN of CNF formula f is denoted LCN(f).
Literal-literza edges is necessary to preserve information once labels are removed (see Appendix for example). The LCN representation is also sufficient to preserve all information:
Observation 3.1. An LCN without node labels uniquely determines the corresponding SAT formula up to isomorphism. The formula can be constructed by grouping nodes into variable pairs according the literal-literal edges, labeling them arbitrarily as Fs: - and reading clauses from the literal- clause edges.
Other representations include the variable-clause graph (VCG) and less common literal- -iniidenc graph (LIG) and cttuse-incidenc graph (CIG). We focus on the LCN in this work, as the LIG and CIG representations lossy, and VCG is not suitable for expressivity analysis because the same formula (up to isomorphism) can have -on-isomorppic VCG representations. See Appendix A for details.
4 RELATED WORK
Machine Learning for SAT. One of the earliest works in this area is NeuroSAT (Selsam et al., 2019) an end-to-end SAT solver framework with GNNs. Their algorithm is based on predicting satisfiability, and hence works with single-bit supervision. QuerySAT (Ozolins et al.! 2022)
unsupervised loss computed from continuous variable values, and query mechanism to update the variable values. Other approaches include transformer-based models such SATformer (Shi al., 2023) and attention- -based variants like SAT-GATv2 (Chang & Liu (025). In a complementary line of work, Yolcu & Póczos (2019) build a local search SAT solver whose variable selection strategy is learned by GNN. Several of these architectures and losses can be evaluated on the G4SAT benchmark (Li et al. 2024).
The end-to-end SAT solvers are mostly of methodological interest, and currently not practical for large instances. Another line rescarch augments classic SAT solvers with machine learning com- ponents, such as learned heuristics branching strategies. [Selsam & Bjørner (2019) adapt the AT architecture to predict unsatisfiability cores, which is used to select branching variables. Other SAT solving components with potential for ML solutions include variable initialization (Wu) 2017)
clause deletion (Vaezipoor et al., 2020) and restart policy (Liang et al.] (0188). See (Guo)
al.
2023 for a comprehensive survey on machine learning methods in SAT solving.
Dataset generation is another promising application area. To mimic industrial SAT instances, Wu learning-based graph representation and design method to generate SAT instances from their implicit model. Another line of work frames SAT generation as a bipartite graph generation problem (You al. 2019).
& Ramanujan (2021)
Expressivity and the Weisfeiler-Lemaa test. It is well known that the Weisfeiler-Leman test bounds the expressive power of MPNNs (Xu al. 2019). This limitation has motivated a large number of more expressive GNN architectures, with expressivity corresponding to k- WL for some
31 iteral-literal edges are already used in practice in most GNN SAT solvers (elsam et al. but their importance is always stated explicitly.
2019 Li et al.
2024
4

---

Published as a conference paper at ICLR 2026
k. > 2 (Morris et al.
2019 Maron et al. 2019 Keriven & Peyré 2019). A comparison of the expressivity of different GNN extensions is given by (Papp & Wattenhofer 2022
The k-WL is powerful tool, but it is not able to solve graph isomorphism in general. The seminal work of Cai et al. (1992) shows that there are pairs of con-isomorphic ((n)-nod graphs that are indistinguishable by the n-WL test. There positive results for special graph classes. Namely, Kiefer et al. (209)) show that planar graphs are identified by 4-WL. Random graphs are mostly
identifiable by the WL test in two iterations (Babai et al. 1980).
Beyond structural expressivity, Grohe (023) analyzes the power of GNNs in terms of circuit com- plexity, showing that GNNs can decide problems in TC (constant-depth circuits with polynomial size)
Complexity Theory, Boolean satisfiability was the first problem proven be NP-complete, by Stephen Cook (Cook) 1971). Later, several variants of SAT have been proven to be equally hard, such PlanarSAT (Lichtenstein, 1982). SAT solving remains an active area of research, with SAT competitions being held annually (Heule et al. (224)).
The computational complexity of different equivalence relations between boolean functions was studied by |Borchert et al. 1998). In their work, two formulas f' on the same set of variables are said to be isomorphic there a bijection a of the variables such that f agree on all assignments up to the mapping a. Under this definition, for instance, tautology is isomorphic to the empty formula. Our notion of isomorphism is stricter, as it requires clauses to be preserved under the mapping, We find that this notion is better suited for the setting with graph representations.
Proof Complexity. The complexity of proving the unsatisfiability of propositional formulas is a central topic in proof complexity. One of the most studied systems is resolution, where the proof consists of clauses derived from the original formula using a simple inference rule. Hard examples for resolution include the Pigeonhole principle (Haken 1985) and the Tseitin formulas (Urquhart, 1987]. Resolution proof length can be related to the width of the proof, where the width of a resolu- tion proof is the maximum number of literals in any clause of the proof (Ben-Sasson Wigderson 2001]. The complexity of resolution has also been characterized in terms of pebbling games (AL- serias & Dalmau 2008 Galesi & Thapen 2005). In this setting, pebbling games are played on single graph unlike the two-graph pebbling games that correspond to k-WL indistinguishabilit (Cai et 1992).
INDISTINGUISHABLE FAMILIES OF SAT INSTANCES
In this section, we construct explicit families of SAT formulas that are provably indistinguishable by the WL-test and the WL hierarchy. As main technical contribution, we show that there 3-SAT formulas that are indistinguishable by the n-LL test, despite one being satisfiable and the other not (Section 5.2).. We also identify practically relevant family of regular SAT formulas that are indistinguishable by WL, yet remain NP-complete. In general, distinguishing SAT instances (regardless of satisfiability) hard graph isomorphism (Appendix C).
5.1 3-REGULAR SAT
To motivate first contribution, start the section with simple example of pair of WL- indistinguishable formulas. Consider a CNF formula f on three variables 21, 02,
f= (m1 V -as) A (-#1 V V3)...
21 23
A (x) V22) A (-21 V -22)
21 @ T'2
A (x2 V2y) A (-z2 V -Z3)
22 @ I's
where @ denotes the xor. See Figure | for the graph representation. The formula is satisfied by 01
(0, 1, We can make similar but unsatisfiable formula f' by replacing the
"This implies (under common complexity theoretic assumptions) that SAT cannot be decided by GNNs. However, note that this does not imply that there must exist n- indistinguishable satisfiable and unsatistiable formulas (which is what we show in Theorem 5.3). Indeed, as shown in Theorem 1] all PlanarS AT instances distinguishable by 4-WL., even though PlanarSAT is NP-complcte.
5

---

Published as a conference paper at ICLR 2026
clauses encoding 22 @ F3 (the third line) with clauses encoding 22 Σz. Note that this change keeps all literal degrees the same. Since each literal appears in exactly two clauses in both f and f", the LCGs of f and f' are WL-indistinguishabl. However, f is clearly unsatisfiable.
This example can be generalized to a family of 3-regular SAT instances. We say that a SAT instance is k-regular if each literal appears in exactly & clauses and each clause contains exactly &s literals. Despite this strong regularity, the class remains computationally hard:
Theorem 5.1. 3-regular SAT is NP-complete.
Although related NP comoleee variants have appeared in the literature (3-SAT Karpp with each variable appearing at most 4 times (Tovey] 1984))
1972), 3-SAT
not aware of a formal proof of this specific result, so we provide one in Appendix D Difor for completeness. formulas are given in the 3-regular SAT format, WL-powerful GNN is essentially useless in solving them:
Observation 5.2. The WL test does not distinguish between any two 3-regular SAT formulas with the same number of variables.
5.2 K- WL INDISTINGUISHABLE SAT INSTANCES
Given that WL cannot distinguish some formulas, one might wonder whether higher-order WL tests suffice. In this section, we answer the question in the negative, showing that there are 3-SAT formulas that are indistinguishable by the WL hierarchy, despite one being satisfiable and the other not.
Theorem 5.3. There are 3-SAT formulas f. f with (n) variables and (n)) clauses such that satisfiable and f is not, but the L,NNs of f and are indistinguisaable by the n- n-WL. A-W..esst test.
Our result uses the seminal work of Cai, Fürer and Immerman Cai et al. (1992), giving a pair of non- isomorphic graphs H and H which are indistinguishable by n- WL. We construct a pair of formulas f. with LCNs isomorphic to H and H, respectively. On high level, our formula fc encodes the existence of an even orientation for a graph G. This an orientation of the edges such that each node has even number of outedges. We show that such an orientation exists if and only if the number of edges is even. Then, even orientation when one of the edges is bidirectional. Exactly one of fC and fa are satisfiable, depending on the parity of m. The proof of Theorem 5.3 is given in Appendix B
construct a twisted formula fc. encoding the existence of an
Interestingly, the construction in Theorem 5.3 is similar to Tseitin formulas, which are known as hard instances for resolution refutation (Urquhart 1987). Tscitin formulas encode a set of linear in- equalities over nodes of a graph. See Definition B. for formal definition. Resolution proofs and likewise the WL test test-rely on exploiting local patterns the formula (or graph), and in both set- tings, the hardest instances include global inconsistency that cannot be detected through purely local reasoning. To the best of our knowledge, this connection between Tseitin formulas and the construction of Cai et al. (992)) has not been previously observed.
Implications for WI.-powerful architectures. Theorem 5.3 shows that in general, satisfiability cannot be expressed by any GNN architecture bounded by the WL hicrarchy. In contrast to pre- dicting satisfiability directly, classic SAT solvers, and some GNN-based approaches (Ozolins et al.) 2022). work by sequentially setting variables. A natural question is whether a few variable assign- ments can help to break symmetries, making formulas more distinguishable, i.e., increasing the effective expressive power of the solver. This mirrors how node labeling tricks are useful for GNNs to solve certain tasks like triangle counting (You et al. [021 202i/Zhang et al. 2021). However, even in this setting, WL-powerful GNNs have fundamental limitations:
Lemma 5.4. Let J. f be formulas with LCNs indistinguishable by k-WL for some k 2 For any partial assignment of variables of J. with at most [k/2] - variables set, there is a cor- responding partial assignment 5 of the variables of f such that LCN(a(f)) and LCN(a are WL-indistinguishale
Here, (C)(( denotes the LCN of the formula f. with additional labels T or 1 for literals set to true or false by a. Lemma 5.4 transfers a theoretical k- WL indistinguishabilty result to a practical setting, where WL-powerful GNN is used to make sequential decisions any decision that is made for f could also be made for

---

Published as a conference paper at ICLR 2026
Restart strategies provide concrete example of this limitation. When restarting, the solver discards the current assignment and restarts the search from scratch. Restarting is a core component of classic solvers (Gomes et al. 2000; Huang al., 2007), and ML has also been used to guide such restarts (Liang et al. (018a). The following result a corollary of Theorem 5.3 and Lemma 5.4 showing that restart prediction is fundamentally hard for WI--powerful models:
Corollary 5.5. WL-powerful GNNs cannot, general, distinguish satisfiable residual formula from an unsatisfiable one, even with (n) variable assignments, where n is the number of variables the formula.
6 POSITIVE RESULTS FOR DISTINGUISHABILTTY
Having shown expressivity limits, we now identify families where GNNs can succeed.
6.1 PLANAR SAT
PlanarSAT AT is a variant of SAT where the clauses are represented as planar graph. The PlanarS AT language is NP-complete (Lichtenstein) 1982). The following result is consequence Kiefer al. 2019), who showed that the 4-WL test distinguishes all planar graphs.
Theorem 6.1. For any SAT formula there is an equisatisfiable PlanarSAT formula f' with polyno- mially many variables and clauses, such that the 4-WL test distinguishes f' from any other formula.
Proof. PlanarSAT NP-complete (Lichtenstein
1982) (this also works in the LCN represen- tation, see Lemma in (Lichtenstein 1982)). The 4L test distinguishes between all planar
graphs (Kiefer et al. 2019).
This result shows that, despite the general limitations of the WL-hierarchy in distinguishing formulas 3.22), there exist natural and computationally hard subsets of SAT, such as PlanarSAT, where already 4-WL is fully expressive. The reduction PlanarSAT is done by replacing edge crossings in the LCN with gadgets that ensure planarity. Unfortunately, the reduction is not efficient in practice, because each gadget adds 9 variables and 20 clauses and there may be up to On²)) edge crossings.
6.2 RANDOM SAT INSTANCES
Random SAT instances can be defined in various ways, often depending on the desired structure or difficulty. In this section, we consider instances generated from randomly sampled graphs (LIGs), where each literal is node and edges connect literals that co-occur in clause. While the LIG representation loses some logical information, Wu & Ramanujan (2021) give a principled procedure for extracting a CNF formula from it:
graph G, a corresponding CNF formula can be extracted by computing a minimal clique edge cover of G The clauses of the for- mula correspond to the cliques in the edge cover. The generated formula does not contain duplicate clauses, subsumed clauses or unit clauses.
Lemma 6.2 ((Wu & Ramanujan 2021)). Given a
We show that a CNF formula extracted from a random literal-incidence graph is likely identified by WL. The proof can be found in Appendix E
Theorem 6.3. CNF formula extracted from uniformly random literal-incidenn incidence graph with n literals is identified by the WL test with probability al least 1 11/7, over the choice of LIG, for a large-enough n.
7 EXPERIMENTS
We aim to evaluate whether WL-powerful architectures (such as GIN (Xu et al.) 2019) are, in principle, capable of predicting satisfying assignment SAT formulas.
A clique edge cover set of cliques in G, such that all edges helong least elique.

---

Published as a conference paper at ICLR 2026
7.1 SETUP
Our experiments are based on the fact that in a node-level prediction task, nodes that are WL- equivalent must have the same output. Given satisfiable formula, we add equality constraints between all WI.-equivalent literals, and check whether the augmented formula remains satisfiable. This is a necessary (but not a sufficient) condition for a WT--powerful GNN to predict a satisfying assignment.
Formally, let f be a satisfiable formula. Running WL for r 2 rounds on (CN gives a partition of the literals Li,...,Ly Lag. We construct an augmented formula Sr that restricts literals in each partition to the same value. For each equivalence class L, ..,..... L, we add the clauses
9j := (-h,, V {)) A (-e, V 1.1)). The formula 9; encodes equality constraint between the literals in Lj. Given satisfiable formula f. a WL-powerful architecture can predict satisfying assignment within r rounds only if fr = ff Ni=1 is satisfiable. We solve f, for different values of r, from the LCN of the original formula f. We let Terit be the smallest r such that fr is satisfiable, such round exists. Conversely, if is unsatisfiable for all r, conclude that WL is not sufficiently powerful to predict satisfying assignments for
1 to Tconverged- where Tconverged the number of rounds for WL converge
7.2 DATASETS
Random instances. The G4SAT benchmark (Li et al. (024) generates random instances from various families, including random 3-SAT (Crawford Auton 1996) and the CA family mimicking community structures in industrial instances (Giráldez-Cru & Levy 2015). Instances are grouped by size (referred to as difficulty in (Li et al. 2024)). The benchmark is designed so that all instances challenging, by choosing instances that near the satisfiability threshold for 3-SAT (Crawford
& Auton 1996) and analogously for other families. See (Li et al. 2024) for descriptions of the families.
SAT competition instances. We use instances from the International SAT competition (Heule et al., 2024). spanning the competitions held between years 2020 and 2025. The instances are selected as hard examples from various applications, including scheduling, cryptography, and hardware equiv- alence checking. Some families are hand-crafted encoding the Pigeonhole principle. Detailed descriptions of the families can be found in the com- petition proceedings; see (Heule et al., 2024) for the 2024 edition The size the instance varies from few hundred variables to 50 million variables. Due to limited computational resources, limit instances to those under 10 MB in size.
difficult for SAT solvers, such as formulas
7.3 RESULTS
See Table I for results on random instances. The number of rounds needed for WI. to distinguish literals sufficiently very low, usually 3 or We observed that in many cases (about 40% of all formulas), WL actually gives all literals unique identifiers. In this case, the constrained formula fr trivially satisfiable because is equal to f. There are few instances in the k-clique and k-vercov families (2.0% and 0.3%, respectively) that WL could not solve [ See Table 4 for the full results on random instances.
For random 3-SAT instances, regardless of the size of the formula, literals almost always suffi- ciently identified after 3 iterations, and WL converges in 4 rounds. This pattern is due to the constant degree of the clauses. In the first iteration, each literal sees its degree de. However, the second iter- ation does not refine the literal partition because every neighbor is a clause with degree 3olyy on the third iteration, the literals observe the degrees of other literals in shared clauses.
'A list of instances for the 2024 competition is available at https::/bbnchmaatt dat de/ ?track mmiin 2024eresuit=ss
"feclique encodes the problem of finding a l cl-liquee on an Rendsi graph. Symmetries in the underlying graph can lead to symmetries in the formula that WL cannot resolve. For example, the graph may contain two nodes that are each fully connected the same clique but not to each other, making them indistinguishable under WI., yet mutually exclusive in the satisfying assignment.
8

---

Published as a conference paper at ICLR 2026
Table 1: Results on random instances, grouped by family. All instances were initially satisfiable. is the smallest number of rounds for which the augmented formula fr is satisfiable. We write unsar when this value does not exist. Feunverged is the number rounds for WL to converge. All values are reported as mean + std.
family
difficulty
Ferit
cconverged
Variables
Clauses
Count
3-sat
easy
2.97 = 0.18
3.68 = 0.47
26 +
119 + 36
1000
medium
3.00 + 0.04
3.92 = 0.28
509 + 198
1000
hard
3.00 + 0.00
4.00 0.00
250 + 29
1065 + 125
100
hard+
3.00 0.00
4.00
921 + 48
3775 - 196
hard++
3.08 + 0.28
4.00
5001 62
20504
25
k-clique
easy
4.12 + 0.73
6.23
33 13
543 426
960
unsat 4.11 + 0.52
0.78
2
217 194
40
medium
0.95
68 18+17 17
2156 + 960
999
unsat
6.00
4
939 =
hard
4.00 + 0.00
6.00
114 20
5554 + 1718
100
Table 2: Results on selection of instances from the international SAT competition. All instances were initially satisfiable.
family
Tcrit
Tconverged
Variables
Count
argumentation
2.94 + 0.44
4.31 + 0.87
1266 + 625
16
circuit-multiplier
unsat
7.18 + 0.40
1075 +
cryptography
15.74 + 14.67
17.63 # 14.34
41510 + 29705
19
unsat 4.17 + 0.51
18.74 + 13.38
19257 37634
23
hamiltonian
5.44
550 = 45
18
heule-folkman
unsat unsat 26.64 + 3.64 unsat
4.91 + 0.30
16614 # 1103
11
heule-nol
8.60 + 1.26
1419 +
10
maxsat-optimum
29.27 + 2.49
22157 # 5623
11
59.00 # 0.00
27597 # 8713
SAT Competition Instances. An overview of the results is shown Table 2 and a more detailed breakdown given in Table (Appendix G). WL takes considerably
rounds to converge. Out of 448 evaluated instances, only 234 could be solved with the expressive power of WL. Across 69 instance families, 38 contained instances where WL is not expressive enough. An example of family with indistinguishable structure is heulc-nol, which encodes type of grid coloring problem (Heule et al. 2024). The regular structure of the instances makes difficult for WL to distinguish literals.
CONCLUSIONS AND FUTURE WORK
Our theoretical results establish fundamental limitations on the expressive power of GNNs for SAT solving. We show that even the full WL hierarchy cannot distinguish between satisfiable and un- satisfiable formulas, while also revealing connections resolution complexity and offering new perspective on the classic construction of of et al. (1922. Additionally, we identify an NP-complete Wi-innistinguishable class of SAT instances, as well as provide positive guarantees for distin- guishing random and planar SAT instances.
Experimentally, we show that WL-powerful architectures are, in principle, expressive enough to predict satisfying assignments for random SAT instances, but struggle with industrial and crafted benchmarks. Our test setup allows us to see a WL-powerful GNN has the necessary expressive power for predicting satisfying assignments, though it does not capture whether that expressivity is sufficient for generalizable learning. Even for random SAT formulas, improved generalization may require higher-order GNNs, symmetry breaking, other architectural improvements.

---

Published as a conference paper at ICLR 2026
We hope GNNs applied to industrial SAT instances in the future. While this remains challeng- ing due to the lack of scalable generators and the large size of many industrial instances these instances provide structurally richer and potentially more demanding testbed. Progress in this direction could offer new insights into generalization that remain hidden when only using random instance distributions.
REPRODUCIBILITY STATEMENT
The code for the experiments is available online Complete proofs of all theoretical results, including background results such as the NP-completeness of 3-regular SAT, are included in the appendix (Ap- pendices B Eb. Details of dataset selection and generation are given in Section 7.2 and Appendix (
REFERENCES
M. Ajtai. Recursive construction for 3-regular expanders. Combinatorica, 14(4):379 416, 1994. doi: O0.100//FF1330263.
Tasniem Nasser Alyahya, Mohamed El Bachir Menai, and Hassan Mathkour. the structure of the boolean satisfiability problem: A survey, ACM Comput. Surv., 55(3), March 2022. ISSN 0360-0300. doi: 10.1 145/3491210.
ora.:i..org/00/ /00. 1145/3491210 0144
Carlos Ansótegui, Jesús Giraldez-Cru, and Jordi Levy. The community structure of sat formulas. In International Conference on Theory and Applications of Satisfiability Testing, pp. 410-423. Springer, 2012.
Albert Atserias and Victor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and Syslem Sciences, 74(3):323-33,, 2008. ISSN 0022-0000. doi: https://doi. encedi rect. com/ stom/sci.a encee
org/10. 101.10006/....ss .6.0025. URL https:://
article /tticcee//1/5500000000000
Computational Complexity 2003.
Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In IJCAI, volume 9, pp. 399-404, 2009.
László Babai, Paul Erdös. and Stanley M. Selkow. Random graph isomorphism. SIAM Journal on Computing. 9(3):628 635, 1980. doi: 10.1137/0209047. URL https::/doi http//ooo..rg....
1137/0209047
Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow-resolutio made simple. ACM,
4892)11 March 2001, ISSN 0004-5411. doi: 10. 10.1145/355827.355855. URL https:
7/doi. oidoi.org//0.110 1145/ 375827 375835
Armin Biere. Adaptive restart strategies for conflict driven sat solvers. In International Conference Theory and Applications of Satisfiability Testing, pp. 28-33. Springer, 2008.
B. Borchert, D. Ranjan, and Stephan. On the computational complexity of some classical equiv- alence relations on boolean functions. Theory of Computing Systems. (1(6))679-6)) 1998. doi: 10.1007740022440000999 URL https: doi. /10 oo..
Jin-Yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):3894410, 1992. doi: 10.1007/BF0130033. URL
https://doi. http://o.oorrg/...o/o/o 1ttp://00..000/F01133053
Wenjing Chang and Wenlong Liu. Sat-gatv2: A dynamic attention-basse graph neural network for solving boolean satisfiability problem. Electronics, 14(3):423, 2025.
Stephen A. Cook. The complexity of theorem- proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing. STOC '71 pp. 151-158, New York, NY, USA, 1971. Association for Computing Machinery. ISBN 978 155034444444 doi: 10.1145/800157. 805047.
10

---

Published as a conference paper at ICLR 2026
James M. Crawford and Larry D. Auton. Experimental results the crossover point in dom 3-sat. Artificial Intelligence, 81(1):31-57. 1996. ISSN 0004-3702. doi: https//doi.org org/
10.101660000-370099900006----110 URL https: /wwww/wwwww.///// www.ssccenceireeeeo com com/science/ Frontiers in Problem Solving: Phase Transitions and
Complexity.
Nicola Galesi and Neil Thapen. Resolution and pebbling games. In Fahiem Bacchus and Toby Walsh (eds.), Theory and Applications of Satisfiability Testing, pp. 76-90, Berlin, Heidelherg, 2005. Springer Berlin Heidelberg. ISBN 978-3-540-33669944
Jesús Giráldez-Cree and Jordi Levy. A modularity- -based random sat instances generator. In Proceed- ings of the 24th International Conference on Artificial Intelligence, IJCAI'15, pp. 1952-1958.
AAAI Press, 2015, ISBN 978 9785533357384.
Carla P Gomes, Bart Selman, Nuno Crato, and Henry Kautz. Heavy-tailed phenomena in satisfia- bility and constraint satisfaction problems. Journal of automated reasoning. 24(1):67-100, 2000.
Martin Grohe. Descriptive Complexity, Canonisation, and Definable Graph Structure Theory. Lec- ture Notes in Logic. Cambridge University Press, 2017.
Martin Grohe. The descriptive complexity of graph neural networks. In 2023 38th Annual ACM/EEE Symposium Logic in Computer Science (LJCS), pp. 1-14, 2023. doi: 10.1109/ JLCS56633.2023.100 10175535
Wenxuan Guo, Hui-Ling Zhen, Xijun Li. Wanqian Luo, Mingxuan Yuan, Yaohui Jin, and Junchi Yan. Machine learning methods solving the boolean satisfiability problem. Machine In- telligence Research, 20(5):640 655, 2023. doi: 10. 10.10077111333-02-113333 1tt.ooor//0.100/1113333333 022 1396-2
URL https:
Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. ISSN 0304-3975. doi:
URL https: Third
//www. scwencediiiicccccco.....occccc.e rect. www
Conference on Foundations of Software Technology and Theoretical Computer Science.
Marijn JH Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Proceedings of SAT competition 2024: Solver, benchmark and proof checker descriptions. 2024.
Jinbo Huang et al. The effect of restarts the efficiency of clause learning. In IJCAI, volume 7, pp. 2318-2323, 2007.
Ningyuan Huang and Soledad Villar. A short tutorial the Weiseeiler-ehhman test and its variants. ICASSP 2021 2021 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pp. 8533 8537, 2021.
Neil Immerman and Eric Lander. Describing Graphs: A First-Order Approach to Graph Canonization, pp. 59-81. Springer New York, New York, NY, 1990. ISBN 978-1- 4612-4478-3. doi: 10. 100100779988-14414447883
URL https::/ddee htt////ci..rg1111000010000
978 100-114612 141124411444--3
Richard M. Karp. Reducibility among Combinatorial Problems, pp. 85-103. Springer US, Boston, MA, 1972. ISBN 978-1-4684-2001-2. doi: 11007/08----4684---1 doi www./rrg..... 1000/078-1111 140---100--4-4-222
URL https://
Nicolas Keriven and Gabriel Peyré. Universal invariant and equivariant graph neural networks.
Curran Associates Inc., Red Hook, NY, USA, 2019.
Sandra Kiefer. Power and limits the Weisfeiler-Leman algorithm. PhD thesis, Dissertation, RWTH Aachen University, 2020, 2020.
Sandra Kiefer, Iia Ponomarenko, and Pascal Schweitzer. The Weisfeiler- dimension of planar graphs at most 3. J. ACM, 66(6), November 2019. ISSN 0004-5411. doi: 10.1 3333003. URL http:/ttt////ttt .rrooioorg/// 01.

---

Published as a conference paper at ICLR 2026
TN Kipf. Semi-supervised classification with graph convolutional networks. arXiv preprint arXiv:1609.02907. 2016.
Zhaoyu Li, Jinpei Guo, and Xujie Si. G4SATBench: Benchmarking and advancing SAT solving with graph neural networks. Transactions on Machine Learning Research, 2024. ISSN 2835-8856.
Jia Hui Liang, Chanseok Oh, Minu Mathew, Ciza Thomas, Chunxiao Li, and Vijay Ganesh. Machine learning-based restart policy for edel sat solvers. In International Conference on Theory and Applications of Satisfiability Testing, pp. 1101 Springer, 2018a.
Jia Hui Liang, Chanseok Oh, Minu Mathew, Ciza Thomas, Chunxiao Li, and Vijay Ganesh. Ma- chine learning-basee basedd restart policy for CDCL SAT solvers. In Olaf Beyersdorff and Christoph M. Wintersteiger (eds.), Theory and Applications of Satisfiability Testing SAT 2018, pp. 94-110, Cham, 2018b. Springer International Publishing. ISBN
David Lichtenstein. Planar formulae and their uses. SIAM Journal on Computing, 11(2):329-343, 1982. doi: 10.1137/0211021 (RLhttps::/
doi org/ 1tt///10..13172111111
Haggai Maron, Heli Ben-Hamu, Hadar Serviansky, and Yaron Lipman. Provably Powerful Gruph Networks. Curran Associates Inc., Red Hook, NY, USA, 2019.
Christopher Morris, Martin Ritzert, Matthias Fey, William L.. Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe. Weisfeiler and Leman go neural: higher-order graph neural networks. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium Ed- ucational Advances in Artificial Intelligence, ISBN 978-1-57735-809-1.
19 19. AAAI Press, 2019. doi: 10. 11669/anai.v33300 0.330..33011602
Matthew W Moskewiez, Conor Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Con- ference, pp. 530-535, 2001.
Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Ko- zlovics. Goal-aware neural SAT solver. In 2022 International Joint Conference on Neural Networks (ICNN), pp. 1-8. IEEE, July 2022. doi: 1111199//iicn2555422229999911179 http://das doi. org www.oog................ 10. 109/ IJCNN55064 2022. 9892733
URL
Pâl András Papp and Roger Wattenhofer. A theoretical comparison of graph neural network exten- sions. In Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvari, Gang Niu, and Sivan Sabato (eds.), Proceedings of the 39th International Conference on Machine Learning, volume 162 of Proceedings of Machine Learning Research, pp. 17323-17345. PMLR, 17-23 Jul 2022.
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE transactions on neural networks, 20(1):61-80, 2008.
Daniel Selsam and Nikolaj S. Bjömnr. Guiding gegh-performanc SAT solvers with unsat-core predictions. In International Conference on Theory and Applications of Satisfiabliity Testing, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning SAT solver from single-bit supervision, 2019. URL pettps://arxiv...o
abs/ 1802. 03685
Zhengyuan Shi, Min Li, Yi Liu, Sadaf Khan, Junhua Huang. Hui-Ling Zhen, Mingxuan Yuan, and Qiang Xu. Satformer: Transformer-based unsat core learning. In 2023 IEFF/ACM International Conference on Computer Aided Design (ICCAD), pp. 1-4. IEEE, 2023.
JP Marques Silva and Karem A Sakallah. Grasp-a new search algorithm for satisfiability. In Pro- ceedings of International Conference on Computer Aided Design, pp. 220-227. IEEE, 1996.
Craig A. Tovey. A simplified NP-complete satisfiability problem. Discrete Applied Mathematics, (1):85-89, 1984. ISSN 01 01662218 doi: http://haiaan////.0m000666612222
12

---

Published as a conference paper at ICLR 2026
Alasdair Urquhart. Hard examples for resolution. ACM, 34(1):209-223) January 1987. ISSN 0004-5411. doi: 10.1145/7531.899 UtL.:a/te///.....g1.1111.11///1/
8928
Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Roger Baker Grosse, and Fahiem Bacchus. Learning clause deletion heuristics with reinforcement learning. 2020. URL httpss:/aakk
semanticscholee org/CorpusID: 2210899112
Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikku- lainen. Neuroback: Improving CDCL SAT solving using graph neural networks. In The Twelfth International Conference on Learning Representations, 2024.
Boris Weisfeiler and A. A. Lehman. A reduction of graph canonical form and algebra arising during this reduction. Saanchno-Techniihesskyy Informatsia, pp. 2(9):12-16, 1968.
Haoze Wu. Improving SAT-Solving with machine learning. In Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, SIGCSE '17, pp. 787-788, New York. NY, USA. 2017. Association for Computing Machinery. ISBN 978 450344666. doi:
76813001788000224444 URL httpt:ttt///....oo org/10 1145/3011111 1445/201668800.2222264
Haoze Wu and Raghuram Ramanujan. Learning to generate industrial SAT instances. Proceedings of the International Symposium on Combinatorial Search, 10:206-207, 09 2021. doi: 10.1609/
socs.v 10011.1849..
Keyulu Xu, Weihua Hu, Jure Leskovee, and Stefanic Jegelka. How powerful are graph neural networks? arXiv preprint arXiv:1810.00820 2018.
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanic Jegelka. How powerful are graph neural networks? In International Conference Learning Representations, 2019.
Emre Yolcu and Barnahás Póczos. Learning local search heuristics for boolean satisfiability. Ad- vances in Neural Information Processing Systems, 32, 2019.
Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovee. G2SAT: Learning to generate SAT formulas. NeurlPS, 2019.
Jiaxuan You, Jonathan M Gomes-Selman, Rex Ying, and Jure Leskovec. Identity-aware graph neural networks. In Proceedings of the AAAI conference artificial intelligence, volume 35, pp- 10737-10745, 2021.
Muhan Zhang, Pan Li, Yinglong Xia, Kai Wang, and Long Jin. Labeling trick: A theory of using graph neural networks for multi-node representation learning. Advances in Neural Information Processing Systems, 34:9061-9073, 2021.
A GRAPH REPRESENNATIION OF SAT FORMULAS
J1
#
g1
Z2
F
F
Z2
T
Left: f f= (x) V -ws) A (a) V v2) A ( 23) A [T
m)) A (~r) m2) A ( (-0z -r3) Right: f' = (mn V -2a) (an V 22) (Ia v3) (Is V x2) A (~ V - A (-x1 -13)
Figure 2: L.Css of f and f". The difference between the formulas is highlighted bold. Removing the literal-literal edges represented by the dashed lines gives the literal-clause graphs.
13

---

Published as a conference paper at ICLR 2026
Literal-clause graphs with negation connections See Section 3 for the definition of the literal- clause graph with negation connections (LCN). The following lemma illustrates why adding literal- literal edges is necessary to preserve all information about the formula when labels are removed.
Lemma A.1. There are 3-SAT formulas I, such that the literal-clause graphs Gj and G are isomorphic but f is satisfiable and f is not.
Proof. Consider the formulas shown in Figure The two LCGs (dashed lines excluded) are isomor- phic. f has solution 21 = 1, 22 0, 23 = 1. However, f is not satisfiable: 21 1 implies 22 = 0 because of cs, and ig =0 because of cg. Now og is false. Conversely, 21 = implies 22 = because of c2, and 2y 0 because of <1. This makes c4 false.
Other representations In this work use the literal-clause graph representation (with negation edges) because it is lossless and corresponds one-to-one with formulas up to isomorphism. Another popular representation is the variable-clause graph (VCG), which connects variables to clauses, with edge colors indicating the sign of the variable. Similarly to the LCN, the VCG preserves all information about the formula. However, a limitation of the VCG representation is that formula admits up to 2" non-isomorphic graph encodings, where is the number of variables. For example, flipping the sign of all occurrences of a variable x in f (x V v) A (-x) produces an isomorphic formula /' (-x V -w) A (1)), but the VCGs are non-isomorphic. In contrast, the LCNs of / and f' are identical. From the perspective of learning- based methods, such invariance is desirable: is analogous to the requirement of permutation invariance in graph learning.
Other known graph representations include the literal-incidence graph (LIG) and the clause- incidence graph (CIG), where literals (clauses) connected to other literals (clauses) if they co- occur in a clause (share a variable). These representations are less commonly used, as they are inherently lossy.
B K-WL INDISTINGUUSHABLLE INSTANCES (PROOF OF THEOREM 5.3
In this section, we prove the following theorem:
Theorem 5.3. There are 3-SAT formulas f. with O(n) variables and (n) clauses such that f is satisfiable and f is not, but the LCNs of f and f are indistinguishable by the n- n-WL test.
The construction based on the seminal work of Cai, Fürer, Immerman (CFI) (Cai et al. 1992, giving a pair of non-isomorphic graphs H and H which are indistinguishable by n- WL. We construct pair of formulas f, with LCNs isomorphic H and H, respectively. On a high level, our formula fG encodes the existence of an even orientation for a graph G. This is an orientation of the edges such that each node has even number of outedges. We show that such an orientation exists if and only if the number of edges is even. Then, we construct Iwisted formula fa. encoding the existence of an even orientation when one of the edges is bidirectional. Exactly one of fc and fc are satisfiable, depending on the parity of m.
B. THE CONSTRUCTION
The CFI construction (Cai et al. 1992) takes in a low degree graph G with only linear sized separa- tors and produces non-isomorphic graphs (G) and X that are indistinguishable by WL. Next, go over the steps construct X (G). or equivalently formula fa with LCN isomorphic X (G). For each vertex v E VG),, we define the following subformula Xx, where k = d(v):
Literals: Ag U Bx, where
A {a,
i k), B; = (b: 1 < $ k}
Clauses: Ck U DE. where
C₁ {cs - (Vies a:) (Vigs (S]()))) is even)
D3 {a, vb i (1,.... ......,,)) k)}
14

---

Published as a conference paper at ICLR 2026
Here [k]] denotes the set {1,... k.. See Figure for diagram of the LCN of X₁ with k = 3. This graph corresponds exactly to the graph Xx in the CFI constructior Note that the negations of the literals are not contained in X3 they will be defined later.
vb
b1
C12
C13
C23
Cp
V by
b2
03
ag Vbs
b3
Figure 3: An L.CN of the formula X3, corresponding to the graph X3 in the CFI construction. Literal nodes are circled. The clauses are connected to the literals by solid lines.
For given graph G, the full formula fo constructed as follows. For each vertex v V(G), add the subformula X) Each edge (v, w) } of is associated with one of the literal pairs (a,, bi). where we call the literals au,w, by.w. The node w on the other side of this edge uses the negations of the literals, that is, aw,v - and b -b,,w- In the LCN, the literal arww is connected to its negation aw,y. and br.w to bw. See Figure 4a for an example.
Now, we define a twisted formula fc. and the corresponding twisted graph (G) as follows. An edge {v, w E(G) chosen arbitrarily. The literal-literal connections twisted, that dv becomes the negation of our and b becomes the negation of aw,v- A twisted edge is shown in Figure 4b
Observation B.1. The LCNs of fo and fc are isomorphic to the graphs X(G) and (G') in Cai
al. 1992), respectively.
To state the result Ca al. 1992), we need the concept of separator:
Definition B.2. A separator of graph G is a set S c V(G) such that the induced subgraph on V \ S has no connected component with more than //) vertices.
Theorem B.3 (Theorem 6.4 in (Cai et al. 1992 Let G be a graph such that every separator of G has at least l + 1 vertices. Then X (G) and X are non non-isomorphic but k- WL indistinguishable
B.2 SATISFIABILITY OF fo AND fG
By construction, literals have their negations on the other side of each edge:
Remark B.4. For normal (not twisted) edge {u, w} E E(G), ar,w = -e and b -bw,e- If the edge is twisted, ag,m = - and b -0
The following is true for JG and ja. for any edge {v, w., w) (twisted or not): Observation B.5. The literals arww be are non-equal in any satisfying assignment.
Proof. This is forced by (a V buge) A (aww, V bregr) = (Angw V begw) A (-app V bb
This allows to talk about satisfying assignments of Sa and fa as orientations of edges of G: Remark B.6. Any satisfying assignment is uniquely characterized by the values of A. On graph without twists, assignments to correspond one-to-one with orientations G. On a twisted edge, either both a,,w and a,,v are true, or both are false.
Consequently, the number of A-literals set to true in fa is m, while in fo it m or + + 1.
The next lemma characterizes the satisfiability of Xx:
The nodes corresponding the Dy clauses not present in the standard construction in Cai et al. but they mention that nodes connecting each a; to b, can he added.
1992
15

---

Published as a conference paper at ICLR 2026
Gg.w
buru
Og.w
Buww Vibss
aw.y
Owre Vbu,a
Owro
Ou, Vbb.
(a) A normal edge.
(b) A twisted edge.
Figure 4: Constructions in the formula fa and Sa for edge {v. w) E E(G). The edges are represented vertically, with the top ellipse corresponding 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.
Lemma B.7. Let be an odd integer and assume that a, + b, for Sis k. X2 is satisfied if and only if an even number of az 's (or equivalently by (ss) to true.
Proof. Let T C (1.... k} be the set of indices i such that ag is set to true. We start by proving that X is satisfied whenever T is even. The clauses in D& satisfied whenever a; b; which is guaranteed by assumption. Consider any clause cs ( (Vies as) V ( (Vigs b,). Since l is odd, [S] is even, and [7] is even, S ST is not partition of .1,..., k). Hence, there is some index i such that is in both sets or neither of the sets. If E n then a, satisfies cs. Else i g S SUT T, and b; satisfies cs.
Conversely, suppose that [T] is odd. Consider the clause es with S= (1,..., k} T. It a clause because |S| is even. is unsatisfied, since F for each E S and b, = F for each $ S. O
The following observation is a direct consequence of Lemma B.7 and Observation B.5 Observation B.8. Assume the degree of every node in G is odd. any solution of fo fa. the number of A-literals set to true is even.
We say that simple graph G has all nodes have even outdegree. The following is a simple fact characterizing the existence of even orientations:
orientation if there is orientation of the edges such that
Lemma B.9. Let H be simple connected graph. H has orientation if and only if m [E(H) is even.
Proof. Let (v) denote the outdegree of node It always holds that Evev douu m.
Assume there exists even orientation of H. Then (v) is even for all Since the sum of even terms always even, m must be even.
Now assume that is even. Start with arbitrary orientation of the edges. For any two vertices v, with odd outdegree, take an arbitrary path connecting v and w and reorient the edges on the path. This changes the outdegrees of v and from odd even, while not changing the parity of other nodes. Repeat this process until all nodes have even outdegree. Suppose that this is not possible, that is, we are left with single node with odd outdegree. We have d (v) m Ewev (u) dd"(w) (w). The left side is odd, while the right side is even because m and the terms of the are even. Hence, we can always find an even orientation.
Using this, we can prove the main lemma characterizing the satisfiability of fa and Je: Lemma B.10. Ler G be connected graph where all degrees are odd 10 If m |E(G) is even
(odd), fo is satisfiable (unsatisfiable), and fa is unsatisfiable (satisfiable).
10 proof can be generalized to mix of odd and even degrees, but chose to do this for simplicity of the argument.
16

---

Published as a conference paper at ICLR 2026
Proof. Suppose that is even. G has orientation by Lemma B.9 We can use this to extract a satisfying assignment of fo by setting 0u = for each outedge of v. This assignment satisfies every subformula by Lemma B. On the other hand, the twisted formula must have m m + A-literals true (Observation B.6 making unsatisfiable (Ohservation B.8)
If m is odd, fo is unsatisfiable by Observation B.S On the other hand, the twisted edge allows us to set both a-literals of the edge to false, effectively removing the edge. The graph G with {u, w) removed has an even number of edges, so we can find satisfying assignment by computing an even orientation of the remaining edges.
Proof of Theorem 5.3 Let G be graph with odd degrees, where the size of the smallest separator is linear in n. We can use the construction of Ajtai (1994) for 3-regular expanders. 'he L.CSs of and f' are isomorphic XG') and X (G). respectively. These graphs are indistinguishable by Theorem B.3 By the above Lemma B.10 exactly one of fa and fo is satisfiable. Note that both fG and fc have at most 3 literals per clause. The number of variables is A(G) ((n) and the number of clauses (2A(G)-1 + 1) O(n).
Tseitin Formulas. Interestingly, this construction is related to Tseitin formulas, which are known as hard instances for resolution refutation proofs (Urquhart 1987).
Definition B.11. A Tseitin formula constructed by taking graph G and a charge function c V(G) + {0, }} labeling the vertices. Each edge E(G) is associated with variable ze- For each vertex, there is a constraint & = > weeN()) (()) [fe, c(v) mod 2, meaning that the parity of the sum of variables of v's edges is equal to the charge. The full formula is defined as AvevEu.
known that a Tseitin formula is satisfiable and only if the sum of charges is even. Hence, satisfiability is global property of the graph. When the underlying graph is an expander (with small degrees), Tseitin formulas are known to be hard instances for resolution (Urquhart 1987.
B.3 IMPLICATIONS FOR WL-POWERFUL, ARCHITECTURES (PROOF OF LEMMA 5.4
To prove Lemma 5.4 we first prove more general statement (Lemma B.12p. p. This uses the equiv- alence between k- WL and the pebbling games of Cai et al. (1922). Using the definition from Kiefer 2020). the bijective k-pebble gume BP (G. H) is defined as follows. The game is played on two graphs G and H. There are two players, a spoiler and a duplicator. The game proceeds in rounds. Each round is associated with configuration (τ, J) of pebbles the two graphs, where u E (V(G))² and ú E (V(H)), where & E [0, k). G[u] denotes the subgraph induced by the nodes in u, where nodes carry the label of its position in the tuple u. The initial configuration is the pair of empty tplles. In each round, the following actions are performed in order:
The spoiler chooses an index i E [A:]
The duplicator chooses a bijection / VGG) + V(H)
The spoiler chooses E (GG) and sets w = f(v).
If i E [4]. a pebble is moved from u. to v in G and from v, to w in H. The new configuration is
(( 11-1, v, #.+1...., U2), (W1, 11 W. Wi41...., We))
Otherwise, a new pebble is placed on e in G and on w in H, and the new configuration is
We, v), (Wi,... we, w))
The spoiler wins if the induced, ordered subgraphs G[z] and H are non-isomorphic. The dupli- cator wins the spoiler never wins.
Let GD denote the whole graph G, where nodes in ū carry the label of their position in the tuple स.
Lemma B.12. Let G and H be two graphs indistinguishable by k- WL for some k 2 3. Then, for every pebbling u E (V(G))', k 2, there exists a pebbling e E (V(H)) such that the pebbled graphs T and H are indistinguishable by WI..
17

---

Published as a conference paper at ICLR 2026
Proof. By the equivalence between k-WL and the bijective k-pebble game (Cai et al. 1992 "1 the duplicator has a winning strategy in BP (G, H). Starting from the empty configuration of BP& H), let spoiler spend the first t rounds to place t pebbles G according to Because the duplicator follows a global winning strategy in BPx (G, H), there exists a pebbling v on H such that the configuration remains partial isomorphism.
We now keep the & pebbles fixed and consider the 2-pebble game played on the graphs GT and H" where the vertices of U, 7 carry unique labels. Consider 2P2 H1 which is equivalent WL on these graphs. To argue that WL does not distinguish these graphs, we show that the duplicator has a winning strategy in 2P2(G". H.
We can simulate any spoiler play in BP2 H in HP, keeping the first t pebbles in place while using the k 2 free pebbles to simulate the two pebbles in BP2. Note that in G the vertices of u already carry unique labels, so the spoiler gains no additional power from placing pebble on already labeled nodes, so we can assume spoiler only plays pebbles on vertices outside of V. Each BP2 round (spoiler picks index, duplicator picks bijection, spoiler picks a vertex G) is then legal BP, round. The duplicator responds with their winning strategy for BPR. The spoiler never reaches winning configuration in (G, H). and hence cannot win in BP BP2 H Therefore the duplicator wins BP2 "H),, which by the known equivalence is the same as WL failing to distinguish G and H
Lemma B.13. Let f, f be formulas with LCNs indistinguishable by k- k-WL. for some h: 2 4. For any partial assignment of variables of f with at most [k/2] 1 variables set, there is a cor- responding partial assignment ā of the variables of f such that LCN(a(f)) and LCN(}(f)) are WL-indistinguisabbe
Proof of Lemma 5.4, The proof follows from Lemma 1.12 which states that if two graphs are indistinguishable by LL, then any labeling of most k nodes in one graph can be matched by a labeling of nodes in the other graph so that the resulting labeled graphs are WL-indistinguishabl..
We can think of assigned literals as being labeled with or 1. There are at most 2[ k 2 labeled literal nodes, since each variable corresponds to two literal nodes. By Lemma B. there exists labeling of at most A 2 nodes in LCN(f) such that the labeled graphs LCN(a
<
and (a (f) are indistinguishable. The labels on these nodes determine corresponding partial assignment (Ø cannot label two adjacent literals e, -L with the same label (e.g. both T), because such labeling would be detectable by 1-WL. as only existing in LCN(A(J))
C GRAPH ISOMORPHISM COMPLETENESS OF DISTINGUISHING LITERAL-CLAUSE GRAPHS
To complement the indistinguishabiity results, we show that, in general, distinguishing LCNs is as hard graph isomorphism. The graph isomorphism problem (GI) asks whether there is an edge- preserving bijection of the nodes. Formally, the decision problem is
GI = {[G, H) G, H are isomorphic graphs}
Let 9 = (LCN(f) : f e 3-SAT} be the set of LCNs of all 3-SAT formulas. We define the graph isomorphism problem on LCNs as the language
GlsAT {GG, H): G, H E are isomorphic graphs)
We use the following formula to encode all relevant information about graph in a CNF formula: Definition C.1 (fc). For each E V(G), let x. be a variable. The edges of G (and [VG)) can be encoded as a CNF formula fc = / (xae) (x. V xww) A (Nrev w.).
This formula is trivially satisfiable and not meaningful from logical perspective, but it uniquely encodes G up to isomorphism.
Note that for à 3, our definition of k-WL (which is more common in the machine learning literature) actually corresponds to k 1-WL. in (Cai al. 1992 Kiefer 2020).
18

---

Published as a conference paper at ICLR 2026
Observation C.2. The LCN of fo is equal to G with the following modifications. Each edge is subdivided with the corresponding clause node added the middle. The original nodes correspond to the positive literals. Two leaf nodes corresponding to the negative literal and the unit clause is connected to each positive literal.
Theorem C.3. The graph isomorphism problem on LCNs of 3-SAT formulas is equally hard as graph isomorphism on general graphs.
Proof. GI < GlsAr: Let G, H. be two graphs and let fa. fH be the corresponding formulas coding the graph structure, as in Definition C.I] These two formulas are isomorphic iff G, H are isomorphic: the two-variable clauses encode edges and the single-variable clauses encode nodes. The LCNs of fa, I'r are isomorphic iff the two formulas are isomorphic (Lemma 3.1
GISAT Gl: Let G Gr be two LCNs. This direction is easy, since G and Gy are just two graphs. Note that graph isomorphism between edge-colored graphs can be reduced to graph isomor- phism between uncolored graphs by replacing each edge with special gadget that does anywhere else in the graph, e.g. a K₃ since an LCN is tripartite. Specifically, for each literal-litens edge {z, mz). remove the edge and add a K1, connecting x and -x the same vertex in the K₃. C
oceur
D 3 3-REGULAR SAT (PROOF OF THEOREM 5.1
Recall that bipartite graph is (a, b)-reuul if all nodes in the left partition have degree and all nodes in the right partition have degree Observation D.I. (a, b)-regular bipartite graphs with na and ny nodes in the partitions are indis- tinguishable by WL.
We use the following lemma manipulate the formula: Remark D.2. Vz) - VV) (VV
Lemma D.3 (Theorem 2.1 Toveyy 1984) modified). For any 6 > 2, given 3-SAT formula f with maximum literal degree A, there is an equisatisfiable formula f with maximum literal degree 6. The formula f' has most n' + 4An variables and m' m 4An clauses.
Proof. Let æ be a variable in f with æ or -I appearing more than d times. We break the variable into s d(x:) + d(-x) variables T1,.... .......,.... F.. where s S 24. The constraint J1 Z2 equivalent to (x1 V -22 ) A (Iz V -x3) A ... A (I, V -x1). We use Remark D.2 on each clause to make them 3-regular. The end result uses 2s variables and has 2s clauses. Each original literal is used once in the constraint clauses, so it can be used - 1 times outside of it.
2. is
Lemma D.4. Given a 3-SAT formula f where each literal appears in at most 3 clauses, there is an equisatisfiabl 3-regular formula f' where each literal in exactly clauses, with most n' 5n variables and m' = m + 9n clauses.
Proof. Let T,r C be the literals in that appear in exactly 3 clauses. First, note that the number of edges in the literal-clause graph of f is
3m 3|
E d(l)
BELAL
Here, the sum of degrees of non-regular literals must a multiple of 3. We need add EeErYe 3 - d(e) 3|L \ L, - d(C) connections to make the literals 3-regular. As shown above, is a multiple of 3, so it is enough to show how to add 3 connections for literals f,, E22,,,, la (possibly some of these are equal). We introduce auxilliary variables a, b, e, d and set b = = 1, while the value of d does not matter. We add the following clauses to form f":
(e,, -b),
(a, -e, d), (a, -e, dd)
(b, aa d), a. -d)
(c, b- d),
(lz, -a,
(c. bb dd)
(Lg, mc)
Note that all 9 clauses are satisfied by either a, b or c. Also, all clauses are unique (even when lg Ex) and non-trivial (no clauses of type V -a)) All auxilliary literals appear exactly three
19

---

Published as a conference paper at ICLR 2026
times. The set of solutions of f' projected to the variables of is the same the set of solutions for f.
The number of missing connections is most 3n, so the number of added variables and clauses is
at most 4n and 9n.
E DISTINGUISHING RANDOM SAT INSTANCES (PROOF OF LEMMA 6.3
This section uses the seminal results Babai et al. (9800) on random graph isomorphism. To state results, we need some related definitions. Let R. be a class of graphs with vertices. A canonical labeling algorithm of is an algorithm which assigns numbers I,..., n to each graph in X,, such that two graphs are isomorphic if and only if the labeled graphs coincide. Note that the labeling must be permutation invariant. Given a canonical labeling, we can test two graphs are isomorphic in linear time by comparing the edges of the graphs.
Babai et al. 1980) gave a canonical labeling algorithm for isomorphism testing on random graphs:
Theorem E.1 ((Babai et al., 1980)). There a class of n-node graphs K. and linear-time algorithm that decides whether a given graph G belongs to K and computes canonical labeling of K. The probability that a uniformly random n-node graph belongs to is at least --17 for large enough n.
Proof sketch. In short, their algorithm computes a unique identifier for each node based on adja- cency to high-degree nodes. For this to work, the top := log n/ log 2 degrees must be unique. Assuming unique degrees for nodes ,i,..., 2r ordered by degree, the adjacency patterns to these nodes gives an Oloo -bi identifier x, each node v, where (Ir,); 1(u (N))). If the top degrees and the generated IDs are unique, this labeling is returned. Otherwise, the graph does not belong to K. It can be shown that both conditions hold with probability at least 1 - n 1/7 over all n-node graphs
is known that the WL test identifies all graphs in K. For clarity, we add the following lemma to make this formal:
Lemma E.2. The WL test distinguishes any two graphs G, H where G E IC and H is any graph non-isomorphic to G.
Proof. The first round labels X of WL partition nodes by degree. The partition given by labels X2 after the second round is clearly at least as fine the partition given by z. in the algorithm of Theorem E. Hence, if x, is unique for each node, then so is x Hence, the multiset of second- round labels is different for any G E K and H & K. In the third round, the unique labels encode all information about edges, so any differences in the adjacency between graphs in I. is detected. Li
F. DISTINGUISHING INSTANCES EXTRACTED FROM RANDOM LIGS
Recall the literal-nniienns graph representation of a CNF formula, where each literal is a node and two nodes are connected if they appear in the same clause. A principled way of extracting a CNF formula from a random literal-incidence graph is given by Wu & Ramanujan (202)) (see Lemma 6.2p. We show that a CNF formula constructed this way is likely identified by the WL test.
Theorem 6.3. A CNF formula extracted from uniformly random literal-ine interall-iiieecee graph with literals identified by the WL test with probability at least (n) -1/7, over the choice of LIG, for large-enough
Proof. Let G be the corresponding literal-incidence graph. We show that the LCN is identified if G identified. Color refinement identifies G, i.e. each node gets unique identifier (Theorem E. with probability at least 1n)-1/7
Consider color refinement on the LCN. We can ignore literal-literal edges due to their different color, they only add expressivity. In two iterations, the information traveling from literals literals via clauses on the LCN is exactly the same as in one iteration on G. By construction, the set of two-hop literal neighbors on the L.CN (ignoring literal-literal edges) exactly the same the set of
20

---

Published as a conference paper at ICLR 2026
neighbors in G. Hence, color refinement the LCN produces unique identifiers for the literals (in at most twice the number of iterations). Since there are no duplicate clauses, clause nodes become identified by the unique set of literals they are connected to. Since all nodes have unique identifier, the LCN is identified (as in Lemma E.2
F EXPRESSIVITY VS. COMPUTATIONAL HARDNESS
common misconception is that a problem is computationally hard (e.g. NP-complete), then the WL hierarchy will also struggle to distinguish some instances of this problem. This is not the case. Distinguishability in GNNs, or equivalently the WL hierarchy (Xu et al., 2019 Morris al. 2019) is structural notion, whereas NP-hardness concerns the computational complexity of deciding a property. These notions are unrelated: there exists NP-hard problem families that the WL hierarchy fully identifies, i.e. distinguishes perfectly. For example, 4- 4LW distinguishes all instances of PT (Theorem 6.1 even though PlanarSAT is NP-complete.
Conversely, our construction (Theorem 5.3) shows that there exists satisfiable and unsatisfiable for- mulas that remain indistinguishable to the full WL hierarchy. This indistinguihhabiity arises because the satisfiability of these formulas does not localize in a way detectable by the WL refinement, not because SAT is computationally hard.
G EXPERIMENTAL RESULTS
G.1 DETAILS ON INSTANCE CENERATION
The default size of instances in G4SATBench is limited (200-400 variables for hard instances). To generate very large instances with number of variables in the thousands, adapt the genera- tion script for 3-SAT by slightly reducing the clause-to-variable ratio from the known satisfiability threshold (Crawford & Auton 1996) of [4.258- ny + 58.26 "y -2/3 where ny is the number of variables. This is known as the threshold number of clauses for 3-SAT instances, where the ratio of satisfiable to unsatisfiable formulas is approximately 50/50, and also where the hardest instances are typically found. To produce very large instances for the 3-SAT family, we change the multiplier from 4.258 to 4518, which reduces the number of clauses slightly. This enables faster generation of satisfiable instances, while still maintaining approximately the same complexity.
G.2 FULL RESULTS
Below are Tables B and 4 presenting the full results of our experiments on the SAT competition and G4SAT benchmark instances.
The competition instances were selected from the International SAT competition from years 2020 to 2025. All instances were initially satisfiable. Due to computational constraints, only evaluated instances with size at most 10MB. Out of 448 evaluated instances, only 234 could be solved with the expressive power of WL. Across 69 instance families, 38 contained instances where WL is not expressive enough. Additionally, there were 72 instances where the evaluation timed out, because a solution was not found within hour.
21

---

Published as a conference paper at ICLR 2026
Table 3: Results instances from the International SAT competition from years 2020 2025. All instances were initially satisfiable. Tont denotes the iteration in the Weisfeiler-Lene Leman algorithm where the WL-partition WL-pariiton-coonstaindd formula becomes satisfiable (unsat if such iteration does not exist). counerged is the number of iterations for the WL algorithm to converge. All values are reported mean standard deviation.
family
crit
cconverged
Variables
Clauses
Count
algebra
43.00 0.00
44.00
0.00
12168 +
55927 0
unsat
59.00 = 0.00
45763 21854
212025 101562
3
antihandwidth
unsat
43.00 0.00
56745 +
177682 0
argumentation
2.94 + 0.44
4.31 0.87
1266 + 625
24764 + 18863
16
at at-least-two-so
unsat
7.00 0.00
2352 +
219297 +
2
auto-correlation
29.00 0.00
37869 + 0
77287 +
2
battleship
unsat
1.00
762 501
8466 = 7770
5
bitvector
unsat 30.00 0.00
11403 0
33386
1
brent-equations
31.11 3.86
72398 + 9398
307082 + 41212
9
unsat
59.00 + 0.00
78934 + 5098
350649 + 22681
2
cardinality-constrain
14.00 + 0.00
18.00 0.00
647 +
3239 +
cellular-autonie automata circuit-multicn multiplelt
59.00 0.00
42271 +
248471 #
unsat
7.18
1075 + 50
20414 = 1517
coloring
6.71
15563 28396
303330 115583
14
cover crafted-cec
unsat
56.00 = 6.00
162628 + 199188
84331 = 98439
4
18.00 1.10
19.00 1.10
25109 + 5971
75253 17929
6
cryptography
15.74 # 14.67
17.63 + 14.34
41510 # 29705
184548 # 86532
19
unsat
1
19257 37634
73907 118053
23
cryptography-
unsat 18.00 2.76
54.00 100 0.00
158751 + 58
373490 258
7
hyypogrrahy--iiee
18.67 2.80
3328 + 599
11072 + 2035
6
discrete-logarthmm
17.50 1.29
23.50 4.43
14876 + 3199
79248 + 18265
4
edge-matching
unsat
13.67 + 2.31
6615 + 3633
73913 + 44663
3
edit-distance
31.00 0.00
32.00 + 0.00
11083 + 0
155964 +
ensemble-computation
6.00 + 0.00
+.00
11607 # 0
73804 + 0
fermat
8.33 + 0.58
11.00
8203 891
45927 5155
3
lixed-shape-rande random
5.00 + 0.00
5,00
3486 + 0
8496 +
3
fpga-routing
unsat
9.50
3331 # 1783
42108 + 27772
2
generic-csp
unsat 7.00
840 + 402
9858 + 4852
2
hamiltonian
4.17 0.51
5.54
550
4951 408
18
hamiltonian-cycle
unsat 0.00
$ 5180
266845 # 38797
9
ww-mooel-check
unsat
3.55
119179 39350
419860 + 67060
2
heule-folkman
unsat
4.91 101
16614 # 1103
20147 # 1492
11
heule-nol
unsat
8.60 1.26
1419 +
7832 +
10
hgen
5.00 0.00
5.00
321 +
1123 +
14
influence-max knights-problem
19.00 + 2.83
21.50 3.54
11323 + 6549
62832 + 36781
2
unsat
+4.33+1.11
107589
25778
389927 + 91758
matrix matrix-multpliics multiplication
9.00 + 0.00
1.000
2396 +
83733
1
max-const- part
23.00 0.00
52.00
30252 0
123402 +
2
maxsat-optimum
26.64 + 3.64
29.27 + 2.49
22157 + 5623
250704 + 108568
11
unsat
59.00 + 0.00
27597 + 8713
318348
145483
7
minimal-disagee Linimal-disagreementt
unsat
59.00 + 0.00
3176
10283 + 42
2
parity
minimal-
36.67 4.04
40.00 + 3.46
7885 + 2006
26129 + 5579
3
superpermutation
unsat
59.00 + 0.00
9075 +
26255 + 15479
2
min-dis-parity
unsat
8.73 + 0.96
1042 211
5861 + 1234
15
modcircuits
unsat
-
479 +
123509 +
1
multiplier-cireut
33.20 # 12.49 14.00 0.00
37.80 11.90
10955 + 5629
43559 + 22450
10
planning
26.00 0.00
439 +
5423 +
1
unsat 25.00
29.44
8666 + 5382
74156 + 36566
3
poly-mult
unsat
55.57 + 9.07
57580 31837
228133 126348
7
22

---

Published as a conference paper at ICLR 2026
factoria
13.33 + 10.69
16.17 15.14
2305 + 2557
6
prime-testing
33.25 # 14.15
34.00
14.54
30102 47706
98632 134347
4
purdom-instances
22.33 2.31
28.33 11.85
4661 327
18469 = 1302
3
pythagorean-trilles
7.00 0.00
7.00
3690 + 4
13674 # 75
2
quasigroup-compl
4.00 0.00
4.00
20940 + 5970
436860 149323
2
unsat
5.00
1890 + 0
12666 + 0
1
random- random-cireuits
1.13
3115 231
184064 = 13856
3
random-csp
3.60 + 0.89
3.80
799 + 369
35723 + 18087
5
random-moduus mandom-modularity
3.00 0.00
4.00
2200 +
9086 +
2
rbsat
4.00 0.00
4.00
869 206
55161 + 22567
9
scheduling
12.14 2.19
3.448
16459 + 3223
113224 + 122825
unsat
30.86 13.37
35633
29001
158119 102896
28
set-covering
2.00 0.00
4.00
758
31049 + 3275
12
sgen
unsat
1.00
220 = 57
528 + 136
2
sliding-puzzle
31.00 0.00
3.00
23029 + 0
86273 +
2
social-golfer
13.67 1.15
16.67 0.58
17469 10785
103810 + 72947
3
unsat
7.63
8098 + 3956
91566 + 65385
3
software-verffication
54.00
20965 # 0
93999 #
ssp-0
12.00 + 0.00
2.00
50093 0
214490 +
stedman-triples
9.29 1.54
10.14 1.41
6225 + 4578
142252
118879
14
subgraph-iso
4.00 + 0.00
5.00
1065 + 382
124130 73773
3
unsat
1.00
598 + 0
14076
sum-of-3-cuhes
11.50 + 0.58
35914 + 6913
175274 + 34488
4
summle
unsat
3.00
102501
12815
215796 + 24955
17
tensors
14.92 + 0.29
1.00
3220 = 0
12439 #
12
termination-analysi
13.00 0.00
17.00
15092 0
65248 +0
1
tree-decomposition
unsat
0.00
74804 + 0
393322
2
Iseitin-formut
8.33 1.15
8.67 + 0.58
334
2356 + 147
unknown
9.33 + 2.52
10.33 3.21
2525 # 1849
267927 21151
3
unsat
7.33 + 1.15
7594 # 7090
125672
112383
3
waerden
2.00 0.00
4.00 + 0.00
242 = 16
31376 3731
2
23

---

Published as a conference paper at ICLR 2026
Table 4: Results the instances from the G4SAT benchmark. Instances are divided by family and difficulty, where difficulty follows the size-based categorization in (Li et al. 2024). The benchmark designed that all instances ratio, which fixed close to the satisfiability threshold for 3-SAT, and analogously for families encoding combinatorial problems. All instances
challenging: hardness is controlled via the clause-to- to-uribb-
initially satisfiable. Taris denotes the WL iteration where the WI.-partition constrained formula becomes satisfiable (unsat such an iteration does not exist). Tconverged the number of iterations for the WL algorithm converge. On average, few iterations is enough for WL to sufficiently distinguish literals, except for few outlier instances in the k-clique, v-vertex cover and ca families. The PS family is omitted due to problems with the generation script. All values are reported as mean + standard deviation.
Perit
i Tcunverged
Variables
Clauses
Count
family
difficulty
3-sat
easy
0.17
3.68 + 0.47
2
119 36
1000
medium
3.00
3.92 # 0.28
119
509 + 198
1000
hard
4.00 0.00 0.00
250
2 29
1065 + 125
100
hard+
4.00 3.00
921 48
3775 # 196
24
hard++
3.08
4.00
5001 62
20504 256
k-clique
easy
0.73
6.86
33
543 + 426
960
unsat
6.77
2
217 194
medium
4.11 + 0.52
0.95
68
2156 + 960
999
unsat
6.00
4
939 +
hard
4.00
6.00
114
5554 1718
100
k-domset
easy
4.71
5.99
32
329 # 186
1000
medium
0.58
5.50
88
1647 # 687
1000
hard
0.67
5.69
137
3986 + 1315
100
k-vercov
easy
4.75 1.14
6.18
33
358 245
993
unsat
4.00
26
159 + 108
7
medium
4.94 1.00
5.88
96
2052 + 936
1000
hard
5.00
5.80
259
7198 + 2159
100
Sr
easy
0.05
3.00
25
146 54
1000
medium
0.12
3.00
118
644 + 249
1000
hard
0.22
3.00
299
1613 + 343
100
24


Reviews:
[{"review_id": "zZBu3STjtk", "reviewer": "Reviewer_ZqMt", "summary": "This paper analyzes the expressiveness power of graph neural networks (GNNs) for the Boolean constraint satisfiability problems. The analysis is based on the observation that the power of GNNs is bounded by Weisfeiler-Leman (WL) test, which is designed to test graph isomorphism. Due to such fundamental limitation, GNNs are proved to be insufficient to solve NP-Complete problems. Furthermore, empirical evaluations are performed on the G4SAT benchmark and SAT Competition 2024.", "questions": "Besides consolidating previous known results, which is a meaningful contribution in the perspective of literature survey, what new insights either theoretical or empirical does this paper provide?", "limitations": "", "rating": 4, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 1, "strengths": "- this paper consolidates many known theoretical results about GNNs and WL test as well as empirical datasets\n- background knowledge about SAT solving, GNNs, graph isomorphism, and WL tests are carefully illustrated", "weaknesses": "- the proposed analysis is not novel, since all reported results are either well-known or immediately implied by previous works. Particularly, Xu et al. (2019) has pointed out that GNNs are bounded by the WL-test, which cannot even solve the graph isomorphism problems that are not as strong as the NP-Complete problems like Boolean satisfiability. \n- the presented theoretical analysis is largely rephrasing previous known results therefore does not contribute new insights\n- there are some empirical observations regarding the number iterations for WL to converge, however, which does not provide meaning guidance on solving satisfiability problem with GNNs", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "FrK5ylM4G8", "reviewer": "Reviewer_cb9V", "summary": "The paper analyzes the expressive limits of GNNs on SAT problems using a literal–clause–negation (LCN) graph representation. It proves that even the full Weisfeiler–Lehman (WL) hierarchy cannot, in general, distinguish satisfiable from unsatisfiable 3-SAT formulas, via a parity-based construction. The authors further show that this limitation persists in sequential variable-assignment settings, linking theory to neural SAT solvers. They complement the negative results with positive findings (e.g., PlanarSAT identifiable by 4-WL) and empirical WL-color diagnostics on random and industrial benchmarks. The work provides a clear, rigorous theoretical contribution, though experiments remain illustrative rather than learning-based.", "questions": "Given that the experiments are WL-diagnostic rather than learned, do you plan to test whether these expressivity limits manifest in actual trained GNN solvers?\n\nGiven that even n-WL cannot distinguish SAT/UNSAT in general, what architectural modifications beyond standard MPNNs (e.g., augmentations, auxiliary features, hybrid approaches) do you believe could address these expressivity bottlenecks while remaining scalable?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "The presentation is clear and well-organized with logical progression from simple examples to full results, making complex theoretical concepts accessible while providing complete proofs in appendices. The analysis is nuanced, including both impossibility and positive results (e.g., PlanarSAT separability, random instances).\nThe authors are transparent about the scope of their results, clearly acknowledging that their experiments test only necessary conditions for expressivity and do not demonstrate actual learning performance.\nThe main theoretical contribution (Theorem 5.3) is rigorous, proving that even the full n-WL hierarchy cannot distinguish SAT/UNSAT formulas in general, and this limitation transfers to practical sequential solvers (Corollary 5.5), showing that even after Θ(n) variable assignments, the indistinguishability persists - meaningfully connecting fundamental expressivity limits to realistic GNN-based SAT solving approaches. The link to Tseitin formulas from proof complexity is noteworthy.", "weaknesses": "The paper lacks any trained GNN experiments, making it unclear whether the theoretical limitations observed actually translate into performance gaps in practice.  The experiments are purely diagnostic and do not involve any trained GNNs, leaving the practical impact of the theoretical limits untested.\n \nLacks an explanation for why industrial instances require higher expressivity than random ones. The paper does not discuss possible ways to overcome the identified expressivity limits, leaving the reader without guidance on how future GNN architectures might address these shortcomings.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "MyzmVN8s93", "reviewer": "Reviewer_4PqT", "summary": "The power of GNNs can be understood by studying WL-testing, which is basically a form of graph isomorphism testing. On a high level, GNNs cannot distinguish some graphs from each other and this is reliant on how the weisfeiler lehman kernel behaves on these graphs. The paper shows that even if GNNs were \"maxed out\" on the WL power hierarchy, there would be SAT instances that would be difficult for them since it is difficult for the WL process itself (this is actually not surprising, given that SAT is a hard problem) but more interestingly, it creates these hard instances constructively, which is better than showing that they exist. Empirically, it then studies real SAT instances. Probably as expected, random SAT instances can fall to WL , and contest SAT instances don't fall as easily.", "questions": "It seems to me that the paper is actually about the suitability of the WL kernel to SAT, and can be thought of better that way. Do you agree ? From a GNN point of view, the empirical section is actually not meaningful (as pointed out under weaknesses)", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper's contribution is mostly theoretical. One of the best aspects is that they actually construct the hard family of instances, which is likely to be useful for further work more than a simple proof of existence. Also, although the paper is about GNNs on paper, most of the results are about the WL kernel's suitability for SAT, which is technically a broader problem. In reality, the paper is about finding the \"blind spots\" of the WL kernel as a method.", "weaknesses": "The empirical study is fairly surface level and misses the mark. We already expect that random instances are easy, contest instances are harder, and hard-by-construction instances are computationally hard. But the main problem is as follows. The power of a GNN is only upper bounded by the power of a WL test. Showing how well the WL test performs on various SAT instances, then, is meaningful only in one direction - if it fails, certainly we don't expect GNNs to succeed, but if it succeeds or performs in an intermediate manner, we *cannot actually confirm* that GNNs will follow ! Thus, the construction of the hard instances is meaningful \"back to GNNs\" though WL is being studied, but the studies on empirical \"actually existing\" instances are statements that only mean something wrt the WL kernel, not GNNs themselves.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "PuStUg5nKb", "reviewer": "Reviewer_2HM5", "summary": "The paper analyzes the expressive capabilities of Graph Neural Networks (GNNs) in the context of SAT solving. The authors particularly look at the Literal-clause graphs with negation connections (LCNs), one of the standard representation used in GNNs for SAT solving. The authors then theoretically prove which families of problems GNNs can and cannot distinguish, using the Weisfeiler-Lehman (WL) test, a well known expressivity analysis technique for GNNs. With experiments, the authors assess whether WL-powerful architectures are, in principle, capable of predicting satisfying assignments on a wide range of benchmark instances including randomly generated and competition benchmark instances. The results show that while almost all random instances are WL-distinguishable, many SAT competition instances are indistinguishable, showing the limitations of GNNs for industrial SAT solving.", "questions": "- Is it possible at all to extend the WL-test to allow for expressivity analysis of VCGs?\n- Are there other suitable graph representations of SAT problems that would be better than LCNs in terms of expressivity? What would the best representation look like, if any?\n- Why were harder instances (hard+, hard++) provided only for 3-SAT? Is it not possible to generate harder instances for other problems as well?\n- The experimental analysis were done on SAT instances only. Would it be possible to extend the analysis to UNSAT instances?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The theoretical results imply that with LCNs, any Message Passing Neural Network based models cannot fully distinguish between SAT and UNSAT instances for certain families of problems such as 3-SAT, even when given partial assignment information.\n- The authors conduct experimental results to determine whether instances in a benchmark set are WL-distinguishable or not, with the experiments being done on a wide range of benchmarks sets.\n- The paper provides insights into the limitations of GNNs for SAT solving, which is an important topic given the recent interest in using machine learning for combinatorial optimization problems.", "weaknesses": "- The theoretical results are limited to LCNs, due to the limitations of expressivity analysis with WL tests as stated in the Appendix. While I understand LCNs to be a common approach of using GNNs for SAT solving such as in NeuroSAT, VCGs are also widely used such as in [1], and the paper would greatly benefit from discussing their insights, other than just briefly stating that it is not possible to perform expressivity analysis on them. I personally think that as VCGs incorporate polarity information directly into the graph edges, it allows them to distinguish graphs for formulas such as those in Figure 2.\n- The random instances from G4SATBench may not be as informative as ones from the SAT competition. To my understanding, this comes down to whether the benchmark was able to randomly produce any problem that is difficult to solve. If performing evaluations on random instances were the objective, the random track from the 2018 SAT competition may be better suited in this regard.\n- I see no reason to limit the experimental results to the 2024 SAT competition benchmarks. Including benchmarks from previous years would only strengthen the experimental contributions.\n\n[1] Yolcu, E., & Póczos, B. (2019). Learning Local Search Heuristics for Boolean Satisfiability. In H. M. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché‑Buc, E. B. Fox, & R. Garnett (Eds.), Advances in Neural Information Processing Systems 32 (NeurIPS 2019) (pp. 7990–8001).\n\n\nMinor issues:\n- The graph visualization in Figure 1 does not match up with the formula given. I believe that C6 should be C1, if we assign clause numbers in order of appearance.\n- Figure 2 seems to be in the middle of the references section.\n- Citations are not formatted correctly; they are missing parentheses. For example \"variables Heule et al. (2024)\" at L123 should be \"variables (Heule et al., 2024)\".\n- In L132 and L137, $\\chi^\\ell(v) := (\\chi^{\\ell-1}(v), \\{ \\{ \\chi^{\\ell-1}(v) : w \\in N(v) \\} \\})$ should be written as $\\chi^\\ell(v) := (\\chi^{\\ell-1}(v), \\{ \\{ \\chi^{\\ell-1}(w) : w \\in N(v) \\} \\})$ (the $v$ should be $w$ in the inner set).\n- In L412, it says \"the only family with some formulas that could not be solved by WL is the k-clique\", but Table 4 clearly shows k-vercov as another family that WL could not fully solve.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)