Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT

1 Introduction

One of the most thoroughly researched topics in theoretical computer science is Satisfiability of Propositional Formulas (SAT). It was one of the first problems shown to be NP-complete by Cook [Cook, 1971] and, independently, by Levin [Levin, 1973]. Furthermore, SAT stands at the core of many results of modern complexity theory, like NPcompleteness proofs [Karp, 1972] or lower bounds on runtime assuming the (Strong) Exponential Time Hypothesis [Impagliazzo et al., 1998; Bringmann, 2014].

Additional to its importance for theoretical research, Propositional Satisfiability also has practical applications. Many practical problems can be transformed into SAT formulas, for example hard- and software verification, automated planning, and circuit design. Such SAT formulas arising from practical and industrial problems are commonly referred to as industrial SAT instances. Surprisingly, even large industrial SAT

∗Contact Author

instances with millions of variables can often be solved efficiently by state-of-the-art SAT solvers. This suggests that these instances have a structure which makes them easier to solve than the theoretical worst-case.

1.1 UniformRandom SAT and the Satisfiability Threshold Conjecture:

In order to study the average-case complexity of Satisfiability, one can generate a formula Φ at random in conjunctive normal form (CNF) with n variables and m clauses. To this end, we assume to have a probability distribution over all formulas with those properties. If the probability distribution is uniform, we will also refer to the model as uniform random k-SAT.

One of the most prominent questions related to uniform random k-SAT is trying to prove the satisfiability threshold conjecture. Intuitively, the satisfiability threshold is the clausevariable-ratio m/n at which the probability to generate a satisfiable formula goes from one to zero. The satisfiability threshold conjecture states that for a formula Φ drawn uniformly at random from the set of all k-CNFs with n variables and m clauses, there is a real number rk such that

For k = 2, Chvatal and Reed [Chvatal and Reed, 1992] and, independently, Goerdt [Goerdt, 1996] proved that r2 = 1. For k ⩾ 3, explicit upper and lower bounds have been derived, e. g., 3.52 ⩽ r3 ⩽ 4.4898 [Hajiaghayi and Sorkin, 2003; Kaporis et al., 2006; D´ıaz et al., 2009]. Coja-Oghlan and Panagiotou [Coja-Oghlan and Panagiotou, 2016] derived a bound (up to lower order terms) for k ⩾ 3 with rk = 2k log 2- 12 (1+ log 2) ± ok(1). Recently, Ding, Sly, and Sun [Ding et al., 2015] proved the exact position of the threshold for sufficiently large values of k.

One goal of showing the conjecture is to connect or disconnect threshold behavior to the average hardness of solving instances. For uniform random k-SAT for example, the on average hardest instances are concentrated around the threshold [Mitchell et al., 1992]. However, the conjecture and a lot of related work only consider formulas that are drawn uniformly at random. But what happens if the formulas are drawn according to a different probability distribution?

1.2 Non-UniformRandom SAT:

There is a substantial body of work, which analyzes the satisfiability threshold in different SAT models, like regular random k-SAT [Boufkhad et al., 2005a], random geometric kSAT [Bradonjic and Perkins, 2014] and 2+p-SAT [Monasson et al., 1996]. However, these models are not motivated by trying to model or understand the properties of industrial instances.

One property of industrial instances we can consider is their degree distribution. The degree distribution of a formula Φ is a function f : N → N, where f(x) denotes the number of different Boolean variables that appear x times in the formula Φ (negated or unnegated). In uniform random k-SAT this distribution is binomial, but recently it has been found out that the degree distribution of many families of industrial instances follows a power-law [Boufkhad et al., 2005b; Ans´otegui et al., 2009a]. This means that the fraction of variables that appear k times is proportional to k-β , where β is a constant intrinsic to the instance. To help close the gap between the degree distribution of uniform random and industrial instances, Ans´otegui, Bonet, and Levy [Ans´otegui et al., 2009a] proposed a power-law random SAT model. Empirical studies [Ans´otegui et al., 2009a; Ans´otegui et al., 2009b; Ans´otegui et al., 2015] found that SAT solvers that are specialized in industrial instances also perform better on power-law formulas than on uniform random formulas. However, it looks like a power-law degree distribution alone makes instances a bit easier to solve, but not actually "easy": median runtimes around the threshold still look like they scale exponentially for several state-of-the-art solvers [Friedrich et al., 2017b; Bl¨asius et al., 2019].

Instead of studying random k-SAT with power-law distributions we would like to have a way of choosing any variable distribution we want. One model that can achieve this goal is a configuration-type model for random k-SAT in which each variable has a fixed number of appearances that are distributed uniformly at random among the k · m variable positions in the formula. For k = 2 this model has already been studied by Cooper, Frieze and Sorkin [Cooper et al., 2007], Levy [Levy, 2017], and Omelchenko and Bulatov [Omelchenko and Bulatov, 2019]. However, we want to consider a slightly different model that is much easier to analyze.

