--- title: "On the Satisfiability Threshold of Random Community-Structured SAT" authors: - "Dina Barak-Pelleg" - "Daniel Berend" doi: "10.24963/ijcai.2018/174" url: "https://ijcai.org/proceedings/2018/174" pdf: "https://ijcai.org/proceedings/2018/0174.pdf" venue: "Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence" year: 2018 pages: "1249-1255" track: "Main track" keywords: - "Constraints and SAT: SAT" - "Constraints and SAT: Constraints and SAT" - "Constraints and SAT: Constraint Satisfaction" --- # On the Satisfiability Threshold of Random Community-Structured SAT Dina Barak-Pelleg, Daniel Berend *Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence*, pages 1249-1255. DOI: [10.24963/ijcai.2018/174](https://doi.org/10.24963/ijcai.2018/174) ## Abstract For both historical and practical reasons, the Boolean satisfiability problem (SAT) has become one of central importance in computer science. One type of instances arises when the clauses are chosen uniformly randomly \textendash{} random SAT. Here, a major problem, recently solved for sufficiently large clause length, is the satisfiability threshold conjecture. The value of this threshold is known exactly only for clause length $2$, and there has been a lot of research concerning its value for arbitrary fixed clause length. In this paper, we endeavor to study the satisfiability threshold for random industrial SAT. There is as yet no generally accepted model of industrial SAT, and we confine ourselves to one of the more common features of industrial SAT: the set of variables consists of a number of disjoint communities, and clauses tend to consist of variables from the same community. Our main result is that the threshold of random community-structured SAT tends to be smaller than its counterpart for random SAT. Moreover, under some conditions, this threshold even vanishes. ## Full text ## 1 Introduction The Boolean satisfiability problem (SAT) is one of the most important problems in theoretical computer science. Historically, it was the first problem proved to be NP-complete [Cook, 1971]. Since the introduction of the problem, there has been growing interest and research of all its aspects. In this problem, one is required to determine whether a certain Boolean formula is satisfiable. An instance of the problem consists of a Boolean formula in several variables v1, . . . , vn. The formula is usually given in conjunctive normal form (CNF). The basic building block of the formula is a literal, which is either a variable vj or its negation vj. A clause is a disjunction of the form l1 ∨ ... ∨ lk of several distinct literals. Thus, altogether, the formula looks like C1 ∧ C2 ∧ ... ∧ Cm, where each Ci is a clause, say Ci = li,1 ∨ ... ∨ li,ki . Given a formula, one may assign a TRUE/FALSE value to each of the variables v1, . . . , vn. The formula is satisfiable, or SAT, if there exists an assignment under which the formula is TRUE, and is unsatisfiable, or UNSAT, otherwise. ∗Research supported in part by the Milken Families Foundation Chair in Mathematics The k-satisfiability (k-SAT) problem is a special case of SAT, in which each clause is a disjunction of up to k literals. Some authors restrict k-SAT to instances with exactly k literals in each clause, which terminology we will follow here. Given n, m and k, let Ω(n, m, k) denote the set of all k-SAT instances with n variables and m clauses. A random k-SAT instance is a uniformly random element of Ω(n, m, k). Namely, each clause is selected uniformly randomly out of all (nk)2k possible clauses of length k, and distinct clauses are independent. Note that two instances, differing in the order of the clauses only, are considered as distinct. The ratio m/n is the density and denoted by α. This parameter turns out to be very important. If α is sufficiently small, then a large random instance with density α is SAT with high probability, whereas if α is sufficiently large then a large random instance is UNSAT with high probability. Despite its loose name, the notion of "with high probability" is well defined. Let (Ej)∞j=1 be a sequence of events. The event Ej occurs with high probability (w.h.p.) if P (Ej) ---→ j→∞ 1. In our case, we take larger and larger random instances with some fixed density, and inquire whether they are SAT or UNSAT. For k ≥ 2, denote [Achlioptas and Peres, 2004]: rk ≡ sup{α : A random density-α instance is SAT w.h.p.} , r∗ k ≡ inf{α : A random density-α instance is UNSAT w.h.p.} . For k = 2, it was proved long ago [Chvátal and Reed, 1992], [Fernandez de la Vega, 1992] and [Goerdt, 1992] that r2 = r∗ 2 = 1. The Satisfiability Threshold Conjecture claims that, in fact, rk = r∗ k for all k [Chvátal and Reed, 1992]. This conjectured common value is the satisfiability threshold. It has been a subject of interest among researchers, theoretically and empirically, to prove the conjecture for k ≥ 3 and find the threshold. Recently, the conjecture has been proved for large enough k [Ding et al., 2015]. As part of this research, lower and upper bounds were obtained on rk and r∗ k for k ≥ 3. In [Franco and Paull, 1983] it was proven that r∗ k ≤ 2k ln2. This has been improved in [Kirousis et al., 1998] to r∗ k ≤ 2k ln 2 - 12 (1 + ln 2) + ok(1). From the other side, a sequence of successive improvements led finally to the bound rk ≥ 2k ln2 - 1 2 (1 + ln 2) + ok(1) [Coja-Oghlan and Panagiotou, 2016]. Thus, with the satisfiability conjecture settled in [Ding et al., 2015] for large k, it follows that rk = r∗ k = 2k ln2 - 12 (1 + ln2) + ok(1) for such k. For small values of k, more specific results were obtained. For k = 3, the best bounds seem to be r3 ≥ 3.42 [Kaporis et al., 2002] and r∗ 3 ≤ 4.506 [Dubois et al., 2000]. Experiments and other results of heuristics, based on statistical physics considerations, indicate that r3 ≈ 4.26 [Mertens et al., 2006; Mézard and Zecchina, 2002], r4 ≈ 9.93, r5 ≈ 21.12, r6 ≈ 43.37, r7 ≈ 87.79 [Mertens et al., 2006]. Much more is known about 2-SAT. First, unlike k-SAT for k ≥ 3, which is an NP-complete problem, 2-SAT instances may be solved by a linear time algorithm [Chvátal and Reed, 1992; Goerdt, 1992]. Also, there is quite precise information about 2-SAT for density very close to the threshold r2 = 1 [Bollobás et al., 2001] and [Wilson, 1998]. It has been argued that instances of random k-SAT do not in fact represent real-world, or industrial, instances. One of the major differences between industrial and random SAT instances is that the set of variables in industrial instances often consists of a disjoint union of subsets, referred to as communities; clauses tend to comprise variables from the same community, with but a minority of clauses containing variables from distinct communities [Ansótegui et al., 2012; Newsham et al., 2014]. There are several additional differences. For example, the variables may be selected nonuniformly (say, according to a power-law distribution [Ansótegui et al., 2009; Giráldez-Cru and Levy, 2017]), and/or the clauses may be of non-constant length. In this paper we work with a (generalization of a) model suggested by [Giráldez-Cru and Levy, 2015] . Our model is similar to the random model, except for the partition of the variables into communities. These communities are of the same size. There are several clause types, differing in the number of variables from the same or distinct communities in each clause. For example, a clause of type (3, 2) is a clause of length 5, comprising 3 random variables from one random community and 2 from another. Our focus is on the satisfiability threshold in this model. The question has been studied in [Giráldez-Cru and Levy, 2015], mostly experimentally, for the model suggested there. We show that the findings in that paper, whereby the threshold tends to be smaller when there are many single-community clauses, remain true in the general model. In fact, if the communities are small, the threshold may even be 0. We present our model in Section 2. The main results are stated in Section 3, and the proofs follow in Section 4. ## 2 Random Industrial SAT In industrial SAT, the strength of the community structure of an instance is usually measured by its modularity [Ansótegui et al., 2012; Giráldez-Cru and Levy, 2016; Park and Newman, 2003]. Roughly speaking, given a graph, its modularity gives an indication for the tendency of the vertices to be connected to other vertices which are similar to them in some way. In our case, an instance defines the following undirected graph. The set of nodes is the set of variables {v1, . . . , vn}. There is an edge (vi, vj) for i ̸= j if there exists a clause in the instance, containing both variables vi (or its negation) and vj (or its negation). Given an instance, high modularity indicates that there exists a partition of the set of variables into subsets, such that a large portion of the edges connect vertices of the same subset, compared to a random graph with the same number of vertices and same degrees [Newman, 2006; Park and Newman, 2003] . As in the regular model, we have n Boolean variables and m clauses in an instance. Each clause is chosen independently of the others. Each variable in each clause is negated with a probability of 12 , independently of the other variables. The model differs from the regular model in several aspects: There is a community structure on the set of variables, and we also do not necessarily assume all clauses to be of the same length. Specifically, the set of variables {v1, . . . , vn} is divided into B disjoint (sets of variables referred to as) communities C1, C2, ..., CB. For simplicity, we assume all communities to be of the same size h, so that n = B · h. As n grows, so do usually both B and h (although at times one of them may remain fixed), and we will write B(n) and h(n) when we want to relate to their dependence on n. For an ℓ-tuple k = (k1, . . . , kℓ) with positive, non-decreasing, integer entries, denote by ΩB (n, k) the set of all clauses formed of k1 variables from some community Ci1 , k2 from another community Ci2 ,. . . , kℓ from some ℓth community Ciℓ , where the indices ij are mutually distinct. We will always implicitly assume that ki ≤ h for each i. Let Pk be the uniform measure on ΩB (n, k). Let T ≥ 1 be some positive integer, and let P be a convex combination P = ∑Tt=1 pt · Pkt , where pt > 0 for each t, ∑Tt=1 pt = 1, and the vectors kt = (k1t, . . . , kℓt) are mutually distinct. That is, P is a measure on ⋃Tt=1 ΩB (n, kt). Using similar notations to [Giráldez-Cru and Levy, 2015], denote by F (n,m,B, P) the probability space of instances, with the sample space (⋃Tt=1 ΩB (n, kt))m and the measure P m. Instances in the model presented in [Giráldez-Cru and Levy, 2015] include clauses of two types: (i) all variables belong to the same community, and (ii) the variables belong to distinct communities. For some 0 < p < 1, each clause is of type (i) with probability p and type (ii) with probability 1 - p. With the above notation, their probability space is for some b. The instance (v1 ∨ v2 ∨ v3) ∧ (v2 ∨ v6) is an instance in In particular, F (n,m, 1, P(k) ) is the regular model of random k-SAT. Denote by F (n,m,B, P)-SAT the satisfiability problem, in which the probability space of the instances is F (n, m, B, P ). As explained above, the clauses in an industrial instance tend to include variables from the same community. In this paper, we deal with the case where one (or more) of the programs Pkt , 1 ≤ t ≤ T, takes clauses whose variables are from a single community, namely kt = (k) for some t and k. In some results, we will further restrict ourselves to the case T = 1 of a single program. ## 3 The Main Results In [Giráldez-Cru and Levy, 2015] it was observed empirically that, when the modularity of the variable incidence graph (VIG) of the instance increases, the threshold decreases. Now, the modularity in our case is larger when more clauses consist of variables from the same community and when the communities are small. Our first result is quite straightforward, but it already hints that instances in the model suggested in Section 2 tend to be no more satisfiable than random k-SAT instances. Note that the first part of the proposition is one of the initial results for random SAT [Franco and Paull, 1983] . Proposition 3.1. Let I be a random instance in F (n, αn, B, P ). - (a) Suppose that for each Pkt , 1 ≤ t ≤ T , the clause length is at most k. If α > 2k ln 2, then I is UNSAT w.h.p. - (b) Let P = P(k) for some k ≥ 2. Our next result points out a significant difference between random instances and community-structured ones. One might expect the threshold to be different for community-structured instances, but it turns out that this difference may be not just quantitative. The following result shows that, surprisingly, under certain conditions the satisfiability threshold is 0. To this end, we will consider m as some function of n, not necessarily m = αn, and write m(n) instead of m. For real functions f and g, we write f = Ω(g) if g = O(f), and f = ω(g) if g = o(f). We also write f = polylog(g) if f = O (lnθ g) for some θ. Theorem 3.2. Let I be a random instance in F (n, m(n), B, P ), where kt = (k) for some 1 ≤ t ≤ T . (a) Let h(n) = O (1). - (i) If P = P(k) for some k and m(n) = o(n1-1/2k ), then I is SAT w.h.p. - (ii) If m(n) = Ω(n1-1/2k ), then I is UNSAT with probability bounded away from 0. - (iii) If m(n) = ω(n1-1/2k ), then I is UNSAT w.h.p. - (b) If h(n) = o ( lnn ln ln n ) and m(n) = Ω ( n polylog(n) ), then I is UNSAT w.h.p. - (c) If h(n) = o (ln n) and m(n) = Ω (n · e-β·ln n/h(n) ) for some β < 1/r∗ k , then I is UNSAT w.h.p. - (d) Let h(n) = O(lnn) and T = 1. Then there exists some ε0 > 0 such that, if m(n) = αn with α > r∗ k - ε0, then I is UNSAT w.h.p. Table 1: Asymptotic satisfiability of a random instance with small communities in F (n, m(n), B, P ). | Parameters - h(n) | Parameters - m(n) | Parameters - T | Results | |---------------------|-----------------------|------------------|--------------| | O(1) | o (n1-1/2k ) | 1 | SAT w.h.p. | | O(1) | Ω (n1-1/2k ) | ∗ | ∈ (0, 1- δ) | | O(1) | ω (n1-1/2k ) | ∗ | UNSAT w.h.p. | | o ( lnn ln ln n ) | Ω(n/polylog(n)) | ∗ | UNSAT w.h.p. | | o (lnn) | Ω(n1-1/(r∗ k+ε)h(n) ) | ∗ | UNSAT w.h.p. | | O (ln n) | (r∗ k - ε) n | 1 | UNSAT w.h.p. | Remark 3.3. (a) The ε0 in part (d) is effective. Namely, as will follow from the proof, one can present such an ε0 explicitly (in terms of the implicit constant in the equality h(n) = O(ln n)). - (b) Still in case (d), one can deal with the general case of arbitrary T as long as the weight of the program (k) in P is sufficiently large. In Theorem 3.2 there are three types of results for the asymptotic satisfiability of a random community-structured instance with n variables, m(n) clauses, B communities of size h(n) = n/B, and probability measure P. Namely, either the probability of satisfiability tends to 0 as n → ∞, or it tends to 1, or it is bounded away from 1. These results are summarized in Table 1. In general, we assume that kt = (k) for some 1 ≤ t ≤ T and k ≥ 1. In the third column we place a '1' or a '∗', depending on whether T is required to be 1 or is arbitrary, respectively. The notation ∈ (0, 1 - δ) indicates a probability bounded away from 1. The proof of Theorem 3.2 will use the following lemma. Lemma 3.4. Consider the spaces F (n,m(n),B, P) and F (n,m′ (n),B, P), where m′ (n) = ω (m(n)). If a random instance in F (n,m(n),B, P) is UNSAT with probability bounded away from 0, then a random instance I ′ in F (n, m′ (n), B, P ) is UNSAT w.h.p. In the proof of Theorem 3.2 (and that of Theorem 3.6) we use some results regarding the classical "balls and bins" problem. In this problem, there are M balls and B bins. Each ball is placed uniformly randomly into one of the bins, independently of the other balls. One quantity of interest is the maximum load, which is the maximum number of balls in any bin. There are several papers studying the size of the maximum load, as well as generalizations of this problem. It seems that [Raab and Steger, 1998] contains all previous results. Our next result seems not to be covered by previous results regarding the balls and bins problem. It will be employed in the proof of Theorem 3.2, and may be of independent interest. Proposition 3.5. Consider the balls and bins problem with B bins and M = M(B) balls. Let s ≥ 1 be an arbitrarily fixed integer. - (a) If M(B) = o(B1-1/s ), then the maximum load is at most s - 1 w.h.p. - (b) If M(B) = Ω(B1-1/s ), then the maximum load is at least s, with probability bounded away from 0. - (c) If M(B) = ω(B1-1/s ), then the maximum load is at least s w.h.p. As noted earlier, random 2-SAT is much better understood than random k-SAT for general k. This enables us to obtain a stronger result than Theorem 3.2 in the case P = P(2). Theorem 3.6. Let I be a random instance in F (n, αn, B, P(2) ). - (a) There exists an 0 < ε0 < 1 such that, if h(n) = o (√n) and α > 1 - ε0, then I is UNSAT w.h.p. - (b) For h(n) = Θ(√n): - (i) If 1 - ε0 < α < 1, where ε0 is as in (a), then I is SAT with probability bounded away from both 0 and 1. (ii) If α = 1 then I is UNSAT w.h.p. - (c) For h(n) = ω(√n) with h(n) = o(n): (i) If α < 1 then I is SAT w.h.p. (ii) If α = 1 then I is UNSAT w.h.p. - (d) For h(n) = Θ(n) : - (i) If α < 1 then I is SAT w.h.p. - (ii) If α = 1 then I is SAT with probability bounded away from both 0 and 1. Table 2: Asymptotic satisfiability of a random instance in F (n, αn, B, P(2) ). | h(n) α | ∈ (1- ε0, 1) | = 1 | |------------------|----------------|--------------| | = o (√n) | UNSAT w.h.p | UNSAT w.h.p. | | = Θ (√n) | ∈ (δ, 1- δ) | UNSAT w.h.p. | | ∈ ω (√n) ∩ o (n) | SAT w.h.p. | UNSAT w.h.p | | = Θ (n) | SAT w.h.p | ∈ (δ, 1- δ) | Remark 3.7. Similarly to Remark 3.3.b, one can deal with the more general case of arbitrary T, as long as one of the programs Pkt is of the form (k) and is of sufficiently large weight. Similarly to Table 1, we summarize the results of the theorem 3.6 in Table 2. Here, we always assume k = 2, m(n) = αn and T = 1. Similarly to Theorem 3.2, we have three types of results for the asymptotic satisfiability of a random instance in F (n, αn,B, P(2) ), two of which are the same as in Table 1. Namely, either the probability of satisfiability tends to 0 as n → ∞, or it tends to 1, or it is bounded away both from 0 and 1. In the latter case we shall use the notation ∈ (δ, 1 - δ). ## 4 Proofs ## Proof of Proposition 3.1: - (a) We follow the proof in the random model [Franco and Paull, 1983]. Fix a truth assignment and consider I. Each clause has at most k literals. The variables are negated with probability 1/2 independently of each other, and hence each clause is satisfied with probability of 1 - 2-k , independently of the other clauses. The expected number of satisfying truth assignments is therefore 2n · (1 - 2-k )αn . As α > 2k ln 2, we have Thus, I is UNSAT w.h.p. - (b) A random instance I in F (n, αn, B, P(k) ) decomposes into B sub-instances Ii, 1 ≤ i ≤ B, where each Ii is formed of those clauses consisting of variables solely from Ci. Obviously, I is SAT if and only if all Ii-s are such. For 1 ≤ i ≤ B, let Ui = 1 if Ii is satisfiable, and Ui = 0 otherwise. The variable U = ∏Bi=1 Ui indicates whether I is satisfiable. Let Wi denote the number of clauses in Ii . Clearly, - (i) Suppose first that h(n) = ω(1). Let αi denote the density of the sub-instance Ii, 1 ≤ i ≤ B. There exists an i with αi ≥ α, and therefore αi > r∗ k . It follows that Ii is UNSAT w.h.p., and hence so is I. The case h(n) = O(1) follows in particular from part (a.iii) of this theorem (to be proved below). - (ii) In this case B(n) = Θ(1). Without loss of generality assume B(n) = B is fixed. For γ > 0, let Let α′ be an arbitrary fixed number, strictly between α and rk. Then: By the weak law of large numbers, and therefore Now consider the second factor on the right-hand side of (2). Clearly, As α′ < rk and B is fixed, the right-hand side of (3) converges to 1 as n → ∞. Hence I is SAT w.h.p. As mentioned in Section 3, the proofs of Theorem 3.2 and Theorem 3.6 make use of some results concerning the balls and bins problem. Let L be the maximum load for M balls and B bins. By [Raab and Steger, 1998], for any δ > 0, w.h.p.for an appropriate constant dc > c. Remark 4.1. The constant dc, in the second part of (4), is the unique solution of the equation in (c,∞) (see [Raab and Steger, 1998, Lemma 3]). A routine calculation shows that dc = c + c · u(1/c), where the function u is the unique non-negative function defined implicitly by the equation The function u(w) has been studied in [Kolchin et al., 1978, pp. 101-102], and in particular expressed as a power series in √w near 0. The fact that dc > c is the reason that the threshold in Theorem 3.2.d is strictly less than r∗ k . One can easily bound dc-c from below. In fact, write dc = c + ε. Then Proof of Theorem3.2: We follow the notations used in the proof of Proposition 3.1. Recall that Ii is the sub-instance formed of those clauses in I consisting of variables solely from Ci, and Wi is the number of clauses in Ii, 1 ≤ i ≤ B. Denote Wmax = max {W1, . . . , WB} . We may assume that T = 1 in all parts of the theorem. In fact, in the general case, if the weight of the program P(k) in P is p, then w.h.p. there will be at least p2 · m(n) clauses consisting of clauses of type (k). To see it, denote by I (k) the sub-instance of I obtained by taking the clauses from the program of type (k) and by m′ (n) the number of clauses in I (k) . Note that m′ (n) is B(m(n), p)-distributed. Employing Chernoff's bound we deduce a lower bound p · m(n)/2 on m′ (n) w.h.p. Since p ·m(n) tends to infinity with n, I (k) is UNSAT w.h.p., which implies that so is I. Since T = 1, each clause corresponds to some community. Consider clauses as balls, and communities as bins. The process of selecting the clauses, as far as the community to which the variables in each clause belong, is analogous to that of placing m(n) balls in B bins uniformly at random. The idea of the proof in parts (b)-(d) will be to prove that w.h.p. we have Wmax/h(n) > r∗ k . This will imply that there is at least one sub-instance Ii with density larger than r∗ k . Thus, already Ii is UNSAT w.h.p., and consequently so is I. - (a) Without loss of generality, assume that h(n) = h > 0 is fixed. - (i) By Proposition 3.5.a, there is no sub-instance with more than 2k - 1 clauses w.h.p. Since instances with less than 2k clauses are certainly satisfiable w.h.p., all Ii-s are SAT, and hence so is I. - (ii) By Proposition 3.5.b, the probability that there is an Ii, 1 ≤ i ≤ B, with at least 2k clauses, is bounded away from 0. Assume, say, that W1 ≥ 2k . Then, with probability at least all 2k distinct clauses consisting of the variables v1, . . . , vk have been drawn. As the instance is UNSAT if it contains all these 2k clauses, the probability for our instance to be UNSAT is bounded away from 0. - (iii) Follows from the previous part and Lemma 3.4. - (b) In view of part (a.iii), we may assume h(n) → ∞. We may also assume that m(n) = n/ lnθ n for some θ ≥ 1. Clearly, m(n) ≤ B. On the other hand, Thus, by (4), w.h.p., the maximum load is at least Now, there are h(n) = o(lnn/ ln lnn) variables in each community. By (5), w.h.p., the density of the subinstance Ii with the maximal number of clauses is at least Hence, this Ii is UNSAT w.h.p., and therefore so is I. - (c) By (4), w.h.p., the number of clauses in the subinstance Ii with the maximal number of clauses is at least For a large enough n As β < 1/r∗ k , for large enough x we have lnx + βx < x/r∗ k . Hence, for large enough n we have This implies that the density of the sub-instance Ii with the maximal number of clauses is at least and thus UNSAT w.h.p. Consequently, so is I. - (d) In view of the previous part, we may assume that h(n) = θ lnn for some θ > 0. Choose c0 such that where dc is as in (4). Let α > c0/θ, and put c = αθ. Thus, c > c0 and dc > dc0 . Let δ < dc - θr∗ k . We have By (4), the size of the largest sub-instance is Wmax ≥ (dc - δ) lnB w.h.p. Hence, w.h.p. the density of this sub-instance is Let us make one comment regarding the proof of Theorem 3.6, which we cannot bring here. The fact that Theorem 3.6 is much more precise than Theorem 3.2 hinges on the fact that the information as to the satisfiability of 2-SAT for various densities is more detailed than for k-SAT in general. In fact, [Bollobás et al., 2001] proved that there exist some 0 < ε0 < 1 and λ0 > 0 such that the satisfiability probability of a random 2-SAT instance I with m = n · (1 + ε) clauses is (Actually, we use only the first two cases.) Note that in the case m = n · (1 - ε) with λ0n-1/3 ≤ ε ≤ ε0, we have for some constants θ1, θ2 > 0. ## 5 Conclusions We have dealt with the satisfiability threshold of a particular model of SAT. This model highlights one of the features in which so-called industrial SAT instances differ from classical SAT instances. Namely, the set of variables decompose into several disjoint subsets-communities.The significance of these communities stems from the fact that clauses tend to contain variables from the same community. We have shown, roughly speaking, that the satisfiability threshold of such instances tends to be lower than for regular instances. Moreover, if the communities are very small, the threshold may even vanish. The paper leaves a lot to study for industrial SAT instances. To begin with, there are other features considered in the literature as being characteristic of industrial instances. For example, in the scale free structure the variables are selected by some heavy-tailed distribution. Moreover, even regarding the issue of communities, there is more to be done. We assumed here that all communities are of the same size. Obviously, there is no justification for this assumption beyond the fact that it simplifies significantly the analysis of the model. What can be said about the threshold if there are both small and large communities? Even prior to that, what would be reasonable to assume regarding the probability of a variable to be selected from each of the communities? ## Acknowledgments We would like to express our gratitude to David Wilson for helpful information regarding the topic of this paper, as well as to the referees for their comments on the first version of the paper. ## References 1. [Achlioptas and Peres, 2004] Dimitris Achlioptas and Yuval Peres. "The threshold for random k-SAT is 2 k ln 2 - O(k)". Journal of the American Mathematical Society 17.4 (2004), 947-973. 2. [Ansótegui et al., 2009] Carlos Ansótegui, María L. Bonet and Jordi Levy. "Towards industrial-like random SAT in- stances". Proc. of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009 (2009). 3. [Ansótegui et al., 2012] Carlos Ansótegui, Jesús Giráldez- Cru and Jordi Levy. "The community structure of SAT formulas". Proc. of Theory and Applications of Satisfia- bility Testing-SAT 2012: 15th International Conference, Trento, Italy, June 17-20, 2012, A. Cimatti, R. Sebas- tiani, Eds., 410-423. 4. [Bollobás et al., 2001] Béla Bollobás, Christian Borgs, Jen- nifer T. Chayes, Jeong H. Bim and David B. Wilson. "The scaling window of the 2-SAT transition". Random Struc- tures & Algorithms 18 (2001), 3, 201-256. 5. [Chvátal and Reed, 1992] Vaclav Chvátal and B. Reed, "Mick gets some (the odds are on his side)", Proc. 33rd Symp. Foundations of Computer Science (1992), 620-627. 6. [Cook, 1971] Stephen A. Cook. "The complexity of theorem proving procedures". Proc. of the Third Annual ACM STOC (1971), 151-158. 7. [Coja-Oghlan and Panagiotou, 2016] Amin Coja-Oghlan and Konstantinos Panagiotou. "The asymptotic k-SAT threshold". Advances in Mathematics 288 (2016), 985-1068. 8. [Ding et al., 2015] Jian Ding, Allan Sly and Nike Sun. "Proof of the satisfiability conjecture for large k". (En- glish summary) STOC'15-Proc. of the 2015 ACM Symposium on Theory of Computing (2015), 59-68. 9. [Dubois et al., 2000] Olivier Dubois, Yacine Boufkhad, and Jacques Mandler. "Typical random 3-SAT formulae and the satisfiability threshold". Proc. 11th ACM-SIAM Symp. on Discrete Algorithm (2000), 126-127. 10. [Fernandez de la Vega, 1992] Wenceslas Fernandez de la Vega, On random 2-SAT, unpublished manuscript (1992). 11. [Franco and Paull, 1983] John V. Franco and Marvin C. Paull. "Probabilistic analysis of the Davis-Putnam proce- dure for solving the satisfiability problem". Discrete Ap- plied Mathematics 5(1) (1983), 77-87. 12. [Giráldez-Cru and Levy, 2015] Jesús Giráldez-Cru and Jordi Levy. "A modularity-based random SAT instances gener- ator". Proc. of the 24th International Joint Conference on Artificial Intelligence, IJCAI'15 (2015), 1952-1958. 13. [Giráldez-Cru and Levy, 2016] Jesús Giráldez-Cru and Jordi Levy. "Generating SAT instances with community struc- ture". Artificial Intelligence 238 (2016), 119-134. 14. [Giráldez-Cru and Levy, 2017] Jesús Giráldez-Cru, Jordi Levy. "Locality in Random SAT Instances". Proc. of the 26th International Joint Conference on Artificial Intelli- gence, IJCAI'17 (2017), 638-644. 15. [Greenberg and Mohri, 2014] Spencer Greenberg and Mehryar Mohri. "Tight lower bound on the probability of a binomial exceeding its expectation". Statistics & Probability Letters 86 (2014), 91-98. 16. [Goerdt, 1992] Andreas Goerdt. "A threshold for unsat- isfiability", Proc. Mathematical Foundations of Com- puter Science 1992: 17th International Symp. Prague, Czechoslovakia, August 24-28, 1992. 629 Springer, Berlin (1992) 264-274. 17. [Kaporis et al., 2002] Alexis C. Kaporis, Lefteris M. Kirousis, and Efthimios G. Lalas. "The probabilistic analysis of a greedy satisfiability algorithm". Proc. of the 10th Annual European Symp. on Algorithms, Lecture Notes in Computer Science 2461, Springer-Verlag, Berlin (2002), 574-585. 18. [Kirousis et al., 1998] Lefteris M. Kirousis, Evangelos Kon- stantinou Kranakis, Danny Krizanc, and Y. C. Stama- tiou. "Approximating the unsatisfiability threshold of ran- dom formulas". Random Structures & Algorithms 12(3) (1998), 253-269. 19. [Kolchin et al., 1978] Valentin F. Kolchin, Boris A. Sev- astýanov and Vladimir P. Chistyakov. "Random alloca- tions". V. H. Winston & Sons, Washington, D.C., (1978). 20. [Mertens et al., 2006] Stephan Mertens, Marc Mézard and Riccardo Zecchina. "Threshold values of random k-SAT from the cavity method". Random Structures & Algo- rithms 28 (2006), 340-373. 21. [Mézard and Zecchina, 2002] Marc Mézard and Riccardo Zecchina. "Random k-satisfiability problem: From ana- lytic solution to an efficient algorithm". Physical Review E 66 (2002), 056126. 22. [Newman, 2006] Mark E. J. Newman. "Finding community structure in networks using the eigenvectors of matrices". Physical Review E 74(3) (2006), 036104. 23. [Newsham et al., 2014] Zack Newsham, Vijay Ganesh, Se- bastian Fischmeister, Gilles Audemard, and Laurent Si- mon. "Impact of community structure on SAT solver per- formance", In Theory and applications of satisfiability testing-SAT 2014, Lecture Notes in Comput. Sci., 8561, Springer (2014), 252-268. 24. [Park and Newman, 2003] Juyong Park and Mark E. J. New- man, Physical Review E 68 (2003), 026112. 25. [Raab and Steger, 1998] Martin Raab and Angelika Steger. "Balls into bins-a simple and tight analysis". J. D. P. Rolim, M. Serna and M. Luby, Eds., Randomization and Approximation Techniques in Computer Science, 1518, Springer, Berlin (1998), 159-170. 26. [Wilson, 1998] David B. Wilson, http://dbwilson.com/2sat- data/ (1998).