MixSATGEN: Learning Graph Mixing for SAT Instance Generation

Thanks for the thorough review and valuable comments. We are encouraged with your acknowledgment of our topic importance, writing clarity, methodology design, and empirical results. Below we respond to your specific comments.

Q1: Experimental results show that the proposed method is not always superior to HardSATGEN.

Please note that reproducing computational hardness in the SAT instance generation task is considerably challenging which has not been achieved until HardSATGEN [1]. Its success stems from its fine-grained control over the instance structure, particularly for the unsatisfiable core structures, as well as the postprocessing design involved to maintain the dominant effect of the unsat core structure.

While the design in [1] is effective, it confines the method to unsatisfiable instances only. Since real-world datasets generally incorporate both satisfiable and unsatisfiable instances, merely learning from the unsat instances can lead to certain negative impacts on downstream tasks like hyperparameter tuning, as evidenced by Table 3 in the new revision. In contrast, MixSAT surpasses this limitation, demonstrating generality to both satisfiable and unsatisfiable instances. MixSAT is also free from the node merge-split framework of previous learning-based methods [1-3], naturally meeting the hardness analysis and requirements set forth in [1]. Notably, our performance on satisfiable instances is significantly superior to all other methods.

We acknowledge that our effectiveness on unsatisfiable instances is not as strong, especially considering [1] already provides a tailored solution for unsatisfiable problems. However, we believe the two methods can complement each other. As evidence, we have supplemented the study with hyperparameter optimization experiments and present the combined effects of both methods in Table 3, which show the significant effectiveness of our methods in practice as a boosting tool complementary to HardSATGEN.

Q2: Hyperparameter tuning with the generated instances.

Thanks for the valuable point. We supplement the hyperparameter tuning results on the state-of-the-art SAT solver Kissat in Table 3 of the new manuscript. Due to the complexity of the table format, we refrain from presenting it in this response.

We adopt one of the Bayesian optimizers HEBO to tune the solver. The tuned hyperparameters include restart interval, reduce interval, and decay, which pose impacts on the frequency of restarting, frequency of learned clause reduction, and per mille scores decay respectively. For each method, the Bayesian optimizer tries 200 sets of hyperparameters and we select the top 5 hyperparameters to evaluate on test instances. The best runtime results are presented in the table. Due to the costly Bayesian optimization process, we select instances with runtimes under 500 seconds for experiments.

Note in Table 2, MixSAT reproduces computational hardness well on satisfiable instances, while HardSATGEN [1] can only learn from unsatisfiable instances. Table 3 shows the matched performance where MixSAT and HardSATGEN perform the best for satisfiable and unsatisfiable instances respectively. Thus, we also consider simultaneously adopting MixSAT learned from satisfiable instances and HardSATGEN learned from unsatisfiable instances for tuning, which presents the best overall performance. In general, the generated instances by the proposed methods bring a significant solver runtime reduction of over 50% to the solver.

Q3: Runtime evaluations conducted with more modern solvers.

Thanks for the comment. We supplement runtime evaluation on Kissat SBVA-Cadical (the overall main-track winner of the 2023 SAT competition) solvers over the generated formulas as well as the original benchmarks in Tables 6 and 7 of the new revision. We set the runtime limit for Kissat at 5000 seconds, while for SBVA-Cadical, no runtime limit is imposed due to its slower execution on the Hard dataset. As seen, MixSAT performs consistently regarding the computational hardness across different solvers.

Q7: Experimental support for "MixSAT introduces some randomness to maintain computational hardness".

Note Table 2 illustrates the average solver runtime of all pairs across each instance. In our analysis, a tunable level of randomness is introduced to prevent hardness degradation caused by the interaction and conflicts of substructures. However, some deterministically generated formulas ($\lambda=0$) have already effectively maintained the hardness, surpassing the entirely random ones (due to inherent randomness). Consequently, the average solver runtime cannot effectively reflect the improvement of hardness led by introducing randomness.