In our paper we consider a generalization of the power-law random SAT model by Ans ´otegui, Bonet, and Levy [Ans ´otegui et al., 2009a]. Our model also allows instances with any given ensemble of variable distributions, instead of just power laws: The variables of each clause are drawn with a probability proportional to the n-th distribution in the ensemble, then they are negated independently with a probability of 1/2 each. Let D (n, k, (⃗ pn)n∈N,m) be such a model with a variable distribution ensemble (⃗ pn)n∈N, where m clauses of length k over n variables are drawn. We call this the clause-drawing model. If we draw clauses in such a way, the variable probability distribution also defines a probability distribution over k-clauses. Instead of drawing exactly m k-clauses over n variables, one can now imagine flipping a coin for each possible k-clause and taking the clause into the formula with the clause probability multiplied with a certain scaling factor s. By doing so, the expected number of clauses in the formula will be exactly s.

We will denote this model by F (n, k, (⃗ pn)n∈N, s) and call it the clause-flipping model.

Although F (n, k, (⃗ pn)n∈N, s) and D(n, k, (⃗ pn)n∈N, m) cannot represent industrial instances accurately, they might still give us some insights into which properties of real-world instances make them easy to solve. The one property our models provide is degree distribution. They allow us to look at the connection between degree distribution and hardness in an average-case scenario.

As one of the steps in analyzing the connection between hardness and threshold behavior in non-uniform random kSAT, we would like to find out for which ensembles of variable probability distributions an equivalent of the satisfiability threshold conjecture holds. To see which ingredients we need to prove the conjecture and which of these ingredients this work provides, we first have to introduce the concept of threshold functions more formally.

1.3 Threshold Functions:

Formally, due to [Friedgut, 2005] a threshold for a monotone property P is defined as follows in the classical context of uniform probability distributions: Let p ∈ [0, 1] and let V = {0, 1}N be endowed with the product measure µp(·): for x ∈ V define µp(x) = p∑ xi (1-p)N-∑ xi , and, for W ⊆ V , µp(W) = ∑x∈W µp(x). Now let P = P(n) be a family of monotone properties. p∗ = p∗ (n) is an asymptotic threshold function for P(n) if for every p = p(n)

Intuitively, a sharp threshold means that the change in probability around the threshold becomes steeper and steeper as the problem size increases, converging to a step function as n tends to infinity. Formally, we say that P(n) has a sharp threshold if there exists a function p∗ = p∗ (n) such that for every constant ε > 0 and for every p = p(n)

Otherwise we call a threshold coarse. The region of p where the limit of µp(P) is bounded away from zero and one is called the threshold interval.

Note, that this definition only holds for satisfiability in the uniform clause-flipping model. In the case of the uniform clause-drawing model, the sharpness of the threshold is defined the same way, but with respect to m or s instead of p on the appropriate probability space.

1.4 Proving the Satisfiability Threshold Conjecture:

In terms of threshold functions, the conjecture states that there is a sharp threshold for satisfiability at m = rk · n and the constant rk is the same for a fixed k and all sufficiently large n. For k = 2, Chvatal and Reed [Chvatal and Reed, 1992] and Goerd [Goerdt, 1996] proved the conjecture and showed that r2 = 1. However, random 2-SAT is easier to analyze than random k-SAT and their techniques do not work for bigger values of k. For uniform random k-SAT the "recipe" for proving the conjecture is as follows:

1. Show the existence of an asymptotic threshold function, i. e. show constant lower and upper bounds on rk.
2. Prove that the threshold is sharp. Friedgut [Friedgut, 1999] showed that the satisfiability threshold for uniform random k-SAT is sharp, although its location is not known exactly for all values of k. However, his result does not prove that rk is the same for a fixed k and all sufficiently large values of n. Friedgut's proof relies on knowing the asymptotic threshold function.
3. Derive the actual constant rk. Ding, Sly, and Sun [Ding et al., 2015] were the first to prove the exact value of rk for values of k bigger than 2. Their proof relies on the result of Friedgut.

We now want to see if we can prove equivalents of these results for non-uniform random k-SAT, more specifically for the clause-drawing model. For non-uniform random 2-SAT we already provided all ingredients to prove or disprove the conjecture for given probability ensembles [Friedrich and Rothenberger, 2019a; Friedrich and Rothenberger, 2019b]. For non-uniform random k-SAT with a power law probability distribution, we provided the first step, showing that the asymptotic threshold is Θ(n) if the power law exponent is β > 2k-1 k-1 [Friedrich et al., 2017a].

