Too much information: why CDCL solvers need to forget learned clauses

Tom Krüger1*, Jan-Hendrik Lorenz1, Florian Wörz1*

1 Institute of Theoretical Computer Science, Universität Ulm, 89069 Ulm,
Germany

All authors contributed equally to this work and are sorted alphabetically.

* Corresponding authors<EMAIL_ADDRESS><EMAIL_ADDRESS>
## Abstract

Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for
solving the satisfiability problem of propositional logic. Instead of a simple
depth-first backtracking approach, this kind of solver learns the reason
behind occurring conflicts in the form of additional clauses. However, despite
the enormous success of CDCL solvers, there is still only a limited
understanding of what influences the performance of these solvers in what way.

Considering different measures, this paper demonstrates, quite surprisingly,
that clause learning (without being able to get rid of some clauses) can not
only help the solver but can oftentimes deteriorate the solution process
dramatically. By conducting extensive empirical analysis, we furthermore find
that the runtime distributions of CDCL solvers are multimodal. This
multimodality can be seen as a reason for the deterioration phenomenon
described above. Simultaneously, it also gives an indication of why clause
learning _in combination with_ clause deletion is virtually the de facto
standard of SAT solving, in spite of this phenomenon. As a final contribution,
we show that Weibull mixture distributions can accurately describe the
multimodal distributions. Thus, adding new clauses to a base instance has an
inherent effect of making runtimes long-tailed. This insight provides an
explanation as to why the technique of forgetting clauses is useful in CDCL
solvers apart from the optimization of unit propagation speed.

##  1 Introduction

Since their inception in the mid-90s [1, 2], CDCL solvers have proven
enormously successful in solving the satisfiability problem of propositional
logic (SAT). As a case in point, we refer to the annual SAT Competition111The
goal of the annual SAT Competition is to promote further improvements in the
field of SAT solving by hosting a competitive event where researchers can
present their newest implementation work. All submitted solvers are put up
against each other to solve a pool of instances. The fastest solver wins. We
refer to http://www.satcompetition.org for more detailed information.: CDCL
solvers won several of the last competitions. In many combinatorial fields,
applied problems are nowadays even solved by reducing the problem to a SAT
instance and invoking a CDCL solver (see e. g. [3]), despite the
$\mathsf{NP}$-completeness of the SAT problem.222SAT solvers have also been
used in the last few years to generate computerized proofs of long-standing
open problems. We refer to [4] for a solution of the Boolean Pythagorean
Triples problem, [5] for Schur number five, or [6] for the resolution of
Keller’s Conjecture with SAT solvers.

The abbreviation CDCL stands for _conflict-driven clause learning_. The
eponymous component of CDCL is _clause learning_ , a mechanism that can
enhance the simple exhaustive exploration of the search tree for possible
satisfying assignments by learning from mistakes made and avoiding these in
the future. During its execution, the solver learns additional clauses
containing this learned information (we refer to Section 2.1 for an
introduction to CDCL solvers). This enables the solver to prune the search
tree and avoid re-exploring similar parts.

In addition to a clause learning scheme, many modern CDCL solvers also employ
a technique to delete some of the new clauses from time to time when they were
deemed not helpful by the solver. However, it is still largely a mystery
whether this deletion process is only used to keep computation times low by
having a manageable clause database or if there is some theoretical benefit to
deleting clauses.

Although both techniques, clause learning and clause deletion, are routinely
employed in modern CDCL solvers, the theoretical underpinnings of the
interactions between the two techniques are not entirely understood [7].

###  1.1 Our contribution

To study the effect of learned clauses on CDCL solvers, we let Glucose 4.1
(see [8, 9]), a leading CDCL solver, first learn the set $\mathbb{L}$ of all
conflict clauses it encounters until a solution of a given instance
$\mathscr{F}$ is found.333We have chosen a diverse set of satisfiable as well
as unsatisfiable instances. We refer to Section 3. In a second step, we
generate a multitude of different sets $L$, where each $L$ is a randomly
sampled subset of $\mathbb{L}$. Finally, we call Glucose 4.1 on the extended
instance $\mathscr{F}\cup L$. This model can be thought of in the following
way: we simulate that the solver learns the clauses $\mathbb{L}$ and then
aggressively deletes some of the learned clauses (only keeping the ones in
$L$) and forgets its current assignment (we refer to this as a “reset”).

Since CDCL is nowadays the leading paradigm of successful SAT solvers, one is
tempted to conjecture that clause learning is always helpful. However, using
the described modification process, we demonstrate in this paper that one must
be careful about this assumption. More specifically, we show that there are a
surprising number of instances where the mean runtime of the extended
instances is dramatically worse than the runtime on the original instance.
This also holds, using runtime-independent measures like the number of
conflicts or propagations that occurred towards a solution. This observation
shows that the observed deterioration phenomenon cannot solely be explained by
a decrease in the unit propagation speed. In particular, we have designed our
sampling process in such a way that the size of the formula does not increase
too much, and unit propagations can be performed at a reasonable cost.

Furthermore, the performance decrease is so substantial that it cannot be
explained by pure chance. This motivates the study of the runtime distribution
of extended instances to shed light on the question of what influence learned
clauses have on CDCL solvers. Focusing on the runtime distribution, we obtain
as our next result that the runtime distribution of Glucose 4.1 is multimodal.
The observed multimodality contrasts the recently obtained result that the
runtime distribution of stochastic local search (SLS) SAT solvers can be
described with a single distribution (namely, a lognormal distribution) [10].

We continue our study to determine what kind of distribution type can be used
to describe this multimodal data. We demonstrate that the runtimes of Glucose
4.1 are mixed Weibull distributed by conducting various statistical analyses.
These distributions possess the long-tailed property for a specific parameter
range, which can lead to exceedingly long runtimes. We also verify this
observation with the Glucose 4.1 solver together with Chanseok Oh’s deletion
strategy and with MiniSAT [11], a minimalist CDCL solver. This leads to a
better understanding of the usefulness of clause deletion techniques in CDCL
solvers.

###  1.2 Related work

This section gives a brief overview of related works in both the study of
runtime distributions and the research on CDCL solvers.

##### Studying runtime distributions of algorithms.

In previous works, the runtime distributions of algorithms were studied. In
[12], 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). Later, these results were extended to a wider
region around the 50 % satisfiable point [13]. In [14], the cost profiles of
combinatorial search procedures were studied. The authors showed that Pareto-
Lévy type heavy-tails often characterize the distributions and empirically
demonstrated how rapid randomized restarts can effectively eliminate heavy-
tail behavior.

In the paper [10], the hardness distributions of several SLS SAT solvers on
logically equivalent modifications of a base instance were studied. The
authors included different instance generation models to rule out any
influence of the model. Introducing the procedure Alfa that we adapt to CDCL
solvers in our work, the paper found that lognormal distributions characterize
this hardness distribution perfectly. The approach of [10] lends itself to the
analysis of existing SLS-CDCL hybrid solvers, like GapSAT [15]. The advantage
of the approach studied in [10] 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. The paper [16] studied the solvers
Sparrow and CCASAT and found that for randomly generated instances, the
lognormal distribution is a good fit for the runtime distributions. This study
was performed on the domains of randomly generated and crafted instances.

Barrero et al. [17] observed empirical evidence suggesting lognormally
distributed runtimes in several types of population-based algorithms like
evolutionary and genetic algorithms.

##### Experimental studies on CDCL solvers.

The reason behind the fact that CDCL algorithms also incorporate a mechanism
to delete (subsets of the) learned clauses from time to time was explained by
Mitchell in [18]: Even when sufficient memory is available, the time required
to perform unit propagation becomes impractical for extensive clause sets,
thus reducing the solver’s performance. Audemard and Simon [9] observed that
despite this phenomenon, deleting too many learned clauses can break the
learning benefit. Thus, many CDCL solvers let the maximum number of learned
clauses grow exponentially. The paper [9] lead to the development of the
Glucose solver using “aggressive clause deletion” together with the “Literals
Block Distance (LBD)” measure. Some solvers also incorporate a dynamic clause
management policy, allowing the solver to _freeze_ some learned clauses for
later use instead of deleting them [19]. In [20], CDCL solver heuristics such
as restarts and clause database management frameworks were analyzed by
studying the resolution proofs produced by the solvers.

##### Theoretical studies on CDCL solvers.

While our study is purely empirical, it is interesting nevertheless to mention
a selection of papers that study CDCL from a theoretical perspective. The
field of proof complexity aims at gaining a theoretical understanding of the
reasoning power of different proof systems. It is well-known that an implicit
CDCL run can be interpreted as resolution proof. In the opposite direction,
there has been a line of research [21, 22, 23] investigating the proof-
theoretic strength of CDCL. This research culminated in papers proving that
CDCL (with non-deterministic variable decisions) can efficiently reproduce
resolution proofs [24] and CDCL (with random variable decisions) can
efficiently find bounded-width resolution proofs [25]. The complexity-
theoretic power of restart in SAT solvers was studied in [26].

###  1.3 Organization of this paper

The rest of this paper is organized as follows. First, in Section 2, we
introduce the notations of the field of SAT solving that we are using, give a
short overview of the technique of conflict-driven clause learning, and give
some statistical background, especially of survival analysis. We proceed to
describe the experimental setup in Section 3. Finally, Section 4 investigates
whether clause learning is useful on average. Section 5 demonstrates that the
runtime distributions of CDCL solver configurations we investigated exhibit a
multimodal behavior. This investigation is continued in Section 6, where it is
shown that the Weibull mixture distribution is a suitable fit for the runtime
distributions of these CDCL solvers.

##  2 Preliminaries

A _literal_ $\ell$ over a Boolean variable $x$ is either $x$ itself or its
negation $\overline{x}\coloneqq\neg x$. A _clause_
$C=(\ell_{1}\lor\dots\lor\ell_{k})$ is a (possibly empty) disjunction of
literals $\ell_{i}$. If a clause contains only one literal, it is called
_unit_. A _CNF formula_ $\mathscr{F}=C_{1}\land\dots\land C_{m}$ is a
conjunction of clauses. We also write clauses as a set of literals and CNF
formulas as a set of clauses. An _assignment_ $\alpha$ for a CNF formula
$\mathscr{F}$ is a function that maps some subset of the variables occurring
in $\mathscr{F}$ to $\\{0,1\\}$. By naturally extending $\alpha$ by the
definition $\alpha(\overline{x})\coloneqq\overline{\alpha(x)}$, we can define
the result of applying $\alpha$ to a clause $C$, which we denote by
$C|_{\alpha}$: one deletes all occurrences of literals $\ell$ from $C$, where
$\alpha(\ell)=0$; if there is a literal $\ell\in C$ with $\alpha(\ell)=1$,
then $C|_{\alpha}=1$. The notation $\mathscr{F}|_{\alpha}$ denotes the formula
where all clauses containing a literal $\ell$ with $\alpha(\ell)=1$ are
deleted, and each remaining clause $C$ is replaced by $C|_{\alpha}$. A clause
$C$ is called a _logical consequence_ of a formula $\mathscr{F}$ if, for all
assignments $\alpha$ with $\mathscr{F}|_{\alpha}=1$, it also holds
$C|_{\alpha}=1$. A set $L$ of clauses is a logical consequence of
$\mathscr{F}$ if each clause $C\in L$ is a logical consequence of
$\mathscr{F}$. We then call the formulas $\mathscr{F}$ and $\mathscr{F}\cup L$
_logically equivalent_.

###  2.1 Conflict-driven clause learning solvers

