SATformer: Transformers for SAT Solving

The mainstream SAT solvers depend on heuristic strategies to speed up the solving process. However, the state-of-the-art SAT solvers are still suffering from the increasing sizes of the problem instances. In the combinatorial optimization area, especially for the SAT problem, deep learning provides an attractive solution to improve the solving efficiency, as surveyed in  Guo et al. (2022).

Generally, there are two approaches to applying deep learning to solve the SAT problem: Learning-aided and end-to-end. On the one hand, the learning-aided approaches aid traditional SAT solvers with a neural network instead of the manual-crafted heuristics. For example, NLocalSAT Zhang et al. (2020) boosts the traditional SAT solver by producing the initialization assignments, and Graph-$Q$-SAT Kurin et al. (2020) replaces the searching heuristic with a reinforcement learning agent. NeuroCore Selsam and Bjørner (2019) and NeuroComb Wang et al. (2021) learn the UNSAT core distribution to guide SAT solving. Although some modern SAT solvers equipped with learning-aided heuristics can solve more industrial problem instances within acceptable runtime, the performance of the overall solving system is still limited by the backbone SAT solver.

On the other hand, the end-to-end approaches solve the SAT problem with neural networks solely. For example, NeuroSAT Selsam et al. (2018) treats the SAT problem as a classification task and trains an end-to-end GNN-based framework to predict the binary results (satisfiable or unsatisfiable). DG-DAGRNN Amizadeh et al. (2018) focuses on the circuit satisfiability problem, i.e., determining whether the single primary output of a given circuit can return logic ’1’. They propose a differentiable method to evaluate the satisfiability value. By maximizing the value, the solver is more likely to find a satisfiable assignment. DeepSAT Li et al. (2022) formulates the SAT solution as produce of conditional Bernoulli distributions and obtains assignment by maximizing the joint probability. Similar to the later learning-based approach, SATformer also aims to solve the SAT problem in a standalone way.

The Transformer Vaswani et al. (2017) is well acknowledged as one of the most powerful architectures in modeling sequential data. With the adoption of Transformer, tremendous progress has been achieved in the field of text comprehension Meng et al. (2020), machine translation Wang et al. (2019) and even computer vision Dosovitskiy et al. (2020); Liu et al. (2021). With the self-attention mechanism, the Transformer block regards the sequential input tokens as a fully connected graph and represents the connectivity between every two nodes. Hence, the Transformer-based model is able to capture the correlation between each pair of tokens.

The first attempt to involve the Transformer for solving MaxSAT problem (a variant of SAT problem) is introduced in Shi et al. (2021). The proposed model represents a given SAT instance into a bipartite graph and applies Transformers to aggregate the message over these nodes. In our work, we regard the clauses as a non-ordering sequence and apply the Transformer to capture the correlations among these clauses.

A Boolean formula $\varphi$ consists of a set of variables $\{x_j{\}}_{i=1}^I\in \{True,False\}$ and a set of Boolean operators {AND ($\wedge$), OR($\vee$), NOT($\neg$), …} over these variables. Solving the SAT problem is determining whether there is at least one valid assignment on the variables so that the given formula $\varphi$ returns $true$.

An arbitrary Boolean formula can be converted into conjunctive normal form (CNF) with an equivalent transformation in linear time Tseitin (1983). Under CNF conventions, variables and theirs negations are named as literal (denoted as $x_j$ or $\neg x_j$). A disjunction of several literals constructs a clause $C_i=(x_1\vee x_2\vee ...)$. A conjunction of clauses forms the propositional instance $\varphi =(C_1\wedge C_2\wedge ...)$. In Eq. (1), we provide an example to explain the CNF, wherein the instance has three variables $I=\{x_1,x_2,x_3\}$ and consists of three clauses $C_1=\neg x_1\vee x_2,C_2=\neg x_2\vee \neg x_3,C_3=x_1\vee x_3$.

Literal-clause Graph (LCG) is a bipartite graph representation of the CNF formulas, which is composed of literal nodes and clause nodes. Two types of edges are defined in LCG: one connects a literal node with a clause node, and another connects a literal node with its corresponding negation. Fig. 1 is an example representing the Eq. (1) in LCG.