The goal of this paper is to show the second ingredient for proving the satisfiability threshold conjecture for non-uniform random k-SAT, sharpness of the satisfiability threshold. In addition to being a stepping stone to proving the conjecture, sharpness of the threshold is of independent interest, since a coarse threshold implies that there is a local property which approximates unsatisfiability. For random SAT this means that with constant probability instances have a constant-sized unsatisfiable subformula, making many instances easy to solve even around the threshold. Moreover, some of our techniques could also be used to analyze more sophisticated models, e.g. the popularity-similarity model [Gir´aldez-Cru and Levy, 2017], which was used in the 2017 SAT Competition.

1.5 Our Results:

We study the sharpness of the satisfiability threshold for nonuniform random k-SAT and identify sufficient conditions on the variable probability distribution which imply a sharp threshold. Therefore, this work provides the second ingredient for proving a version of the satisfiability threshold conjecture for the non-uniform models D(n, k, (⃗ pn)n∈N,m) and F (n, k, (⃗ pn)n∈N, s). In the context of these models, the classical result of Friedgut [Friedgut, 1999] reads as follows:

Theorem 1.1 (by Friedgut). For all n ∈ N let ⃗ pn = (1/n, 1/n, . . . , 1/n) be a variable probability distribution on n variables. If there is an asymptotic satisfiability threshold mc = t(n) on D (n, k, (⃗ pn)n∈N,m), then satisfiability has a sharp threshold on F (n, k, (⃗ pn)n∈N, s) with respect to s, and a sharp threshold on D (n, k, (⃗ pn)n∈N,m) with respect to m.

Our main theorem extends this to our non-uniform model.

Theorem 1.2. Let k ⩾ 2, let (⃗ pn)n∈N be an ensemble of variable probability distributions on n variables each and let sc = t(n) be an asymptotic satisfiability threshold for F (n, k, (⃗ pn)n∈N, s) with respect to s. If ‖⃗ pn‖∞ = o (t- k 2k-1 · log- k-1 2k-1 t) and ‖⃗ pn‖22 = O (t-2/k ), then satisfiability has a sharp threshold on F (n, k, (⃗ pn)n∈N, s) with respect to s.

Furthermore, we show that the same holds for the clausedrawing model of non-uniform random k-SAT.

Theorem 1.3. Let k ⩾ 2, let (⃗ pn)n∈N be an ensemble of variable probability distributions on n variables each and let mc = t(n) = ω(1) be the asymptotic satisfiability threshold for D (n, k, (⃗ pn)n∈N,m) with respect to m. If ‖⃗ pn‖∞ = o (t- k 2k-1 · log- k-1 2k-1 t) and ‖⃗ pn‖22 = O (t-2/k ), then satisfiability has a sharp threshold on D (n, k, (⃗ pn)n∈N, m) with respect to m.

Our results actually state that the threshold is sharp for a certain, fixed value of n in the following sense: Let P be the monotone property that a k-CNF is unsatisfiable and let µs be the product probability measure induced by F (n, k, (⃗ pn)n∈N, s). It then holds that there is a function s∗ = s∗ (n) such that

It is still possible that the probability function behaves differently for higher n due to the changing number of variables and probabilities. Nevertheless, Friedgut's original result also only asserts sharpness for a certain, fixed value of n. This is also the reason why the sharp threshold result does not automatically prove the satisfiability threshold conjecture: There could be different sharp threshold functions (including leading constant factors) for different values of n. For example, there could be some strange oscillations of the function.

2 Proof Sketch

In the paper we only show Theorem 1.2, i. e. we show the result in the non-uniform clause-flipping model. However, we can show that in the context of the main theorem, the sharpness of the threshold carries over to the clause-drawing model with the same ensemble of probability distributions, thus implying Theorem 1.3. We also show that under the same conditions, the asymptotic thresholds of the two models coincide. This is important in order to use Theorem 1.2 in the first place if only the asymptotic threshold in D (n, k, (⃗ pn)n∈N,m) is known.

The proof of Theorem 1.2 uses Bourgain's Sharp Threshold Theorem in the version from O'Donnell's book [O'Donnell, 2014]. In general, it follows the lines of Friedgut's proof of sharpness for the threshold of uniform random kSAT [Friedgut, 1999].

We assume toward a contradiction that the threshold is coarse. Then the Sharp Threshold Theorem tells us that there have to be so-called "boosters" of constant size that appear with constant probability in the random formula. These boosters have the property that conditioning on their existence boosts the probability of the random formula to be unsatisfiable by at least an additive constant.

One kind of booster are unsatisfiable subformulas of constant size. Conditioning on these would boost the probability to be unsatisfiable to one. We rule these out by showing that they do not appear with constant probability.

