Structure Based Dataset on SAT Solving with Graph Neural Networks

Authors: yi  fu
anthony  tompkins
yang  song
maurice  pagnucco
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-26 10:24:42

Abstract: Satisfiability (SAT) solvers based on techniques such as conflict driven clause learning (CDCL) have produced excellent performance on both synthetic and real world industrial problems. While these CDCL solvers only operate on a per-problem basis, graph neural network (GNN) based solvers bring new benefits to the field by allowing practitioners to exploit knowledge gained from previously solved problems to expedite solving of new SAT problems. Prior works in the GNN for SAT space often improve the performance of GNN based solvers with novel architectures or large synthetic datasets. However, one specific area that is often studied in the context of CDCL solvers, but largely overlooked in GNN solvers, is the relationship between graph theoretic measure of structure in SAT problems and the generalisation ability of GNN solvers. To bridge the gap between structural graph properties (e.g., modularity, self-similarity) and the generalisability (or lack thereof) of GNN based SAT solvers, we present StructureSAT: a curated dataset, along with code to further generate novel examples, containing a diverse set of SAT problems from well known problem domains. Furthermore, we also utilise a novel splitting method that focuses on deconstructing the families into more detailed hierarchies based on their structural properties. With the new dataset, we aim to help explain problematic generalisation in existing GNN SAT solvers, and demonstrate an alternative approach to expedite GNN training efficiency by exploiting knowledge of structural graph properties. We conclude with multiple future directions that can help researchers in GNN based SAT solving develop more effective and generalisable SAT solvers.

Main paper: 
 introduction: 
 The satisfiability (SAT) [10] problem is a hallmark of computer science research with remarkable real-world utility, especially in solving combinatorial optimisation problems. SAT has formed the basis of the study of computational complexity especially around the complexity class of NP problems. Moreover, as a theoretical tool, it has facilitated research into the nature of computation and solving difficult computational problems. On the practical side, SAT has been applied to many interesting real world problems such as logistics planning [36] , product configuration [56] , and software verification [34] , retaining its high relevance today. complementary approach to representing and solving SAT problems by incorporating the benefits of deep learning [26] . Using an optimisation based approach, as opposed to a pure search like algorithm in CDCL, GNN-based solvers have the potential to adapt useful information from training problems to accelerate solving unseen novel problems.However, SAT problems largely reside in NP-hard problems. In reality, for machine learning methods such as GNNs, prior works have demonstrated provably negative results on challenges that are NP-hard [62] . Although deep neural networks have the ability to ingest large datasets [39, 55] , there lacks a dataset that facilitates sufficiently large and unbiased training for SAT problems, and existing SAT datasets with higher difficulties generally have a limited number of problems. Indeed, currently the largest benchmarks SATLIB [32] and SATCOMP [33] contain less than 10k industrial problems. While we can generate synthetic datasets to train GNNs [53] , the resulting models would struggle to generalise to more diverse and challenging, or real-world problems [44] , limiting the application of GNN-based solvers. Moreover, we believe generalisation in the context of SAT problems has currently been greatly underrated and oversimplified. More specifically, SAT problems in prior work are typically generated in a random manner without delving into what makes instances difficult or useful for training, potentially limiting the models from generalising to more challenging datasets, especially to industrial instances. For example, the largest SAT dataset on GNN -G4SATBench [44] , which is constructed with 7 generators, only considers generalisation on the numbers of variables as a measure of performance vs. complexity. However, the impact of the quality of a dataset is greatly overlooked and remains a less explored area. In particular, problem difficulty can be strongly influenced by the intrinsic graph structure of each problems, as shown experimentally on traditional solver [2] . No prior work has shown if the same structural properties studied in SAT so far could influence GNN's performance, especially their ability to generalise.To bridge the gap between structural measures and generalisability of GNNs on SAT, we propose StructureSAT, a large-scale dataset containing diverse problem domains and structural measures. In this work, we are not interested in the set of all possible SAT problems, but rather existing, well studied, SAT problem domains which we aim to analyse through the lens of graph theoretic structure. Thus, we focus on small, easy-to-generate synthetic training datasets for developing GNN models that can better generalise. StructureSAT contains 11 SAT domains from 4 high level categories: random, crafted, pseudo-industrial and industrial, within which we study 9 structural properties that have proven to be influential to traditional SAT solvers, including both conjunctive normal form (CNF) based and graph based properties [2] . We carefully deconstruct each problem domains based on their structural properties, and split each domain into low-value property subsets and high-value property subsets for each of the properties. Details of the dataset can be found in Appendix B. Moreover, to capture the relationship between the SAT problem structures and generalisation ability of GNN solvers, we conduct thorough experiments using 3 GNN baselines and benchmark their generalisation performance on a diverse set of in-domain and out-domain problems. Our results highlight the existing challenge and potential future directions on improving the generalisation performance of current GNN-based solvers. We bring light to training set to test set generalisation in GNN-based SAT solvers, and graph theoretic notions of structure, which have been well studied in the CDCL SAT literature but only lightly touched on for GNN-based SAT solving. 