Besides, given an unsatisfiable instance in CNF, if a sub-problem constructed by its several clauses is also unsatisfiable, then such sub-problem with specific clauses is referred to as an UNSAT core. Take the unsatisfiable instance ${\varphi }_U$ shown in Eq. (2) as an example. We can extract an unsatisfiable sub-problem ${\varphi }_U^{{}^{\prime }}=C_2\wedge C_5\wedge C_6$ as one of the UNSAT cores of the original instance ${\varphi }_U$. The concept of UNSAT core is further explained by the searching-based solving process. As the clauses $C_2$ and $C_6$ only include one literal, to satisfy both clauses, the variables must be assigned as $x_1=false,x_2=true$. Nevertheless, the assignment does not satisfy clause $C_5$ under any cases, no matter what value is assigned to the remaining variable $x_3$. Therefore, the solver proves there is an inevitable conflict within these clauses so that all searching branches for solving problem ${\varphi }_U^{{}^{\prime }}$ fail. It should be noted that there is no UNSAT core in a satisfiable instance.

Since the UNSAT cores provide sufficient causality for unsatisfiability judgement, one can determine a CNF instance is unsatisfiable or not by converting the original problems into UNSAT core extraction. In this work, we solve the SAT problem in a novel manner by learning to capture the clauses which leads to the unsatisfiablity of the instance (i.e., clauses included in UNSAT core) and modeling the interactions among these clauses.

Fig. 2 shows the overview of our proposed SATformer. Firstly, our model employs GNN to obtain the clause representation and literal representation from a CNF instance. After performing message-passing for several iterations based on the LCG, the GNN learns the literal embeddings with rich information from the connecting clauses and the clause embeddings containing information from the involving literals.

Secondly, after getting the clause embedding, we design a classifier to predict which clauses are involved in UNSAT core. Formally, the classifier is implemented by a Multilayer Perceptron (MLP)as shown in Eq. (3), where $H_i^0$ is the embedding of clause $C_i$ produced by GNN, $y_i\in (0,1)$ is the prediction, and $n$ is the number of clauses. It should be noted that this structure is not perfect for classifying clauses with high accuracy. Nevertheless, similar to the NeuroCore Selsam and Bjørner (2019) which learns a heuristic that assigns higher priority to the important variables, the proposed classifier can help to highlight the clauses that are contributing more to unsatisfiability.

Thirdly, we consider that the unsatisfiability comes from the interaction among clauses in the UNSAT core. We take the clauses embeddings from GNN as inputs and apply the Transformer to capture such clause relationships. Benefiting from the self-attention mechanism inside the Transformer, the SATformer gives more attention to the clauses likely to be involved in the UNSAT core, which is proved in Sec. 4.3. However, the plain Transformer only learns the pairwise correlation. There is almost no cause of unsatisfiability coming from a pair of clauses. To deal with this problem, we merge clauses into clauses groups in a hierarchical manner and train a Hierarchical Transformer to model clause groups, which is elaborated in Sec. 3.4.

We adopt the multi-task learning (MTL) Caruana (1997) strategy to improve the performance of SATformer. As shown in Fig. 2, we train our model to predict UNSAT core (Task-a) and satisfiability (Task-b) simultaneously.

Firstly, although the UNSAT core is not unique for a given instance, there are only a few possible combinations of minimal unsatisfiable core (MUC), i.e., the UNSAT core with minimal size. We denote $n$ as the number of clauses and label a binary vector $Y_a^{\ast }=\{y_1^{\ast },y_2^{\ast },...,y_n^{\ast }\}$ as a ground truth for each instance, which represents whether the clause is included in MUC. Hence, the binary vector $Y_a^{\ast }$ for a satisfiable instance is all zero and some bits are assigned one for an unsatisfiable instance.

We denote that the clause embedding matrix is $H^0=\{H_1^0,H_2^0,...,H_n^0\}$ and obtain $Y_a=\{y_1,y_2,...,y_n\}$ to model a probability distribution over clauses as Eq. (4). We regard $Y_a$ as the contribution to unsatisfiability, where the larger value means that the corresponding clauses are more likely to form the MUC.

