##### Fixing the Generating Model

The generating model for the set $\boldsymbol{\boldsymbol{L}}$ is specified in
Algorithm 5. Note that there are pronounced similarities to the model employed
in Section 3.1. However, there are two notable differences. First, the model
from Algorithm 5 does not necessarily use clauses generated by resolution.
Instead, other methods (for example, CDCL, like in the GapSAT solver) can also
be used to produce logically equivalent clauses. In this sense, the model from
Algorithm 5 generalizes the model discussed in Section 3.1. On the other hand,
in Algorithm 5, we restrict ourselves to clauses with a certain fixed length
$\ell$. In that sense, the chosen model is weaker than the one in Section 3.1.
The reason for this restriction is that otherwise, another random variable,
namely the length of the added clause, would have to be considered, which
would only further complicate the analysis.

Input: Boolean formula $F$, probability $p\in(0,1]$, set $\mathbb{L}$
containing logically equivalent clauses with respect to $F$ such that
$\exists\ell\in\mathbb{N}$: $\forall K\in\mathbb{L}$: $|K|=\ell$

$\boldsymbol{L}\coloneqq\emptyset$

foreach  _$K\in\mathbb{L}$_ do

with probability $p$ do $\boldsymbol{L}\coloneqq\boldsymbol{L}\cup\\{K\\}$

Algorithm 5 Generation of the random set $\boldsymbol{L}$.

##### Some Preliminary Comments for the Analysis of the Random Variables
$\boldsymbol{P}$, $\boldsymbol{Q}$, and $\boldsymbol{R}$

As indicated above, the Johnson SB distribution is applied several times in
the following. For our purposes, the exact values of the distribution’s
parameters are irrelevant for the most part. Therefore, we often omit the
brackets containing the exact values of the parameters. In addition, we often
deal with asymptotic distributions in this section. A sequence of random
variables $\boldsymbol{X_{1}},\boldsymbol{X_{2}},\dots$ with associated cdfs
$F_{1},F_{2},\dots$ has an asymptotic distribution $F$ if
$\lim_{n\rightarrow\infty}F_{n}(x)=F(x)$ for all $x$. A prominent example is
that a (suitably scaled) random variable
$X\sim{\operatorname{Bin}\\!\big{(}n,\,p\big{)}}$ is asymptotically normally
distributed for $n\rightarrow\infty$.

Finally, in the following, it is necessary to argue frequently about the
number of unsatisfied clauses given a specific assignment. For this purpose,
we introduce a suitable notation.

######  Definition 53.

Let $G$ be a CNF formula, $\beta$ an assignment of $G$ and
$x\in\mathrm{Vars}({G})$. We set

$\displaystyle\mathrm{UNSAT}_{G}(\beta)$ $\displaystyle~{}~{}\coloneqq~{}~{}$
$\displaystyle\big{\\{}D\in G\bigm{|}D\beta=0\big{\\}},$
$\displaystyle\mathrm{UNSAT}_{G}(\beta,\in\\!x)$
$\displaystyle~{}~{}\coloneqq~{}~{}$ $\displaystyle\big{\\{}D\in
G\bigm{|}D\beta=0\text{ and }x\in\mathrm{Vars}({D})\big{\\}},$
$\displaystyle\mathrm{UNSAT}_{G}(\beta,\notin\\!x)$
$\displaystyle~{}~{}\coloneqq~{}~{}$ $\displaystyle\big{\\{}D\in
G\bigm{|}D\beta=0\text{ and }x\notin\mathrm{Vars}({D})\big{\\}}.$

Using the symbol $\boldsymbol{\\#}$ before any of these sets denotes the
cardinality of the set.

####  4.4.1 Distribution Analysis of the Random Variable $\boldsymbol{P}$

We begin our distribution analysis with the random variable $\boldsymbol{P}$.
The goal of this subsection is to prove that $\boldsymbol{P}$ is
asymptotically Johnson SB distributed (Proposition 58).

The rough idea of the proof is to rewrite $\boldsymbol{P}$ (up to a constant)
as the fraction $\frac{1}{1+\boldsymbol{X}}$, see Equation (56), where
$\boldsymbol{X}$ is asymptotically lognormal distributed. Thus, in order to
analyze the random variable $\boldsymbol{P}$, it is helpful to establish a
relationship between the lognormal and the Johnson SB distribution.

For that, one technical detail should be clarified beforehand. In the previous
sections, we mainly considered the three-parameter lognormal distribution, i.
e., the lognormal distribution, which is shifted by an additional location
parameter. However, for most of this section, we use the two-parameter
lognormal distribution, which can be interpreted as a three-parameter
lognormal distribution with location parameter zero.

######  Lemma 54 ([Emp18]).

Let $\boldsymbol{X}\sim{\operatorname{LogN}\left(\mu,\sigma^{2}\right)}$, then
for all $c\in\mathbb{R}^{+}$ we have

$\frac{1}{c+\boldsymbol{X}}\sim{\operatorname{SB}\left(\gamma=\frac{\mu-\ln
c}{\sigma},\,\delta=\frac{1}{\sigma},\,\lambda=\frac{1}{c},\,\xi=0\right)}.$

###### Proof.

For a proof, refer to Appendix B.2. ∎

Furthermore, a connection between binomial and lognormal distributions can
also be shown. We need this connection to show that $\boldsymbol{X}$ is
asymptotically lognormal distributed. For this purpose, the following lemma is
necessary.

######  Lemma 55 ([Lac11]).

If $\boldsymbol{Y}\sim{\operatorname{Bin}\\!\big{(}n,\,p\big{)}}$, then
$\log\boldsymbol{Y}$ is asymptotically normally distributed.

###### Proof.

The proof is given in Appendix B.3. ∎

Together with Definition 15 this lemma immediately yields the following
corollary.

######  Corollary 56.

Let $\boldsymbol{Y}$, $\boldsymbol{Z}$ be two independent binomial
distributions. Then, $\boldsymbol{Y}$, $\boldsymbol{Z}$, as well as
$\boldsymbol{Y}/\boldsymbol{Z}$, are asymptotically lognormal distributed.

###### Proof.

By applying Definition 15 of lognormal distributions, we see that a random
variable is lognormal distributed if and only if its logarithm is normally
distributed. According to Lemma 55, both $\log\boldsymbol{Y}$ and
$\log\boldsymbol{Z}$ are asymptotically normally distributed. Therefore, it
follows that $\boldsymbol{Y}$ and $\boldsymbol{Z}$ are both asymptotically
lognormal distributed.

It holds that

$\log(\boldsymbol{Y}/\boldsymbol{Z})=\log\boldsymbol{Y}-\log\boldsymbol{Z}.$

By Lemma 55, we already know that $\log\boldsymbol{Y}$ and
$\log\boldsymbol{Z}$ are each asymptotically normal distributed. An extremely
valuable property is that the difference of independent normal distributions
is again normally distributed. Therefore, we note that
$\log\boldsymbol{Y}-\log\boldsymbol{Z}$ is asymptotically normal distributed
and, as a result, $\boldsymbol{Y}/\boldsymbol{Z}$ is asymptotically lognormal
distributed. ∎

######  Remark 57.

Note that this corollary does not contradict the famous theorem by de Moivre
and Laplace, which states that $\boldsymbol{Y}$ is approximately normally
distributed. Roughly speaking, this is because both approximations converge
towards the same limiting distribution. For further elaboration, refer to
[Che17].

We are now ready to analyze the asymptotic distribution of the random variable
$\boldsymbol{P}$.

######  Proposition 58.

The random variable

$\boldsymbol{P}\coloneqq\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)\mid\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}$

is asymptotically Johnson $\operatorname{SB}$ distributed.

###### Proof.

As a first step, it is worthwhile to clarify what exactly is being examined.
Therefore, we will initially focus on the conditions in
$\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)\mid\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}$.
The conditions $A(\alpha)$ and
$\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}$ tell us that SRWA
was initialized in $\alpha$ and is in $\beta$ after exactly $c$ flips. Due to
the additional condition $\operatorname{FirstSel}(c+1)$, we know that a clause
from $\boldsymbol{L}$ is chosen for the $(c+1)$-st flip. In other words, a
clause from the newly added clauses is picked.

Subject to these conditions, we are interested in how likely the algorithm
will flip $x$ next. This first requires selecting a clause containing $x$ and
then, in the next step, selecting $x$ as the variable to be flipped (cf.
Algorithm 4). Since these two events are independent, the overall probability
can be expressed as the product of the two individual probabilities.