structuresat: 
 StructureSAT consists of multiple problem domains, for each of which we control the corresponding attribute values. In this section, we briefly explain SAT problems and present the structure properties measured in the dataset. Then, we introduce the types of data and generators used for raw data generation. Lastly, we detail our structure-based splitting method. Detailed explanations of our dataset are presented in Appendix B.In propositional logic, the SAT problem is the problem of finding an assignment of truth values (true or false) to propositional variables that make a Boolean formula satisfiable (i.e., true). Boolean formulae are typically expressed in conjunctive normal form (CNF). We denote the set of propositional variables by V . A literal l is either a variable v ∈ V or its negation ¬v (or v). A clause c is a disjunction of literals (l 1 ∨ l 2 ∨ ..l n ), where ∨ denotes propositional logic "or". A formula f is a conjunction of clauses (c 1 ∧ c 2 ∧ ...c n ), where ∧ denotes propositional logic "and". Generally speaking classical SAT solvers can be divided into complete solvers and incomplete solvers. A complete solver is able to prove unsatisfiability or find a satisfying assignment if they exist for a problem. Most complete solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm [18, 17] , a backtracking search algorithm. Two popular variations of DPLL solver are the Conflict-Driven Clause Learning (CDCL) solvers [46] , which learn and add new conflict clauses to the original formula, and look-ahead solvers [31] , which do lookahead for a selected decision variable. In contrast, an incomplete solver cannot prove unsatisfiability such as the Moser-Tardos (MT) solver [12] and WalkSAT solver [51] that are derived from the stochastic local search (SLS) algorithm, which repeatedly selects variable and changes its value until an assignment or a limit is reached.SAT formulas have been expressed using various graphs focusing on different structural properties [2] . Traditional SAT community usually encodes SAT formulas as undirected weighted graph including variable incidence graph (VIG) and clause-variable incidence graph (CVIG) [7] . VIG is a graph with literals as nodes and two literals are connected with edges if and only if they occur in the same clauses. CVIG is a bipartite graph having the set of variables and clauses as vertices. They are connected if a variable occurs inside a clause. Another commonly used set of graphs are unweighted graphs including VIG, variable clause graphs (VCG), literal incidence graphs (LIG), and literal clause graphs (LCG). LIG extends VIG through extra edges between literals and their negations. VCG and LCG are bipartite graphs similar to CVIG, but without weights. LCG also has an extra edge between literals and their complements. Among all the graphs, LCG has been used most in GNN based SAT solving as others either lose important information of clause (LIG and VIG), or information of polarity (VCG). As prior research [44] has shown that the particular bipartite graph construction (LCG or VCG) does not have much effect on model accuracy while non-bipartite graphs (LIG or VIG) , we will be focusing on LCG only.In this work we classify structural properties of SAT problems into two classes based on the embedding methods: CNF based properties and graph based properties [1] . These properties are used as splitting method for training and testing in the dataset.Given a SAT problem P , the CNF based properties are related to the CNF encoding of P . The most popular ones are Backbone [37] and Phase transition [14] . Graph based properties are structural properties from embeddings of a LCG graph G. Given a problem with set of variables V and set of clauses C, the LCG graph G with vertex X and weight w is defined as G = (X, x|x ∈ C ∧ V , w) and the weight is either 1/|X| if variable is in clause, 1/|V | for weights between variables and their negations, or 0 if nodes are not connected. Each node x in graph has degree deg x . Included graph properties in StructureSAT are Self-similary [3] , Scale-free [6] , Treewidth [47] , Centrality [22] , Community structure [5] , Small-world [58] and Entropy [66] .We use various existing SAT generators and datasets to produce original SAT formulas in 11 domains. These include Random-3-SAT generated using CNFgen [40] , SR(n) [53] , Combinatorial problems (5 domains) from CNFgen [40] , Community Attachment (CA) from [24] , Popularity-Similarity (PS) [25] , industrial problems SATCOMP from SATCOMP2007 and psudo-industrial problems from Graph Generative Models G2SAT [63] .We also propose a novel splitting method for StructureSAT and focus on 3 types of generalisation tasks. After generating the raw datasets, instead of randomly splitting them to train/valid/test sets, we divide each raw datasets based on specific structural values. Specifically, for each domain, we select the average value Z from every calculated graph-based properties, as shown in Table 3 , and split each domain into a low-value subset and a high-value subset, producing a total of 16 subsets (8 structures * 2 ranges) per domain. Each subsets contains 80k training data and 10k validation data. 1For different testing sets, we focus on 3 aspects of test problems: in-domain larger problems, in-domain problems with different properties, and out-of-distribution problems. Specifically, for in-domain larger problems, we follow the random generation process and generate larger problem sets for all the synthetic generators. For example, for training with SR problems, the training and validation sets contain problems with 10-40 number of variables, while the testing sets contain problems with 40-100 and 100-200 number of variables, each with 10k pairs.To test generalisation on in-domain problems with different structures, we are interested in random 3-SAT with different c/v ratios and different backbone values on all domains. For analysing the CNF based property -c/v ratio on random 3-SAT, the training and validation sets are problems with 10-40 number of variables, and a c/v ratio of roughly 4.7. Our testing set contain random 3-SAT problems with same number of variables, but different number of clauses. Specifically the test set has a c/v ratio of 3.5, 4, 5.5 and 6, with each ratio having 10k pairs of problems.For out-of-distribution problems, we randomly generate 10k problem pairs from each synthetic generators without property split, while also including small-size industrial and application problems from SATCOMP and generated G2SAT problems.We also empirically analyze the effect of augmentation to generalization, since this might cause the destroying of structure during the addition of learned clauses [5] . Prior work [44] has shown that training on problems with adding learned clauses from CDCL solvers could lead to better accuracy on augmented SAT domains than training on raw problems. Thus, we gather learned clauses from produced DRAT-trim proofs [60] after running problems with the CadiCal solver [21] , then augment our dataset with the collected learned clauses. 