The model is trained by minimizing the Kullback-Leibler (KL) divergence Kullback and Leibler (1951):

Secondly, the SATformer predicts binary satisfiability as another task (Task-b). The model learns to produce a prediction results $Y_b\in (0,1)$ with single-bit supervision $Y_b^{\ast }\in \{0,1\}$. We apply Binary Cross-Entropy (BCE) loss to train the model.

Thus, the overall loss is the weighted sum of $L_a$ and $L_b$

Intuitively, Task-a aims to distinguish which clauses contribute more to unsatisfiability. In this case, our model learns to pay much attention to these clauses and predicts the final satisfiability as Task-b. Therefore, we can improve the solving accuracy by leveraging useful information between these two related tasks.

We further propose a Hierarchical Transformer design to model the correlation among clauses. Formally, for the plain Transformer $T$, we define the embeddings of the input tokens as $H=\{H_1,H_2,...,H_n\}$. The self-attention matrix $A$ and updated embedding $\hat{H}=(\widehat{H_1},\widehat{H_2},...,\widehat{H_n})$ are denoted as:

where the $Q$, $K$, $V$ produced by three projections represent quires, keys, and values. $W^Q$, $W^K$, $W^V$ are three learnable weights. The self-attention matrix $A$ describes the similarities between queries and keys for each pair of input tokens.

The unsatisfiability can not be determined by a pair of clauses. As the example instance in Eq. (2), the solver require to consider at least $3$ clauses ($C_2$, $C_5$ and $C_6$) to assert unsatisfiable. However, capturing the dependency among multiple tokens within one Transformer block is impractical. Even if increasing the number of Transformer blocks can mitigate this problem, this approach significantly increases the model complexity. In this paper, we propose a Transformer structure in a hierarchical manner, as shown in Fig. 3. Briefly, the model merges clauses within a fixed-size window into a clause group and then packages these groups into another group. The produced clause group embedding contains the information from all clauses covered by the lower-level groups. At a higher level, the model takes clause group embeddings as input tokens and learns the relationship between two clause groups.

More formally, the clause embeddings from the GNN model are denoted as $H_1^0,...,H_n^0$, where $n$ is the number of clauses. We also denote the clause group embeddings as $G_1^l,...,G_{D^l}^l$, where $D^l$ is the number of windows in level $l$ and the maximum level is $L$. Given the fixed window size $w$, we calculate $D^l$ as Eq. (9). Before dividing the embeddings into groups, we randomly pad the length of the embedding matrix as $w\cdot D^l$. For example, if there are $n=11$ clauses and the window size $w=4$, we divide these $11$ clauses with $1$ more padding clauses into $D^0=3$ windows at the first level.

Within a window with size $w$, the clause embeddings (clause group embeddings) are updated as:

where $d$ is the window index and matrix $H_d^{l-1}=\{H_{(d-1)\cdot w}^{l-1},...,H_{d\cdot w}^{l-1}\}$ consists of the embedding vectors of clauses in the window $d$. We also combine these clause embeddings into one group embedding for each window. The combination of clause group embedding is implemented with linear transformation LN. For the higher level, i.e., $l\ge 2$, the inputs of the Transformer Block should be clause group embeddings $G_d^{l-1}=\{G_{(d-1)\cdot w}^{l-1},...,G_{d\cdot w}^{l-1}\}$ instead of $H_d^{l-1}$.

We still take the instance in Eq. (2) as an example. When the window size is $3$, these $9$ clauses are divided into $3$ clause groups, where $G_1^1$ contains the information from $\{C_1,C_2,C_3\}$, $G_2^1$ represents $\{C_4,C_5,C_6\}$, and so on. We cannot find any UNSAT cores by combining clauses pairwise, but at a high level, the clauses contained by $G_1^1$ and $G_2^1$ can construct an UNSAT core. Therefore, to determine whether the instance is satisfiable, the model should consider the pairwise relationship of groups in various grain sizes.