_Conflict-driven clause learning_ SAT algorithms, or _CDCL_ for short, are one
of the most remarkable success stories in computer science. Introduced in the
works [1] and [2], CDCL can yield dramatic speedups over the simple recursive
depth-first backtracking approach DPLL [27, 28]. The DPLL algorithm
essentially selects an unassigned variable $x$ of the formula $\mathscr{F}$ it
is trying to solve, and branches with calls to $\texttt{DPLL}(F|_{[x=0]})$ and
$\texttt{DPLL}(F|_{[x=1]})$. While CDCL has been intensely studied by
theoreticians and practitioners, we still do not have a complete understanding
of _all_ mechanisms involved.

####  2.1.1 Clause learning

In the following, we give a simple introduction to one of the most fundamental
CDCL techniques: _clause learning_. Informally speaking, this can be seen as a
modification of DPLL, where the algorithm adds some clauses to $\mathscr{F}$
if it reaches a conflict, i. e., when the partial assignment constructed thus
far falsifies a clause in $\mathscr{F}$. The idea behind this is to prune the
search tree and avoid having to re-explore some literal assignments that will
not lead to a solution.

We introduce clause learning mostly by example, following the exposition in
[29], and refer the reader to [3, 30] for more details. As an example,
consider as solver input the formula given in conjunctive normal form

$\displaystyle\begin{aligned} &(\overline{x_{1}}\lor
x_{2})\land(\overline{x_{2}}\lor x_{3}\lor
x_{4})\land(\overline{x_{2}}\lor\overline{x_{5}})\land(\overline{x_{4}}\lor
x_{5}\lor x_{6})\,\land\\\ &(\overline{x_{7}}\lor
x_{8})\land(\overline{x_{8}}\lor\overline{x_{9}})\land(x_{9}\lor\overline{x_{10}})\land(x_{3}\lor\overline{x_{8}}\lor
x_{10}).\end{aligned}$ (1)

Suppose that the CDCL solver makes its first _decision_ to assign $x_{1}=1$.
The solver always looks out for clauses where all literals but one are
assigned value 0 by the current assignment, and the remaining literal is
unassigned (so-called _unit clauses_) [3] and assign this remaining literal so
that the clause is satisfied. This process is called _unit propagation_ and is
repeated until there are no more unit clauses. In our example, using unit
propagation, the solver sets $x_{2}=1$ due to the clause
$\left(\overline{x_{1}}\lor x_{2}\right)|_{[x_{1}=1]}$. It then sets $x_{5}=0$
because of the clause
$(\overline{x_{2}}\lor\overline{x_{5}})|_{[x_{1}=1,\>x_{2}=1]}$. No more
assignments can be made by unit propagation. To move things further along, the
solver has to make another decision. In our example, the solver now decides to
set $x_{3}=0$. By unit propagation, $x_{4}=1$ and $x_{6}=1$ are assigned.
Suppose, in its third decision, the solver sets $x_{7}=1$. Using unit
propagation, the assignments $x_{8}=1$, $x_{9}=0$, $x_{10}=1$, _and_
$x_{10}=0$ are made. This is a _conflict_ since the variable $x_{10}$ cannot
be set to both $0$ and $1$.

Fig 1: Conflict graph. The figure shows the conflict graph generated in our
example run of CDCL when solving formula (LABEL:eq:FormulaForCDCL). The
decision literals are marked in gray. The conflict literals are marked in red.
The reason(s) for a propagation is given as label(s) of the edge(s). The first
unique implication point (1UIP) is shown in blue. The 1UIP cut is the dashed
blue line leading to the learned clause $(x_{3}\lor\overline{x_{8}})$. The
graphic is adapted from [29].

During _conflict analysis_ , the solver learns a new clause. For this process,
the solver uses the _implication graph_ that was built in stages during the
execution of the algorithm (see Fig 1). In this graph, _decision literals_ (in
our example, $x_{1}$, $\overline{x_{3}}$, and $x_{7}$) are the source
vertices. The _conflict literals_ in our example are $x_{10}$ and
$\overline{x_{10}}$. Furthermore, the graph includes vertices for every
literal that has been assigned the value $1$. A directed edge from node $u$ to
node $v$ is included if the value of $v$ was set by unit propagation and
$\overline{u}$ occurs in the clause that was the _reason_ for variable $v$
being set.

The _level_ of a decision variable $x$ is defined as the number of decision
variables that have been assigned before $x$ plus 1. Literals that are implied
by unit propagation by a decision literal $x$ have the same level as $x$. In
our example, $x_{1},x_{2},\overline{x_{5}}$ have level 1;
$\overline{x_{3}},x_{4},x_{6}$ are level 2; and
$x_{7},x_{8},\overline{x_{9}},x_{10},\overline{x_{10}}$ are at the _conflict
level_ 3.

A vertex $v$ is called _UIP_ (_unique implication point_), if all paths from
the conflict level decision literal $x_{7}$ to the conflict literals
$x_{10},\overline{x_{10}}$ run through $v$. Here, $x_{7}$ and $x_{8}$ are
UIPs. The UIP closest to the conflict literals is called _first UIP_ (_1UIP_)
[31]. In our example, $x_{8}$ is the 1UIP. While there are many ways to learn
clauses from conflicts, the most popular method, invoked by a majority of
modern CDCL solvers, is based on the 1UIP learning scheme.444This learning
scheme is considered to work best (see [32] for a comparative study of
different learning schemes). In this scheme, the implication graph is uniquely
cut such that

  1. 1.

the 1UIP and all literals assigned before the conflict level are on one side,

  2. 2.

while all literals assigned after the 1UIP are on the other side (cf. [18]).

This cut, shown in Fig 1, yields the literals $\overline{x_{3}}$ and $x_{8}$
as starting points of the separated edges. The clause
$\neg(\overline{x_{3}}\land x_{8})=(x_{3}\lor\overline{x_{8}})=:C$ can be
shown to be a logical consequence of the original formula. This clause is
called the _learned clause_. The solver adds this clause to the clause set.

Using so-called _non-chronological backtracking_ , the solver now jumps back
to the level of the last variable in $C$ being assigned before the variable
$x_{8}$ of the conflict level, i. e., it jumps back to level 2, where
$\overline{x_{3}}$ was assigned. Then, using unit propagation on the clause
$C$, the variable $x_{8}$ would be assigned $0$.

####  2.1.2 Clause deletion and literal block distance

Many CDCL algorithms also incorporate a mechanism to delete (subsets of the)
learned clauses from time to time. As Mitchell explains in [18], this is due
to the fact that even when sufficient memory is available, the time required
to perform unit propagation becomes impractical for very large clause sets,
thus reducing the performance of the solver. However, deleting too many
learned clauses breaks down the learning benefit [33]. To identify good
learned clauses during the search, [9] introduced the notion of literal
blocks. Intuitively, this measure tries to capture semantic relations between
literals.

######  Definition 2.1 ([9]).

Let $C$ be a learned clause that is being falsified by the current partial
assignment. Suppose $C$ is being partitioned into $k$ literal sets with
respect to their level. The _literal block distance_ (_LBD_) of the clause $C$
is defined to be $k$.

Clauses with higher LBD are considered to be less useful. Other measures
considered when deleting clauses are the size, age, and activity of a clause
[34].

###  2.2 Statistical background

This section briefly introduces the statistical tools used in this paper.

######  Definition 2.2 ([35]).

Let $X$ be a real-valued random variable.

  * •

Its _cumulative distribution function_ (_cdf_) is the function
$F\colon\mathbb{R}\to[0,1]$ with

$F_{X}(t)\coloneqq\operatorname{\mathbb{P}}\left[X\leq t\right].$

  * •

Its _quantile function_ $Q_{X}\colon(0,1)\to\mathbb{R}$ is given by

$Q_{X}(p)\coloneqq\inf\big{\\{}t\in\mathbb{R}\bigm{|}F_{X}(t)\geq p\big{\\}}.$

  * •

If there is a non-negative, integrable function $f_{X}$ such that

$F_{X}(t)=\int_{-\infty}^{t}f_{X}(u)\,\mathrm{d}u,$

then we call $f_{X}$ the _probability density function_ (_pdf_) of $X$.

  * •

The _survival function_ of $X$ is given by

$S_{X}(t)\coloneqq\operatorname{\mathbb{P}}\left[X>t\right]=1-F_{X}(t).$

We need the fact that the quantile function is the inverse of the cdf in the
next section.

####  2.2.1 Visual data analysis

To compare two probability distributions, we use the explorative graphical
tool of _Q–Q plots_. These plots compare two distributions by plotting their
quantiles against each other. If the result is a line, one can assume that the
underlying distributions are the same.

######  Definition 2.3.

Let $F$ and $G$ be two cdfs. Then the graph
$\big{(}F^{-1}(p),G^{-1}(p)\big{)}$ for $0<p<1$ is called _Q–Q plot_ of $F$
and $G$.

######  Remark 1 ([36]).

If $F$ and $G$ are identical, the Q–Q plot is the main diagonal. If
$F(x)=G\left(\frac{x-\mu}{\sigma}\right)$, then $F^{-1}(p)=\mu+\sigma
G^{-1}(p)$. Thus, the Q–Q plot of $F$ and $G$ shows a linear relationship of
slope $\sigma$ and intersection $\mu$.

In a goodness-of-fit problem, one theoretical cdf is given, and we have
empirical observations drawn from the other distribution.

######  Definition 2.4.

Given a sample $y_{(1)}\leq y_{(2)}\leq\dots\leq y_{(k)}$, we let
$p_{i}\coloneqq\hat{F}_{n}(y_{i})$ and $x_{i}\coloneqq Q(p_{i})$, where
$\hat{F}_{n}$ is the empirical cumulative distribution function and $Q$ is the
theoretical quantile function of a theoretical distribution function $F$. In
the _Q–Q plot_ , we plot the points $(x_{i},y_{i})$ for $i=1,\dots,k$.

####  2.2.2 Survival analysis and censored data

We use survival analysis (see [37] for an introduction to the subject) to
analyze data in which the time until an event is of interest. The time until
this event happens is called _event time_. If all events are observed, we can
estimate the cdf with the help of the observations, for which we use the
empirical cdf.

######  Definition 2.5.

Let $X_{1},\dots,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},\dots,x_{n})$
is defined as

$\hat{F}_{n}(t)\coloneqq\frac{1}{n}\sum_{i=1}^{n}\mathbbm{1}_{\\{x_{i}\leq
t\\}},\quad t\in\mathbb{R},$

where $\mathbbm{1}_{A}$ is the indicator function of event $A$.

Since in some of our experiments, it turned out to be computationally
infeasible to wait until all formula instances are solved, we use a tool from
non-parametric statistics to estimate the survival function of the
corresponding runtime random variable. That is, we are working with incomplete
observations. To nevertheless estimate the survival function from a sample of
censored survival data, we use the Kaplan–Meier product-limit estimator [38,
39].

Let $T$ be a non-negative random variable (which indicates the time until an
event of interest takes place, e. g., finding the solution of a formula). Let
$t_{1},\dots,t_{k}$ be the points in time when events $1,\dots,k$ would have
happened (think of a solution for formula $\mathscr{F}_{j}$ being found if the
solver was not stopped) whose common distribution is that of $T$. _Right-
Censoring_ is present when we have some information about event time (e. g.,
the solver was still running at a certain point in time), but for some events,
we do not know the exact event time (because we stopped the solver early).
More precisely, to avoid excessively long runtime, we later choose for every
$j\in\\{1,\dots,k\\}$ a fixed integer $c_{j}$ as the _censoring time_ for
event $j$ (meaning that after this time, the solving of $\mathscr{F}_{j}$ is
aborted). Then, the data available for estimating the survival function
$S_{T}$ of the random variable $T$ is the sequence of observations

