A Modularity-Based Random SAT Instances Generator

1 Introduction

The Boolean Satisfiability Problem (SAT) is one of the most studied problems in Computer Science. It was the first known NP-complete problem. However, many application problems (such as cryptography, hardware and software verification, planning, scheduling, among others) may be encoded into SAT, and efficiently solved by modern SAT solvers.

It is accepted that random k-CNF and industrial SAT instances have a distinct nature. While random formulas can be easily generated on demand, the set of industrial instances, which encode real-world problems, is limited. The problem of generating realistic pseudo-industrial random instances is stated in [Selman et al., 1997; Kautz and Selman, 2003; Dechter, 2003] as one of the most important challenges for the next few years. The main motivation of this challenge is improving the process of development and test of SAT solvers, and their possible specialization.

There exist a wide variety of works on the analysis of the nature of industrial SAT instances. The intuition is that these formulas have some kind of structure, which is exploited by SAT solvers. In many of these works, SAT formulas are represented as graphs, and some (graph) features are studied. The classical Erd¨os-R´enyi model has been extensively used for generating random graphs. In this model, the arity of nodes follows a binomial distribution, with small variability. This is exactly the case of random k-CNF formulas. However, the structure of most real-world problems cannot be described with this classical model, and therefore, new models have been defined. For instance, Preferential Attachment [Barab´asi and Albert, 1999] is used to explain the scale-free structure of some real networks, where the arity of nodes follows a power-law distribution, with big variability. In the context of SAT, some notions of structure have also been studied, such as the small-world property [Walsh, 1999], the scale-free structure [Ans´otegui et al., 2009a], or the centrality [Katsirelos and Simon, 2012], or the self-similarity [Ans´otegui et al., 2014], among others.

∗This work is partially supported by the CSIC project 201450E045.

There also exist many methods for generating industriallike random instances. In [Slater, 2002], it is described a method based on the characteristic path length and clustering coefficient. In [Burg et al., 2012], it is presented a generator that combines subparts of real-world instances to create new ones. In [J¨arvisalo et al., 2012], it is proposed an instance generator based on finding optimal circuits of Boolean functions. In [Ans´otegui et al., 2009b], it is used the notion of scale-free graph to generate formulas where the number of variable occurrences follows a power-law distribution.

The inspiration of this work is [Ans´otegui et al., 2012]. In that paper, it is stated that industrial SAT formulas exhibit a clear community structure (i.e. high modularity Q). This means that, representing formulas as graphs, we can find a partition of the formula into communities with many edges between nodes of the same community, and few edges connecting distinct communities. This property is very characteristic in real-world problems in contrast to randomly generated instances, where modularity is very low. In the context of SAT, it has been shown that the community structure is correlated with the runtime of CDCL SAT solvers, and the modularity is the best predictor of this runtime to date [Newsham et al., 2014]. Moreover, it has also been used to improve the performance of some solvers [Martins et al., 2013; Sonobe et al., 2014]. To the best of our knowledge, there exists no SAT instance generator considering the community structure.

In this paper, we present a new model of generation of random CNF problems based on the community structure 1 . With this new model, we can generate formulas for any given value of modularity. For a high modularity, the resulting formula is more adequate to model industrial problems than classical random k-CNF. This generator allows us to isolate the effect of modularity on the performance and behavior of SAT solvers. For instance, we show that CDCL solvers concentrate their decisions on variables of the same (or few) module along time.

The rest of the paper proceeds as follows. After some preliminaries on modularity of graphs in Section 2, we describe the generation model in Section 3. In Section 4, we show that this model works appropriately for different input values of number of variables n and clauses m. In Section 5, we show that, if the formulas exhibit a phase transition region SATUNSAT when the ratio clause/variable is increased, then it does not depend on the modularity. Finally, in Section 6, we give empirical evidence that the performance of SAT solvers is consistent with the nature of the generated formulas, i.e. SAT solvers specialized in industrial formulas work better in high modular instances than SAT solvers specialized in random k-CNF, and vice versa.

2 Preliminaries

SAT is the problem of deciding if the variables of a propositional formula can be assigned in such a way that the formula is evaluated as true. In this context, some concepts are natural: a literal is either a variable or its negation, a clause is a disjunction of literals, a conjunctive normal form (CNF) formula is a conjunction of clauses, and a k-CNF is a CNF in which all clauses have exactly k literals.

An undirected weighted graph G is a pair G = (V,w), where V is the set of nodes, and w : V × V → R+ is the edge-weight function that satisfies w(x, y) = w(y, x).