As shown in Eq. (12), similar to the Feature Pyramid Networks (FPN) Lin et al. (2017), we also obtain level embedding $F^l$ based on the maximum pooling (MaxPooling) of all $H^l$ or $G^l$ as belows:

Finally, a MLP readout the concatenation (Cat) of these level embeddings and the pooling of final clause group embedding $G^{L\ast }$.

With the Hierarchical Transformer, our proposed SATformer can capture the effect on satisfiability among multiple clauses rather than pairs of clauses.

We present the details of the experimental setting, including the construction of datasets and the hyperparameter of the SATformer model. In the following experiments, we adopt the same settings described here for all models if there is no special case.

Evaluation metric: Our SATformer predicts the satisfiability of a given instance. We construct both satisfiable and unsatisfiable instances in the testing dataset and record the accuracy of binary classification. We still try to decode the satisfiability assignment in the appendix, which is similar to NeuroSAT Selsam et al. (2018).

Dataset preparation: We generate $100K$ satisfiable instances and $100K$ unsatisfiable instances. Following the same dataset generation scheme in  Selsam et al. (2018), a pair of random $k$-SAT satisfiable and unsatisfiable instances are generated together with only one different edge connection. Here, SR($m$) represents that the instance contains $m$ variables. In our training dataset, we set the problem size as SR($3-10$). Furthermore, we enumerate all possible clause subsets of each instance and label the minimal UNSAT cores. We also generate default testing datasets, each containing $50$ satisfiable and $50$ unsatisfiable instances in SR($3$-$10$), SR($20$), SR($40$) and SR($60$), respectively.

Implementation Details: In the GNN structure, we adopt the same configurations as NeuroSAT Selsam et al. (2018), except for reducing the number of message-passing iterations from $26$ to $10$. In the Hierarchical Transformer structure, we directly use clause embeddings as input tokens, resulting in the same hidden state dimension as $128$. The window size $w$ is assigned to $4$, and the total level of the hierarchical structure is $4$. Inside each Transformer block, we set the number of heads in the multiple head self-attention mechanism as $8$. The MLPs to produce two predictions for Task-a and Task-b are all configured as 3 layers. We train the model for $80$ epochs with batch-size $16$ on a single Nvidia V100 GPU. We adopt the Adam optimizer Kingma and Ba (2014) with learning rate ${10}^{-4}$ and weight decay ${10}^{-10}$.

Model Complexity: The complexity of NeuroSAT and above SATformer are illustrated in Tab. 1, where # FLOPs is the number of floating-point operations and # Para. is the total number of trainable parameters. Although our model requires more trainable parameters to build up Transformer structures, SATformer performs faster (lower # FLOPs) than NeuroSAT due to the fewer message-passing iterations.

We compare our SATformer with another learning-based SAT solver NeuroSAT Selsam et al. (2018). As an end-to-end SAT solver, SATformer does not compare with the learning-aided approaches. We also do not consider the other standalone SAT solver Amizadeh et al. (2018); Ozolins et al. (2021); Li et al. (2022) because they can not produce a single binary result.

Both NeuroSAT and our SATformer require the input instances are in CNF. While SR($m$) presents the problem scale, we use another metric $CV=\frac{n}{m}$ to better quantize the problem difficulty, where $n$ is the number of clauses and $m$ is the number of variables. The higher $CV$ value means that there are more clause constraints in the formula, and the instance is more difficult to be solved. The instances from the training dataset and the default testing dataset have $CV>5$. These satisfiable instances only have $1$ or $2$ possible satisfying assignments in total. Besides, we also produce the $50$ satisfiable and $50$ unsatisfiable simplified instances with $CV=4$ for each scale of problems. To ensure fairness, we train the NeuroSAT on the same training dataset in SR($3$-$10$). The results of binary classification are listed in Tab. 2.