$\big{(}(\widetilde{t}_{j},c_{j})\big{)}_{j=1,\dots,k}\quad\text{ with
}\quad\widetilde{t}_{j}\coloneqq\min\\{t_{j},c_{j}\\},$

as well as _censoring indicators_ $\mathrm{cen}_{j}\in\\{0,1\\}$ of the form

$\displaystyle\mathrm{cen}_{j}=0:\\!\iff t_{j}<c_{j}.$ (2)

That is, we either know that the formula $\mathscr{F}_{j}$ was solved in time
(and we know the time $t_{j}$ needed for this), or we know that the solver was
still running at the censoring time $c_{j}$.

######  Definition 2.6 ([38, 39]).

The _Kaplan–Meier estimator_ is given by

$\widehat{S}_{T}(t)\coloneqq\prod_{i:\,t_{i}\leq
t}\left(1-\frac{d_{i}}{n_{i}}\right),$

where (in our case)

  * •

$t_{i}$ is a point in time when (at least one) formula was solved,

  * •

$d_{i}$ is the number of experiments, where the solver finished at time
$t_{i}$, and

  * •

$n_{i}$ is the number of experiments that have not yet had an event or have
not been censored up to time $t_{i}$.

If there are no censored observations, the Kaplan–Meier estimator reduces to
one minus the empirical cumulative distribution function (see e. g. [37]),
also known as the empirical survival function.

##  3 Experimental setup

There have been significant advances in the theoretical field of proof
complexity developing a theoretical understanding of CDCL solvers, as we have
surveyed in Section 1.2. Unfortunately, no model completely captures clause
deletion in CDCL solvers. For example, in [21, 24, 25], the analyses of
theoretical solvers rely crucially on the assumption that the learned clauses
are never deleted. For these reasons, an experimental approach seems the most
reasonable to investigate the effect of pre-learned clauses and clause
deletion.

Let us briefly summarize our experimental approach before discussing its
details. First, we recorded all learned clauses $\mathbb{L}$ a CDCL solver
will find on “its way towards” a solution of a formula $\mathscr{F}$; then, we
extended the original instance with subsets $L\subseteq\mathbb{L}$ of these
pre-learned clauses; and finally, we analyzed the runtime of such extended
instances compared to the original instance $\mathscr{F}$ (see Section 3.1 for
additional details on and a discussion of this modification process).

We now describe our CDCL solver configurations and choice of benchmarks.

##### Investigated solvers and deletion strategies.

Our SAT solver of choice for the majority of our experiments was Glucose 4.1
(see [8, 9]) in the non-parallelized version. First introduced in 2009, the
Glucose project, which is based on the famous MiniSAT solver [11], was quite
successful in the past SAT Competitions. To increase confidence in the
results, we also performed experiments using the deletion strategy of Chanseok
Oh in combination with the Glucose 4.1 solver. We furthermore extended the
examination to the MiniSAT solver.

##### Instances.

We obtained a relevant, diverse, and well-documented pool of satisfiable and
unsatisfiable instances by choosing all instances from the SAT Competition
2020, which were solved by Glucose 3.0 between $30\text{\,}\mathrm{min}$ and
$5000\text{\,}\mathrm{s}$ ($\approx$ $83\text{\,}\mathrm{min}$).555Glucose 3.0
was used for the filtering of the instances. We, however, later used Glucose
4.1 for our experiments as this was the newest version of the solver that was
available at the start of our experiments. This solver did not yet participate
in the SAT Competition 2020. The upper bound comes from a time limit imposed
in the SAT Competition, where all solvers are cut off after 5000 s. A more
detailed description of all selected instances can be found in S2 Table.. We
also refer to the proceedings of the SAT Competition 2020 [40, 41]. A vigilant
reader may notice that we have 53 instances in our pool, whereas our selection
criterion applies to 61 instances of the SAT Competition 2020. We eliminated
the remaining eight instances from the pool because they caused technical
complications in at least one stage of our experimental setup. For example,
three cases failed during clause recording as the number of learned clauses
was too high and the required disk space to save all of them exceeded all
reasonable limits. On the remaining five instances, Glucose 4.1 ran out of RAM
for some extensions. These cases could skew the runtime analysis since we do
not know how Glucose 4.1 would have performed with enough memory. Therefore,
we excluded them from the analysis.

###  3.1 Generating extensions from learned clauses

During execution, modern CDCL solvers learn plenty of clauses. All these
learned clauses are directly implied by the clauses of the initial formula
$\mathscr{F}$, which means that $\mathscr{F}\cup L$ is logically equivalent to
$\mathscr{F}$ for all $L\subseteq\mathbb{L}$, with $\mathbb{L}$ being the set
of all learned clauses. We call $L$ an _extension_ of the _base instance_
$\mathscr{F}$ and $\mathscr{F}\cup L$ an _extended instance_.

Input: Boolean formula $\mathscr{F}$ (the base instance) Let $\mathbb{L}$ be
the set of all learned clauses during the execution of
CDCLSolver$(\mathscr{F})$

$L\coloneqq\emptyset$

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

with probability _$p$_ do $L\coloneqq L\cup\\{C\\}$

Call CDCLSolver$(\mathscr{F}\cup L)$ and record several performance measures

Algorithm 1 Modified version of a CDCL Solver. We used this modified version
of $\texttt{CDCLSolver}{}\in\big{\\{}\texttt{Glucose}\leavevmode\nobreak\
\texttt{4.1}{},\>\texttt{Glucose}\leavevmode\nobreak\
\texttt{4.1}{}\texttt{\,+\,ChanseokOh},\>\texttt{MiniSAT}{}\big{\\}}$ in our
experiments to model the clause learning and clause deletion process as a
random process. Each call of this modified algorithm uses CDCLSolver to solve
an extended instance $\mathscr{F}\cup L$. This allows us to study the runtime
distribution of CDCLSolver.

##### Our model.

We adapt the approach presented in [10] to CDCL solvers. We refer to Algorithm
1, which requires a pool of pre-learned clauses $\mathbb{L}$. These clauses
were gathered by running
$\texttt{CDCLSolver}{}\in\big{\\{}\texttt{Glucose}\leavevmode\nobreak\
\texttt{4.1}{},\>\texttt{Glucose}\leavevmode\nobreak\
\texttt{4.1}{}\texttt{\,+\,ChanseokOh},\>\texttt{MiniSAT}{}\big{\\}}$ on a
base instance $\mathscr{F}$ and logging all learned clauses to a file. Thus,
the set $\mathbb{L}$ contains all clauses CDCLSolver learned “on its way” to a
satisfying assignment or to an unsatisfiability proof. The random sampling of
a subset $L\subseteq\mathbb{L}$ was implemented by independently selecting
each clause in the pool $\mathbb{L}$ with probability $p$. This subset $L$ is
used to study the runtime of CDCLSolver on the extended instance
$\mathscr{F}\cup L$. For our experiments, we chose $p=0.01$ and generated $N$
different extensions $L^{(1)},\dots,L^{(N)}$ for each of the 53 base instances
in our instance pool. That is, for each base instance $\mathscr{F}$, we
recorded the performance measures (runtime, number of conflicts, number of
propagations, etc.) of CDCLSolver on the extended instances $\mathscr{F}\cup
L^{(1)},\dots,\mathscr{F}\cup L^{(N)}$. We chose $N=5000$ for Glucose 4.1 and
$N=1000$ for the additional experiments with Glucose 4.1 \+ ChanseokOh and
MiniSAT. In this way, we can study the performance of CDCLSolver on instances
that _already_ contain some of the learned clauses.

The scripts for generating the sets $\mathbb{L}$ corresponding to the base
instances, as well as the scripts for reconstructing our sampled sets $L$ can
be found in S1 File.. Regarding only the experiments where
$\texttt{CDCLSolver}{}=\texttt{Glucose}\leavevmode\nobreak\ \texttt{4.1}{}$,
we produced 1.5 TB of instance data in the DIMACS format. Recording the
performance, we used $265\,000$ calls of Algorithm 1 with sometimes
surprisingly long runtimes.

##### Interpretation of the model.

Our model can be interpreted in the following two ways:

  1. (a)

We force the investigated solver CDCLSolver to always keep the clauses in $L$
in memory, while it is solving $\mathscr{F}\cup L$. This is interesting
because the clauses in $L$ were learned by the same solver on “its way to” a
solution. This can be thought of as providing the solver these clauses for
free by a _useful_ clause oracle.

  2. (b)

The investigated solver CDCLSolver starts by trying to solve the base instance
$\mathscr{F}$. During its execution, the solver learns the clauses of the core
pool $\mathbb{L}$. Let a reset of the solver be defined as an aggressive
clause deletion of part of the learned clauses in the database with a
simultaneous deletion of the current assignment. We model this reset as a
probabilistic process that takes place just before a solution is found, i. e.,
the solver deletes each of the learned clauses with probability $1-p$. The set
$\mathbb{L}$ could be thought of as being kept as a _frozen set_. Our model
studies the runtime distribution after this reset.

One should observe that our sampling process was designed so that all
extensions have comparable LBD properties. For example, the median LBD of an
extension is approximately the median LBD of the pool $\mathbb{L}$. The same
holds for various LBD quantiles. Thus, long runtimes on extended instances
cannot be explained by the fact that the set $L$ of the extended instance has
“poor” LBD properties. The same observation holds for the average size of the
learned clauses in the extensions. Long runtimes on extended instances are
thus not due to the fact that these extensions have a higher number of clauses
with more literals and are thus less likely to become unit and actually guide
the solver. Additionally, the sizes $|\mathscr{F}\cup L|$ follow a Gaussian
normal distribution for fixed $\mathscr{F}$. Even if a solver scales the size
of the learned clause database with the size of the original problem and thus
accumulates even more learned clauses, this observation is not enough to
explain the multimodality and long-tailed phenomenons observed.

We furthermore would like to mention that we did not increase the base
instance $\mathscr{F}$ by too many clauses: the median increase of
$|\mathscr{F}\cup L|$ when compared to $|\mathscr{F}|$ is just 3 %. This
increase cannot explain the enormous deteriorations that we have observed.

##### Limitations of our model.

One obvious criticism of the approach described above is that our model is not
a 100 % precise modeling of CDCL solvers as they are implemented in practice.
For example, our experimental setup cannot preserve variable activities
between the solving of $\mathscr{F}$ and $\mathscr{F}\cup L$. Our notion of a
reset also assumes that the reset takes place just before a solution is found.
In practice, a deletion of learned clauses is usually triggered much earlier.
However, to conduct a thorough statistical analysis of runtime distributions,
we had to make sure that the set $\mathbb{L}$ is large enough to sample at
least 1000 quite different extensions. Our approach also has the benefit of
studying the combined influence of learned clauses from far apart _batches_ (a
batch is the set of clauses learned between restarts666A restart of a CDCL
solver consists of deleting the current partial assignment while keeping the
set of learned clauses. This concept should not be confused with our notion of
a reset. of the solver). We believe that our approach lends itself to getting
a more _global_ understanding of the role of learned clauses.

