{'fraction_non_alphanumeric': 0.03681759307741064, 'fraction_numerical': 0.01209799652768209, 'mean_word_length': 4.488203266787659, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Evidence for Long-Tails in SLS Algorithms

Stochastic local search (SLS) is a successful paradigm for solving the satisfiability problem of propositional logic. A recent development in this area involves solving not the original instance, but a modified, yet logically equivalent one. Empirically, this technique was found to be promising as it improves the performance of state-of-the-art SLS solvers. Currently, there is only a shallow understanding of how this modification technique affects the runtimes of SLS solvers. Thus, we model this modification process and conduct an empirical analysis of the hardness of logically equivalent formulas. Our results are twofold. First, if the modification process is treated as a random process, a lognormal distribution perfectly characterizes the hardness; implying that the hardness is long-tailed. This means that the modification technique can be further improved by implementing an additional restart mechanism. Thus, as a second contribution, we theoretically prove that all algorithms exhibiting this long-tail property can be further improved by restarts. Consequently, all SAT solvers employing this modification technique can be enhanced.


Introduction
also demonstrated that although adding new clauses can improve the mean runtime, there exist instances where adding clauses can harm the performance of SLS. This behavior is worth studying to help eliminate the risk of increasing the runtime of such procedures.
For this reason, we study the runtime (or more precisely, hardness) distribution of the procedure Alfa, introduced in this work, that models the addition of a set of logically equivalent clauses L to a formula F and the subsequent solving of this amended formula F (1) := F ∪ L by an SLS solver. Our empirical evaluations show that this distribution is long-tailed. We want to stress the fact that studies on the runtime distribution of algorithms are quite sparse even though knowledge of the runtime distribution of an algorithm is extremely valuable: (1) Intuitively speaking, if the distribution is long-tailed, one knows there is a risk of ending in the tail and experiencing very long runs; simultaneously, the knowledge that the time the algorithm used thus far is in the tail of the distribution can be exploited to restart the procedure (and create a new logically equivalent instance F (2) ). We will prove this statement in a rigorous manner for all long-tailed algorithms. (2) Given the distribution of an algorithm's sequential runtime, it was shown how to predict and quantify the algorithm's expected speedup due to parallelization [1]. (3) If the distribution of hardness is known, experiments with few instances can lead to parameter estimations of the underlying distribution [13]. (4) Knowledge of the distribution can help compare competing algorithms: one can test if the difference in the means of algorithm runtimes is significant if the distributions are known [13].

Our Contributions
Our contributions consist of an empirical as well as theoretical part, specified below.
Statistical Runtime/Hardness Distribution Analysis. By conducting a plethora of experiments (total CPU time 80 years) and using several statistical tools for the analysis of empirical distributions, we conjecture that Alfa equipped with SLS solvers based on Schöning's Random Walk Algorithm [36], SRWA for short, follows a long-tailed distribution (Conjecture 8). The evidence obtained further suggests that this distribution is, in fact, lognormal (Conjecture 6). We measure the goodness-of-fit of our results over the whole domain using the χ 2 -statistic.
Restarts Are Useful For Long-Tailed Algorithms. Lorenz [22] has analyzed the lognormal and the generalized Pareto distribution for the usefulness of restarts and their optimal restart times. Given that our Strong Conjecture 6 holds, this result implies that restarts are useful for Alfa. We will also show that this is the case if only the Weak Conjecture 8 holds: We theoretically prove that restarts are useful for the class of algorithms exhibiting a long-tailed distribution.

Related Work and Differentiation
In [13], the authors presented empirical evidence for the fact that the distribution of the effort (more precisely, the number of consistency checks) required for backtracking algorithms to solve constraint satisfaction problems randomly generated at the 50 % satisfiable point can be approximated by the Weibull distribution (in the satisfiable case) and the lognormal distribution (in the unsatisfiable case). These results were later extended to a wider region around the 50 % satisfiable point [32]. It should be emphasized that this study created all instances using the same generation model. This resulted in the creation of similar yet logically non-equivalent formulas. We, however, will firstly use different models to rule out any influence of the generation model and secondly generate logically equivalent modifications of a base instance (see Algorithm 1). This approach lends itself to the analysis of existing SLS solvers [23]. The major advantage is that the conducted work is not lost in the case of a restart: only the logically equivalent instance could be changed while keeping the current assignment.
In [16], the cost profiles of combinatorial search procedures were studied. The authors showed that they are often characterized by the Pareto-Lévy distribution and empirically demonstrated how rapid randomized restarts can eliminate this tail behavior. We will theoretically prove the effectiveness of restarts for the larger class of long-tailed distributions.
The paper [1] studied the solvers Sparrow and CCASAT and found that for randomly generated instances the lognormal distribution is a good fit for the runtime distributions. For this, the Kolmogorov-Smirnov statistic sup t∈R |F n (t) − F (t)| was used. Although the KS-test is very versatile, this comes with the disadvantage that its statistical power is rather low. Clearly, the KS statistic is also nearly useless in the tails of a distribution: A high relative deviation of the empirical from the theoretical cumulative distribution function in either tail results in a very small absolute deviation. It should also be remarked that the paper studies only few formulas in just two domains, 10 randomly generated and 9 crafted. Our work will address both shortcomings in this paper: The χ 2 -test gives equal importance to the goodness-of-fit over the entire support; and various instance domain models (both theoretical and applied) are considered in this paper.
▶ Remark. Unfortunately, the term heavy-or long-tailed distribution is not used consistently in the literature. We will follow [12] and use the notion given in Definition 7.

Preliminaries
We assume familiarity with terminologies such as Boolean variable, literal, clause, CNF formula, the SAT problem, and assignment flips in SLS solvers and refer the reader to e. g. [37]. We furthermore trust that the reader has basic knowledge of the proof system Resolution [8,33]. Stochastic local search (SLS) solvers operate on complete assignments for a formula F . These solvers are started with a randomly generated complete initial assignment α 0 . If α 0 satisfies F , a solution is found. Otherwise, the SLS solver tries to find a solution by performing a random walk over the set of complete assignments for the underlying formula. A formula F logically implies a clause C if every complete truth assignment which satisfies F also satisfies C, for which we write F ⊨ C. If L is a set of clauses we write F ⊨ L if F ⊨ C for all C ∈ L.
▶ Definition 1. Let X be a random variable for the runtime of an SLS algorithm A on some input. For t > 0, the algorithm A t is obtained by restarting A after time t if no solution was found. Restarts are useful if there is a t > 0 such that where X t models the runtime of A t .
▶ Definition 4. Let X 1 , . . . , X n be independent, identically distributed real-valued random variables with realizations x i of X i . Then the empirical cumulative distribution function ( ecdf) of the sample (x 1 , . . . , x n ) is defined aŝ where 1 A is the indicator of event A.

Design of the Adjusted Logical Formula Algorithm Alfa
Our SLS solver Alfa (Adjusted logical formula algorithm) receives a satisfiable formula F as input. The algorithm then proceeds by adding to F a set L of logically generated clauses. It finally calls an SLS solver to solve the clause set F ∪ L.
Algorithm 1 Alfa acts as a base algorithm that can use different SLS algorithms.
Input: Boolean formula F , Promise: F ∈ SAT Generate randomly a set L of clauses such that F ⊨ L Call SLS(F ∪ L) for some SLS solver SLS Definition 5 is used in Algorithm 2 as a natural way to sample a set L of logically equivalent clauses with respect to a base instance F . Finally, we set Res n w (F ).

Experimental Setup, Instance Types, and Solvers Used
Hoos and Stützle [18] introduced the concept of runtime distribition to characterize the cdf of Las Vegas algorithms, where the runtime can vary from one execution to another, even with the same input. To obtain enough data for a fitting of such a distribution, for each base instance F we created 5000 modified instances F (1) , . . . , F (5000) by generating resolvent sets L (1) , . . . , L (5000) each by using Algorithm 2 with w = 4 and a value of p such that the expected number of resolvents being added was 1 10 |F |. Note that we also conducted a series of experiments to rule out the influence of p on our results. Each of these modified instances was solved 100 times, each time using a different seed. For i = 1, . . . , 5000 and j = 1, . . . , 100 we thus obtained the values flips S (F (i) , s j ) indicating how many flips were used to solve the modified instance F (i) with solver S when using the seed s j . Next, we calculated the mean number of flips mean S (F (i) ) := 1 100 100 j=1 flips S (F (i) , s j ) required to solve F (i) with solver S whose hardness distribution we are going to analyze.
All experiments were performed on bwUniCluster 2.0 and three local servers. Sputnik [39] was used to distribute the computation and to parallelize the trials. Due to the heterogeneity of the computer setup, measured runtimes are not directly comparable to each other. Consequently, we instead measured the number of variable flips performed by the SLS solver. This is a hardware-independent performance measure with the benefit that it can also be analyzed theoretically. To give an indication of how flips relate to wall-clock time, one million flips take about one second of computing time on one of our servers. To give an idea of the computational effort involved, obtaining the data for the ecdf of a 100 variable base instance with SRWA took an average of 17,193,517 seconds (≈ 199 days) when unparallelized. This clearly prohibited examining instances having a number of variables currently being routinely solved by the state-of-the-art SLS algorithms. For the experiments the following instance types were used:

Hidden Solution:
We implemented the CDC algorithm [5,6] in [24] to generate instances with a hidden solution. For this, at the beginning, a complete assignment α is specified to ensure the generated formula's satisfiability. Then, repeatedly a randomly generated clause C is added to the formula with a weighted probability p i depending on the number i of correct literals in C with respect to α. We included this type of instances because SLS solvers struggle to solve such instances. Experiments like these might be beneficial to find theoretical reasons for this behavior.

Hidden Solution With Different Chances:
We also created sets of formulas with different underlying p i values to rule out the influence of these.

Uniform Random:
To generate uniform, random k-SAT instances with n variables and m clauses, each clause is generated by sampling k literals uniformly and independently. Using Gableske's kcnfgen [14], we generated formulas with n ∈ {50, 60, 70, 80, 90} variables and a clause-to-variable ratio r close to the satisfiability threshold [29] of r ≈ 4.267. We checked each instance with Glucose3 [2, 11] for satisfiability until we had 5 formulas of each size.

5.
Coloring: These formulas assert that a graph is colorable with 3 colors. We generated these formulas, using [21], over random graphs with n vertices and m = 2.254n edges in expectation, which is slightly below the non-colorability threshold [20]. We obtained 32 satisfiable instances in 150 variables.
Our experiments investigated leading SLS solvers where the dominating component is based on the random walk procedure proposed in [36]. In this paper, Schöning's Random Walk Algorithm SRWA was introduced, which is one of the solvers we used. The probSAT solver family [3] is based on this approach. One of these solvers won the random track of the SAT competition 2013 [4]. Another advancement of SWRA was implemented as YALSAT [7], which won the random track of the SAT competition 2017 [17]. These performances and similarities were reasons for choosing SRWA, probSAT, and YALSAT as SLS solvers for this paper. The connection to GapSAT [23] is another case in point.
For SRWA we conducted most of our experiments: All instance types were tested, including different change values for the generation of the hidden solution. For probSAT, 55 hidden solution instances with n ∈ {50, 100, 150, 200, 300, 800} were used. Since YALSAT can be regarded as a probSAT derivate, we tested YALSAT with 10 hidden solution instances with 300 variables each.

Experimental Results and Statistical Evaluation
The goal of this section is to explore the scenarios described above in more detail. We are particularly interested in how the hardness of an instance changes when logically equivalent clauses are added in the manner described above. To characterize this effect as accurately as possible, studying the ecdf is the most suitable method for this purpose. In turn, the ecdf can be described using well-known distribution types such as e. g., the normal distribution. In the following, we shall demonstrate that the three-parameter lognormal distribution, in particular, provides an exceptionally accurate description of the runtime behavior, and this is true for all considered problem domains and all solvers. The results are so compelling that we ultimately conjecture that the runtimes of Alfa-type algorithms all follow a lognormal distribution, regardless of the considered problem domain.
To illustrate this point, we first demonstrate our approach using two base instances. The first one is a factorization instance that was solved by SRWA. The second instance has a hidden solution and was solved by probSAT. For later reference, we refer to the first instance as A and to the second instance as B. As described above, we obtain 5000 samples for each base instance. Using these data points, we estimate the lognormal distribution's three parameters by applying the maximum likelihood method (see [41]). After that, one can visually evaluate the suitability of the fitted lognormal distribution for describing the data. A useful method of visualizing the suitability is to plot the ecdf and the fitted cdf on the same graph.
Such a comparison is illustrated in Figure 1 for the two instances A and B. In both cases, no difference between the empirical data of the ecdf and the fitted distribution can be detected visually. In other words, the absolute error between the predicted probabilities from the fitted cdf versus the empirical probabilities from the ecdf is minuscule. Even though these are only two examples, it should be noted that these two instances are representative of the behavior of the investigated algorithms. Hardly any deviation could be observed in this plot type for all instances and all algorithms. All data is published under [41].
For the analysis, however, one should not confine oneself to this plot type. Although absolute errors can be observed easily, relative errors are more difficult to detect. Such a relative error may have a significant impact when used for decisions such as restarts. To illustrate this point, suppose that the true probability of a run of length ℓ is 0.0001. In contrast, the probability estimated based on a fit is 0.001. As can be seen, the absolute error of 0.0009 is small, whereas the relative error of 10 is large. If one were to perform restarts after ℓ steps, the actual expected runtime would be ten times greater than the estimated expected runtime. Thus, the erroneous estimate of that probability would have translated into an unfavorable runtime. This example should illustrate the importance of checking the tails of a distribution for errors as well.
The left tail, i. e., the probabilities for very small values, can be checked visually by plotting the ecdf and fitted cdf with both axes logarithmically scaled. Thereby, the probabilities for extreme events (in this case, especially easy instances) can be measured accurately. The two instances A and B are being examined in this manner in Figure 2. As can be observed, the lognormal fit accurately predicts the probabilities associated with very short runs. For the other instances, lognormal distributions were mostly also able to accurately describe the probabilities for short runs. However, the behavior of the ecdf and the fitted lognormal distribution differed very slightly in a few instances.
Lastly, the probabilities for particularly hard instances should also be checked. Any mistakes in this area could lead to underestimating the likelihood of encountering an exceptionally hard instance. For analyses of this type, the survival function S is a useful tool; if F is the cdf, S(x) := 1 − F (x). Therefore, the survival function's value S(x) represents the probability that an instance is (on average) harder than x in our case. If we plot the empirical survival function, i. e.,Ŝ n (x) := 1 −F n (x), and the fitted survival function together on a graph with logarithmically scaled axes, we can easily detect errors in the right tail.   Here, there is a discernible deviation between A and B. While for A, the lognormal fit provides an accurate description of the probabilities for long runs, in the case of B, the empirical survival function seems to approach 0 somewhat slower than the lognormal estimate. In the vast majority of cases, these extreme value probabilities are accurately reflected by the lognormal fit. In most other cases, the empirical survival function approaches 0 more slowly than the lognormal fit. Thus, in these cases, the likelihood of encountering an exceptionally hard instance is underestimated.
So far, we discussed the behavior of lognormal fits based on this visual inspection. Altogether, we concluded that lognormal distributions seem to be well suited for describing the data. Next, we shall concretize this through a statistical test. To be more precise, we apply the χ 2 -test as a goodness-of-fit test for each base instance. For each such instance, the fitted lognormal distribution used the 5000 data points, and afterwards, the χ 2 -test statistic is computed. Subsequently, the probability that such a value of the test statistic occurs under the assumption of the so-called null hypothesis is determined. We will refer to this probability as the p-value. In our case, the null hypothesis is the assumption that the data follow a lognormal distribution. If the fit is poor, then a small p-value will occur. If p is sufficiently small, the null hypothesis is rejected. We reject the null hypothesis if p < 0.05.
Two more remarks are due on this matter. First, from a high p-value, one cannot prove that the assumption that the data are lognormally distributed is correct. However, we use a sufficiently high p-value as a heuristic whether this assumption is reasonable.
Secondly, there is an obstacle that complicates statistical analysis by this method. As described, each of the 5000 data points is obtained by first sampling 100 runtimes of the corresponding instance and then calculating the mean. This means that we do not work with the actual expected values but only estimates. In other words, this implies that our data is noisy. The greater the variance in the respective instance, the greater the corresponding noise. If one were to apply the χ 2 -test to this noisy data, some cases would be incorrectly rejected, especially if the variance is large. To overcome this limitation, we additionally use a bootstrap-test, which is based on Cheng [9]. This test is presented in Algorithm 3.
Briefly summarized, this test simulates how our data points were generated, assuming the null hypothesis. For this purpose, particular attention should be paid to how the test Algorithm 3 Bootstrap-test for noisy data Input: (noisy) random sample y = (y 1 , y 2 , . . . , y n ), integer N , significance α ∈ (0, 1) θ ← MLE(y, F ), lognormal maximum likelihood estimation, F is the lognormal cdf X 2 ← ChiSquare(y,θ), Chi-squared goodness of fit test statistic for j = 1 to N do y ′ ← (y ′ 1 , . . . , y ′ n ), where all y ′ i are i. i. d. samples from the fitted lognormal distribution with parametersθ y ′ ← y ′ + noise, where noise is sampled from an n-dimensional normal distribution sample is rendered noisy. Owing to the central limit theorem, it is reasonable to assume that the initial data's sample mean originates from a normal distribution around the true expected value. We use this assumption in the bootstrap-test using a noise signal drawn from a normal distribution with expected value 0. The variance of this normal distribution is determined from the initial data and divided by 100 (cf. central limit theorem).
If there is a large difference between the respective p-values of the χ 2 -and bootstrap-tests, this suggests that the variance in the initial data is too high and that the number of samples used to calculate the sample mean should be increased. However, this case has only occurred twice, and we explicitly indicate it later. In all other cases, the p-values of the χ 2 -and the bootstrap-tests were similar. To illustrate this point, let us consider the p-values of the two instances A and B. The excellent representation of the runtime behavior over the entire support on instance A is also reflected in the two p-values. Using the χ 2 -test, one obtains a p-value of approximately 0.783, and using the bootstrap-test, one obtains a p-value of 0.76. Since these two p-values are both above 0.05, we conclude that the assumption that lognormal distributions describe the runtimes is reasonable.
In contrast, for instance B, we observed that while a lognormal distribution accurately describes the main part of the distribution, the probabilities for extremely long runs are inadequately represented. This observation is again reflected in the respective p-values. The χ 2 -test yields a p-value of ≈ 0.008, and the bootstrap-test yields a p-value of 0.013. Since both p-values are below 0.05, the assumption that these data originate from a lognormal distribution is rejected.
Overall, this example is intended to demonstrate that these two statistical tests can show an inadequate fit, even if the problems only arise for extreme values. Second, it should demonstrate that the p-values of the two tests are generally similar; if the p-values differ significantly, then more samples should be used to calculate the sample mean.
We now proceed by considering the adequacy of lognormal distributions for describing SRWA runtimes. The results of the statistical analysis are reported in Table 1 and can be found in [41].
The first line in the table represents for how many instances the statistical tests rejected the lognormal distribution hypothesis. The second line indicates how many instances have been checked in total. It should be noted that the same number of instances was rejected by the χ 2 -test as was by the bootstrap-test. Thus, there is no need to distinguish between the tests here. It should also be mentioned that in statistical tests, there is always a possibility that a hypothesis will be rejected even though the null hypothesis holds (type 1 error). At  hidden different chances uniform factoring coloring  total  rejected  0  2  1  2  0  5  # of instances  20  120  25  33  32 230 Table 1 Statistical goodness-of-fit results for Alfa+SRWA runtimes over various problem domains. The rejected row contains the number of instances where the lognormal distribution is not a good fit according to the χ 2 -test at a significance level of 0.05. To put these results into perspective, the second row contains the total number of instances of each domain. Out o a total of 230 instances, 5 got rejected. a significance level of 0.05, this probability is at the most 5%. Accordingly, the total of 5 rejected instances may be attributed to so-called type 1 errors. This statement is also supported by the fact that no exceptionally low p-value was observed, i. e., no p-value that is unusual for a total of 230 samples.
For probSAT, on the other hand, the situation appears to be different. The results are summarized in Table 2 and [41]. The columns refer to the number of variables in the  Table 2 Goodness-of-fit results for Alfa+probSAT over various hidden solution instance sizes. The rejected row contains the number of instances where the lognormal distribution is not a good fit according to the χ 2 -test at a significance level of 0.05. To put these results into perspective, the second row contains the total number of instances of each instance size.
corresponding SAT instances. The number of rejected instances is again identical regardless of whether the χ 2 -or bootstrap-test is applied. As can be seen, the lognormal distribution hypothesis was rejected for 7 of the 55 instances. This number can no longer be accounted for by type 1 errors at a significance level of 0.05. However, one can observe that the majority of rejected instances occur for a small number of variables. If one were to consider only the instances from 150 variables onwards, then the remaining rejected instances may be attributed to type 1 errors. This raises the suspicion that there may be a limiting process, i. e., that the lognormal distribution hypothesis is only valid for n → ∞.
Lastly, a difference between the two static tests emerges for YALSAT. According to the χ 2 -test, 2 of the total 10 instances are rejected. However, using the bootstrap-test, the lognormal distribution hypothesis is not rejected for any instance. Therefore, one cannot rule out the possibility that lognormal distributions are the natural model to describe the instances, but more experiments are required to make a more precise statement.
In summary, the presumption that lognormal distributions are the appropriate choice for describing runtimes has been reinforced for SRWA. For probSAT, this appears plausible at least above a certain instance size. Likewise, the choice of lognormal distributions also seems reasonable for YALSAT. These observations lead us to the following conjecture. If this statement is true, then it would be intriguing in that one can infer how modifying the base instance affects the hardness of instances. This effect is likely to be the result of generating models for lognormal distributions. Just as the normal distribution is a natural model for the sum of i. i. d. random variables, the lognormal distribution is a natural model for the multiplication of i. i. d. random variables. Thus, one can hypothesize that each added clause exerts a small multiplicative effect on the instance's hardness.
Simultaneously, the three parameters of the lognormal distribution also provide insight into how the hardness of the instance changes. For example, the location parameter γ implies an inherent problem hardness that cannot be decreased regardless of the added clauses' choice. At the same time, γ also serves as a numerical description for the value of this intrinsic hardness. Using Bayesian statistics, it is possible to infer the parameters while the solver is running. These estimated parameters can, for example, be used to schedule restarts. This would lead to a scenario similar to that discussed in [34].
Conjecture 6 is a strong statement. However, a small deviation of the probabilities, for example, at the left tail, would render the strong conjecture invalid from a strict mathematical point of view. Particularly, visual analyses revealed that the left tail's behavior, i. e., for extremely short runs, is occasionally not accurately reflected by lognormal distributions. Conversely, the right tail, i. e., the probabilities for particularly long runs, are usually either correctly represented by lognormal distributions or, occasionally, the corresponding probability approaches 0 even more slowly. We, therefore, rephrase our conjecture in a weakened form. Our observations fit a class of distributions known as long-tail distributions defined purely in terms of their behavior at the right tail. It should be noted that lognormal distributions have the long-tail property [12,30]. That is, if the Strong Conjecture holds, the Weak Conjecture is implied. The reverse is, however, not true. In the next section, we show an important consequence in case the Weak Conjecture holds.

Restarts Are Useful For Long-Tailed Distributions
If the Strong Conjecture holds, i. e., if the runtimes are lognormally distributed, then restarts are useful [22]. This section extends this result and mathematically proves that restarts are useful even if only the Weak Conjecture holds. This will be achieved by showing that restarts are useful for long-tailed distributions. A condition for the usefulness of restarts, as defined in Definition 1, was proven in [22]. We will show the result using this theorem that is restated below.
▶ Theorem 9 ([22]). Let X be a positive, real-valued random variable having quantile function Q, then restarts are useful if and only if there is a quantile p ∈ (0, 1) such that Even if the quantile function and the expected value are unknown, R(p, X) can be characterized for large values of p. ▶ Lemma 10. Consider a positive, real-valued random variable X with pdf f and quantile function Q such that E[X] < ∞. Also, assume that the limit lim t→∞ t 2 · f (t) exists. Then, Proof. In the following, let F and f be the cdf and pdf of X, respectively. We start by specifying the derivative of Q with respect to p as a preliminary consideration. From F = Q −1 and the application of the inverse function theorem [35] it follows: As the first step in our proof, we consider the limiting value of the second summand of R(p, X). This value can be determined by integration by substitution with x = Q(u) followed by applying the change of variable method with p = F (t): The last equality holds because the numerator matches the definition of the expected value. Next, we examine the limit of (1 − p)Q(p)/ E[X]. Since lim p→1 (1 − p) = 0, the limit of (1 − p) · Q(p)/ E[X] needs to be examined more closely. For this purpose, L'Hospital's rule is applied twice as well as the change of variable method with p = F (t) is used in the following: It is well-known that if lim inf t→∞ t 2 · f (t) > 0 were to hold, then the expected value E[X] would be infinite (this statement is, for example, implicitly given in [12]). This would contradict the premise of the lemma; therefore, lim inf t→∞ t 2 · f (t) = 0. Moreover, since, by assumption, lim t→∞ t 2 · f (t) exists, we may conclude that A frequently used tool for the description of distributions is the hazard rate function.
▶ Definition 11 ([31]). Let X be a positive, real-valued random variable having cdf F and pdf f . The hazard rate function r : R + → R + of X is given by In particular, there is an interesting relationship between the long-tail property and the hazard rate function's behavior.
▶ Lemma 12 ([30]). Let X be a positive, real-valued random variable with hazard rate function r such that the limit lim Proof. The appendix contains a proof of this lemma since the manuscript [30] was still unpublished at the time of writing. ◀ With the help of these preliminary considerations, we are now ready to show that restarts are useful for long-tailed distributions.
▶ Theorem 13. Consider a positive, long-tailed random variable X with continuous pdf f and hazard rate function r. Also assume that either E[X] = ∞ holds or the limits lim t→∞ r(t) and lim t→∞ t 2 · f (t) both exist. In both cases, restarts are useful for X.
Proof. Let F be the cdf and Q the quantile function of X. We begin with the case E[X] = ∞. According to Theorem 9, restarts are useful if and only if for some p ∈ (0, 1). However, if the expected value E[X] is infinite, then the left side of this inequality is zero and the inequality is obviously satisfied. Hence, the statement follows. Secondly, we assume that E[X] < ∞ and that both lim t→∞ r(t) and lim t→∞ t 2 · f (t) exist. Equation (1) can now be used to calculate the following derivative: Consider the limit of this expression for p → 1. Once again, the change of variable method is applied with p = F (t), resulting in: By assumption, X has a long-tail distribution and the limit of lim t→∞ r(t) exists. For this reason, lim t→∞ r(t) = 0 follows as a result of Lemma 12. Furthermore, since E[X] < ∞ holds, we may conclude that The condition from Theorem 9 can be rephrased in such a way that restarts are useful if and only if R(p, X) − p < 0. According to Lemma 10, the left-hand side of this inequality approaches 0 for p → 1. However, as has been shown in Equation (2), the derivative of R(p, X) − p approaches infinity for p → 1. These two observations imply that there is a p ∈ (0, 1) satisfying R(p, X) − p < 0. Consequently, restarts are useful for X. ◀ It should be noted that the conditions of this theorem are not restrictive since all naturally occurring long-tail distributions satisfy these conditions (see also [30]).
If Conjecture 8 is true, then this statement follows immediately by Theorem 13.

Conclusion
We have provided compelling evidence that the runtime of Alfa follows a long-tailed or lognormal distribution. According to [38], the usefulness of restarts is a necessary, however not a sufficient, condition to obtain super-linear speedups by parallelization. Since we have shown that the necessary condition is (presumably) satisfied, this immediately raises the question of whether super-linear speedups are obtained by parallelizing Alfa-type algorithms. We additionally want to pose the question whether some of the Conjectures 6 or 8 can be theoretically proven. A first line of attack would be to analyze the special case of an solver like SRWA whose runtime was already theoretically analyzed.
The technique of analyzing the runtime distribution of Alfa could be further developed to help better understand the behavior of CDCL solvers. These kind of solvers heavily employ the technique of adding new clauses and deleting some clauses. This can be thought of as solving a new logically equivalent formula of the base instance.
Preliminary results on the solvers excluded for heuristic reasons seem to suggest that the Alfa-method forces the runtime of the base solver to exhibit a multimodal behavior. Thus, the lognormal distribution is not a good fit in this case. However, an initial visual inspection of the data indicates an even heavier tail.
In the next step, we show that the second statement implies the third statement, using logical contraposition to prove this. We, therefore, assume that lim inf t→∞ r(t) > 0 holds, or in other words, the following holds: By exploiting this property, we are able to estimate the integral x+y x r(t) dt: ∀x > x 0 : Thus it is shown that if the third statement does not hold, the second statement does not hold either.
In the last step, we shall demonstrate that the third statement implies the second statement. Since r(t) ≥ 0 holds for all t ∈ R + , one may express lim t→∞ r(t) = 0 as follows: Once again, we may exploit this property to estimate the integral x+y x r(t) dt: ∀x > x 0 : x+y x r(t) dt < x+y x C dt = y · C.
Since this estimate holds for all C > 0, this immediately yields lim