From Tab. 2, we have a few observations. Firstly, our SATformer achieves higher performance than NeuroSAT across all datasets. For example, the NeuroSAT can only correctly classify $67\%$ in SR($20$) and $56\%$ in SR($40$) when $CV>5$, but our SATformer has an accuracy of $70\%$ in SR($20$) and $61\%$ in SR($40$). Secondly, the results of NeuroSAT have no significant difference when reducing the problem difficulty, but our SATformer performs better on the simplified instances. For example, SATformer solves all instances with $CV=3$ despite the problem scale. The reason is that SATformer relies on the correlation among clauses to solve SAT problems. With the smaller number of clauses, SATformer harnesses such correlation more easily. In contrast, NeuroSAT only learns the instance-level feature with single-bit supervision and does not obtain richer representations with the reduction of problem difficulty.

To conclude, our SATformer outperforms the NeuroSAT. Our SATformer also shows a similar property as the traditional SAT solver, i.e., they can achieve higher performance on these instances with lower difficulty.

This section investigates the effectiveness of the Transformer Blocks in SATformer. On the one hand, we compare our SATformer with a derived model framework SATformer-MLP, which replaces Transformer blocks with MLPs of the equivalent number of model paremeters (# Param.). Tab. 3 shows the experimental results. Since the SATformer-MLP regards all clauses equally instead of selectively enhancing the correlation between some clauses, it shows an inferior performance to the original SATformer.

On the other hand, as the Transformer distinctively treats token pairs based on the self-attention mechanism, we explore the attention weights on different token pairs. Based on the Task-a UNSAT core prediction, we equally divide the clauses into two categories: likely to form an UNSAT Core (denoted as C-clause) and Ulikely to form an UNSAT core (denoted as U-clause) cause unsatisfiable. Therefore, the pairwise connections are classified into $4$ types: between the C-clause and C-clause (CC), the C-clause and U-clause (CU), the U-clause and C-clause (UC), the U-clause and U-clause (UU). We calculate the overall attention weights for these $4$ types, respectively, and list the percentage in Tab. 4. The higher percentage means the model pays much attention to the corresponding pairwise correlation. Transformer assigns almost $70\%$ attention weights on the connection CC. Moreover, plus the connection CU and UC, the model allocates for $97.23\%$ attention weights in total to the capture the correlation related to C-clauses. Therefore, our Transformer-based mainly focuses on the clauses, which contributes more to unsatisfiability.

To summarize, our SATformer not only captures the relationship among clauses but also learns how to pay much attention to these clauses that are more likely to raise unsatisfiability.

In this subsection, we design an ablation study and also build some special cases to indicate the effectiveness of our Hierarchical Transformer.

Firstly, we apply some plain Transformer blocks to replace the hierarchical structure. This model takes clause embeddings as input tokens and updates with $4$ (same as $L=4$ in default SATformer configuration) stacked Transformer blocks (denoted as SATformer-NoHier). Then, the model produces an embedding vector by pooling all updated clause embeddings and predicts the final binary results. As shown in Tab. 5, SATformer-NoHier deals with fewer instances than SATformer. For example, SATformer-NoHier only achieves $70\%$ accuracy in SR($3$-$10$) and degrades as a randomly guessing classifier in SR($40$) and SR($60$) instances. On the contrary, the SATformer is still available in SR($40$) and SR($60$). The reason is that SATformer-NoHier can only learn the pairwise dependency, while a pair of clauses do not show a decisive effect on the satisfiability. Although the model can model multiple relationships by stacking Transformer blocks, $4$ layers of Transformer are still far from sufficient.

Secondly, to further demonstrate the ability of multiple relationship modeling, we construct two equivalent unsatisfiable instances as Eq. (13) based on Eq. (2) with different clause orders. These three clauses $C_2$, $C_5$, and $C_6$ forming MUC are highlighted with underlines.

We train the other two SATformer models with window size $w=3$, but the hierarchical level is different, where one is $L=1$, and another is $L=2$. As shown in Fig. 4, for the instance ${\varphi }_{U1}$, the clauses (from $C_1$ to $C_6$) in the first two groups can construct an unsatisfiable sub-instance. Hence, by modeling the pairwise relationship between input token embeddings $G_1^1$ and $G_2^1$ in level $l=1$ can determine the satisfiability. However, no pairwise correlation leads to unsatisfiability in the first hierarchical level in ${\varphi }_{U2}$. According to the experimental results, the model relying on the group embeddings in level $l=1$ can only predict ${\varphi }_{U1}$ correctly as unsatisfiable.

Moreover, if we add one more Transformer block in level $l=2$, the model can learn group embedding $G_1^2$, which contains the information from these $3$ clause groups. In this case, the SATformer model predicts both instances correctly.

In summary, our SATformer can learn the relationships among multiple tokens due to the pairwise self-attention mechanism and hierarchical manner. Besides, to mitigate the effect of clause ordering, we shuffle the clauses every $10$ training iteration.

To investigate the effectiveness of the MTL strategy in our SATformer, we train another model without UNSAT core supervision (denote as SATformer-NoCore) and compare the model with the original SATformer. Tab. 6 shows the experimental results. After removing the Task-a UNSAT core prediction, the model performance on these $4$ datasets all decreases.

Generally, UNSAT core retains rich information for the contribution of clauses to unsatisfiability. Predicting the UNSAT core is significantly related to SAT solving. Therefore, the MTL strategy benefits the model performance.

We explore the impact of GNN message-passing iterations on the performance of our SATformer. Here, the number of GNN message-passing rounds is denoted as $r$. In the default configuration of SATformer, the GNN module performs $10$ times aggregations between literals and clauses, while NeuroSAT has $r=26$. We incrementally increase the message-passing times of SATformer from $r=10$ to $r=26$. The results of satisfiability prediction are listed in Tab. 7.

Firstly, although our SATformer has fewer $r$ than NeuroSAT (see SATformer $r=10$ and NeuroSAT $r=26$), SATformer shows a better accuracy on each dataset than NeuroSAT. For example, SATformer with $10$ rounds message-passing predicts $94\%$ instances correctly on the dataset in CV>$5$ and SR($3$-$10$). NeuroSAT has a lower accuracy, where the $r=24$ model predicts $87\%$ and the $r=10$ model only predicts $62\%$.

Secondly, with the increase of GNN rounds $r$, both SATformer and NeuroSAT gain performance improvement. The prediction accuracy of SATformer increases from $77\%$ to $83\%$ on the dataset in CV>$5$ and SR($20$), when $r$ increases from $10$ to $26$. Since the SATformer achieves high accuracy on the datasets containing simple problem instances (CV=$4$ and CV=$3$), the accuracy improvement is not very significant when we increase the GNN rounds. Besides, the SATformer with $r=24$ shows a higher computational complexity, where # FLOPs is 228.64 M, larger than NeuroSAT 207.91 M.

In this section, we decode one of the satisfying assignments from literal embeddings, as same as the NeuroSAT Selsam et al. (2018). More specifically, we apply $k$-means to cluster the literal embeddings into two clusters ($A$ and $B$). After that, there are two possible assignments are generated, one assignment contains variables in $A$ is assigned to be true and the variables in $B$ is false; the reverse cases offer the second potential assignments.If one of the two assignments can satisfy the instance, we consider the SAT problem is solved.

The results are shown in Tab. 8. Firstly, with the same GNN message-passing rounds, SATformer solves more instances than NeuroSAT. For example, SATformer with $w=26$ solves $78\%$ instances in CV>$5$ and SR($3$-$10$). However, NeuroSAT only solves $50\%$ instances in the same dataset. We suspect the superior performance of SATformer comes from two aspects. On the one hand, SATformer learns a better representation than NeuroSAT with the Transformer-based structure to model relationships between clauses. On the other hand, conflict is strongly related to the task searching satisfying assignment in the traditional SAT solver. The model captures inevitable conflict among clauses with strong supervision from the UNSAT core. Therefore, SATformer obtains rich both clause embeddings and literal embeddings, which benefits SAT solving.

Secondly, with the decrease of instance difficulty, i.e., the decrease of CV, both SATformer and NeuroSAT solve more instances. The reason is that there are more potential satisfying assignments in the instances with lower difficulty. Although the model cannot find a clear clustering result for some variables, the produced assignment still has a high probability of satisfying the instance.

To conclude, our SATformer not only predicts satisfiability correctly for more instances but also solves more problem instances than NeuroSAT. Besides, the performance is much better when solving the instance with lower difficulty.