The probability of selecting a clause containing $x$ is the ratio of the
unsatisfied clauses from $\boldsymbol{\boldsymbol{L}}$ containing $x$ to all
clauses from $\boldsymbol{L}$, as one already knows that a clause from
$\boldsymbol{\boldsymbol{L}}$ is chosen. If a clause $K$ containing $x$ has
been selected, then $x$ will be flipped with probability $1/|K|$. In Algorithm
5, we have restricted ourselves to clauses of equal length $\ell$, so $1/|K|$
is constant and is therefore not a random variable. With these preliminary
considerations,
$\boldsymbol{P}=\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)\mid\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{FirstSel}(c+1)\big{)}$
can now be given more precisely:

$\displaystyle\begin{split}\boldsymbol{P}&=\frac{1}{|K|}\cdot\frac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\in\\!x)}{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta)}\\\
&=\frac{1}{\ell}\cdot\frac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\in\\!x)}{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\in\\!x)+\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\notin\\!x)}\\\
&=\frac{1}{\ell}\cdot\dfrac{1}{1+\dfrac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\notin\\!x)}{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\in\\!x)}}.\end{split}$
(56)

We can now utilize knowledge about the model used to generate
$\boldsymbol{\boldsymbol{L}}$ (cf. Algorithm 5). Since each clause from
$\mathbb{L}$ is independently from each other included in
$\boldsymbol{\boldsymbol{L}}$ with probability $p$, both
$\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\in\\!x)$
and
$\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\notin\\!x)$
are binomially distributed. Moreover, since no clause can both contain and not
contain $x$, the two random variables are independent of each other. As a
consequence,

$\boldsymbol{X}\coloneqq\frac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\notin\\!x)}{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\beta,\in\\!x)}$

is asymptotically lognormal distributed according to Corollary 56. Then, Lemma
54 yields the result. ∎

####  4.4.2 Distribution Analysis of the Random Variable $\boldsymbol{Q}$

The analysis of the random variable $\boldsymbol{Q}$ can be achieved using
similar reasoning as before. Again, we show that $\boldsymbol{Q}$ is
asymptotically Johnson SB distributed.

######  Proposition 59.

The random variable

$\boldsymbol{Q}\coloneqq\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(k)=0\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(k)=0\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)$

is asymptotically Johnson SB distributed.

###### Proof.

Let us again focus on the conditions in the above probability expression. We
know that on its random walk from assignment $\alpha$ to $\gamma$, SRWA has
never selected a clause of the set $\boldsymbol{\boldsymbol{L}}$ in the $k-1$
flips this random walk took. By design, SRWA is independent of its past. Thus,
the information that it started from $\alpha$ and that no clause from
$\boldsymbol{\boldsymbol{L}}$ was selected in the last $k-1$ flips does not
affect the probability of choosing a clause from $\boldsymbol{\boldsymbol{L}}$
for the current flip. In contrast, the information that the algorithm is in
assignment $\gamma$ is of relevance. Therefore, the probability that no clause
from $\boldsymbol{\boldsymbol{L}}$ is chosen is given by the ratio of the
original unsatisfied clauses under $\gamma$ to all unsatisfied clauses in the
extended instance $F\cup\boldsymbol{\boldsymbol{L}}$. Based on this reasoning,
$\boldsymbol{Q}$ can be expressed as follows:

$\displaystyle\boldsymbol{Q}$
$\displaystyle=\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\mathrm{Sel}(k)=0\mid\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,A(\alpha)\big{)}$
$\displaystyle=\frac{\\#\mathrm{UNSAT}_{F}(\gamma)}{\\#\mathrm{UNSAT}_{F}(\gamma)+\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}$
$\displaystyle=\frac{1}{1+\frac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}{\\#\mathrm{UNSAT}_{F}(\gamma)}}.$

Due to the model for generating $\boldsymbol{\boldsymbol{L}}$, we conclude
that $\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)$ is
binomially distributed. Moreover,
$\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)$ is
asymptotically lognormal distributed because of Corollary 56. Since lognormal
distributions are closed under multiplication of constants,
$\frac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}{\\#\mathrm{UNSAT}_{F}(\gamma)}$
is also asymptotically lognormal distributed. According to Lemma 54 it follows
that $\boldsymbol{Q}$ is asymptotically Johnson SB distributed. ∎

####  4.4.3 Distribution Analysis of the Random Variable $\boldsymbol{R}$

For the analysis of the random variable $\boldsymbol{R}$, we use another
helpful property of lognormal distributions: They are closed under
reciprocity.

######  Lemma 60 ([CE88]).

If $\boldsymbol{X}\sim{\operatorname{LogN}\left(\mu,\sigma^{2}\right)}$, then
$\frac{1}{\boldsymbol{X}}\sim{\operatorname{LogN}\left(-\mu,\sigma^{2}\right)}$.

With this knowledge, one can now turn to the analysis of $\boldsymbol{R}$
itself.

######  Proposition 61.

The random variable
$\boldsymbol{R}\coloneqq\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(c+1)=1\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(c+1)=1\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,A(\alpha)}}{.}\;\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,A(\alpha)\right)$
is asymptotically Johnson SB distributed.

###### Proof.

The reasoning is similar to that in Section 4.4.2. The probability that a
clause from $\boldsymbol{\boldsymbol{L}}$ is selected is given by the ratio of
unsatisfied clauses from $\boldsymbol{\boldsymbol{L}}$ to the total number of
unsatisfied clauses:

$\boldsymbol{R}=\frac{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}{\\#\mathrm{UNSAT}_{F}(\gamma)+\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}=\dfrac{1}{1+\dfrac{\\#\mathrm{UNSAT}_{F}(\gamma)}{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}}.$

In our model for adding the new clauses,
$\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)$ has a
binomial distribution. Thus
$\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)$ is
asymptotically lognormal distributed (cf. Corollary 56). By applying Lemma 60,
we see that
$\frac{\\#\mathrm{UNSAT}_{F}(\gamma)}{\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)}$
is also asymptotically lognormal distributed. Lemma 54 then implies that
$\boldsymbol{R}$ is asymptotically Johnson SB distributed. ∎

####  4.4.4 Concluding Remarks Regarding the Analysis of the Random Variables

In the results of this section, we frequently mentioned that the random
variables are asymptotically Johnson SB distributed. Nevertheless, it is
crucial to clarify _under which conditions_ the random variables converge to a
Johnson SB distribution.

As a starting point, we commonly deal with binomial distributions of the form
$\boldsymbol{\\#}\boldsymbol{\mathrm{UNSAT}}_{\boldsymbol{L}}(\gamma)\sim{\operatorname{Bin}\\!\big{(}n_{\gamma},\,p\big{)}}$,
where $n_{\gamma}$ is the number of clauses in $\mathbb{L}$ that are
unsatisfied under $\gamma$. Our results take effect precisely when
$n_{\gamma}$ approaches infinity.

As is common practice, these results can also be applied under weaker
conditions. For example, if one has “only” a large number of unsatisfied
clauses in $\mathbb{L}$, then the random variables are not exactly Johnson SB
distributed, but Johnson SB distributions then represent an excellent
approximation.

###  4.5 Putting Everything Together

In the last two sections, we observed the distribution of the expected runtime
of Alfa. Then, in Section 4.3, we deduced an expression for this distribution
consisting of the random variables $\boldsymbol{P}$, $\boldsymbol{Q}$, and
$\boldsymbol{R}$. Finally, in Section 4.4, we considered these random
variables in detail. We found that each asymptotically follows a Johnson SB
distribution, respectively. In other words, the distribution consists of
asymptotically Johnson SB distributed random variables.

######  Main Result.

The expected runtime $\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}$
consists of approximately Johnson SB distributed random variables.

While this is not enough to prove Strong Conjecture (Conjecture 19), the
distribution of $\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}$ can be
treated as Johnson SB for all intents and purposes. Note that this result is
slightly weaker than the Strong Conjecture. Therefore, it does not make our
conjectures obsolete.

##  5 Conclusion

It has been shown in [LW20] that adding new, logically equivalent clauses to a
formula improves the performance of SLS SAT solvers on average. Building upon
this observation, we have shown the following main results in this paper:

  1. 1.

Treating this process as a random process, the hardness distribution follows a
Johnson SB distribution. These distributions can converge to long-tailed
distributions.

  2. 2.

