HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation
Authors: Joseph Cotnareanu
Zhanguang Zhang
Hui-Ling Zhen
Yingxue Zhang
Mark Coates
Venue: NeurIPS 2024 poster (2024)
Keywords: Graph Learning
Boolean Satisfiability
Circuit Design
Primary area: graph_neural_networks
TL;DR: We leverage intrinsic properties of SAT problems and GNNs to efficiently generate new SAT problems for data augmentation in Deep Learning settings.

Abstract: Efficiently determining the satisfiability of a boolean equation --- known as the SAT problem for brevity --- is crucial in various industrial problems.  Recently, the advent of deep learning methods has introduced significant potential for enhancing SAT solving. However, a major barrier to the advancement of this field has been the scarcity of large, realistic datasets.  The majority of current public datasets are either randomly generated or extremely limited, containing only a few examples from unrelated problem families. These datasets are inadequate for meaningful training of deep learning methods.  In light of this, researchers have started exploring generative techniques to create data that more accurately reflect SAT problems encountered in practical situations. These methods have so far suffered from either the inability to produce challenging SAT problems or time-scalability obstacles.  In this paper we address both by identifying and manipulating the key contributors to a problem's ``hardness'', known as cores. Although some previous work has addressed cores, the time costs are unacceptably high due to the expense of traditional heuristic core detection techniques. We introduce a fast core detection procedure that uses a graph neural network. Our empirical results demonstrate that we can efficiently generate problems that remain hard to solve and retain key attributes of the original example problems. We show via experiment that the generated synthetic SAT problems can be used in a data augmentation setting to provide improved prediction of solver runtimes.

HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation
Joseph Cotnareanu 1,,,3, Zhanguang Zhang 4 Hui-Ling Zhen
Yingxue Zhang' Mark Coates
McGill University" International Laboratory on Learning Systems (ILLS)?
Mila Québec Institute Huawei Noah's Ark Lah" joseph. cotnareanu@nail. wtw.mmmmmmmmmmm.mmmmmmmmmml.mmmm ca, mark. coates@mcgill ca, (zhanguang- zhang, zhenhuil ing2, yingxue zhang) com
Abstract
Efficiently determining the satisfiability of boolean equation known the SAT problem for brevity - is crucial in various industrial problems. Recently, the advent of deep learning methods has introduced significant potential for enhancing SAT solving. However, a major barrier to the advancement of this field has been the scarcity of large, realistic datasets. The majority of current public datasets are either randomly generated or extremely limited, containing only a few examples from unrelated problem families. These datasets are inadequate for meaningful training of deep learning methods. In light of this, researchers have started exploring generative techniques to create data that more accurately reflect SAT problems encountered in practical situations. These methods have so far suffered from either the inability to produce challenging SAT problems or sane-scllabiltty obstacles. this paper we address both by identifying and manipulating the key contributors to a problem's 's "hardness", known as cores. Although some previous work has addressed cores, the time costs are unacceptably high due to the expense of traditional heuristic core detection techniques. We introduce a fast core detection procedure that uses a graph neural network. Our empirical results demonstrate that we can efficiently generate problems that remain hard to solve and retain key attributes of the original example problems. We show via experiment that the generated synthetic SAT problems can be used in a data augmentation setting to provide improved prediction of solver runtimes
Introduction
The boolean satisfiability problem (the SAT problem) emerges in multiple industrial settings such circuit design (Goldberg al. 200T), cryptoanalysis (Ramamoorthy and Jayagowri, 2023). and scheduling (Habiby et 20.1) While machine learning is not well suited for solving SAT problems solvers are typically required to have perfect accuracy and return correct proofs it does have applications in predicting wall-clock solving time for a given solver, which is important for algorithm selection (Kadioglu et al. 2010 KhudaBukhsh et al. 2009) and benchmarking (Fuchs et al. 2023).
SAT has also been gaining attention in Lange-Language-aee Model reasoning, as it is natural tool for interacting with the propositionalllogee
structure of many reasoning problems (Ye et al. 2023).
A major challenge for SAT-related learning is the scarcity of high quality, reasonably homogeneous, real-structured data. The most commonly-used datasets have been compiled via series of annual
We acknowledge the support of the Natural Sciences and Engincering Research Council of Canada (NSERC). Nous remercions le Conseil de recherches en sciences naturelles et génie du Canada (CRSNG) de son soutien. We make our code publically available at https: h/gg: /htpttttttugu/..///g///ggg/... com/ wttpaaa...oooooooooooooaoooooooo htt.apppppooooaaaaaaaaaaaarraaaa
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

International SAT Competitions. The industrial origins of the compiled instances differ substantially. so the dataset highly heterogeneous. The data is a good test for heuristic SAT solvers but for data-driven learning methods, this heterogeneous, sparse data is unsuitable. More complex models are thus forced to use randomly generated data (Selsam and Bjørner 2019). This is problematic because the hardness-inducing dynamics in industrial data are very different from those in randomly generated problems. Training or testing on most existing randomly generated data provides little insight into how a model will perform on real industrial problems (Balyo et al. 2022).
Recently, deep-learning methods have been in- troduced to generate more realistic SAT in- stances. Early models (Wu and Ramanujan 2019;|Yor et al.] 2019 Garzón et 20,2) can generate instances that are structurally similar to original instances, but the problems are con- siderably easier to solve, a phenomenon called hardness collapse. Preserving hardness is es- sential, as generating only very easy problems renders the resultant dataset ineffective for dis- tinguishing the best- rest-performing solver from the worst. Additionally, such datasets fail to help the model learn to predict real runtimes. A recent study has succeeded in preserving hardness (Li ett al. 2023). Unfortunately, the resultant method is prohibitively computationally expensive for synthetic data generation and augmentation for deep-learning. It can take
Cone-Costt Per Instance
HardSATGEN
hour
minute
G2MILP W2SAT
HardCore
second
easy (0%)
original (100%) hard (200%)
Instance Hardness (% original)
Figure Our method (HardCore) achieves the best trade-off of inference cost and SAT-problen hardness.
week to generate limited number of new problem instances. We summarize the cost/hardness trade-offs in Figure |
In this work, we take advantage of the connection between problem's core and its hardness. The core is comprised of the identifiable minimal subsets a boolean SAT problem that are unsatisfiable (UNSAT). Our strategy is to preserve the core of an original instance while iteratively adding random clauses to construct similar, but sufficiently diverse, problem instances that can enhance learning. To do this, need to detect the core after each iteration. Unfortunately, traditional core detection algorithms are slow and can take hundreds of seconds, as they often require to solve the SAT problem (Wetzler al. 2014). Clearly, such algorithm is impractical for building fast generator, as core detection needs to be performed hundreds of times for every instance we generate.
To address this, we rephrase core detection binary node classification algorithm (core/not-core). We train a graph neural network to perform the task. Importantly, we can circumvent the data starvation issue, because our random data generation procedure generates hundreds of example instances that can be used for training the core detection algorithm. We can also take advantage of the fact that while it is important to identify the vast majority of clauses that belong the core, can tolerate a relatively high number of false-alarms by post post-processing with a fast pruning algorithm.
We make the following novel research contributions:
We propose a novel method for SAT generation that the first that can both (i) preserve hardness and (ii) generate instances in reasonable time frame. We can thus generate thousands of hard instances to augment a dataset in minutes or hours.
We demonstrate experimentally that our proposed procedure preserves the key aspects of the original instances that impact solver runtimes. This hardness preservation is crucial when augmented dataset is used to learn to predict solver times, a vital task for solver benchmarking and selection.
We illustrate the value of our augmentation process for solver runtime prediction. On an example dataset, our augmentation process reduces mean absolute error by 20-50 percent. In contrast, all other generation algorithms achieve no statistically significant improvement.
2 Background: Boolean Satisfiability
The Boolean Satisfiability Problem (SAT) is the problem of determining whether there exists an assignment of variable values that satisfies the given Boolean formula, rendering it true. Typically, SAT instance is represented in Conjunctive Normal Form (CNF), which is written conjunction (logical AND) of disjunctions (logical OR), for example
Definitions and Notation

---

C). The signed version of each variable that appears in the formula known as a literal. For example, A and ーA are both literals of the variable A (Biere et al.)
V
2009
Chapter 2).
Another useful representation of CNF is as of sets, where each set (referred to clause) represents a disjunction in the CNF and contains the literals included in that disjunction. Denote the i-th clause in the formula f by ej and the j-th literal in clause C₁ as (j. If there are ne clauses in f and ny, literals in clause C₁ we can express the formula as G = - i 4. ʃ - G3-
Core Definition Given unsatisfiable (UNSAT) instance U, there is a subset of clauses called a Minimally Unsatisfiable Subset (MUS) or a Core. This subset the smallest possible subset of clauses from U that is UNSAT (Birre et al. 2009. Chapter 11).
Graph Representation of CNFs There are several common CNF graph representations. In this work, we use the Literal-Claus Graph (LCG), an undirected and bipartite graph. Each node in the first set of nodes represents clause and each node in the second represents literal. We construct an edge for each occurrence of literal in clause; the set of undirected edges is defined as Th M
i= j=0 9.).
3 Related Work
3.1 Deep-learned SAT generation
The problem of learned generation for SAT problems was first established 2019 with SATGEN (Wu and Ramanujan 2019), motivated by lack of access to industrial SAT problems. SATGEN used a graph generative adversarial network (GAN) to generate graph representations of SAT problems.
G2SAT You et al. 2019) represents problems as graphs. The graphs are progressively split into small trees, and a graph neural network (GNN) is trained discern which trees should be merged to restore the original graph. While innovative, the method is slow due to its need to sample many tree pairs to form SAT problem of sufficient size. The most recent improvement on the G2SAT framework, HardSATGEN (Li et al. (023), includes some domain-inspiree
considerations in its design, such as communities and cores. HardS ATGEN the first deep-learned SAT generation method that can generate problems which are not trivial to solve for solvers: often the generated problems take nearly as long or even longer for solver to solve than the corresponding seed problem. Unfortunately. however, the core awareness aspects of the design cause HardS to be extremely slow, making it challenging to use in any setting that needs many new instances.
W2SAT Wen and Yu, 2023) follows an approach more similar to the original SATGEN. It employs a low-cost general graph generation model, and obtains new SAT problems via graph decoding. W2SAT is extremely efficient, but like G2SAT, it is incapable of generating hard problems. G2MILP (Geng et al.) 2023). designed to generate Mixed Integer Linear Programs (MILPs), which are the general case of SAT. A naive modification allows to use G2MILP to generate SAT problems. The method is nearly as efficient as W2SAT, but also struggles to generate hard instances.
3.2 Core Prediction
Core Detection can be helpful tool for understanding UNSAT problems. Cores are often seen as strong indicator of the hardness of an UNSAT problem (Ansótegui et al.) 2008). There are multiple classical, verifiable methods for Core Detection, with the current standard being Drat-Trim (Wetzler et al. 2014). Drat-trim requires that the problem be solved once by SAT solver, which is very slow. In response to this, Neurocore (Selsam and Björner 2019) was designed to predict the core of SAT problem. Neurocore converts the input problem to graph and uses a GNN to predict cores. Strangely, however, Neurocore does this on variables rather than clauses. Cores are defined to be subsets of clauses, rather than variables, and so this choice seems unnatural. Neurocore strives to be machine-leaming based pariable-selection heuristic for SAT solvers, which motivates the focus on variables.
3