While these are valid points, we nevertheless hope that our runtime
distribution study provides new insights into the role of clause deletion. The
aim of our model is not to completely understand all aspects of CDCL solvers
but to get a better understanding of one of them. At the current state of
research on CDCL solvers, clearly, all such models will have their drawbacks
and will not be able to represent all heuristics correctly. Further points
that could be investigated or improved upon in future research are noted in
Section 7.

###  3.2 The challenge of solving a myriad of hard formulas

Solving over $265\,000$ hard Boolean formulas in a reasonable time required
parallelization, for which we used Sputnik [42], and a somewhat more complex
experimental setup. We additionally distributed the formulas over two regular
servers (Luna, Erpel) and an HPC cluster (BwUniCluster 2.0). See Table 1 for
more details.777Note that due to such a diverse hardware setup, runtime
comparisons have to be done with caution. More details on this and other
metrics can be found in Section 4. During our experiments, we always
additionally considered time-independent theoretical measures.

After we initially started the experiments on just the Luna Server, we were
confronted with surprisingly long runtimes on certain extended formulas. The
corresponding original instances were solved after at most 95 minutes, but for
some extended formulas, it took Glucose 4.1 more than ten days to solve them.
This led us to

  1. (a)

distribute the calls of Algorithm 1 over multiple hardware nodes, and

  2. (b)

introduce a timeout strategy (censoring) as introduced in Section 2.2.2.

Only 12 out of all 53 instances encountered censoring in the Glucose 4.1
experiments, meaning that the solver reached the timeout limit for at least
one extended instance. In most cases, the solving of only a few extended
instances had to be stopped due to the timeout policy. More details on the
number of censored extended instances can be found in S2 Table.. Said
censoring timeouts $c_{j}$ were assigned to each extended formula
$\mathscr{F}_{j}$ according to an offset geometric distribution such that

$\displaystyle
c_{j}\sim\text{Geo}\left(\frac{1}{$12\text{\,}\mathrm{h}$}\right)+$5000\text{\,}\mathrm{s}$.$

We have chosen the value of $5000$ seconds since this is the cut-off in the
SAT Competition. The distribution
$\text{Geo}\left(\frac{1}{$12\text{\,}\mathrm{h}$}\right)$ has an expectation
of $12$ hours. This approach led to a total CPU time of $16$ years and $8$
month. All raw data obtained in this way can be found in S1 File..

Having used censoring in acquiring our data makes the use of survival
analysis, as elaborated in Section 2.2.2, necessary.

Table 1:  Summary of the hardware used in our experiments.

Name | Node |  CPU | Cores | Frequency | RAM
---|---|---|---|---|---
Erpel |  Intel Xeon E5-2698 v3 | 32 | 2.30 GHz | 256 GB
Luna |  AMD EPYC 7742 | 64 | 2.25 GHz | 256 GB
BwUniCluster 2.0 | HPC |  Intel Xeon Gold 6230 | 40 | 2.10 GHz | 96 GB
HPC Broadwell |  Intel Xeon E5-2660 v4 | 28 | 2.00 GHz | 128 GB

Table notes. Erpel and Luna are standard server architectures, whereas the
BwUniCluster 2.0 is a high-performance computing cluster.

##  4 Is clause learning useful on average?

Clearly, augmenting a basic DPLL solver with a clause learning mechanism is
far from a modern CDCL solver. However, clause learning is arguably the most
important technique in CDCL solvers, lending its name to the paradigm. One
would therefore expect that clause learning (especially when guided by state-
of-the-art heuristics) is generally useful, i. e., one would expect that
providing the solver with learned clauses for free does increase the
performance of the solver when compared to the base instance, where the solver
has to learn all clauses by itself (we use interpretation (a) of our model in
this section).

To check this assumption, we performed a parametric test of whether the mean
difference between the base instance and the 5000 (possibly censored) runtimes
on the extended instances solved with Glucose 4.1 equals 0. For this, we
assumed that the paired differences follow a Gaussian normal distribution. To
perform this test, we used the “NADA2: Data Analysis for Censored
Environmental Data” package [43] in R (we refer to the book [44] for an in-
depth treatment of the statistical methods involved). For the threshold value
in the statistical null-hypothesis tests, we used the standard value $p=0.05$.

In this section, we—quite surprisingly—demonstrate that clause learning is
oftentimes useful, but there are also _many_ instances where a dramatic
negative effect can be observed. We speak of a _negative effect_ if the mean
of the runtimes required to solve the extended instances was statistically
significantly greater ($p=0.05$) than the runtime required to solve the base
instance. We refer to Table 2 for an overview of the different effects.
Interestingly, almost all instances can be very clearly categorized in the
table because the obtained $p$-values are remarkably low (the exceptions are
marked in the table).

Table 2:  The effect of learned clauses (without deletion) on the runtime of
Glucose 4.1.

| With censoring | Without censoring
---|---|---
Positive effect | 5 | 26 [$\ddagger$]
No significant effect | 0 |  11 [$\dagger$]
Negative effect | 7 | 14 [$\ddagger$]

Table notes. We say that clause learning has a _positive effect_ if the mean
of the runtimes required to solve the extended instances was statistically
significantly smaller ($p=0.05$) than the runtime required to solve the base
instance. If the mean is statistically significantly greater than the runtime
for the base instance, we speak of a _negative effect_. Otherwise, it has _no
significant effect_. The base instances are grouped in the table based on
whether there was at least one extended instance of this base instance where
censoring occurred (_with censoring_) or not (_without censoring_).
$\vartriangleright$ [$\dagger$] The observed $p$-value was $p=0.53$ for the
unsatisfiable instance ncc_none_5047_6_3_3_0_0_41_p0.01 (see S2 Table. for the
complete list of $p$-values). The observed effect was negative.
$\vartriangleright$ [$\ddagger$] Furthermore, the non-censored instances with
negative effects include an instance (namely 6g_5color_164_100_01) with
$p=0.039$. This $p$-value is noteworthy since all other $p$-values are smaller
than $2.657\cdot 10^{-4}$ (again, see S2 Table.).

It is worth mentioning that in [45], a fundamental difference in the way
modern CDCL solvers solve satisfiable and unsatisfiable instances was
reported. There is still no consensus in the community regarding the role
learned clauses play in obtaining a satisfying assignment. However, most agree
that the role of learned clauses is more pronounced when the solver is
constructing a proof of unsatisfiability. By analyzing the effect of learned
clauses with respect to the satisfiability of the formula, we found that in 63
% of the cases, the effect was negative for satisfiable instances and in 27 %
for unsatisfiable instances (see Table 3).

Table 3:  The effect of learned clauses (without deletion) on the runtime of
Glucose 4.1 with respect to the satisfiability of the base instance.

| Satisfiable | Unsatisfiable
---|---|---
Positive effect |  17 [$\ddagger$] | 24 [$\dagger$]
No significant effect |  10 [$\ddagger$] |  21 [$\dagger$]
Negative effect | 12 [$\ddagger$] |  29 [$\dagger$]

Table notes. See Table 2 for an explanation of the rows. The dagger-symbols
have the same meaning as in Table 2.

We want to emphasize that there are also quite a few instances where adding
the set $L$ yields a deterioration in the number of conflicts occurring during
a run of the solver. In more than 11% of the cases, an adverse effect was
observed, which cannot be explained by pure chance and is quite surprising. We
refer to Table 4 for an analysis of the effect of learned clauses concerning
the number of conflicts. We chose to study this additional measure due to the
heterogeneous server architecture outlined in Table 1: The runtimes differ
very slightly between the server; however, the number of conflicts needed to
solve an instance is a robust, hardware-independent measure.

Table 4:  The effect of learned clauses (without deletion) on the number of
conflicts used by Glucose 4.1.

| With censoring | Without censoring
---|---|---
Positive effect | 8 | 37
No significant effect | 0 |  30
Negative effect | 2 |  34

Table notes. See Table 2 for an explanation of the rows and columns (replace
_runtime_ by _number of conflicts_). $\vartriangleright$ Out of the six
instances with a negative effect, two were unsatisfiable, and four were
satisfiable. $\vartriangleright$ Two of the 53 instances (both with censoring)
had to be excluded from the tests due to numerical complications in the
censored data paired $t$-test (NADA2 package).

For a comparison of runtime vs. number of conflicts, we refer to Table 5. We
want to point out that in each case where an opposite effect for time and
number of conflicts can be observed, the effect was negative for time and
positive for the number of conflicts. As mentioned in Section 1.2, this might
be explainable by the observation of Mitchell [18]: the required time to
perform unit propagation becomes too high for very large clause sets, which
reduces the performance of the solver. If an extended instance already
contains more clauses than the base instance, the propagation speed when
solving the extended instance is lower. Furthermore, many solvers scale the
size of the learned clause database with the size of the original problem,
leading to the solver to learn even more clauses, which causes the propagation
speed to lower again.

Table 5:  Comparison between the effect of adding clauses (without deletion)
for time and number of conflicts of Glucose 4.1.

| With censoring | Without censoring
---|---|---
Same effect for time and number of conflicts | 7 | 30
Opposite effect | 3 | 10

Table notes. We excluded one instance where, for at least one measure, our
experiments could not determine if there was a positive or negative effect for
that measure.

In both cases, i. e., regardless of whether one considers the runtime or the
number of conflicts, the observed performance deterioration cannot be
explained by pure chance. This is all the more surprising since the set of
learned clauses $L$ is not just any random set of clauses but clauses that the
same solver learned on “its way to” a solution. These clauses should thus
contain very useful information for the solver when it is solving the same
formula from scratch but with this additional information. Therefore, one
would expect that each and any of such a clause would benefit the guidance of
CDCL towards a solution.

To explain this deterioration phenomenon, one should therefore consider the
influence of clause _deletion_. Our experimental setup can be interpreted as
switching off clause deletion for the set of added clauses $L$ (while keeping
all other heuristics and optimizations of the solver) and learning all those
clauses at once. Note that the solver learns some additional clauses during
its run and can delete them. The set $L$, however, is fixed during the run.
Seemingly, clause deletion at the right points in time is as crucial as clause
learning. This statement cannot be fully explained by a blow-up in the size of
the clause database, as the unit-propagation-independent measure of the number
of conflicts also increased in many cases.

##  5 Multimodal behaviors in CDCL solvers

In Section 4, our focus was to compare the behavior of Glucose 4.1 on the
unmodified base instance to the behavior on the modified instances that
extended this base instance. From now on, we focus on studying the
distributions of the modified instances with respect to different measures
(see interpretation (b) of our model).

Our precise aim in this section is to get an understanding of the modality of
the ensuing CPU time distributions. Recall that in statistics, a probability
distribution with a single peak is called _unimodal_ ; otherwise, we speak of
a _multimodal_ distribution (a more formal definition can be found in [46]).
An easy way to inspect the modality of a distribution is to inspect the
histogram of the distribution visually. This method has the additional
advantage that no statistical test has to be used that can distinguish between
unimodal and bimodal distributions but rely on the knowledge of the underlying
distribution type (i. e., one does not need to know in advance if the
distribution can be resolved into, e. g.,  _normal_ distributions [47]).

Since our obtained data points are censored, we cannot immediately plot the
histogram. To overcome this obstacle, we have used the Kaplan–Meier estimator
(see Definition 2.6) implemented in the Survival package [48] in R to obtain a
fit of the underlying survival function. The Kaplan–Meier fit can be computed
without prior knowledge of the underlying distribution. Graphically, the
Kaplan–Meier survival curve is a step function with a drop each time the
solver has finished an instance. The points where a drop can be observed can
thus be used as an estimation basis to create the histogram. Note that in the
improbable event that two instances take precisely the same time to be solved
(while solving times are often very large), the resulting histogram
underestimates the number of instances in the corresponding bin. However, this
kind of event occurs so seldom that, for all intents and purposes, we can be
satisfied with the obtained estimation of the actual histogram.

