I
L
L
U
S
T
R
A
T
I
O
N
B
Y
E
U
G
E
N
E
K
O
S
T
S
O
V
lem instances (we have considered
dozens), and solvers (again, dozens).
We have robustly found that even very
succinct EHMs can achieve high accu-
racies, meaning they describe simple
relationships between instance char-
acteristics and algorithm runtime.a
This makes our approach important
even for theoretically inclined com-
puter scientists who prefer proofs
to experimental findings: EHMs can
uncover new, simple relationships
between instance characteristics and
runtime, and thereby catalyze new
theoretical work.
The focus of this article is on ways
that EHMs contribute to our
understanding of NP-complete problems;
however, they are also useful in a variety of practical applications. Most
straightforwardly, they can aid the
distribution of problem instances
across a cluster, or predict how long
a run will take to complete. More
interestingly, they can be used to
combine a set of high-variance algorithms into an “algorithm portfolio”
that outperforms its constituents;
be leveraged to automatically make
benchmark distributions more challenging; and aid in the configuration
(or “tuning”) of highly parameterized
algorithms for good performance on
given instance distributions. More
detailed explanations of these applications appear in sidebars throughout this article.
Phase Transitions in
Uniform-Random 3-SAT
We begin by describing the most widely
known relationship between a characteristic of fixed-size random SAT
instances and solver runtime. (
After this, we consider more realistic
instances of SAT and other NP-hard
problems.) Let p(c, v) denote the probability that a satisfiable 3-SAT for-
a We do not survey the literature on algorithm
performance prediction here; instead we focus on our own work. For extensive discussions of related work, please see Hutter et al.
21
and Leyton-Brown et al.
29
mulab will be generated by uniformly
sampling c clauses of three variables
each from a set of v variables, negating
each with probability 0.5. In the early
1990s, researchers discovered that
when v is held constant, p(c, v) exhibits a “phase transition” as c/v crosses
a critical value of about 4. 26.
8, 31 Intuitively, instances with few clauses are
underconstrained and thus almost
always satisfiable, while those with
many clauses are overconstrained and
almost always unsatisfiable. The interesting fact is that, for all fixed values
of v so far tested, the phase transition
b A SAT formula F is solved by deciding whether
there exists an assignment of its variables under which F evaluates to true. A subclass of particular importance is 3-SAT. A 3-SAT instance
is a conjunction of clauses, each of which is a
disjunction of three variables or their negations. For example, (v1 ∨¬ v2 ∨ v4) ∧ (¬v1 ∨¬v3
∨ v4) is a simple formula with v = 4 variables and
c = 2 clauses that has several satisfying assign-
ments (for example, [v1, v2, v3, v4] = [true, true,
false, false]).
point at which p(c, v) is exactly 0.5, ap-
pears to coincide with a runtime peak
even for the SAT solvers that perform
best on these instances. This finding
thus links an algorithm-independent
property of an instance (c/v) with al-
gorithm-specific runtime in a way that
has proven robust across solvers.
Figure 1 (left) shows this relationship
using real data. The dotted line shows
p(c, v) for uniform-random 3-SAT instances with v = 400, while the solid line
shows the mean runtime of march _
hi,
11 one of the best SAT solvers for
uniform-random 3-SAT, on the same
instances. We do indeed observe both
a phase transition and a hardness spike
at the phase transition point. However, there is more to the story. Figure 1
(right) plots raw runtime data (on a log
scale) for march _ hi, with each point
corresponding to a single (random)
3-SAT formula. We can now see that the
c/v ratio does not suffice to fully explain
march _ hi’s empirical behavior on
these instances: there is still substan-