We have proven that restarts are useful to avoid long-tails. Thus, the
algorithms can be further improved by implementing a restart strategy.

There are several possible starting points for future research. In this work,
we studied the runtime distributions of SAT solvers on modified instances. A
major influencing factor for our work was that different problem formulations
are often employed in mixed integer programming. Therefore, it would be
interesting to see if Johnson SB distributions are also the appropriate
descriptive model in that context or if a different family of distributions
has to be used. This would also provide more insight into how exactly modified
instances affect an algorithm.

As can be inferred from the theoretical analysis of the runtime behavior,
Johnson SB distributions significantly impact the overall runtime. This
suggests that for future studies of algorithms, one should also consider using
the Johnson SB distribution as a suitable model, alongside established
distribution types such as the normal, lognormal, and Weibull distributions.
This is especially true if one knows that there is an upper bound for the
runtimes since the Johnson SB, in contrast to the other distributions
mentioned, is able to model finite support. Such a scenario is given, for
example, in the case of a systematic search. As soon as the search tree has
been completely traversed, the algorithm terminates. Thus, the runtime of the
algorithm can be bounded from above by the size of the search tree.

Furthermore, it could be a worthwhile pursuit to theoretically investigate the
distribution of other SLS solving paradigms, such as configuration checking
solvers, e. g., CCAnr [CLS15], or WalkSAT [SKC94]. For the case of CDCL
solvers we have reported results in [KLW22].

## Code and Data Availability

The source code realizing the methodologies described in this paper and the
corresponding results are freely available. Therefore, all experiments are
fully reproducible. The corresponding code of Section 3 (visual and
statistical evaluations) is available under

https://github.com/FlorianWoerz/Towards-an-Understanding-of-Long-Tailed-
Runtimes.

All evaluations take place in the files that can be found under

./evaluation/jupyter_SB/evaluate_*.ipynb.

A permanent version of this repository has been preserved under

doi:10.5281/zenodo.6945926.

The CNF data (all base instances, resolvents, and modifications) can be found
under

doi:10.5281/zenodo.4715893.

The source code of concealSATgen that was used in Section 3.2.1 to generate
hidden solution instances is published under [LW21].

## Acknowledgments

The authors acknowledge support by the state of Baden-Württemberg through
bwHPC. This research was funded by the Deutsche Forschungsgemeinschaft (DFG,
German Research Foundation).

The authors would like to express their gratitude to Uwe Schöning for several
helpful discussions regarding the theoretical analysis.

Furthermore, the authors are greatly indebted to the anonymous referees of the
European Symposium on Algorithms (ESA ’21) and the ACM Journal of Experimental
Algorithmics (ACM JEA) for several comments that immensely helped to improve
the presentation of this paper.

## Previous Versions of the Paper

This is the full-length version of the paper in the ACM Journal of
Experimental Algorithmics (JEA). It is an extended and enhanced version of the
paper “Evidence for Long-Tails in SLS Algorithms,” [WL21] presented at ESA
2021. Section 3 describes the results from [WL21], adapted to the Johnson SB
distribution which converges to lognormal distributions. Section 4 and the
appendix is entirely new material providing mathematical justification for the
fact that Johnson SB distributions underlie the modification model.