For a more detailed investigation of multimodal behavior, we have used
Hartigans’ dip test statistic [46]. This test determines the amount of
multimodality by “the maximum difference, over all sample points, between the
empirical distribution function, and the unimodal distribution function that
minimizes that maximum difference”.888More formally, let
$\rho(F,\mathscr{A}):=\inf_{G\in\mathscr{A}}\|F-G\|_{\infty}$ for any function
space $\mathscr{A}$ of bounded functions. The _dip_ of a cdf $F$ is given by
$D(F):=\rho(F,\mathscr{U})$, where $\mathscr{U}$ is the class of unimodal
distribution functions [46]. Phrased differently, the dip of a distributions
function measures departure from unimodality. We have used a threshold dip
value of $0.005$ to classify multimodal histograms: All histograms with a dip
value over $0.005$ can clearly be seen to exhibit multimodal behavior, using
only visual inspection. We want to emphasize that this cut-off value is rather
strict (see e. g., Fig 4 (b) which is clearly multimodal but below the
threshold value).

We have printed the resulting estimated histogram using Kaplan–Meier of a
representative instance in Fig 2. As can be clearly seen, the distribution is
multimodal, as witnessed by the two peaks. The Hartigans’ dip test value also
confirms this.

Fig 2: Multimodal histogram of runtime distribution. We used the Kaplan–Meier
estimate to obtain the histogram of the runtime distribution of the instance
UNSAT_ME_seq-sat_Thoughtful_p11_6_59-typed.pddl_43. We used the
_Expectation–maximization_ (EM) method to obtain the pdf of the fitted Weibull
mixture model (see Definitions 6.1 and 6.2 for an introduction to this kind of
distribution). The EM algorithm is an algorithm that allows cluster analysis
by starting with a heuristically initialized model and alternating between two
steps. First, in the expectation-step (_E-step_), the association of the data
points to the different clusters gets changed. Then, in the maximization-step
(_M-step_), the model’s parameters get improved by using this new association
of the data points. We refer to the classic paper [49] for an introduction to
the algorithm. The resulting fitted distribution that is seen in the plot is
clearly multimodal. This is supported by a Hartigans’ dip test value of
$0.015>0.005$.

To facilitate our inspection of the histograms, we also investigated the
histograms for the logarithmically scaled runtimes. This method has been found
to usually give a clear separation into a visible multimodal histogram if the
underlying distribution is indeed multimodal (see e. g. [50, 51] for the
earliest applications of this technique). In Fig 3 we have shown an instance
where the multimodality cannot be seen in the histogram at first glance but
can clearly be made out in the histogram with logarithmically scaled runtimes.
Using this technique, we found that a significant fraction of 25 % of the
instances exhibited dominant multimodal behavior.

Fig 3: Histogram of runtimes vs. histogram of logarithmically scaled runtimes.
Scaling the $x$-axis of a histogram logarithmically can often uncover
multimodality that is not clearly visible in the unscaled histogram. The
graphic depicts both histograms for the instance size_5_5_5_i019_r12, where
this difference is very pronounced. (above) Histogram of CPU times with a
Hartigans’ dip test value of 0.005. (below) Histogram of logarithmically
scaled CPU times with a Hartigans’ dip test value of 0.016.

Due to the heterogeneous server architecture, we also studied the histograms
for hardware-independent measures, like the number of propagations and
decisions needed to come to a solution. Again, we could observe the
multimodality phenomenon for these measures. We refer to Fig 4 as a
continuation of the histogram shown in Fig 2.

Fig 4: Multimodal histogram of the distribution for the number of propagations
and decisions. The histograms show the distribution of the two measures
propagations and decisions required to solve the extended instances of
UNSAT_ME_seq-sat_Thoughtful_p11_6_59-typed.pddl_43. Both histograms for the
hardware-independent measures have the same multimodal form as the histogram
for CPU time shown in Fig 2. (above) Histogram for number of propagations with
a Hartigans’ dip test value of 0.005. (below) Histogram for number of
decisions with a Hartigans’ dip test value of 0.004.

Using the threshold value of 0.005 for Hartigans’ dip test, 32 % of all
instances exhibit multimodal behavior for at least one measure (CPU time,
logarithmized CPU time, propagations, or decisions).

This multimodal grouping of instances into several categories could be helpful
in an investigation of the usefulness of the added clauses. We make this
thought more precise in the next section and investigate the distribution type
underlying the model.

##  6 Finding the right mixture distribution type

In Section 5, we have already seen that the runtime behavior is multimodal for
a substantial part of the instances. This section aims to study which types of
distributions are suitable to describe this behavior. Since most well-known
distributions, such as the normal distribution, are unimodal or at most
bimodal, this suggests that one must resort to another type of distribution.

The presence of the many peaks indicates that the different extended instances
(and underlying clauses) can be divided into categories. Each category
corresponds to the hardness of the extended instance, where the hardness is
again not a fixed value but a random variable. If one confines oneself to a
single category of extended instances, one is (potentially) no longer
confronted with multimodal behavior but can describe the remaining data
utilizing a unimodal distribution.

By (randomly) adding the clauses to $L$, we then end up in this category of
extended instances with a certain probability. If such an analysis is
conducted for each category, we eventually obtain a description of the
complete runtime behavior. Specifically, this means that for each category,
the underlying runtime distribution, as well as the probability of ending up
in that category, must be identified. The runtime behavior across all extended
instances is then characterized by a so-called finite mixture distribution.

######  Definition 6.1.

Let $X$ be a random variable having the cdf $F_{X}$. Let
$F_{1},F_{2},\dots,F_{N}$ be cdfs and $p_{1},p_{2},\dots,p_{N}$ be weights
with $p_{i}>0$ for all $i\in\\{1,\dots,N\\}$ and $\sum_{i=1}^{N}p_{i}=1$. If

$\displaystyle F_{X}(x)=\sum_{i=1}^{N}p_{i}\cdot F_{i}(x)$

holds for all $x\in\mathbb{R}$, then $X$ has an _$N$ -component (finite)
mixture distribution_.

Fig 5: Mixture distribution and components. The figure shows the Weibull
components (in black) underlying the mixture distribution (in red) of instance
UNSAT_ME_seq-sat_Thoughtful_p11_6_59-typed.pddl_43. The Weibull components
were scaled according to their respective $p_{i}$-values. For the histogram of
this instance, refer to Fig 2.

In our case, $N$ can be understood as the number of categories. Furthermore,
$p_{i}$ describes the probability of ending up in category $i$, in which case
$F_{i}$ is the runtime distribution for category $i$. We refer to Fig 5 of a
depiction of the components underlying a mixture distribution.

In principle, one can choose arbitrary cdfs $F_{1}$ to $F_{N}$. However, it is
common practice to choose the cdfs from the same family of (parametric)
distributions, where only the parameters of the distribution differ. For
example, a popular model are Gaussian mixture distributions in which the cdfs
describe normal distributions varying with respect to their expected value and
variance. Therefore, the question arises of which parametric distribution type
should be chosen for the mixture distribution. We shall argue that a
distribution based on the so-called Weibull distribution is an appropriate
type of distribution.

######  Definition 6.2 ([52]).

A random variable $X$ with a pdf given by

$\displaystyle
f_{X}(x)=\begin{cases}\frac{k}{a}\cdot\left(\frac{x-\ell}{a}\right)^{k-1}\cdot\mathrm{e}^{-\left(\frac{x-\ell}{a}\right)^{k}},&x\geq
0\\\ 0,&x<0\end{cases}$

is _3-parameter Weibull distributed_ with parameters $k\in\mathbb{R}^{+}$
(_shape_), $a\in\mathbb{R}^{+}$ (_scale_), and $\ell\in\mathbb{R}$
(_location_). The cdf of $X$ is given by

$\displaystyle
F_{X}(x)=\begin{cases}1-\mathrm{e}^{-\left(\frac{x-\ell}{a}\right)^{k}},&x\geq
0\\\ 0,&x<0.\end{cases}$

If the location parameter $\ell$ is zero, we call the distribution
_2-parameter Weibull distributed_ or just _Weibull distributed_.

We first start by analyzing instances that can be described with only one
component (i. e., a 1-component mixture distribution). The idea behind this is
that one can derive information about the instances that require more than one
component. A suitable graphical tool for this analysis is provided by Q–Q
plots, where the observed quantiles are plotted against the theoretical
quantiles of a given distribution (recall Section 2.2.1). In the following, we
consider the required CPU time until the respective instance is solved, i. e.,
either a satisfying assignment is constructed, or a proof of unsatisfiability
is established.

Fig 6: Q–Q plot. The Q–Q plot for instance crafted_n11_d6_c4_num19 was
obtained by the quantiles of a fitted 3-parameter Weibull distribution and the
data quantiles. The plot appears as a straight line. The correlation
coefficient calculates to 0.9997979. For reference, the identity is given in
gray.

As an example, we consider the data from one instance in Fig 6. We use a
fitted 3-parameter Weibull distribution as the theoretical distribution. As
can be seen in the figure, the Q–Q plot yields a straight line, indicating
that the theoretical distribution can describe the empirical data very well.
So we can conclude that a 3-parameter Weibull distribution is a suitable
description for this instance. This is not only the case in this example. For
example, one can use the correlation coefficient to measure how linear a
certain relationship is. A correlation coefficient of 0.999 describes an
extremely strong linear relationship. We used this value and examined all Q–Q
plots. In total, 12 instances reach a correlation coefficient of at least
0.999 if a fitted 3-parameter Weibull distribution is used as theoretical
distribution. This suggests that a substantial number of instances can be
described by a _single_ Weibull distribution. It should also be emphasized
that other typical distribution types, such as the normal or lognormal
distribution, do not provide good fits. While Weibull distributions describe a
considerable fraction of the instances, this begs the question of what to do
with the remaining instances.

First, it should be emphasized that especially the instances where
multimodality is strong cannot be described by a single Weibull distribution.
Then, however, it is natural to assume that the individual components of a
mixture distribution follow Weibull distributions. We pursue this line of
thought in more detail in the following.

Graphical analyses are well suited to argue that Weibull distributions are
appropriate. First, we examine how the Weibull distribution behaves at the
left tail, i. e., the behavior if $x$ approaches $0$. It is well known that
Weibull distributions have a linear appearance on a $\log$–$\log$ plot of the
cdf at the left tail. To see this, we investigate the logarithm of the Weibull
cdf $F$ with location parameter $\ell=0$ for $x\geq 0$:

$\displaystyle\log
F(x)=\log\left(1-\mathrm{e}^{-\left(\frac{x}{a}\right)^{k}}\right).$

Plugging the Taylor expansion of $\exp(-x)$ into this equation yields:

$\displaystyle\log F(x)$
$\displaystyle=\log\left(1-\left[1-\left(\frac{x}{a}\right)^{k}+\frac{(\frac{x}{a})^{2k}}{2!}-\dots\right]\right)$
$\displaystyle=\log\left(\left(\frac{x}{a}\right)^{k}-\frac{\left(\frac{x}{a}\right)^{2k}}{2!}+\dots\right).$

Considering the behavior as $x$ approaches $0$, we notice that the trailing
terms approach $0$ much faster than $(x/a)^{k}$ and thus can be neglected.
Hence, we obtain:

