# a_modularitybased_random_sat_instances_generator__b7287f01.pdf

A Modularity-Based Random SAT Instances Generator

Jes us Gir aldez-Cru and Jordi Levy IIIA - CSIC Campus UAB, Bellaterra, Spain {jgiraldez,levy}@iiia.csic.es

Nowadays, many industrial SAT instances can be solved efficiently by modern SAT solvers. However, the number of real-world instances is finite. Therefore, the process of development and test of SAT solving techniques can benefit of new models of random formulas that capture more realistically the features of real-world problems. In many works, the structure of industrial instances has been analyzed representing them as graphs and studying some of their properties, like modularity. In this paper, we use modularity, or community structure, to define a new model of pseudoindustrial random SAT instances, called Community Attachment. We prove that the phase transition point, if exists, is independent on the modularity. We evaluate the adequacy of this model to real industrial problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure.

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

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

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. 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

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)

structure. In this paper, we present a new model of generation of random CNF problems based on the community structure1. 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 l 2 edges. Thus, to give the same relevance to all clauses, edges have a weight w(x, y) = P

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.

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

Q(G, C) = X

x,y Ci w(x, y)

x,y V w(x, y)

x Ci deg(x))

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 n k

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 nk2k

ck c k 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:

c 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 k 2 internal edges. The sum of the weights of the

2A 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 Γ

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

8 else // distinct communities

9 for i {1, . . . , k} do

10 repeat Ci := rand({1, . . . , c});

11 until i < i(Ci = Ci);

13 Cl := Ø;

14 for i {1, . . . , k} do