The Variable Incidence Graph (VIG) of a SAT instance Γ is the graph whose nodes represent the variables of Γ, and there exists an edge between two variables if they both appear in a clause cl. A clause with l literals results into ( l2) edges. Thus, to give the same relevance to all clauses, edges have a weight w(x, y) = ∑ cl∈Γ x,y∈cl 1/(|cl| 2 ), where |cl| = l is the length of the clause cl.

The community structure of a graph is usually measured using the notion of modularity [Newman and Girvan, 2004]. Defined for a graph G and a partition C of its vertexes into communities, the modularity Q (see Eq. 1) measures the fraction of internal edges (edges connecting vertexes of the same community) w.r.t. a random graph with same number of vertexes and same degree. This avoids that the best partition is the one made up by an only community containing all vertexes.

1 This modularity-based SAT generator is available in http://www.iiia.csic.es/˜jgiraldez/software

The modularity of a graph is the maximal modularity for any possible partition: Q(G) = max{Q(G, C) | C}.

Computing the modularity of a graph is NP-hard [Brandes et al., 2008]. Due to its complexity, instead of computing the (exact) modularity, most of methods in the literature approximate a lower-bound in the value of Q.

3 The Model

In the classical random k-SAT model, a random formula Fk(n, m) is a set of m clauses over n variables, where clauses are chosen uniformly and independently among all 2k (nk) non-trivial clauses of length k. 2 In this paper we present a new model of random formulas: the Community Attachment (CA) model. This is parametric in a probability P and a partition C of the set of variables, and it allows the generation of highly modular formulas.

Definition 1 Community Attachment. Let N be a set of n variables, a partition C of N into c communities of the same size s = n/c, with k ≤ c ≤ n/k, and a real value 0 ≤ P ≤ 1. A random formula Fk(n,m, c, P) is a set of m non-trivial clauses with k literals over the n variables, selected independently as follows. With probability P, choose a clause uniformly among all c 2k (n/c k ) clauses with all literals in the same community; and with probability 1 - P, a clause uniformly among all nk 2k ck (ck) clauses with all literals in distinct communities.

Notice that in the previous definition we need to impose the restriction k ≤ c ≤ n/k to ensure that there always exists at least one possible clause to select. Notice also that for k = 2 and P = n/c-1 n-1 we have the classical 2-SAT model: F2(n, m) = F2(n, m, c, n/c-1 n-1 ), but for bigger k the community attachment model does not subsume the classical model.

Given a SAT formula Γ with n variables and m clauses, consider the VIG G of Γ. Our model ensures a lower-bound for the modularity of this graph.

Theorem 2 Given a formula Γ ∈ Fk(n, m, c, P ), let G be its VIG. The average modularity of G is bounded as:

PROOF: Recall that modularity is defined as the maximal modularity for all possible partitions of the nodes into communities. Here we consider the partition used to generate the formula. For this particular partition, when we select a clause with all variables in the same community (with probability P), we get (k2) internal edges. The sum of the weights of the

2 A non-trivial clause of length k contains k distinct, noncomplementary literals.

Algorithm 1: Community Attachment

Input: int n, m, c, k; real Q; Output: k-CNF SAT Instance Γ 1 Γ := Ø; 2 P := Q+1/c; 3 for j ∈ {1, . . . ,m} do 4 if rand([0, 1]) ≤ P then // same community 5 r := rand({1, . . . , c}); 6 for i ∈ {1, . . . , k} do 7 Ci := r; 8 else // distinct communities 9 for i ∈ {1, . . . , k} do 10 repeat Ci := rand({1, . . . , c}); 11 until ∀i′ < i(Ci′ ̸= Ci); 12 repeat 13 Cl := Ø; 14 for i ∈ {1, . . . , k} do 15 Xi := rand({⌊(Ci-1) nc ⌋+1, . . . , ⌊Ci nc ⌋}); 16 Cl := Cl ∨ rand({-1, 1}) · Xi; 17 until ∀i′ < i(Xi′ ̸=Xi); 18 Γ := Γ ∧ Cl; 19 return Γ;

edges generated by a single clause is always 1. Therefore, the fraction of internal edges is, on average, P m m . The sum of nodes degrees is 2m, thus 2m/n is the expected node degree. Since n/c is the number of nodes per community, the sum of nodes degrees in one community is nc 2m n .

Summarizing, for this partition C, we get

that is a lower-bound for the modularity.