To straightforwardly reiterate the effect of randomness on the computational hardness of generating formulas, below and also in Table 5 of the new revision presents the results on instance pairs where MixSAT exhibits some degree of hardness degradation. We gradually increased the $\lambda$ value to enhance the randomness. As seen, when the randomness increases, the hardness of the initially degraded pairs is recovered to a certain extent compared with the ground truth. Note although pair $e$-$f$ fails to maintain hardness on both deterministic ($\lambda=0$) and purely random generations, it gains some hardness when partial randomness is introduced ($\lambda=0.5$).

---

We hope this response could help address your concerns. We sincerely wish that you could reconsider the novel contribution and potential impact of our work on the community. We look forward to receiving your valuable feedback soon.

---

Reference:

[1] HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline. KDD 2023.

[2] G2SAT: Learning to Generate SAT Formulas. NeurIPS 2019.

[3] On the Performance of Deep Generative Models of Realistic SAT Instances. SAT 2022.

Q4: The performance of the proposed method depends on how we make a pair. However, the details of making pairs are not reported in the paper.

Firstly, it is essential to note that the core methodology of our approach centers around the design of the interpolation method, which is non-trivial when applied to graph structures, especially in the case of large-scale bipartite graphs with distinctive structures. In the paper, we elaborate on how we design the graph interpolation method to ensure consistency in generating data that aligns with the original distribution, in structural (through matching) and hardness (through matching with randomness) aspects.

On the other hand, of course pair selection method is an integral part of our methodology. The process of how we filter pairs has been detailed in Sec. 2.3 of the original paper, with the specific design outlined as follows:

We introduce an entropy-based filter to first select potentially valuable pairs for mixing (since the similarity of different pairs can vary much, not all pairs can yield quality matching results), which assesses and filters pairs using the row-wise entropy of the soft alignment matrix $\mathbf{S}\in\mathbb{R}^{n_1\times n_2}$: $h = -\sum_{i=0}^{n_1} \sum_{j=0}^{n_2}s'\_{ij}\log{s'\_{ij}} \quad \text{where} \quad s'\_{ij} = \frac{s\_{ij}}{\sum\_{k}s\_{ik}}$ which implies the sharpness of the soft alignment matrix between $G_1$ and $G_2$. A smaller value of $h$ denotes more distinct matching relations, leading to a potentially better pair for mixing.

Q5: The reason behind selecting these instances as datasets to make the evaluation fair.

When selecting instances to construct the dataset for evaluation, we consider the following factors:

1. It should include instances derived from real-world application scenarios to ensure the practical value of our experimental validation. Therefore, we choose instances from SAT competition benchmarks, which are encoded from real-world scenarios.

2. We aim to maintain an equal proportion of satisfiable and unsatisfiable instances in our data to verify the general applicability of MixSAT. Hence, we maintain a 1:1 ratio of sat to unsat instances in the dataset.

3. Recognizing the significance of computational hardness in experimental validation, we specifically select instances with higher computational hardness to constitute the Hard dataset.

Q6: Experimental support for "the proposed method is more efficient".

To demonstrate the efficiency advantage of MixSAT over previous state-of-the-art learning-based methods that generate from scratch, we compared G2SAT[2] with MixSAT ($\lambda=0.1, \tau=1.0$) for single instance generation, which is adopted as the standard training scheme in [3].

The pipelines consist of two processes: training and generating. The training process only needs to be performed once for a particular dataset, while the generating process can produce formulas repeatedly according to the target quantity. We measure the time for training and generating one specific formula. As shown below and also in Table 8 of the updated revision, MixSAT is significantly more efficient than G2SAT in both processes. Specifically, for the generating phase, MixSAT costs only approximately 1/2000 runtime compared to G2SAT.

We sincerely appreciate your prompt reply and the acknowledgment of our response. Below we respond to your new questions.