## References

  * [AB63] John Aitchison and J. A. C. Brown.  The Lognormal Distribution – with special reference to its uses in economics.  University of Cambridge Department of Applied Economics Monograph: 5. Cambridge University Press, 2nd edition, 1963.
  * [AS09] Gilles Audemard and Laurent Simon.  Predicting learnt clauses quality in modern SAT solvers.  In Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI ’09), pages 399–404, 2009.
  * [ATC13] Alejandro Arbelaez, Charlotte Truchet, and Philippe Codognet.  Using sequential runtime distributions for the parallel speedup prediction of SAT local search.  Theory and Practice of Logic Programming, 13(4-5):625–639, 2013.
  * [Bal15] Adrian Balint.  Original implementation of _probSAT_ , 2015.  Available at https://github.com/adrianopolus/probSAT.
  * [BBJM21] Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors.  Proceedings of MaxSAT Evaluation 2021: Solver and Benchmark Descriptions, volume B-2021-2 of Department of Computer Science Report Series B. University of Helsinki, 2021.
  * [BC18] Tomáš Balyo and Lukás Chrpa.  Using algorithm configuration tools to generate hard SAT benchmarks.  In Proceedings of the 11th International Symposium on Combinatorial Search (SOCS ’18), pages 133–137. AAAI Press, 2018\.
  * [BCC+03] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu.  Bounded model checking.  Advances in Computers, 58:117–148, 2003.
  * [BFFH20] Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger.  CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020.  In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51–53. University of Helsinki, 2020.
  * [BFH21] Armin Biere, Mathias Fleury, and Maximillian Heisinger.  CaDiCaL, Kissat, Paracooba entering the SAT Competition 2021.  In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions, volume B-2021-1 of Department of Computer Science Report Series B, pages 10–13. University of Helsinki, 2021.
  * [BHL+02] Wolfgang Barthel, Alexander K. Hartmann, Michele Leone, Federico Ricci-Tersenghi, Martin Weigt, and Riccardo Zecchina.  Hiding solutions in random satisfiability problems: A statistical mechanics approach.  Physical review letters, 88(188701):1–4, 2002.
  * [BHvMW09] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors.  Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
  * [Bie14] Armin Biere.  Yet another local search solver and Lingeling and friends entering the SAT Competition 2014.  In Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, volume B-2014-2 of Department of Computer Science Report Series B, pages 39–40. University of Helsinki, 2014.
  * [Bie17] Armin Biere.  Cadical, lingeling, plingeling, treengeling, yalsat entering the sat competition 2017.  In Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, volume B-2017-1 of Department of Computer Science Report Series B, pages 14–15. University of Helsinki, 2017.
  * [BM16] Adrian Balint and Norbert Manthey.  dimetheus.  In Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, volume B-2016-1 of Department of Computer Science Report Series B, pages 37–38. University of Helsinki, 2016.
  * [BS00] Robert G. Bartle and Donald R. Sherbert.  Introduction to real analysis.  Wiley New York, 3rd edition, 2000.
  * [BS12] Adrian Balint and Uwe Schöning.  Choosing probability distributions for stochastic local search and the role of make versus break.  In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT ’12), volume 7317 of Lecture Notes in Computer Science, pages 16–29. Springer, 2012.
  * [CBRZ01] Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu.  Bounded model checking using satisfiability solving.  Formal Methods in System Design, 19(1):7–34, 2001.
  * [CE88] Edwin L. Crow and Kunio Shimizu (Editors).  Lognormal Distributions: Theory and Applications, volume 88 of Statistics: A Series of Textbooks and Monographs.  Marcel Dekker, 1988.
  * [Che17] Russell Cheng.  Non-standard parametric statistical inference.  Oxford University Press, 2017.
  * [CLS15] Shaowei Cai, Chuan Luo, and Kaile Su.  CCAnr: A configuration checking based local search solver for non-random satisfiability.  In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT ’15), volume 9340 of Lecture Notes in Computer Science, pages 1–8. Springer, 2015.
  * [Coo71] Stephen A. Cook.  The complexity of theorem-proving procedures.  In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC ’71), pages 151–158, 1971.
  * [CZ18] Shaowei Cai and Xindi Zhang.  Reasonls.  In Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, volume B-2018-1 of Department of Computer Science Report Series B, pages 52–53. University of Helsinki, 2018.
  * [CZ19] Shaowei Cai and Xindi Zhang.  Four relaxed CDCL solvers.  In Marijn J. H. Heule, Matti Järvisalo, and Martin Suda, editors, Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Report Series B, pages 35–36. University of Helsinki, 2019.
  * [CZ21] Shaowei Cai and Xindi Zhang.  Deep cooperation of CDCL and local search for SAT.  In Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT ’21), volume 12831 of Lecture Notes in Computer Science, pages 64–81. Springer, 2021.
  * [CZFB22] Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere.  Better decision heuristics in CDCL through local search and target phases.  Journal of Artificial Intelligence Research, 74:1515–1563, 2022.
  * [Die21] Maximilian Diemer.  Source code of _GenFactorSat_ , 2021.  Newest version available at https://github.com/madiemer/gen-factor-sat/.
  * [Emp18] Sextus Empiricus.  Reciprocal of shifted lognormal random variable.  Cross Validated (Stats Stack Exchange), 2018.  URL: https://stats.stackexchange.com/q/379626.
  * [EPV08] Tobias Eibach, Enrico Pilz, and Gunnar Völkel.  Attacking bivium using SAT solvers.  In Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing (SAT ’08), volume 4966 of Lecture Notes in Computer Science, pages 63–76. Springer, 2008.
  * [ES04] Niklas Eén and Niklas Sörensson.  An extensible SAT-solver.  In 6th International Conference on Theory and Applications of Satisfiability Testing (SAT ’03), Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer, 2004.
  * [FKZ11] Sergey Foss, Dmitry Korshunov, and Stan Zachary.  An Introduction to Heavy‑Tailed and Subexponential Distributions, volume 6.  Springer, 2011.
  * [FRV97] Daniel Frost, Irina Rish, and Lluís Vila.  Summarizing CSP hardness with continuous probability distributions.  In Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI/IAAI ’97), pages 327–333, 1997.
  * [Gab15] Oliver Gableske.  Source code of _kcnfgen (version 1.0)_ , 2015.  Retrieved from https://www.gableske.net/downloads/kcnfgen_v1.0.tar.gz.
  * [GS97] Carla P. Gomes and Bart Selman.  Algorithm portfolio design: Theory vs. practice.  In Proceedings of the 13th Conference on Uncertainty in Artificial Intelligence (UAI ’97), pages 190–197, 1997.
  * [GSCK00] Carla P. Gomes, Bart Selman, Nuno Crato, and Henry A. Kautz.  Heavy-tailed phenomena in satisfiability and constraint satisfaction problems.  Journal of Automated Reasoning, 24:67–100, 2000.  Related version in  _CP_ ’97.
  * [HS98] Holger H. Hoos and Thomas Stützle.  Evaluating Las Vegas algorithms: Pitfalls and remedies.  In Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI ’98), pages 238–245, 1998.
  * [JKB94] Norman L. Johnson, Samuel Kotz, and Narayanaswamy Balakrishnan.  Continuous Univariate Distributions, Volume 1.  Wiley Series in Probability and Statistics. John Wiley & Sons, 2nd edition, 1994.
  * [Joh49a] Norman Lloyd Johnson.  Bivariate Distributions Based on Simple Translation Systems.  Biometrika, 36(3-4):297–304, 1949.
  * [Joh49b] Norman Lloyd Johnson.  Systems of Frequency Curves Generated by Methods of Translation.  Biometrika, 36(1-2):149–176, 1949.
  * [KKS00] Alexis C. Kaporis, Lefteris M. Kirousis, and Yannis C. Stamatiou.  A note on the non-colorability threshold of a random graph.  The Electronic Journal of Combinatorics, 7(1), 2000.
  * [KLW22] Tom Krüger, Jan-Hendrik Lorenz, and Florian Wörz.  Too much information: Why CDCL solvers need to forget learned clauses.  PLOS ONE, 17(8):1–28, 2022.  doi:10.1371/journal.pone.0272967.
  * [Lac11] John M. Lachin.  Biostatistical Methods: The Assessment of Relative Risks.  John Wiley & Sons, 2nd edition, 2011.
  * [LENV17] Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals.  CNFgen: A generator of crafted benchmarks.  In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT ’17), pages 464–473, 2017.
  * [LM06] Inês Lynce and João Marques-Silva.  SAT in bioinformatics: Making the case with haplotype inference.  In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT ’06), volume 4121 of Lecture Notes in Computer Science, pages 136–141. Springer, 2006\.
  * [Lor18] Jan-Hendrik Lorenz.  Runtime distributions and criteria for restarts.  In Proceedings of the 44th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM ’18), pages 493–507. Springer, 2018.
  * [LRV16] Eduardo Lalla-Ruiz and Stefan Voss.  Improving solver performance through redundancy.  Journal of Systems Science and Systems Engineering, 25(3):303–325, 2016.
  * [LW20] Jan-Hendrik Lorenz and Florian Wörz.  On the effect of learned clauses on stochastic local search.  In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT ’20), volume 12178 of Lecture Notes in Computer Science, pages 89–106. Springer, 2020\.  Implementation and statistical tests of GapSAT available at Zenodo doi:10.5281/zenodo.3776052.
  * [LW21] Jan-Hendrik Lorenz and Florian Wörz.  Source code of _concealSATgen_ , February 2021.  Newest version available at https://github.com/FlorianWoerz/concealSATgen/.
  * [Man21] Norbert Manthey.  The MergeSat solver.  In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT ’21), volume 12831 of Lecture Notes in Computer Science, pages 387–398. Springer, 2021\.
  * [MMZ+01] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik.  Chaff: Engineering an efficient SAT solver.  In Proceedings of the 38th Design Automation Conference (DAC ’01), pages 530–535, 2001.
  * [MMZ06] Stephan Mertens, Marc Mézard, and Riccardo Zecchina.  Threshold values of random $k$-SAT from the cavity method.  Random Structures & Algorithms, 28(3):340–373, 2006\.
  * [MS96] João P. Marques-Silva and Karem A. Sakallah.  GRASP—a new search algorithm for satisfiability.  In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD ’96), pages 220–227, 1996.
  * [MU17] Michael Mitzenmacher and Eli Upfal.  Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis.  Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis. Cambridge University Press, 2nd edition, 2017\.
  * [NWZ20] Jayakrishnan Nair, Adam Wierman, and Bert Zwart.  The fundamentals of heavy tails: Properties, emergence, and estimation.  Preprint, California Institute of Technology, 2020.
  * [RBH03] Marvin Rausand, Anne Barros, and Arnljot Hoyland.  System reliability theory: models, statistical methods, and applications.  John Wiley & Sons, 2nd edition, 2003.
  * [RF97] Irina Rish and Daniel Frost.  Statistical analysis of backtracking on inconsistent CSPs.  In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP ’97), pages 150–162, 1997.
  * [RHK02] Yongshao Ruan, Eric Horvitz, and Henry A. Kautz.  Restart policies with dependence among runs: A dynamic programming approach.  In Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP ’02), volume 2470 of Lecture Notes in Computer Science, pages 573–586. Springer, 2002\.
  * [Rud64] Walter Rudin.  Principles of mathematical analysis, volume 3.  McGraw-Hill New York, 1964.
  * [Sch02] Uwe Schöning.  A probabilistic algorithm for k-sat based on limited local search and restart.  Algorithmica, 32(4):615–623, 2002.  Preliminary version in _FOCS ’99_.
  * [SKC94] Bart Selman, Henry A. Kautz, and Bram Cohen.  Noise strategies for improving local search.  In Proceedings of the 12th National Conference on Artificial Intelligence (AAAI ’94), pages 337–343. AAAI Press / The MIT Press, 1994.
  * [SNC09] Mate Soos, Karsten Nohl, and Claude Castelluccia.  Extending SAT solvers to cryptographic problems.  In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT ’09), volume 5584 of Lecture Notes in Computer Science, pages 244–257. Springer, 2009\.
  * [VLS+15] Gunnar Völkel, Ludwig Lausser, Florian Schmid, Johann M. Kraus, and Hans A. Kestler.  Sputnik: _ad hoc_ distributed computation.  Bioinformatics, 31(8):1298–1301, 2015.
  * [Wic17] Sven Dag Wicksell.  On logarithmic correlation with an application to the distribution of ages at first marriage.  Meddelanden från Lunds Astronomiska Observatorium, 84:1–21, 1917.
  * [WL21] Florian Wörz and Jan-Hendrik Lorenz.  Evidence for long-tails in SLS algorithms.  In Petra Mutzel, Rasmus Pagh, and Grzegorz Herman, editors, Proceedings of the 29th Annual European Symposium on Algorithms (ESA ’21), volume 204 of LIPIcs, pages 82:1–82:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.ESA.2021.82.
  * [WL22] Florian Wörz and Jan-Hendrik Lorenz.  Data set for “Towards an Understanding of Long Tailed Runtimes”, 2022\.  We have provided all data of this paper. All base instances, resolvents, and modifications can be found under doi:10.5281/zenodo.4715893. Visual and statistical evaluations can be found under https://github.com/FlorianWoerz/Towards-an-Understanding-of-Long-Tailed-Runtimes, where all evaluations take place in the files ./evaluation/jupyter_SB/evaluate_*.ipynb. A permanent version of this repository has been preserved under doi:10.5281/zenodo.6945926.

