MixSATGEN: Learning Graph Mixing for SAT Instance Generation
Authors: Xinyan Chen
Yang Li
Runzhong Wang
Junchi Yan
Venue: ICLR 2024 poster (2024)
Keywords: Combinatorial Optimization
Boolean Satisfiability Problem
Graph Generation
Graph Matching
Primary area: general machine learning (i.e., none of the above)

Abstract: The Boolean satisfiability problem (SAT) stands as a canonical NP-complete task. In particular, the scarcity of real-world SAT instances and their usefulness for tuning SAT solvers underscore the necessity for effective and efficient ways of hard instance generation, whereas existing methods either struggle to maintain plausible hardness or suffer from limited applicability. Different from the typical construction-based methods, this paper introduces an adaptive and efficient graph interpolation approach that in place modifies the raw structure of graph-represented SAT instance by replacing it with a counterpart from another instance. Specifically, it involves a two-stage matching and mixing pipeline. The matching aims to find a correspondence map of literal nodes from two instance graphs via learned features from a matching network; while the mixing stage involves iteratively exchanging clause pairs with the highest correspondence scores until a specified replacement ratio is achieved. We further show that under our matching-mixing framework, moderate randomness can avoid hardness degradation of instances by introducing Gumbel noise. Experimental results show the superiority of our method with both resemblance in structure and hardness, and general applicability.