experiment: 
 In this section, we experimentally evaluate the out-of-distribution generalisation ability of GNN-based SAT solvers with StructureSAT. Specifically, we investigate the following questions: Q1: How does the structure influence generalisation to larger size problems; Q2: Could GNNs generalise to the same domain but for problems with different structure; Q3: How much does structure influence out of distribution generalisation; Q4: Does training on augmented problems influence out of distribution generalisation? Due to the limit in space, we will present the experiment on Q3 and Q4 only in the following section. All other experiments can be found in Appendix F.With the newly developed dataset, with details we conduct several experiments on the task of predicting satisfiablity of SAT problems, which is considered as supervised binary graph-classification task. We consider 3 baseline GNN models NeuroSAT [53] , GCN [38] and GIN [61] in our experiments and follow the implementation of G4SATBench [44] . We refer the reader to Appendix E for more implementation details. As prior work has shown that different GNN models perform similarly in general [44] , we want to emphasise that the main focus of this paper is to find the general trend on generalisation performance of GNN-based SAT solvers with regard to various structural measures, which can guide future development of robust GNN-based solvers applicable to challenging problems.Out-of-distribution generalisation without augmentation To answer Q3, we train NeuroSAT on the small and big split of SR , and test on different domains without splits. As presented in Table 1 , the results differ vastly across the structures and domains. Taking D f as an example, both k-clique and PS have similar D f values. However, testing results on PS are significantly better than on k-clique. Furthermore, models trained on larger D f group seems to do better on PS, while PS has a larger D f value than SR on average. This suggests that training on problems with similar metric as testing problems could possibly increase GNN performance. However, it contradicts the fact that smaller α v reaches better performance on CA, as CA dataset has bigger α v value than SR(n). One possible reasons for this contradiction would be that the performance of GNN is not determined by one single metric property, but rather a combination of properties. A Related work SAT dataset. SAT problems can be classified into different categories, mainly as random, crafted, and industrial [1] . Research studies related to SAT either generate synthetic instances using generators or use existing datasets. Most generators focus on similar type of problems like random k-SAT and combinatorial problem generators like CNFgen [40] . The largest established datasets are SATLIB [32] and the yearly SAT Competitions (SATCOMP) [33] . To overcome the limitation on number of instances in existing industrial dataset, new generators have been proposed to generate pseudoindustrial SAT instances, including hand-crafted generators Community Attachment (CA) [24] and Popularity-Similarity (PS) [25] , or graph-generative models generators [63, 43, 42, 15, 23] . For GNN based SAT solving, [53] proposed random generator SR(n) and [11] generated uniform-random 3-SAT instances as datasets. G4SATBench [44] produced a dataset including 7 types of synthetic generators with varying variable sizes. Following G4SATBench, our dataset extend to 10 types of synthetic generators with better quality and hardness measures from structural values. We also include industrial dataset for more generalisation test and analysis on real-world application.SAT structural properties. As traditional SAT solvers perform differently over random, crafted, and industrial instances, it is believed that different SAT domains have distinct underlying properties [2] .Results in this filed have been wildy used in improving traditional solvers [8] and portfolio based solvers [57] , classifying benchmark [4] , generating instances [25] , and defining problem hardness [49] . Thus, many attempts have been made to define, prove, and analyze the structural measures within SAT, including problem-based properties and solver-based properties. Problem-based properties are further divided to CNF-based, including phase-transition [14] , backdoor [37] and backbones [37] , and graph-based, including scale-free [6] , self-similar [3] , centrality [35] , treewidth [47] , entropy [66] , small-worlds [58] and community structure [5] . Solver-based properties are directly related to SAT solver such as: mergeability and resolvability [67] . These measures are either proved mathematically, or analyzed through solver-related parameters such as solving time. However, all the works are experimented with traditional SAT solver. Furthermore, there is little work on multiple properties [41, 67] while most works only focus on single measure and benchmark. In this work, we select several related measures from [1] , and calculate their values on each of our selected domains. We also propose new splitting method of our dataset to high-value subset and low-value subset of each structure, while analyzing them against cross-domain generalisation result on GNN, concluding the important and hard features for GNN to capture.GNN for SAT solving. GNN has been applied to SAT solving mainly as problem solvers, including standalone solvers and hybrid solvers. Standalone solvers are networks trained to classify problems as satisfiable or unsatisfiable themselves, which mainly encodes the formula as LCG graphs [53, 64, 13, 54, 11, 30, 19, 50] . On the other hand, hybrid solvers treat GNN as a guidance to traditional solvers by replacing their heuristics with network predictions. These solvers focuses on predicting specific tasks such as UNSAT core [52] , glue clauses [29] , backbone variables [59] , for CDCL solvers and initial assignment [65, 45] for SLS solvers. Although hybrid solvers generally achieve better results than standalone solvers, they acts as modifications of traditional solvers instead of discussing solvability of GNNs, which is out of scope of our work. Furthermore, for most GNN-based solvers, only the ability to generalise to larger in-distribution problems is discussed, which ignores the underlying structure of each domain. In this work we train several GNNs as standalone solvers from [44] , and combine the structure properties of SAT with out-of-distribution generalisation on GNN.StructureSAT consists of multiple problem domains, for each of which we control the corresponding attribute values. In this section, we start by presenting the structure properties measured in the dataset. Next, we introduce the types of data and generators used for raw data generation. Last but not least, we detail the construction process of our dataset, our structure-based splitting method, and the generalisation tasks we focus on.In this work we classify structural properties of SAT problems into two classes based on the embedding methods: CNF based properties and graph based properties [1] . These properties are used as splitting method for training and testing in the dataset. While there are usually 4 types of graphs to represent SAT problems Fig. 1 , we use the LCG graph in this work due to having the most amount of information among all 4 types. CNF based properties. Given a problem P with set of variables V , the CNF based properties are related to the CNF encoding of a problem.• Backbone [37] refers to the set of literals of a problem which are true in all satisfying assignments. The value of each literals in the set is fixed in all assignments of the problem. StructureSAT calculates the size of the backbones(B b ) of satisfiable instances only.• Phase transition [14] is a phenomenon measured by clause to variable ratio (n c /n v ), where n c and n v represents number of clauses and variables respectively. It is evident that an easy-hardeasy pattern occurs for random k-SAT where transition for random 3-SAT is at c = 4.258 * n + 58.26 * n -1/2 [16] . Although the phenomenon has been observed in both random k-SAT and peudo-industrial instances, we will only be focusing it on random 3-SAT in this dataset.Graph based properties are structural properties from embeddings of a LCG graph G. The definition is extended from the CVIG definition from [7] . Given a problem with set of variables V and set of clauses C, the LCG graph G with vertex X and weight w is defined as G = (X, x|x ∈ C ∧ V , w) and the weight is either 1/|X| if variable is in clause, 1/|V | for weights between variables and their negations, or 0 if nodes are not connected. Each node x in graph has degree deg x .• Self-similary [3] is measured by fractal dimension(D f ). G is self-similar if the minimum number of boxes of size s required to cover G decreases polynomially for some D f .• Scale-free [6] can be measured by frequency of variables (α v ) or clauses size (α c ). A graph is scale-free if the arity of nodes is characterized by a random variable N that follows a power-law distribution.• Treewidth (T w ) [47] measures the tree-likeness of graphs. It is the minimum width over all possible tree decomposition of G. In this work we calculate treewidth using treewidth -min -degree function from NetworkX [27] , which calculates using the Minimum Degree heuristic.• Centrality specifies how important a node is within a graph. Following [22] , Betweeness Centrality BE = jk px j ,x k (xi) px j ,x k is studied, where p xj , x k (x i ) is the number of paths that pass through x i ,and p xj , x k is the total number of shortest paths from node x j to x k .• Community structure [5] is measured by modularity(Q). The modularity Q of G is a value from 0 to 1, computed with respect to a given partition C of the same graph and is a measure of the fraction of within-community edges in relation to another random graph that has an equal number of vertices and degree. A graph's modularity score corresponds to the maximal modularity of any possible partition in C: Q(G) = max{Q(G, C)|C}. While computing the exact value of Q is NP-hard, it is possible to approximate lower-bounds to Q, which can be calculated asQ(G, C) = Ci∈C x,y∈Ci w(x, y)x,y∈V w(x, y)EQUATIONwhere w(x, y) is the weight between vertex x and y.• Small-world [58] measures the extent of graph topology. It is approximated using Proximity Ratio (P r ). A graph is considered small-world if P r ≥ 1. In this work we use the sigma function from NetworkX [27] for calculation, which is only an approximation of the P r value due to the need for random graph generation. • Entropy [66] measures the uncertainty of random systems. Given volume of the graph vol G , we measure the One-dimensional Entropy (H) following [66] , which can be defined asEQUATIONWe use various existing SAT generators and datasets to produce original SAT formulas in 11 domains.To analyse the property distributions in different domains, we generate 10k problem pairs for selected domains, with each pair containing 50% satisfiable and 50% unsatisfiable problems. Although the generated problems are easy for traditional SAT solvers to solve, they contain a variety of properties and are efficient for modern GNNs to learn on, which provide enough insight for our purpose. Fig. 2 shows the distributions of various structural properties described in Appendix B.1 from calculating the statistical values on raw data pairs with a 60 seconds timeout. For industrial SAT problems and graph generative model generators, less than 100 pairs are selected. In the next section we detail the provided domains in StructureSAT, including important parameters used for generation.Random-3-SAT: Uniform random 3-SAT (r-3SAT) is a special case for Random k-SAT where each clause contains exactly 3 literals. The problems are generated using CNFgen [40] with 10 -40 number of variables at the phase transition point. [53] is a special expression of random k-SAT that consists of a balanced dataset with pairs, with k as the maximum number of variables in the problem. Each pair contains one satisfiable problem and one unsatisfiable problem, differing by 1 single literal in one clause. In this work we use problem with 10 -40 number of variables as main training data, represented as SR .SR(n): SR(n)Combinatorial problems (5 domains): For most combinatorial problems, the goal is to find some combination of elements in a solution space while respecting defined constraints. A valid solution would correspond to a satisfying assignment in the SAT encoding of the problem [9] . In StructureSAT, we generate 5 combinatorial problems using CNFgen [40] . Each problem is related to solving constraints over a graph. Thus, we generate random graphs using the Erdős-Rényi model [48] with edge probability v k-1/( v 2 ), where v representing number of vertex. The selected parameters and problems include k-coloring, CA: Community Attachment (CA) is a seminal work generated from [24] to mimic the community structure of industrial problems, i.e., value of modularity Q on a SAT instance's VIG graph. In StuctureSAT, we select 0.7-0.9 as the value of Q. The generator uniformly and randomly selects 4 to 5 literals inside the same community with probability P = Q + 1/co, where co is the number of communities, and 4 to 5 literals in distinct community with probability 1 -P . These process are done iteratively to form a formula.3 ≤ k ≤ 4, k-dominating-set, 2 ≤ k ≤ 3, k-clique-detection, 3 ≤ k ≤ 4, k-vertex-cover, 3 ≤ k ≤ 5,PS: Popularity-Similarity (PS) [25] is a problem generation algorithm developed on the idea of locality, which is a measure of both community structure and scale-free structure on a SAT instance's VCG graph. PS randomly samples variable v in clause c with the probability T , where β is the power-law distribution, θ is random angle assigned to v and c, T is the temperature between 0.75 and 1.5, and R is an approximate normalisation constant.P = 1/(1 + n β v * n β1 c * θ nv * nc /R)G2SAT: To overcome the limiting number of instances in industrial problem, graph generative models have been used as problem generator. In this work we mainly use G2SAT [63] as generator. Following previous work, we select 20 problems from the industrial dataset, standadise with SatElite preprocessor [20] , and generate similar instances using GraphSAGE [28] and a two-phase generation process. Both industrial and G2SAT datasets are used mainly as testing set in the dataset.This section describes augmented dataset setup that might affect the generalisation ability of GNN. CDCL-based SAT produce conflict clauses during searching and add learned clauses, which are reverse of conflict clauses, to the original problems. Prior work [44] has shown that training on augmented SAT problems with the learned clauses added could lead to better accuracy on augmented SAT domains than training on raw problems. Since this might be caused by the destroying of structure during the addition of learned clauses [5] , we are interested in an empirical analysis on the structural difference and their effect on out-of-distribution generalisation in this work. Thus, we gather learned clauses from produced DRAT-trim proofs [60] after running problems with the CadiCal solver [21] , then augment our dataset with the collected learned clauses.We also propose a novel splitting method for StructureSAT and focus on 3 types of generalisation tasks. After generating the raw datasets, instead of randomly splitting them to train/valid/test sets, we divide each raw datasets based on specific structural values. Specifically, for each domain, we select the average value Z from every calculated graph-based properties, as shown in Table 3 , and To test the generalisation GNNs, we focus on 3 aspects: in-domain larger problems, in-domain problems with different properties, and out-of-distribution problems. For all the synthetic generators, we follow the generation process described in Appendix B.2.1 and randomly generate problems with 10-40, 100-200, and 200-300 number of variables, each with 10k pairs. To test generalisation on uniform size problems with different structures, we are interested in random 3-SAT with different c/v ratios and different backdoor/graph properties evaluation on all domains. When calculating phase transition on random 3-SAT with 10-40 number of variables, the ratio value is roughly 4.7. To make the generation process easier, our generated test set has a c/v ratio of 3.5, 4, 5.5 and 6, as the further away from phase transition point, the harder it is to generate balanced dataset. For out-of-distribution problems, we randomly generate 10k problem testing data from each synthetic generators without property split, thus holding the structural range as in Fig. 2 , Fig. 3 and Fig. 4 . Small-size industrial and G2SAT problems are also selected as part of testing set.To get a comprehensive understanding of base dataset domains without splitting, we extend Fig. 2 and plot 6 other graph property distributions in Fig. 3 and Fig. 4 including α c , H, BE, P r , T w and c/v ratio. Since LCG is a bipartite graph, some calculations have been adjusted to accommodate its bipartite characteristics. For example, the clustering coefficient in P r has been modified to use the bipartite clustering coefficient calculation.The figures show a wide variety of distributions over graph properties among different domains. Some distinguishable differences can be seen within Q in Fig. 2 , where random, crafted, and industrial problems have low, medium, and high values, respectively. Additionally, industrial and crafted domains have a wider range of D f values than random domains. In Fig. 3 , the value range of B e ranks from lowest to highest in crafted, industrial, and random domains, while industrial problems have highest H values. For available P r values in Fig. 4 , the values from random domains 3-SAT and SR are close to 1, while the pseudo-industrial problems CA and PS have higher P r . All the distinct characteristics within the dataset highlight potential of affecting generalisation differently with GNNs.Despite being the first dataset to more deeply analyze SAT structure in terms of GNN generalisation, there are still a few limitations and many possibilities to consider for future work. Firstly, StructureSAT is separated into subsets, where each subset has one domain and focuses on one type of feature only. While useful for identifying individual factors of influence at a property level, a multivariate analysis of features and domains could be considered in future work. Secondly, due to certain problems being fundamentally intractable, we do not consider CNF based features like backdoor [37] . The structure calculations in Fig. 2 are limited to a 60 seconds timeout as most industrial and G2SAT generative processes are computationally hard to compute. Exploring effective algorithms of computing the structural properties on SAT, especially large problems, could be a potential future direction. Thirdly, although we include SATCOMP2007 in our dataset and calculate structural values of individual problems, the models we trained could not be efficiently tested on large industrial and G2SAT problems. Thus we only test on 24 G2SAT problems and 12 small industrial problems used to generate the G2SAT problems inside experiment. However, either better models or larger training sets could be included in future work for GNNs to solve large industrial problems. Lastly, as we only generated 100k pairs of data for each domain and divided inside the base dataset, there is overlap between different property split groups. Potential future work could be generating datasets with more controllable feature values as what CA generator do [24] .Models used in this work include NeuroSAT [53] , GCN [38] and GIN [61] .Our Dataset and Code base are available in StructureSAT1 . The link also include detailed instruction on downloading and running experiment with the dataset.Experiments with GNN are done using existing work from [44] . Experimental parameters include 1e -04 learning rate, 1e -08 weight decay and 32 number of message passing iterations. All the experiments are run on a machine with a NVIDIA A4500.StructureSAT is openly licensed via CC BY 4.0.This section details some additional experiments. In this section, for simplicity, we make SR stand for SR , R3 stand for Random-3-SAT, KCL stand for k-clique, KD stand for k-dominating-set, KV stand for k-vertex-cover, KCO stand for k-coloring, AM stand for automorphism, G2 stand for G2SAT, and IN stand for industrial problems. Note that for simple computation, we select 24 small problems from G2SAT. 12 industrial problems used to train G2SAT are used as industrial problems in this section. Different ratio generalisation. Table 5 shows the result of NeuroSAT trained on random 3-SAT and tested on a varying c/v ratio, through which we try to answer Q2. Surprisingly, although models are trained at the phase transition, which is the "hardest" point for random 3-SAT as discussed in Appendix B.1, testing at the phase transition point has the lowest accuracy. Furthermore, the further away c/v is from the phase transition point, the better their testing accuracy. This signals that GNNs are not always better at solving problems with similar properties to the training data.Out-of-domain generalisation Below are extended results for out-of-domain generalisation.Table 6 shows the result of GCN model trained on SR , splitted by 3 graph properties, while Table 8 shows the result of GIN model with same training set.Table 7 shows the result of NeuroSAT model trained on random 3-SAT problems splitted by 5 graph properties.Table 9 shows the result of NeuroSAT model trained on SR problems while predicting satisfying assignment. Comparison with Traditional Solver In the following section we compare the performance of traditional solver CDCL with one of the NeuroSAT models trained on SR(10-40) splitted on small α c , and show the results in Table 10 . The NeuroSAT model was tested with a batch size of 212 on the AM domain, 412 on KCL, and 512 on all other domains. Both the CDCL and NeuroSAT solvers were tested on the same machine to ensure consistency in comparisons. Regarding solving accuracy, for the tested datasets generated by random generators, the traditional CDCL solver achieved 100% accuracy, while NeuroSAT, trained on SR(n), reached approximately 50% accuracy on certain domains. In terms of solving time, NeuroSAT, with appropriately selected batch sizes, demonstrated the potential to solve problems faster than CDCL solvers on both random and crafted instances. Additionally, CDCL's solving time are generally similar, with variations occurring depending on the domain type (random vs. crafted), while the GNN solver's performance was more sensitive to the domains themselves. For instance, the CDCL solver exhibited similar solving times across random problems SR and R3, while solving times across combinatorial domains (KCL, KD, KV) were consistent yet distinct from random domains. In contrast, NeuroSAT solved R3 significantly faster than SR, despite both being categorized as random domains, which is likely due to differences in the size and complexity of the input graphs across domains. This also suggest the complete different solving Our dataset and codebase are available here.Our dataset and codebase are available here.https://drive.google.com/drive/folders/1ZrhRlRqQUTrYExVzVbXaocjvNIi2Os25?usp=sharing. 
 
 Appendix:  