##  Appendix A The Finite Case

Recall that in Equations (8) and (12) on page 8 we have seen that

$\displaystyle\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\alpha)\big{)}}=\mathcal{F}+\mathcal{I}=\sum_{c\in\mathbb{N}_{0}}$
$\displaystyle\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}}$
$\displaystyle+\>$
$\displaystyle\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\mathrm{NeverSel}\mid
A(\alpha)\big{)}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\mathrm{NeverSel},\,A(\alpha)\big{)}}.$

In Section 4.3.1, we have analyzed the term
$\mathcal{I}=\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\mathrm{NeverSel}\mid
A(\alpha)\big{)}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\mathrm{NeverSel},\,A(\alpha)\big{)}}$,
i. e., the case in which no clause of $\boldsymbol{\boldsymbol{L}}$ ever gets
selected. We have seen that we can write

$\displaystyle\mathcal{I}\cong\sum_{i\in\mathbb{N}_{0}}\prod_{k=1}^{i}\sum_{\gamma:\,F\gamma=0}\boldsymbol{Q},$

where $\boldsymbol{Q}$ is asymptotically Johnson SB distributed (cf.
Proposition 59). Our aim in this appendix is to obtain a similar
representation for

$\mathcal{F}\coloneqq\sum_{c\in\mathbb{N}_{0}}\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}}.$

We then proceed to analyze the distribution of the ensuing random variables in
Section 4.3.3 of the main body.

To abbreviate the notation, we use the next definition in the following.

######  Definition 62.

We let
$\boldsymbol{V}\coloneqq\operatorname{Vars}\\!\big{(}\mathrm{UNSAT}_{\boldsymbol{L}}(\beta)\big{)}$,
where $\mathrm{UNSAT}_{\boldsymbol{L}}(\beta)$ is the set of clauses in
$\boldsymbol{L}$ that are falsified by $\beta$.

Let us now state the first intermediate result of this section.

######  Proposition 63.

It holds that

$\displaystyle\mathcal{F}$
$\displaystyle=\sum_{c\in\mathbb{N}_{0}}\sum_{\beta:\,\boldsymbol{L}\beta=0}\bigg{\\{}\operatorname{\mathbb{P}}\bigl{[}\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\operatorname{FirstSel}(c+1),\,A(\alpha)}}{.}\,\operatorname{FirstSel}(c+1),\,A(\alpha)\bigr{]}\cdot\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}$ (60)
$\displaystyle\phantom{MMMMMM}\cdot\sum_{x\in\boldsymbol{V}}\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)\mid\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}$
(64)
$\displaystyle\phantom{MMMMMMMM}\cdot\Big{(}c+1+\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\beta^{\prime})\big{)}}\Big{)}\bigg{\\}}.$
(65)

###### Proof.

We will apply the LTE twice to analyze the finite case (i. e., terms in
$\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\alpha)\big{)}}$
with an eventual selection of a clause from $\boldsymbol{L}$). In the first
application of the LTE we condition over the event
$\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}$ and obtain

$\displaystyle\mathcal{F}\stackrel{{\scriptstyle\phantom{\text{LTE}}}}{{=}}$
$\displaystyle\sum_{c\in\mathbb{N}_{0}}\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}}$
$\displaystyle\stackrel{{\scriptstyle\text{LTE}}}{{=}}$
$\displaystyle\sum_{c\in\mathbb{N}_{0}}\sum_{\beta:\,\boldsymbol{L}\beta=0}\Big{\\{}\operatorname{\mathbb{P}}\bigl{[}\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\operatorname{FirstSel}(c+1),\,A(\alpha)}}{.}\,\operatorname{FirstSel}(c+1),\,A(\alpha)\bigr{]}\cdot\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}$
$\displaystyle\phantom{MMMMM}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,A(\alpha)\big{)}}\Big{\\}}.$

Due to Example 45 (iii), we only need to consider such $\beta\in\\{0,1\\}^{n}$
in the sum emerging from the application of the LTE that falsify a clause in
$\boldsymbol{L}$.

For the second application of the LTE we condition over the event
$\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)$. Then, we can write

$\displaystyle\mathcal{F}\stackrel{{\scriptstyle\text{LTE}}}{{=}}$
$\displaystyle\sum_{c\in\mathbb{N}_{0}}\sum_{\beta:\,\boldsymbol{L}\beta=0}\Big{\\{}\operatorname{\mathbb{P}}\bigl{[}\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\operatorname{FirstSel}(c+1),\,A(\alpha)}}{.}\,\operatorname{FirstSel}(c+1),\,A(\alpha)\bigr{]}\cdot\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}$ (69)
$\displaystyle\phantom{MMMMM}\cdot\sum_{x\in\boldsymbol{V}}\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)\mid\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)}$
(73)
$\displaystyle\phantom{MMMMM}\phantom{MM}\cdot\,\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right),\,A(\alpha)\big{)}}\Big{\\}}.$
(74)

One can notice the following two facts: First, the expression

$\operatorname{\mathbb{P}}\bigl{[}\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\operatorname{FirstSel}(c+1),\,A(\alpha)}}{.}\,\operatorname{FirstSel}(c+1),\,A(\alpha)\bigr{]}$

is no random variable depending on $\boldsymbol{\boldsymbol{L}}$ since the
event $\operatorname{FirstSel}(c+1)$ ensures that in none of the first $c$
for-loop iterations, a clause from $\boldsymbol{L}$ gets selected, but only in
the $(c+1)$-st iteration. Thus, the probability that the algorithm ends up in
$\beta$ after the $c$-th flip does not depend on $\boldsymbol{L}$ since the
algorithm behaves as on the original instance $F$.

Secondly, observe that the term appearing in line (74) can be expressed
recursively as

$\displaystyle\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right),\,A(\alpha)\big{)}}=c+1+\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\beta^{\prime})\big{)}},$
(75)

where $\beta^{\prime}\coloneqq\beta[x]$, since $c$ flips were performed to get
from the initial assignment $\alpha$ to assignment $\beta$, and one $x$-flip
was performed to get from $\beta$ to $\beta^{\prime}$. The remaining expected
runtime is independent of the previous history of the performed random walk
and thus only depends on the event $A(\beta^{\prime})$. Now, replacing (74)
with (75) yields the proposition. ∎

While it turns out in Section 4.4.1 that we are able to analyze the
distribution of the random variable

$\boldsymbol{P}\coloneqq\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right)\mid\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{FirstSel}(c+1),\,A(\alpha)\big{)},$

appearing in line (64), and show that it is asymptotically Johnson SB
distributed, the distribution analysis of the more harmless-looking random
variable
$\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}$ appearing in line (60) requires further work.

The main idea in the following steps is to split the information that the
event $\operatorname{FirstSel}(c+1)$ contains into several events, apply the
chain rule and analyze the resulting cases separately. While in the beginning,
this might seem like a lot of unnecessary calculations, after being done, we
will reap the fruit of our labor: we will be able to conduct a distribution
analysis of all random variables easily. For this purpose, recall Definition
41: Let $\mathrm{Sel}(c)$ be the indicator variable being 1 if and only if a
clause in $\boldsymbol{\boldsymbol{L}}$ gets selected in the $c$-th iteration
of SRWA.

Following the above-specified plan, we next apply the chain rule to the random
variable
$\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}$. With the notation of Definition 41 in place, and using the
fact that

$\operatorname{FirstSel}(c+1)=\\{\mathrm{Sel}(c+1)=1\\}\cap\bigcap_{i=1}^{c}\\{\mathrm{Sel}(i)=0\\},$

one obtains

$\displaystyle\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\operatorname{FirstSel}(c+1)\mid
A(\alpha)\big{)}$ (79) $\displaystyle=$
$\displaystyle\>\,\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\\{\mathrm{Sel}(c+1)=1\\}\cap\bigcap_{i=1}^{c}\\{\mathrm{Sel}(i)=0\\}\;\stretchleftright{\mid}{\vphantom{\\{\mathrm{Sel}(c+1)=1\\}\cap\bigcap_{i=1}^{c}\\{\mathrm{Sel}(i)=0\\}A(\alpha)}}{.}\;A(\alpha)\right)$
(83) $\displaystyle=$
$\displaystyle\>\,\mathcal{D}_{1}\cdot\prod_{k=1}^{c}\mathcal{D}_{2},$ (84)

where