Q1: The new results in Table 3 are interesting. Could you please tell me more details about the experimental settings? How do you prepare training and test data?

We adhere closely to HardSATGEN's experimental settings of its solver tuning experiment. The data used for tuning the solver aligns with the datasets employed in previous experiments concerning graph structure (Sec. 3.2) and computational hardness (Sec. 3.3). The training set is consistent with previous experiments, specifically the HARD dataset. Trained models are then applied to generate new instances based on reference instances hard-a, hard-d, hard-f, and hard-g, which are selected from the HARD dataset with runtimes of less than 500 seconds. This selection is motivated by the very time-intensive nature of hyperparameter optimization, involving testing all augmented instances with 200 sets of hyperparameters. Opting for instances with shorter runtimes, such as the aforementioned four, helps mitigate experiment overhead. The reference instances collectively form the test data. The underlying expectation is that the augmented data could effectively guide the solver to enhance its performance on the original data.

Q2: Table 8 shows a significant improvement over G2SAT. Why do you compare with G2SAT? What happens if we compare MixSAT with other baselines?

Previous learning-based methods, such as G2SAT, GCN2S, and HardSATGEN, share a common foundation built on the node merge-split framework brought out by G2SAT, employing the same main generation process involving a sequence of node-merging operations (differing mainly in the use of differently trained networks to select the node pairs for merging). Consequently, the runtime results of G2SAT serve as the representative for these approaches operating within the same paradigm. The remaining baselines under the split-merge paradigm show no significant difference in terms of time efficiency compared to G2SAT.

Given that the efficiency comparison primarily centers around learning-based methods, traditional hand-crafted methods are not included in Table 8. However, we can still provide discussions of these methods in this response below:

Traditional generative methods including CA and PS can generate instances within mere seconds and require no training. They are more efficient than MixSAT. However, since the paradigm of these methods basically follows the pipeline of first identifying one or two structural metrics and then specifying an algorithm capable of controlling these metrics, these models fail to unravel specific data characteristics adaptively, merely matching partial structural metrics through manual control, as discussed in G2SAT and HardSATGEN. This can also be evidenced by Tables 1-3.

---

We hope this response could help address your concerns, and look forward to receiving your feedback soon.

We sincerely appreciate your valuable engagement and the time you dedicated to reviewing our work. However, we may hold differing opinions on certain points you raised. Below we respond to your concerns.

The experimental results on runtime evaluation (Table 2) are not strong. This result mismatches with the claim described in the introduction. In the introduction, the proposed method is said to achieve hardness reproducing and structure resemblance.

We admit that Table 2's results are not strong. But as we noted before, the resemblance in computational properties is very challenging (as listed as one of the ten key challenges in propositional reasoning and search [1]), and in fact MixSAT's results have already been the best among all other hand-crafted methods and learning-based methods with general applicability. Please note again HardSATGEN is a tailored method for UNSAT instances, whose success is at the cost of its ability to learn from SAT instances. Moreover, we respectfully believe underperforming one baseline under a specific task for partial data should not directly lead to rejection. We have revised the expression "achieve hardness reproducing" in the introduction to "achieve better hardness resemblance" to more accurately align with the observed empirical results.

[1] Ten challenges in propositional reasoning and search. IJCAI 1997.

The proposed method is evaluated with a few instances whose selection procedure (Appendix D) seems somewhat subjective. From the information described in Appendix D, I cannot judge whether the selection process of instances is fair or not.

We assert that the principles outlined in Appendix D are devoid of any subjective bias. We never cherry-picked the instances with the aim of maximizing MixSAT's performance. We are in the process of organizing our code and plan to upload it before the rebuttal deadline to ease your concerns. The rationale behind the three rules of selection in Appendix D is as follows:

1. The objective is to augment real-world SAT data to solve the data bottleneck in real-world scenarios, it is natural to select real-world data rather than random instances.