When P is big enough, the modularity is very close to this lower-bound, because the partition used in the formula generation is highly modular. Therefore, we can use the previous theorem to generate formulas with a desired modularity Q. We simply take:

which ensures at least a modularity Q. In practice, as we will see in Section 4, the formulas we obtain have a modularity Q ≈ P - 1c , except when P and m/n are small.

In Alg. 1, it is described in detail an implementation of a generator of community attachment random formulas from Fk(n,m, c, P). Using P = Q+ 1c these formulas will have an expected modularity close to Q.

4 Validation of the Model

In order to analyze the community structure of the SAT instances obtained with our model, we have generated some sets of random formulas for different values of Q ∈ {0.9, 0.8, 0.7, 0.5, 0.3} (hence P = Q + 1/c). Remark that the modularity Q of (real) industrial SAT instances is usually greater than 0.7, while no modularity greater than 0.3 is found for classical random k-CNF formulas. Moreover, the number of communities c is usually in (10, 100) [Ans´otegui et al., 2012]. In Fig. 1, we analyze their modularity Q and their number of communities c, varying the number of variables n and the clause/variable ratio m/n (we fix m/n = 4 and n = 1000 respectively). We use the algorithm described in [Ans´otegui et al., 2012] to compute an approximation for Q and c. In fact, this algorithm computes a lower-bound for Q. The dispersions of the approximated Q and c are very small, so they are not shown in the plots.

We observe that the modularity Q and the number of communities c are almost unaffected by these variations of n and m/n. In general, the approximation computed for Q is slightly smaller than expected, and the partition into communities is also very similar to the partition used in the generation. Recall that the algorithm used to approximate Q returns a lower-bound of it. For small values of m/n and P , the number of clauses relating variables of the same expected community is very small. This produces the existence of some unconnected sub-communities within each expected community. Hence, c and Q are much greater than expected, and Q cannot be estimated as P - 1/c. When we generate formulas with small values of P , e.g. Q = 0.3 and c = 40, we observe that, although the formulas have a guaranteed lower-bound of Q ≥ 0.3, the computed approximation of Q is smaller (close to 0.2 when n ≈ 20000). The number of communities is also smaller than expected. In this case, this error is not produced by our model. It is due to the greediness of the algorithm used to approximate Q, which is not able to find a similar partition to the one used in the generation.

5 Phase Transition

In classical random k-CNF instances, some interesting properties, as the satisfiability or the hardness, are correlated to the clause/variable ratio m/n [Mitchell et al., 1992]. The Satisfiability Threshold Conjecture, which remains open, suggests that it may exist a critical ratio r, such that below this point all formulas are SAT (under-constrained) and above it they are UNSAT (over-constrained) with uniformly positive probability, when n tends to infinity. Experimentally, this phase transition point has been shown to be around r ≈ 4.26 for k = 3. Moreover, the hardness of these instances is also characterized by this parameter: closer to this ratio, harder the instance.

In this section we check if this phenomenon also exists in the random SAT instances generated with our model, and if the new transition point, noted r′ , differs from the classical r′ ̸= r. In Fig. 2, we represent the fraction of UNSAT instances for some sets of random formulas with distinct Q, varying the clause/variable ratio m/n. We observe that the fraction of UNSAT formulas increases with m/n. Therefore, for small (big) values of m/n, nearly all formulas are SAT (UNSAT). When Q is small, the value r′ is close to the classical r ≈ 4.26. Recall that when P ≈ 1/c, our model is quite similar to the classical random k-SAT model. However, we also observe that, when Q increases, r′ decreases. The natural question is if this decrease in r′ is also valid for n tending to infinity. In our experimentation we use the biggest value of n allowing us to get a solution in less than 3 hours (see Table 1).

In order to explain this decrease in the phase transition point r′ , and predict the behavior when n tends to infinity, we will consider the extreme case with P = 1. In these formulas, clauses only contain variables of the same community. Therefore, the formula is composed by c unconnected sub-formulas, and the whole formula is UNSAT if, and only if, at least one of the sub-formulas is UNSAT. Moreover, in this extreme case, all sub-formulas follow the classical model Fk(n/c,m′ ), for some m′ . On average, all sub-formulas contain E[m′ ] = m/c clauses; and all of them contain s = n/c variables. Hence, the average clause/variable fraction in subformulas is also E[m′/s] = m/c n/c = m/n. However, even when the fraction m/n is smaller than the classical r (and so the expected clause/variable ratio of the formula), with some probability, some of the sub-formulas may get a large portion of clausesm′ such that m′ n/c > r. This makes that sub-formula UNSAT with high probability. This has the effect of decreasing the phase transition point for finite n and c.

