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-