---

Clauses
Core Prediction GNNs
Variables
BB
1st Iteration
Core Clauses
Easy Input
Repeat
Added Variable
De-Coring
Stop?
Yes
Hard Output
Figure 2: Core Refinement. The core refinement process comes in two steps: (I) Core Prediction,
in which we use GNN-based architecture to identify the core of the generated instance; and (2)
De-Coring, in which add a non-conflicted literal to clause in the core, rendering the satisfiable and giving rise to new, harder minimal unsatisfiable subset (core). As steps (1) and (2)
are repeated, the easiest core of the problem gradually refined, raising the hardness the generated instances.
Problem Statement
Given training set of UNSAT CNFs S {fi, f2... fms and corresponding of label vectors R (ri, r2, Fmg }. we wish to train generative model G that can construct new examples. The label vector r E Rd represents the hardness of the SAT problem and we model it as a deterministic mapping, i.e., time for a ppe-siecif set of SAT solvers.
g(fi.. In experiments, the vector is derived by recording the SAT solving
We assume that the m, CNFs in the training set are i.i.d. examples from an underlying distribution D. We denote the generative model distribution by (S).). highlighting that is dependent on the random training set S. We can obtain new dataset of mg i.i.d. samples So using the generative model. The total number of samples in the augmented set $ is then ms + mg.
Our primary goal is to derive generative procedure that produces sufficiently representative but also diverse samples such that the error obtained by training model the augmented dataset Š is less than that obtained by training on the original dataset S. As an example task, we consider the prediction of runtime for candidate solver. In this case, the appropriate loss function is the absolute егror between the predicted time and the true time.
Beyond this, we are also interested in the distance between the distributions D and Dg. We examine this through the lens hardness label vectors. The application of g to the CNF descriptors generated according to D or De induces distributions in Rd To evaluate the similarity of the original and generated instances, we calculate the empirical maximum mean discrepancy (MMD) distance between these induced distributions.
5 Methodology
Our generation strategy can be broken into three steps: (1) extraction of the core from seed instance;
(2) addition of random new clauses, generated with low cost; and (3) iterative core refinement. Figure 2 provides overview of the key core refinement procedure. It consists of a two-step cycle of (a) high-speed core extraction using our novel GNN-based method; and (b) unconflicted literal addition to break any undesirably easy core.
5.1 Generating Hard Instances
Trivial Cores Cores are the primary underlying hardness providers in UNSAT instances, because solver must only determine that subset of CNF is UNSAT for the whole CNF to be UNSAT, and

---

core is the smallest subset of clauses of a CNF that is UNSAT. Small cores with few clauses are generally easier to solve due to less variable assignment combinations. An example of a trivial core is (AV B)A (-A A - (-AV BB).
Whenever add a new random clause trivial core. For example, consider an UNSAT instance which includes three of the clauses from the example above: (A V B)A (-AV B)Λ (A -B). If during generation we unknowingly add the clause (-A V -BB,, the UNSAT instance's 's large (hard) core will be replaced by a trivial one, leading to hardness collapse. Maintaining awareness of cores and potential cores in a CNF as we perform modifications is challenging. We take different approach, which we refer to as Core Refinement.
UNSAT instance, there is the danger of creating
Core Refinement The Core Refinement pro- cess is made up of two steps that are repeated n times, where n is the number of generated clauses. The procedure is depicted in Figure 2 The first step of the process is to identify the core of the generated instance. The addition of random clauses during generation is very likely create core that is trivially easy solve and it may not be the same as the core of the original instance. Once
Predicted Core Clauses
0.7
0.9
0.4
0.2
0.4
0.8
Loss
a
True Core
Labels
FC
have detected this easy core, we make it satisfiable by adding a new literal to clause in the core. The addition of single, flexible literal eliminates the constraints of the core and makes it possible satisfy.
GNN en hn) GN N(c etc. Ht) GN N ev h²)
Returning to the previous example, the UN- SAT CNF (A V B)А (-AV B)A (A -B)A (-AV-B) can be made satisfiable by modifying any of the clauses in this fashion: (Av B A (-A v A (A V BB) (-A BB). The in- troduction of literal C in the first clause means that (A = 0, B = 0, C 1) is now a satisfying solution.
3 Layers
LCG Input
B
As these two steps are repeated, the core of the instance gradually becomes larger and is likely to be more difficult. The process ends after a fixed number of iterations. In our experiments, we choose this to be the number of generated clauses. Since the hardness of the core is the hardness the instance (Ansótegui et al. (2088) the refinement process can be seen progres- sively raising the hardness of the problem.
Figure Core Prediction GNN Architecture We construct our GNN using three parallel mes- sage passing neural networks (MPNN) whose cal- culated node embeddings are aggregated at each layer to form the layer's 's node embeddings. Read- out is done by taking the sigmoid of fully- connected layer on clause node embeddings and thresholding. Training is supervised by taking bi- nary classification loss between the true core labels and the clause nodes' core prediction probabilities.
Underlying Hard Core Guarantee The Core Refinement process is designed to repeatedly eliminate easy cores, so after each iteration, the core becomes harder. Finally, after many iterations, we hope that the remaining core is as hard as the original instance. This process can only be guaranteed to lead to a hard core if an underlying hard core exists in the instance at the start of the refinement process. Refinement then whittles away easy cores until only the hard one remains.
There a possibility of creating hard core through the random generation of clauses, but we cannot rely on this. We must introduce an element to our design to ensure there is a hard core. To achieve this we identify cores from the original instances and include them in the generated instances.
5.2 Core Prediction
We have two critical objectives for our method: low cost and hard outputs. While the Core Refinement process serves us well in generating hard instances, naive implementation using existing core detection algorithms is unacceptably expensive in terms of computation requirements. Current core
5

---

detection algorithms first solve the SAT problem, making Core Detection NP-Complete (Wezzler al.
2
We adopt the strategy of approximating the Core Detection algorithm. Since an instance can be naturally represented using bipartite graph, and the goal of core detection is binary classification of each clause, we expect that a graph neural network is a promising approach.
Graph Construction We represent each instance as a graph as outlined in Section We make two changes: (a) we add pressage-passing edges to connect matching positive and negative literals (e.g, -A and A): (b) we replace each undirected edge with two directed edges. These changes are designed to facilitate the diffusion of information in the GNN. We denote the set of literal-literal message passing edges by En Ul (4++,, 4-), where nye is the number of variables in the instance.
Mlay We denote the set of literal-tocclasee directed edges by E U Ur=ō (4),, Cz). We denote the set of Hause-to-literal directed edges by Edt U U (c,, (,.
GNN Architecture Given the heterogeneous nature of our graph, arising from different node and edge types, we use three Graph Message Passing models (one for each edge type), as described in Figure 3 We couple these models by averaging their embeddings after each layer. We define a single layer where each clause node by passing the embeddings through fully connected linear readout layer followed by a sigmoid function to the clause node embeddings. We threshold the values to obtain positive and negative classifications of core membership:
a non-lnnne mon-linear activation function. Finally, we obtain core membership probability for
1 (GNNNV,E.. + GNN(V, &,,(VVE,, h = of oul 100.5(0(xh + b)).
(1)
Training Our augmentation process is motivated by a scarcity of data. We must therefore address this when training the core detection GNN. We achieve augmentation of the available data by executing the generation pipeline described above for a small number of instances, using a slow, traditional but proof-pro providdovi tool for Core Detection in the Core Refinement process. By saving the instance-core pair after each iteration of the core refinement process, we can construct sufficient supervision data for training the Core Prediction GNN model. Although the instance-core pairs construct this way are correlated, there is sufficient variability for the GNN model to generalize well to other instances. We train the model using the standard binary cross-entropy loss function. For experimental results showing the performance of our Core Prediction model, see row titled "LEC" in Table in the Appendix B
Experiments and Results
6.1 Experimental Setting
Proprietary Circuit Data (LEC Internal) This LEC Internal data is a set of UNSAT instances which are created and solved during the Logic Equivalence Checking (LEC) step of circuit design. LEC needs to be performed after certain circuit optimization steps to ensure that the optimization process has not corrupted the logic of the circuit. If the logic is uncorrupted, the created SAT problem will be UNSAT. Since it is extremely rare that these optimizations in fact corrupt the circuit, more than 99% of LBC instances are UNSAT. For each generative method, we will generate problems for each problem in the data.
Synthetic Data (K-SAT Random) Acknowledging the importance of reproducibility, we also provide results on synthetic data. This data is generated by randomly sampling a CNF with m clauses of & literals over variables. Clauses are sampled without replacement. We have previously argued that random data differs from real data in important ways that make it unsuitable for machine learning applied to real problems. Holding to this view, we use this data primarily to provide a surrogate to the internal data for experimental reproduction purposes, rather than to present results a second dataset. For each generative method, we will generate problems for each problem in the data. For details concerning both the LEC Internal and K-SAT data, see Table 3 in the Appendix.

---

Note on Public Competition Data A large and commonly public dataset for SAT is the SAT Competition data (Heule et al., 2019). Unfortunately, argued previously, this data is generally ill-positioned for machine learning as it is highly heterogeneous, Despite this, we recognize its value and importance as a widely accepted dataset. Thus, we include in Tables [f and final results on the Data Augmentation experiment done below, done on the "Teeitin" and "FDMUS" families found in the public competition data. Our method shows improvement on the un-augmented data consistent with our findings on the synthetic and proprietary data prosented in this section.
Appendix B
Data splits for training the HardCore GNN and the runtime-prediction model There are three separate groupings of the dataset: (i) Core Prediction training data, (ii) generation seeding data, and (iii) the remaining data. This split is chosen randomly. Core Prediction training data can be small (we used 15 problems), because we use each problem as a seed instance 5 times for generation followed by core-refinement with a traditional core detector. Saving problem-core pairs at each step, we obtain 15,000 training pairs for the core-predictor model. The seeding data are used seed HardCore once the core predictor is trained in order to obtain generations to evaluate. These generations are then compared against the seed data for runtime similarity. Finally, these generations (and their seeds) are used to train a runtime-
runtime-predictor predictor model, which is evaluated on the remaining un-used data.
SAT Solvers We select 7 solvers for hardness analysis: Kissat3 (Birre et al. 2020), Bulky (Fleury and Biere 2022). UCB (Cherif al., 2022). ESA (Cherif et al. 2022), MABGB (Cherif et al. 2022), moss (Cherif et al. 2022) and hywalk (Chowdhury) 2023). These solvers exhibit complementary performance characteristics: when some of these solvers perform well certain instances, some perform very poorly. This results a diverse runtime distributions our analysis. We run our experiments a Intel(R) Xeon(R) Platinum 8276 CPU @ 2.20GHz epu and 3 Nvidia Tesla V100 GPUs.
We compare to the following baselines:
high-cost split-merge generator with community structure and core detection that is capable of generating hard instances.
HardSATGEN (Li et al. 2023):
W2SAT (Wen and Yu, 2023); ; A low-cost generative method that utilizes less common SAT
graph representation which was reported to generate very easy problems.
G2MILP (Geng et al. 2023): A low-cost VAE-based generative model designed for the general case of SAT: MILPs
6.2 Research Questions
Our work is motivated by the goal of fast generation of hard and realistic UNSAT datasets for data augmentation. Given these goals, we now establish our strategy for evaluating our model, identifying the key research questions that our experiments explore.
6.2.1 Question Is the method able generate hard instances?
In order to quantify 'hardness', we choose the wall-clock solving time for each solver as a metric. We deem set of generated instances 'hard' if the average solver runtime is at minimum 80% of the original dataset's average hardness. If average solver time for the set of generated instances is below 5%, we consider that hardness collapse has occurred.
In T we compare generated with original hardness. W2SAT and G2MILP both suffer hardness collapse, whereas HardSATGEN and HardCore generate hard instances.
6.2.2 Question Is the method fast?
We measure generation speed by the time required to generate an instance (in seconds). We evaluate this by measuring the wall-clock time of each model during inference and dividing by the number of generated instances. Generally, a method should be able to generate hundreds of instances per hour so that augment dataset in reasonable time frame.
In Table T the division between fast and slow procedures is very clear: W2SAT, G2MILP, and HardCore all exhibit similar instance generation times, with W2SAT being the fastest. In contrast,
7

---

Table Evaluation generated datasets on LEC data. Hardness level (%): percentage of runtime of generated dataset relative to original dataset, closer to 100% is better. Speed (s): average time cost to generate one instance, lower is better. Maximum Mean Diserepancy (MMD): distance between distributions of generated and original datasets, lower is better.
W2SAT
HardSATGEN
G2MILP
HardCore
Hardness (%)
~0
267
~
176
Time per instance (8)
1.2
6441
3.3
4.3
Similarity (MMD)
0.492
0.004
LEC Original (Green) and HardCore (Blue) runtimes
LEC Original (Green) and HardCore (Blue) runtimes
1500
1500
1250
Runtima in Seconds
Runtime In Seconds
1000
1000
750
750
500
500
250
250
2
6
2
Solver id
Salver id
Figure 4: HardCore (Left) and HardSATGEN (Right). Boxplots of runtimes per solver for Original (Green) and Generated (Blue) instances on LEC data. HardCore appears to produce per-solver distributions which are much closer to the original than HardSATGEN which tends to produce high-variance and on-average much harder problems than the original.
HardSATGEN takes close to 2 hours to generate a single instance. To generate 1000 LEC instances this speed we would need 75 days.
6.2.3 Question Is the method able generate datasets that are similar the original datasets in terms of bardness distribution?
Although past work such as Li et al. (2023); Wen and Yu (2023: ): You et al. (2019) has examined graph statistics such modularity and clustering coefficients, we find little evidence that these are indicative of the hardness of generated instances. Instead, we focus on the similarity of the distributions of the hardness vectors because hardness is of primary importance when working with SAT problems.
LEC Internal HardCore Original Rank Solvers
LEC Internal HardSATGEN Original Rank Solvers
Original
Oriqinal
0.4
HardCCoe
0.4
HardSATGEN
0.3
0.3
0.2
0.2
6
2
3
Figure 5: LEC Internal Rank Solvers. We compare original and synthetic best-solver observations for HardCore (left) and HardSATGEN (right).

---

As G2MILP and W2SAT exhibit hardness collapse, we only compare HardSATGEN and HardCore for runtime distribution analysis. Note that due HardSATGEN's s high cost, we can only generate 50 LEC instances and 50 K-SAT instances within 3 days. In the following experiments, we compare "original" and "generated" data. Here, "original" refers to only those instances used as seeds during inference for each model; "generated" refers to the outputs. Hence, the "original" sets for HardSATGEN and HardCore are different because the number of seed instances is different (due to time constraints we are limited in how many HardSATGIR instances we can generate). We evaluate the similarity between original and generated data through the Maximum Mean Discrepancy (MMD) metric, the runtime distribution, and the best solver distribution.
As shown in Table I HardCore achieves runtime distributions far closer to the original distributions compared to HardSATGEN with respect to the MMD metrie. We calculate these values by taking the MMD between the set of instances used as seeds during generation (a subset of the training set) and the corresponding set of generated instances. We note that while HardCore achieves low MMD, the solving time of individual instances is considerably different from that of their associated seeds. This implies that low MMD of HardCore is not achieved by replicating or barely modifying seed instances. Our later experiments investigating augmentation suggest that there is sufficient diversity being injected in the generated instances.
In Figure we visually compare the per-solver runtime distribution of HardCore's s generated datasets to the corresponding original datasets. HardCore produces per-solver distributions which are visibly much closer to the original distributions than HardSATGEN. In Figure we see striking similarity between the HardCore distribution of best-performing solvers and the original distribution, indicating that the HardCore synthetic instances are solved most efficiently by the same solvers as the original instances, in a distributional sense. Meanwhile, greater discrepancy can be seen between original and -egnertee data, particularly for solvers and 6. A full histogram of LEC solver ranks is shown in Figure of Appendix B
6.2.4 Question 4: Can we successfully augment training data with the method's generated data for machine learning?
We address the task of runtime prediction and compare the performance of two models: one trained on only original data and the other trained on a dataset augmented with generated instances. We train the SATzilla model to predict solver runtime of one specific solver on a given instance. We repeat this for each of the solvers. We calculate the MAE of the predicted total runtime for each solver and average over the solvers. We compare HardCore, W2SAT and two versions of ATGEN: (i) HTrdSATGEN -Strictttttttteae and (ii) HardSATGEN-A many instances as possible in the time it takes HardCore to generate the desired number of instances. For HardSATGENT ATGEN-N, we generated N instances, where N was selected as the number that could be generated in approximately 3 days of computation. We also compare to the un-augmented training sets and refer to it as Original.
For HardSATGEN-Stricn we only generate as
In order to observe performance over varying sizes of training data, we conduct this experiment for several quantities of original training instances, which is denoted Data Size. Three augmentation instances are generated per original instance, and augmentation is only allowed by using the original instances in the training set. Validation sets are selected from the original data only, with an 80/20 split train/validation split. For LEC the test-set is made up of 10000 randomly selected problems which were not selected for training or validation. For K-SAT the test-set is made up of the problems which were not picked for train/validation from the 1351 original instances.
Table 2 shows that for both K-SAT random data and LEC Internal dataset, training on data augmented using HardCore leads to a 20-50 percent reduction in MAE. The gain of data augmentation increases with larger data size. In contrast, no other data generation method leads to comparable improvement.
6.3 GNN generalization to other datasets: do we have to re-train for new unseen circuits?
In order to measure GNN generalization to new data without re-training, we create a new split of the LEC data. Each problem in the LEC data can be traced back to one of 29 circuits. By randomly splitting circuits into training circuits and test circuits (and then building training and evaluation sets with their respective problems), we measure generalizability, Note that we would not expect the

---

Table MAE of Runtime Prediction averaged across solvers and 15 trials. Asterisks are placed at the best result which passes the Wilcoxon pairwise ranking test against the second-best for < 0.05. For boxplot visualization showing each trials result, see Appendix Figure] 7
K-SAT Random
LEC Internal
Data Size
10
20
30
40
100
200
300
400
500
HardSATGEN-J
2416
2306
2172
2182
666
797
605
617
463
HardSATGEN-SOn
2179
2578
2488
2456
627
742
565
638
513
W2SAT
2606
2046
1807
1377
724
704
634
611
535
Original
2750
2743
2109
1449
707
795
557
606
526
HardCore
2156
1796*
1615
930
514
481
369
282*
338
model to generalize to problems derived from completely different application domain (although fine-tuning a previously model in a domain adaptation strategy might be interesting to explore).
In row titled "Circuit-Split LEC" in Table44o Appendix B we report the GNN performance on this
experiment. In the paper we discussed that Core recovery the priority, because we falsely classify true true-positives then we may be unable to de-core the current core (since the necessary clause may be undetected, whereas if we mis-classify true-negatives then we will simply de-core non-core clause. Given enough iterations of core-refinement de-coring (since the clause for de-coring is randomly selected from among the detected clauses). With this in mind, the threshold byper-parameed becomes useful parameter in cases where classification performance is weakened: we can boost Core Recovery (recall) by lowering the threshold. Tuning this threshold is very low-cost: testing thousand problems takes 500 seconds on a GPU. We find that by testing values [0.1, 0.3, 0.5, 0.7, 0.9) which takes 25 minutes can tune the threshold to provide similar recall to the in-distribution model.
true-positvve clause will eventually be selected for
which is used on the sigmoid outputs at model readout
7 Limitations
The primary limitation of our work is that it is restricted UNSAT problems. While some SAT applications are almost entirely UNSAT (c.g., circuit design), many are not. With our proposed approach, this limitation is unavoidable because cores only present in UNSAT problems. However, there is a concept for SAT problems analogous to the core, known as a backbone. Focusing on preserving the backbone potential avenue for analogous method for satisfiable SAT problems.
Another limitation that our work relies solely upon empirical results to demonstrate its efficacy, and these results are only presented on two datasets, one of which is synthetic. To partially address this concern, we conducted several trials and statistical significance testing to ensure the reliability of our empirical analysis.
Another limitation is that our method struggles scale extremely large SAT problems. As the size of the SAT problem increases, memory and computation costs scale in polynomial complexity, meaning that SAT problems which have millions of clauses are currently out of reach for this method. For more in-depth discussion of scaling, please see the Scaling subsection A.3 3 in Appendix
8 Conclusion
We present fast method for generating UNSAT problems that preserves hardness. Existing deep- learned SAT generation algorithms either (1) are incapable of generating problems that are even 5% as hard as the example input problems; or (2) can generate hard problems but take many hours for each instance. Our proposed method targets the core of SAT problem and iteratively performs refinement using GNN-based core detection procedure, Our experiments demonstrate that method generates instances with similar solver runtime distribution as the original instances. For more challenging industrial dataset, we show that data augmentation using our proposed technique leads to significant reduction in runtime prediction error.
10

---

References
Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manya. 2008. Meauring the Hardness of SAT Instances. In Proc. AAAI Int. Conf. Artificial Intell.
Tomas Balyo, Marijn J.H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda (Eds.). 2022. Proc. of SAT Competition: Solver and Benchmark Descriptions.
Armin Biere. Katalin Fazekas, Mathias Fleury, and Maximillian Hessinger. 2020. Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition. SAT COMPETITION, 50.
Armin Biere, Marjin Heule, Hans von Maaren, and Toby Walsh, 2009. Handbook of Satisfiability. IOS Press.
Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. 2022. Kissat MAB: Upper Confidence Bound Strategies to Combine VSIDS and CHB. SAT COMPETITION, 14.
Md Solimul Chowdhury. 2023. kissat-hywalk gb, kissat-hywalk-exp. kissat-hywalk-exp-ae and malloblin Entering the SAT Competition. SAT COMPETITION 1428, 28.
Mathias Fleury and Armin Biere. 2022. GIMSATUL, ISASAT, KISSAT. SAT' COMPETITION, 10.
Tobias Fuchs, Jakob Bach, and Markus Iser. 2023. Active Learning for SAT Solver Benchmarking. In Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems. Springer, 407-425,
Iván Garzón, Pablo Mesejo, and Jesús Giráldez-Cru. 2022. On the Performance of Deep Generative Models of Realistic SAT Instances. In Proc. Inf. Conf. Theory and Applications of Satisfiability Testing (SAT 2022), Vol. 236. 3:1-3:19.
Zijie Geng, Xijun Li, Jie Wang, Xiao Li, Yongdong Zhang, and Feng Wu. 2023. A Deep Instance Generative Framework for MILP Solvers Under Limited Data Availability. In Proc. Adv. Neural Inf. Process. Syst.
Evguenii Goldberg, Mukul R. Prasad, and Robert King Brayton. 2001. Using SAT for combinational equivalence checking. In Proc. Conf. Design, Automation and Test in Europe.
Payam Habiby, Sebastian Huhn, and Rolf Drechsler. 2021. Optimization-based Test Scheduling for IEEE 1687 Multi-Power Domain Networks Using Boolean Satisfiability. In Proc. Int. Conf. Design & Technology of Integrated Systems in Nanoscale Era (DTIS). 1-4.
Marijn Heule, Matti Järvisalo, and Martin Suda. 2019. SAT Competition 2018. Journal Satisfiability Boolean Modeling and Computation 11, 133-154.
Serdar Kadioglu, Yuri Malitsky, Meinolf Sellmann, and Kevin Tiemney 2010. ISAC Instance-Speccffe Algorithm Configuration. In Proc European Conf. Artificial Intell. 751-756.
Ashiqur R. KhudaBukhsh, Lin Xu, Holger H. Hoos, and Kevin Leyton-Brown. Brown. 2009. SATenstein: Automatically Building Local Search SAT Solvers From Components. In Proc. Int. Joint Conf. Artificial Intell. 517-524.
Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, and Junchi Yan. 2023. HardS ATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure- Structure-Hardness--Ne Hardness-Aware Baseline. In Proc. of ACM SIGKDD Conf. Knowledge Discovery and Data Mining.
Athilinagam Ramamoorthy and P. Jayagowri. 2023. The ofate-of-the-ar Boolean Satisfiability based cryptanalysis. Materials Today: Proceedings 80 (2023), 2539-2545.
Daniel Selsam and Nikolaj Bjørner. 2019. Guiding Predictions. In Proc. Int Conf. Theory and Applications of Satisfiability Testing. 336-353.
SAT Solvers with Unsat-Core
Weihuang Wen and Tianshu Yu. 2023. W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs, arXiv23002.00272 [cs.LG]
11

---

Nathan Wetzler, Marijn J.H. Heule, and Warren A. Hunt. 2014. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. In Theory and Applications of Satisfiability Testing. Springer, 422-429.
Haoze Wu and Raghuram Ramanujan. 2019. Learning to generate industrial sat instances. In Proc. Int. Symp. Combinatorial Search, Vol. 10. 206-207.
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023, SatLM: Satisfiability-Aidee Language Models Using Declarative Prompting. arXiv:2305.0965 09666 [cs.CL]
Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovee. 2019. G2SAT: Learning Generate SAT Formulas. In Proc. Adv. Neural Inf. Process. Syst.
A Appendix
A.1 Data
Table Data Statistics. Note that LEC is much larger dataset than Tseitin in every regard: average variable and clause counts, average hardness on Kissat solver and dataset size.
var.
clause
runtimes (s)
count
LEC
1328
5167
388
78730
K-SAT
398
1751
2700
1351
A.2
Hyper-parameters
In our design process, given the cost of running experiments - in particular measuring runtime of generated instances we did not conduct exhaustive hyperparameter searches. Hyperparameters were set following design considerations and rationales, which will be discussed here.
The random generation method we use is Popularity-Similariy This has several syper-parameter:: average clause size, Be, B, and T. Average clause size determines the average number of literals per generated clause, Be and B, are constants in the probability distribution for clause and variable selection, respectively. and T is a constant the exponent of the probability of an edge existing between clause and variable. Conducting an cxhaustive search over these hyperparameters is expensive because the evaluation of each configuration is via runtime-measuremenn, which requires the solving of a large number of SAT problems by multiple solvers. We communicated with the authors of the paper which presented HardSATGEN, and were able to obtain their hyperparameter configuration for Popularity- -iimaiitt--iimliittyyy (PS), which was included among their reported baselines. For continuity with previous work and in the interest of reducing the computational budget, we used the provided configuration.
The GCN backbone within our core prediction module has two hyperparameters, namely the number of hidden dimensions and the number of layers. Three potential values were chosen for initial exploration of layer size: [3, 4, 15]. In many applications, GCN networks are configured to have only 3 4 layers. This is because GNN networks in general
prone to over-smoothing as the number of layers increases. 15 layers was added to validate this behavior within our context. For hidden dimension size chose potential values: [32, 64]. Our findings were that the model size increased via additional layers and hidden feature size, there was minimal improvement in performance. Thus, we selected the smallest defined configuration of layers and hidden dimension of 32.
Finally, there is the Core-Refinement hyperparameter that specifies the number of iterations. This value can be set in terms of the number of generated clauses, since one clause is modified at each iteration. The safest setting clauses, such that, if necessary, the method is allowed to modify every generated clause. In practice, this was the setting we used.
the number of iterations to equal the number of generated
A.3 Scaling
Memory limitations are the primary challenge for our proposed method, due to the need to store the graph. For our experimental hardware (32GB GPU) and our implementation of the graph
12

---

building/storage (0(mm) for problem with n clauses and m variables), problem with 256,000
variables and 1,000,000 clauses would require 256, 000 x 1, 000, 000 x 256 x 10 bits, or 32 gigabytes. Given a GPU with 32GB of memory, this would be a breaking point for the method. Of course, this the worst case, which only occurs for a completely dense graph representation. In practice, clauses in the LEC data, for example, tend to have on average 3 or 4 variables. Since in the LCG clause nodes are only connected to the variables of which they consist, each clause node would then only have degree of 3 or 4, meaning the graph is very sparse. Thus, in practice the primary memory cost of our model scales more so according to (dd), assuming average number of variables in clause is d, and assuming the implementation is adapted to leverage the sparse structure (using edge-lists lists instead of dense adjacency matrix, for example).
In cases where the problem is large and dense, another option might be the use of more specialized GNN methods that are specially designed to handle very large graphs. For example, by sampling from neighhourhoods or loading portions of the graph from storage.
For time-cost scaling, the primary point in the pipeline in which we suffer scaling challenges is during pre-processing. We build graphs from the text-file representation of the problems. The time-cost of this step linear with the problem size, measured in terms of the number of clauses. Given this, time-cost is not a major factor in the scaling issue.
We will add text to clarify the scalability considerations outlined above and specify the precise nature of an "extremely large" problem that would challenge our proposed generative model.
A.4 HardCore GNN Core Prediction Implementation Details
We implement HardCore in DGL using 3 Graph Convolutional Network layers combined into a hetero- GNN, where outputs of each layer are aggregated with a mean using the hererograph package in DGL. We train using 15 problems from the dataset, and we obtain training enf-core pairs using Drat-Trim in the Core Refinement step for 200 iterations per instance. We train for I epoch using Binary Cross Entropy loss.
A.5 K-SAT Random Generation Algorithm 1 Algorithm for generating I K-SAT Random instance.
N(mms m.)
c ~ N N Go) 4 int(me)
cnf < randkenf (3, m, n)
where randkenf(k, m, n) returns enf m with k-var clauses from n variables.
Algorithm T shows the process by which we generated K-SAT Random instances as discussed in Section 6.1 We randomly sample hyper-parameters (number of clauses, number of variables) from a small window in order to introduce some additional variety into the dataset, and generate by randomly sampling sets of 3 variables without replacement. In our work we chose N N4000, 100), c ~ N4.44, 0.05).
B
Supplementary Results
Figure 6 shows stacked histograms of the rankings for each solver, following up on the rank-1 histogram shown in Figure The top row allows us to compare the ranking distribution of original LEC instances and HardCore's generations. The bottom row allows us the same for ATGES Note that the original distributions are different for HTrESATGEN and HardCore because the methods were fed different quantities of data. Given ATGEN' cost, only 10 instances could be used for generation (to generate 50 instances), whereas HardCore is given 1445 instances and generates 5780. On inspection of the figure, we note the similarity of the original and HardCore ranking distributions. For example in HardCore, solver I's distribution of rankings shows a very similar proportion of rank ranks 2-6, with perhaps slightly higher rank (and lower rank 7) than original. In contrast, HTrNSATGEN shows very different distribution than the data it was given. For exmaple, we see density in rank for solvers 5 and where there was none in the original data given to HardSATGEN, Even comparing to the true original distribution of which the top- histogram is
13

---

100%
solver rankings LEC original
solver rankings for LEC generated data
80%
occurences
occurences
60%
40%
40%
20%
0%
3
5
7
salver
salver
100%
solver rankings for LEC original data
100%
solver rankings for LEC generated data
80%
80%
occurences
rank
60%
40%
20%
20%
0%
0%
salver
solver
Figure 6: HardCore (top) and HardSATGEN (bottom) Comparison of Solver Ranking Histograms for Original and Generated LEC data.
representative (HardCore was given enough data to be considered representative sample of the whole dataset), we start differences that solver has rank-1 density from HardSATGEN and that HardSATGEN seems to prefer solver 4 more frequently than whereas the Original data favors over 4 as rank-1 solver.
Table 4: GNN Core Prediction Performance
1 Core Recovery Ratio TP
ITP-PI 4 Core Size Discrepancy
fAccuracy TP4TN P4N
P+N
Circuit-Split LEC
0.97
0.05
0.65
LEC
0.960
0.009
0.940
In table row- "Cireuit-Split LEC" consider the GNN's performance test-set of problems originating from circuits which were not represented in the GNN's training set, as described in subsection 6.3 We note very high recall, at the cost of acuracy and trivial hyper-paramter tuning cost. In Table row-title "LEC" we examine the classification performance of the Core Prediction GNN module. We calculate Core Recovery (which Recall), Size Discrepancy metric due an observation during the design process that the Core Prediction module had a tendency to grossly over-predd vverpptedict and Accuracy. We find that the module performs impressively. The Core Prediction is able to identify 96% of the Core, meaning core clause is highly unlikely to be completely missed the same time, Accuracy also quite high. This important because false positives could mean the selected clause for De-Coring is in fact not part of the core. With an accuracy of 94%, de-coring on non-core clauses will very rare.
over multiple iterations.
In Section 6.2.4 We compare the performance of two runtime prediction models: one trained on only original data and the other trained on dataset augmented with generated instances.
To observe performance over differing levels of data availability, we conduct this experiment for several quantities of original training instances denoted Data Size. 3 Augmentation instances allowed per original, and augmentation is only allowed by using the original instances in the training set. Validation sets selected from the original data only, with 80/20 split train/validation split.
In Figure we can that while there is considerable overlap with whiskers of the other methods, HardCore outperforms all other methods all data sizes by at least one quartile of results. In
14

---

Predicted Runtime MAE on LEC Data
1400
Original
HardCore
1200
HardSATGEN-50
Runtime MAE
1000
HardSATGEN-Strict
W2SAT
800
600
400
200
0
100
200
300
400
500
Size of Original Data Used
Figure 7: Mean MAE on Runtime Prediction. Boxplot-view of results presented Table for LEC data.
addition to increased prediction accuracy (lower MAE), HardCore demonstrates tendency to reduce variance in performance, which we note by the lower thisker-to-whiske spread the boxplots. This effect is especially notable in data-size 200, but also be seen relative other augmentation methods for data size 300.
In the table below we show data augmentation experimental results. Since there are only 135 problems, and our focus is on data-scarce settings, we use small datasets to train the SATZilla-based that for all datasets aside from the smallest one, using HardCore to
predictor. In the table, generate an augmented dataset leads to 4%-6% reduction MAE compared to training using the original data.
Table 5: Data Augmentation experiment: MAE of Runtime Prediction averaged across solvers and 15 trials. We train runtime prediction model according to the experimental setting in 6.4.2 of the paper. Columns in the table indicate the number of original problems used in the training set (we generate 4 times per original problem in the training set). Results in the "HardCore" row are MAE for runtime prediction model trained on HardCore-augmenn augmented data, whereas "Original" indicates un-augmented performance.
Tseitin Dataset Size
Training Data
10
20
30
40
50
HardCore- Saaddoor--Aumeetee
3618.9
3410.0
3311.4
3417.7
3419.4
Original "Un-Augmentedd
3369.6
3581.9
3576.1
3544.7
3608.5
15

---

Table Data Augmentation experiment: MAE of Runtime Prediction averaged across solvers and 15 trials. We train a runtime prediction model according to the experimental setting in 6.4.2 of the paper. Columns the table indicate the number of original problems used in the training set (we generate 4 times original problem in the training set). Results in the "HardCore" row are MAE for runtime prediction model trained on aarmmeee- data, whereas "Original" indicates un-augmented performance.
FDMUS Dataset Size
Training Data
100
200
300
400
500
SandCooreAAgmented
0.220
0.197
0.162
0.142
0.142
Original (Un-Augmented)
0.246
0.213
0.184
0.173
0.145
16

---

NeurIPS Paper Checklist
1. Claims
Question:
Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We claim to propose a method which can generate SAT problems at low time-cost while still providing challenging problems. Our experimental results carefully designed to demonstrate these attributes.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results be expected to generalize other settings.
is fine include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
We have discussed computational complexity and the limited scope of the method.
Justification:
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification. asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect the scope of the claims made, e.g., if the approach was only tested on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full of assumptions and complete (and correct) proof?
17

---

Answer:
[NA]
Justification:
We do not provide theoritcal results this work.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should complemented by formal proof's provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We make our best efforts to ensure our results are reproducible. We provide source code along with clear README instructions in the supplementary material. We introduce the full pipeline of our method as well as each component design in the methodology section Moreover, we also provide sufficient experiment details in the experimental setting 6.1
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (c.g., to registered users), but it should be possible for other researchers to have some path to reproducing verifying the results.
18

---

5. Open access to data and code
Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
The source code is provided in the GitHub link provided on the first page, along with clear README instructions to ensure our code can run with minimal effort from users.
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips. cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed run to reproduce the results. See the NeurIPS code and data submission guidelines (https www.eeeeeeoeeemmmeeeeeeeeeee
for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [Yes]
Justification: All the training and testing details are included in experiment setting sec- tion 6.1 We provide additional details regarding the data, the hyperparameter selection and the implementation details in, appendix A. A.4
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can provided either with the code, appendix, or as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [Yss]
Justification: We conduct thorough Wilcoxon pair-rank statistical significance tests our key result table in 2 asterisks are placed at the best result which passes the Wilcoxon pairwise ranking test against the second-best for p 0.05.
Guidelines:
The answer NA means that the paper does not include experiments.
19

---

The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the enror bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall
with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification: We discuss the processing units used in experimental setting section 6.1 as well as wall-clock computation time in 6.2.2
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make it into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics http:////.e.erese.cc////////saas
Answer: [Yes]
Justification:
We have read and confirm our work fully complies with the Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. there special consid- eration due to laws or regulations in their jurisdiciio))
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: We do not believe this work represents significant potential societal impacts, either positive negative.
20

---

Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g.. disinformation, generating fake profiles, surveillance), fairesss considerations (e.g., dep.oymmly of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of MI).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our experimental data is either proprietary or synthetic, and is of low risk level to people as it is generally circuit-design data
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question:
Are the creators or original owners of assets (e.g., code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: The codes we used as basic bricks to build our method, particularly Hard- SATGEN, are properly cited in code (Readme file). No license restriction noticed for HardSATGEN code. All the datasets we used in the experiments are also cited and follow the license from the original source.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
21

---

The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g.. website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that re-packaged, both the original license and the license of the derived asset (if it has changed) should provided.
If this information is not available online, the authors are encouraged to reach out to the asset's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: In the source code and data provided in the supplementary materials, we explicitly state that they are released under the CC BY-NC 4.0 license to encourage academic usage.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: Not involved with crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: This work does not require research with human subjects.
22

---

Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with
human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent)
may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
23


Reviews:
[{"review_id": "0OTQmCQ9Xw", "reviewer": "Reviewer_RF4y", "summary": "This paper addresses the scarcity of practical data (industrial satisfiability problem instances) for training deep learning methods for SAT solving. The existing data augmentation methods suffer from either the limited scalability or the collapsed hardness of the generated instances. Therefore, the authors introduced a fast augmentation method while preserving the original data's hardness. The primary technical contribution is a fast UNSAT core detection procedure using graph neural networks to monitor the hardness of UNSAT formulae during data augmentation. The empirical evaluation confirmed the new method’s fast generation speed and the preserved hardness of the generated instances. In the application of solver runtime prediction, the augmented data led to a 20-50 percent reduction in mean absolute error.", "questions": "1. How much time did you spend on collecting data and training the core predictor? If the core predictor doesn’t generalize well to a new family of instances, is the re-train time going to be a huge overhead of your method?\n2. How many instances are generated from a single seed instance by HardCore and HardSATGEN? If you could use one seed instance to generate multiple instances, why can’t you keep the same number of seed instances for HardCore and HardSATGEN in line 304?\n3. Why do you use the extremely small data size (e.g., 10 and 100) in Table 2? It should be considerably insufficient, even after the three-time augmentation, to train a fair runtime predictor.", "limitations": "The limitations have been well addressed. The authors acknowledged that the method can only be applied to UNSAT instance generation and is not suitable for the SAT case. They also mentioned that the results are limited to the current datasets and their method can’t scale to large SAT problems with millions of clauses.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "The proposed method achieved the best of both worlds. It has a similar speed to a fast generator while preserving a similar hardness of generated instances to a high-quality but slow generator.\n\nThe proposed idea is simple and easy to follow, yet effective. The paper is well-written.\n\nThe authors performed extensive evaluations to demonstrate the preserved hardness of the generated instances in various aspects, such as the preserved average hardness, the hardness distribution over instances, the runtime distribution per solver, and the best-solver distribution over instances.\n\nThe authors illustrated the effectiveness of their method in a practical application (solver runtime prediction). The augmented data successfully reduced the mean absolute error by 20-50 percent.", "weaknesses": "The authors don’t present how well the core predictor generalizes to other datasets. We may need to re-train the core predictor when applied to a new family of instances if it doesn’t generalize well, which would introduce extra overhead not presented in the current evaluation.\n\nThe technique to eliminate an easy core described in lines 176-191 has been proposed in [1]. The authors should cite the work and move the content to related work.\n\n[1] Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, and Junchi Yan. 2023. HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline. In Proc. of ACM SIGKDD Conf. Knowledge Discovery and Data Mining\n\nIn line 190, the satisfying solution should be (A=0, B=0, C=1).\n\nThe axis label is missing in Fig. 5.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We would like to thank the reviewer for their insightful and\nconstructive review. In following the reviewers comments we have\nuncovered new, valuable experiments (Circuit-Split LEC) as well as\nshort-comings in the description of certain details of the experimental\nsetting.\n\n## Weaknesses\n\n1.  *GNN generalization to other datasets not shown. If we have to\n    re-train for new data, this consists of overhead.*\\\n\n    In order to measure GNN generalization to new data without\n    re-training, we create a new split of the LEC data. Each problem in\n    the LEC data can be traced back to one of 29 circuits. By randomly\n    splitting circuits into training circuits and test circuits (and\n    then building training and evaluation sets with their respective\n    problems), we can measure generalizability. Note that we would not\n    expect the model to generalize to problems derived from a completely\n    different application domain (although fine-tuning a previously\n    model in a domain adaptation strategy might be interesting to\n    explore).\n\n    In Table 2 we report the GNN performance on this experiment. In the\n    paper we discussed that Core recovery is the priority, because if we\n    falsely classify true-positives then we may be un-able to de-core\n    the current core (since the necessary clause may be un-detected),\n    whereas if we mis-classify true-negatives then we will simply\n    de-core a non-core clause. Given enough iterations of\n    core-refinement, a true-positive clause will eventually be selected\n    for de-coring (since the clause for de-coring is randomly selected\n    from among the detected clauses). With this in mind, the threshold\n    hyper-parameter which is used on the sigmoid outputs at model\n    readout becomes a useful parameter in cases where classification\n    performance is weakened: we can boost Core Recovery (recall) by\n    lowering the threshold. Tuning this threshold is very low-cost:\n    testing a thousand problems takes 500 seconds on a GPU. We find that\n    by testing values $[0.1, 0.3, 0.5, 0.7, 0.9]$ --- which takes 25\n    minutes --- we can tune the threshold to provide similar recall to\n    the in-distribution model.\n\n|                   | ↑ Core Recovery Ratio (Recall) | ↓ Core Size Discrepancy (TP-P)/(P+N) | ↑Accuracy  |\n|-------------------|--------------------------------|--------------------------------------|------------|\n| Circuit-Split LEC | 0.97                           | 0.05                                 | 0.65       |\n| LEC               | 0.960                          | 0.009                                | 0.940      |\n\n\n2.  *The de-coring method of adding a literal to a clause was put\n    forward by the HardSATGEN paper. HardSATGEN should be cited and this\n    should be moved to related work.*\\\n    Thank you for this comment. We will modify the paper to acknowledge\n    this and cite HardSATGEN accordingly. We did not intend to imply\n    that this was a contribution of our work.\n\n3.  *Correct Satisfying solution at l. 190* Thank you, we will make this\n    correction.\n\n4.  *Fig. 5 axis label missing* Thank you, we will correct this in the\n    final version.\n\n## Questions\n\n1.  *How long does it take to collect training data and train the core\n    predictor for new family of instances?*\\\n    Data collection requires the execution of iterative core refinement\n    using a traditional core detection algorithm. This process is indeed\n    costly. With 200x parallelization, which is easily achievable using\n    a moderately-sized server, data collection for training the GNN\n    predictor takes approximately 26 hours. The training itself of the\n    GNN is relatively cheap computationally, taking only 135 minutes.\n    While there are thus training costs, we stress that the generation\n    is very low-cost, which allows us to amortize training cost over\n    many generations. For example, HardCore can generate 20,000 LEC\n    instances in 24 hours, once trained. This means that the total time\n    required to generate those 20,000 instances, including\n    training-time, is 24+26+2.25 hours, which amounts to 9 seconds per\n    instance. This is very low compared to HardSATGEN's generation cost\n    for LEC of 6441 seconds per instance, even without including its\n    training time-cost.\n\n2.  *How many instances are generated per seed?*\\\n    We generate 5 instances per seed using each method. We will add this\n    information to the experimental setting in the text.\n\n3.  *If we can use a seed more than once, why can't we obtain many\n    HardSATGEN generations?*\\\n    With HardSATGEN, the primary bottleneck is the slow iterative\n    core-detection step during generation. Given that this must be\n    performed for each generation (and not only for each seed),\n    generating 100 instances from only 1 seed (100 instances per seed)\n    with HardSATGEN has the same cost as generating 100 instances from\n    100 seeds (1 instance per seed). HardSATGEN's generations were\n    limited during our experiments by time budgets for generation, not a\n    scarcity of seeds (we have as many seeds for HardSATGEN as we did\n    for HardCore and the other baselines).\n\n4.  *Why do we use such small data in Table 2 (runtime-prediction\n    experiment) It should be insufficient to train a fair runtime\n    predictor?*\\\n    The motivation for our work is that SAT data is often scarce. This\n    is especially the case for public datasets. Therefore in this\n    downstream task, our goal was to model a realistic case, where one\n    is provided with only a small number of examples in the dataset for\n    training the predictor.", "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": "G1XyNQHFI6", "reviewer": "Reviewer_kFMW", "summary": "This paper introduces HardCore, a novel method for efficiently generating hard Unsatisfiable (UNSAT) Boolean Satisfiability (SAT) problems, addressing the critical challenge of data scarcity. The approach combines a Graph Neural Network (GNN) for rapid core prediction with an iterative core refinement process, enabling the generation of thousands of hard instances in minutes or hours while preserving problem difficulty. HardCore outperforms existing methods in terms of generation speed and hardness preservation, as demonstrated through experiments on both Logic Equivalence Checking (LEC) data and K-SAT Random data. Despite limitations such as applicability only to UNSAT problems and potential scalability issues with extremely large instances, HardCore represents an advancement in SAT problem generation.", "questions": "How would one extend your technique to more structured classes of formulas?", "limitations": "It would really strengthen the paper if the authors were to study the structural properties (e.g., clause-variable ratio, tree width, hierarchical community structure,...) of the generated instances and identify why they are hard for modern SAT solvers.", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "* The work provides a meaningful contribution to the SAT community by introducing a novel method that generates SAT instances within a reasonable timeframe while preserving the hardness of the original problems. The work has potential applications in various industrial settings, though the scalability limit of the approach might pose a challenge.\n   * The authors conduct extensive experiments, comparing their method against multiple baselines and evaluating various aspects such as hardness preservation, generation speed, and similarity to original distributions. The paper compares against relevant and recent baselines (HardSATGEN, W2SAT, G2MILP), providing a comprehensive view of how HardCore performs relative to the state-of-the-art.\n   * Innovative core refinement process: The iterative core refinement process (Figure 2) is a clever approach to gradually increasing problem hardness while avoiding the creation of trivial cores.", "weaknesses": "* The experiments primarily focus on two datasets (LEC Internal and K-SAT Random), with one being proprietary. This somewhat limits the generalizability of the results.\n   * While the paper focuses on runtime distributions and solver rankings, it lacks a deeper analysis of the structural properties of the generated instances (e.g., clause-to-variable ratios, community structure) compared to the original ones.\n   * The core refinement process (Section 5.1) involves adding a single literal to break easy cores. The paper doesn't explore more sophisticated strategies or justify why this simple approach is sufficient.\n   * The paper mentions struggles with \"extremely large SAT problems\" but doesn't clearly define what constitutes \"extremely large\" or provide empirical evidence of where the method breaks down.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We wish to express our gratitude to the reviewer for their\nacknowledgement of our extensive experimentation and innovation. The\nreviewer's comments have guided us to explore meaningful improvements to\nthe presented work: complete results on an additional public dataset, a\ndeeper analysis of scaling considerations and comparison of SAT-problem\nstatistics. The reviewer has also illuminated multiple promising avenues\nfor future work.\n\n## Weaknesses\n\n1.  *The experiments focus on only 2 datasets, limiting result\ngeneralizability* \n\nPlease see the global rebuttal for the\npresentation of results on a new dataset in order to address this\nissue. We introduce some data from the SAT Competition database and\npresent results which show that HardCore is able to generate\nproblems which resemble the SAT Competition (SC) data in hardness.\nResults also show that HardCore is able to provide data augmentation\nwhich improves a runtime-prediction model's performance by 4-6%.\n\n2.  *Lacks \"deeper analysis\" of structural properties\n(clause-to-variable ratios, community structure)*\n\nWe chose not to report such results in the paper because such statistics have neither been claimed nor shown\nto have causal connections to hardness or industrial structure, only correlation.\n\nDespite this, we agree with the reviewer that the paper would\nbenefit by a presentation of the structural properties of the\ninstances generated by HardCore. In the table below, we compare the\nstatistics of the generated instances to those of the original\nproblems, replicating the experiment that was peformed in the\nHardSATGEN paper. We report the number of variables and clauses,\nclustering on the variable-instance graph, and modularity on four\ngraph-representations. Note that both HardCore and HardSATGEN only\nadd a single auxiliary variable (to eliminate easy cores), so the\nnumber of variables is a close match. HardCore maintains the number\nof clauses by setting the number of generated clauses (an easily-set\nparameter of the generation algorithm) accordingly. For other\nstatistics, HardCore achieves values that are relatively close to\nthose of the original instances, with a slightly reduced modularity\nin the VIG and LIG representations, compared to HardSATGEN. This is\nlikely because HardSATGEN monitors VIG communities while HardCore\ndoes not consider incidence representations.\n\n|              | HardSATGEN | HardCore  | original |\n|--------------|------------|-----------|----------|\n| num. vars    | **933.8    | **933.8** | 932.8    |\n| num. clauses | 3395.16    | **3400.2  | 3400.2   |\n| VIG clust.   | 0.38       | **0.39    | 0.39     |\n| mod. VIG     | **0.74**   | 0.56      | 0.74     |\n| mod. LIG     | **0.74 **  | 0.63      | 0.75     |\n| mod. VCG     | **0.81     | 0.78      | 0.81     |\n| mod. LCG     | **0.64**   | **0.64    | 0.67     |\n\n\nIt is our view that hardness distributions --- whether per-solver,\nranking, multi-solver --- are considerably more important than the\nmeasured structural statistics presented in previous works. Other\ngenerators, despite being capable of preserving structural\nstatistics reasonably well, generate trivial problems. These clearly\ndiffer in critical ways from the seed instances from the perspective\nof the solvers. For example, W2SAT reports modularity very similar\nto the original problems' modularity and yet fails to generate hard\ninstances. Since HardCore is directly shown to preserve hardness\nbehavior well, we did not strive for similar modularity.\n\n3.  *De-coring is done by adding a single literal to break cores. More\nsophisticated strategies are not explored. Why is this approach\nsufficient?* \n\nExploring more sophisticated de-coring strategies could\nbe an interesting direction for future work, especially for\napplication to more structured formula families. We\nchose to use the established de-coring paradigm from the HardSATGEN\nmethod, considering it to be interpretable due to its\nsimplicity. More complicated strategies, which might add or remove\nexisting variables from the clauses (instead of adding new ones),\ncould introduce unforeseen conflicts and cores which are easier than the current de-coring target. The\ncurrent strategy guarantees the removal of the current core, without\nconstructing a new one, which is desirable. Since the approach\nproved experimentally effective, we did not explore other\nstrategies.\\\n\n4.  *The paper mentions struggles with extremely large problems. Define\nwhat constitutes \"extremely large\" or provide empirical evidence of\nwhere it breaks down* \n\nPlease see our discussion of scalability in\nthe global rebuttal, in which we describe the memory-scaling in\nworst-case dense problems and more realistic sparse problems and in\nwhich we discuss worst-case break-down given our hardware.\n\n## Questions\n\n1.  *How would one extend the work to more structured classes of\nformulas?*\n\nFor highly structured problems, the generation mechanism would have\nto be designed such that a formula adheres to the required\nstructure.\n\nStructured problems such as the pigeonhole problem and\ngraph-coloring are often easy to generate. For example, a graph\ncoloring problem can be generated by generating a graph in any\nrandom way, and then applying the coloring problem. A pigeonhole\nproblem can be generated simply by parameters for the\nproblem.\n\nCore Prediction itself would likely remain un-changed. In fact, if\nthe data are focused on one structured\nclass of formulas, we would expect high performance from the\nprediction model.\n\nSpecial care would be required to ensure that the\nde-coring operation does not corrupt the required structure of the\nproblem. By adding a new variable to\nde-coring target clauses, we may change structure of the problem \nin such a way that it no longer conforms to the strict\nstructure of the family. De-coring operations would therefore have\nto be specially designed for each family type.\n\nThis represents an interesting challenge and is an intriguing\ndirection for future work.", "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": "E8L65b3tot", "reviewer": "Reviewer_vCMn", "summary": "This paper proposes a novel method for generating hard UNSAT problems. The method targets the \"core identification\" problem and iteratively performs refinement using a GNN-based detection procedure, which preserves the key aspects of the original instances that impact solver runtimes. The experimental results show that the method can generate instances with a similar solver runtime distribution as the original instances in a short time.", "questions": "1. Please provide justifications on the correlation between solving hardness and UNSAT core size. \n2. Even though considering the minimal UNSAT core, one instance may contain multiple cores. How to handle this one-to-many mapping problem? This problem is significant as it is directly related to the supervision.\n3. The random k-SAT and LEC cases have a very strong bias compared to the real instances. The authors should also prove the generalization ability of their proposed approach on more diverse datasets, such as SAT competition benchmarks. \n4. In Section 6.2.3, you mention that you use a subset of the training set as the evaluation dataset. This is not the right.\n5. When you perform the core refinement step, can the problems generated in the middle be used? How does n, the number of refinement steps, affect the characteristics and performance of the generated problems?", "limitations": "Yes, the authors have stated the limitations of their work.", "rating": 4, "confidence": 5, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "This paper introduces a novel method to generate hard UNSAT problems in a reasonable time frame, which alleviates the data scarcity problem in the SAT solving domain and improves the performance of deep learning methods in this area. Compared to previous methods, this method can generate SAT problems that are more similar to the original instances.", "weaknesses": "1. There is not enough support for the correlation between hardness and core size. For example, in the random 3-SAT problem, the UNSAT core can constitute a significant portion of total instances, even more than 80%, yet modern solvers can easily address these instances.\n2. Lack of details about model training. There are no explanations on how to prepare the training dataset. \n3. The experimental setting is not convincing. Authors only perform the proposed hard case generation approach on LEC and random k-SAT problems, however, there are no details about how to construct these two datasets. Moreover, it is essential to show results on other datasets to showcase the generalization ability of the proposed method, such as the SAT competition benchmarks. \n4. There are some logical problems in the paper’s writing. In the “Core Refinement” part, the paper states that the addition of random new clauses is likely to create a trivial core. However, I find that in the core refinement pipeline, there is no addition of new clause. Instead, new literal is added. The writing here is kind of messy.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their careful and critical comments. These\ncomments have prompted several new explorations, including an\nexamination of the progression of hardness during refinement, and the\naddition of a new dataset to the experimental setting. These improve\nboth the strength of our results and the depth of our analysis of the\nmethod.\n\n## Weaknesses\n\n1.  *Correlation between hardness and core size is not sufficiently\nsupported.*\n\nWe do not claim in the paper that there is a correlation between the\ncore size and the hardness. For our proposed\ntechnique to work, our key assumption is that if a problem is easy\nthen core prediction can identify the easiest core, and then by\nremoving that core the problem is made harder. The experimental results\ndemonstrate that we generate challenging problem instances,\nproviding support that our assumption is correct. We agree with the\nreviewer that there is value in providing more direct evidence.\n\nFirst, we evaluate the hardness of the original problems in the LEC dataset. Note that this is a\nreal-world dataset derived during industrial circuit design. Figure\n3 (left) in the attached pdf shows that there is a general trend of\nthe hardness increasing as the core size increases, up to a\nthreshold of 4000-5000 clauses. This trend is observed for absolute\ncore size rather than the percentage of clauses in the core; the\nreviewer's observation is correct that an 80% core can be easy.\n\nAlthough we observe this correlation, it\nis not essential for our method. Much more important are the results\nshown in Figure 3 (right) in the pdf, where we show how the hardness\nchanges as a result of refinement. The figure shows\nboxplots of the percentage change in hardness for different bins of\ninitial hardness. For easy problems we increase the\nhardness sometimes by a factor of over 200, indicating successful\nhardening of hardness-collapsed problems.\n\n2.  *Model training details missing.*  \n\nDetails on how the training data is prepared for the core prediction\nmodel (In particular, how supervision labels are generated) is\nprovided at l. 233.\n\nThere are three **separate** groupings of the dataset: (i) Core\nPrediction training data, (ii) generation seeding data, and (iii)\nthe remaining data. This split is chosen randomly. Core\nPrediction training data can be small (we used 15 problems),\nbecause we use each problem as a seed instance 5 times for generation \nfollowed by core-refinement with a traditional core detector. Saving problem-core pairs at each step,\nwe obtain 15,000 training pairs for the\ncore-predictor model. The seeding data are used to\nseed HardCore once the core predictor is trained in order to obtain\ngenerations to evaluate. These generations are then compared against\nthe seed data for runtime similarity. Finally, these generations\n(and their seeds) are used to train a runtime-predictor model,\nwhich is evaluated on the remaining un-used data.\n\nThe core prediction model is trained with a binary cross-entropy\nloss using the prepared data.\nFor more details on the training procedure, please consider the\ncode provided in the supplementary material. We will add a detailed\ndescription of this training process in an appendix.\n\n3.  *only 2 datasets, no SAT Competition benchmarks. *\n\nPlease see the global rebuttal, in which we present new results on\nSAT Competition data. \n\n4.  *Construction details of the used datasets are not provided.*\n\nFor details on how the K-SAT dataset was generated, please see\nAppendix section A.4. The problems from the LEC dataset are\nSAT problems which were solved during the design of real circuits,\nand were saved for future use in analysis and research.\n\n5.  *Unclear writing: in \\\"Core Refinement\\\", the paper states that\nadding new clauses is likely to create trivial cores, but clauses\nare not added during core refinement.*\\\n\nIn the text, the correction will be at line 176: \"The addition of\nrandom clauses during **generation** is very likely to [...]\".\nClauses are not added during refinement, the reviewer is correct.\n\n## Questions\n\n1.  *Justify core-size and hardness correlation*.\\\n\nSee Weakness 1.\n\n2.  *One instance may have multiple cores. How to handle this one-to-many mapping problem.*\\\n\nThe goal of the estimator is not to only the easiest core. \nThe first core to be output by the detection algorithm is considered the easiest \n(finding a core proves the problem UNSAT, solving the problem).\nWe use the outputs of the core detector as labels for\nsupervision, and find that the GNN is able to identify the easiest\ncore based on performance results shown in Table 4 of Appendix B of\nthe paper. Once that core is de-cored, the other core may now be the\neasiest, and it will be detected in the next refinement step.\n\n3.  *k-SAT and LEC cases have very strong bias compared to real\ninstances.*\\\n\nWe believe the LEC cases we use in the paper must be considered as\nreal instances as they come from real industry.\nLogic Equivalence Checking (LEC) is a critical step in\nlogic synthesis for circuit design. The LEC data we use in the paper came from the\ndesign pipeline of 29 industrial circuits by a prominent circuit\ndesign company.\n4.  *The authors should show generalization ability on the SAT\ncompetition data.*\\\n\nSee weakness 3.\n\n5.  *In section 6.2.3 it is mentioned that a subset of training data is\nused as evaluation data. This is not right.*\\\n\nWe do not evaluate with training data at any point in the\nexperimental method. We have been unable to locate any reference to\nthis in Section 6.2.3. If you could kindly quote the line (or\nparagraph) in which this was conveyed, we would be very happy to\nclarify the issue.\n\n6.  *Can problems from halfway through core refinement be used? How does\nthe number of refinement steps affect performance?*\\\n\nYes, although they will likely be easier. Problems usually get harder in\na smooth progression during refinement, as shown in Figure 1 (left).", "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": "v5bVLYMgba", "reviewer": "Reviewer_1y8R", "summary": "This paper presents a procedure for synthesizing hard UNSAT formulas from a given distribution of UNSAT formulas. Concretely, a formula is generated by 1) extracting a core from a seed instance; 2) adding random new clauses; and 3) refining the formula to become harder. In step 3), a GNN is trained to predict UNSAT core of a given formula and the predicted core is relaxed, potentially yielding a larger core. On two problem distributions, LEC Internal and random K-SAT, the proposed method can generate hard instances faster than previous approaches, and the generated instances exhibit similar hardness distribution.", "questions": "1. We have previously argued that random data differs from real data in important ways that make it unsuitable for machine learning applied to real problems. Could you elaborate?", "limitations": "The authors adequately addressed the limitations. No potential negative societal impact.", "rating": 7, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "- The proposed method strikes a good balance between the hardness of the generated instances and the generation time. It can generate instances much harder than W2SAT, while in a much faster manner than HardSATGEN. \n- The combination of the two ideas, iteratively relaxing core to generate hard instances and learning to predict cores, is quite clever and elegant. \n- The fact that the solver performance on the synthetic instances resembles that on the original instances is a good indication that the generated instances are similar in some way to the original instances.", "weaknesses": "- It seems that the proposed core refinement technique can be viewed as a post-processing step that can be applied to any initial formulas (e.g., ones generated by W2SAT). Have the authors considered building on top of previous DL-generated formulas? Compared with formulas generated by randomly adding clauses to an original UNSAT core, conceptually, formulas generated by a method like W2SAT, which are trained to embed a formula distribution, seem to be a more justifiable starting point. \n- The method can still only handle relatively small formulas.\n- Given that the LEC benchmarks are proprietary, only random K-SAT will be made publicly available. However, one could have considered using dataset such as SATLIB like in previous work (e.g., SATGEN, G2SAT, W2SAT).\n\nMinor:\n- x axis labels are missing in Figure 5. \n- Line 353: \"syntehtic\" -> synthetic", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We deeply appreciate the reviewer's generous acknowledgement of the\nelegance and performance of our method. In addition, the reviewer's\ncomments about scalability and publicly available data have led us to\nmake significant additions to the depth of our work's experimental\nsetting and analysis. Finally, the reviewer has provided an insightful\nfuture direction regarding the generation mechanism used in our method.\n\n## Weaknesses\n\n1.  *Core refinement can be viewed as post-processing applied to any\n    generator. Have authors considered building on top of previous\n    DL-generators? Starting with methods like W2SAT which are trained to\n    embed formula distributions seems more justifiable than starting\n    with a random generator.*\\\n    Viewing core refinement here as a post-processing step applicable to\n    any generator is valid. During the design of the proposed method, we\n    did consider building on top of previous DL-generators. However, a\n    random generator designed to emulate industrial problems was\n    selected for its simplicity, minimal cost, and the convenience of\n    not having to train it. Indeed, perhaps using a DL generator may\n    improve the downstream performance. Investigating such possibilities\n    could prove insightful and is a valuable direction for future work.\n\n2.  *The method can still only handle small formulas*\\\n    While scalability is certainly a concern as discussed in the\n    Limitations section of the text, the breaking point of our method\n    for a 32GB GPU, for example, would be in worst-case a graph with\n    hundreds of thousands of variables and clauses. This is a problem\n    size beyond many real-world applications. In the LEC data, no\n    problem exceeds 100,000 clauses. This limitation was primarily\n    expressed in consideration of the SAT Competition data, in which\n    problems (almost always randomly generated problems) can sometimes\n    reach a million clauses or more. Our scalability limitation, as\n    discussed in the general response, is primarily related to memory,\n    and the storage of the adjacency matrix of the graph. A potential\n    direction for future work is to investigate the application of\n    existing high-efficiency GNN methods that are capable of addressing\n    graphs of tens-of- millions of nodes.\n\n3.  *Only K-SAT will be made publicly available. Why not use dataset\n    such as SATLIB like in previous work?*\\\n    We decided against using SATLIB as the great majority of its\n    problems are either randomly generated or not UNSAT (our method is\n    limited to UNSAT problems). Additionally, similarly to the SAT\n    competition benchmarks, the data is composed of problems from\n    several highly distinct sources, which is undesirable for\n    machine-learning applications. Despite this, we have included in the\n    global rebuttal and single-page pdf results on data from the SAT\n    Competition, showing that our method is able to generate hard\n    problems and provide data augmentation for SAT Competition data. We\n    will make the code for our SAT Competition experiments publicly\n    available.\n\n## Questions\n\n1.  *It has been argued that random data differs from real data in\n    important ways that make it unsuitable for machine learning applied\n    to real problems. Could you elaborate?*\\\n    The clearest demonstration of the difference between real data and\n    random data, in our view, is the notable difference in solver\n    performance. It is generally accepted in the literature that some\n    solvers are random-specialized and others are industry-specialized.\n    For example, the experimental results in \\[1\\] are heavily based on\n    this. One can also see such specialization by noting that the best\n    solver on the SAT Competition random tracks is not the same as the\n    best solver on the SAT Competition main track. In fact, the\n    existence of separate tracks itself indicates an acknowledged\n    distinction between the types of data.\n\n    Given this distinction between the behavior of random and industrial\n    data, training an industrial-facing model on random data leads to an\n    out-of-distribution problem. Inference must be performed for\n    problems that are very different from the training data. It would be\n    equivalent to augmenting a real-world image dataset with random\n    patterns. In most cases the model will perform poorly. For example,\n    SAT-solver selection is a machine-learning task for SAT in which,\n    given a problem, we aim to rapidly choose the solver which is likely\n    to solve the problem the fastest. This is a task which greatly\n    benefits industrial settings in which thousands of SAT problems must\n    be solved each day and computation and time costs must be minimized.\n    Training such a selection model on random data would result in the\n    model learning a wholly different runtime distribution than that of\n    the industrial data. A similar example is low-cost benchmarking, in\n    which a model is trained to predict the performance of a solver over\n    a benchmark. This task is of interest to solver-designers, as it can\n    be much cheaper than running a design-iteration of a new solver on\n    the whole benchmark data. If random data is used to learn to\n    benchmark a solver on industrial problems, the predictor would\n    likely predict benchmarks as if the industrial data were in fact\n    random. A third example is the task of hyper-parameter tuning of\n    solvers, as presented in the HardSATGEN paper as a down-stream task.\n    If one were to use random data to tune the hyper-parameters, the\n    solvers would likely be poorly tuned for industrial data, whose\n    hardness distributions are very different to random data.\n\n    [1]J. Giraldez-Cru and J. Levy, \"Generating sat instances with\n    community structure,\" in Artificial Intelligence, 2016, p. 119--134.", "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:
We thank the reviewers for the insightful and thoughtful reviews. All
reviewers have stated that the proposed method is novel and stands as a
meaningful and innovative contribution to the field. Several reviewers
agreed that the experimentation was extensive and demonstrative of
improvements over existing work. The primary concerns expressed in the
reviews were (1) scalability and cost overhead; (2) result
generalizability to other datasets; and (3) certain details which
required clarification. We have addressed these concerns in the response
by (1) providing a more detailed cost analysis for the pre-processing of
data; (2) presenting new results on a public dataset; and (3) providing
additional clarifications, details and analysis where required.

\(1\) Scalability: Memory limitations are the primary challenge for our
proposed method, due to the need to store the graph. For our
experimental hardware (32GB GPU) and our implementation of the graph
building/storage ($O(nm)$ for a problem with $n$ clauses and $m$
variables), a problem with 256,000 variables and 1,000,000 clauses would
require $256,000 \times 1,000,000 \times 1 = 256 \times 10^9$ bits, or
32 gigabytes. Given a GPU with 32GB of memory, this would be a breaking
point for the method. Of course this is the worst case, which only
occurs for a completely dense graph representation. In practice, clauses
in the LEC data, for example, tend to have on average 3 or 4 variables.
Since in the LCG clause nodes are only connected to the variables of
which they consist, each clause node would then only have degree of 3 or
4, meaning the graph is very sparse. Thus, in practice the primary
memory cost of our model scales moreso according to $O(dn)$, assuming
average number of variables in a clause is $d$, and assuming the
implementation is adapted to leverage the sparse structure (using
edge-lists instead of dense adjacency matrix, for example).

In cases where the problem is large and dense, another option might be
the use of more specialized GNN methods that are specially designed to
handle very large graphs. For example, by sampling from neighborhoods or
loading portions of the graph from storage.

For time-cost scaling, the primary point in the pipeline in which we
suffer scaling challenges is during pre-processing. We build graphs from
the text-file representation of the problems. The time-cost of this step
is linear with the problem size, measured in terms of the number of
clauses. Given this, time-cost is not a major factor in the scaling
issue.

We will add text to clarify the scalability considerations outlined
above and specify the precise nature of an "extremely large" problem
that would challenge our proposed generative model.

\(2\) Public Dataset:

SAT Competition data is an aggregation of thousands of families of
problems and is therefore highly heterogeneous. As discussed briefly in
the introduction, this heterogeneity is highly unfavorable for machine
learning algorithms and tasks. Thus, machine-learning papers are often
required to find creative ways to provide large-scale experimental data
(and this may not conform to real-world data). In \[1\], for example,
data is randomly generated.

In order to demonstrate that our method can generalize to other
datasets, we now provide new results on all UNSAT problems from the SAT
Competition data coming from the "Tseitin" family. The data was compiled
using the GBD database, querying for "family=Tseitin and result=unsat".
There are 135 "Tseitin"-family problems in the database,

We repeat the runtime distribution experiments on this data, generating
5 instances for each of the 135 seed instances. We see very similar
stacked histograms for the solver rankings (Fig. 2 in the attached
response pdf). Fig. 2 (right) shows per-solver boxplots comparing seed
instances and generated instances. Overall these are similar, although
solvers 1 and 6 show greater upper-range in the original data compared
to HardCore. However, the median solve times for solvers 1 and 6 are
still close.

In the table below we show data augmentation experimental results. Since
there are only 135 problems, and our focus is on data-scarce settings,
we use small datasets to train the SATZilla-based predictor. In the
table, we see that for all datasets aside from the smallest one, using
HardCore to generate an augmented dataset leads to a 4%-6% reduction in
MAE compared to training using the original data.

\[1\] D. Selsam et. al., "Learning a sat solver from single-bit
supervision,", in ICLR, 2019.

| Training Data           | 10              | 20            | 30              | 40              | 50              |
|-------------------------|-----------------|---------------|-----------------|-----------------|-----------------|
| HardCore-Augmented      | 3618.9          | **3410.0** | **3311.4** | **3417.7** | **3419.4** |
| Original (Un-Augmented) | **3369.6**| 3581.9        | 3576.1          | 3544.7          | 3608.5          |

   Data Augmentation experiment: MAE of Runtime Prediction averaged
  across 7 solvers and 15 trials. We train a runtime prediction model
  according to the experimental setting in 6.4.2 of the paper. Columns
  in the table indicate the number of original problems used in the
  training set (we generate 4 times per original problem in the training
  set). Results in the "HardCore" row are MAE for a runtime prediction
  model trained on HardCore-augmented data, whereas "Original" indicates
  un-augmented performance.

Meta-review: This paper proposed a new way of synthesizing hard UNSAT formulas (specifically the industrial satisfiability problem instances) for training deep learning methods for SAT solving. The main idea is to have a fast UNSAT core detection procedure using GNNs. With the augmented data, the paper is able to achieve significant improvement, while also to generate instances faster than previous ones. 

Overall the reviewers like the balance achieved by the authors between the quality of the generated instances and the speed. And this can be very practically applicable, given the ease of the implementation. While the reviewer vCMn had some initial concerns, the authors have provided convincing rebuttal to address that.

With above, we recommend the acceptance of this paper.
Decision: Accept (poster)