Published as a conference paper at ICLR 2024
MIXSATGEN, LEARNING GRAPH MIXING FOR SAT INSTANCE GENERATION
Xinyan Chen Yang Li Runzhong Wang's Junchi Yan"
Department of Computer Science and Engineering & 2Zhiyuan College Shanghai Jiao Tong University
(moss_chen, yanglily, runzhong. wang, yan junchi (asjtu. edu. https://github: com/ http/hhhinkab-bbee SwTO/MiMTe... XSATGEN
ABSTRACT
The Boolean satisfiability problem (SAT) stands as a canonical No-complete task. In particular, the scarcity of real-world SAT instances and their usefulness for tuning SAT solvers underscore the necessity for effective and efficient ways of hard instance generation, whereas existing methods either struggle to maintain plausible hardness or suffer from limited applicability. Different from the typical construction-oon methods, this paper introduces an adaptive and efficient graph interpolation approach that in place modifies the raw structure of graph-represented SAT instance by replacing it with a counterpart from another instance. Specifically, it involves two-stage matching and mixing pipeline. The matching aims to find a correspondence map literal nodes from two instance graphs via learned features from a matching network; while the mixing stage involves iteratively exchanging clause pairs with the highest correspondence scores until a specified replacement ratio is achieved. We further show that under moderate randomness can avoid hardness degradation of instances by introducing Gumbel noise. Experimental results show the superiority of our method with both resemblance in structure and hardness, and general applicability.
matching-mixinn
framework,
INTRODUCTION
Combinatorial problems are fundamental in computer science and operation research, encompassing wide range of problems prevalent in real-world applications (Bengio et al., 2021; Li et al., 2023b; Geng al., 2023; et al., 2024). Within this realm, the Boolean Satisfiability Problem (SAT) (Guo et al., 2023) holds special significance for its versatile representational capability, which determines whether there exists an assignment general is NP-hard. SAT has served widespread practical applications, ranging from planning (Kautz et al., 1992), verification (Clarke et al., 2001), to cryptography (Soos et al., 2009). A recent line of research has witnessed the integration of machine learning methods into SAT solving in data-driven paradigm (Guo et al., 2023), either as promotive components for heuristics (Selsam & Bjørner, 2019; Li et al., 2022a) in end-to-end manner (Selsam et al., 2019; Amizadeh et al., 2018). In these methods, bipartite graph-based representation, c.g. literal-clause graph (LCG) (Biere et al., 2009), for SAT instances have been widely adopted which provides an explicit way of generating SAT instances via graph learning techniques in addition with certain heuristics (You et al., 2019; Li et al., 2023a).
Boolean variables that satisfies a Boolean formula and in
Both model training for modern learning baased based SAT solvers and hyperparameter tuning for traditional solvers require relevant instances to either tune the trainable model parameters or the hyperparameters. Unfortunately, SAT instances are often scarce in practice (Li al., 2023a; Giráldez-Cri & Levy, 2017). Hence extensive efforts have been recently made to generate quality instances. Compared to hand- crafted methods (Giráldez-Cru & Levy, 2017; 2015), learning- baasidg--bscdd methods (Li et al., 2023a; You al., 2019; Garzón al., 2022) show the promise of automatically discerning patterns from specific data, unveiling the underlying structural priors. However, the difficulty of these works often lies in how to resemble the hardness of the given (real) instances reference. For instance, a generation
"Correppondence author. t denotes equal contribution. This work was in part supported by NSFC (92370201, 62222607) and SITU Trans-med Awards Research (STAR) 20210106.

---

Published as a conference paper at ICLR 2024
Lined
Liural
CINN
-00
(1
(xt MRM
(19-2V
(xbi -30
Usaal Nade Feature
Literal Genooeendooe Nep
Refesnne Antazer
Eschnas and with Conernted Ineareo catbile cormppodoee
Libea
Grapps Matchhing
Laerl Cluso
Cause
Graph Mixing
CMN Modiile
Vartalla Commppandanne
2VV2331
(2V-22--344
(LV-2V -31
[1
(3/93)
Litenal Stake Fattanos
Vanable
Figure I: Methodology overview. Given a pair of bipartite graph-represented SAT instances, the matching stage predicts the correspondences of literals and variables. In the mixing stage, clause pairs are iteratively exchanged based on the mapping until specified replacement ratio is achieved.
model trained on reference benchmarks that need hundreds of seconds solve often generates trivial instances that can be solved in mere seconds. One notable recent progress to maintain the hardness refers to HardSATGEN (Li et al., 2023a) which proposes a multi-stage split-merge process to mimic the hardness via both learning scheme as well as heuristics in terms of logical substructures within SAT instances. The introduced heuristics may not arbitrary datasets and moreover, the method requires unsatisfiable reference instances which may not be available in some real-world datasets.
To overcome the challenges of previous construction methods, resort to graph mixing (interpolation) that directly manipulates the raw structures of SAT instances in place. The resulting advantages as will also be detailed later in this paper are twofold: 1) more efficient as we do not need to generate the instance from scratch; 2) more adaptive with less human heuristics as the mixing process could be performed in coherent optimization paradigm. We aim discover the potential shortest editing path (Abu-Aisee Abshhh et al., 2015) from one graph instance to another and then output along this path as the generation results, as shown in Fig. 2. It provides general and conceptually simple solution to achieve better hardness and structure resemblance, which also allows the absence of unsatisfiable instances in reference training data. The key idea is to replace certain substructures of graph-represented SAT instances from one instance with substructures from another, and the instances are both from the reference benchmark.
Lioaal
Libeaa
I
Inabaanc
Graph Distribution
Figure 2: MiXSATGEN interpolates reference instances along graph edit paths within the underlying distribu- tion to generate new instances.
Li et al. (2023a) shows that for the split-merge framework, employing similar strategies alongside similar initial structures can result in generated instances possessing similar substructures, leading to a degradation in difficulty. We posit that the same issue may be prevalent among various learning- based methods. Specifically, learning-baa based methods excel at identifying similarities within structures and often employ consistent learned strategies for generation. This frequently incurs the contenance of similar structures, which in turn, can easily lead to conflicts due to their close correlation, and sub- sequently the emergence of small unsatisfiable cores that cause hardness degradation. Based on this analysis, we argue that moderate randommess could help computational hardness maintenance for in- stance generation. This idea supported in Table by replacing certain substructures in one instance using that of another instance, random graph-level mixups of SAT instances with unified variable correspondence map between two instances, can possibly retain or even elevate the solving difficulty.
Beyond random mixup between two SAT instances, we further consider learning to mix up the certain substructure given two reference instances for better structural properties preservation. The scheme of exchanging the substructures is designed by the considerations: 1) all the variables and therefore the substructures need to be matched between two instances; 2) the exchanged substructure can largely preserve the original essential patterns and the mixed instances remain within the underlying distribution of reference instances. To achieve such properties, we propose a two-stage matching and mixing pipeline dubbed MiXSATGEN way of graph interpolation for generation as presented in
2

---

Published as a conference paper at ICLR 2024
Fig. 1. The matching employs the inner products between literal node features to obtain the similarity matrix, which is subsequently post-processed using the Gumbel-Sinkhonl algorithm (Mena et al., 2018), to establish stochastic correspondence map between the literals of two reference instances. The Gumbel noise (Jang et al., 2016) is to incorporate a controllable level of randomness to modulate the matching outcomes, avoiding the hardness degradation issue. The features are extracted by graph networks pretrained in SAT solving tasks and subsequently online optimized by the graph matching loss. The extracted node embeddings reduce the problem into linear assignment task as solved via the Hungarian method (Kuhn, 1955), which is then enforced on the correspondence map obtain a specific assignment of the literal nodes. In the mixing stage, clause pairs with the highest correspondence scores are iteratively exchanged until a specified replacement ratio is achieved. Experiments show MiXSATGEN's comparative performance for structure and hardness resemblance as well as general applicability.
2 RELATED WORK
SAT Generators. Different from mainstream generative models (Ho et al., 2020; Li et al., 2022b; 2023c; Zhang et al., 2024b), SAT instance generation requires strong domain knowledge, and can be categorized into hand-crafted and learning-based methods. Hand-crafted methods (Giráldez-Cru & Levy, 2015; 2017) usually involve one or two structural metrics and devise algorithms to manipulate these metrics w.r.t. reference. In general, hand-crafted generators fail adaptively unravel specific data characteristics, merely matching partial metrics. In contrast, learning- matically capture global graph structures during training. G2SAT (You et al., 2019) and its follow-up GCN2S (Gazzón et al., 2022) represent SAT instances as bipartite LCGs and develops one-stage node split-merge framework for bipartite graph generation. Unfortunately, these works are not yet able to produce non-trivial hard instances and only generate instances that can be solved in seconds. To resolve this issue, HardSATGEN (Li al., 2023a) takes the key substructures of real-worls SAT instances c.g. the community structure and the unsatisfiable cores into consideration, and introduces a fine-grained control mechanism to mimic the hardness the reference benchmark. One possible drawback is that it requires unsatisfiable instances for reference and relies human intervention for post-prows post-processing. In parallel with boolean satisfiability, LinSATNee (Wang et al., 2023b) also studies the generative process that enforces linear satisfiability the output of neural networks, and similar tearning-based generators are also studied in other combinatorial problems (Geng et al., 2024).
generators auto-
Graph Matching. As a building block in our framework, we are particularly in favour of deep graph matching (Yan et al., 2020) which mainly follow two ways: 1) The quadratic methods where both node and edge affinities are explicitly modeled (Wang al., 2021a; 2023a; Liu et al., 2022a; 2023; Lu et al., 2024); 2) The linear methods where node features embed the edge features, resulting in a linear matching problem (Yu et al., 2020; Wang al., 2019; 2020; Jiang et al., 2022). We resort to the latter paradigm for its scalability.
Graph Mixup. Mixup methods (Zhang et al., 2022; Liu et al., 2022b) have been proposed for graph data augmentation. Despite methods like Wang et al. (2021b) that interpolate latent representations of graph pairs, most methods manipulate the raw graph structures. Yoo et al. (2022); Park al. (2022) combine random subgraphs and specially selected subgraphs from different graphs to generate new graphs, respectively. (Guo & Mao, 2021; Ling et al., 2023) linearly interpolates continuous- valued adjacency matrices and feature matrices for augmentation, based correspondence map, respectively. Yet such mixup operations require continuous adjacency matrices and structures, which do not apply to SAT with discrete structures and varying- sized instances.
arbitrary node-level
METHODOLOGY
Training
233 Cldlo Masding
The flow diagram of our approach as well as the section organization are presented in Fig. 3.
23 Nacter Modid Premtinng
131 lond
tekoppdaee Replioennt
Compandie
Clise
3.1 PRELIMINARIES AND FORMULATION
SAT and its Graph Representation. SAT is to deter- mine the existence of a valid Boolean assignment for a Boolean formula. These formulas are constructed using Boolean variables linked by logical operators
Milking Yanalde
224 Kaskaa dedioee
Sanddag
Generating
Figure 3: Flow diagram of our methodology.
3

---

Published as a conference paper at ICLR 2024
like conjunction (A), disjunction (V), and negation (-). Typically, Boolean expressions cast exprrees
in the Conjunctive Normal Form (CNF) (Tseitin, 1983) of a conjunction of clauses. Each clause represents disjunction of literals, where literal can signify either a variable its negation. The graph representation of SAT' compromises four basic forms (Biere et al., 2009): literal-clause graph (LCG), literal-inidence graph (LIG), variable-clause graph (VCG), and variable-incidence graph (VIG). This paper adopts LCG, which is a bipartite graph with two sets of nodes: literals and clauses. Edges within this representation signify the presence of given literal within a specific clause
In particular, this paper primarily adopts the LCG representation of SAT instances for its bijective nature to raw SAT instances. A bipartite LCG is formulated as G = (V, E) where V Via Va and & S {(v). u, E Via, 1/ E Val. An LCG with n literals and m clauses maintains Via = (I,... . and Va- = (c (c..... ................................ Cm.) Here Via and Vaa denotes the literal nodes and clause nodes, respectively. The edges can only connect literal nodes and clause nodes for the occurrence of the literal in the clause. LCG also has an equivalent representation known as Weighted VCG (WVCG). Its graph form is simplified as VCG with the negation between variables and clauses encoded into the weighted edges, where values of and - represent positive and negative literals, respectively.
Graph Matching Objective. Graph Matching (GM) computes the node-level assignment among two or multiple graphs based on the graph structures, which is optimal in some sense. two-graph matching can be modeled as the Quadratic Assignment Problem (QAP), with its most general form Lawler's s QAP (Leordeanu & Hehert, 2005; Yan et al., 2020) formulated as:
max(xx Kx), X1, Lais
X I,, S 1m2: X {0, (0,1) x
where vee(X) is column-wise vectorized X E {0, 1) x which denotes the assignment matrix. Here K E Rg denotes the affinity matrix, where the diagonal elements indicate the node-to-node similarity and the off-diagonal elements carry the edge-to-edge similarity. The objective x Kx quantifies the similarity between nodes and edges, for maximization.
3.2 MATCHING: VARIABLE ALIGNMENT VIA GRAPH MATCHING
3.2.1 FEATURE EXTRACTION AND MODEL PRETRAINING
Real-world SAT instances are often large in size, e.g. with thousands of nodes a single LCG, which is out of the capacity of existing graph matching methods. We resort to utilizing graph networks to embed the edge information and the clause node features into the literal node features, thereby reducing the quadratic matching problem over the entire graph pairs to linear one over literal nodes.
Following the classic NeuroSAT (Selsam et al., 2019), the graph network learns the embeddings for the literal and clause nodes through a k-round message passing scheme, which formulated as:
LSTM.
MLP,
(b(* (h(*t11) 11
LSTM:
Σ (eCAVO
MLP. (b) .nf" fff=-11 9
(2)
where A((-) denotes the neighboring node set, and hn(*) and h.aa) denote the k-th layer literal and clause embeddings, respectively. MLP, and MLP, denote two multi-layer perceptions for clauses and literals, and LSTM, and LSTM, denote the layer-norm LSTMs (Hochreiter & Schmidhuber, 1997).
we pretrain the graph networks with a SAT solving task which predicts the binary label of each variable for a satisfying assignment. It enables the model to not only capture the graph structure but also naturally discover the inherent properties regarding the hardness. Denoting (+) as the Sigmoid function, the binary prediction of each variable is produced by a learned MIP, with the last-layer embeddings of each pair of literals h,(") and (N) as the input:
For
yo = a (MLP
[M. (N) (N)) (N09)) [)
(3)
The unsupervised training objective follows Ozolins et al. (2022) that differentially maximizes the satisfiability of SAT instance & over predicted soft assignment x E [0, 1]", formulated as:
= Σ log 1 - (-x)
(4)
C
SEct
TEe
where e and c denote the positive and negative-form variable sets. The model design and the pretraining task are specified among selections in the benchmarking work G4SATBench (Li et al., 2023d) as the most efficient ones in our proposed pipeline. The extracted literal node feature matrix is denoted as H Ra which is concatenated by n d-dimensional literal node feature vectors.
4

---

Published as a conference paper at ICLR 2024
3.2.2 VARIABLE-LEVEL CORRESPONDENCE COMPUTATION
Given an LCG pair G1. G2 with 2n,, 2nz literals (7), n2 variables) as well as their literal features H1, H2, the similarity between the two literal sets M, E [0, 1] can be obtained by inner- product M, = H, H The graph structural information is already encoded in H1, H2 by graph networks. The variable similarity can be obtained from the literal similarity considering the two literal matching forms regarding the literal phases. For example, when matching variable and j. the two forms for literal matching include {(.. (-1,, and {(4,-1y) -ly: 22), Denoting x the variable similarity matrix as M. [0. 1]m,xx,, the similarity between variables can be set by aggregating the scores of literal pairs within each matching form and selecting the maximum value:
M. = max (M + M -ly), M, -,,] + [M(,),)))
(5)
Based on the obtained variable similarity matrix M,, we aim to achieve an alignment X {0, 1 1)m X between the two graphs that satisfies the stochastic constraint, formulated as:
E
X1p2 Lais X 1n S 1
(6)
The Hungarian linear assignment solver (Kuhn, 1955) can effectively achieve such solution satisfy- ing the stochastic constraint in polynomial time, where the linear assignment problem is formulated as:
max tr X
[X T M.,)
s.l. X (0,1)"xx7,
XI, = In
X 1
1
(7)
where X denotes the discrete assignment matrix. To enable differentiability for further online optimization as presented in Sec. 3.2.3, we resort to the differentiable and approximate version of Hungarian, i.e. the Sinkhorn algorithm (Sinkhorn & Knopp, 1967), for a relaxed projection from the positive matrix to a stochastic matrix S E [0, 1mm1x== by alternativeyy normalizing its rows and columns. The gap between Sinkhorn and Hungarian can be controlled with Sinkhorn's 's hyperparameter т. A smaller results sharper output that closely approximates the discrete assignment matrix, but it leads more required iterations. Conversely, larger has the opposite effect. In our pipeline,
S Sinkhorn (M,) s.t. S1,, = 1 1n, S 1ng E
[0, 1 x
(8)
serves as the node-level matching result for further online optimization. While a discrete assignment matrix for generation can still be efficiently computed through the Hungarian algorithm over S.
3.2.3 ONLINE MATCHING OPTIMIZATION
For the matching purpose, the model pretrained with the solving task is subsequently online optimized for each specific instance pair to maximize the similarity between the node features and between the edge features. The optimization objective follows the classic modeling of the graph matching problem as Lawler's QAP (Leordeanu & Hebert, 2005) and replaces the discrete assignment matrix X E {0, 1 with the relaxed soft assignment matrix S E [0, 1Jmh x=2 to enable differentiability:
((s) - Ks
Here vec(S) is the column-wise vectorized version of matrix S, and S is the soft assignment matrix derived from Eq. (8). K E R Xmin2 denotes the affinity matrix, which contains the explicit affinity scores between node pairs and edge pairs. Minimizing J(s) requires finding the optimal assignment matrix s which maximizes the matching similarity of the two graphs.
3.2.4 RANDOMNESS INCORPORATION WITH GUMBEL-SINKIONN
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, we introduce tunable level of randomness to the matching results avoid hardness degradation through Gumbel-Sinkhorn (Mena et al., 2018).
The Gumbel trick is known for its property to recast a difficult sampling problem as an maximiza- tion operation (Balog et al., 2017). Introducing randomness to assignments is non-trivial, while Gumbel trick on discrete assignment distributions well studied in (Mena et al., 2018) with the following satisfying sampling property. For random assignment P following the Stubbel-Matchne distribution (Mena et al., 2018) with parameter M, i.. P ~ G.M. it can be verified that H(M + r) G.M. where I denotes Gumbel noise matrix. Here M can be viewed as the
5

---

Published as a conference paper at ICLR 2024
Literal
Literal
Literal
Literal
Literal
Clause
Clause
Clause
Clause
Clause
Cai
SAN
CAA
6aj
(a) Global confidence for every elause G,
(o) Local confidence for related clauses in
(c) Global Gioball confidence for remaiined clauses in
[d] Clause Replacement for Graph misup
Figure 4: Single clause replacement iteration. Node color indicates confidence, line color indicates literal phases and weighted edges, and the dotted node signifies an outlier. (a): the clause for replacing in Gi is determined based on global confidence. (b) and (c): tracking the most matching clause in G2 referring to the local and global confidence. (d): the two selected clauses are exchanged.
similarity matrix, and (-) denotes the matching operator providing the best matching results, which can be achieved by the Hungarian algorithm for the linear matching case.
To sample from the use the certain solution of the linear matching problem, we extend the correspondence computation process in Sec. 3.2.2 by replacing the raw Sinkhorn algorithm with the Gumbel-Sinkhorn in Eq. (8):
distribution G (M,)(MM)) with randomness rather than directly
S Sinkhorn ((Mg AT) /T)
(10)
where À denotes the factor controlling the noise intensity, and I controls the significance of parameter M the entire distribution. A larger diminishes the impact of the initial matrix and introduces increased randomness, and vice versa. Then H (M) can be viewed as samples from the assignment
distribution centered with the parameter M and variated with the randomness controlled by À and т.
3.3 MIXING: GRAPH INTERPOLATION VIA ITERATIVE CLAUSE REPLACEMENT
Since the similarity of different pairs can vary much, not all pairs can yield quality matching results. To this end, we introduce an entropy-basee based filter to first select potentially valuable pairs for mixing, which assesses and filters pairs using the row-wise entropy of the soft alignment matrix S R xma;
h =
s/g log s/y
where
Siy
(1I)
8tk
which implies the sharpness of the soft alignment matrix between G1 and G2. A smaller value of denotes more distinct matching relations, leading a potentially better pair for mixing.
Subsequently, given a selected LCG pair G1, G2 with 2n,, 2nz literals (a1, n2 variables) from the filter, well the discrete variable assignment matrix P obtained from the Hungarian algorithm, we proceed to perform iterative clause-level replacement for graph mixing. Based on the variable assignment, the literal assignment can be derived simply by ascertaining the matching of literal phases. This determination can be obtained by comparing (M, + [1 -bi) and (M, -1,] [1 -1,)) in Eq. (5), while the corresponding confidence of each matched literal pair can readily received from the relevant entry of the Sinkhorn output matrix S. Note that the two reference graphs often differ in size, which could result unmatched outlier nodes within the larger graph.
The mixing process in Fig. 4, commences with computing the global confidence for the clauses in G1- Each clause is assigned a confidence score derived as the sum of the confidences associated with its constituent variables. These confidence scores guide the ordering sequence in which clauses selected for replacement. Once e₁ in G1 is identified, its contained variables and their corresponding matches in G2 are traced to locate the group of clauses in G2 linked to the matching variables. A local confidence score is assigned to each related clause in G2, based on the sum of traced variables linked to it. By sorting the related clauses, we can select more refined group by excluding low-scoring clauses. Another global confidence is computed for the remaining group of clauses in G2, and the clause 02 with the highest score is determined for replacement. In the replacement stage, we remove all original edges associated with and inherit 's match-replaced variable connection. During replacement, if c2 contains an outlier variable that cannot be matched to any variable in G1. new variable is created in G, and the correspondence relation between the two variables is stored in the map. The clause-level mixing iterations continue until reaching the mixing ratio of clauses.

---

Published as a conference paper at ICLR 2024
4 EXPERIMENTS
4.1 EXPERIMENTAL SETUP
Datasets. The real-world SAT instances are collected from SATLIB benchmark library (Hoos & Stützle, 2000) and SAT Competition 2021 (Balyo et al., 2021). We separate the dataset into two categories, EASY and HARD, by the computational hardness, to assess the performance of MixSATGEN across varying levels of computational hardness. The instances preprocessed by removing duplicate clauses. As a result, the processed instances encompass variable counts ranging from 82 to 450 and clause counts spanning from 327 to 5424. Half of the selected instances, i.c. instances in the EASY dataset, exhibit low computational hardness, as they could be solved by CaDiCaL. (Fleury & Heisinger, 2020) in less than second. The remaining instances in the HARD dataset maintain& a substantial solving time regarding the same SAT solver. The precise solving times for each formula are provided reference in Table 2. Each dataset includes 4 satisfiable formulas (a-d) and 4 unsatisfiable formulas (e-h) to ensure balanced representation of satisfiability.
Baselines. We involve both hand-crafted generators and learning- based generators in our comparative analysis of MiXSATGEN. The sund-crafted generators include the Community Attachment (CA) model (Giráldez-Cru & Levy, 2015) and the ropularty--Similaiii (PS) model (Giráldez-Cru Levy, 2017). For learning-basse based SAT generators, we include G2SAT (You et al., 2019) and GCN2S (Garzón et al., 2022), both of which employ one-stage node split-merge framework with different network backbones. The more recently proposed HardSATGEN (Li et al., 2023a) is also compared, which employs an improved multi-stage split-merge pipeline, excelling in maintaining computational hardness, albeit limited to the unsatisfiable benchmark. A fully random mixing scheme is also established within MixSATGEN's ' framework based on random variable assignment maps.
MiXSATGEN Settings. We first finetune the pretrained model with 0.0001 learning rate, 200 epoches and 4 iterations of message passing (Selsam et al., 2019). For the filtering process mentioned in Sec.3.3, we select the top 3 pairs with the lowest row-wise entropy out of the pairings within the dataset for each instance. We set the mixing ratio at 5% in the main experiments. We adjust À to control the randomness level, while the temperature parameter 7 is set in main experiments. The graph matching methods are implemented through Pygmtools (Wang et al., 2024).
4.2 PERFORMANCE ON GRAPH STRUCTURES
The benchmarks originating from practical applications encode distinct problems with different structural distributions. The generated formulas are desired to exhibit similar structural properties to those in the training dataset. We follow the previous studies (Ansótegui et al., 2009; Newsham et al., 2014; You et al., 2019; Li et al., 2023a) to evaluate the structural properties by graph statistics. The metrics include modularity Newman & Girvan (2004) in VIG, VCG, LIG, LCG, averaging clustering coefficient Newman (2001) in VIG. Table shows that both hand-crafted methods achieve a certain level of similarity in some metrics; however, they fall short in capturing others. In contrast, the lcarning-based based methods exhibit more comprehensive emulation of the overall structure. Note that HardSATGEN excels in reconstruction for some metrics, particularly on the hard dataset. However, it is limited to unsatisfiable training instances, which limits its applicability. Since the other methods are aligned with the overall datasets, we do not directly compare HardSATGEN to them but merely present its statistics. The empirical results demonstrate MIXSATGEN'S competitive structural retention across most metrics. Furthermore, the variation trend highlights the effectiveness of Gumbel noise introduction, ranging MixSATGEN (A = 0) that signifies a completely deterministic matching to MiXSATGEN (random) with a completely random assignment. Generally, observe that the less randomness added to MiXSATGEN, the more precise it becomes in capturing structural properties.
4.3 PERFORMANCE ON MAINTAINING COMPUTATIONAL HARDNESS
As expected in the ten key challenges in propositional reasoning and search (Kautz et al., 1997). the generated formulas need to closely replicate the computational properties of the references. Following Li et al. (2023a), we employ the direct SAT solver runtime for assessing the hardness. We utilize CaDiCaL (Fleury & Heisinger, 2020) the test solver and leverage the runlim tool' to measure the solving time for each individual instance. The maximum solving time limitation for an instance is set 2,500 seconds. Given the potential significant variation in solving time
hhtp::// jkk. rrnlim/
7

---

Published as a conference paper at ICLR 2024
Table 1: Evaluation on graph structural properties. The relative errors are in brackets. Best resem- blance in bold. "HardSATGEN only compares to unsatisfiable reference instances.
Disrect
Metool
VIG
VCG
LIG
LOG
Clastriig
Modalaity
Modalasity
Midullsit
Modilarit
Reference
04
0.55-405
0:75:4005
0.08:111 19
Refermnce (UNSAT)
0.5119009
64922003
0.71:0008
0,54::002
0.64:0.07
CA (Ginlllee Cru Levy, 2015)
0,312000 36%6)
0.51=0000
8.3-21000 (16-58))
B.54=0008 (20,019))
0.5540004 (21 2513
(Cinlldox Lovs, 2017;
061100 12
0.05 10:0
(91 1111))
0.24.00011 (65-4255)
-001 (96. 186.19961
J666)
025AT (Yec cis..
0.82..0019
0.7210
(1.5%))
BASY
OCN2S (Carnln 20123
0.36:4017 (17.22%)
0.64-100 62%) 0.42:0005
0:661-004 (98)
9000-000 1
083-00 14 (6.4%)
HaNEATGEN (Li et al, 3023g)
0,4120 10 (20.354)
(12.94%)
0:03:0000 (11,59%)
0.54:00.04
(0.22) (0.22%)
0,1100 04 (5.2894)
MA 0)
IL06 (8.49%)
0.54 0.10
(0-12%)
0.84 (1.50%
MiXSATGEN 0.1,7 1)
0.00 (10.355)
0.00 (6/))
= (0.26))
(1.37993
2946)
(0000)2000)))
MisSATGEN ( - 1
0.40 1: 0.06 (14.55%)
0.53
0.00 (3.95%)
0.24 2: 0.03 (0066%)
0.7 L 0.15 (2,6966
0.68 a 0.04 c1 (256)
MiXSATGEN (randon)
0,35 0:11 (25.625)
0.53
= 0.00 (6.38)
0.73 s 0.1 (2,658)
0.64 = 0.14 06.3799
0.08 + 0.04 (1 (1.56))
Reforrece
04110:11
6:5910.18
0:34:0:11
0.67
0.72 0212
Reference (UNSAT)
0,760009
19
0.0040.114
0,020023
0.67=0115
CA (CinlloosCmm Lovy. 3015)
0:37:000 (12688
0.4--0 15 (796699)
0.56 EUt6 (706666)
00050. 8956)
PS (CanlitessC & Ley, 2017;
0:53-0 25 (37 1953
00K-114 (80 125)
125-D00000-557
B.12
0.06 (17 A806
(61-4755)
GISAT (Yos et... 20199
0,56200 20 (36718)
0.742111 (2698R)
0.1220.41 18.22))) 2642)
0.7-00.00 (201899)
07762002 (5-48%)
HARD
GCNIS (Carntn stal. 2013)
0.19
2st.:n.30:11.00 (445)
6.661..3 6890
ILT2 R:87 (UUBS)))
(4.68%)
(.80).0.20(28855)
MiSSATGEN
0 0,15 (4.9%%
0.55 a: 0.16 (6.54%)
0:54 0.13 (0.2%)
0.66 =: 1,6-0.0412.008
0.71 a 0. (0536))
MISSATGEN (A 0.1. 1)
6:39 0.15 18 (4.0%)
0.54 -0----00 (.16:1 78%3
0.24 + 0.1322 1993
0.05 - 14 5053
OUT 4 1.12 2456)
MIsKATGEN 0.3, 1)
18
9993
0.23 (1
B.6 (3.9999
1196) 0.70
MivSATGEN 12 1
0.35 (7.748)
56R)
(2.425)
Table 2: Solver runtime evaluation. Standard deviations are in brackets. Best resemblance in bold.
Mathol
Jany porrgg)
bonks
band4
hander
tand-i
Iued-e
bank-
hand-3
banf-k
Refermee
254.22
1382.71
1204-43
$52.85
3629:03
1502.04
CA (Olsidoo--ru & Lovy, 2015)
(50,01)
0.1
(50.00)
1=0000
0.01
(26000)
0.01
(50.00)
0.01
(20.00)
0.01
(2002)
0.55
(28.00)
0.01
(50.00)
0.01
PS (GedMMre-Cr& & Lavy, 2017)
(10.0))
00)
(10:13)
041
120.12
0.41
(10.00)
0.01
(10.00
(10.00)
0.01
(10.0)
0.01
(10.00)
0001
C10.00
GISAT 2019)
(5000)
(6000)
150000
(40.00)
(40.00)
(4000)
(50000
(50
OCNSS (Camnde 2007)
(3000)
001
(+1161 201
457.47
(=14005)
10213
(40000)
0,01
(5000)
0.01
(4010%)
0.51
(4010))
0,01
(A)
0.01
(40.00
5:01
HuASKTGEN at, 2023g)
N/A
NIA
NIA
2267.95
1038.15
MicSATCEN (A. =t)
0.1
(=122419)
(= (0)
355.70
(5120005)
S9N TH
(555 500
42.48
(4371)
4.75
(5001)
0,01
(2001)
0,03
(5001)
0.01
MiSSATGEN (1- 0.1.
(1124405)
S5.23
$37.9
001
0C1
MiSSATGEN (A - 05,7 1)
(S4011)
567.64
C- 487.20
476.23
C53057 41)
775.66
C650 14)
42.65
(-349.33
167.0
(4000)
D01
(41000)
(4000)
0.1
MiSSATGEN (A 1.0
(50.00)
00)
(1448.11)
308.77
(=344
413.85
(2:00.63)
200.40
C1933.00
65
(=10000
9.54
(10.00)
0.01
(50.00)
000
(20.00
061
MisSATGEN
(-0.41)
(-977.800
(-746-975)
(1889-31)
(16
(1000)
(4000)
(1000)
among different reference instances, we report results for each reference instance. Table shows the superiority of MiXSATGEN in generating promising hard instances meanwhile exhibiting general applicability. Almost all baselines experience a notable degradation regarding computational hardness. ATGNS excels in hardness maintenance, yet is limited for unsatisfiable benchmarks (Li et al., 2023a). The results of varying À show its impact on controlling the introduction of randomness. Increasing À tends to push the method towards a direction of complete randomness. However, due to the inherent variability introduced by randomness, not all examples conform precisely to this trend.
4.4 SOLVER HYPERPARAMETT TUNING BASED ON GENERATED INSTANCES.
SAT solvers with default hyperparameters perform well on general benchmarks. While in practice, with sufficient data in hand, SAT solvers can be further tuned for specific data sources. Table presents the hyperparameter tuning results on the SOTA solver Kissat (Fleury & Heisinger, 2020). We adopt a Bayesian optimizer HEBO fooven-Rivers et al., 2022) 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. The tuning range of these three hyperparameters are [1. lc2], [le2, 1c4], and [1, 2c2] respectively. For each method, reee]ctesspeiiii
the Bayesian optimizer trics 200 sets of hyperparameters and we select the top 5 hyperparameters to evaluate on test instances. The best runtime results presented in the table. Due to the costly Bayesian optimization process, we select instances with runtimes under 500 seconds for experiments. Note that in Table MixSATGEN reproduces computational hardness well on satisfiable instances, while HardS (Li et al., 2023a) can only learn from unsatisfiable instances. Table 3 shows the matched performance where MiXSATGEN and ATGES perform the best for satisfiable and unsatisfiable instances respectively. Thus, we also consider simultaneously adopting ATGEN 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.
8

---

Published as a conference paper at ICLR 2024
Table 3: Results of solver hyperparameter tuning for specific data. Tg: average solving runtime on generated instances; Te: average runtime on test instances; hhrd-: runtime of instance hard-i. Time is in seconds. Best performance for satisfiable, unsatisfiable, and overall data are marked in bold
Method
Hyperpannnteess
Average
Saiifable
Unsatistable
Ascegge
Thunky
Anczage
Defaii
1000, 50
NIA
190.96
155 60
254.14
204.55 87
$1.09
81.00)
$7.05
CA (GiiillaaCC& & Lesg, 2015)
(5, 8478, 33p
0.05
(-153 598)
354.66l fv
(+45.756)
54.12
(-327.45)
1036
(-185.7%)
505 10
(-09.053
55.3
(-35.39L)
112.08
(-47.29%
83.95
(Cinilaaoo Lecy, 2017)
3596, 16)
0.03
(-5888))
(676.766)
56.19
(:100:79)
460747
(-70.5%)
18
(66255)
(13,05)
75.56
(-16.9%)
G2SAT (You al, 2019)
(-906]
(106.15)
(-24.93)
GUNSS (Cuenin et A00ny
(18, 1555, 583
0.75
(-53.8%)
240.75
(-109.36)
325.62
(98.119)
(- (-102.59%)
414.47
(-56.45)
51.74
(-166%
(-17.5%)
HanSATTOEN (Lá 20134)
(2, 065 180
49.80
(-51 (P8)
197.72
(+8375))
25:35
[-101 316]
066 29
(-88 69)
545. 52
(+9,09))
30.12
(+13,488)
70.12
(+12.11)
50.12
MisSATGEN
(67, 2007 98)
11.22
(450
04.54
(+70.366
46.16
(+01 (09)
22.
(3..22))
(-100.95)
66.48
(-51.5%)
122.70
(458.88)
41.59
MicSATOEN HEGSATGEN
79.
(453.2%)
(-349%)
Table 4: Solver runtime with varying mixing ratio. Table 5: Solver runtime with varying randomness.
Raio
Midied
pare-o
pario
pards
porrarc
palned
par
patre-
4400
25.72:22
13811221888
199 03983330100
254.22
1383.71
357.85
2629 033
1106 676880000000
145 244796
31%
1003 51:4.5
10.50-331 31
02244.56 56
0.2042001
138.1::18455
199003
35 55.9041000
11
21.14:0044
122-72412555
300112:4.00
MuSSCUREN
1M5-7229-00
BAISI0E
02
0.113014
3,591006
442.113355
188.95.18..0 49
21.4212.41
39:1--991
S2185-255.5
13801881884.88 36
MISLATCEN
15
9.3031500
0.310.00
0:238.30
218 (5812222
111644211201.99
195
11.4929.12
4.5 ABLATION STUDY
Mixing Ratio. Due to the large mixing ratio and different example features, it is more meaningful to analyze a single sample than mean performance. We select four of the most representative instance pairs on the HARD dataset for display. Table 4 shows the runtime variations during the replacement ratio increment for the selected instance pairs. MiXSATGEN is evaluated under the setting of = 0.1, r 1, with a comparison to that of a completely random setting. For pairs b-a where MiXSATGEN outperforms the random setting, the assignment matrix obtained is quite sharp with certainty, resulting in promising hardness maintenance when the replacement ratio increases. While for pairs a-d, b-d and d-c where the random setting surpasses MiXSATGEN, the random side experiences some degradation, yet still maintains a plausible difficulty level at 25% replacement ratio. This provides opportunity to enhance the difficulty generated by MiXSATGEN at the same ratio, as the random setting introduces more computational hardness compared to MixSATGEN.
Randomness. Note Table 2 presents the average solver runtime of all pairs for each instance. However, as the hardness of some deterministic generated formulas (A = 0) is better maintained than that of the completely random ones, the average solver runtime cannot effectively reflect the improvement of hardness led by introducing randomness. Table presents the results on instance pairs where MiXSATGEN exhibits some degree of hardness degradation to straightforwardly reiterate the effect of randomness on the computational hardness of generating formulas. We gradually increases the À value to enhance the randomness. As seen, when the randomness increases, the hardness of the initially degraded pairs is recovered to certain extent compared with the reference. Note although pair e-f fails to maintain hardness on both deterministic (A = 0) and purely random formulas, gains an amount of hardness when partial randomness is introduced (A 0.5).
5 CONCLUSION AND OUTLOOK
This paper presents an interpolation-basse matching and mixing approach namely MiXSATGEN that modifies the raw structure of graph-repeesented SAT instances by exchanging their substructures. The matching process efficiently provides the informative node-level correspondence for subsequent substructure mixing. Then we introduce controlled randomness via Gumbel noise to the matching matrices to prevent hardness degradation. MiXSATGEN less relies on heuristics and human interven- tions, compared with HardS (Li et al., 2023a) and can handle satisfiable benchmarks that HardSATGEN cannot learn from. Empirical results show its superiority in structure resemblance and hard instance generation as well as general applicability. One future work is the study on combining strong learning- based solvers (Li et al., 2023b; Zhang et al., 2024a) with instance generation scheme e.g. in the sense of training data augmentation which has been common in vision (Zhu et al., 2020). It is also possible to incorporate multiple graphs for matching (Yan et al., 2014; Jiang et al., 2021).
9

---

Published as a conference paper at ICLR 2024
REFERENCES
Zeina Abu-Aisheh, Romain Raveaux, Jean- Yves Ramel, and Patrick Martineau. An exact graph edit distance algorithm for solving pattern recognition problems. International Conference on Pattern Recognition Applications and Methods, 2015.
Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning solve circuit-SAT: An unsupervised differentiable approach. In International Conference on Learning Representations, 2018.
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. On the structure of industrial sat instances. In International Conference Principles and Practice of Constraint Programming, pp. 127-141. Springer, 2009.
Matej Balog, Nilesh Tripuraneni, Zoubin Ghahramani, and Adrian Weller. Lost relatives of the gumbel trick. In International Conference on Machine Learning, pp. 371-379, 2017.
Tomáš Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda (eds.). Proceedings of SAT' Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2021.
Yoshua Bengio, Andrea Lodi, and Antoine Prouvost. Machine learning for combinatorial optimization: methodological tour d'horizon. European Journal of Operational Research, 290(2):405 421, 2021.
Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009.
Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal methods in system design, 19:7-34, 2001.
Alexander Cowen- Wenlong Lyu, Rasul Tutunov, Zhi Wang, Antoine Grosnit, Ryan-Rhys Griffiths, Alexandre Maravel, Jianye Hao, Jun Wang. Jan Peters, and Haitham Bou Ammar. Hebo: Pushing the limits of sample-efficient hyperparameter optimisation. Journal of Artificial Intelligence Research, 74, 07 2022.
Armin Biere Katalin Fazekas Mathias Fleury and Maximilian Heisinger. Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. SAT COMPETITION, 50:2020, 2020.
Iván Garzón, Pablo Mesejo, and Jesús Giráldez-Cru, On the performance of deep generative models of realistic sat instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), 2022.
Haoyu Geng, Runzhong Wang, Fei Wu, and Junchi Yan. Gal-vne: Solving the problem with global reinforcement learning and local one-shot neural prediction. In ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2023.
Zijie Geng, Xijun Li, Jie Wang, Xiao Li, Yongdong Zhang, and Feng Wu. deep instance generative framework for milp solvers under limited data availability. Advances in Neural Information Processing Systems, 36, 2024.
Jesús Girâldez-Cru and Jordi Levy. A modularity-based random sat instances generator. In Interna- tional Joint Conference on Artificial Intelligence, 2015.
Jesús Giráldez-Cru and Jordi Levy. Locality in random sat instances. In International Joint Confer- ences on Artificial Intelligence, 2017.
Hongyu Guo and Yongyi Mao. Intrusion-free graph mixup. 2021.
Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, and Junchi Yan. Machine learning methods in solving the boolean satisfiability problem. Machine Intelligence Research, 2023.
10

---

Published as a conference paper at ICLR 2024
Andrew Haberlandt, Harrison Green, and Marijn JH Heule. Effectiie auxiliary variables via structured reencoding. arXiv preprint arXiv:2307.01904 2023.
Jonathan Ho, Ajay Jain, and Pieter Abbeel. Denoising diffusion probabilistic models. Advances in neural information processing systems, 2020.
Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural computation, 9(8): 1735-1780, 1997.
Holger Hoos and Thomas Stützle. SATLIB: An online resource for research on SAT, pp. 283-292. 04 2000.
Eric Jang, Shixiang Gu, and Ben Poole. Categorical reparameterization with gumbel-softmax. arXiv preprint arXiv: 1.01 144, 2016.
Zetian Jiang, Tianzhe Wang, and Junchi Yan. Unifying offline and online multi-graph matching via finding shortest paths supergraph. TPAMI, (31)):33648-36 2021.
Zetian Jiang, Jiaxin Lu, Tianzhe Wang, and Junchi Yan. Learning universe model for partial matching networks over multiple graphs. ArXiv, abs/2210.10374. 2022.
H Kautz, McAllester, and Selman. Ten challenges in propositional reasoning and search. In International Joint Conference Artificial Intelligence, 1997.
Henry A Kautz, Bart Selman, et al. Planning as satisfiability. ECAL, volume 92, pp. 359-363. Citeseer, 1992.
Harold W Kuhn. The hungarian method for the assignment problem. Naval research logistics quarterly, 2(1-2):83-97, 1955.
Marius Leordeanu and Martial Hebert. A spectral technique for correspondence problems using pairwise constraints. In Tenth IEEE International Conference on Computer Vision (ICCV'05) Volume I, volume 2, pp. 1489. IEFF, 2005.
Xijun Li, Fangzhou Zhu, Hui-Ling Zhen, Weilin Luo, Meng Lu, Yimin Huang, Zhenan Fan, Zirui Zhou, Yufei Kuang, Zhihai Wang, et al. Machine learning insides optverse ai solver: Design principles and applications. arXiv preprint S..i::2401.059660 2024.
Yang Li. Yuqi Jia, Wanqian Luo, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, and Junchi Yan. Kissat adaptive restart, kissat efexp: Adaptive restart policy and variable scoring improvement. SAT COMPETITION, pp. 39, 2022a.
Yang Li, Yichuan Mo, Liangliang Shi, and Junchi Yan. Improving generative adversarial networks via adversarial learning in latent space. Advances in Neural Information Processing Systems, 2022b.
Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Wanqian Luo, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, and Junchi Yan. Hardsatgen: Understanding the difficulty of hard sat formula gen- eration and a strong caettuur-hhaddess---ae on Knowledge Discovery and Data Mining (KDD), 2023a.
baseline. In ACM SIGKDD International Conference
Yang Li, Jinpei Guo, Runzhong Wang, and Junchi Yan. T2t: From distribution learning in training to gradient search in testing for combinatorial optimization. In Advances in Neural Information Processing Systems, 2023b.
Yang Li, Liangliang Shi, and Junchi Yan. lid-gan: an iid sampling perspective for regularizing mode collapse. In International Joint Conference on Artificial Intelligence, 2023c.
Zhaoyu Li. Jinpei Guo, and Xujie Si. G4satbench: Benchmarking and advancing sat solving with graph neural networks. arXiv preprint arXiv:2309.1694) 2023d.
2023d.
Hongyi Ling, Zhimeng Jiang, Meng Liu, Shuiwang Ji, and Na Zou. Graph mixup with soft alignments. arXiv preprint 2rXiv:2306.06788 2023.
11

---

Published as a conference paper at ICLR 2024
Chang Liu, Chenfei Lou, Runzhong Wang, Alan Yuhan Xi, Li Shen, and Junchi Yan. Deep neural network fusion via graph matching with applications to model ensemble and federated learning. In International Conference Machine Learning, pp. 13857-13869, PMLR, 2022a.
Chang Liu, Shaofeng Zhang, Xiaokang Yang, and Junchi Yan. Self-supervised learning of visual graph matching. In European Conference on Computer Vision, pp. 370-388. Springer, 2022b.
Chang Liu, Zetian Jiang. Runzhong Wang, Lingxiao Huang. Pinyan Lu, and Junchi Yan. Revocable deep reinforcement learning with affinity regularization for outlier-robust graph matching. In The Eleventh International Conference on Learning Representations, 2023.
Jiaxin Lu, Zetian Jiang, Tianzhe Wang, and Junchi Yan. MBc: A framework towards convergent, flexible, and unsupervised learning mixture graph matching and clustering. The Twelfth International Conference Learning Representations, 2024.
Gonzalo Mena, David Belanger, Scott Linderman, and Jasper Snoek. Learning latent permutations with gumbel-sinkhorn networks. In International Conference on Learning Representations, 2018.
Mark EJ Newman. Clustering and preferential attachment in growing networks. Physical review E, 64(2):025102, 2001.
Mark EJ Newman and Michelle Girvan. Finding and evaluating community structure in networks. Physical review E, 69(2):026113 13, 2004.
Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Impact of community structure on sat solver performance. In International Conference on Theory and Applications of Satisfiability Testing, pp. 252-2522662222 352-268. Springer, 2014.
Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics, Goal-aware neural sat solver. In International Joint Conference on Neural Networks, 2022.
Joonhyung Park, Hajin Shim, and Eunho Yang. Graph transplant: Node saliency-guided graph mixup with local structure preservation. In AAAI Conference on Artificial Intelligence, volume 36, pp. 7966-7974, 2022.
Daniel Selsam and Nikolaj Bjørner Neurocore: Guiding regh-performance sat solvers with unsat-core predictions. CoRR, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a sat solver from single-bit supervision. In International Conference on Learning Representations, 2019.
Richard Sinkhorn and Paul Knopp. Concerning nonnegative matrices and doubly stochastic matrices. Pacific Journal of Mathematics, 21(2):343-34) 348, 1967.
Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending sat solvers to cryptographic problems. In International Conference on Theory and Applications of Satisfiability Testing, pp. 244-257. Springer, 2009.
Grigori S Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967-1970, pp. 466-483, 1983.
Runzhong Wang. Junchi Yan, and Xiaokang Yang. Learning combinatorial embedding networks for deep graph matching. In Proceedings of the IEEE/CVF international conference on computer vision, pp. 3056-3065, 2019.
Runzhong Wang, Junchi Yan, and Xiaokang Yang. Combinatorial learning of robust deep graph matching: an embedding based approach. IEEE Transactions on Pattern Analysis and Machine Intelligence, 2020.
Runzhong Wang, Junchi Yan, and Xiaokang Yang. Neural graph matching network: Learning lawler's quadratic assignment problem with extension to hypergraph and multiple- graph matching. IEEE Transactions Pattern Analysis and Machine Intelligence, 44(9):5261-52799 2021a.
12

---

Published as a conference paper at ICLR 2024
Runzhong Wang, Ziao Guo, Shaofei Jiang, Xiaokang Yang, and Junchi Yan. Deep learning of partial graph matching via differentiable top-k. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pp. 6272 62221,21,220 2023a.
Runzhong Wang, Yunhao Zhang, Ziao Guo, Tianyi Chen, Xiaokang Yang, and Junchi Yan. Linsatner: The positive linear satisfiability neural networks. In International Conference on Machine Learning, 2023b.
Runzhong Wang, Ziao Guo, Wenzheng Pan, Jiale Ma, Yikai Zhang, Nan Yang, Qi Liu, Longxuan Wei, Hanxue Zhang, Chang Liu, Zetian Jiang, Xiaokang Yang, and Junchi Yan. Pygmtools: A python graph matching toolkit. Journal of Machine Learning Research, 2024.
Yiwei Wang, Wei Wang, Yuxuan Liang, Yujun Cai, and Bryan Hooi. Mixup for node and graph classification. In Proceedings of the Web Conference 2021, pp. 3663-3674, 2021b.
Yan, Y. Li, W. Liu, H. Zha, X. Yang, and Chu. Graduated consistency- optimization for multi-graph matching. In ECCV, 2014.
Junchi Yan, Shuang Yang, and Edwin R Hancock. Learning for graph matching and related combi- natorial optimization problems. International Joint Conference on Artificial Intelligence, pp. 4988 4996, 2020.
Jaemin Yoo, Sooyeon Shim, and U Kang. Model-agmostic augmentation for accurate graph classifica- tion. In Proceedings of the ACM Web Conference 2022, pp. 1281-1291, 2022.
Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec. G2sat: Learning to generate sat formulas. Advances in neural information processing systems, volume 32, 2019.
Tianshu Yu, Runzhong Wang,
Junchi Yan, and Baoxin Li. Learning deep graph matching with channel-independent embedding and hungarian attention. In International conference on learning representations, 2020.
Changwen Zhang, Wenli Ouyang, Hao Yuan, Liming Gong, Yong Sun, Ziao Guo, Zhichen Dong, and Junchi Yan. Towards imitation learning to branch for mip: A hybrid reinforcement learning based sample augmentation approach. In International Conference on Learning Representations, 2024a.
Shaofeng Zhang, Meng Liu, Junchi Yan, Hengrui Zhang, Lingxiao Huang, Xiaokang Yang, and Pinyan Lu. m-mix: Generating hard negatives via multi-sample mixing for contrastive learning. In Knowledge Discovery and Data Mining Conference (SIGKDD), 2022.
Shaofeng Zhang, Jinfa Huang, Qiang Zhou, Zhibin Wang, Fan Wang, Jiebo Luo, and Junchi Yan. Continuous-mulle multiple image outpainting in one-step via positional query and a diffusion- based approach. In ICLR, 2024b.
Jianchao Zhu, Junchi Yan, and Hongyuan Zha. Automix: Mixup networks for sample interpolation via cooperative barycenter learning. In European Conference on Computer Vision, 2020.
13

---

Published as a conference paper at ICLR 2024
APPENDIX
A SUPPLEMENTARY EXPERIMENTS
All the experiments are performed on a singlc GPU of GeForce RTX 3090. The affinity matrix K is calculated on an AMD Ryzen Threadripper 3970X 32-core CPU with 128GB memory.
A.1 MORE RESULTS SOLVER RUNTIME
Table 6 and Table 7 show the evaluation of solvers Kissat (Fleury & Heisinger, 2020) and SBVA VA- Cadical (Haberlandt et al., 2023)² runtime over the generated formulas as well as the original benchmarks. 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, MixSATGEN perform consistently regarding the computational hardness across different solvers.
Table 6: Kissat runtime evaluation. Standard deviations are in brackets. Best resemblance in bold.
Method
hard-a
hard-b
hard-c
hard-d
hard-e
hard-f
bard-g
hard-h
Grand Truth
155.60
1216.28
1478.99
254.14
2033.51
33.09
81.00
1898.28
CA (Girlldez-Cmi Levy, 2015)
0.01
0.01
0.01
0.01
0,01
0.04
0.01
0,01
(1.0.0))
(10.00)
(10.00)
(10.00)
(10.00)
(10.02)
(10.00)
(10.00)
PS (Giräldez-Cru Levy, 2017)
(=0.01)
0,07
(=0.02)
0,07
(=0.00)
0.01
(+0.00)
0.01
(=0000)
0.01
(+0.00)
0,01
(+0.00)
0.01
(=0.000
0.01
0.01
0.01
0.01
0.01
0.01
0.01
0.01
0,01
G2SAT (You 2019)
(1.0.00)
(100.00)
(10.00)
(10.00)
(10.00)
(10.00)
(10.00)
(10.00)
GCN2S (Ganzin al., 2022)
(+:343.27)
1686.27
(=1744
16.18
(=0.00)
0.01
(=0.00)
0.01
(=0.00)
0.01
(+0.00)
0:01
(+0.000
0.01
(=0.000
0,01
HardSATGEN (Li al., 2023a)
N/A
N/A
N/A
N/A
(1 (1115))5)
1915.25
(12.16)
47.83
(1332.34)
137.69
1964.77
(1936)6)
MixSATGEN (A- 0)
103.62
443.61
1741.31
35.07
0.91
0.01
0.01
0.01
(+-7.44)
(+594,33)
(+2306626)
(-72.85)
(+1.41)
(+0.00)
(+0.00)
(+0.00)
MiXSATGEN (A= 0.1, 1)
61.18
485.24
1669.61
54.45
13.22
0.01
0.01
0.01
(1:67.41)
(1542.34)
(1:2355 .0))
(=8688)
(=1502)
(10000)
(10.00)
(1:0.00)
MisSATGEN (A- 0.5. 1)
684.30
970.01
1355.34
48.07
147.09
0.02
0.01
0.01
(+-944.8))
(+1355.16))
(+1851,322
(=67,87)
(+:207.34 34))
(+0,01)
(+0.00)
(+0.000)
MiXSATOEN (A- 1.0, 1)
(+-2350.91)
1675.33
(5535.15)
385.76
(=458)87)
311.94
(=119.10)
(#4.50)
(+0.01)
(+0.00)
(=+0.00)
MixSATGEN (random)
1190.95
851.71
504.22
100.23
0.52
0.01
0.01
0,01
(.1191))5)
(L 1503.2)))
(1.1002.57)
(1248.36)
(10.75)
(10.00)
(100000
(1.0.00)
Table 7: Cadicall runtime evaluation. STDs are in brackets. Best resemblance in bold.
Method
bard-o
hard-b
bard-:
bard-d
hard-e
hard-/
hard-g
hard-h
Ground Truth
3125.56
369.54
2630.29
59.89
4122.88
80.39
103.19
1079.08
CA (Giráldez-Cru Lovy, 2015)
(+0.01)
0.12
(-0.00)
0.13
(+0.00)
0.06
(+0.00)
0.05
(+0.00)
0.06
(+0.04)
0.12
(+0.00)
0.05
(+0.00)
0.06
PS (Giräldez-Cru & Levy, 2017)
(+0.02)
0.81
(=0.02)
0,80
(+0.00)
0.07
(+0.00)
0.07
(=0.000
0.07
(+0.00)
0.07
(++0.00)
0.06
(+0.00)
0.06
G2SAT (You et al., 2019)
(++0.00)
0.13
(=0.00)
0.13
(+0.00)
0.07
(+0.000
0.07
(=00000
(+00.00)
0.07
(=00.00)
(+0.00)
GCN25 (Gazzón et al., 2022)
7324.38
14,80
0.06
0.06
0.05
0.06
0.05
0.06
(113333.4D)
(115.511)
(10.00)
(10.00)
(1:0.00)
(1.0.00)
(100000)
(10.00)
HardSATGEN at,,, 2023a)
N/A
N/A
N/A
N/A
(1300311)
4249.16
(17.34)
67,53
(177.77)
116.32
(1.22.15
1254.20
MixSATGEN (A
1048.88
185.46
2113.74
91.30
7.87
0.06
0.05
0.05
(336..855
(1:205:27)
(122638.77)
(#128.31)
(=7.48)
(20.00)
(20.01)
(10.01)
MisSATGEN (A 0.1,
989.84
219.44
6669
87.56
40.14
0.12
0.10
0.11
(11377668)
(1:16.88)
(19425.98)
(1127.11)
(1:4499))
(10.04)
(1:0.03)
(10.03)
MisSATGEN (A 0.5,7
(d:4000.04
303.93
(114.30)
11.37
(11099.89)
959.93
(1933880
77.23
(4:323.01)
232.24
(1:0233
0.17
(100000)
0.06
(10,00)
0.06
MiXSATGEN (A- 1.0,7
(L.307.17 17)
237.04
(1.272.73)
372.09
(1)
433.07
(1232.177)
170.34
(1:22336)
17.79
(1.0.88)
0.17
(10004)
(10.04)
MixSATGEN (random)
986.48
806.81
$25,09
558.82
3,58
0,10
0.11
0.09
1463.39)
(1:1145.72)
(1. (313332.83)
(.12822994
(1 (8.3333)3)
(1:0.02)
(1:0.03)
(10.01)
A.2 PIPELINE EFFICIENCY
To demonstrate the efficiency advantage of MixSATGEN over previous Late-of-the-art learning- based methods that generate from scratch, we compare G2SAT (You et al., 2019) with MiXSATGEN
"The overall mrin-track winner of the 2023 SAT competition.
14

---

Published as a conference paper at ICLR 2024
01 1.0) for single instance generation, which is adopted as the standard training scheme in Garzón et al. (2022). As shown Table 8, the pipelines consist of two processes: training and generating. The training process only needs to be performed once for 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 with reference instances from the Hard dataset. The results show that MiXSATGEN is significantly more efficient than G2SAT in both processes. Specifically, for the generating phase, MixSAT costs only approximately 1/2000 runtime compared to G2SAT.
Table 8: Consumed time of training and generating process for single instance generation.
Training
Generating
G2SAT (You et al., 2019)
4467,051 2315.81
2242.07
MiXSATGEN
1760.031457.889
1.4410.22
A.3 SECONDARY INTERPOLATION
To evaluate the effect of secondary interpolation on the performance of formulas generated by MixSATGEN, we select two representative instance pairs and apply MiXSATGEN() 0.1, 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 in Table 9, where 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 MiXSATGEN in generating hard formulas through interpolation.
Table 9: Solver runtime comparison of formulas secondary interpolation by MiXSATGEN.
Ground Truth
Interpolated 10%
10%
6-a
1382.71 852.85
1023.25 4.69
1001.97 = 7.28
1042.53 4.78
hard d-c
199.63 190.70
6.13 + 3.14
3.56
A.4 SATISFIABILITY PHASE PRESERVATION
The results of satisfiability phase preservation for generated formulas are presented in Table 10. It is observed that despite being trained dataset with a one-to-one ratio of satisfiable 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, MiXSATGEN maintains the closest phase ratio the original reference instances.
Table 10: Satisfiability ratio of generated formulas and the preserve accuracy.
Method
EASY
HARD
UNSAT ratio
SAT accuracy
UNSAT accuracy
UNSAT ratio
SAT
UNSAT
50.00%
50,00%
CA (Giraldezz Cru 2015)
87.5%
0.00%
75.00%
75.00%
0.00%
50, 50.00%
PS (Girdldes-Cnn Cra & Levy, 2017)
0.007%
100.00%
0.00%
0.00%
100.00%
D.007%
G2SAT (You al., 2019)
100.00%%
0.00%
100.00%
100.00%
0.00%
100.007%
GCN2S (Gazzón
HTrdSATGEN (1.i es al., 2023a)
100%
NIA
100.00%
100.00%
N/A
100.007%
MisSATGEN
50.00%
83.33%
$1.33%
43.41%
19%
25.00%
B PSEUDOCODE FOR MIXSATGEN
The algorithms for the training and generating process of MixSATGEN in Sec. 3 are presented in Alg. and Alg. 2.
C DATASET CONSTRUCTION
When selecting instances to construct the dataset for evaluation, consider the following factors:
15

---

Published as a conference paper at ICLR 2024
Algorithm 1 Training process of MixSATGEN
Input: LCG pair G1, G2 with 2n1, 2n2 literals; pretrained embedding model D; training epoch Output: Optimized embedding model D;
for i 1 to do H - D(G))
H2 D(G2)
(16:))))'0 + H
{0, -1;)} + H2, n2
M/M is the InnerProduct
Calculate M, where Mo[i,j] max (Mili.,4] Mi[-4, -4,, Mil4, -4] + Mi[- 4J)
< Sinkhorn (.)
K AffinityMatris (Ga G1. G2)
loss + -vec(S) (8) Kvec(S)
Update D with loss
end for
Algorithm 2 Generating process of MixSATGEN
Input: LCG pair G1, G2 with 2m1 2ny literals; optimized embedding model D; mixing ratio 3;
noise intensity factor X; gumbel temperature т; Output: Interpolated formula G3;
// Matching.
H. < (
H2 D(G2)
{(4, -L,) + H
(1g ==,))==++ H2. E
MM, is the InnerProduct
Calculate M, where M. max (M14, + MI/4, M4],, -4] + MI(-4,4)
r ~ Gumbel
Sinkhorn ((M, + AT) /T) // /Guumel-Sinkhorn
P < Hungarian(S)
Extract correspondence map and confidence score of variables from P
// Mixing.
G3 + G1
// Global confidence for every clause in G1-
Calculate the global confidence score of every clause e₁ in G1 with sum of the confidences of its variables
while the substituted clause ratio < 3 do
Pick e₁ in descending order of global confidence score over G1 // Local confidence for related clause in G2.
Trace clause C22 on G2 whose item has shared variables with 6₁ through correspondence map
Calculate the local confidence score of clause C2 in C2 with sum of the confidences of its shared variables with ej through correspondence map
C2 h- clauses with the highest local confidence score in C2
// Global confidence for remained clause in G2.
Calculate the global confidence score of C2 in C2 with sum the confidences of its variables
C2 clauses with the highest global confidence in C2
C2 f- take a clause from C2 randomly
// Clause replacement for graph mixup.
Remove all edges of Cı on G3
I + [literal / Ga} where the correspondence literal of links 02 G2
Add edges between / L and 0₁ on G3
end while
1) It should include instances derived from real-world application scenarios to ensure the practi- cal value our experimental validation. Therefore, we choose instances from SAT Competition benchmarks, which are encoded from real-world scenarios.
16

---

Published as a conference paper at ICLR 2024
2) We aim to maintain equal proportion of satisfiable and unsatisfiable instances in data to verify the general applicability of MixSAT. Hence, we maintain a 1:1 ratio sat to unsat instances in the dataset.
3) Recognizing the significance of computational difficulty in experimental validation, we specifically select instances with higher computational hardness to constitute the Hard dataset.
4) We select formulas that have a suitable scale range of around hundreds of variables and hundreds to thousands of clauses. While current graph network based methods may have difficulty scaling to very large graphs, MixSATGEN also faces the same scale constraint due to the scale-related resource-consuming affinity matrix construction in training process.
17


Reviews:
[{"review_id": "7pagZd5VZv", "reviewer": "Reviewer_KdVD", "summary": "This paper proposes MixSAT, a ML-based generation approach for SAT instances. Instead of generating formulas ex novo, MixSAT interpolates exising pairs of formulas using:\n\n-    GNN-based representation learning for capturing structural properties in a latent representation\n-    Differentiable Gumbel-Sinkhorn stochastic matching between instances\n-    Graph interpolation via iterative clause replacement\n\nThe generated formulas statistically retain similar structural properties and preserve the hardness of the original instances.", "questions": "1) Besides structural properties and hardness, does MixSAT preserve the SAT/UNSAT ratio of the original data?\n2) What are the limitations of your approach?\n3) Do you observe a degratation in performance when interpolating formulas generated by MixSAT?\n4) Is it possible to learn a binary classifier that accurately discriminates original vs. MixSAT instances?\n\nMinors:\n\n\"The Boolean satisfiability problem (SAT) stands as a canonical NP-complete combinatorial optimization (CO) problem\"\n\nSAT is a decision problem, not a CO. Max-SAT is the optimization counterpart.\n\n\"there exists an assignment of Boolean variables that satisfies a Boolean formula and in general is NP-hard.\"\n\nSAT is NP-complete. I understand that, in principle, the formulas that MixSAT generates could be used in non-decision settings too. I would then rephrase the sentences above, making it clear that you address generation of propositional logic instances for decision (SAT) and other problems (e.g. Max-SAT)\n\n\"e.g. in EDA.\"\n\nWhat EDA stands for?\n\nAdding the pseudocode of MixSAT would greatly help.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "-    Overall very clear presentation\n-    Well-motivated problem\n-    The proposed technique seems sound and novel\n-    Promising initial results", "weaknesses": "-    Minor points related to the presentation and evaluation\n-    I would also discuss the limitations of MixSAT", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "SjYPUwOPZN", "reviewer": "Reviewer_5Kyc", "summary": "This paper is devoted to machine learning assisted generation of\nfamilies of benchmark formulas for propositional satisfiability (SAT)\nsolvers. The paper builds on the use of graph representations of\nformulas in conjunctive normal form (CNF) and utilizes a graph\ninterpolation approach, which modifies the graph structure by\nreplacing some of its substructures from other similar instances. The\npaper argues that the proposed approach is able to maintain the\noriginal hardness of the corresponding families of benchmarks, thanks\nto the use of Gumpel noise. The presented experimental results claim\nto demonstrate the advantage over the state of the art in SAT\nbenchmark generation from the perspective of (1) maintaining the\nstructure of the benchmark family and (2) its hardness.", "questions": "- A key question is this line of research is whether the formulas\n  generated automatically exhibit the properties intrinsic to\n  \"industrial instances\". This is important given the widespread use\n  of modern SAT solvers in industrial settings. So I would like to ask\n  the authors whether the ability of their approach to capture this.\n\n- Can you comment on the rationale of (at least some of) the steps\n  your approach performs?", "limitations": "", "rating": 5, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "- The entire flow of the proposed approach are provided one after\n  another.\n- The overall presentation is nice, especially the figures look\n  beautiful and help a reader understand the ideas.\n- To the best of my understanding, the proposed approach is novel.", "weaknesses": "- Although all the steps of the approach are listed, they are not\n  augmented with clear arguments for why they are used. This seems to\n  be a standard issue with all the works on applying ML methods in/for\n  combinatorial problem solvers where the authors propose to apply\n  ~50-100 steps with no clear justification. This trend is clearly\n  detached from the mainstream SAT research where each idea has to be\n  clearly articulated and justified. Granted it may be just me getting\n  lost in matters that are straightforward to any ML expert.\n\n- Experimental results look rather weak to me as they seem to be a\n  mixed bag. At least, I don't see a clear advantage of the proposed\n  approach over the state of the art in terms of the hardness of the\n  generated formulas.\n\n- Minor: the authors say that SAT is a combinatorial optimization (CO)\n  problem while it isn't. There is no optimization in the original\n  decision formulation of SAT.\n\n- Minor: I would suggest rewording the sentence (in the introduction):\n  \"resemble the computational complexity\". Computational complexity of\n  SAT is well understood.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "FtHfAsgLjC", "reviewer": "Reviewer_SBgK", "summary": "This paper proposes a method for automatically generating SAT instances. Automatic generation of SAT instances is highly demanded since we need a large amount of SAT instances for estimating parameters of learning-based SAT solvers or tuning hyperparameters of traditional SAT solvers. While previous state-of-the-art learning-based SAT instance generation methods generate instances from a single reference, the proposed algorithm, MixSAT, generates SAT instances by interpolating two SAT instances. MixSAT first makes an assignment map of variables of two SAT instances. Then, it uses the map to select similar clauses and finally exchanges these similar clauses to make new SAT instances. On making an assignment map, the proposed method puts random noise for preserving difficulties. Experimental results show that MixSAT can preserve more graph structural properties than baseline methods, except for UNSAT instances. Moreover, MaxSAT preserves the difficulty of SAT instances, in hard satisfiable instances.", "questions": "I'd be happy if the authors addressed my concerns mentioned in the weakness section.", "limitations": "", "rating": 5, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "**Important topic:**\nI agree with the motivation that we need more real-world SAT instances to improve the performance of Boolean SAT solvers. I agree that to generate SAT instances, preserving difficulty is a challenging task since SAT instances seem sensitive to small changes. \n\n**Clearly written paper:**\nThe paper is generally clearly written and easy to read. Figures 1-3 help us understand the complex procedure of MaxSAT.\n\n**The idea of using interpolation is interesting:**\nThe idea of using interpolation is interesting. It seems a reasonable way of data augmentation. Moreover, the proposed method seems\ncarefully designed to perform interpolation between two CNFs.\n\n**Experimental results show the superiority of the proposed method:**\nAlthough not always better than HardSATGEN, the proposed method outperforms other baseline methods.", "weaknesses": "**Experimental results are not strong:**\n1. Experimental results show that the proposed method is not always superior to HardSATGEN. Especially, the running time evaluation results in Tab.2 show that the proposed method fails to preserve the computational difficulties of hard instances. The results seem to contradict the claim of the paper.\n1. Li et al. (2023) reported that hyperparameter tuning with instances generated by HardSATGEN improves performance on real-world problems. Since a primal objective of generating SAT instances is to tune the parameters of solvers, the paper should report the results of using the instances generated by MixSAT to tune the parameters of existing solvers. \n1. Runtime evaluations were conducted with CaDiCaL. I think the paper should also report the performance of different solvers like Kissat since different solvers sometimes show completely different performances. In performance evaluation, Li et al. (2023) compared the performance of three different solvers. It seems a safer way to evaluate the running time of SAT solvers.\n\n\n\n**Some important details of experiments are missing:**\nSome important details of experiments are not reported in the paper:\n1. The proposed method generates instances by interpolating two instances. Therefore, 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.\n2. It is said that the dataset was taken from SATLIB and SAT Competition 2021. However, how the authors select easy and hard [a-h] instances from a large amount of instances seems not explained in the paper. The paper should show the reason behind selecting these instances to make the evaluation fair.\n\n\n\n**There are claims not supported by experimental results:**\nSome claims of the paper seem not supported by the experimental results:\n1. The paper says the proposed method is more efficient (page 2), but no experimental results support the claim.\n2. The paper says that MaxSAT introduces some randomness to maintain computational hardness. However, experimental results reported in Table 2 show that randomness does not help much in preserving hardness.\n\nThese points make me feel that the proposed approach is not well-motivated.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)