$\displaystyle\log
F(x)\approx\log\left(\left(\frac{x}{a}\right)^{k}\right)=k\cdot\log
x-k\cdot\log a\quad\text{for }x\to 0.$

By substituting $z=\log x$, one finds that the cdf $F$ indeed appears linearly
in the neighborhood of zero on a $\log$–$\log$ plot.

For mixture distributions, this method is useful for making statements about
the smallest component. Suppose that $F(x)=\sum_{i}^{N}p_{i}F_{i}(x)$ is the
cdf of a mixture distribution. Here, $F_{1}$ is the cdf of a Weibull
distribution, and for small $x$, we have $F_{1}(x)\gg 0$ and $F_{2}(x)\approx
F_{3}(x)\approx\dots\approx F_{N}(x)\approx 0$. Thus, $F(x)\approx
p_{1}F_{1}(x)$ is also valid; moreover, due to the reasoning above, the cdf
$F$ appears linearly on a $\log$–$\log$ plot in the neighborhood of zero.
Conversely, one can argue that $\log$–$\log$ plots of the cdf are suitable for
evaluating whether the smallest cdf can be characterized by a Weibull
distribution.

Another popular method of analyzing Weibull distributions is to examine the
survival function $S(x)=1-F(x)$. In particular, the survival function
transformed as follows is used:

$\displaystyle\log\big{(}-\log S(x)\big{)}$
$\displaystyle=\log\left(-\log\mathrm{e}^{-\left(\frac{x}{a}\right)^{k}}\right)$
$\displaystyle=\log\left(\left(\frac{x}{a}\right)^{k}\right)=k\cdot\log
x-k\cdot\log a.$

In other words, a Weibull distribution appears linear if the survival function
is double logarithmized in this manner and the $x$-axis is singly
logarithmized. We can apply this graphical tool to determine whether the
largest component in a mixture distribution can be described by a Weibull
distribution.

Again, suppose that $F(x)=\sum_{i}^{N}p_{i}F_{i}(x)$ is the cdf of a mixture
distribution. Here, $F_{N}$ is the cdf of a Weibull distribution, and for
large $x$, we have $F_{N}(x)\ll 1$ and $F_{1}(x)\approx
F_{2}(x)\approx\dots\approx F_{N-1}(x)\approx 1$. Thus, we have

$\displaystyle S(x)=1-F(x)=1-\sum_{i=1}^{N}p_{i}F_{i}(x)$
$\displaystyle\approx
1-\underbrace{\sum_{i=1}^{N-1}p_{i}}_{=1-p_{N}}-p_{N}F_{N}(x)$
$\displaystyle=p_{N}-p_{N}F_{N}(x)=p_{N}\big{(}1-F_{N}(x)\big{)}.$

By the above argument, the doubly logarithmized survival function $S$ and
singly logarithmized $x$-axis will appear approximately linear for large $x$.
Conversely, such a plot can also be used to deduce whether the largest
component can be described by a Weibull distribution.

These two plot types are therefore suitable for finding out whether the
extreme values, i. e., particularly short and particularly long runs, are
described by Weibull distributions, respectively. Thus, as before, we examine
the CPU times and investigate them with the help of these two plot types.

Fig 7: Inspection of the smallest and largest component of the Weibull mixture
model. Based on the Kaplan–Meier estimator, the estimations of the cdf and
survival function of the multimodal instance bivium-40-200 are shown
(Hartigans’ dip test value 0.010). Both the left and the right tails appear as
straight lines (depicted in red). The plot of the cdf is a $\log$–$\log$ plot,
while the plot of the survival function is a $\log\log$–$\log$ plot. The gray
area marks the confidence interval. This suggests that the smallest and
largest component of the underlying mixture model are Weibull distributions.
(left) Estimation of the cdf. (right) Estimation of the survival function.

In Fig 7, we exemplarily consider one instance. Note that both the left and
the right tails appear as straight lines. Using the reasoning presented above,
we can therefore infer that for both cases, a Weibull distribution is
appropriate to characterize the left and the right tail, respectively. On the
one hand, Weibull distributions describe both the left and the right tail and,
in some cases, the entire support. On the other hand, it is common practice to
use only one type of distribution for mixed distributions. Therefore, we argue
that the runtime distributions can be described by Weibull distributions.

One can derive some highly intriguing insights into the operation of CDCL
solvers from the knowledge that Weibull distributions describe the runtime
behavior of such solvers. First, if the shape parameter $k$ of the Weibull
distribution is less than 1, then the distribution has the so-called long-tail
property [53].999For $k=1$, the Weibull distribution reduces to an exponential
distribution which is _light-tailed_ (and thus not long-tailed). For $k>1$,
the Weibull distribution is also light-tailed [53].

Fig 8: Long-/Heavy-Tails. This figure shows various plots of the unimodal
instance 6g_5color_164_100_01 (Hartigans’ dip test value 0.003). This is an
example of an instance with a long-tailed runtime distribution. (a) The plot
shows the histogram of runtimes (in gray) and the fitted pdf (in red). Both
are shifted to the left by the minimal time $T_{0}$ required to solve any
extended instance. The obtained shape parameter of the fit is
$k=$0.884\,654\,5$<1$. Thus, the distribution is long-tailed. (b) We have
plotted the logarithm of the tail of the distribution, i. e., $\log S(x)$. By
visual inspection, one can see that it decays sub-linearly. In this case,
$\liminf_{x\to\infty}-{\log\operatorname{\mathbb{P}}\left[X>x\right]}/{x}=0$.
This property characterizes the class of so-called _heavy-tailed_
distributions (a superset of the class of long-tailed distributions) [53].
Intuitively, this means that the algorithm has a non-vanishing probability of
requiring very long runtimes. For comparison, we have plotted the logarithmic
survival function of an exponentially distributed random variable with the
same expectation in blue. The logarithm of the tail of such an exponential
distribution decays linearly. (c) Zoomed in version of (b). This clearly shows
the sublinear decay by focusing on the curvature.

Roughly speaking, this property indicates that the algorithm either finishes
(relatively) quickly or takes exceedingly long.101010 Long-tails are not
equivalent to heavy-tails or powerlaws. Following [54] and [53], we say that a
positive, real-valued random variable $X$ is _long-tailed_ , if and only if
for all $x\in\mathbb{R}^{+}$ it holds
$\operatorname{\mathbb{P}}\left[X>x\right]>0$, and for all
$y\in\mathbb{R}^{+}$ it holds
$\lim_{x\rightarrow\infty}\operatorname{\mathbb{P}}\left[X>x+y\right]/\operatorname{\mathbb{P}}\left[X>x\right]=1$.
For an illustration of a long-tailed runtime distribution and a further
elaboration on the subject of the long-tailed property, refer to Fig 8. See
also Fig 3 (a) for another depiction of a long-tailed distribution.

We have also conducted experiments with Glucose 4.1 using the deletion
strategy of Chanseok Oh. Again, there are long-tails present. The same holds
for experiments conducted with the MiniSAT solver (where the mean runtimes
worsened significantly when compared to Glucose 4.1). We refer to Fig 9.

Fig 9: Multimodal and long-tailed effect with MiniSAT. The histogram shows the
distributions of CPU times when solving the extended instances of
6g_5color_164_100_01 with MiniSAT. Both a multimodal behavior as well as a
long-tailed effect are visible. The multimodality is confirmed by a Hartigans’
dip test value of $0.031$.

What is remarkable about this is that algorithmic restarts have been proven to
be useful for long-tailed distributions [10, 55]. This means that the
algorithm can be accelerated by reinitializing it from scratch. In our
context, such a reset111111We again would like to point out that such a reset
is not the same as a restart in a CDCL solver. of the solver consists of
discarding all added clauses $L$ that were added to the original base instance
$\mathscr{F}$. Instead, a new set of clauses $L^{\prime}$ is sampled from the
base set of frozen clauses $\mathbb{L}$ that is then added to the original
instance $\mathscr{F}$. Of course, the search tree is also reset to the top
level at the same time.

Therefore, the observation that Weibull distributions describe the runtime
behavior implies that aggressive clause deletions (in the form of complete
database flushes) together with forgetting the partial assignment are useful
in the context of CDCL solvers, i. e., they improve the runtime. However, what
is remarkable about this is not the mere observation that these two techniques
improve the runtime because this fact has already been shown empirically (see
e. g. [2, 56, 9, 57]). It is more interesting that we are reaching a
conclusion as to why these techniques have a positive effect on the
performance. Adding new clauses to the base instance has the inherent effect
of making runtimes long-tailed. While the added clauses usually improve the
performance, there is a non-negligible chance that the performance
deteriorates (sometimes drastically). The easiest way to circumvent this
problem is to delete the learned clauses and reset the search tree
periodically.

It is also worth repeating the observations on Table 4. Here, the effect of
adding clauses is measured by the number of conflicts. This table tells us
that, contrary to common belief [18], the degraded performance is not only due
to the increase in the size of the base instance $\mathscr{F}$ and thus due to
a more considerable overhead for each propagation. Instead, it implies that
some clauses lead the CDCL algorithm itself astray, i. e., to a path in the
search tree that does not yield a solution.

Since clause deletions and forgetting partial assignments are useful because
Weibull distributions describe the runtimes, this shifts the question to why
adding clauses causes Weibull distributions. A possible starting point is
provided by the Fisher–Tippett–Gnedenko theorem [58, 59, 60, 61]. Roughly
speaking, this theorem states that the minima and maxima of independent and
identically distributed random variables converge to one of three distribution
types (under the condition that they converge at all). The Weibull
distribution is one of these three distribution types. This suggests that the
reason for the observed runtimes may be a minimum or maximum process. For
example, the runtimes could be significantly influenced by the quality of the
“best” or “worst” clause, where by the quality of the clause, we mean the
extent to which the clause guides the heuristics of the CDCL algorithm towards
a solution. However, this is only a hypothesis that should be further
investigated in other future research.

##  7 Conclusion and further research

We have modeled the technique of clause learning in CDCL solvers by solving
new logically equivalent formulas of a base instance. This allowed us to
analyze the resulting runtime distribution.

We have provided compelling evidence that this distribution is a Weibull
mixture model, completing the runtime distribution study [10] for both
paradigms of SAT solvers. In addition, the Weibull fit was suitable for both
multimodal and unimodal instances. Because the underlying distribution is
Weibull, adding new clauses thus has an inherent effect of making runtimes
long-tailed in both SLS and CDCL solvers. The long-tailed runtime distribution
in CDCL solvers yields additional motivation to improve on existing clause
deletion schemes. These are not only needed to speed up unit propagation steps
but are indispensable tools to avoid getting stuck in the tail of the
distribution and ultimately avoid excessively long solving times.
Additionally, the long-tailed property theoretically explains why completely
flushing the learned clause database and forgetting the partial assignment
(so-called resetting) is useful for CDCL algorithms.

We furthermore provided a hypothesis for the suitability of the Weibull
distribution by invoking the Fisher–Tippett–Gnedenko theorem. It seems
reasonable that runtimes are heavily influenced by the quality of the “best”
and “worst” clauses. An analysis of these clause qualities, especially in the
context of LBD [9], seems like a fruitful pursuit for further research.

A refined approach in future research could also investigate the influence of
different batches of learned clauses on the runtime (e. g., are clauses
learned later always more helpful than clauses learned earlier “towards the
way of” a solution?). It might also be interesting to examine the quality of
clauses from trimmed proofs with the approach shown in this paper. Since
Glucose 4.1 has a feature to dynamically adapt its search strategy during a
run, a very interesting follow-up investigation could also consist of
classifying the clusters of extended instances by the search strategies used
by the solver.