15 Xi := rand({ (Ci 1) n

c +1, . . . , Ci n

16 Cl := Cl W rand({ 1, 1}) Xi;

17 until i < i(Xi = Xi);

18 Γ := Γ V 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 n

n . Summarizing, for this partition C, we get

E[Q(G, C)] = Pm

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 1

c, 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 + 1

c 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

0 5000 10000 15000 20000

Q=0.9 Q=0.8 Q=0.7 Q=0.5 Q=0.3

0 1 2 3 4 5 6 7 8 9 10

Q=0.9 Q=0.8 Q=0.7 Q=0.5 Q=0.3

0 5000 10000 15000 20000

Q=0.9 Q=0.8 Q=0.7 Q=0.5 Q=0.3

0 1 2 3 4 5 6 7 8 9 10

Q=0.9 Q=0.8 Q=0.7 Q=0.5 Q=0.3

Figure 1: Approximations of modularity Q (top) and no. of communities c (bottom) of some sets of random SAT formulas, varying the number of variables n with m/n = 4 (left), and varying the clause/variable ratio m/n with n = 1000 (right). Each plotted data is the mean of 50 instances. The input number of communities c is fixed to 40.

Q r n solver R S [R] 0.9 4.06 5000 Glucose 80.86 125.28 0.8 4.11 2000 Glucose 291.87 1217.23 0.7 4.13 1200 Glucose 211.64 791.76 0.5 4.18 600 March 544.19 1051.81 0.3 4.24 600 March 3492.36 3117.23

Table 1: Phase transition point r of some sets of 200 random SAT instances with k = 3, c = 40 and varying Q. We also report the number of variables n, the solver and runtime R (mean R and standard deviation S [R]) needed to solve them.

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 clauses m 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

3.7 3.75 3.8 3.85 3.9 3.95 4 4.05 4.1 4.15 4.2 4.25 4.3 4.35 4.4

Percentage UNSAT formulas (%)

Q = 0.9 Q = 0.8 Q = 0.7 Q = 0.5 Q = 0.3

Figure 2: Fraction of UNSAT formulas for some sets of 200 random SAT formulas with k = 3, c = 40, and varying the clause/variable ratio m/n (see the number of variables n of each family in Table 1).

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

P(Ci is UNSAT) =

m r s (c 1)m r s

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 m n , may be approximated as: m n

= m (m 1) (m n + 1)

n! (m n/2)n

2πn(n/e)n =

= mn 1 1 2m/n 2m

2πn(n/e)n mn(1/e)n2/2m

2πn(n/e)n =

m e n en/2m

using the middle value in the numerator, and the Stirling approximation in the denominator. When c , we can also approximate

(c 1)m r s = cm r s (1 1/c)c m rs

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

P(Ci UNSAT) 1

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

P(Ci UNSAT) = O r

0 2000 4000 6000 8000 10000 12000 14000 16000 18000 20000

Decision along time

Figure 3: Decided variables along the execution of Mini Sat on a random instance with n = 1000, m = 4200, k = 3, c = 10 and Q = 0.8.

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 kn n

In this case we get

P(Ci UNSAT) = O

r c 1 (c 1) r

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 Mini Sat [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.

0.01 0.1 1 10 100 1000 10000 100000

Runtime March

Runtime Glucose

0.01 0.1 1 10 100 1000 10000 100000 Runtime Glucose

0.01 0.1 1 10 100 1000 10000 100000 Runtime Glucose

0.01 0.1 1 10 100 1000 10000 100000

Runtime March

Runtime Glucose

0.01 0.1 1 10 100 1000 10000 100000 Runtime Glucose

Q = 0.3 UNSAT SAT f(x)=x

Figure 4: Relation between the runtimes (seconds) of Glucose and March, for some sets of 200 random SAT instances with Q {0.9, 0.8, 0.7, 0.5, 0.3}, k = 3 and c = 40 at the phase transition point. (i.e., using families of Table 1). The timeout is set to 3 hours.

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.

References [Ans otegui et al., 2009a] Carlos Ans otegui, Maria Luisa Bonet, and Jordi Levy. On the structure of industrial SAT instances. In Proc. of CP 09, pages 127 141, 2009. [Ans otegui et al., 2009b] Carlos Ans otegui, Maria Luisa Bonet, and Jordi Levy. Towards industrial-like random SAT instances. In Proc. of IJCAI 09, pages 387 392, 2009. [Ans otegui et al., 2012] Carlos Ans otegui, Jes us Gir aldez Cru, and Jordi Levy. The community structure of SAT formulas. In Proc. of SAT 12, pages 410 423, 2012. [Ans otegui et al., 2014] Carlos Ans otegui, Maria Luisa Bonet, Jes us Gir aldez-Cru, and Jordi Levy. The fractal dimension of SAT formulas. In Proc. of IJCAR 14, pages 107 121, 2014. [Audemard and Simon, 2009] Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Proc. of IJCAI 09, pages 399 404, 2009. [Barab asi and Albert, 1999] Albert L. Barab asi and R eka Albert. Emergence of scaling in random networks. Science, 286:509 512, 1999. [Brandes et al., 2008] Ulrik Brandes, Daniel Delling, Marco Gaertler, Robert G orke, Martin Hoefer, Zoran Nikoloski, and Dorothea Wagner. On modularity clustering. IEEE Trans. on Knowledge and Data Engineering, 20(2):172 188, 2008. [Burg et al., 2012] Sebastian Burg, Michael Kaufmann, and Stephan Kottler. Creating industrial-like SAT instances by clustering and reconstruction. In Proc. of SAT 12, pages 471 472, 2012. [Dechter, 2003] Rina Dechter. Constraint Processing. Morgan Kaufmann, 2003. [E en and S orensson, 2003] Niklas E en and Niklas S orensson. An extensible SAT-solver. In Proc. of SAT 03, pages 502 518, 2003. [Heule et al., 2004] Marijn J. H. Heule, Joris E. van Zwieten, Mark Dufour, and Hans van Maaren. March eq: Implementing additional reasoning into an efficient lookahead SAT solver. In Proc. of SAT 04, pages 345 359, 2004. [J arvisalo et al., 2012] Matti J arvisalo, Petteri Kaski, Mikko Koivisto, and Janne H. Korhonen. Finding efficient circuits for ensemble computation. In Proc. of SAT 12, pages 369 382, 2012. [Katsirelos and Simon, 2012] George Katsirelos and Laurent Simon. Eigenvector centrality in industrial SAT instances. In Proc. of CP 12, pages 348 356, 2012. [Kautz and Selman, 2003] Henry A. Kautz and Bart Selman. Ten challenges redux: Recent progress in propositional reasoning and search. In Proc. of CP 03, pages 1 18, 2003.

[Martins et al., 2013] Ruben Martins, Vasco M. Manquinho, and Inˆes Lynce. Community-based partitioning for maxsat solving. In Proc. of SAT 13, pages 182 191, 2013. [Mitchell et al., 1992] David Mitchell, Bart Selman, and Hector Levesque. Hard and easy distributions of SAT problems. In Proc. of AAAI 92, pages 459 465, 1992. [Newman and Girvan, 2004] Mark E. J. Newman and Michelle Girvan. Finding and evaluating community structure in networks. Phys. Rev. E, 69(2):026113, 2004. [Newsham et al., 2014] Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Impact of community structure on SAT solver performance. In Proc. of SAT 14, pages 252 268, 2014. [Selman et al., 1997] Bart Selman, Henry A. Kautz, and David A. Mc Allester. Ten challenges in propositional reasoning and search. In Proc. of IJCAI 97, pages 50 54, 1997. [Slater, 2002] Andrew Slater. Modelling more realistic SAT problems. In Proc. of AJCAI 02, pages 591 602, 2002. [Sonobe et al., 2014] Tomohiro Sonobe, Shuya Kondoh, and Mary Inaba. Community branching for parallel portfolio SAT solvers. In Proc. of SAT 14, pages 188 196, 2014. [Walsh, 1999] Toby Walsh. Search in a small world. In Proc. of IJCAI 99, pages 1172 1177, 1999.