2. To test the applicability generality of the methods (i.e. performance on SAT and UNSAT sources), we select an equal number of SAT and UNSAT instances to compose the datasets. This is natural to approximate real-world application data that encompasses both SAT and UNSAT instances (otherwise we may not need a SAT solver to decide instances' satisfiability).

3. The imposition of a hardness requirement serves to guarantee the verifiability of the solver runtime experiment. We initially selected the dataset of G2SAT to evaluate our methods, but we observed that most of its instances could be solved in nearly 0 seconds, which made the solver runtime comparison meaningless. Thus, for solver runtime evaluation, we select hard instances from G2SAT and supplement additional instances from SAT competition to form the Hard dataset. While the instances in the Easy dataset are all from G2SAT.

We consider these selections to be fundamental and intuitive requirements. If you are still confused about some of the specific selection rules, please let us know.

However, I think the experimental settings explained by the authors are not convincing since they use instances augmented from hard-[adfg] for tuning parameters and evaluate the performance of the tuned models using the original hard-[adfg] as the test data.

This design is out of the consideration that the objective is to augment SAT instances that follow the original data distribution, thereby solving the data bottleneck. Please kindly note that this is not a training-testing paradigm, but rather a reference-augmentation paradigm similar to Tables 1 and 2 for structure and hardness resemblance evaluation. The performance of the solver tuned on instances augmented from hard-[adfg] and tested on the original hard-[adfg] instances shows the higher-level resemblance of the generated instances to the reference instances (obeying the same underlying distribution), such that the augmented data could effectively guide the solver to enhance its performance on the original data sources. This achievement is non-trivial, as can be evidenced by the failures of all previous methods in this setting including HardSATGEN. Please also note that this experimental setting exactly follows the solver tuning results in HardSATGEN.

---

We hope this response could help address your remaining concerns. We believe our work could contribute to the community as a novel framework for SAT instance generation, distinct from previous methods adhering to the split-merge framework. We sincerely wish that you could reconsider the methodology novelty, efficiency superiority, and general empirical superiority on structure and hardness, as well as the potential impact of our work on the community. We look forward to receiving your feedback soon.

Thank you for your timely reply and your valuable engagement in this tight rebuttal window, which helps a lot for us to refine our paper.

Since these rules would not be enough to identify the hard instances used in experiments from SATLIB and SAT 2021, I think that there are some implicit rules in the selection procedure.

Indeed, our instances are originally sourced from G2SAT, a dataset derived from SATLIB and SAT 2021. The Easy dataset is directly from G2SAT. The Easy dataset directly originates from G2SAT. However, given the scarcity of challenging instances in G2SAT (only 4 hard instances), we have supplemented the remaining 4 instances from SAT 2021, ensuring they share similar problem scales with G2SAT instances. The underlying implicit rule may be that current graph network based methods may not be able to scale to very large graphs (SAT 2021 often contains problems with 10k variables and 100k clauses). While also, our affinity matrix construction is somehow resource-consuming, thus MixSAT still cannot exceed the scale limit of current learning-based methods. Thanks again for noting, we are sorry that we omitted this underlying scale requirement, we will supplement this in Appendix D. On the other hand, we have uploaded our code to https://anonymous.4open.science/r/MixSAT/, which can be evaluated by any data to prove MixSAT's performance.

I also agree that the results of the hyperparameter tuning task are non-trivial. However, these results do not show that the proposed method can be used to solve the data scarcity problem described in the introduction.

The ultimate objective of SAT instance generation is to generate instances that resemble the original data, regarding structure and hardness. As guided in Ten challenges in propositional reasoning and search (IJCAI 1997):

"CHALLENGE 10: Develop a generator for problem instances that have computational properties that are more similar to real-world instances."

We believe the requirement of the resemblance between the generated and original data is sufficient to resolve the data scarcity problem. After all, that is the whole point of SAT instance generation methods in the first place. Our newly supplemented solver tuning results can support this data resemblance on a higher level, which surpasses all other baselines. From the application perspective, we admit it should better follow the training-testing paradigm, while our current solver tuning results may not be supportive enough for this point. In your initial review, you mentioned HardSATGEN as an example for the hyperparameter tuning experiments. It is per your request to follow its setting and supplement the new results to show the superiority of MixSAT. We believe the new results are still meaningful and can strengthen our paper as evidence for a higher level of resemblance between the generated and original data. Please also note that previous baselines are all ineffective for the current solver tuning setting, let alone the solver tuning performance for application purposes. We will continue to make efforts to another version of solver tuning results, but since the discussion window is closing, we wonder whether our efforts in the rebuttal period have met your requests and addressed most of your concerns, we would sincerely appreciate it if you could reconsider the current overall paper contribution and the massive new results supplemented in this very tight rebuttal window to strengthen our paper.

Thanks again for your interest and dedicated efforts in reviewing our work. We truly appreciate that and look forward to receiving your feedback soon.

Q2: Experimental results on hardness seem weak.

Although MixSAT performs weaker than HardSATGEN [1] on unsat instances, it outperforms other methods. Please note that reproducing computational hardness in the SAT instance generation task is considerably challenging which has not been achieved until [1]. Its success stems from its fine-grained control over the instance structure, particularly for the unsatisfiable core structures, as well as the postprocessing design involved to maintain the dominant effect of the unsat core structure.

While the design in [1] is effective, it confines the method to unsatisfiable instances only. Since real-world datasets generally incorporate both satisfiable and unsatisfiable instances, merely learning from the unsat instances can lead to certain negative impacts on downstream tasks like hyperparameter tuning, as evidenced by Table 3 in the current revision. In contrast, MixSAT surpasses this limitation, demonstrating generality to both satisfiable and unsatisfiable instances. MixSAT is also free from the node merge-split framework of previous learning-based methods [1-3], naturally meeting the hardness analysis and requirements set forth in [1]. Notably, our performance on satisfiable instances is significantly superior to all other methods.

We acknowledge that our effectiveness on unsatisfiable instances is not as strong, especially considering [1] already provides a tailored solution for unsatisfiable problems. However, we believe the two methods can complement each other. As evidence, we have supplemented the study with hyperparameter optimization experiments and present the combined effects of both methods in Table 3, which shows the significant effectiveness of our methods in practice as a boosting tool complementary to HardSATGEN.

Q3: Whether the formulas generated automatically exhibit the properties intrinsic to "industrial instances"?

The data we adopt in our experiments are exactly derived from real-world scenarios (from SAT Competition Benchmarks). Note the disparity between industrial data and real-world data can be viewed as minimal, as both originate from practical application scenarios. The experiments are designed to evaluate whether the generated instances exhibit the properties intrinsic to real-world instances. The evaluation for the real-world resemblance is two-fold: 1) structural properties compared to the reference real-world instances (Sec. 3.2); 2) computational properties compared to the reference real-world instances (Sec. 3.3). In the rebuttal period, we also supplement solver hyperparameter tuning results in Sec. 3.4, which indicates that the generated instances maintain close properties to the reference real-world instances so that hyperparameter tuning led by them could bring a significant solver runtime reduction of over 50% to the solver. The evaluation has already shown the effectiveness of MixSAT in generating instances that exhibit the properties intrinsic to real-world instances.