## Supporting information

##### S1 File.

Generated data and evaluations. We have provided all data of this paper in the
repository [62] (doi:10.5281/zenodo.6642166). This collection contains the
scripts for obtaining the sets $\mathbb{L}$ and reconstructing our sampled
sets $L$. Furthermore, all data obtained by calling
$\texttt{CDCLSolver}(\mathscr{F}\cup L)$ can be found, where
$\texttt{CDCLSolver}{}\in\big{\\{}\texttt{Glucose}\leavevmode\nobreak\
\texttt{4.1}{},\>\texttt{Glucose}\leavevmode\nobreak\
\texttt{4.1}{}\texttt{\,+\,ChanseokOh},\>\texttt{MiniSAT}{}\big{\\}}$.
Additionally, we included visual and statistical evaluations used in this
paper.

##### S2 Table.

Instance pool. This supporting table describes the instances used for our
experiments with Glucose 4.1. The instance
bivium-40-200-0s0-0x92fc13b11169afbb2ef11a684d9fe9a19e743cd6aa5ce23fb5-19 was
abbreviated by bivium-40-200 in the table. The column _SAT/UNSAT_ indicates
whether the instance is satisfiable (SAT) or unsatisfiable (UNSAT). Note that
extending an instance with a set $L\subseteq\mathbb{L}$ preserves the
satisfiability of the instance. The column _cen_ denotes the number of
censored data points of each instance during the Glucose 4.1 trials, i. e.,
$\sum_{j=1}^{5000}\mathrm{cen}_{j}$, where $\mathrm{cen}_{j}$ is the censoring
indicator introduced in Equation (2). The columns $Z_{\text{time}}$ and
$p_{\text{time}}$ report the results of the $t$-test for CPU time as described
in Section 4. Similarly, the columns $Z_{\text{confl}}$ and $p_{\text{confl}}$
report the results of the $t$-test for the number of conflicts as described in
Section 4. In both cases, a negative value of the test statistic $Z$ signifies
a positive effect for the mean of the extended instances. All values were
rounded to two places. The values “—” in the table denote the two instances
where complications in the $t$-test for the censored number of conflict data
occurred. The table itself can be found on the following pages in landscape
mode.

instance | SAT/UNSAT | cen | $Z_{\text{time}}$ | $p_{\text{time}}$ | $Z_{\text{confl}}$ | $p_{\text{confl}}$
---|---|---|---|---|---|---
instance | SAT/UNSAT | cen | $Z_{\text{time}}$ | $p_{\text{time}}$ | $Z_{\text{confl}}$ | $p_{\text{confl}}$
3bitadd_32.cnf.gz.CP3-cnfmiter | UNSAT | 8 | $-118.792$ | 0 | $-271.1447$ | 0
59-129706 | SAT | 1 | $-253.6202$ | 0 | $-321.228$ | 0
6g_5color_164_100_01 | SAT | 0 | $2.0645$ | $0.038\,97$ | $-50.0449$ | 0
abw-K-dwt__234.mtx-w55 | UNSAT | 0 | $-6167.8143$ | 0 | $-4888.9771$ | 0
bivium-40-200 | UNSAT | 0 | $-10\,026.9726$ | 0 | $-178\,525.3584$ | 0
crafted_n11_d6_c4_num19 | UNSAT | 0 | $-1247.165$ | 0 | $-2295.2396$ | 0
cz-alt-3-7 | UNSAT | 0 | $-3480.316$ | 0 | $-5057.1774$ | 0
DLTM_twitter249_74_10 | UNSAT | 0 | $-3526.2268$ | 0 | $-3923.3739$ | 0
DLTM_twitter799_70_13 | SAT | 0 | $43.731$ | 0 | $17.598$ | $2.553\text{\cdot}{10}^{-69}$
Kakuro-easy-117-ext.xml.hg_5 | SAT | 0 | $-93.8529$ | 0 | $-164.0922$ | 0
Kakuro-easy-125-ext.xml.hg_4 | UNSAT | 0 | $-395.6815$ | 0 | $-407.9576$ | 0
Kakuro-easy-132-ext.xml.hg_9 | SAT | 17 | $54.5121$ | 0 | $23.0849$ | $6.569\,999\,999\,999\,998\text{\cdot}{10}^{-118}$
Kakuro-easy-149-ext.xml.hg_4 | UNSAT | 0 | $-190.9724$ | 0 | $-383.805$ | 0
Kakuro-easy-154-ext.xml.hg_4 | UNSAT | 0 | $-313.4033$ | 0 | $-758.95$ | 0
LABS_n038_goal002 | UNSAT | 0 | $-8917.9104$ | 0 | $-18\,594.8845$ | 0
LABS_n071_goal001-sc2013 | UNSAT | 0 | $-915.2317$ | 0 | $-2133.7492$ | 0
logistics-unsat-logistics-rotate-11t5.sat05-1141.reshuffled-07 | UNSAT | 19 | $201.1461$ | 0 | $-51\,659.7118$ | 0
ls16-normalized.cnf.gz.CP3-cnfmiter | UNSAT | 134 | $-11.7643$ | $5.959\text{\cdot}{10}^{-32}$ | $-123.2689$ | 0
mm-2x3-8-8-sb.1.sat05-475.reshuffled-07 | UNSAT | 0 | $-6888.6225$ | 0 | $-14\,486.5844$ | 0
ncc_none_12477_5_3_3_0_0_435991723 | UNSAT | 2 | $220.0471$ | 0 | $-503.9177$ | 0
ncc_none_12477_5_3_3_1_0_435991723 | SAT | 0 | $70.0259$ | 0 | $-12.3312$ | $6.156\text{\cdot}{10}^{-35}$
ncc_none_2_18_9_3_0_0_435991723 | UNSAT | 0 | $-94.0668$ | 0 | $-303.3008$ | 0
ncc_none_3047_7_3_3_1_0_1 | SAT | 0 | $79.937$ | 0 | $20.152$ | $2.586\text{\cdot}{10}^{-90}$
ncc_none_5047_6_3_3_0_0_41 | UNSAT | 0 | $0.6349$ | $0.5255$ | $-38.2074$ | 0
ncc_none_5047_6_3_3_3_0_435991723 | SAT | 0 | $122.9951$ | 0 | $-19.457$ | $2.543\,999\,999\,999\,999\,4\text{\cdot}{10}^{-84}$
newpol34-4 | UNSAT | 8 | $-132.6987$ | 0 | $-229.2936$ | 0
preimage_80r_491m_160h_seed_407 | SAT | 0 | $8.1145$ | $4.877\text{\cdot}{10}^{-16}$ | $-104.5238$ | 0
preimage_80r_492m_160h_seed_136 | SAT | 0 | $-1513.8527$ | 0 | $-1562.7196$ | 0
preimage_80r_493m_160h_seed_249 | SAT | 0 | $-39.3012$ | 0 | $-172.7256$ | 0
problem_23.smt2 | UNSAT | 276 | $225.1704$ | 0 | $112.6824$ | 0
QG7a-gensys-ukn009.sat05-3849.reshuffled-07 | UNSAT | 0 | $-1200.6596$ | 0 | $-4072.5468$ | 0
SAT_ME_opt_snake_p15.pddl_25 | SAT | 0 | $-107.3781$ | 0 | $-73.324\,700\,000\,000\,007$ | 0
SAT_P_opt_snake_p02.pddl_32 | SAT | 0 | $56.7815$ | 0 | $3.7618$ | $1.687\text{\cdot}{10}^{-4}$
size_5_5_5_i019_r12 | SAT | 2403 | $36.9619$ | $4.697\,999\,999\,999\,998\text{\cdot}{10}^{-299}$ | — | —
sqrt_ineq_3.c | SAT | 53 | $65.7117$ | 0 | — | —
sted1_0x0_n438-636 | SAT | 0 | $-2212.6877$ | 0 | $-2600.0604$ | 0
sted2_0x0_n219-342 | SAT | 0 | $-402.6359$ | 0 | $-493.0695$ | 0
sted3_0x1e3-147 | SAT | 0 | $35.8734$ | $7.932\,999\,999\,999\,996\text{\cdot}{10}^{-282}$ | $-83.77$ | 0
sted5_0x0-157 | SAT | 0 | $20.9248$ | $3.185\,999\,999\,999\,999\,6\text{\cdot}{10}^{-97}$ | $-58.9789$ | 0
UNSAT_ME_seq-opt_Tidybot_p17.pddl_29 | UNSAT | 0 | $-56.3562$ | 0 | $-87.2381$ | 0
UNSAT_ME_seq-opt_Tidybot_p19.pddl_29 | UNSAT | 3 | $-191.0753$ | 0 | $-165.0739$ | 0
UNSAT_ME_seq-sat_Thoughtful_p11_6_53-typed.pddl_49 | UNSAT | 0 | $-66.2987$ | 0 | $-166.7853$ | 0
UNSAT_ME_seq-sat_Thoughtful_p11_6_59-typed.pddl_43 | UNSAT | 0 | $13.1279$ | $2.277\,999\,999\,999\,999\,8\text{\cdot}{10}^{-39}$ | $-77.3153$ | 0
UNSAT_ME_seq-sat_Thoughtful_p11_6_62-typed.pddl_47 | UNSAT | 0 | $-5.1463$ | $2.657\text{\cdot}{10}^{-7}$ | $-108.344$ | 0
UNSAT_MS_opt_snake_p06.pddl_30 | UNSAT | 0 | $48.986$ | 0 | $8.9487$ | $3.596\text{\cdot}{10}^{-19}$
UNSAT_MS_opt_termes_p04.pddl_79 | UNSAT | 5 | $133.1695$ | 0 | $-156.4602$ | 0
UNSAT_MS_opt_termes_p11.pddl_65 | UNSAT | 0 | $-50.2965$ | 0 | $-104.7226$ | 0
UNSAT_P_opt_snake_p02.pddl_31 | UNSAT | 0 | $18.2025$ | $4.925\,999\,999\,999\,999\text{\cdot}{10}^{-74}$ | $-149.7934$ | 0
UNSAT_P_sat_snake_p05.pddl_30 | UNSAT | 0 | $55.4446$ | 0 | $-78.7091$ | 0
UNSAT_P_seq-opt_Barman_p435.1.pddl_32 | UNSAT | 0 | $65.3064$ | 0 | $-99.0964$ | 0
UNSAT_P_seq-opt_Barman_p435.2.pddl_32 | UNSAT | 0 | $-31.9013$ | $2.559\,999\,999\,999\,998\,4\text{\cdot}{10}^{-223}$ | $-208.8378$ | 0
w15 | UNSAT | 0 | $-18\,343.1535$ | 0 | $-10\,427.5411$ | 0
w19-5.1 | UNSAT | 0 | $-9522.4478$ | 0 | $-8114.498$ | 0

## Acknowledgments and Funding

The authors acknowledge support by the state of Baden-Württemberg through
bwHPC. This research was supported by the Deutsche Forschungsgemeinschaft
(DFG) under project number 430150230, “Complexity measures for solving
propositional formulas”.

The authors also would like to express their gratitude to the anonymous
reviewers of the paper. Their suggestions immensely helped the presentation of
the paper and provided many interesting ideas for additional experiments that
were performed.

Furthermore, the authors would like to thank Mathias Fleury for helpful
discussions.