$\displaystyle\mathcal{D}_{1}$
$\displaystyle\coloneqq\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(c+1)=1\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(c+1)=1\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right),\text{
and }$ $\displaystyle\mathcal{D}_{2}$
$\displaystyle\coloneqq\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(k)=0\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(k)=0\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right).$

Here, the _nullary intersection_
$\bigcap_{j=1}^{0}\\{\mathrm{Sel}(j)=0\\}\coloneqq\Omega$, i. e., as the whole
sample space, because the condition of the intersection is a vacuous truth.

We analyze the random variables of the first factor, i. e., $\mathcal{D}_{1}$,
and the factors in the big product of line (84), i. e., $\mathcal{D}_{2}$,
separately in the cases A.1 and A.2 below. In Section A.3, we finish the case
analysis and present the central proposition of this appendix.

###  A.1 The Case $\boldsymbol{\mathrm{Sel}(c+1)=1}$ of the First Factor
$\mathcal{D}_{1}$ in Line (84)

With the LTP, conditioning on the event
$\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}$ one obtains

$\displaystyle\mathcal{D}_{1}$
$\displaystyle=\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(c+1)=1\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(c+1)=1\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)$
$\displaystyle=\sum_{\gamma:\,F\gamma=0}\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(c+1)=1\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(c+1)=1\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)$
$\displaystyle\phantom{=\sum_{\gamma:\,F\gamma=0}}\cdot\operatorname{\mathbb{P}}\left[\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right].$

Note that once again,
$\operatorname{\mathbb{P}}\left[\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right]$
does not depend on $\boldsymbol{\boldsymbol{L}}$ since the event
$\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\}$ rules out the usage of any clauses
of $\boldsymbol{\boldsymbol{L}}$ on the way from $\alpha$ to $\gamma$. One
readily checks that

$\displaystyle\begin{split}&\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(c+1)=1\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(c+1)=1\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)\\\
=\>&\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\mathrm{Sel}(c+1)=1\mid\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c},\,A(\alpha)\big{)}\\\
=\>&\boldsymbol{Q},\end{split}$ (85)

since SRWA has the property that past history does not matter, i. e., once the
algorithm has arrived in assignment $\gamma$ after $c$ steps, it does not
matter how it arrived in this assignment or what clauses it touched on its
way.

We will take care of the distribution analysis of the random variable
$\boldsymbol{Q}$ in Section 4.4.2.

###  A.2 The Case $\boldsymbol{\mathrm{Sel}(k)=0}$ of the Factors in the Big
Product of Line (84)

For $k\in\\{1,\dots,c\\}$ we analyze the factors in the big product of line
(84) with the LTP conditioning on
$\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1}$:

$\displaystyle\mathcal{D}_{2}$
$\displaystyle=\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(k)=0\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(k)=0\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)$
$\displaystyle=\sum_{\gamma:\,F\gamma=0}\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(k)=0\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(k)=0\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)$
$\displaystyle\phantom{=\sum_{\gamma:\,F\gamma=0}}\cdot\operatorname{\mathbb{P}}\left[\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1}\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right].$

An analogous argumentation as in Section A.1 shows that

$\operatorname{\mathbb{P}}\left[\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1}\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right]$

is no random variable. Similarly, one can use the reasoning brought forward in
the last section to see that

$\displaystyle\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\left(\mathrm{Sel}(k)=0\;\stretchleftright{\mid}{\vphantom{\mathrm{Sel}(k)=0\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\;\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,\bigcap_{j=1}^{k-1}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right)$
$\displaystyle=\>$
$\displaystyle\boldsymbol{\operatorname{\ThisStyle{\ooalign{$\SavedStyle\mathbb{P}$\cr\kern-0.18pt$\SavedStyle\mathbb{P}$\cr\kern
0.18pt$\SavedStyle\mathbb{P}$}}\\!}_{\boldsymbol{L}}}\big{(}\mathrm{Sel}(k)=0\mid\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{k-1},\,A(\alpha)\big{)}.$

We will use $\boldsymbol{R}$ in the following to denote the above specified
random variable. Its distribution analysis can be found in Section 4.4.3.

###  A.3 Putting Together Both Cases

Having obtained the results of the last two sections, we immediately arrive at
the following.

######  Proposition 64 (Analysis of the finite case $c<\infty$).

The term
$\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\alpha)\big{)}}$ can
be written as

$\displaystyle\sum_{c\in\mathbb{N}_{0}}\sum_{\beta:\,\boldsymbol{L}\beta=0}\left\\{C_{3}\left(\sum_{\gamma:\,F\gamma=0}C_{4}\cdot\boldsymbol{R}\right)\cdot\prod_{k=1}^{c}\left(\sum_{\gamma:\,F\gamma=0}C_{4}\cdot\boldsymbol{Q}\right)\right.\left.\cdot\sum_{x\in\boldsymbol{V}}\boldsymbol{P}\cdot\left(c+1+\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\beta^{\prime})\big{)}}\right)\right\\}+\mathcal{I},$

with the constants being defined by

$\displaystyle C_{3}\coloneqq C_{3}(\alpha,c,\beta)$
$\displaystyle\coloneqq\operatorname{\mathbb{P}}\bigl{[}\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c}\operatorname{FirstSel}(c+1),\,A(\alpha)}}{.}\,\operatorname{FirstSel}(c+1),\,A(\alpha)\bigr{]}\in[0,1],$
$\displaystyle C_{4}\coloneqq C_{4}(\alpha,c,\gamma)$
$\displaystyle\coloneqq\operatorname{\mathbb{P}}\left[\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}\stretchleftright{\mid}{\vphantom{\mathrm{From}_{\alpha}\mathrm{To}_{\gamma}\mathrm{In}_{c}\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)}}{.}\,\bigcap_{j=1}^{c}\\{\mathrm{Sel}(j)=0\\},\,A(\alpha)\right]\in[0,1],$

and the random variables $\boldsymbol{P}$, $\boldsymbol{Q}$, and
$\boldsymbol{R}$ as in Proposition 51.

###  A.4 Allowing Restarts

At the beginning of Section 4.3, we mentioned that our arguments implicitly
assume that SRWA does not employ any restarts. However, for the most part, our
arguments also apply to the restarted version of the algorithm. The only
technical challenge is adapting Equation (75) in the appendix:

$\displaystyle\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right),\,A(\alpha)\big{)}}=c+1+\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}A(\beta^{\prime})\big{)}}.$
(86)

Here, the difficulty is that after some flips, a restart is due, and thus SRWA
does not continue its search in $\beta^{\prime}\coloneqq\beta[x]$. Instead, a
new random assignment is chosen.

At its core, the reasoning behind Equation (86) is still valid. The left-hand
side of Equation (86) uses the condition $\operatorname{FirstSel}(c+1)$, which
tells us that the algorithm performed $c+1$ flips without finding a satisfying
assignment. The only difference is that SRWA might have performed one (or
several) restarts in the meantime. This can be handled by introducing an
additional counter $T$ in the expectation
$\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}$. The counter $T$ is used to
count the number of remaining flips until a restart is performed.
Incorporating this counter in the argument readily yields the following
equations:

$\displaystyle\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}T=0,\,A(\alpha)\big{)}}=\sum_{\beta\in\\{0,1\\}^{n}}\operatorname{\mathbb{P}}\bigl{[}A(\beta)\bigr{]}\cdot\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}T=t_{\textnormal{restart}},\,A(\beta)\big{)}},$

where $\operatorname{\mathbb{P}}\bigl{[}A(\beta)\bigr{]}=\frac{1}{2^{n}}$; and

$\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}{\big{(}\operatorname{FirstSel}(c+1),\,\mathrm{From}_{\alpha}\mathrm{To}_{\beta}\mathrm{In}_{c},\,\operatorname{Flip}_{\alpha}\\!\left(c,\beta,x\right),\,T=d,\,A(\alpha)\big{)}}\\\
=\>c+1+\boldsymbol{\operatorname{ER}_{\boldsymbol{L}}}\Big{(}T=\big{(}d-(c+1)\big{)}\bmod{t_{\textnormal{restart}}},A(\beta^{\prime})\Big{)}.$

The rest of the analysis remains unaltered besides the need to add the counter
$T$ in each part of the proofs.

##  Appendix B Connections Between Different Distributions

###  B.1 Embedded Models: Johnson SB Approaches Lognormal

In this section, we provide some details about the embedding property of
lognormal and Johnson SB distributions.