Q4: Minor issues and suggestions.

We sincerely appreciate your thorough review. We will revise the manuscript accordingly to elevate it into a more refined paper.

---

We hope this response could help address your concerns. We sincerely wish that you could reconsider the novel contribution and potential impact of our work on the community. We look forward to receiving your valuable feedback soon.

---

Reference:

[1] HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline. KDD 2023.

[2] G2SAT: Learning to Generate SAT Formulas. NeurIPS 2019.

[3] On the Performance of Deep Generative Models of Realistic SAT Instances. SAT 2022.

[4] Learning latent permutations with gumbel-sinkhorn networks. ICLR 2018.

Thanks for the valuable comments, and recognition of our presentation and novelty. Below we respond to your specific comments.

Q1: The rationale of the steps the approach performs.

Thanks for the note. We totally agree with your assertion that the rationale behind every effort of the methodology design should be articulated and elucidated in the paper.

We believe this principle should be a consensus across both the mainstream SAT research and the ML4SAT research. In fact, we try to make efforts to achieve such clarity in the original paper. Indeed, we acknowledge that certain points may not have been sufficiently clarified, leading to confusion. Here we would like to elucidate the underlying rationale for each design choice in our methodology. We hope this clarification addresses your concerns and fortifies the overall clarity of our work.