## References

  * 1. Marques-Silva JP, Sakallah KA.  GRASP: A Search Algorithm for Propositional Satisfiability.  IEEE Transactions on Computers. 1999;48(5):506–521.
  * 2. Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S.  Chaff: Engineering an Efficient SAT Solver.  In: Proceedings of the 38th Design Automation Conference (DAC ’01). ACM; 2001. p. 530–535.
  * 3. Marques-Silva JP, Lynce I, Malik S.  Conflict-Driven Clause Learning SAT Solvers.  In: Biere A, Heule MJH, van Maaren H, Walsh T, editors. Handbook of Satisfiability. vol. 336 of Frontiers in Artificial Intelligence and Applications. 2nd ed. IOS Press; 2021. p. 133–182.
  * 4. Heule MJH, Kullmann O, Marek VW.  Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer.  In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT ’16). vol. 9710 of Lecture Notes in Computer Science. Springer; 2016. p. 228–245.
  * 5. Heule MJH.  Schur Number Five.  In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI ’18), the 30th Innovative Applications of Artificial Intelligence (IAAI ’18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI ’18). AAAI Press; 2018. p. 6598–6606.
  * 6. Brakensiek J, Heule MJH, Mackey J, Narváez DE.  The Resolution of Keller’s Conjecture.  In: Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR ’20). vol. 12166 of Lecture Notes in Computer Science. Springer; 2020. p. 48–65.
  * 7. Franco J, Martin J.  A History of Satisfiability.  In: Handbook of Satisfiability. vol. 336 of Frontiers in Artificial Intelligence and Applications. 2nd ed. IOS Press; 2021. p. 3–74.
  * 8. Audemard G, Simon L. The Glucose SAT Solver; 2014.  https://www.labri.fr/perso/lsimon/glucose/.
  * 9. Audemard G, Simon L.  Predicting Learnt Clauses Quality in Modern SAT Solvers.  In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI ’09); 2009. p. 399–404.
  * 10. Wörz F, Lorenz JH.  Evidence for Long-Tails in SLS Algorithms.  In: Proceedings of the 29th Annual European Symposium on Algorithms (ESA ’21). vol. 204 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik; 2021. p. 82:1–82:16.
  * 11. Eén N, Sörensson N.  An Extensible SAT-solver.  In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT ’03). vol. 2919 of Lecture Notes in Computer Science. Springer; 2003. p. 502–518.
  * 12. Frost D, Rish I, Vila L.  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); 1997. p. 327–333.
  * 13. Rish I, Frost D.  Statistical Analysis of Backtracking on Inconsistent CSPs.  In: Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP ’97); 1997. p. 150–162.
  * 14. Gomes CP, Selman B, Crato N, Kautz HA.  Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems.  Journal of Automated Reasoning. 2000;24(1/2):67–100.
  * 15. Lorenz JH, Wörz F.  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). vol. 12178 of Lecture Notes in Computer Science. Springer; 2020. p. 89–106.
  * 16. Arbelaez A, Truchet C, Codognet P.  Using sequential runtime distributions for the parallel speedup prediction of SAT local search.  Theory and Practice of Logic Programming. 2013;13(4-5):625–639.
  * 17. Barrero DF, Muñoz P, Camacho D, Rodríguez-Moreno MD.  On the statistical distribution of the expected run-time in population-based search algorithms.  Soft Computing. 2015;19(10):2717–2734.
  * 18. Mitchell DG.  A SAT Solver Primer.  Bulletin of the EATCS. 2005;85:112–132.
  * 19. Audemard G, Lagniez J, Mazure B, Sais L.  On Freezing and Reactivating Learnt Clauses.  In: Proceeedings of the 14th Internation Conference on Theory and Applications of Satisfiability Testing (SAT ’11); 2011. p. 188–200.
  * 20. Kokkala JI, Nordström J.  Using Resolution Proofs to Analyse CDCL Solvers.  In: Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP ’20). vol. 12333 of Lecture Notes in Computer Science. Springer; 2020. p. 427–444.
  * 21. Beame P, Kautz HA, Sabharwal A.  Towards Understanding and Harnessing the Potential of Clause Learning.  Journal of Artificial Intelligence Research. 2004;22:319–351.
  * 22. Hertel P, Bacchus F, Pitassi T, Gelder AV.  Clause Learning Can Effectively P-Simulate General Propositional Resolution.  In: Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI ’08); 2008. p. 283–290.
  * 23. Buss SR, Hoffmann J, Johannsen J.  Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning.  Logical Methods in Computer Science. 2008;4(4):1–28.
  * 24. Pipatsrisawat K, Darwiche A.  On the power of clause-learning SAT solvers as resolution engines.  Artificial Intelligence. 2011;175(2):512–525.
  * 25. Atserias A, Fichte JK, Thurley M.  Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution.  Journal of Artificial Intelligence Research. 2011;40:353–373.
  * 26. Li C, Fleming N, Vinyals M, Pitassi T, Ganesh V.  Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers.  In: Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT ’20). vol. 12178 of Lecture Notes in Computer Science. Springer; 2020. p. 233–249.
  * 27. Davis M, Putnam H.  A Computing Procedure for Quantification Theory.  Journal of the ACM. 1960;7(3):201–215.
  * 28. Davis M, Logemann G, Loveland DW.  A machine program for theorem-proving.  Communications of the ACM. 1962;5(7):394–397.
  * 29. Schöning U, Torán J.  The Satisfiability Problem: Algorithms and Analyses. vol. 3 of Mathematics for Applications (Mathematik für Anwendungen).  Lehmanns Media; 2013.
  * 30. Buss S, Nordström J.  Proof Complexity and SAT Solving.  In: Biere A, Heule MJH, van Maaren H, Walsh T, editors. Handbook of Satisfiability. vol. 336 of Frontiers in Artificial Intelligence and Applications. 2nd ed. IOS Press; 2021. p. 233–350.
  * 31. Zhang L, Madigan CF, Moskewicz MH, Malik S.  Efficient Conflict Driven Learning in a Boolean Satisfiability Solver.  In: Digest of Technical Papers of the IEEE/ACM International Conference on Computer Aided Design (ICCAD ’01). IEEE; 2001. p. 279–285.
  * 32. Dershowitz N, Hanna Z, Nadel A.  Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver.  In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT ’07). vol. 4501 of Lecture Notes in Computer Science. Springer; 2007. p. 287–293.
  * 33. Audemard G, Simon L.  On the Glucose SAT solver.  International Journal on Artificial Intelligence Tools (IJAIT). 2008;27(1):7–25.
  * 34. Darwiche A, Pipatsrisawat K.  Complete Algorithms.  In: Handbook of Satisfiability. vol. 336 of Frontiers in Artificial Intelligence and Applications. 2nd ed. IOS Press; 2021. p. 101–132.
  * 35. Johnson NL, Kotz S, Balakrishnan N.  Continuous Univariate Distributions, Volume 1.  2nd ed. Wiley Series in Probability and Statistics. John Wiley & Sons; 1994.
  * 36. Gibbons JD, Chakraborti S.  Nonparametric Statistical Inference: Fourth Edition, Revised and Expanded.  Statistics: A Dekker series of textbooks and monographs. Marcel Dekker; 2014.
  * 37. Aalen OO, Borgan Ø, Gjessing HK.  Survival and Event History Analysis: A Process Point of View.  Statistics for Biology and Health. Springer Science & Business Media; 2008.
  * 38. Böhmer P.  Theorie der unabhängigen Wahrscheinlichkeiten.  In: Rapports Mémoires et Procés – verbaux de Septième Congrès International D’actuaires Amsterdam. vol. 2; 1912. p. 327–343.
  * 39. Kaplan EL, Meier P.  Nonparametric Estimation from Incomplete Observations.  Journal of the American Statistical Association. 1958;53(282):457–481.
  * 40. Balyo T, Froleyks N, Heule MJH, Iser M, Järvisalo M, Suda M.  Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions.  University of Helsinki, Department of Computer Science; 2020.
  * 41. Froleyks N, Heule MJH, Iser M, Järvisalo M, Suda M.  SAT Competition 2020.  Artificial Intelligence. 2021;301:103572.
  * 42. Völkel G, Lausser L, Schmid F, Kraus JM, Kestler HA.  Sputnik: _ad hoc_ distributed computation.  Bioinformatics. 2015;31(8):1298–1301.
  * 43. Julian P, Helsel D. NADA2: Data Analysis for Censored Environmental Data; 2021.  Available from: https://rdrr.io/cran/NADA2/.
  * 44. Helsel DR.  Statistics for Censored Environmental Data Using Minitab and R.  CourseSmart Series. Wiley; 2012.
  * 45. Oh C.  Between SAT and UNSAT: The Fundamental Difference in CDCL SAT.  In: Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT ’15). vol. 9340 of Lecture Notes in Computer Science. Springer; 2015. p. 307–323.
  * 46. Hartigan JA, Hartigan PM.  The dip test of unimodality.  The Annals of Statistics. 1985;13(1):70–84.
  * 47. Pearson K.  Contributions to the mathematical theory of evolution: On the dissection of asymmetrical frequency-curves.  Philosophical Transactions of the Royal Society A. 1894;185:71–110.
  * 48. Therneau TM. A Package for Survival Analysis in R; 2021.  Available from: https://rdrr.io/cran/survival/.
  * 49. Dempster AP, Laird NM, Rubin DB.  Maximum likelihood from incomplete data via the EM algorithm.  Journal of the Royal Statistical Society: Series B (Methodological). 1977;39(1):1–22.
  * 50. Folk RL, Ward WC.  Brazos river bar: a study in the significance of grain size parameters.  Journal of Sedimentary Research. 1957;27(1):3–26.
  * 51. Dyer KR.  Grain size parameters for sandy-gravels.  Journal of Sedimentary Research. 1970;40(2):616–620.
  * 52. Rinne H.  The Weibull Distribution: A Handbook.  CRC press; 2008.
  * 53. Nair J, Wierman A, Zwart B.  The Fundamentals of Heavy Tails: Properties, Emergence, and Estimation; 2020.
  * 54. Foss S, Korshunov D, Zachary S.  An Introduction to Heavy‑Tailed and Subexponential Distributions. vol. 6.  Springer; 2011.
  * 55. Lorenz JH.  Restart Strategies.  Distinguished Dissertations. Books on Demand; 2021.
  * 56. Goldberg E, Novikov Y.  BerkMin: A fast and robust SAT-solver.  Discrete Applied Mathematics. 2007;155(12):1549–1561.
  * 57. Sörensson N, Biere A.  Minimizing Learned Clauses.  In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT ’09). vol. 5584 of Lecture Notes in Computer Science. Springer; 2009. p. 237–243.
  * 58. Fréchet M.  Sur la loi de probabilité de l’écart maximum.  Annales de la Société Polonaise de Mathématique. 1927;6(1):93–116.
  * 59. Fisher RA, Tippett LHC.  Limiting forms of the frequency distribution of the largest or smallest member of a sample.  Mathematical Proceedings of the Cambridge Philosophical Society. 1928;24(2):180–190.
  * 60. Von Mises R.  La distribution de la plus grande de $n$ valeurs.  Rev math Union interbalcanique. 1936;1:141–160.
  * 61. Gnedenko BV.  Sur la distribution limite du terme maximum d’une serie aleatoire.  Annals of Mathematics. 1943; p. 423–453.
  * 62. Krüger T, Lorenz JH, Wörz F. Supplementary Data for “Too much information: CDCL solvers need to forget and perform restarts”; 2021.  The repository can be found under doi:10.5281/zenodo.6642166.