Owing to their high eficiency, state-of-the-art solvers are applied to solve a wide range of computational problems for industrial purposes. The satisfiability problem (SAT) is a well-known NP-complete problem, and SAT solvers are the applications for solving SAT. The high performance of SAT solvers is attributed to the exploitation of the underlying structure of industrial SAT problems. Industrial problems derived from real-world problems exhibit more biased and prominent structural properties compared to random ones. However, research has shown that clause learning, an essential technique of modern SAT solvers, decreases the degree of structure of industrial problems. This study intends to answer 'why learnt clauses are efective though they destroy the structure of problems -the hypothetical source of eficiency?' . We hypothesize that this can be explained by the diference in the quality of clauses; the quality of the learnt clause correlates to the change in structure, and high-quality (useful) clauses destroy the structure less. To verify this, we investigated the time variance of two structural measures, treewidth and modularity, throughout the search process to observe the impact of learning. Additionally, we analyzed the relationship between the quality of a learnt clause, measured by the literal block distance (LBD), and its efect on the structural changes, measured by the modularity. Our findings include the following: (1) The value of these measures does not change monotonically rather it fluctuates over time. (2) The efect of learnt clauses on the structural change is correlated with these qualities -low-quality clauses characterized by large LBD values tend to decrease modularity more than high-quality clauses with small LBD values, and vice versa. These findings determine the relationship between the quality of learnt clauses and their impact on the structure of a SAT problem. The study suggests potential avenues for developing methods for a more efective evaluation of learnt clauses based on structural measures.
The Boolean satisfiability problem (SAT) is a well-known NP-complete problem; thus, problems
containing numerous variables are considered computationally intractable. However, in practice,
conflict-driven clause learning (CDCL) SAT solvers, which are applications widely used for
solving SAT problems, occasionally solve problems with millions of variables in a reasonable
time (e.g., a few minutes or hours). This gap between theoretical understanding and practical
results may originate from the structure of SAT problems. Unlike random SAT problems used
in theoretical research, industrial problems derived from real-world problems exhibit biased
and prominent structural properties. These structural properties are quantified by measures
such as backdoors [
Although the original industrial problems exhibit properties distinct from those of random
problems, some studies [
To address this question, we focus on the clause quality and clause deletion procedure based on the quality measures. Solvers obtain learnt clauses at every conflict during the search process, which can result in the acquisition of millions of clauses. Retaining all these clauses is neither practical nor eficient, considering the memory requirements and the impact on the search eficiency of propagation. Consequently, modern SAT solvers delete learnt clauses based on the quality of these clauses. Based on the learning procedure, our hypothetical story to answer the above question is as follows: • Through the deletion process, high-quality clauses are maintained in the solver, whereas low-quality ones are deleted. Furthermore, high-quality clauses are more frequently used (i.e., propagated or analyzed) than low-quality ones. • Although the structure of the problem may explain the eficiency of the solver, learnt clauses are known to decrease the structural properties. • High-quality clauses decrease less or even increase the structural properties of SAT problems; in contrast, low-quality clauses decrease them. • This results in maintaining or even increasing the actual structural properties because of the deletion and less usage of lower-quality clauses.
• This maintained structure contributes to finding solutions even in large-size problems.
To validate this hypothesis, this study aims to understand the relationship between the quality and structural measures of learnt clauses through experimental analysis. We investigated the changes of two measures, treewidth and modularity, throughout the search process. Additionally, we analyzed the relationship between the quality of a learnt clause and its efect on the change in the modularity value. The objective of the analysis is to understand: how much and when the value of structural measures changes by the learnt clauses; and which quality of the learnt clauses changes these values more. The findings of this study provide a deep understanding of clause learning and deletion, as well as the relationship between the problem structure and clause learning.
The remainder of this paper is organized as follows: Section 2 introduces SAT solvers and structural measures. Section 3 presents the results of experimental observations. Section 4 summarizes the paper and suggests future research directions.
The SAT problem is a decision problem of the Boolean formula. A Boolean formula is an
expression that uses the logical operators AND, OR, and NOT to combine Boolean variables,
which can only hold True or False values. The SAT problem asks if a true/false assignment
exists to variables in a Boolean formula that makes the whole formula true, and it is a famous
NP-complete problem. SAT solvers are algorithmic applications designed to solve SAT problems,
using various techniques to find a satisfying assignment of variables (satisfiable, SAT) or
determine that no such assignment exists (unsatisfiable, UNSAT). CDCL is a major algorithm
adopted by many solvers. State-of-the-art CDCL solvers occasionally solve problems with
even more than one million variables and clauses. Owing to their eficiency, they are used
to solve real-world problems such as computer-aided proofing [
A key function of CDCL solvers is clause learning [
The size and literal block distance (LBD) [12] are two popular measures for evaluating the quality of learnt clauses. The size of the clause is defined as the number of literals contained in the learnt clause. A literal is a variable or the negation of a variable. For a clause comprised of literals {1, 2, . . . , }, the clause size is calculated as: || = . The smaller the clause size is, the more useful the clause is evaluated to be. LBD is a more efective measure, defined as the count of distinct decision levels to which the literals of a clause belong. For a clause with literals from decision levels {1, 2, . . . , }, LBD is given as:
LBD() = |{1, 2, . . . , }| A lower LBD value suggests a high degree of interaction among the literals in the clause in the implication graph, enhancing the potential of the clause for efective search space pruning. Therefore, CDCL solvers prefer learnt clauses with lower LBD values. Owing to the efectiveness of LBD, the LBD score has been used not only for learnt clause management but also for other heuristic techniques (e.g., restart strategy [13] and decision branching heuristic [14]).
The input for the SAT solver is usually given in the conjunctive normal form (CNF). A formula is said to be in CNF if it is a conjunction of one or more clauses, where a clause is a disjunction of literals. An example of a CNF formula is ( ∨ ) ∧ (¬ ∨ ), where ( ∨ ) and (¬ ∨ ) are clauses, and , , and ¬, and are literals. Industrial SAT problems indicate prominent structural properties. Examples of structural measures are treewidth and modularity. For the graph representation of a SAT problem to calculate these measures, a variable incidence graph (VIG) is widely used. weight is defined as (, ) = ∑︀∈,,∈ 1/(︀ |2|)︀ .
Definition 1. Variable incidence graph (VIG):
A VIG is a graph representation of logical expressions. Let be a SAT problem for a set of variables and clauses . The nodes of the VIG are denoted by , and the edge , ∈ between and ∈ denotes the existence of a clause ∈ containing , in . The edge
Both the and ¬ literals belong to node in VIG. When the same pair of variables (, ) appears more than once in , () sums all the weights of pairs. This means that the shorter the clause becomes, the higher the edge weight is, and vice versa. In this study, we used VIG as a graph representation of the SAT problem. The two structural measures, treewidth and modularity, are calculated on the VIG.
Treewidth characterizes the degree of resemblance of a given graph to a tree. The smaller the treewidth, the more the graph resembles a tree. For a graph = (, ), the treewidth is defined as the size of the largest bag (subgraph) in the optimal tree decomposition of the graph minus one.
tw() = min max || − 1
T ∈ ( ) (1) Here, = ( ( ), ( )) is a tree of , and ⊆ for ∈ ( ) represents a bag in the decomposition. The following conditions must hold: ⋃︀∈ ( ) = : Every vertex in is included in at least one bag; for every edge (, ) ∈ , there exists a bag such that , ∈ . For all , , ∈ | ∈ ( ), if is on the path from to in , then ∩ ⊆ ; the bags that contain a particular vertex in must form a connected subtree in .
This concept involves decomposing a graph into a tree-structured collection of subgraphs.
Each subgraph contains a vertex subset. Treewidth is a useful parameter for various
computational problems, as many NP-hard graph problems can be solved in polynomial time for
graphs of bounded treewidth [15]. For this reason, the relationship between the hardness of
SAT problems and the value of treewidth has been widely studied [
Modularity evaluates the quality of a given partition of the input graph. For a weighted edge graph = (, ) and a partition = {1, 2, ..., } of its vertices , where is pairwise disjoint and ⋃︀ =1 = , the modularity is computed as follows: (, ) = 1 ∑|︁| ∑|︁| [︂ 2 =1 =1 − () × () ]︂ 2 (, ) (2)
Here, is the element at the -th row and -th column of the adjacency matrix of the graph , () denotes the sum of the weights of the edges connected to vertex , equals the sum of the weights of all edges in the graph, ∈ is the community to which vertex belongs, and (, ) equals 1 if vertices and belong to the same community (i.e., = ), and 0 otherwise.
A community in a graph is defined as a group of vertices more densely connected internally than the rest of the graph. The division of a graph into such communities is often denoted as a partition. Modularity quantifies the degree of deviation of the number of edges within communities from a random distribution. A high modularity score suggests that the graph exhibits a robust community structure. The following subsection introduces various research regarding the modularity and structures of SAT.
Ferrara et al. [
First, we assessed how much and when learning changes the structural measures. Related works
[
The scatterplot in Figure 1a reveals the variation in the treewidth value between and . Let be the original problem and be the learnt clauses maintained by the solver at time . is the result of clauses learnt and deleted up to point . The time when the search is finished is , which is either at the 3600 s timeout or when the solver finds a SAT or UNSAT solution. The problem at time is defined by + ; thus = + . Hereafter, refers to the graph of the problem. A dot in the scatter plot figure represents a problem, and its position (original, last) represents the values of treewidth tw( ) and tw( ), respectively. In 78% of problems, treewidth( ) < treewidth( ) were observed, and in particular, 11% of problems have the value changed by a factor of 10 or more. Note that the figure is on a double-logarithmic graph. Similarly, Figure 1b details the modularity value for each problem. This result also reveals modularity( ) > modularity( ) for 84% of the problems. In particular, there were 64% of problems that showed almost zero values below 0.05. These results are consistent with those of existing studies; The learning changes the structure toward the random-like one —in other words, the learning destroys the structure.
Next, Figure 2 details the temporal change of the values of the measures, showing four problems as typical examples. Similar trends are observed in most problems, as seen in [20]. The left and right vertical axes indicate the modularity value and treewidth, respectively. The horizontal axis indicates the time series: ‘original’ indicates the values of , original CNF graph before preprocessing; ‘0’ is the value of the graph of the preprocessed formula. We observed these measures approximately every 300 s until . The figures claim two arguments. First, the values of measures change immediately after starting the search, particularly between 0 and 300 s, and do not vary monotonically. Second, the measures oscillate back in a zigzag 1.E+010.E+00 1.E+01 1.E+02 1.E+03 1.E+04 1.E+05 1.E+06
Original state (a) treewidth 0.0 0.2 0.8
1.0 0.4 0.6
Original state (b) modularity manner as time progresses. This phenomenon is assumed to occur as the result of the deletion of learnt clauses. These results suggest a hypothetical explanation: the deletion of badly evaluated clauses with large LBD values restores the changed structure; and thus, the deletion of learnt clauses is efective for solver performance because of the power of structure restoration. modularity treewidth modularity treewidth original 0 300 600 900 1200 1500 1800 2100 2400 2700 3000 3300 3594 (a) ktf_TF-3.tf_2_0.02_24 modularity treewidth
We hypothesize that high-quality clauses decrease less the structural properties of SAT problems less than low-quality clauses, or even increase them. If this is true, it will resolve the contradiction between the explanation that the structure of the problem is a factor in the eficiency of the SAT solver and the observation that learnt clauses increase the eficiency of the SAT solver while destroying the structure of the problem. We conducted an experiment to identify which learnt clause changed the structure more. We analyzed the relationship between LBD and the degree of change by comparing the delta of the modularity Q between and + a learnt clause , namely, delta with the addition of a learnt clause.
Definition 4. For a learnt clause , Δ() = ( + , ′) − ( , ).
Modularity requires a graph and its partition . The calculation of partition (community) detection costs numerous resources for millions of learnt clauses. Therefore, we calculated Δ with two assumptions: partition does not change by adding a clause, that is, ′ = ; the change in , i.e., the sum of the weight of all edges, can be ignored by adding a clause with weight 1. These assumptions are reasonable when adding at most one learnt clause to the original problem that has thousands of clauses. We ran Glucose 4.2.1 with a 3600 s time limit to export all the learnt clauses and their information, such as LBD and its literals, to files. The export was conducted when learnt clauses were obtained, updated, or deleted. The clause was determined to be the same as literal identity.
Four typical examples are depicted in Fig 3 as boxplots of the Δ distribution for each LBD. Each chart shows the median as the orange line, quartiles as the edges of the box, and outliers as the circles if data points are more than 1.5 times the interquartile box. Clear trends are observed in these figures —the smaller the LBD is, the larger the average Δ is. This result indicates that better clauses (smaller LBD clauses) slightly decrease or even increase the modularity value. This trend was observed among most problems, as shown in [20]. We analyzed the diferences between all the clauses and the clauses of LBD 2 to determine the overall trend among all problems. The average Δ for all clauses across problems was − 5.3 × 10− 5, with 76% displaying a negative mean Δ. In contrast, clauses with an LBD of 2 had a mean Δ of − 4.4 × 10− 5, and 68% exhibited negative values. These results show that clauses with small values of LBD (here LBD of 2) are not necessarily positive clauses, while the percentage of clauses with positive Δ is high (i.e., enhancing the structure of the problem). This supports our hypothesis that ‘high-quality clauses decrease the structural properties of SAT problems less than low-quality clauses, or even increase them.’
Conversely, to see what characteristics are present in clauses with positive Δ values, a comparative analysis was performed between clauses with positive Δ and any Δ. Mean LBD values and the number of communities per problem for each set of learned clauses were calculated. The aggregate means are shown in Table 1. Similar to the boxplot, positive Δ clauses had lower LBD values and fewer community afiliations. Moreover, as anticipated, clauses characterized by a positive Δ were afiliated with a smaller number of communities. Ansótegui et al.,[16] revealed that although most of the learnt clauses decreased the modularity value, some clauses increased it. Combining this with our results suggests that learning lowquality clauses decreases modularity, and learning high-quality clauses slightly decreases or ltQ 0 a e d ltaQ 0 e d 2 1 1 2 4 2 2 4 6 1.0 0.5 taQ 0.0 l e d 0.5 1.0 1 2 3 4 5 6 7 8 9101112131415161718192021222324252627282930
LBD 1 2 3 4 5 6 7 8 9101112131415161718192021222324252627282930
LBD even increases modularity.
The previous analysis showed that high-quality clauses (measured by LBD values) have a small impact on the decrease of modularity (i.e., Δ). However, this is probably because of the pseudo-correlation with size, not between LBD and Δ, because modularity is a measure on the graph, LBD is correlated with the size of the clause, and the size strongly influences the VIG weight. To analyze the impact solely based on the LBD values excluding the impact of size, we visualized the correlation as a heatmap among the clause size, LBD, and mean Δ in Figure 4. The color of each cell represents the mean of Δ, and the vertical and horizontal axes represent the LBD and clause size, respectively. When examining colors vertically for a given size, a notable diference is observed —smaller LBD values correspond to larger average values of Δ. These results support the argument presented in Figure 3. The complete results of all problems are available in [20] where most of the problems show a similar trend.
Furthermore, we analyzed the overall trend of all problems by calculating the partial correlation coeficients of the LBD, size, and Δ values to confirm the above implication from the observations. A partial correlation coeficient measures the relationship between two variables when one variable is held constant. This assesses the pure correlation between two variables, excluding the influence of other variables. To define the partial correlation coeficient, we consider three random variables , , . The partial correlation coeficient of and is denoted as ., and the following formula can be derived: . = √︁(1 − 2)(1 − 2)
− . Here, represents the correlation coeficient of and , and is the control variable of . calculating the correlation coeficient of , without the influence of . The partial correlation coeficients were found to be +0.54 between the size and LBD, − 0.09 between the size and Δ, and − 0.24 between LBD and Δ, respectively. These results indicate that LBD and Δ weakly correlate, even without any outlier operation, and allow us to conclude that the value of LBD afects the value of Δ. This could explain the efectiveness of the three-tier scheme for clause management. The clauses that can enhance the structure remain in tier 1 (measured by LBD), and those that destroy the structure are put in tier 3 and will be removed soon.
This study explored the impact of clause learning in CDCL SAT solvers on the structural properties of SAT problems, focusing specifically on two measures: treewidth and modularity. The investigation was organized around two key experiments: the time variance in these measures during the search process to assess the impact of clause deletion, and the relationship between the quality of a learnt clause and its subsequent efect on modularity.
The first experiment revealed that these measures do not change monotonically but fluctuate periodically. This fluctuating pattern is due to the continuous interplay of clause learning and deletion processes, indicating that clause deletion can restore the changed structure. This implies diferences in the impact of the structural change between the deleted and remaining clauses. The second experiment showed that the quality of learnt clauses, measured by LBD values, was a significant factor impacting structural changes; low-quality clauses, characterized by large LBD values, were found to decrease in modularity more than high-quality clauses. This result explains the fluctuation in the first experiment. More importantly, it resolves the question of ‘why learnt clauses are efective though they destroy the structure of problems?’ . The learnt clauses as a whole (considering all obtained clauses) tend to decrease the structural properties of problems, but the actual structural properties are maintained or even increased owing to high-quality clauses. These insights can potentially inform that the benefits of clause deletion are beyond addressing memory constraints and reducing the propagation time —forgetting 3 6 9 21 51 18 21 24 27 30 33 36 93 42 45 48 51 54 57 60 63 66 69 72 76 size 2 6 01 41 18 22 26 30 34 38 42 46 05 54 58 62 66 70 74 78 82 86 90 94 98 size 2 6 01 41 18 22 26 30 34 38 42 46 05 54 58 62 66 70 74 78 82 86 90 94 98
size 2 6 01 41 18 22 26 30 34 38 42 46 05 54 58 62 66 70 74 78 82 86 90 94 98
size low-quality learnt clauses helps restore the distinct structural properties of problems to maintain the problem ‘structured’, enabling its eficient solution.
In future research, exploring similar studies employing other measures, such as scale-free and centrality, could ofer further insight into our current findings. The interrelation between the degree of modularity changes (Δ) and the consequent efect on the solver runtime presents yet another intriguing area of study. If a robust correlation in the runtime is found, Δ or other structural measures could provide efective evaluation measures for the quality of learnt clauses. They could even replace traditional measures, such as LBD or size; for instance, a clause that increases the structural measure might be deemed beneficial. Beyond modularity Δ, other structural measures also warrant consideration for this purpose and can enhance the performance of CDCL SAT solvers. Moreover, these measures could be invaluable specifically for parallel learnt clause sharing. As LBD is derived from the solver decision tree, it inherently depends on the state of the search. Given that each parallel worker would operate in a distinct state of search, this inevitably results in diferent decision trees and LBD values. This suggests that basing the decision of learnt clause sharing on LBD might not be the most efective approach. On the other hand, structural measures derived from the original instance, such as Δ employed in this study, potentially ofer better solutions. These measures are common information available to all parallel workers and can thus provide a unified measure to judge the usefulness of clauses.
We express our deep gratitude to the reviewers for their insightful comments and to participants at the Pragmatics of SAT workshop for enriching discussions. We also wish to acknowledge the meaningful discussion with Professor Hiroshi Imai and the members of his laboratory. boolean satisfiability solver, in: IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281), 2001, pp. 279–285. doi:10.1109/ICCAD.2001.968634. [12] G. Audemard, L. Simon, Predicting learnt clauses quality in modern SAT solvers, in: Proceedings of the 21st international jont conference on Artifical intelligence, IJCAI’09, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2009, pp. 399–404. URL: https://dl.acm.org/doi/10.5555/1661445.1661509. [13] A. Biere, A. Frohlich, Evaluating cdcl restart schemes, in: Proceedings of Pragmatics of SAT 2015 and 2018, volume 59 of EPiC Series in Computing, EasyChair, 2019, pp. 1–17. doi:10.29007/89dw. [14] W. Chang, G. Wu, Y. Xu, Adding a lbd-based rewarding mechanism in branching heuristic for sat solvers, in: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE), 2017, pp. 1–6. doi:10.1109/ISKE.2017.8258780. [15] E. C. Freuder, Complexity of k-tree structured constraint satisfaction problems, in: Proceedings of the Eighth National Conference on Artificial Intelligence - Volume 1, AAAI’90, AAAI Press, 1990, p. 4–9. URL: https://dl.acm.org/doi/10.5555/1865499.1865500. [16] C. Ansótegui, J. Giráldez-Cru, J. Levy, L. Simon, Using community structure to detect relevant learnt clauses, in: Theory and Applications of Satisfiability Testing – SAT 2015, Springer International Publishing, 2015, pp. 238–254. doi:10.1007/ 978-3-319-24318-4\_18. [17] M. Hamann, B. Strasser, Flow-cutter-pace17, 2017. URL: https://github.com/kit-algo/ lfow-cutter-pace17, last accessed: 2023-04-17. [18] Networkx: Modularity, https://networkx.org/documentation/stable/reference/algorithms/ generated/networkx.algorithms.community.quality.modularity.html, 2023. Last accessed: 2023-04-17. [19] G. Simon, Laurent; Audemard, About the glucose sat solver, 2018. URL: https://www.labri.
fr/perso/lsimon/research/glucose/, accessed: 2023-3-8. [20] Image repository for all instances, https://github.com/messhiida/PoS2023-images.git, 2023.
Last accessed: 2023-05-03.