• Why mixing? Previous node split-merge framework for SAT instance generation exhibits poor performance in computational hardness resemblance. Though more fine-grained controls in [1] on structures can improve the performance, it also introduces applicability limitations. Thus we resort to a different graph interpolation approach that directly manipulates the raw structures of SAT instances in place, which is achieved by mixing substructures of SAT instances. This design is more efficient, more adaptive, and can naturally avoid the hardness degradation causes in the split-merge framework as analyzed in [1]. (Page 2)

• Why matching? The exchanged substructures should be matched such that the mixing process can largely preserve the original essential patterns and the mixed instances remain within the underlying distribution of reference instances regarding both structural similarity and computational hardness. (Page 3)

• Why adopt the neural SAT solving task as a pretraining task? It is for the sake of hardness-awareness. This pretraining task enables the model to not only capture the graph structure but also naturally discover the inherent properties regarding the computational hardness of the instances. (Page 4)

• Why perform online optimization with matching loss? The pretraining task guarantees plausible initial node features, but it is not directly related to the matching purpose. The online optimization with matching loss is to directly maximize the similarity between the node features of the two SAT instances. (Page 5)

• Why introduce randomness? Learning-based methods excel at identifying similarities within structures. With the replacement on top of the learned variable correspondence map, similar substructures from two reference graphs can easily interact and probably lead to conflicts and consequent hardness degradation. Thus, beyond the regular matching pipeline, a tunable level of randomness could avoid hardness degradation. (Page 5)

• Why use Gumbel trick to introduce randomness? Introducing randomness to assignments is non-trivial, while Gumbel trick on discrete assignment distributions is well studied in [4] with satisfying sampling property that $H(\mathbf{M}+\mathbf{\Gamma})\sim\mathcal{G.M.}(\mathbf{M})$, where $\mathbf{\Gamma}$ denotes a Gumbel noise matrix, $\mathcal{G.M.}(\mathbf{M})$ is the Gumbel-Matching distribution with parameter $\mathbf{M}$, and $H(\cdot)$ denotes the matching operator providing the best matching results, which can be achieved by the Hungarian algorithm for the linear matching case. (Page 5)

• Why this mixing algorithm? The mixing algorithm we propose in this paper is simple and natural. It directly utilizes the variable matching confidence obtained in the matching process, which increases the probability of replacing similar structures. We perform substitutions at the clause level because clauses are the smallest substructure of the SAT formula, thus they correspond to the smallest interpolation step in the interpolation scenario. (Page 6)

We have revised the manuscript accordingly to increase the presentation clarity of our paper. Please let us know if you have any other confusion regarding the approach rationale.

Q4: Is it possible to learn a binary classifier that accurately discriminates original vs. MixSAT instances?

Due to the limited data availability in specific SAT scenarios (which is also the motivation for designing generation algorithms), the current dataset size is insufficient to support the training of a classification network. In fact, we believe this situation is widely acknowledged in literature [1,2].

We understand your concern, as classification is a method to discern whether the generated distribution approximates the real one. Indeed, in our experiments, out of the same consideration, we have already validated the structural and hardness similarities between generated and real instances. Additionally, during the rebuttal period, we have highlighted MixSAT's superior performance in solver tuning. We believe these results sufficiently support the approximation of the distribution between the data generated by our method and real-world data.