When n/c tends to infinity, the situation is completely different as the following theorem states.

Theorem 3 The set of formulas Fk(n,m, c, P) with P = 1 has a phase transition point r′ at the same clause/variable ratio r of the classical Fk(n,m).

PROOF: Let r′ = m/n and r be the classical phase transition point. The minimal r′ such that the probability that some of the sub-formulas has more than r s clauses (hence it is UNSAT with high probability when s tends to infinity), will be the phase transition point for this special case P = 1 of our model.

The probability that a given community Ci contains r s clauses when the formulas has m clauses is

Suppose that the formula has m = r′ n clauses. Recall also n = c · s. We also assume that both the number of communities c and their size s tend to ∞.

When m, n → ∞, and m/n → ∞, the binomials (mn ), may be approximated as:

using the middle value in the numerator, and the Stirling approximation in the denominator.

When c → ∞, we can also approximate

Replacing these two approximations, and m = r′ c s we get

For s, c →∞, this function is dominated by the exponential factor

The base of the exponentiation is strictly smaller than one except for r = r′ . Therefore, when the number of communities and their size both tend to infinity, even in the extreme case P = 1, the probability that the formula is UNSAT is zero, for r′ < r, i.e. the phase transition point is the same as for the classical random formulas.

In the case that c is finite, the approximation we have used for the binomial is not correct. When k is constant and n → ∞, we may use

In this case we get

Like in the previous case, the base of the exponentiation is one, only when r′ = r. Therefore, the phase transition point is just the same.

6 SAT Solvers Performance

In this section we show that industrial-specialized SAT solvers exploit the community structure of the formula, whereas random-specialized solvers do not.

In Fig. 3 we show which variable is decided along the execution of MiniSat [E´en and S¨orensson, 2003] on one of our random SAT instances. Notice that our generator assigns consecutive numbers to all variables of the same community. We observe that the solver is focused on only one community, only deciding variables of this community, and it changes to another, from time to time.

Finally, in Fig. 4 we compare the performance of the SAT solvers Glucose [Audemard and Simon, 2009] and March [Heule et al., 2004] over some sets of SAT formulas generated with our model, with distinct modularity values.

While Glucose is a CDCL SAT solver which has been shown very good for solving industrial problems, March is a lookahead SAT solver commonly used to solve random k-CNF instances. For high modularities (see Q = 0.9), Glucose solves all the instances, but March is only able to solve few UNSAT instances. More precisely, they are the ones in which there exists a very small unsatisfiability core, composed of variables of one or few communities. Notice that higher the modularity, more likely to find these instances with small refutations. It is also interesting to remark that Glucose also finds UNSAT formulas easier than SAT formulas, for high modularity. As Q decreases, March is able to solve more instances (see Q = 0.7), and it starts to be as fast as Glucose, if it is not faster, when the modularity is small enough (see Q = 0.5). Finally, when Q is very small (see Q = 0.3), March is able to solve all the instances but Glucose only solves few of them. The number of variables used in each set is not the same (see Table 1). We can also conclude that high modularity makes formulas easier to be solved by CDCL SAT solvers. This was also shown in [Newsham et al., 2014].

7 Conclusions

In the SAT community, it is accepted that industrial problems exhibit some kind of structure that is exploited by modern solvers. Nowadays, one of the most intriguing problems in this community is to better characterize this structure, with the aim of develop random SAT instances generation models that capture realistically the features of industrial problems, for SAT solving testing purposes.

Recently, the notions of community structure and modularity have been used with success to explain the structure of SAT instances [Ans´otegui et al., 2012], and their hardness [Newsham et al., 2014]. Using these concepts, we present a modularity-based generator, which generates random k-CNF SAT instances of any desired modularity Q.

Industrial problems are characterized by a high modularity. Therefore, our model can generate more realistic pseudoindustrial random formulas on demand. We validate the adequacy of this model checking that (i) the community structure of the resulting formulas is the expected, (ii) if there exists a phase transition region SAT-UNSAT characterized by the clause/variable ratio, it is independent on the modularity, and (iii) the SAT solvers performances are consistent to the formulas of our modularity-based generator, i.e. SAT solvers specialized in industrial (random) problems perform better in high modular (low modular) instances generated by our model, and vice versa.