Decision: All reviewers agree that this work provides an interesting benchmark for SAT solving with GNNs, and the topic would likely be of interest to the MATH-AI community.

Reviews: review: title: title: Official Review
main_review: main_review: The paper presents StructureSAT, which is a novel dataset that consists of SAT problems of various sources and types. One highlight of the paper is the investigation on the generalization capability of GNN solvers. However, the paper could benefit from more theoretical analysis and more extensive experiments (particularly, more GNN baselines and more state-of-the-art GNN variations that have better expressivity or generalization performance).
title: title: This paper introduces StructureSAT, a novel dataset for SAT solving with Graph Neural Networks (GNNs) that focuses on the relationship between structural properties and GNN generalization. The authors propose a structure-aware splitting method and conduct experiments to evaluate GNN performance across various problem domains and structural properties, aiming to bridge the gap between traditional SAT solving techniques and modern machine learning approaches.
main_review: main_review: This paper presents a novel and important contribution to the field of SAT solving with machine learning techniques. The introduction of StructureSAT and the insights gained from the generalization experiments are valuable to the research community. While there are areas for improvement, such as more detailed comparisons with traditional solvers and deeper error analysis, the overall quality and significance of the work merit acceptance. The paper opens up several interesting avenues for future research and has the potential to influence the development of more effective GNN-based SAT solvers.