Q5: What EDA stands for?

EDA stands for "Electronic Design Automation", a practical application scenario of SAT problem, where SAT instances exhibit scarcity. Sorry for the confusion and we have fixed it in the revision.

Q6: Pseudocode of MixSAT.

Thanks for the comment. We supplement the pseudocode in Appendix C to further enhance our methodology presentation clarity.

Q7: Minor issues and suggestions.

We sincerely appreciate your thorough review. We will revise the manuscript accordingly to elevate it into a more refined paper.

---

We hope this response could help ease your concern and wish to receive your further feedback soon.

---

Reference:

[1] HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline. KDD 2023.

[2] G2SAT: Learning to Generate SAT Formulas. NeurIPS 2019.

[3] On the Performance of Deep Generative Models of Realistic SAT Instances. SAT 2022.

[4] Locality in random SAT instances. IJCAI 2017.

Thanks for the valuable comments, nice suggestions, and for acknowledging the presentation clarity, methodology novelty, and technical soundness of our paper. Below we respond to your specific comments.

Q1: Besides structural properties and hardness, does MixSAT preserve the SAT/UNSAT ratio of the original data?

Thanks for the comment. The results of satisfiability phase preservation for generated formulas are presented below and also in Table 10 of the current revision. It is observed that despite being trained on a dataset with a one-to-one ratio of satisfiable to unsatisfiable instances, previous methods exhibit a tendency to generate a specific satisfiability phase. Notably, instances generated by G2SAT, GCN2S, and HardSATGEN are all unsatisfiable, while PS generates exclusively satisfiable instances. Among all the methods, MixSAT maintains the closest phase ratio to the original reference instances.

Unsatisfiable ratio of the generated instances:

Q2: What are the limitations of your approach?

Currently, the primary limitation of our approach lies in the fact that our hardness reproducing performance on unsatisfiable examples, though better than other methods, is not as effective as that achieved by HardSATGEN [1]. However, please note that reproducing computational hardness in the SAT instance generation task is considerably challenging which has not been achieved until [1]. Its success stems from its fine-grained control over the instance structure, particularly for the unsatisfiable core structures, as well as the postprocessing design involved to maintain the dominant effect of the unsat core structure.

While the design in [1] is effective, it confines the method to unsatisfiable instances only. Since real-world datasets generally incorporate both satisfiable and unsatisfiable instances, merely learning from the unsat instances can lead to certain negative impacts on downstream tasks like hyperparameter tuning, as evidenced by Table 3. In contrast, MixSAT surpasses this limitation, demonstrating generality to both satisfiable and unsatisfiable instances. MixSAT is also free from the node merge-split framework of previous learning-based methods [1-3], naturally meeting the hardness analysis and requirements set forth in [1]. Notably, our performance on satisfiable instances is significantly superior to all other methods.

On the other hand, we believe the two methods can complement each other. As evidence, we have supplemented the study with hyperparameter optimization experiments and present the combined effects of both methods in Table 3 of the current revision, which shows the significant effectiveness of our methods in practice as a boosting tool complementary to HardSATGEN.

Q3: Do you observe a degratation in performance when interpolating formulas generated by MixSAT?

To evaluate the effect of secondary interpolation on the performance of formulas generated by MixSAT, we select two representative instance pairs and apply MixSAT ($\lambda=0.1,\tau=1$) to obtain their 5% mixing ratio formulas. We then use these formulas as the start formulas and interpolate them with their corresponding goal formulas, resulting in 10% mixing ratio formulas. We compare these formulas with the original formulas, the 5% start formulas, and the 10% formulas obtained by one interpolation. The comparison is shown below and also in Table 9 of the current revision, where we can see that the secondary interpolation does not degrade the performance of the formulas, as they maintain the same level of hardness as the one-interpolated formulas. This demonstrates the robustness of MixSAT in generating hard formulas through interpolation.