Then, we consider subformulas, which give the second highest boost: maximally quasi-unsatisfiable subformulas. These are subformulas which have only one satisfying assignment for the variables appearing in them and adding any new clause over those variables makes them unsatisfiable. We want to show that these cannot boost the probability of a formula to be unsatisfiable by a constant.

Again toward a contradiction, we assume, that conditioning on a maximally quasi-unsatisfiable subformula T is enough to boost the unsatisfiability probability by a constant. First, we prove that conditioning on T is equivalent to adding a number of clauses of size shorter than k to the random formula over variables not appearing in T . Then, we use a version of Friedgut's coverability lemma to show that, if adding these clauses of size smaller than k makes the random formula unsatisfiable with constant probability, then also adding o(t) clauses of size k makes the random formula unsatisfiable with nearly the same constant probability. We prove that this probability is dominated by the probability to make the original random formula unsatisfiable for a slightly bigger scaling factor. However, due to the assumption of a coarse threshold, the slope of the probability function for unsatisfiability has to be small at one point in the threshold interval. If we consider exactly this point, the probability to make the original random formula unsatisfiable cannot be increased by a constant with our slightly increased scaling factor. This contradicts our assumption that the probability is boosted by a constant in the first place. Thus, quasi-unsatisfiable subformulas cannot be boosters.

After showing this, every less restrictive subformula cannot be a booster either. That means, the only possible boosters are unsatisfiable subformulas, which we ruled out already. Therefore, the implication of the Sharp Threshold Theorem does not hold, which contradicts the assumption of a coarse threshold and therefore proves the statement.

In order to come to this conclusion, we have to generalize Friedgut's results, like showing that no short unsatisfiable subformula can exist with sufficiently high probability. Furthermore, his lemma to bound the maximum slope of the probability function cannot be applied anymore, even in a more general form. Instead, we use the maximum slope that is implied by assuming a coarse threshold. Also, we had to adapt Friedgut's lemma which allowed us to substitute clauses of size smaller than k with k-clauses. In his work, a quasi-unsatisfiable subformula can spawn a constant number of clauses of length k - 1. Now a quasi-unsatisfiable subformula can spawn clauses of any length l ⩽ k and it can spawn more than a constant number of clauses.

3 Example Application of the Theorem

We can use Theorem 1.3 as a tool to show sharpness of the threshold for non-uniform random k-SAT with different probability distributions on the variables. As an example, we apply the theorem for an ensemble of power-law distributions.

Corollary 3.1. Let (⃗ pn)n∈N be an ensemble of general powerlaw distributions with the same power-law exponent β ⩾ 2k-1 k-1 + 1 + ε, where ε > 0 is a constant and ⃗ pn is defined over n variables. For k ⩾ 2 both F (n, k, (⃗ pn)n∈N, s) and D (n, k, (⃗ pn)n∈N,m) have a sharp threshold with respect to s and m, respectively.

Proof. From [Friedrich et al., 2017a] we know that the asymptotic threshold for D(n, k, (⃗ pn)n∈N,m) is at m = Θ(n) for β ⩾ 2k-1 k-1 + ε. We know that this implies an asymptotic threshold at s = Θ(n) for the clause-flipping model F (n, k, (⃗ pn)n∈N, s) with the same probability ensemble (⃗ pn)n∈N. It is now an easy exercise to see that

and that ‖⃗ pn‖∞ = maxi=1,...,n(pn,i) = O (n-(β-2)/(β-1) ). One can now verify ‖⃗ pn‖22 = O (n-2/k ) and ‖⃗ pn‖∞ = o(n-k/(2k-1) · log-(k-1)/(2k-1) (n)) for β > 2k-1 k-1 + 1 + ε and k ⩾ 2. This implies a sharp threshold for F (n, k, (⃗ pn)n∈N, s) and D (n, k, (⃗ pn)n∈N, m) due to Theorem 1.2 and Theorem 1.3.

4 Discussion

In our paper we show sufficient conditions on the variable probability distribution of non-uniform random k-SAT for the satisfiability threshold to be sharp. The main theorems can readily be used to prove sharpness for a wide range of random k-SAT models with heterogeneous distributions on the variable occurrences: If the threshold function is known asymptotically, one only has to verify two conditions on the variable distribution, which can be done easily in most cases.

We suspect that it is possible to generalize the result to demanding only ‖⃗ p‖∞ = o (t-1/k ), since the additional factor is only needed in one lemma. In any case it would be interesting to complement the result with matching conditions on coarseness of the threshold.

We hope that our results make it possible to derive a proof in the style of Ding, Sly, and Sun [Ding et al., 2015] for certain variable probability ensembles, effectively proving the satisfiability threshold conjecture for these ensembles.