######  Lemma 65 ([Che17, JKB94]).

The lognormal distribution is an embedded model of the SB distribution.

###### Proof (adapted from [Che17]).

Reparametrizing with $b=\alpha^{-1}$ and
$\gamma=\delta\bigl{(}\ln{(\alpha^{-1}-a)}-\mu\bigr{)}$ yields

$\displaystyle
f(x)=\frac{1}{\sqrt{2\pi}}\frac{(\frac{1}{\alpha}-a)\delta}{(x-a)(\frac{1}{\alpha}-x)}\exp\biggl{\\{}-\frac{1}{2}\biggl{[}\delta\left(\ln{\left(\frac{1}{\alpha}-a\right)}-\mu\right)+\delta\ln{\frac{x-a}{\frac{1}{\alpha}-x}}\biggr{]}^{2}\biggr{\\}}.$

The log-likelihood function $\mathcal{L}$ is then given by:

$\displaystyle\mathcal{L}(a,\delta,\alpha,\mu)=-\frac{1}{2}\ln{2\pi}+\ln{\delta}+\ln{\frac{\frac{1}{\alpha}-a}{\frac{1}{\alpha}-x}}-\ln{(x-a)}-\frac{1}{2}\biggl{[}\delta\left(\ln{\frac{\frac{1}{\alpha}-a}{\frac{1}{\alpha}-x}}-\mu\right)+\delta\ln{(x-a)}\biggr{]}^{2}.$

Thus,

$\displaystyle\ell(a,\delta,\alpha,\mu)\coloneqq\frac{\partial}{\partial\alpha}\,\mathcal{L}(a,\delta,\alpha,\mu)=-\dfrac{\left(x-a\right)\left(\delta^{2}\ln\frac{\frac{1}{\alpha}-a}{\frac{1}{\alpha}-x}+\delta^{2}\ln\left(x-a\right)-\delta^{2}\mu-1\right)}{\left(a\alpha-1\right)\left(x\alpha-1\right)}.$

Furthermore, as

$\displaystyle\lim_{\alpha\rightarrow
0}\ln{\frac{\frac{1}{\alpha}-a}{\frac{1}{\alpha}-x}}=0$

holds, we have

$\displaystyle\lim_{\alpha\rightarrow
0}\,\mathcal{L}(a,\delta,\alpha,\mu)=-\frac{1}{2}\ln{2\pi}+\ln{\delta}-\ln{(x-a)}-\frac{1}{2}\bigl{[}\delta\ln{(x-a)}-\delta\mu\bigr{]}^{2}~{}\textnormal{and}$
$\displaystyle\lim_{\alpha\rightarrow
0}\,\ell(a,\delta,\alpha,\mu)=-\left(x-a\right)\left(\delta^{2}\ln\left(x-a\right)-\delta^{2}\mu-1\right).$

We represent $\mathcal{L}$ as a Taylor series of $\alpha$ in $\alpha=0$.
Observing this series expansion for $\alpha\rightarrow 0$ yields:

$\displaystyle\lim_{\alpha\rightarrow 0}\,\mathcal{L}(a,\delta,\alpha,\mu)$
$\displaystyle=\lim_{\alpha\rightarrow
0}\,\left(\mathcal{L}(a,\delta,0,\mu)+\ell(a,\delta,0,\mu)\cdot\alpha+\mathrm{O}(\alpha^{2})\right)$
$\displaystyle=-\frac{1}{2}\ln{2\pi}+\ln{\delta}-\ln{(x-a)}-\frac{1}{2}\delta^{2}\bigl{[}\ln{(x-a)}-\mu\bigr{]}^{2}$
$\displaystyle\phantom{==}+\left(x-a\right)\left[1+\delta^{2}\left(\mu-\ln\left(x-a\right)\right)\right]\lim_{\alpha\rightarrow
0}\,\alpha+\lim_{\alpha\rightarrow 0}\,\mathrm{O}(\alpha^{2})$
$\displaystyle=-\frac{1}{2}\ln{2\pi}+\ln{\delta}-\ln{(x-a)}-\frac{1}{2}\delta^{2}\bigl{[}\ln{(x-a)}-\mu\bigr{]}^{2}.$

This is precisely the log-likelihood function of a lognormal distribution.
Thus, the Johnson SB distribution approaches a lognormal distribution for
$\alpha\rightarrow 0$ (or $b\rightarrow\infty$ as well as
$\gamma\rightarrow\infty$ in the original parameterization222 There is a
slight typo in the quoted source [Che17], stating that $b$ should approach
zero. However, following the presented argument in [Che17], it is clear that
$b$ has to approach infinity since $\alpha$ approaches zero and
$b=\frac{1}{\alpha}$. ). ∎

###  B.2 A Proof of Lemma 54

In this section, we will prove one of our main lemmas. This lemma will be used
in the distribution analysis of the random variables $\boldsymbol{P}$,
$\boldsymbol{Q}$, and $\boldsymbol{R}$.

######  Lemma 66 (Lemma 54 restated).

Let $\boldsymbol{Y}\sim{\operatorname{LogN}\left(\mu,\sigma^{2}\right)}$, then
we have

$\frac{1}{c+\boldsymbol{Y}}\sim{\operatorname{SB}\left(\gamma=\frac{\mu-\ln
c}{\sigma},\,\delta=\frac{1}{\sigma},\,\lambda=\frac{1}{c},\,\xi=0\right)}$

for all $c\in\mathbb{R}^{+}$.

###### Proof of Lemma 54 (adapted from [Emp18]).

Let $\boldsymbol{W}\sim{\operatorname{N}\left(\mu,\sigma^{2}\right)}$. Then
$-\boldsymbol{W}\sim{\operatorname{N}\left(-\mu,\sigma^{2}\right)}$. By
definition,
$\boldsymbol{Y}\coloneqq\mathrm{e}^{\boldsymbol{W}}\sim{\operatorname{LogN}\left(\mu,\sigma^{2}\right)}$.
Define the random variable

$\boldsymbol{X}\coloneqq\frac{1}{c+\boldsymbol{Y}}=\frac{1}{c+\mathrm{e}^{\boldsymbol{W}}}=\frac{1}{c+c\cdot\mathrm{e}^{\boldsymbol{W}-\ln
c}}=\frac{1}{c+c\cdot\mathrm{e}^{\boldsymbol{W^{\prime}}}}=\frac{\mathrm{e}^{-\boldsymbol{W^{\prime}}}}{c\mathrm{e}^{-\boldsymbol{W^{\prime}}}+c},$

where

$\boldsymbol{W^{\prime}}\sim{\operatorname{N}\left(\mu-\ln
c,\sigma^{2}\right)}.$

A few simple rearrangements yield

$-\boldsymbol{W^{\prime}}=\log\left(\frac{c\boldsymbol{X}}{1-c\boldsymbol{X}}\right)=\log\left(\frac{\boldsymbol{X}}{\frac{1}{c}-\boldsymbol{X}}\right).$

Letting $\lambda\coloneqq 1/c$ and $\xi\coloneqq 0$, we have

$-\boldsymbol{W}=\log\left(\frac{\boldsymbol{X}-\xi}{\xi+\lambda-\boldsymbol{X}}\right).$

Define $\delta\coloneqq\frac{1}{\sigma}$ and $\gamma\coloneqq\frac{\mu-\ln
c}{\sigma}$ and let $\boldsymbol{Z}$ be a random variable such that

$\boldsymbol{Z}=-\boldsymbol{W^{\prime}}\cdot\delta+\gamma.$

Since

$-\boldsymbol{W^{\prime}}\sim{\operatorname{N}\left(\ln
c-\mu,\sigma^{2}\right)},$

we have

$-\boldsymbol{W^{\prime}}\cdot\delta\sim{\operatorname{N}\left(\frac{\ln
c-\mu}{\sigma},1\right)}$

and

$-\boldsymbol{W^{\prime}}\cdot\delta+\gamma\sim{\operatorname{N}\left(0,1\right)}.$

Per definition,
$\boldsymbol{X}\sim{\operatorname{SB}\left(\gamma=\frac{\mu-\ln
c}{\sigma},\,\delta=\frac{1}{\sigma},\,\lambda=\frac{1}{c},\,\xi=0\right)}$. ∎

###  B.3 A Proof of Lemma 55

Our aim in this section will be to provide a proof of Lemma 55. We have
restated the lemma below for convenience.