### Quality:
##### Strengths:
- The paper addresses an important and timely topic in the intersection of SAT solving and machine learning.
- The methodology is sound and well-justified, incorporating both CNF-based and graph-based structural properties.
- The experimental design is comprehensive, covering various aspects of generalization.

##### Weaknesses:
- The paper lacks a detailed comparison with state-of-the-art CDCL solvers, which could provide more context for the GNN performance.

### Clarity of writing:
##### Strengths:
- The paper is generally well-structured and easy to follow.
- The authors clearly explain their motivation and approach.

##### Weaknesses:
- Some technical details, particularly in the description of structural properties, could be explained more clearly for readers less familiar with SAT solving terminology.

### Originality of the paper:
##### Strengths:
- The focus on structural properties and their impact on GNN generalization is novel and potentially impactful.
- The structure-aware splitting method is an innovative approach to dataset creation.

##### Weaknesses:
- While the combination of ideas is novel, many of the individual components (GNNs for SAT, structural analysis of SAT problems) have been explored separately in previous work.

### Significance of this work:
##### Strengths:
- The introduction of StructureSAT as a large-scale, diverse dataset is a significant contribution to the field)
- The insights gained from the generalization experiments could influence future development of GNN-based SAT solvers.

##### Weaknesses:
- The paper could elaborate more on the practical implications of the findings for real-world SAT solving applications.
title: title: Structure Based Dataset on SAT Solving with Graph Neural Networks
main_review: main_review: **Summary**: This paper introduces StructureSAT, a dataset of SAT problems, along with code to generate SAT problems. It also presents a method for splitting the dataset into more detailed hierarchies based on structural properties. The authors conduct various experiments to evaluate the generalization capabilities of different GNN solvers using this dataset. The results showcase existing challenges and suggest potential future directions for enhancing generalization performance.

**Pros**: The paper provides a novel perspective on improving GNN-based SAT solvers. The dataset is well-designed and covers various domains, and the authors conduct a sufficient number of experiments. Additionally, the writing is clear and well-structured.

**Cons**: The paper may be vague for those outside the field and could benefit from providing more detailed explanations.
title: title: A Good Benchmark for Evaluating the Impact of Structural Properties on GNN-based SAT Solvers
main_review: main_review: This paper introduces StructureSAT, a large benchmark designed to evaluate the generalization capabilities of GNN-based SAT solvers across various structural properties of SAT instances. The comprehensive experiments demonstrate that different structural properties can influence the generalization ability of GNN-based SAT solvers to some extent.

While I find the exploration of structural properties in SAT instances intriguing and commend the efforts in dataset construction and evaluation, the paper's focus is primarily on empirical performance evaluation. However, it appears challenging to derive a unified conclusion about how GNN-based SAT solvers perform consistently across instances with large or small values of these properties. Additionally, it remains unclear how these insights can be leveraged to enhance or optimize the performance of GNN-based solvers when encountering specific ranges of these structural properties.