######  Lemma 67 (Lemma 55 restated, [Lac11]).

If $\boldsymbol{Y}\sim{\operatorname{Bin}\\!\big{(}n,\,p\big{)}}$, then
$\log\boldsymbol{Y}$ is asymptotically normally distributed.

For the proof of the lemma, we will need to introduce some technical
machinery.

######  Definition 68 (Order in probability).

For a sequence of random variables $(\boldsymbol{X_{n}})_{n\in\mathbb{N}}$ and
a corresponding sequence of constants $(a_{n})_{n\in\mathbb{N}}$, we write
$\boldsymbol{X_{n}}\in\mathrm{O}_{p}(a_{n})$ if for all $\varepsilon>0$, there
exists an $M>0$ and an $N>0$ such that

$\operatorname{\mathbb{P}}\left[\left|\frac{\boldsymbol{X_{n}}}{a_{n}}\right|>M\right]<\varepsilon\quad\text{for
all}\quad n>N.$

######  Definition 69.

An estimator $\boldsymbol{\hat{\theta}_{n}}$ is a _consistent estimator_ for
the parameter $\theta$ if
$\boldsymbol{\hat{\theta}}\underset{n\to\infty}{\overset{p}{\longrightarrow}}\theta$.
An estimator $\boldsymbol{\hat{\theta}_{n}}$ is a _$\sqrt{n}$ -consistent
estimator_ for the parameter $\theta$ if
$\boldsymbol{\hat{\theta}_{n}}-\theta=\mathrm{O}_{p}(1/\sqrt{n})$.

######  Example 70.

From the central limit theorem, it follows that for all $\varepsilon>0$ it
holds

$\operatorname{\mathbb{P}}\bigl{[}|\boldsymbol{\overline{X}_{n}}-\mu|>\varepsilon\bigr{]}=\operatorname{\mathbb{P}}\left[\frac{\sqrt{n}|\boldsymbol{X_{n}}-\mu|}{\sigma}>\frac{\sqrt{n}\varepsilon}{\sigma}\right]=2\left(1-\Phi\left(\frac{\sqrt{n}\varepsilon}{\sigma}\right)\right)\stackrel{{\scriptstyle
n\to\infty}}{{\longrightarrow}}0,$

i. e.,
$\boldsymbol{\overline{X}_{n}}\underset{n\to\infty}{\overset{p}{\longrightarrow}}\mu$.
Thus, $\boldsymbol{\overline{X}_{n}}$ is a consistent estimator for $\mu$.
Because
$\sqrt{n}\big{(}\boldsymbol{\overline{X}_{n}}-\mu\big{)}\underset{n\to\infty}{\overset{d}{\longrightarrow}}{\operatorname{N}\left(0,\sigma^{2}\right)}$,
we can also see that $\boldsymbol{\overline{X}_{n}}$ is a
$\sqrt{n}$-consistent estimator of $\mu$.

######  Theorem 71 (Slutsky’s Theorem).

Let
$(\boldsymbol{X_{n}})_{n\in\mathbb{N}},(\boldsymbol{A_{n}})_{n\in\mathbb{N}},(\boldsymbol{B_{n}})_{n\in\mathbb{N}}$
be sequences of random variables. If $\boldsymbol{X_{n}}$ converges to a
random variable $\boldsymbol{X}$ in distribution,
$\boldsymbol{X_{n}}\underset{n\to\infty}{\overset{d}{\longrightarrow}}\boldsymbol{X}$,
and $\boldsymbol{A_{n}}\underset{n\to\infty}{\overset{p}{\longrightarrow}}a$,
as well as
$\boldsymbol{B_{n}}\underset{n\to\infty}{\overset{p}{\longrightarrow}}b$, then

$\boldsymbol{A_{n}}+\boldsymbol{B_{n}}\boldsymbol{X_{n}}\underset{n\to\infty}{\overset{d}{\longrightarrow}}a+b\boldsymbol{X}.$

With these definitions in place, we can now prove Lemma 55.

###### Proof of Lemma 55 (adaped from [Lac11]).

Let $n\in\mathbb{N}^{+}$ and $p\in(0,1)$. For $i\in\\{1,\dots,n\\}$ let
$\boldsymbol{X_{i}}\sim{\operatorname{Bern}(p)}$. Let $(x_{1},\dots,x_{n})$
denote a corresponding sample of these random variables. Then,
$\boldsymbol{S_{n}}\coloneqq\boldsymbol{X_{1}}+\dots+\boldsymbol{X_{n}}\sim{\operatorname{Bin}\\!\big{(}n,\,p\big{)}}$.
Since

$\operatorname{\mathbb{E}}[\boldsymbol{\overline{X}_{n}}]=\operatorname{\mathbb{E}}\left[\frac{1}{n}\sum_{i=1}^{n}\boldsymbol{X_{i}}\right]=\frac{1}{n}\operatorname{\mathbb{E}}\left[\sum_{i=1}^{n}\boldsymbol{X_{i}}\right]=\frac{1}{n}\sum_{i=1}^{n}\operatorname{\mathbb{E}}[\boldsymbol{X_{i}}]=\frac{1}{n}np=p,$

a natural moment estimator of $p$ is the _sample mean_
$\boldsymbol{\overline{X}_{n}}\coloneqq\boldsymbol{S_{n}}/n$. In the
following, we let $\overline{x}_{n}\coloneqq\frac{1}{n}(x_{1}+\dots+x_{n})$
denote the concrete sample mean. Applying Taylor’s expansion to the mapping
$x\mapsto\log x$, we obtain

$\log\overline{x}_{n}=\log p+\frac{\mathrm{d}\log
p}{\mathrm{d}p}(\overline{x}_{n}-p)+R_{2}(\xi),$

where

$R_{2}(\xi)=\frac{\mathrm{d}^{2}\log\xi}{\mathrm{d}\xi^{2}}(\overline{x}_{n}-p)^{2}$

is the Lagrange remainder term and $\xi$ lies between $\overline{x}_{n}$ and
$p$. Since $\log^{\prime}(x)=\frac{1}{x}$ and
$\log^{\prime\prime}(x)=-\frac{1}{x^{2}}$ for all $x>0$, this yields to

$\sqrt{n}\big{(}\log\overline{x}_{n}-\log
p\big{)}=\sqrt{n}\frac{\overline{x}_{n}-p}{p}-\sqrt{n}\frac{(\overline{x}_{n}-p)^{2}}{2\xi^{2}}.$

It is well known that $\boldsymbol{\overline{X}_{n}}$ is asymptotically normal
distributed (and the same holds for the concrete realizations
$\overline{x}_{n}$), more precisely

$\overline{x}_{n}\stackrel{{\scriptstyle
d}}{{\approx}}{\operatorname{N}\left(p,\frac{p(1-p)}{n}\right)}.$

Thus, the first term on the right-hand side,
$\sqrt{n}\frac{\overline{x}_{n}-p}{p}$, is likewise asymptotically normal
distributed, more precisely

$\sqrt{n}\frac{\overline{x}_{n}-p}{p}\stackrel{{\scriptstyle
d}}{{\approx}}{\operatorname{N}\left(0,\frac{1-p}{p}\right)}.$

In Example 70, we saw that $\overline{x}_{n}$ is a $\sqrt{n}$-consistent
estimator of $p$. Hence, $(\overline{x}_{n}-p)^{2}\to 0$ as $n\to\infty$
faster than $n^{-1/2}$. Thus,

$\sqrt{n}R_{2}(\xi)\underset{n\to\infty}{\overset{p}{\longrightarrow}}0.$

Therefore, asymptotically $\sqrt{n}\big{(}\log\overline{x}_{n}-\log p\big{)}$
is the sum of two random variables, the first one converging in distribution
to the normal, the second one converging in probability to zero (i. e., a
constant). From Slutsky’s Theorem, it follows that

$\sqrt{n}\big{(}\log\overline{x}_{n}-\log
p\big{)}\underset{n\to\infty}{\overset{d}{\longrightarrow}}{\operatorname{N}\left(0,\frac{1-p}{p}\right)}.$

Hence,

$\displaystyle\log\overline{x}_{n}\stackrel{{\scriptstyle
d}}{{\approx}}{\operatorname{N}\left(\log p,\frac{1-p}{np}\right)}.$

In other words, $\overline{x}_{n}$ is asymptotically lognormal distributed.
Since $\overline{x}_{n}$ is binomially distributed, the claim follows. ∎