Authors Jakob Nordstr{\"o}m, Johan H{\aa}stad,
License CC-BY-3.0
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557
www.theoryofcomputing.org
Towards an Optimal Separation of
Space and Length in Resolution∗
Jakob Nordström† Johan Håstad‡
Received February 16, 2011; Revised March 9, 2013; Published May 27, 2013
Abstract: Most state-of-the-art satisfiability algorithms today are variants of the DPLL
procedure augmented with clause learning. The main bottleneck for such algorithms, other
than the obvious one of time, is the amount of memory used. In the field of proof complexity,
the resources of time and memory correspond to the length and space of resolution proofs.
There has been a long line of research trying to understand these proof complexity measures,
as well as relating them to the width of proofs, i.e., the size of a largest clause in the proof,
which has been shown to be intimately connected with both length and space. While strong
results have been proven for length and width, our understanding of space has been quite poor.
For instance, it has remained open whether the fact that a formula is provable in short length
implies that it is also provable in small space (which is the case for length versus width), or
∗ A preliminary version of this paper appeared in the Proceedings of the 40th Annual ACM Symposium on Theory of
Computing (STOC ’08).
† Part of this work done while at the Massachusetts Institute of Technology supported by the Royal Swedish Academy of
Sciences, the Ericsson Research Foundation, the Sweden-America Foundation, the Foundation Olle Engkvist Byggmästare, and
the Foundation Blanceflor Boncompagni-Ludovisi, née Bildt. Currently supported by the European Research Council under
the European Union’s Seventh Framework Programme (FP7/2007–2013) / ERC grant agreement no 279611 and by Swedish
Research Council grants 621-2010-4797 and 621-2012-5645.
‡ Supported by the European Research Council under the European Union’s Seventh Framework Programme
(FP7/2007–2013) / ERC grant agreement no 226203.
ACM Classification: F.4.1, F.1.3, I.2.3
AMS Classification: 68Q05, 68Q15, 68Q17, 68T15
Key words and phrases: proof complexity, resolution, length, space, width, separation, lower bound,
pebbling, black-white pebble game
© 2013 Jakob Nordström and Johan Håstad
c b Licensed under a Creative Commons Attribution License (CC-BY) DOI: 10.4086/toc.2013.v009a014
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
whether these measures are unrelated in the sense that short proofs can be arbitrarily complex
with respect to space.
In this paper, we present some evidence indicating that the latter case should hold and
provide a roadmap for how such an optimal separation result could be obtained. We do so by
√
proving a tight bound of Θ( n) on the space needed for so-called pebbling contradictions
over pyramid graphs of size n. This yields the first polynomial lower bound on space that
is not a consequence of a corresponding lower bound on width, as well as an improvement
of the weak separation of space and width (Nordström, STOC 2006) from logarithmic to
polynomial.
Contents
1 Introduction 474
1.1 Previous work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475
1.2 Questions left open by previous research . . . . . . . . . . . . . . . . . . . . . . . . . . 476
1.3 Our contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477
1.4 Subsequent developments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 478
2 Proof overview and paper organization 478
2.1 Sketch of preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 478
2.2 Proof idea for pebbling contradictions space bound . . . . . . . . . . . . . . . . . . . . 479
2.3 Detailed overview of formal proof of space bound . . . . . . . . . . . . . . . . . . . . . 481
2.4 Paper organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 484
3 Formal preliminaries 484
3.1 The resolution proof system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 484
3.2 Pebble games and pebbling contradictions . . . . . . . . . . . . . . . . . . . . . . . . . 486
4 A game for analyzing pebbling contradictions 488
4.1 Some graph notation and definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 488
4.2 Description of the blob-pebble game and formal definition . . . . . . . . . . . . . . . . 489
4.3 Blob-Pebbling price . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 493
5 Resolution derivations induce blob-pebblings 495
5.1 Definition of induced configurations and theorem statement . . . . . . . . . . . . . . . . 495
5.2 Some technical lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 497
5.3 Erasure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 498
5.4 Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 498
5.5 Axiom download . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 498
5.6 Wrapping up the proof of Theorem 5.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . 502
6 Induced blob configurations measure clause set size 503
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 472
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
7 Black-white pebbling and layered graphs 508
7.1 Some preliminaries and a tight bound for black pebbling . . . . . . . . . . . . . . . . . 508
7.2 A tight bound on the black-white pebbling price of pyramids . . . . . . . . . . . . . . . 511
7.3 An exposition of the proof of the limited hiding-cardinality property . . . . . . . . . . . 516
8 A tight bound for blob-pebbling the pyramid 526
8.1 Definitions and notation for the blob-pebbling price lower bound . . . . . . . . . . . . . 527
8.2 A lower bound assuming an extension of the LHC property . . . . . . . . . . . . . . . . 529
8.3 Some structural transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 531
8.4 Proof of the generalized limited hiding-cardinality property . . . . . . . . . . . . . . . . 534
8.5 Recapitulation of the proof of Theorem 1.1 and optimality of result . . . . . . . . . . . . 547
9 Conclusion and open problems 548
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 473
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
1 Introduction
Ever since the fundamental NP-completeness result of Cook [24], the problem of deciding whether a
given propositional logic formula in conjunctive normal form (CNF) is satisfiable or not has been on
center stage in Theoretical Computer Science. In more recent years, SATISFIABILITY has gone from a
problem of mainly theoretical interest to a practical approach for solving applied problems. Although
all known Boolean satisfiability solvers (SAT solvers) have exponential running time in the worst case,
enormous progress in performance has led to satisfiability algorithms becoming a standard tool for solving
a large number of real-world problems such as hardware and software verification, experiment design,
circuit diagnosis, and scheduling.
A rather surprising aspect of this development is that the most successful SAT solvers to date are
still variants of the resolution-based Davis-Putnam-Logemann-Loveland (DPLL) procedure [28, 29]
augmented with clause learning [7, 46]. For instance, the great majority of the best algorithms in recent
rounds of the international SAT competitions [58] fit this description. DPLL procedures perform a
recursive backtrack search in the space of partial truth value assignments. The idea behind clause learning
is that at each failure (backtrack) point in the search tree, the system derives a reason for the inconsistency
in the form of a new clause and then adds this clause to the original CNF formula (“learning” the clause).
This can save a lot of work later on in the proof search, when some other partial truth value assignment
fails for similar reasons. The second main bottleneck for this approach, in addition to the obvious one of
time, is the amount of memory used by the algorithms. Since there is only a limited amount of space, all
clauses cannot be stored. The difficulty lies in obtaining a highly selective and efficient clause caching
scheme that nevertheless keeps the clauses needed. Thus, understanding time and memory requirements
for clause learning algorithms, and how these requirements are related to one another, is a question of
great practical importance. We refer to, e.g., [41, 45] for a more detailed discussion SAT solving with
examples of applications.
The study of proof complexity originated with the seminal paper of Cook and Reckhow [26]. In its
most general form, a proof system for a language L is a predicate P(x, π), computable in time polynomial
in |x| and |π|, such that for all x ∈ L there is a string π (a proof ) for which P(x, π) = 1, whereas for any
x 6∈ L it holds for all strings π that P(x, π) = 0. A proof system is said to be polynomially bounded if for
every x ∈ L there is a proof πx of size at most polynomial in |x|. A propositional proof system is a proof
system for the language of tautologies in propositional logic.
From a theoretical point of view, one important motivation for proof complexity is the intimate
connection with the question of P versus NP. Since NP is exactly the set of languages with polynomially
bounded proof systems, and since TAUTOLOGY can be seen to be the dual problem of SATISFIABILITY,
we have the famous theorem of [26] that NP = co-NP if and only if there exists a polynomially bounded
propositional proof system. Hence, if it could be shown that there are no such proof systems, P 6= NP
would follow as a corollary since P is closed under complement. One way of approaching this distant
goal is to study stronger and stronger proof systems and try to prove superpolynomial lower bounds on
proof size. However, although great progress has been made in the last couple of decades for a variety of
proof systems, it seems that we are still very far from fully understanding the reasoning power of even
quite simple ones.
A second important motivation is that, as was mentioned above, designing efficient algorithms for
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 474
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
proving tautologies (or, equivalently, testing satisfiability), is an important problem not only in the theory
of computation but also in applied research and industry. All automated theorem provers, regardless of
whether they actually produce a written proof or not, explicitly or implicitly define a system in which
proofs are searched for and rules which determine what proofs in this system look like. Proof complexity
analyzes what it takes to simply write down and verify the proofs that such an automated theorem prover
might find, ignoring the computational effort needed to actually find them. Thus, a lower bound for a
proof system tells us that any algorithm, even an optimal (non-deterministic) one making all the right
choices, must necessarily use at least the amount of a certain resource specified by this bound. In the
other direction, theoretical upper bounds on some proof complexity measure give us hope of finding good
proof search algorithms with respect to this measure, provided that we can design algorithms that search
for proofs in the system in an efficient manner. For DPLL procedures with clause learning, the time and
memory resources used are measured by the length and space of proofs in the resolution proof system.
The field of proof complexity also has rich connections to cryptography, artificial intelligence and
mathematical logic. Some good surveys providing more details are [8, 11, 59].
1.1 Previous work
Any formula in propositional logic can be converted to a CNF formula that is only linearly larger and is
unsatisfiable if and only if the original formula is a tautology. Therefore, any sound and complete system
for refuting CNF formulas can be considered as a general propositional proof system.
Perhaps the single most studied proof system in propositional proof complexity, resolution, is such
a system that produces proofs of the unsatisfiability of CNF formulas. The resolution proof system
appeared in [18] and began to be investigated in connection with automated theorem proving in the 1960s
[28, 29, 56]. Because of its simplicity—there is only one derivation rule—and because all lines in a proof
are clauses, this proof system readily lends itself to proof search algorithms.
Being so simple and fundamental, resolution was also a natural target to attack when developing
methods for proving lower bounds in proof complexity. In this context, it is more convenient to prove
bounds on the length of refutations, i. e., the number of clauses, rather than on the total size of refutations.
The length and size measure differ by at most a multiplicative factor given by the number of variables
and are hence polynomially related. In 1968, Tseitin [61] presented a superpolynomial lower bound on
refutation length for a restricted form of resolution, called regular resolution, but it was not until almost
20 years later that Haken [36] proved the first superpolynomial lower bound for general resolution. This
(weakly) exponential lower bound of Haken has later been followed by many other strong results on
resolution refutation length for different formula families, e. g., in [10, 17, 22, 23, 52, 54, 55, 62].
A second complexity measure for resolution, first made explicit by Galil [33], is the width, measured
as the maximal size of a clause in the refutation. Ben-Sasson and Wigderson [17] showed that the minimal
width W(F `⊥) of any resolution refutation of a k-CNF formula F is bounded from above by the minimal
refutation length L(F ` ⊥) by
p
W(F ` ⊥) = O n log L(F ` ⊥) , (1.1)
where n is the number of variables in F. Since it is also easy to see that refutations of polynomial-size
formulas in small width must necessarily be short (simply for the reason that (2 · #variables)w is an upper
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 475
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
bound on the total number of distinct clauses of width w), the result in [17] can be interpreted as saying
roughly that there exists a short refutation of the k-CNF formula F if and only if there exists a (reasonably)
narrow refutation of F. This gives rise to a natural proof search heuristic: to find a short refutation, search
for refutations in small width. It was shown in [14] that there are formula families for which this heuristic
exponentially outperforms any DPLL procedure regardless of branching function.
The formal study of space1 in resolution was initiated by Esteban and Torán [31]. Intuitively, the
space Sp(π) of a refutation π is the maximal number of clauses one needs to keep in memory while
verifying the refutation, and the space Sp(F ` ⊥) of refuting F is defined as the minimal space of any
resolution refutation of F. A number of upper and lower bounds for refutation space in resolution and
other proof systems were subsequently presented in, for example, [2, 13, 30, 32]. Just as for width, the
minimum space of refuting a formula can be upper-bounded by the size of the formula. Somewhat
unexpectedly, however, it also turned out that the lower bounds on refutation space for several different
formula families exactly matched previously known lower bounds on refutation width. Atserias and
Dalmau [5] showed that this was not a coincidence, but that the inequality
W(F ` ⊥) ≤ Sp(F ` ⊥) + O(1) (1.2)
holds for any k-CNF formula F, where the (small) constant term depends on k. In [47], the first author
proved that the inequality (1.2) is asymptotically strict by exhibiting a k-CNF formula family of size O(n)
refutable in width W(Fn ` ⊥) = O(1) but requiring space Sp(Fn ` ⊥) = Θ(log n).
1.2 Questions left open by previous research
Despite all the research that has gone into understanding the resolution proof system, a number of
fundamental questions have remained unsolved. We touch briefly on two such questions below, and then
discuss a third one, which is the main focus of this paper, in somewhat more detail.
As was mentioned above, equation (1.1) says that short refutation length implies narrow refutation
width. Observe, however, that this does not mean that there is a refutation that is both short and narrow,
since there is no guarantee that the refutations on the left- and right-hand sides of (1.1) are the same one.
An intriguing open question is whether small length and width can always be achieved simultaneously,
or whether there is a trade-off between these two measures. For the restricted case of so-called tree-like
resolution it is known that there can be strong trade-offs [12], but the case of the (much more powerful)
general resolution proof system has remained open.
A second, analogous problem concerns space and length. Combining equation (1.2) with the observa-
tion above that narrow refutations are trivially short, one can immediately conclude that small refutation
clause space implies short refutation length. But again, this does not imply that any small-space refutation
must also be short. In fact, it was shown in [12] that the refutations on the two sides of the inequality
(1.2) in general cannot be the same one. An interesting question is whether small space of a refutation
implies that it can also be made short, or whether space and length might have to be traded off against
one another.
1 The space measure discussed in this introduction is known as clause space. Another natural, but less studied, space measure
is total space, which counts the maximal number of variable occurrences that must be kept in memory simultaneously. The
focus of the current paper, however, is almost exclusively on clause space.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 476
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
A third, even more fundamental question is whether short length has any implications for space. Note
that for width, rewriting the bound in (1.1) in terms of pthe number of clauses |Fn | instead of the number of
variables tells us that if the width of refuting Fn is ω |Fn | log|Fn | , then the length of refuting Fn must be
superpolynomial in |Fn |. This is known p to be almost
tight, since [20] shows that there is a k-CNF formula
family {Fn }∞ n=1 that requires width Ω 3
|Fn | but nevertheless can be refuted in length O(|Fn |). Hence,
formula families refutable in polynomial length can have somewhat wide minimum-width refutations, but
not arbitrarily wide ones.
What does the corresponding relation between length and space look like? The inequality (1.2)
tells us that any correlation between length and clause space cannot be tighter than the correlation
between length and width, so in particular we get from the previous paragraph that k-CNF formulas
refutable in polynomial length may have at least “somewhat spacious” minimum-space refutations. At
the other end of the spectrum, given any resolution refutation π of F in length L it can be proven using
results from [31, 39] that the space needed is at most O(L/ log L). This gives an upper bound on any
possible separation of the two measures. But is there a Ben-Sasson–Wigderson style upper bound on
space in terms of length similar to (1.1)? Or are length and space on the contrary unrelated in the
sense that there exist k-CNF formulas Fn with short refutations but maximal possible refutation space
Sp(Fn ` ⊥) = Ω L(Fn ` ⊥)/ log L(Fn ` ⊥) in terms of length?
We remark that for tree-like resolution, [31] showed that there is a tight correspondence between
length and space, exactly as for length versus width. The case for general resolution has been discussed
in, e. g., [12, 32, 60], but there has been no consensus on what the right answer should be. However,
these papers identify a plausible formula family for answering the question, namely so-called pebbling
contradictions defined in terms of pebble games over directed acyclic graphs.
1.3 Our contribution
The main result in this paper provides an indication that the true answer to the question about the
relationship between space and length is more likely to be at the latter extreme, i. e., that the two measures
can be separated in the strongest sense possible. More specifically, as a step towards reaching this goal we
prove an asymptotically tight bound on the clause space of refuting pebbling contradictions over so-called
pyramid graphs.
Theorem 1.1. The clause space of refuting pebbling contradictions over pyramid graphs of height h in
resolution grows as Θ(h), provided that the number of variables per vertex in the pebbling contradictions
is at least 2.
This theorem yields the first separation of space and length (in the sense of a polynomial lower bound
on space for formulas refutable in polynomial length) that is not a consequence of a corresponding lower
bound on width, as well as an exponential improvement of the separation of space and width in [47].
Namely, from Theorem 1.1 we easily obtain the following corollary.
Corollary 1.2. For all k ≥ 4, there is a family {Fn }∞
n=1 of k-CNF formulas of size Θ(n) that can be
refuted in resolution in length L(Fn ` ⊥) = O(n) and width W(Fn ` ⊥) = O(1) but require clause space
√
Sp(Fn ` ⊥) = Θ( n).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 477
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
1.4 Subsequent developments
In a joint paper [15] by Ben-Sasson and the first author, the separation in Corollary 1.2 has been improved
to a clause space lower bound Sp(Fn ` ⊥) = Ω(n/ log n) while still keeping the upper bounds on length
L(Fn `⊥) = O(n) and width W(Fn `⊥) = O(1). This is essentially optimal up to multiplicative constants
(except possibly for a logarithmic factor in the space-width separation). The construction in [15] follows
the general roadmap laid out in the current paper, but changes the family of formulas under consideration
in Theorem 1.1. The new results are therefore incomparable with those in the current paper in that the
techniques used in [15] cannot prove Theorem 1.1, whereas our techniques, although similar, do not
extend to the results in [15].
Even considering the progress made in [15], we believe that the results presented in our paper retain
independent interest. This is so since our formula families are simpler, and an improvement of our
techniques could conceivably yield optimal, tight results up to constant additive terms. This, in turn,
could possibly be used to settle the question how hard it is to decide the space requirements for refuting a
k-CNF formula. This problem is easily seen to be in PSPACE but is not known to be PSPACE-complete.
Due to the inherent space blow-up between upper and lower bounds in [15], it is hard to envision the
results from there being used for similar purposes. We elaborate briefly on this issue in Section 9.
2 Proof overview and paper organization
Since the proof of our main theorem is fairly involved, we start by giving an intuitive, high-level
description of the proofs of our results and outlining how this paper is organized.
2.1 Sketch of preliminaries
A resolution refutation of a CNF formula F can be viewed as a sequence of derivation steps on a
blackboard. In each step we may write a clause from F on the blackboard (an axiom clause), erase
a clause from the blackboard or derive some new clause implied by the clauses currently written on
the blackboard.2 The refutation ends when we reach the contradictory empty clause. The length of a
resolution refutation is the number of clauses in the refutation, the width is the size of the largest clause in
the refutation, and the clause space is the maximum number of clauses on the blackboard simultaneously.
We write L(F ` ⊥), W(F ` ⊥) and Sp(F ` ⊥) to denote the minimum length, width and clause space,
respectively, of any resolution refutation of F.
The pebble game played on a directed acyclic graph (DAG) G models the calculation described by G,
where the source vertices contain the input and non-source vertices specify operations on the values of the
predecessors (see Figure 1). Placing a pebble on a vertex v corresponds to storing in memory the partial
result of the calculation described by the subgraph rooted at v. Removing a pebble from v corresponds to
deleting the partial result of v from memory. A pebbling of a DAG G is a sequence of moves starting
with an empty graph G without pebbles and ending with all vertices in G empty except for a pebble on
the (unique) sink vertex. The cost of a pebbling is the maximal number of pebbles used simultaneously
2 For our proof, it turns out that the exact definition of the derivation rule is not essential—our lower bound holds for any
sound rule. What is important is that we are only allowed to derive new clauses from the set of clauses currently on the board.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 478
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
− 1 −
+ × 7 + 6 ×
4 3 2
(a) DAG encoding calculation. (b) After pebbling with results filled in.
Figure 1: Example of modelling calculation as pebbling of DAG.
at any point in time during the pebbling. The pebbling price of a DAG G is the minimum cost of any
pebbling, i. e., the minimum number of memory registers required to perform the complete calculation
described by G.
The pebble game on a DAG G can be encoded as an unsatisfiable CNF formula PebdG , a so-called
pebbling contradiction of degree d. See Figure 2 for a small example. Very briefly, pebbling contradictions
are constructed as follows:
• Associate d variables x(v)1 , . . . , x(v)d with each vertex v (in Figure 2 we have d = 2).
• Specify that all sources have at least one true variable, for example, the clause x(r)1 ∨ x(r)2 for the
vertex r in Figure 2.
• Add clauses saying that truth propagates from predecessors to successors. For instance, for the
vertex u with predecessors r and s, clauses 4–7 in Figure 2 are the CNF encoding of the implication
(x(r)1 ∨ x(r)2 ) ∧ (x(s)1 ∨ x(s)2 ) → (x(u)1 ∨ x(u)2 ).
• To get a contradiction, conclude the formula with x(z)1 ∧ · · · ∧ x(z)d where z is the sink of the DAG.
We will need the observation from [14] that a pebbling contradiction of degree d over a graph with
n vertices can be refuted by resolution in length O d 2 · n and width O(d).
2.2 Proof idea for pebbling contradictions space bound
Pebble games have been used extensively as a tool to prove time and space lower bounds and trade-offs
for computation. Loosely put, a lower bound for the pebbling price of a graph says that although the
computation that the graph describes can be performed quickly (any graph can be pebbled in linear time),
it requires large space. Our hope is that when we encode pebble games in terms of CNF formulas, these
formulas inherit the same properties as the underlying graphs. That is, if we pick a DAG G with high
pebbling price, since the corresponding pebbling contradiction encodes a calculation which requires large
memory we would like to try to argue that any resolution refutation of this formula should require large
space. Then a separation result would follow since we already know from [14] that the formula can be
refuted in short length.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 479
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
(x(r)1 ∨ x(r)2 ) ∧ (x(u)1 ∨ x(v)1 ∨ x(z)1 ∨ x(z)2 )
∧ (x(s)1 ∨ x(s)2 ) ∧ (x(u)1 ∨ x(v)2 ∨ x(z)1 ∨ x(z)2 )
∧ (x(t)1 ∨ x(t)2 ) ∧ (x(u)2 ∨ x(v)1 ∨ x(z)1 ∨ x(z)2 )
∧ (x(r)1 ∨ x(s)1 ∨ x(u)1 ∨ x(u)2 ) ∧ (x(u)2 ∨ x(v)2 ∨ x(z)1 ∨ x(z)2 )
∧ (x(r)1 ∨ x(s)2 ∨ x(u)1 ∨ x(u)2 ) ∧ x(z)1
∧ (x(r)2 ∨ x(s)1 ∨ x(u)1 ∨ x(u)2 ) ∧ x(z)2
z
∧ (x(r)2 ∨ x(s)2 ∨ x(u)1 ∨ x(u)2 )
∧ (x(s)1 ∨ x(t)1 ∨ x(v)1 ∨ x(v)2 )
u v
∧ (x(s)1 ∨ x(t)2 ∨ x(v)1 ∨ x(v)2 )
∧ (x(s)2 ∨ x(t)1 ∨ x(v)1 ∨ x(v)2 )
∧ (x(s)2 ∨ x(t)2 ∨ x(v)1 ∨ x(v)2 ) r s t
Figure 2: The pebbling contradiction Peb2Π2 for the pyramid graph Π2 of height 2.
More specifically, what we would like to do is to establish a connection between resolution refutations
of pebbling contradictions on the one hand, and the so-called black-white pebble game [27] modelling
the non-deterministic computations described by the underlying graphs on the other. Our intuition is
that the resolution proof system should have to conform to the combinatorics of the pebble game in the
sense that from any resolution refutation of a pebbling contradiction PebdG we should be able to extract a
pebbling of the DAG G. Our goal is to prove a lower bound on the resolution refutation space of pebbling
contradictions reasoning along the following lines:
1. First, find a way of interpreting sets of clauses currently “on the blackboard” in a refutation of the
formula PebdG in terms of black and white pebbles on the vertices of the DAG G.
2. Then, prove that this interpretation captures the pebble game in the following sense: for any resolu-
tion refutation of PebdG , looking at consecutive sets of clauses on the blackboard and considering
the corresponding sets of pebbles in the graph we get a black-white pebbling of G in accordance
with the rules of the pebble game.
3. Finally, show that the interpretation also captures clause space in the sense that if the content of the
blackboard corresponds to N pebbles on the graph, then there must be at least N clauses on the
blackboard.
Combining the above with known lower bounds on the pebbling price of G, this would imply a lower
bound on the refutation space of pebbling contradictions and a separation from length and width. For
clarity, let us spell out what the formal argument of this would look like.
Consider an arbitrary resolution refutation of PebdG . From this refutation we extract a pebbling of G.
At some point in time t in the obtained pebbling, there must be a lot of pebbles on the vertices of G since
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 480
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
this graph was chosen with high pebbling price. But this means that at time t, there are a lot of clauses on
the blackboard. Since this holds for any resolution refutation, the refutation space of PebdG must be large.
The separation result now follows from the fact that pebbling contradictions are known to be refutable in
linear length and constant width if d is fixed.
Unfortunately, we cannot quite get this idea to work. In the next subsection, we describe the
modifications that we are forced to make and show how we can make the bits and pieces of our
construction fit together to yield Theorem 1.1 and Corollary 1.2 for the special case of pyramid graphs.
2.3 Detailed overview of formal proof of space bound
The black-white pebble game played on a DAG G can be viewed as a way of proving the end result of
the calculation described by G. Black pebbles denote proven partial results of the computation. White
pebbles denote assumptions about partial results which have been used to derive other partial results (i. e.,
black pebbles), but which will have to be verified for the calculation to be complete. The final goal is a
black pebble on the sink z and no other pebbles on the graph, corresponding to an unconditional proof of
the end result of the calculation with any assumptions made along the way having been eliminated.
Translating this to pebbling contradictions, it turns out that a fruitful way to think of a black pebble
on v is that it should correspond to truth of the disjunction di=1 x(v)i of all positive literals over v, or to
W
“truth of v.” A white pebble on a vertex w can be understood to mean that we need to assume the partial
result on w to derive some black pebble on v above w in the graph. Extending the reasoning above we
get that this corresponds to an implication di=1 x(w)i → dj=1 x(v) j which can be rewritten as the set of
W W
clauses ( )
d
_
x(w)i ∨ x(v) j i ∈ [d] . (2.1)
j=1
Based on this, we decide that a white-pebbled vertex should correspond to “falsity of w,” i. e., to all
negative literals x(w)i , i ∈ [d], over w.
Using this intuitive correspondence, we can translate sets of clauses in a resolution refutation of
d
PebG into black and white pebbles on G as in Figure 3. It is easy to see that if we assume x(s)1 ∨ x(s)2
and x(t)1 ∨ x(t)2 , this assumption together with the clauses on the blackboard in Figure 3(a) imply
x(v)1 ∨ x(v)2 , so v should be black-pebbled and s and t white-pebbled in Figure 3(b). The vertex u is also
black since x(u)1 ∨ x(u)2 certainly is implied by the blackboard. This translation from clauses to pebbles
is quite straightforward, and seems to yield well-behaved pebblings for all “sensible” refutations of PebdG .
The problem is that we have no guarantee that the resolution refutations will be “sensible.” Even
though it might seem more or less clear how an optimal refutation of a pebbling contradiction should
proceed, a particular refutation might contain unintuitive and seemingly non-optimal derivation steps
that do not make much sense from a pebble game perspective. In particular, a resolution derivation
has no obvious reason always to derive truth that is restricted to single vertices. For instance, it could
add the axioms x(u)i ∨ x(v)2 ∨ x(z)1 ∨ x(z)2 , i = 1, 2, to the blackboard in Figure 3(a), derive that the
truth of s and t implies the truth of either v or z, i. e., the clauses x(s)i ∨ x(t) j ∨ x(v)1 ∨ x(z)1 ∨ x(z)2 for
i, j = 1, 2, and then erase x(u)1 ∨ x(u)2 from the blackboard. Although it is hard to see from such a small
example, this turns out to be a serious problem in that there appears to be no way that we can interpret
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 481
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
z
x(u)1 ∨ x(u)2
x(s)1 ∨ x(t)1 ∨ x(v)1 ∨ x(v)2
u v
x(s) ∨ x(t) ∨ x(v) ∨ x(v)
1 2 1 2
x(s) ∨ x(t) ∨ x(v) ∨ x(v)
2 1 1 2
x(s)2 ∨ x(t)2 ∨ x(v)1 ∨ x(v)2 r s t
(a) Clauses on blackboard. (b) Corresponding pebbles in the graph.
Figure 3: Example of intuitive correspondence between sets of clauses and pebbles.
z
x(s)1 ∨ x(t)1 ∨ x(v)1 ∨ x(z)1 ∨ x(z)2
x(s) ∨ x(t) ∨ x(v)1 ∨ x(z)1 ∨ x(z)
2
u v
1 2
x(s) ∨ x(t) ∨ x(v) ∨ x(z) ∨ x(z)
2 1 1 1 2
x(s)2 ∨ x(t)2 ∨ x(v)1 ∨ x(z)1 ∨ x(z)2 r s t
(a) New set of clauses on blackboard. (b) Corresponding blobs and pebbles.
Figure 4: Interpreting sets of clauses as black blobs and white pebbles.
such derivation steps in terms of black and white pebbles without making some component in the proof
idea in Section 2.2 break down.
Instead, what we do is to invent a new pebble game, with white pebbles just as before, but with black
blobs that can cover multiple vertices instead of single-vertex black pebbles. A blob on a vertex set V can
be thought of as truth of some vertex v ∈ V . The derivation sketched in the preceding paragraph, resulting
in the set of clauses in Figure 4(a), will then be translated into white pebbles on s and t as before and a
black blob covering both v and z in Figure 4(b). We define rules in this blob-pebble game corresponding
roughly to black and white pebble placement and removal in the usual black-white pebble game, and add
a special inflation rule allowing us to inflate black blobs to cover more vertices.
Once we have this blob-pebble game, we use it to construct a lower bound proof as outlined in
Section 2.2. First, we establish that for a fairly general class of graphs—namely layered graphs, where the
vertices can be divided into layers and all edges go between consecutive layers—any resolution refutation
of a pebbling contradiction can be interpreted as a blob-pebbling on the DAG in terms of which this
pebbling contradiction is defined. Intuitively, the reason that this works is that we can use the inflation
rule to analyze apparently non-optimal steps in the refutation.
Theorem 2.1. Let PebdG denote the pebbling contradiction of degree d ≥ 1 over a layered DAG G. Then
there is a translation function from sets of clauses derived from PebdG into sets of black blobs and white
pebbles in G such that any resolution refutation π of PebdG corresponds to a blob-pebbling Pπ of G under
this translation.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 482
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
In fact, the only property that we need from the layered graphs in Theorem 2.1 is that if w is a vertex
with (immediate) predecessors u and v, then there is no path between the siblings u and v. The theorem
holds for any DAG satisfying this condition.
Next, we carefully design a cost function for black blobs and white pebbles so that the cost of the
blob-pebbling Pπ in Theorem 2.1 is related to the space of the resolution refutation π.
Theorem 2.2. If π is a refutation of a pebbling contradiction PebdG of degree d > 1, then the cost of the
associated blob-pebbling Pπ is bounded by the space of π by cost(Pπ ) ≤ Sp(π) + O(1).
Without going into too much detail, in order to make the proof of Theorem 2.2 work we can only
charge for black blobs having distinct lowest vertices (measured in topological order), so additional blobs
with the same bottom vertices are free. Also, we can only charge for white pebbles below these bottom
vertices.
Finally, we need lower bounds on blob-pebbling price. Because of the inflation rule in combination
with the peculiar cost function, the blob-pebble game seems to behave rather differently from the standard
black-white pebble game, and therefore we cannot appeal directly to known lower bounds on black-white
pebbling price. However, for a more restricted class of graphs than in Theorem 2.1, but still including
binary trees and pyramids, we manage to prove tight bounds on the blob-pebbling price by generalizing
the lower bound construction for black-white pebbling in [42].
Theorem 2.3. Any so-called layered spreading graph Gh of height h has blob-pebbling price Θ(h). In
particular, this holds for pyramid graphs Πh .
Putting all of this together, we can prove our main theorem.
Theorem 1.1 (restated). Let PebdΠh denote the pebbling contradiction of degree d > 1 over the pyramid
graph of height h. Then the clause space of refuting PebdΠh by resolution is Sp(PebdΠh ` ⊥) = Θ(h).
Proof. The upper bound Sp(PebdΠh ` ⊥) = O(h) is easy. A pyramid of height h can be pebbled with
h + O(1) black pebbles, and a resolution refutation can mimic such a pebbling in constant extra clause
space (independent of d) to refute the corresponding pebbling contradiction.
The interesting part is the lower bound. Let π be any resolution refutation of PebdΠh . Consider the
associated blob-pebbling Pπ provided by Theorem 2.1. On the one hand, we know that it holds that
cost(Pπ ) = O(Sp(π)) by Theorem 2.2, provided that d > 1. On the other hand, Theorem 2.3 tells us that
the cost of any blob-pebbling of Πh is Ω(h), so in particular we must have cost(Pπ ) = Ω(h). Combining
these two bounds on cost(Pπ ), we see that Sp(π) = Ω(h).
The pebbling contradiction PebdG is a (2+d)-CNF formula and for constant d the size of the formula is
linear in the number of vertices n of G (compare Figure 2). Thus, for pyramid graphs Πh the corresponding
pebbling contradictions PebdΠh have size quadratic in the height h. Also, when d is fixed the upper bounds
mentioned at the end of Section 2.1 become L(PebdG `⊥) = O(n) and W(PebdG `⊥) = O(1). Corollary 1.2
√
now follows if we set Fn = PebdΠh for d = k − 2 and h = b nc and use Theorem 1.1.
Corollary 1.2 (restated). For all k ≥ 4, there is a family of k-CNF formulas {Fn }∞
n=1 of size O(n) such
√
that L(Fn ` ⊥) = O(n) and W(Fn ` ⊥) = O(1) but Sp(Fn ` ⊥) = Θ( n).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 483
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
2.4 Paper organization
Section 3 provides formal definitions of the concepts introduced in Sections 1 and 2. The bulk of the paper
is then spent proving the lower-bound part of our main result in Theorem 1.1. In Section 4, we define
our modified pebble game, the “blob-pebble game,” that we will use to analyze resolution refutations of
pebbling contradictions. In Section 5 we prove that resolution refutations can be translated into pebblings
in this game, which is Theorem 2.1 in Section 2.3. In Section 6, we prove Theorem 2.2 saying that
the blob-pebbling price accurately measures the clause space of the corresponding resolution refutation.
Finally, after giving a fairly detailed exposition of the lower bound on black-white pebbling of [42] in
Section 7 (with a somewhat simplified analysis tailor-made for our purposes), in Section 8 we delve
into the details of the proof construction and modify it to apply to our blob-pebble game. This gives us
Theorem 2.3. Now Theorem 1.1 and Corollary 1.2 follow as in the proofs given at the end of Section 2.3.
We conclude in Section 9 by giving suggestions for further research.
3 Formal preliminaries
In this section, we define resolution, pebble games and pebbling contradictions. This is standard material
and much of the discussion below is identical or very close to similar sections in [15, 47, 49].
3.1 The resolution proof system
A literal is either a propositional logic variable x or its negation, denoted x. We define x = x. Two literals
a and b are strictly distinct if a 6= b and a 6= b, i. e., if they refer to distinct variables.
A clause C = a1 ∨ · · · ∨ ak is a set of literals. Throughout this paper, without loss of generality all
clauses C are assumed to be nontrivial in the sense that all literals in C are pairwise strictly distinct
(otherwise C is trivially true since it contains some variable and its negation, and it is easy to show that
such clauses can be ignored). We say that C is a subclause of D if C ⊆ D. A clause containing at most k
literals is called a k-clause.
A CNF formula F = C1 ∧ · · · ∧Cm is a set of clauses. A k-CNF formula is a CNF formula consisting
of k-clauses. We define the size S(F) of the formula F to be the total number of literals in F counted with
repetitions. More often, we will be interested in the number of clauses |F| of F.
In this paper, when nothing else is stated it is assumed that A, B,C, D denote clauses; C, D sets of
clauses; x, y propositional variables; a, b, c literals; α, β truth value assignments; and ν a truth value
0 (false) or 1 (true). We write (
α(y) if y 6= x,
α x=ν (y) = (3.1)
ν if y = x,
to denote the truth value assignment that agrees with α everywhere except possibly at x, to which it
assigns the value ν. We let Vars(C) denote the set of variables and Lit(C) the set of literals in a clause C.3
This notation is extended to sets of clauses by taking unions. Also, we employ the standard notation
[n] = {1, 2, . . . , n}.
3 The notation Lit(C) is slightly redundant given the definition of a clause as a set of literals, but we include it for clarity.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 484
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
A resolution derivation π : F ` A of a clause A from a CNF formula F is a sequence of clauses
π = {D1 , . . . , Dτ } such that Dτ = A and each line Di , i ∈ [τ], either is one of the clauses in F (an axiom
clause) or is derived from clauses D j , Dk in π with j, k < i by the resolution rule
B∨x C∨x
. (3.2)
B ∨C
We refer to (3.2) as resolution on the variable x and to B ∨C as the resolvent of B ∨ x and C ∨ x on x. A
resolution refutation of a CNF formula F is a resolution derivation of the empty clause ⊥ (the clause with
no literals) from F. Perhaps somewhat confusingly, this is sometimes also referred to in the literature as a
resolution proof of F, and we will use the two terms “proof” and “refutation” interchangeably in this
paper.
For a formula F and a set of formulas G = {G1 , . . . , Gn }, we say that G implies F, denoted G F,
if every truth value assignment satisfying all formulas G ∈ G satisfies F as well. It is well known that
resolution is sound and implicationally complete. That is, if there is a resolution derivation π : F ` A, then
F A, and if F A, then there is a resolution derivation π : F ` A0 for some A0 ⊆ A. In particular, F is
unsatisfiable if and only if there is a resolution refutation of F.
With every resolution derivation π : F ` A we can associate a DAG Gπ , with the clauses in π labelling
the vertices and with edges from the assumption clauses to the resolvent for each application of the
resolution rule (3.2). There might be several different derivations of a clause C in π, but if so we can
label each occurrence of C with a timestamp when it was derived and keep track of which copy of
C is used where. A resolution derivation π is tree-like if any clause in the derivation is used at most
once as a premise in an application of the resolution rule, i. e., if Gπ is a tree. (We may make different
“time-stamped” vertex copies of the axiom clauses in order to make Gπ into a tree.)
The length L(π) of a resolution derivation π is the number of clauses in it, counted with repetitions.
We define the length of deriving a clause A from a formula F as L(F ` A) = minπ:F ` A {L(π)}, where the
minimum is taken over all resolution derivations of A. In particular, the length of refuting F by resolution
is denoted L(F ` ⊥).
The width W(C) of a clause C is |C|, i. e., the number of literals appearing in it. The width of a set
of clauses C is W(C) = maxC∈C {W(C)}. The width of deriving A from F by resolution is W(F ` A) =
minπ:F ` A {W(π)}, and the width of refuting F is denoted W(F ` ⊥).
We next define the measure of space. Following the exposition in [31], a proof can be seen as a Turing
machine computation, with a special read-only input tape from which the axioms can be downloaded
and a working memory where all derivation steps are made. The clause space of a resolution proof is
the maximum number of clauses that need to be kept in memory simultaneously during a verification of
the proof. The total space4 is the maximum total space needed, where also the width of the clauses is
taken into account. For the formal definitions, it is convenient to use an alternative definition of resolution
introduced in [2].
Definition 3.1 (Resolution). A clause configuration C is a set of clauses. A sequence of clause configu-
rations {C0 , . . . , Cτ } is a resolution derivation from a CNF formula F if C0 = 0/ and for all t ∈ [τ], Ct is
obtained from Ct−1 by one of the following rules:
4 We remark that there is some terminological confusion in the literature here. In some papers, this measure has been referred
to as “variable space” instead of “total space.” The terminology used here is due to Hertel and Urquhart (see [37]), and we feel
that although this naming convention is as of yet less well-established, it feels much more natural.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 485
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Axiom download Ct = Ct−1 ∪ {C} for some C ∈ F.
Erasure Ct = Ct−1 \ {C} for some C ∈ Ct−1 .
Inference Ct = Ct−1 ∪ {D} for some D inferred by resolution from C1 ,C2 ∈ Ct−1 .
A resolution derivation π : F ` A of a clause A from a formula F is a derivation {C0 , . . . , Cτ } such that
Cτ = {A}. A resolution refutation of F is a derivation of the empty clause ⊥ from F.
Definition 3.2 (Clause space [2, 12]). The clause space of a resolution derivation π = {C0 , . . . , Cτ }
is maxt∈[τ] {|Ct |}. The clause space of deriving the clause A from the formula F is Sp(F ` A) =
minπ:F ` A {Sp(π)}, and Sp(F ` ⊥) denotes the minimum clause space of any resolution refutation of F.
Definition 3.3 (Total space [2]). The total space of a clause configuration C is TotSp(C) = ∑C∈C W(C).
The total space of a resolution derivation {C0 , . . . , Cτ } is maxt∈[τ] {TotSp(Ct )}, and TotSp(F ` ⊥) is the
minimum total space of any resolution refutation of F.
In this paper, we will be almost exclusively interested in the clause space of general, unrestricted
resolution refutations. When we write simply “space” for brevity, we mean clause space in general
resolution.
3.2 Pebble games and pebbling contradictions
Pebble games were originally devised for studying programming languages and compiler construction,
but have later found a variety of applications in computational complexity theory. In connection with
resolution, pebble games have been used both to analyze resolution derivations with respect to how much
memory they consume (using the original definition of space in [31]) and to construct CNF formulas
which are hard for different variants of resolution in various respects (see for example [3, 14, 19, 21]).
An excellent survey of pebbling up to ca. 1980 is [51]. A second article, with more narrow focus but
covering some more recent developments, is the first author’s upcoming survey [48].
The black pebbling price of a DAG G captures the amount of memory, i. e., the number of registers,
required to perform the deterministic computation described by G. The space of a non-deterministic
computation is measured by the black-white pebbling price of G. We say that vertices of G with indegree 0
are sources and that vertices with outdegree 0 are sinks or targets. In the following, unless otherwise
stated we will assume that all DAGs under discussion have a unique sink, and this sink will always be
denoted z. The next definition is adapted from [27], though we use the established pebbling terminology
introduced by [39].
Definition 3.4 (Pebble game). Suppose that G is a DAG with sources S and a unique sink z. The black-
white pebble game on G is the following one-player game. At any point in the game, there are black
and white pebbles placed on some vertices of G, at most one pebble per vertex. A pebble configuration
is a pair of subsets P = (B,W ) of V (G), comprising the black-pebbled vertices B and white-pebbled
vertices W . The rules of the game are as follows:
1. If all immediate predecessors of an empty vertex v have pebbles on them, a black pebble may be
placed on v. In particular, a black pebble can always be placed on any vertex in S.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 486
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
2. A black pebble may be removed from any vertex at any time.
3. A white pebble may be placed on any empty vertex at any time.
4. If all immediate predecessors of a white-pebbled vertex v have pebbles on them, the white pebble
on v may be removed. In particular, a white pebble can always be removed from a source vertex.
A black-white pebbling from (B1 ,W1 ) to (B2 ,W2 ) in G is a sequence of pebble configurations
P = {P0 , . . . , Pτ } such that P0 = (B1 ,W1 ), Pτ = (B2 ,W2 ), and for all t ∈ [τ], Pt follows from Pt−1 by
one of the rules above. If (B1 ,W1 ) = (0, / 0),
/ we say that the pebbling is unconditional, otherwise it is
conditional.
The cost of a pebble configuration P = (B,W ) is cost(P) = |B ∪ W | and the cost of a pebbling P =
{P0 , . . . , Pτ } is max0≤t≤τ {cost(Pt )}. The black-white pebbling price of (B,W ), denoted BW-Peb(B,W ),
is the minimum cost of any unconditional pebbling reaching (B,W ).
A complete pebbling of G, also called a pebbling strategy for G, is an unconditional pebbling reaching
/ The black-white pebbling price of G, denoted BW-Peb(G), is the minimum cost of any complete
({z}, 0).
black-white pebbling of G.
A black pebbling is a pebbling using black pebbles only, i. e., having Wt = 0/ for all t. The (black)
pebbling price of G, denoted Peb(G), is the minimum cost of any complete black pebbling of G.
We think of the moves in a pebbling as occurring at integral time intervals t = 1, 2, . . . and talk about
the pebbling move “at time t” (which is the move resulting in configuration Pt ) or the moves “during the
time interval [t1 ,t2 ].”
The only pebblings we are really interested in are complete pebblings of G. However, when we prove
lower bounds for pebbling price it will sometimes be convenient to be able to reason in terms of partial
pebbling move sequences, i. e., conditional pebblings.
A pebbling contradiction defined on a DAG G encodes the pebble game on G by postulating the
sources to be true and the sink to be false, and specifying that truth propagates through the graph according
to the pebbling rules. The definition below is a generalization of formulas previously studied in [19, 53].
Definition 3.5 (Pebbling contradiction [17]). Suppose that G is a DAG with sources S, a unique sink z
and with all non-source vertices having indegree 2, and let d > 0 be an integer. Associate d distinct
variables x(v)1 , . . . , x(v)d with every vertex v ∈ V (G). The dth degree pebbling contradiction over G,
denoted PebdG , is the conjunction of the following clauses:
Wd
• i=1 x(s)i for all s ∈ S (source axioms),
• x(u)i ∨ x(v) j ∨ dl=1 x(w)l for all i, j ∈ [d] and all w ∈ V (G) \ S, where u, v are the two predecessors
W
of w (pebbling axioms).
• x(z)i for all i ∈ [d] (sink axioms or target axioms),
The formula PebdG is a (2+d)-CNF formula with O d 2 · |V (G)| clauses over d · |V (G)| variables.
An example pebbling contradiction is presented in Figure 2 on page 480.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 487
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
GO
\
v
v
G\ GMv ∪ GO
v
\
v
GM
Figure 5: Notation for sets of vertices in DAG G with respect to a vertex v.
4 A game for analyzing pebbling contradictions
We now start working on the proof of Theorem 1.1, which will require the rest of this paper. In this section
we present the modified pebble game that we will use to study the clause space of resolution refutations
of pebbling contradictions. We remark that the game has been somewhat simplified as compared to the
preliminary version [50] of this paper, incorporating some ideas from [15].
4.1 Some graph notation and definitions
We first present some notation and terminology that will be used in what follows. See Figure 5 for an
illustration of the next definition.
Definition 4.1 (Graph notation). We let succ(v) denote the immediate successors and pred(v) denote the
immediate predecessors of a vertex v in a DAG G. We will usually drop the prefix “immediate” so that
the terms “successor” and “predecessor” refer to an immediate successor or predecessor, respectively,
unless stated otherwise.
Taking the transitive closures of succ(·) and pred(·), we let GOv denote all vertices reachable from v
(vertices “above” v) and GMv denote all vertices from which v is reachable (vertices “below” v). We write
\v
GM and GO v to denote the corresponding sets with the vertex v itself removed.
\
If pred(v) = {u, w}, we say that u and w are siblings. If u 6∈ GMv and v 6∈ GMu , we say that u and v are
non-comparable vertices. Otherwise they are comparable.
For V a set of vertices, we let bot(V ) denote the bottom vertices of V , i. e., the subset of vertices
\
v
bot(V ) = {v ∈ V | V ∩ GM = 0},/ and we let top(V ) = {v ∈ V | V ∩ GO v = 0}
\ / denote the top vertices in V .
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 488
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
When reasoning about arbitrary vertices we will often use as a canonical example a vertex r with
assumed predecessors pred(r) = {p, q}.
Note that for a leaf v we have pred(v) = 0,/ and for the sink z of G we have succ(z) = 0. / Also note
v O
that GM and Gv are sets of vertices, not subgraphs. However, we will allow ourselves to overload the
notation and frequently use it for both the subgraph and its vertex set. In a similar fashion, as a rule
we will overload the notation for the graph G itself and its vertices, and usually write only G when we
mean V (G), and when this should be clear from context.
In this paper, we will focus on layered directed acyclic graphs. Let us give a formal definition of this
concept for completeness.
Definition 4.2 (Layered DAG). A layered DAG is a DAG whose vertices are partitioned into (nonempty)
sets of layers V0 ,V1 , . . . ,Vh on levels 0, 1, . . . , h, and whose edges run between consecutive layers. That is,
if (u, v) is a directed edge, then the level of u is L − 1 and the level of v is L for some L ∈ [h]. We say that
h is the height of the layered DAG.
Throughout this paper, we will assume that all source vertices in a layered DAG are located on the
bottom level 0. A family of layered DAGs that will be of particular interest to us are so-called pyramid
graphs, which are defined as follows.
Definition 4.3 (Pyramid graph). The pyramid graph Πh of height h is a layered DAG with h + 1 levels,
where there is one vertex on the highest level (the sink z), two vertices on the next level et cetera down to
h + 1 vertices at the lowest level 0. The ith vertex at level L has incoming edges from the ith and (i + 1)st
vertices at level L − 1.
We also need some notation for contiguous and non-contiguous topologically ordered sets of vertices
in a DAG.
Definition 4.4 (Paths and chains). We say that V is a (totally) ordered set of vertices in a DAG G, or a
chain, if all vertices in V are comparable (i. e., if for all u, v ∈ V , either u ∈ GMv or v ∈ GMu ). A path P is a
contiguous chain, i. e., such that succ(v) ∩ P 6= 0/ for all v ∈ P except the top vertex.
We write P : v w to denote a path starting in v and ending in w. A source path is a path that starts
at some source vertex of G. A path via w is a path such that w ∈ P. We will also say that P visits w.
For a chain V we write Pvia (V ) denote the set of all source paths that visit all vertices in V , or that
agree with V . Also, we write Pvia (V ) for the union of all vertices in paths P ∈ Pvia (V ).
S
4.2 Description of the blob-pebble game and formal definition
To prove a lower bound on the refutation space of pebbling contradictions, we want to interpret derivation
steps in terms of pebble placements and removals in the corresponding graph. In Section 2, we outlined
an intuitive correspondence between clauses and pebbles. The problem is that if we try to use this
correspondence, the pebble configurations that we get do not obey the rules of the black-white pebble
game. Therefore, we are forced to to change the pebbling rules. In this section, we present the modified
pebble game used for analyzing resolution derivations.
Our first modification of the pebble game is to alter the rule for white pebble removal so that a white
pebble can be removed from a vertex only when a black pebble is placed on that same vertex. This will
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 489
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
make the correspondence between pebblings and resolution derivations much more natural. Clearly, this
is only a minor adjustment, and it is easy to prove formally that it does not really change anything.
Our second, and far more substantial, modification of the pebble game is motivated by the fact that in
general, a resolution refutation a priori has no reason to follow our pebble game intuition. Since pebbles
are induced by clauses, if at some derivation step the refutation chooses to erase “the wrong clause”
from the point of view of the induced pebble configuration, this can lead to pebbles just disappearing.
Whatever our translation from clauses to pebbles is, a resolution proof that suddenly out of spite erases
practically all clauses must surely lead to practically all pebbles disappearing, if we want to maintain a
correspondence between clause space and pebbling cost. This is all in order for black pebbles, but if we
allow uncontrolled removal of white pebbles we cannot hope for any nontrivial lower bounds on pebbling
price (to see this, just white-pebble the two predecessors of the sink, then black-pebble the sink itself and
finally remove the white pebbles).
Our solution to this problem is to keep track of exactly which white pebbles have been used to get a
black pebble on a vertex. Loosely put, removing a white pebble from a vertex v without placing a black
pebble on the same vertex should be in order, provided that all black pebbles placed on vertices above v in
the DAG with the help of the white pebble on v are removed as well. We do the necessary bookkeeping by
defining subconfigurations of pebbles, each subconfiguration consisting of a black pebble together with
all the white pebbles this black pebble depends on, and requiring that if any pebble in a subconfiguration
is removed, then all other pebbles in this subconfiguration must be removed as well.
Another problem is that resolution derivation steps can be made that appear intuitively bad given
that we know that the end goal is to derive the empty clause, but where formally it appears hard to nail
down wherein this supposed badness lies. To analyze such apparently non-optimal derivation steps, we
introduce an inflation rule in which a black pebble can be inflated to a blob covering multiple vertices.
The way to think of this is that a black pebble on a vertex v corresponds to derived truth of v, whereas for
a blob pebble on V we only know that some vertex v ∈ V is true, but not which one.
We now present the formal definition of the concept used to “label” each black blob pebble with the
set of white pebbles (if any) this black pebble is dependent on. The intended meaning of the notation
[B]hW i is a black blob on B together with the white pebbles W below B with the help of which we have
been able to place the black blob on B. We refer to the structure [B]hW i grouping together a black blob B
and its associated white pebbles W as a blob subconfiguration, or just subconfiguration for short.
Definition 4.5 (Blob subconfiguration). For sets of vertices B,W in a DAG G, [B]hW i is a blob subcon-
figuration if B 6= 0/ and B ∩ W = 0.
/ We refer to B as a (single) black blob and to W as (a number of
= 0,
different) white pebbles supporting B. We also say that B is dependent on W . If W / B is independent.
Blobs B with |B| = 1 are said to be atomic. A set of blob subconfigurations S = [Bi ]hWi i | i = 1, . . . , m
together constitute a blob-pebbling configuration.
Since the definition of the game we will play with these blobs and pebbles is somewhat involved, let
us first try to give an intuitive description.
• There is one single rule corresponding to the two rules 1 and 3 for black and white pebble placement
in the black-white pebble game of Definition 3.4. This introduction rule says that we can place a
black pebble on any vertex v together with white pebbles on its predecessors (unless v is a source,
in which case no white pebbles are needed).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 490
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
• The analogy for rule 2 for black pebble removal in Definition 3.4 is a rule for “shrinking” black
blobs. A vertex v in a blob can be eliminated by merging two blob subconfigurations, provided that
there is both a black blob and a white pebble on v, and provided that the two black blobs involved
in this merger do not intersect the supporting white pebbles of one another in any other vertex
than v. Removing black pebbles in the black-white pebble game corresponds to shrinking atomic
black blobs.
• A black blob can be inflated to cover more vertices, as long as it does not collide with its own
supporting white vertices. Also, new supporting white pebbles can be added at an inflation move.
There is no analogy of this move in the usual black-white pebble game.
• The rule 4 for white pebble removal also corresponds to merging in the blob-pebble game, in the
sense that the white pebble used in the merger is eliminated as well.
• Other than that, individual white pebbles, and individual black vertices covered by blobs, can never
just disappear. If we want to remove a white pebble or parts of a black blob, we can do so only by
erasing the whole blob subconfiguration.
The formal definition follows. See Figure 6 for some examples of blob-pebbling moves.
Definition 4.6 (Blob-pebble game). Let G be a DAG with unique sink z. The blob-pebbling rules for
going from a blob-pebbling configuration S0 to a blob-pebbling configuration S on G are as follows:
Introduction S = S0 ∪ [v]hpred(v)i for any v ∈ V (G).
Merger S = S0 ∪ [B]hWi if there are [B1 ]hW1 i, [B2 ]hW2 i ∈ S0 such that
1. B1 ∩ W2 = 0,
/
2. |B2 ∩ W1 | = 1; let v∗ denote this unique element in B2 ∩ W1 ,
3. B = B1 ∪ (B2 \ {v∗ }) = (B1 ∪ B2 ) \ {v∗ }, and
4. W = (W1 \ {v∗ }) ∪ W2 = (W1 ∪ W2 ) \ {v∗ }.
We write [B]hWi = merge([B1 ]hW1 i, [B2 ]hW2 i) and refer to this as a merger on v∗ .
Inflation S = S0 ∪ [B]hWi if there is a [B0 ]hW 0 i ∈ S0 such that B ⊇ B0 and W ⊇ W 0 .
We say that the blob-pebbling configuration [B]hWi is derived from [B0 ]hW 0 i by inflation or that
[B0 ]hW 0 i is inflated to yield [B]hWi.
Erasure S = S0 \ [B]hWi for [B]hWi ∈ S0 .
A blob-pebbling move at time t from St−1 to St is either an introduction or any sequence of mergers,
inflations and erasures.
For
blob-pebbling configurations S0 and Sτ on G, a blob-pebbling from S0 to Sτ in G is a sequence
P = S0 , . . . , Sτ of blob-pebbling moves. The blob-pebbling P is unconditional if S0 = 0/ and
conditional
otherwise. A complete blob-pebbling of G is an unconditional pebbling P ending in Sτ = [z]h0i / for z
the unique sink of G.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 491
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
(a) Empty pyramid. (b) Introduction move.
(c) Two subconfigurations before merger. (d) The merged subconfiguration.
(e) Subconfiguration before inflation. (f) Subconfiguration after inflation.
Figure 6: Examples of moves in the blob-pebble game.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 492
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
4.3 Blob-Pebbling price
We have not yet defined what the price of a blob-pebbling is. The reason is that it is not a priori clear
what the “correct” definition of blob-pebbling price should be.
It should be pointed out that the blob-pebble game has no obvious intrinsic value—its function is
to serve as a tool to prove lower bounds on the resolution refutation space of pebbling contradictions.
The intended structure of our lower bound proof for resolution space is that we want look at resolution
refutations of pebbling contradictions, interpret them in terms of blob-pebblings on the underlying graphs,
and then translate lower bounds on the price of these blob-pebblings into lower bounds on the size of the
corresponding clause configurations. Therefore, we have two requirements for the blob-pebbling price
Blob-Peb(G):
1. It should be sufficiently high, i. e., sufficiently similar to standard black-white pebbling price to
enable us to prove good lower bounds on Blob-Peb(G), preferrably by making it possible to use
lower bound proof techniques for BW-Peb(G) to obtain analogous bounds for Blob-Peb(G).
2. It should also be sufficiently low, in the sense that it should take into consideration the way
subconfigurations are obtained from clauses in resolution derivations, so that lower bounds on
Blob-Peb(G) translate back to lower bounds on the size of the clause configurations.
Hence, when defining pebbling price in Definition 4.7 below, we should also have to have in mind the
coming Definition 5.2 saying how we will interpret clauses in terms of blobs and pebbles, so that these
two definitions together make it possible for us to get a lower bound on clause set size in terms of pebbling
cost.
For black pebbles, we could try to charge 1 for each distinct blob. But this will not work, since
then the second requirement above fails. For the translation of clauses to blobs and pebbles sketched in
Section 2.3 it is possible to construct clause configurations that correspond to an exponential number of
distinct black blobs measured in the clause set size. The other natural extreme seems to be to charge
only for mutually disjoint black blobs. But this is far too generous, and the first requirement above fails.
To get a trivial example of this, take any ordinary black pebbling of G and translate in into an (atomic)
blob-pebbling, but then change it so that each black pebble [v] is immediately inflated to [{v, z}] after
each introduction move. It is straightforward to verify that this would yield a pebbling of G in constant
cost. For white pebbles, the first idea might be to charge 1 for every white-pebbled vertex, just as in the
standard pebble game. On closer inspection, though, this turns out to lead to technical problems in the
proofs, and so this seems to be not quite what we need.
The definition presented below turns out to give us both of the desired properties above, and allows
us to prove an optimal bound. Namely, we define blob-pebbling price so as to charge 1 for each distinct
bottom vertex that is the unique bottom vertex of its black blob, and so as to charge for the subset of
supporting white pebbles W ∩ GMb in a subconfiguration [B]hWi that are located below all bottom vertices
bot(B) of its black blob B. Multiple distinct blobs with the same bottom vertex come for free, however,
as do blobs that do not have a unique bottom vertex. Also, any supporting white pebbles that are not
“completely below” its own blob in the sense described above are also free, although we still have to keep
track of them.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 493
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Definition 4.7 (Blob-pebbling price). For a blob subconfiguration [B]hWi, we define B([B]hWi) =
{bot(B)} to be a chargeable black vertex if |bot(B)| = 1 and set B([B]hWi) = 0/ otherwise. We say
that WM ([B]hWi) = W ∩ b∈bot(B) GMb are the chargeable white vertices. The chargeable vertices of
T
the subconfiguration [B]hWi are all vertices in the union B([B]hWi) ∪ WM ([B]hWi). This definition is
extended to blob-pebbling configurations S in the natural way by letting B(S) = [B]hWi∈S B([B]hWi)
S
and WM (S) = [B]hWi∈S WM ([B]hWi).
S
a blob-pebbling configuration S is cost(S) = B(S) ∪ W (S) , and the cost of a blob-
The cost of M
pebbling P = S0 , . . . , Sτ is cost(P) = maxt∈[τ] cost(St ) .
The blob-pebbling price of a blob subconfiguration [B]hWi, denoted Blob-Peb([B]hWi), is the minimal
cost of any unconditional blob-pebbling P = {S0 , . . . , Sτ } such that Sτ = [B]hWi . The blob-pebbling
price of a DAG G is Blob-Peb(G) = Blob-Peb([z]h0i), / i. e., the minimal cost of any complete blob-
pebbling of G.
We will also write W(S) to denote the set of all white-pebbled vertices in S, including non-chargeable
ones.
We stress again that we make no claim that Definition 4.7 is the “obviously correct” definition of
blob-pebbling price—it just happens to be a definition that works. In fact, there are other possible options,
some of which are arguably more natural but lead to more complicated proofs or slightly worse bounds.
To conclude this section, we just want to mention one alternative definition which seems slightly more
natural to us, which yields a slightly stronger pebbling price, and which might therefore be useful if
lower bounds on blob-pebbling price are to be extended from layered graphs to more general DAGs (as
discussed in Section 9).
Namely, for B1 , . . . , Bm any sets of vertices, let us say that a set of distinguished representatives for
B1 , . . . , Bm is a set R = {b1 , . . . , bm } where bi ∈ Bi \ j<i B j for all i ∈ [m]. Note that in general, such
S
sets of distinguished representatives need not exist, but we can always find a partial set of distinguished
representatives for B1 , . . . , Bm , which we define to be a set of distinguished representatives for some
(ordered) subset Bi1 , . . . , Bis of the vertex sets. Now we can define the cost of a blob-pebbling configuration
S to be
cost(S) = max R ∪ WM (S)
(4.1)
R
where the maximum is taken over all partial sets of distinguished representatives R for the black blobs in
S.
The proof of Theorem 6.5, which says that the clause space of a resolution refutation is lower bounded
by the cost of the pebbling it induces, can be adapted to work for this definition if one proves first a
lower bound for black blobs only and then a second lower bound for white pebbles only, and finally
combine them in the obvious way by taking the maximum of the two bounds. Unfortunately, this loses a
constant factor of 2, and for reasons explained in Section 9 we are interested in getting exactly the right
multiplicative constants in this part of our argument. Therefore, in this paper we decided to stick with
Definition 4.7 instead.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 494
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
5 Resolution derivations induce blob-pebblings
In this section, we show how resolution refutations of pebbling contradictions can be translated to
blob-pebblings (as described in Definition 4.6) of the corresponding DAGs. For simplicity, in the current
section, as well as in the next one, we will write v1 , v2 , . . . , vd instead of x(v)1 , x(v)2 , . . . , x(v)d for the d
variables associated with v in a dth degree pebbling contradiction. That is, in Sections 5 and 6 small
letters with subscripts will denote variables in propositional logic only and nothing else.
It turns out that for technical reasons, it is convenient to ignore the target axioms z1 , . . . , zd in a
pebbling contradiction and focus on resolution derivations of dl=1 zl from
W
the rest of the formula rather
d d d
than resolution refutations of all of PebG . Let us write *PebG = PebG \ z1 , . . . , zd to denote the pebbling
formula over G with the target axioms in the pebbling contradiction removed. The next lemma is the
formal statement saying that we may just as well study derivations of dl=1 zl from *PebdG instead of
W
refutations of PebdG .
Wd
Lemma 5.1. For any DAG G with sink z, it holds that Sp(PebdG ` ⊥) = Sp(*PebdG ` l=1 zl ).
Proof. From any resolution derivation π ∗ : *PebdG ` dl=1 zl , we can obtain a resolution refutation of PebdG
W
from π ∗ in the same space by resolving the final clause dl=1 zl with all sink axioms zl , l = 1, . . . , d, one
W
by one in space 3.
In the other direction, for π : PebdG ` ⊥ we can extract a derivation of dl=1 zl in at most the same space
W
by simply omitting all downloads of and resolution steps on zl in π, leaving the literals zl in the clauses.
Instead of the final empty clause ⊥ we get some clause D ⊆ dl=1 zl , and since *PebdG 2 D $ dl=1 zl and
W W
Wd
resolution is sound, we have D = l=1 zl .
In view of Lemma 5.1, from now on we will only consider resolution derivations from *PebdG and try
to convert clause configurations in such derivations into sets of blob subconfigurations.
To avoid cluttering the notation with an excessive amount of brackets, we will sometimes use sloppy
notation for sets. We will allow ourselves to omit curly brackets around singleton sets when this is clear
from context, writing e. g., V ∪ v instead of V ∪ {v} and [B ∪ b]hW ∪ wi instead of [B ∪ {b}]hW ∪ {w}i.
Also, we will sometimes omit the curly brackets around sets of vertices in black blobs and write, e. g.,
[u, v] instead of [{u, v}].
5.1 Definition of induced configurations and theorem statement
If r is a non-source vertex with pred(r) = {p, q}, we say that the axioms for r in *PebdG is the set
Axd (r) = pi ∨ q j ∨ dl=1 rl | i, j ∈ [d]
W
(5.1)
Wd
and if r is a source, we define Axd (r) = i=1 ri . For V a set of vertices in G, we let Axd (V ) =
Ax (v) | v ∈ V . Note that with this notation, we have *PebdG = Axd (v) | v ∈ V (G) . For brevity, we
d
introduce the shorthand notation
And+(V ) =
Wd
i=1 vi | v ∈ V , (5.2a)
Or+(V ) =
W Wd
v∈V i=1 vi . (5.2b)
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 495
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
The reader can think of And+(V ) as “truth of all vertices in V ” and Or+(V ) as “truth of some vertex in V .”
We say that a set of clauses C implies a clause D minimally if C D but for all C0 $ C it holds that
0
C 2 D. If C ⊥ minimally, C is said to be minimally unsatisfiable. We say that C implies a clause D
maximally if C D but for all D0 $ D it holds that C 2 D0 . To define our translation of clauses to blob
subconfigurations, we use implications that are in a sense both minimal and maximal.
Definition 5.2 (Induced blob subconfiguration). Let G be a DAG and C a clause configuration derived
from *PebdG . Then C induces the blob subconfiguration [B]hWi if there is a clause set D ⊆ C such that
D ∪ And+(W ) Or+(B) (5.3a)
but for which it holds for all strict subsets D0 $ D, W 0 $ W and B0 $ B that
D0 ∪ And+(W ) 2 Or+(B) , (5.3b)
+ 0 +
D ∪ And (W ) 2 Or (B) , and (5.3c)
+ + 0
D ∪ And (W ) 2 Or (B ) . (5.3d)
We write S(C) to denote the set of all blob subconfigurations induced by C. To save space, when all
conditions (5.3a)–(5.3d) hold, we write
D ∪ And+(W ) B Or+(B) (5.4)
and refer to this as precise implication or say that the clause set D ∪ And+(W ) implies the clause Or+(B)
precisely. Also, we say that the precise implication D ∪ And+(W ) B Or+(B) witnesses the induced blob
subconfiguration [B]hWi.
Let us see that this definition agrees with the intuition presented in Section 2.3. An atomic black
pebble on a single vertex v corresponds, as promised, to the fact that di=1 vi is implied by the current
W
set of clauses. A black blob on V without supporting white pebbles is induced precisely when the
disjunction Or+(V ) = v∈V di=1 vi of the corresponding clauses follow from the clauses in memory, but
W W
no disjunction over a strict subset of vertices V 0 $ V is implied. Finally, the supporting white pebbles just
indicate that if we indeed had the information corresponding to black pebbles on these vertices, the clause
corresponding to the supported black blob could be derived. Remember that our cost measure does not
take into account the size of blobs. This is natural since we are interested in clause space, and since large
blobs, in an intuitive sense, corresponds to large (i. e., wide) clauses rather than many clauses.
We are now ready to state the main result of this section, which says that if we apply the translation
of clauses to blobs and pebbles in Definition 5.2 on all the clause configurations in a resolution derivation
of dl=1 zl from *PebdG , then we obtain essentially a legal blob-pebbling of G.
W
Wd d
Theorem 5.3. Let π = C0 , . . . , Cτ be a resolution derivation of i=1 zi from *PebG for a DAG G.
Then the induced blob-pebbling configurations S(C0 ), . . . , S(Cτ ) form the “backbone” of a complete
blob-pebbling P of G in the sense that:
• S(C0 ) = 0,
/
• S(Cτ ) = {[z]h0i},
/ and
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 496
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
• for every t ∈ [τ], the transition S(Ct−1 ) S(Ct ) can be accomplished in accordance with the
blob-pebbling rules in cost max cost(S(Ct−1 )), cost(S(Ct )) + O(1).
π : *PebG ` i=1 zi we can associate a complete blob-pebbling Pπ of G
d dW
In particular, to any derivation
such that cost(Pπ ) ≤ maxC∈π cost(S(C)) + O(1).
We prove the theorem by forward induction over the derivation π. By the pebbling rules in Def-
inition 4.6, any subconfiguration [B]hWi may be erased freely at any time. Consequently, we need
not worry about subconfigurations disappearing during the transition from Ct−1 to Ct . What we do
need to check, though, is that no subconfiguration [B]hWi appears inexplicably in S(Ct ) as a result of a
derivation step Ct−1 Ct , but that we can always derive any [B]hWi ∈ S(Ct ) \ S(Ct−1 ) from S(Ct−1 ) by
the blob-pebbling rules. Also, when several pebbling moves are needed to get from S(Ct ) to S(Ct−1 ),
we need to check that these intermediate moves do not affect the pebbling cost by more than an additive
constant.
The proof boils down to a case analysis of the different possibilities for the derivation step to get
from Ct−1 to Ct . Since the analysis is quite lengthy, we divide it into subsections. But first of all we need
some auxiliary technical lemmas.
5.2 Some technical lemmas
The next three lemmas are not hard, but will prove quite useful. We present the proofs for completeness.
Lemma 5.4. Let C be a set of clauses and D a clause such that C D minimally and a ∈ Lit(C) but
a 6∈ Lit(C). Then a ∈ Lit(D).
Proof. Suppose not. Let C1 = {C ∈ C | a ∈ Lit(C)} and C2 = C \ C1 . Since C2 2 D there is a truth value
assignment α such that α(C2 ) = 1 and α(D) = 0. Note that α(a) = 0, since otherwise α(C1 ) = 1 which
would contradict C1 ∪ C2 = C D. It follows that a ∈ / Lit(D). Flip a to true and denote the resulting
truth value assignment by α a=1 . By construction α a=1 (C1 ) = 1 and C2 and D are not affected since
{a, a} ∩ Lit(C2 ) ∪ Lit(D) = 0, / so α a=1 (C) = 1 and α a=1 (D) = 0. Contradiction.
Lemma 5.5. Suppose that C, D are clauses and C is a set of clauses. Then C ∪ C D if and only if
C a ∨ D for all a ∈ Lit(C).
Proof. Assume that C ∪ C D and consider any assignment α such that α(C) = 1 and α(D) = 0 (if
there is no such α, then C D ⊆ a ∨ D). Such an α must set C to false, i. e., all a to true. Conversely,
if C a ∨ D for all a ∈ Lit(C) and α is such that α(C) = α(C) = 1, it must hold that α(D) = 1, since
otherwise α(a ∨ D) = 0 for some literal a ∈ Lit(C) satisfied by α.
Lemma 5.6. Suppose that C D minimally. Then no literal from D can occur negated in C, i. e., it holds
that {a | a ∈ Lit(D)} ∩ Lit(C) = 0.
/
Proof. Suppose not. Let C1 = {C ∈ C | ∃a such that a ∈ Lit(C) and a ∈ Lit(D)} and let C2 = C \ C1 .
Since C2 2 D there is an α such that α(C2 ) = 1 and α(D) = 0. But then α(C1 ) = 1, since every C ∈ C1
contains a negated literal a from D, and these literals are all set to true by α. Contradiction.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 497
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
We also need the following key technical lemma connecting implication with inflation moves.
Lemma 5.7. Let C be a clause set derived from *PebdG . Suppose that B,W ⊆ G, B ∩ W = 0, / are vertex
sets such that C ∪ And+(W ) Or+(B). Then the blob subconfiguration [B]hWi is derivable by inflation
from some [B0 ]hW 0 i ∈ S(C).
Proof. Pick D ⊆ C, W 0 ⊆ W and B0 ⊆ B minimal such that D ∪ And+(W 0 ) Or+(B0 ). Then D ∪
And+(W 0 ) B Or+(B0 ) by definition. Note, furthermore, that B0 6= 0/ since the clause set on the left-hand
side must be non-contradictory. Also, since B0 ∩ W 0 ⊆ B ∩ W = 0/ we must have D 6= 0, / because by
Lemma 5.4 it cannot be the case that And+(W 0 ) Or+(B0 ). This means that C induces [B0 ]hW 0 i, and
clearly [B0 ]hW 0 i can be inflated to [B]hWi, from which the lemma follows.
We now start the case analysis in the proof of Theorem 5.3 for the different possible derivation steps
in a resolution derivation.
5.3 Erasure
Suppose that Ct = Ct−1 \ {C} for C ∈ Ct−1 . It is easy to see that the only possible outcome of erasing
clauses is that blob subconfigurations disappear. We note for future reference that this implies that the
blob-pebbling cost decreases monotonically when going from S(Ct−1 ) to S(Ct ).
5.4 Inference
Suppose that Ct = Ct−1 ∪ {C} for some clause C derived from Ct−1 . No blob subconfigurations can
disappear at an inference step since Ct−1 ⊆ Ct . Suppose that [B]hWi is a new subconfiguration at time t
witnessed by D ∪ {C} ∪ And+(W ) B Or+(B) for some D ⊆ Ct−1 . Since C is derived from Ct−1 , we have
Ct−1 C. Thus, it holds that Ct−1 ∪ And+(W ) Or+(B) and Lemma 5.7 tells us that [B]hWi is derivable
by inflation from S(Ct−1 ).
Since no subconfiguration disappears, the pebbling cost increases monotonically when going from
S(Ct−1 ) to S(Ct ) for an inference step, which is again noted for future reference.
5.5 Axiom download
This is the interesting case. Assume that a new blob subconfiguration [B]hWi is induced at time t as
the result of a download of an axiom C ∈ Axd (r). Then C must be one of the clauses inducing the
subconfiguration, and we get that there is a clause set D ⊆ Ct−1 such that
D ∪ {C} ∪ And+(W ) B Or+(B) . (5.5)
Observe that if we have Ct−1 ∪ And+(W ) Or+(B) at time t − 1, then according to Lemma 5.7 [B]hWi
is derivable by inflation from S(Ct−1 ) and we are done. Therefore, it what follows we assume the
non-implication
Ct−1 ∪ And+(W ) 2 Or+(B) . (5.6)
Our intuition is that download of an axiom clause C ∈ Axd (r) in the resolution derivation should
correspond to an introduction of [r]hpred(r)i in the induced blob-pebbling. We want to prove that
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 498
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
any other blob subconfiguration [B]hWi in S(Ct ) \ S(Ct ) can be obtained by the pebbling rules from
S(Ct−1 ) ∪ [r]hpred(r)i. Also, we need to prove that the pebbling moves needed to go from S(Ct−1 ) to
the new configuration
S(Ct ) do not increase the blob-pebbling cost by more than an additive constant
compared to max cost(S(Ct−1 )), cost(S(Ct )) = cost(S(Ct )).
As a warm-up, let us consider the case when r is a source, i. e., pred(r) = 0/ and C = di=1 ri . We
W
make a case analysis depending on whether r ∈ B in (5.5) or not.
1. r ∈ B: It clearly holds that
∪ And+(0)
Wd
i=1 ri / B Or+(r) (5.7)
(the left- and right-hand sides are identical), and since the implication in (5.5) is precise, for any B
such that r ∈ B we must have B = {r} and W = 0. / Hence [B]hWi = [r]h0i./ This corresponds to an
introduction for the source r at time t, which certainly is a legal blob-pebbling move.
2. r ∈
/ B: In this case we can rewrite (5.5) as
D ∪ And+(W ∪ r) B Or+(B) (5.8)
for (W ∪ r) ∩ B = 0,/ which shows that [B]hW ∪ ri ∈ S(Ct−1 ). Then [B]hWi can be derived by first
/ and then a merger of this subconfiguration with [B]hW ∪ ri on r.
an introduction of [r]h0i
We see that when r is a source, we can get from S(Ct−1 ) to S(Ct ) first by an introduction of [r]h0i
/ and
then possibly by some mergers on r and some erasures all combined into one pebbling move. This implies
that the pebbling cost increases monotonically.
The case when r is a non-source is a bit more involved, but the general idea is the same. Suppose
that pred(r) = {p, q}. Then the downloaded axiom can be written C = pi ∨ q j ∨ dl=1 rl (for some fixed
W
indices i and j) and (5.5) becomes
Wd +
D ∪ {pi ∨ q j ∨ l=1 rl } ∪ And (W ) B Or+(B) , (5.9)
where we recall that by definition, we have B ∩ W = 0.
/ Observe that it must hold that
{p, q} ∩ B = 0/ , (5.10)
since if, say, q ∈ B, we could apply Lemma 5.5 on pi ∨ q j ∨ dl=1 rl to derive that the implication
W
+ + + +
C t−1 ∪ And (W ) Or (B ∪ q) = Or (B) holds, contradicting (5.6). Also, the fact that And (r) =
d d
W
l=1 rl pi ∨ q j ∨ l=1 rl implies that
W
r∈/W (5.11)
since otherwise And+(W ) pi ∨ q j ∨ dl=1 rl = C and we would again have a contradiction to (5.6).
W
As in the case when r was a source vertex, the induction step is by a case analysis depending on
whether or not r ∈ B in the implication (5.9), which, as we recall, is (5.5) with added information about
exactly what the downloaded axiom clause C looks like.
1. r ∈ B: We split this case into subcases depending on whether p, q ∈ W or not. By the symmetry of
p and q, we have the following three possibilities to consider:
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 499
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
(a) {p, q} ⊆ W ,
(b) p ∈ W , q ∈
/ W,
(c) {p, q} ∩ W = 0.
/
We analyze these cases in order.
(a) {p, q} ⊆ W : This is the easiest case. Since by assumption r ∈ B and {p, q} ⊆ W , the sub-
configuration [B]hWi ∈ S(Ct ) can be derived by an introduction of [r]hp, qi followed by an
inflation of [r]hp, qi to [B ∪ r]hW ∪ {p, q}i = [B]hW i.
(b) p ∈ W , q ∈
/ W : In this case [r]hp, qi cannot be inflated to [B]hWi, since q ∈/ W . We need to
find some way to eliminate the white pebble on q.
To do this, first apply Lemma 5.5 on q j ∈ Lit pi ∨ q j ∨ dl=1 rl in (5.9) to get
W
D ∪ And+(W ) Or+(B ∪ q) . (5.12)
Then, observing that (B ∪ q) ∩ W = 0/ since q ∈
/ W by assumption, use Lemma 5.7 to find
D0 ⊆ D, Bq ⊆ B, and Wq ⊆ W such that
D0 ∪ And+(Wq ) B Or+(Bq ∪ q) (5.13)
(where we note that the vertex q cannot disappear from the right-hand side because of the
non-implication (5.6)).
In this way, we have found a subconfiguration [Bq ∪ q]hWq i ∈ S(Ct−1 ) with q covered by a
black blob. Using this subconfiguration, we can derive [B]hWi as follows:
• introduce [r]hp, qi,
• merge [r]hp, qi and [Bq ∪ q]hWq i on q to get [Bq ∪ r]hWq ∪ pi,
• inflate [Bq ∪ r]hWq ∪ pi to [Bq ∪ r ∪ B]hWq ∪ p ∪ W i = [B]hWi, and
• erase [Bq ∪ r]hWq ∪ pi and possibly also [r]hp, qi.
In the inflation step, we used that r ∈ B and p ∈ W by assumption and that Bq ⊆ B and Wq ⊆ W
by construction. Also note that the merger is correct since r ∈
/ W ⊇ Wq as noted in (5.11) and
(Bq ∪ q) ∩ {p, q} ⊆ (B ∪ q) ∩ {p, q} = q as noted in (5.10).
(c) {p, q} ∩ W = 0:/ Now both p and q have to be eliminated if we are to use [r]hp, qi to derive
[B]hWi. As in the previous case 1b, we can use Lemma 5.5 (twice) to get
D ∪ And+(W ) Or+(B ∪ p) ∧ Or+(B ∪ q) (5.14)
and then appeal to Lemma 5.7 to find [B p ∪ p]hWp i, [Bq ∪ q]hWq i ∈ S(Ct−1 ) with B p ∪ Bq ⊆ B
and Wp ∪ Wq ⊆ W . Using these subconfigurations, we can perform a pebbling to get [B]hWi
as follows:
• introduce [r]hp, qi,
• merge [r]hp, qi with [Bq ∪ q]hWq i on q to get [Bq ∪ r]hWq ∪ pi,
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 500
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
• continue by merging [Bq ∪ r]hWq ∪ pi with [B p ∪ p]hWp i on p, resulting in the subcon-
figuration [B p ∪ Bq ∪ r]hWp ∪ Wq i,
• finally inflate [B p ∪ Bq ∪ r]hWp ∪ Wq i to [B]hWi and erase the auxiliary subconfigura-
tions used along the way.
In this final inflation, we used for the black blob that B p ∪ Bq ⊆ B by construction and r ∈ B
by assumption, and for the white pebbles that Wp ∪ Wq ⊆ W by construction. Also, we have
to check that all mergers are legal, but this follows from (5.10) and (5.11) and from how the
sets Bq , Wq , Br , Wr were constructed.
This concludes the analysis for the case r ∈ B for a non-source vertex r.
2. r ∈
/ B: This case is quite similar to the previous case r ∈ B. Here also we make a subcase analysis
depending on whether |pred(r) ∩ W | is equal to 2, 1 or 0.
Before we do this, though, we show that there is a particular subconfiguration in S(Ct−1 ) that will
be useful for us. Since And+(r) pi ∨ q j ∨ dl=1 rl , it follows from (5.9) that
W
D ∪ And+(W ∪ r) Or+(B) , (5.15)
and since B ∩ (W ∪ r) = 0/ (remember that we are now assuming r ∈
/ B), we can use Lemma 5.7 to
find a subconfiguration
[Br ]hWr ∪ ri ∈ S(Ct−1 ) , Br ⊆ B, Wr ⊆ W , (5.16)
which will play an important role in the pebblings below.
(a) {p, q} ⊆ W : To derive the subconfiguration [B]hWi from S(Ct−1 ) in this case, introduce
[r]hp, qi and merge with the subconfiguration [Br ]hWr ∪ ri ∈ S(Ct−1 ) in (5.16) to obtain
[Br ]hWr ∪ {p, q}i. This merger is in accordance with the pebbling rules since Br ∩ {p, q} ⊆
B ∩ {p, q} = 0/ according to (5.10). Then inflate [Br ]hWr ∪ {p, q}i to the subconfiguration
[Br ∪ B]hWr ∪ {p, q} ∪ W i = [B]hWi.
/ W : As in case 1b, Lemma 5.5 says that D ∪ And+(W ) Or+(B ∪ q), and since
(b) p ∈ W , q ∈
(B ∪ q) ∩ W = 0/ holds by assumption we can apply Lemma 5.7 to find a subconfiguration
[Bq ∪ q]hWq i ∈ S(Ct−1 ) as in (5.13) such that Bq ⊆ B, Wq ⊆ W . Now do the following
sequence of pebbling steps:
• introduce [r]hp, qi,
• merge [r]hp, qi with [Bq ∪ q]hWq i on q to get [Bq ∪ r]hWq ∪ pi,
• merge [Bq ∪ r]hWq ∪ pi with the subconfiguration [Br ]hWr ∪ ri ∈ S(Ct−1 ) in (5.16) on r
to get [Bq ∪ Br ]hWq ∪ p ∪ Wr i,
• finally inflate [Bq ∪ Br ]hWq ∪ p ∪ Wr i to [B]hWi and then do the necessary erasures of
auxiliary subconfigurations.
(c) {p, q} ∩ W = 0: / As in case 1c, appeal to Lemmas 5.5 and 5.7 to find subconfigurations
[B p ∪ p]hWp i, [Bq ∪ q]hWq i ∈ S(Ct−1 ) with B p ∪ Bq ⊆ B and Wp ∪ Wq ⊆ W . Using these sub-
configurations as well as [Br ]hWr ∪ ri ∈ S(Ct−1 ) in (5.16), we can derive [B]hWi as follows:
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 501
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
• introduce [r]hp, qi,
• merge [r]hp, qi with [Bq ∪ q]hWq i on the vertex q to derive [Bq ∪ r]hWq ∪ pi,
• merge [Bq ∪ r]hWq ∪ pi with [B p ∪ p]hWp i on the vertex p to derive the subconfiguration
[B p ∪ Bq ∪ r]hWp ∪ Wq i,
• merge [B p ∪ Bq ∪ r]hWp ∪ Wq i with [Br ]hWr ∪ ri on r resulting in the subconfiguration
[B p ∪ Bq ∪ Br ]hWp ∪ Wq ∪ Wr i,
• conclude by inflating [B p ∪ Bq ∪ Br ]hWp ∪ Wq ∪ Wr i to [B]hWi and erasing auxiliary
subconfigurations as needed.
Double-checking the set intersections and inclusions shows that all these pebbling steps are
legal.
This concludes the analysis for the case r ∈
/ B.
Summing up, to make the transition from S(Ct−1 ) to S(Ct ) in the axiom download case, we can
perform the following sequence of moves (in order):
1. Introduce [r]hpred(r)i.
2. Perform zero or more mergers of [r]hpred(r)i with subconfigurations in S(Ct−1 ) on some subset of
the vertices {r} ∪ pred(r).
3. Make zero or more inflations of the new subconfigurations resulting from the introduction and
mergers in steps 1 and 2.
4. Erase all intermediate subconfigurations derived in steps 1 and 2 and used in step 3 but not present
in S(Ct ).
We need to show that the maximum cost during all of these intermediate pebbling moves is bounded in
terms of cost(S(Ct−1 )) and cost(S(Ct )). But this is immediate from the definition. Note that step 1 is
one pebbling move and that the sequence of steps 2–4 counts as one move. This latter move ends in the
blob-pebbling configuration S(Ct ) with cost(S(Ct )) ≥ cost(S(Ct−1 )). The only thing that can happen in
the intermediate move is that [r]hpred(r)i is introduced and then later erased, but if so this is an extra cost
shows that the intermediate cost in the pebbling moves to get from S(Ct−1 ) to S(Ct ) is
of at most 3. This
kept below max cost(S(Ct−1 )), cost(S(Ct )) + 3 which is what we need.
5.6 Wrapping up the proof of Theorem 5.3
To finish the proof, let us fix an arbitrary resolution derivation π = {C0 , . . . , Cτ } of di=1 zi from *PebdG .
W
The induction hypothesis is vacuously true at time 0, since for C0 = 0/ we clearly must have S(C0 ) = 0. /
(To argue this formally, notethat we require B ∩ W = 0/ and use Lemma 5.4.) At time τ, the only subcon-
Wd
figuration induced by Cτ = i=1 zi is S(Cτ ) = {[z]h0i}.
/ Finally, we have proven in the induction step
that for all t ∈ [τ], the blob-pebbling
moves needed to accomplish the transition S(Ct−1 ) S(Ct ) can be
performed in cost max cost(S(Ct−1 )), cost(S(Ct )) + 3. Theorem 5.3 follows by induction.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 502
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
6 Induced blob configurations measure clause set size
In this section, we prove that if a set of clauses C induces a blob-pebbling configuration S(C) according
to Definition 5.2, then the cost of S(C) as specified in Definition 4.7 is at most |C|. That is, the cost of an
induced blob-pebbling configuration provides a lower bound on the size of the set of clauses inducing it.
This is Theorem 6.5 below.
Observe that we cannot expect a proof of this fact to work regardless of the pebbling degree d.
The induced blob-pebbling in Section 5 makes no assumptions about d, but for first-degree pebbling
contradictions we know from [12] that Sp(*Peb1G ` z1 ) = Sp(Peb1G ` ⊥) = O(1). Provided d ≥ 2, though,
we show that one has to pay at least N clauses to get an induced blob-pebbling configuration of cost N.
We introduce some notation to simplify the proofs in what follows. Let us define Varsd (u) =
{u1 , . . . , ud }. We say that a vertex u is represented in a clause C derived from *PebdG , or that C mentions u,
if Varsd (u) ∩ Vars(C) 6= 0. / We write
V (C) = u ∈ V (G) Varsd (u) ∩ Vars(C) 6= 0/
(6.1)
to denote all vertices represented in C. We will also refer to V (C) as the set of vertices mentioned by C.
This notation is extended to sets of clauses by taking unions. Furthermore, we write
CJUK = {C ∈ C | V (C) ∩ U 6= 0}
/ (6.2)
to denote the subset of all clauses in C mentioning vertices in a vertex set U.
We now show some technical results about CNF formulas that will come in handy in the proof of
Theorem 6.5. Intuitively, we will use Lemma 6.1 below together with Lemma 5.4 on page 497 to argue
that if a clause set C induces a lot of subconfigurations, then there must be a lot of variable occurrences in
C for variables corresponding to these vertices. Note, however, that this alone will not be enough, since
this will be true also for pebbling degree d = 1.
Lemma 6.1. Suppose for a set of clauses C and clauses D1 and D2 with Vars(D1 ) ∩ Vars(D2 ) = 0/ that
C D1 ∨ D2 but C 2 D2 . Then there is a literal a ∈ Lit(C) ∩ Lit(D1 ).
Proof. Pick a truth value assignment α such that α(C) = 1 but α(D2 ) = 0. Since C D, we must have
α(D1 ) = 1. Let α 0 be the same assignment except that all satisfied literals in D1 are flipped to false (which
is possible since they are all strictly distinct by assumption). Then α 0 (D1 ∨ D2 ) = 0 forces α 0 (C) = 0, so
the flip must have falsified some previously satisfied clause in C.
The fact that a minimally unsatisfiable CNF formula must have more clauses than variables seems to
have been proven independently a number of times (see, e. g., [1, 6, 23, 43]). We will need the following
formulation of this result, relating subsets of variables in a minimally implicating CNF formula and the
clauses containing variables from these subsets.
Theorem 6.2. Suppose that F is CNF formula that implies a clause D minimally. For any subset of
variables V of F, let FV = {C ∈ F | Vars(C) ∩ V 6= 0} / denote the set of clauses containing variables
from V . Then if V ⊆ Vars(F) \ Vars(D), it holds that |FV | > |V |. In particular, if F is a minimally
unsatisfiable CNF formula, we have |FV | > |V | for all V ⊆ Vars(F).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 503
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Proof. The proof is by induction over V ⊆ Vars(F) \ Vars(D). The base case is easy. If |V | = 1, then
|FV | ≥ 2, since any x ∈ V must occur both unnegated and negated in F by Lemma 5.4.
The inductive step just generalizes the proof of Lemma 5.4. Suppose that |FV 0 | > |V 0 | for all strict
subsets V 0 $ V ⊆ Vars(F) \ Vars(D) and consider V . Since FV 0 ⊆ FV if V 0 ⊆ V , choosing any V 0 of size
|V | − 1 we see that |FV | ≥ |FV 0 | ≥ |V 0 | + 1 = |V |.
If |FV | > |V | there is nothing to prove, so assume that |FV | = |V |. Consider the bipartite graph with
the variables V and the clauses in FV as vertices, and edges between variables and clauses for all variable
occurrences. Since for all V 0 ⊆ V the set of neighbours N(V 0 ) = FV 0 ⊆ FV satisfies |N(V 0 )| ≥ |V 0 |, by
Hall’s marriage theorem there is a perfect matching between V and FV . Use this matching to satisfy FV
assigning values to variables in V only.
The clauses in F 0 = F \ FV are not affected by this partial truth value assignment, since they do not
contain any occurrences of variables in V . Furthermore, by the minimality of F it must hold that F 0 can
be satisfied and D falsified simultaneously by assigning values to variables in Vars(F 0 ) \V .
The two partial truth value assignments above can be combined to an assignment that satisfies all of
F but falsifies D, which is a contradiction. Thus |FV | > |V |, and the theorem follows.
Continuing our intuitive argument, given that Lemmas 5.4 and 6.1 tell us that many induced subcon-
figurations imply the presence of many variables in C, we will use Theorem 6.2 to demonstrate that a lot
of different variable occurrences will have to translate into a lot of different clauses provided that the
pebbling degree d is at least 2. Before we prove this formally, let us try to provide some
W intuition for
why it should be true by studying two special cases. Recall the notation And+(V ) = i∈[d] vi v ∈ V
+ W W
and Or (V ) = v∈V i∈[d] vi from Section 5.
Example 6.3. Suppose that C is a clause set derived from *PebdG that induces N independent black blobs
B1 , . . . , BN that are pairwise disjoint, i. e., Bi ∩ B j = 0/ if i 6= j. Then the implications
C Or+(Bi ) (6.3)
hold for i = 1, . . . , N. Remember that since *PebdG is non-contradictory, so is C.
It is clear that a non-contradictory clause set satisfying (6.3) for all i is quite simply the set
C = Or+(Bi ) i = 1, . . . N
(6.4)
consisting precisely of the clauses implied. Also, it seems plausible that this is the best one can do.
Informally, if there would be strictly fewer clauses than N, some clause would have to mix variables from
different blobs Bi and B j . But then Lemma 5.4 says that there will be extra clauses needed to “neutralize”
the literals from B j in the implication C Or+(Bi ) and vice versa, so that the total number of clauses
would have to be strictly greater than N.
As it turns out, the proof that |C| ≥ N when C induces N pairwise disjoint and independent black
blobs is very easy. Suppose on the contrary that (6.3) holds for i = 1, . . . , N but that |C| < N. Let α be a
satisfying assignment for C. Choose α 0 ⊆ α to be any minimal partial truth value assignment fixing C to
true. Then for the size of the domain of α 0 we have |Dom(α 0 )| < N, since at most one distinct literal is
needed for every clause C ∈ C to fix it to true. This means that there is some Bi such that α 0 does not set
any variables in Varsd (Bi ). Consequently α 0 can be extended to an assignment α 00 setting C to true but
Or+(Bi ) to false, which is a contradiction.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 504
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
We remark that the above argument works for any pebbling degree including d = 1. Intuitively, this
means that one can charge for black blobs even in the case of first degree pebbling formulas.
Example 6.4. Suppose that the clause set C induces an blob subconfiguration [B]hWi with W 6= 0,
/ and
let us assume for simplicity that C is minimal so that the implication
C ∪ And+(W ) Or+(B) (6.5)
holds. We claim that |C| ≥ |W | + 1 provided that d > 1.
Since by definition B ∩ W = 0/ we have Vars(Or+(B)) ∩ Vars(And+(W )) = 0,/ and Theorem 6.2 yields
that |C ∪ And+(W )| ≥ |CJW K ∪ And+(W )| > |Vars(And+(W ))|, using the notation from (6.2). This is
not quite what we want—we have a lower bound on |C ∪ And+(W )|, but what we need is a bound on |C|.
But if we observe that |Vars(And+(W ))| = d|W | while |And+(W )| = |W |, we get that
|C| ≥ |Vars(And+(W ))| − |And+(W )| + 1 = (d − 1)|W | + 1 ≥ |W | + 1 (6.6)
as claimed.
Note that this time we had to use that d > 1 in order to get a lower bound on the clause set size. And
indeed, it is not hard to see that a single clause of the form C = v1 ∨ w∈W w1 can induce an arbitrary
W
number of white pebbles if d = 1. Intuitively, white pebbles can be had for free in degree-1 pebbling
formulas.
In general, matters are more complicated than in Examples 6.3 and 6.4. If [B1 ]hW1 i and [B2 ]hW2 i
are two induced blob subconfigurations, the black blobs B1 and B2 need not be disjoint, the supporting
white pebbles W1 and W2 might also intersect, and the black blob B1 can intersect the supporting white
pebbles W2 of the other blob. Nevertheless, if we choose with some care which vertices to charge for, the
intuition provided by our examples can still be used to prove the following theorem.
Theorem 6.5. Suppose that G is a DAG and let C be a set of clauses derived from the pebbling formula
*PebdG for d ≥ 2. Then |C| ≥ cost(S(C)).
Proof. Suppose that the induced set of blob subconfigurations is S(C) = [Bi ]hWi i i ∈ [m] . By Defini-
tion 4.7, we have cost(S(C)) = B ∪ WM where
B = bot(Bi ) [Bi ]hWi i ∈ S(C) and |bot(Bi )| = 1
(6.7)
and
WM =
[ \
Wi ∩ GMb . (6.8)
[Bi ]hWi i∈S(C) b∈bot(Bi )
We need to prove that |C| ≥ B ∪ WM .
We first show that all vertices in B ∪ WM are represented in some clause in C. By Definition 5.2, for
each [Bi ]hWi i ∈ S(C) there is a clause set Ci ⊆ C such that
Ci ∪ And+(Wi ) Or+(Bi ) (6.9)
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 505
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
and such that this implication does not hold for any strict subset of Ci , Wi or Bi . Fix (arbitrarily) such a
clause set Ci for every [Bi ]hWi i ∈ S(C) for the rest of this proof.
For the induced black blobs Bi we claim that Bi ⊆ V (Ci ), which certainly implies B ⊆ V (C). To estab-
lish this claim, note that for any v ∈ Bi we can apply Lemma 6.1 with D1 = dj=1 v j and D2 = Or+(Bi \ {v})
W
on the implication (6.9), which yields that the vertex v must be represented in Ci ∪ And+(Wi ) by some
/ we have Vars(And+(Wi )) ∩ Vars(Or+(Bi )) = 0/ and thus v j ∈ Lit(Ci ).
positive literal v j . Since Bi ∩ Wi = 0,
Also, we claim that Wi ⊆ V (Ci ). To see this, note that since Bi ∩ Wi = 0/ and the implication (6.9) is
minimal, it follows from Lemma 5.4 that for every w ∈ Wi , all literals w j , j ∈ [d], must be present in Ci .
Hence, in particular, it holds that Wi ∩ b∈bot(Bi ) GMb ⊆ V (Ci ).
T
We now prove by induction over subsets R ⊆ B ∪ WM that |CJRK| ≥ |R|. The theorem clearly follows
from this since |C| ≥ |CJRK|. (The letter R is chosen to suggest that this is the set of vertices representing
the blob-pebbling configurations [Bi ]hWi i ∈ S(C) in the clause set C.) The base case |R| = 1 is immediate,
since we just demonstrated that all vertices r ∈ R are represented in C.
For the induction step, suppose that |CJR0 K| ≥ |R0 | for all R0 $ R. Pick a vertex r ∈ top(R), i. e., a
“topmost” vertex r ∈ R such that GO r ∩ R = 0.
\ / We associate a blob subconfiguration [Bi ]hWi i ∈ S(C)
with r as follows. If {r} ∈ bot(Bi ) for some [Bi ]hWi i, fix [Bi ]hWi i arbitrarily to such a subconfiguration.
Otherwise, there must exist some [Bi ]hWi i such that r ∈ Wi ∩ b∈bot(Bi ) GMb , so fix any such subconfigu-
T
ration. An important observation is that for r and [Bi ]hWi i chosen in this way it holds that
GO
[
R∩ b ⊆ {r} . (6.10)
b∈bot(Bi )
This is so since if bot(Bi ) is a single vertex r, this means that all of Bi resides above this vertex in G, and
if r ∈ b∈bot(Bi ) GMb this is just another way of saying that bot(Bi ) ⊆ GO O
r and hence Bi ⊆ Gr .
T
Consider the clause set Ci ⊆ C from (6.9) associated with [Bi ]hWi i above. Clearly, by construction
r ∈ V (Ci ) is one of the vertices of R mentioned by Ci . We claim that the total number of vertices in R
mentioned by Ci is upper-bounded by the number of clauses in Ci mentioning these vertices, i. e., that
Ci JRK ≥ R ∩ V (Ci ) . (6.11)
Before establishing this claim, let us show that it is sufficient to prove the theorem. To this end, let us
write
R[i] = R ∩ V (Ci ) (6.12)
to denote the set of all vertices in R mentioned by Ci and assume that |Ci JRK| = |Ci JR[i]K| ≥ |R[i]|. Observe
that Ci JR[i]K ⊆ CJRK, since Ci ⊆ C and R[i] ⊆ R. Or in words: the set of clauses in Ci mentioning vertices
in R[i] is certainly a subset of all clauses in C mentioning any vertex in R. Also, by construction Ci does
not mention any vertices in R \ R[i] since R[i] = R ∩ V (Ci ). That is, we have
CJR \ R[i]K ⊆ CJRK \ Ci (6.13)
in our notation. Combining the (as of yet unproven) Claim 6.11 for Ci JRK = Ci JR[i]K asserting that
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 506
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Ci JR[i]K ≥ |R[i]| with the induction hypothesis for R \ R[i] ⊆ R \ {r} $ R we get
.
CJRK = Ci JRK ∪ (C \ Ci )JRK
.
≥ Ci JR ∩V (Ci )K ∪ CJR \V (Ci )K
= Ci JR[i]K + CJR \ R[i]K (6.14)
≥ |R[i]| + |R \ R[i]|
= |R|
and the theorem follows by induction.
It remains to verify the Claim 6.11 that |Ci JR[i]K| ≥ |R[i]| for R[i] = R ∩ V (Ci ) 6= 0.
/ To do so, recall
first that r ∈ R[i]. Thus, R[i] 6= 0/ and if R[i] = {r} we trivially have |Ci JR[i]K| ≥ 1 = |R[i]|. Suppose
therefore that R[i] % {r}. We want to apply Theorem 6.2 on the formula F = C. i ∪ And+(Wi ) on the
left-hand side of the minimal implication (6.9). Let R0 = R[i] \ {r}, write R0 = R1 ∪ R2 for R1 = R0 ∩ Wi
and R2 = R0 \ R1 , and consider the subformula
FR0 = C ∈ Ci ∪ And+(Wi ) V (C) ∩ R0 6= 0/
(6.15)
= Ci JR0 K ∪ And+(R1 )
of F = Ci ∪ And+(Wi ). A key observation for the concluding part of the argument is that by (6.10) we
have Varsd (R0 ) ∩ Vars(Or+(Bi )) = 0.
/
For each w ∈ R1 , the clauses in And+(R1 ) contain d literals w1 , . . . , wd and these literals must all
occur negated in Ci by Lemma 5.4. For each u ∈ R2 , the clauses in Ci JR0 K contain at least one variable ui .
Appealing to Theorem 6.2 with clause D = Or+(Bi ) and variable subset V = Varsd (R0 ) ∩ Vars(Ci ) ⊆
Vars(F) \ Vars(Or+(Bi )), we get
FR0 = Ci JR0 K ∪ And+(R1 )
≥ Varsd (R0 ) ∩ Vars(Ci ) + 1 (6.16)
≥ d R1 + R2 + 1 ,
and rewriting this as
Ci JR[i]K ≥ Ci JR0 K
= FR0 − And+(R1 )
(6.17)
≥ (d − 1) R1 + R2 + 1
≥ R[i]
establishes the claim.
We have two concluding remarks. Firstly, we note that the place where the condition d ≥ 2 is needed
is the very final step (6.17). This is where an attempted lower bound proof for first degree pebbling
formulas *Peb1G would fail for the reason that the presence of many white pebbles in S(C) says absolutely
nothing about the size of the clause set C inducing these pebbles. Secondly, another crucial step in the
proof is that we can choose our representative vertices r ∈ R so that (6.10) holds. It is thanks to this that
the inequalities in (6.16) go through. The way we make sure (6.10) holds is to charge only for (distinct)
bottom vertices in the black blobs, and only for supporting white pebbles below these bottom vertices.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 507
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
7 Black-white pebbling and layered graphs
Having come this far in the paper, we know that resolution derivations induce blob-pebblings. We also
know that blob-pebbling cost gives a lower bound on clause set size and hence on the space of the
derivation. The final component needed to make the proof of Theorem 1.1 complete is to show lower
bounds on the blob-pebbling price Blob-Peb(Gi ) for some nice family of DAGs {Gi }∞ i=1 .
Perhaps the first idea that comes to mind is to try to establish lower bounds on blob-pebbling price
by reducing this problem to the problem of proving lower bounds for the standard black-white pebble
game of Definition 3.4. This is what is done in [47] for the restricted case of trees. There, for the
pebblings Pπ that one gets from resolution derivations π : *PebdT ` di=1 zi in a rather different so-called
W
“labelled” pebble game, an explicit procedure is presented to transform Pπ into a complete black-white
pebblings of T in essentially the same cost except for a small constant-factor blow-up. The lower bound
on pebbling price in the labelled pebble game then follows immediately by using the known lower bound
for black-white pebbling of trees in [44].
Unfortunately, the blob-pebble game seems more difficult than the game in [47] to analyze in terms
of the standard black-white pebble game. The problem is the inflation rule in combination with the cost
function. It is straightforward to show that without inflation, the blob-pebble game is essentially just a
disguised form of black-white pebbling. Thus, if we could convert any blob-pebbling into an equivalent
pebbling not using inflation moves without increasing the cost by more than, say, some constant factor,
we would be done. But in contrast to the case for the labelled pebble game in [47] played on binary trees,
it seems hard to transform blob-pebblings into black-white pebblings in a cost-preserving way.
Instead, what we do is to prove lower bounds directly for the blob-pebble game. This is not
immediately clear how to do, since the lower bound proofs for black-white pebbling price in, e. g.,
[27, 35, 42, 44] all break down for the more general blob-pebble game. And indeed, to obtain lower
bounds we have to limit our attention to the class of layered spreading graphs (to be defined below), a
class that includes binary trees and pyramid graphs.
In our proof, we borrow heavily from the corresponding bound for black-white pebbling by Klawe [42],
but we need to go quite deep into the construction in order to make the changes necessary for the proof
go through in the blob-pebbling case. In this section, we therefore give a detailed exposition of the lower
bound in [42]. We believe that an in-depth description of this construction, which in addition has been
somewhat simplified as compared to the original paper, is crucial in order to give the reader a fair chance
to understand what is going on in the next section, where we generalize the bound from the black-white
pebble game to the blob-pebble game in Definition 4.6.
7.1 Some preliminaries and a tight bound for black pebbling
Unless otherwise stated, in the following G denotes a layered DAG (Definition 4.2); u, v, w, x, y, z denote
vertices of G, where as before z is assumed to be the unique sink vertex; U,V,W, X,Y denote sets of
vertices; P denotes a path; and P denotes a set of paths. We will also use the following notation.
Definition 7.1 (Layered DAG notation). For a vertex u in a layered DAG G we let level(u) denote
the level of u. For a vertex set U we let minlevel(U) = min{level(u) : u ∈ U} and maxlevel(U) =
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 508
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
h+1 s7
z h u6 s6
...
v5 u5 s5
y1 y2
4 w4 v4 u4 s4
x1 x2 x3
3 x3 w3 v3 u3 s3
w1 w2 w3 w4
2 y2 x2 w2 v2 u2 s2
v1 v2 v3 v4 v5
1 z y1 x1 w1 v1 u1 s1
u1 u2 u3 u4 u5 u6
s1 s2 s3 s4 s5 s6 s7 ...
1 2 3 4 h h+1
(a) Pyramid graph of height h = 6. (b) Pyramid as fragment of 2D rectilinear lattice.
Figure 7: The pyramid Π6 of height 6 with labelled vertices.
max{level(u) : u ∈ U} denote the lowest and highest level, respectively, of any vertex in U. Vertices in U
on particular levels are denoted as follows:
• U{ j} = {u ∈ U | level(u) ≥ j} denotes the subset of all vertices in U on level j or higher.
• U{ j} = {u ∈ U | level(u) > j} denotes the vertices in U strictly above level j.
• U{∼ j} = U{ j} \U{ j} denotes the vertices exactly on level j.
The vertex sets U{ j} and U{≺ j} are defined completely analogously.
For the layered DAGs G under consideration we will assume that all sources are on level 0 and that
all non-sources have indegree 2.
Although most of what will be said in what follows holds for arbitrary layered DAGs, we will focus
on pyramids since these are the graphs that we are most interested in. Figure 7(a) presents a pyramid
graph with labelled vertices that we will use as a running example. Pyramid graphs can also be visualized
as triangular fragments of a directed two-dimensional rectilinear lattice. Perhaps this can sometimes
make it easier for the reader to see that “obvious” statements about properties of pyramids in some of the
proofs below are indeed obvious. In Figure 7(b), the pyramid in Figure 7(a) is redrawn as such a lattice
fragment.
In the standard black and black-white pebble games, we have the following upper bounds on pebbling
price of layered DAGs.
Lemma 7.2. For any layered DAG Gh of height h with a unique sink z and all non-sources having vertex
indegree 2, it holds that Peb(Gh ) ≤ h + O(1) and BW-Peb(Gh ) ≤ h/2 + O(1).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 509
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
z z1
u v u1 v1
r s t r1 s1 s2 t1
p q m n p1 q1 q2 m1 q3 m2 m3 n1
(a) Pyramid graph Π3 of height 3. (b) Binary tree T3 with vertex labels from Π3 .
Figure 8: Binary tree with vertices labelled by pyramid graph vertices as in proof of Lemma 7.2.
Proof. The bounds above are true for complete binary trees of height h according to [44]. It is not hard
to see that the corresponding pebbling strategies can be used to pebble any layered graph of the same
height with at most the same amount of pebbles.
Formally, suppose that the sink z of the DAG Gh has predecessors x and y. Label the root of Th by z1
and its predecessors by x1 and y1 . Recursively, for a vertex in Th labelled by wi , look at the corresponding
vertex w in Gh and suppose that pred(w) = {u, v}. Then label the vertices pred(wi ) in Th by u j and vk for
the smallest positive indices j, k such that there are not already other vertices in Th labelled u j and vk . In
Figure 8 there is an illustration of how the vertices in a pyramid Π3 of height 3 are mapped to vertices in
the complete binary tree T3 in this manner.
The result is a labelling of Th where every vertex v in Gh corresponds to one or more distinct vertices
v1 , . . . , vkv in Th , and such that if pred(wi ) = {u j , vk } in Th , then pred(w) = {u, v} in Gh . Given a pebbling
strategy P for Th , we can pebble Gh with at most the same amount of pebbles by mimicking any move on
any vi in Th by performing the same move on v in Gh . The details are easily verified.
In this section, we will identify some layered graphs Gh for which the bound in Lemma 7.2 is also
the asymptotically correct lower bound. As a warm-up, and also to introduce some important ideas, let us
consider the black pebbling price of the pyramid Πh of height h.
Theorem 7.3 ([25]). Peb(Πh ) = h + 2 for h ≥ 1.
To prove this lower bound, it turns out that it is sufficient to study blocked paths in the pyramid.
Definition 7.4. A vertex set U blocks a path P if U ∩ P 6= 0.
/ A vertex set U blocks a set of paths P if U
blocks all P ∈ P.
Proof of Theorem 7.3. It is easy to devise (inductively) a black pebbling strategy that uses h + 2 pebbles
(using, e. g., Lemma 7.2). We show that this is also a lower bound.
Consider the first time t when all possible paths from sources to the sink are blocked by black pebbles
(there is such a time since the black pebble on the sink blocks all paths at the end of the pebbling).
Suppose that P is one previously open path that was blocked at time t. Then P must be blocked by placing
a pebble on some source vertex u. The path P contains h + 1 vertices, and for each vertex v ∈ P \ {u}
there is a unique path Pv that coincides with P from v onwards to the sink but arrives at v in a straight
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 510
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
z
y1 y2
x1 x2 x3
w1 w2 w3 w4
v1 v2 v3 v4 v5
u1 u2 u3 u4 u5 u6
s1 s2 s3 s4 s5 s6 s7
Figure 9: Set of converging source paths (dashed) for the path P : u4 y1 (solid).
line from a source “in the opposite direction” of that of P, i. e., via the immediate predecessor of v not
contained in P. At time t − 1 all such paths {Pv | v ∈ P \ {u}} must already be blocked, and since P is still
open no pebble can block two paths Pv 6= Pv0 for v, v0 ∈ P \ {u}, v 6= v0 . Thus at time t there are at least
h + 1 pebbles on Πh . Furthermore, without loss of generality each pebble placement on a source vertex is
followed by another pebble placement (otherwise perform all removals immediately following after time
t before making the pebble placement at time t). Thus at time t + 1 there are h + 2 pebbles on Πh .
We will use the idea in the proof above about a set of paths converging at different levels to another
fixed path repeatedly, so we write it down as a separate observation.
Observation 7.5. Suppose that u and w are vertices in Πh on levels Lu < Lw and that P : u w is a
path from u to w. Let K = Lw − Lv and write P = {v0 = u, v1 , . . . , vK = w}. Then there is a set of K paths
P = {P1 , . . . , PK } such that Pi coincides with P from vi onwards to w and arrives to vi in a straight line
from a source vertex via the immediate predecessor of vi which is not contained in P, i. e., is distinct
from vi−1 . In particular, for any i, j with 1 ≤ i < j ≤ k it holds that Pi ∩ Pj ⊆ Pj ∩ P ⊆ P \ {u}.
We will refer to the paths P1 , . . . , PK as a set of converging source paths, or just converging paths, for
P : u w. See Figure 9 for an example.
7.2 A tight bound on the black-white pebbling price of pyramids
The rest of this section contains an exposition of the black-white pebbling price lower bound for pyramids
by Klawe [42], which we will adapt in Section 8 to work for the blob-pebble game. We have slightly
modified (and hopefully simplified) the proofs, and have also had to change much of the notation and
terminology in [42] to agree better with this the rest of this paper in general and the blob-pebble game
in particular. Perhaps the most important change is that we restrict all definitions to layered graphs, in
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 511
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
contrast to Klawe who deals with a somewhat more general class of DAGs. We concentrate on layered
graphs mainly to avoid unnecessary complications in the exposition, and since it can be proven that no
graphs in [42] can give a better size/pebbling price trade-off than one gets for layered graphs anyway.
Recall from Definition 4.4 that a path via w is a path P such that w ∈ P. We will also say that P
visits w. The notation Pvia (w) is used to denote all source paths visiting w. Note that a path P ∈ Pvia (w)
visiting w may continue after w, or may end in w.
Definition 7.6 (Hiding set). A vertex set U hides a vertex w if U blocks all source paths visiting w, i. e.,
if U blocks Pvia (w). U hides W if U hides all w ∈ W . If so, we say that U is a hiding set for W . We write
VUW to denote the set of all vertices hidden by U.
Our perspective is that we are standing at the sources of G and looking towards the sink. Then U
hides w if we “cannot see” w from the sources since U covers all paths approaching w (in particular,
a vertex w hides itself). When U blocks a path P is is possible that we can “see” the beginning of the
path, but we cannot walk all of the path since it is blocked somewhere on the way. The reason why this
terminological distinction is convenient will hopefully become clear in the next section.
Note that if U should hide w, then in particular it must block all paths ending in w. Therefore, when
looking at minimal hiding sets we can assume without loss of generality that no vertex in U is on a level
higher than w.
It is an easy exercise to show that the hiding relation is transitive, i. e., that if U hides V and V hides
W , then U hides W . Let us state this as a proposition for reference.
Proposition 7.7. If V ⊆ VUW and W ⊆ VV W then W ⊆ VUW.
One key concept in Klawe’s paper is that of potential. The potential of a black-white pebble
configuration P = (B,W ) is intended to measure how “good” the configuration P is, or at least how hard
it is to reach in a pebbling. Note that this is not captured by the cost of the current pebble configuration.
For instance, the final configuration Pτ = ({z}, 0) / is the best configuration conceivable, but only costs 1.
At the other extreme, the configuration P in a pyramid with, say, all vertices on level L white-pebbled
and all vertices on level L + 1 black-pebbled is potentially very expensive (for low levels L), but does not
seem very useful. Since this configuration on the one hand is quite expensive, but on the other hand is
extremely easy to derive (just white-pebble all vertices on level L, and then black-pebble all vertices on
level L + 1), here the cost seems like a gross overestimation of the “goodness” of P.
Klawe’s potential measure remedies this. The potential of a pebble configuration (B,W ) is declared
to be the minimum measure, as defined next, of any set U that together with W hides B. Recall that
U{ j} denotes the subset of all vertices in U on level j or higher in a layered graph G.
Definition 7.8 (Measure). The jth partial measure of the vertex set U in G is
(
j j + 2|U{ j}| if U{ j} 6= 0, /
mG (U) =
0 otherwise,
and the measure of U is mG (U) = max j mGj (U) .
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 512
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Definition 7.9 (Potential). We say that U is a hiding set for a black-white pebble configuration P = (B,W )
in a layered graph G if U ∪ W hides B. We define the potential of the pebble configuration to be
potG (P) = potG (B,W ) = min{mG (U) : U is a hiding set for (B,W )} .
If U is a hiding set for (B,W ) with minimal measure mG (U) among all vertex sets U 0 such that U 0 ∪ W
hides B, we say that U is a minimum-measure hiding set for P.
Since the graph under consideration will almost always be clear from context, we will tend to omit
the subindex G in measures and potentials.
We remark that although this might not be immediately obvious, there is quite a lot of nice intuition
why Definition 7.9 should be a relevant estimate of how “good” a pebble configuration is. We refer the
reader to Section 2 of [42] for a discussion about this. Let us just note that with this definition, the pebble
configuration Pτ = ({z}, 0)/ has high potential, as we shall soon see, while the configuration with all
vertices on level L white-pebbled and all vertices on level L + 1 black-pebbled has potential zero. This
agrees with our intuitive understanding as explained before Definition 7.8.
Remark 7.10. Klawe does not use the level of a vertex u in Definitions 7.8 and 7.9, but instead the black
pebbling price Peb({u}, 0)
/ of the configuration with a black pebble on u and no other pebbles in the
DAG. For pyramids, these two concepts are equivalent, and we feel that the exposition can be made
considerably simpler by using levels.
Klawe proves two facts about the potentials of the pebble configurations in any black-white pebbling
P = {P0 , . . . , Pτ } of a pyramid graph Πh :
1. The potential correctly estimates the goodness of the current configuration Pt by taking into account
the whole pebbling that has led to Pt . Namely, pot(Pt ) ≤ 2 · maxs≤t {cost(Ps )}.
2. The final configuration Pτ = ({z}, 0) / = h + O(1).
/ has high potential, namely pot({z}, 0)
Combining these two parts, one clearly gets a lower bound on pebbling price.
For pyramids, part 2 is not too hard to show directly. In fact, it is a useful exercise if one wants to
get some feeling for how the potential works. Part 1 is much trickier. It is proven by induction over the
pebbling. As it turns out, the whole induction proof hinges on the following key property.
Property 7.11 (Limited hiding-cardinality property). We say that the black-white pebble configuration
P = (B,W ) in G has the limited hiding-cardinality property, or just the LHC property for short, if there is
a vertex set U such that
1. U is a hiding set for P,
2. potG (P) = m(U),
3. U = B or |U| < |B| + |W | = cost(P).
We say that the graph G has the limited hiding-cardinality property if all black-white pebble configurations
P = (B,W ) on G have the limited hiding-cardinality property.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 513
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Note that requirements 1 and 2 just say that U is a vertex set that witnesses the potential of P. The
important point here is requirement 3, which says (basically) that if we are given a hiding set U with
minimum measure but with size exceeding the cost of the black-white pebble configuration P, then we
can pick another hiding set U 0 which keeps the minimum measure but decreases the cardinality to at
most cost(P).
Given Property 7.11, the induction proof for part 1 follows quite easily. The main part of the paper [42]
is then spent on proving that a class of DAGs including pyramids have Property 7.11. Let us see what the
lower bound proof looks like, assuming that Property 7.11 holds.
Lemma 7.12 (Theorem 2.2 in [42]). Let G be a layered graph possessing the LHC property and suppose
that P = {P0 = 0, / P1 , . . . , Pτ } is any unconditional black-white pebbling on G. Then it holds for all
t = 1, . . . , τ that potG (Pt ) ≤ 2 · maxs≤t {cost(Ps )}.
Proof. To simplify the proof, let us assume without loss of generality that no white pebble is ever removed
from a source. If P contains such moves, we just substitute for each such white pebble placement on v a
black pebble placement on v instead, and when the white pebble is removed we remove the corresponding
black pebble. It is easy to check that this results in a legal pebbling P0 that has exactly the same cost.
The proof is by induction. The base case P0 = 0/ is trivial. For the induction hypothesis, suppose
that pot(Pt ) ≤ 2 · maxs≤t {cost(Ps )} and let Ut be a vertex set as in Property 7.11, i. e., such that Ut ∪ Wt
hides Bt , pot(Pt ) = m(Ut ) and |Ut | ≤ cost(Pt ) = |B| + |W |.
Consider Pt+1 . We need to show that pot(Pt+1 ) ≤ 2 · maxs≤t+1 {cost(Ps )}. By the induction hypothe-
sis, it is sufficient to show that
pot(Pt+1 ) ≤ max{pot(Pt ), 2 · cost(Pt+1 )} . (7.1)
We also note that if Ut ∪ Wt+1 hides Bt+1 we are done, since if so pot(Pt+1 ) ≤ m(Ut ) = pot(Pt ). We
make a case analysis depending on the type of move made to get from Pt to Pt+1 .
1. Removal of black pebble: In this case, Ut ∪ Wt+1 = Ut ∪ Wt obviously hides Bt+1 ⊂ Bt as well, so
pot(Pt+1 ) ≤ pot(Pt ).
2. Placement of white pebble: Again, Ut ∪ Wt+1 ⊃ Ut ∪ Wt hides Bt+1 = Bt , so pot(Pt+1 ) ≤ pot(Pt ).
3. Removal of white pebble: Suppose that a white pebble is removed from the vertex w, so Wt+1 =
Wt \ {w}. As noted above, without loss of generality w is not a source vertex. We claim that
Ut ∪ Wt+1 still hides Bt+1 = Bt , from which pot(Pt+1 ) ≤ pot(Pt ) follows as above.
To see that the claim is true, note that pred(w) ⊆ Bt ∪ Wt by the pebbling rules, for otherwise we
would not be able to remove the white pebble on w. If pred(w) ⊆ Wt we are done, since then
Ut ∪ Wt+1 hides Ut ∪ Wt and we can use the transitivity in Proposition 7.7. If instead there is some
v ∈ pred(w) ∩ Bt , then Ut ∪ Wt = Ut ∪ Wt+1 ∪ {w} hides v by assumption. Since w is a successor
of v, and therefore on a higher level than v, we must have Ut ∪ Wt \ {w} hiding v. Thus in any case
Ut ∪ Wt+1 hides pred(w), so by transitivity Ut ∪ Wt+1 hides Bt+1 .
4. Placement of black pebble: Suppose that a black pebble is placed on v. If v is not a source, by
the pebbling rules we again have that pred(v) ⊆ Bt ∪ Wt . In particular, Bt ∪ Wt hides v and by
transitivity we have that Ut ∪ Wt+1 = Ut ∪ Wt hides Bt ∪ {v} = Bt+1 .
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 514
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
The case when v is a source turns out to be the only interesting one. Now Ut ∪ Wt does not
necessarily hide Bt ∪ {v} = Bt+1 any longer. An obvious fix is to try with Ut ∪ {v} ∪ Wt instead.
This set clearly hides Bt+1 , but it can be the case that m(Ut ∪ {v}) > m(Ut ). This is problematic,
since we could have pot(Pt+1 ) = m(Ut ∪ {v}) > m(Ut ) = pot(Pt ). And we do not know that the
inequality pot(Pt ) ≤ 2 · cost(Pt ) holds, only that pot(Pt ) ≤ 2 · maxs≤t {cost(Ps )}. This means that
it can happen that pot(Pt+1 ) > 2 · cost(Pt+1 ), in which case the induction step fails. However,
we claim that using the limited hiding-cardinality property (Property 7.11) we can prove for
Ut+1 = Ut ∪ {v} that
m(Ut+1 ) = m(Ut ∪ {v}) ≤ max{m(Ut ), 2 · cost(Pt+1 )} , (7.2)
which shows that (7.1) holds and the induction steps goes through.
Namely, suppose that Ut is chosen as in Property 7.11 and consider Ut+1 = Ut ∪ {v}. Then Ut+1
is a hiding set for Pt+1 = (Bt ∪ {v},Wt ) and hence pot(Pt+1 ) ≤ m(Ut+1 ). For j > 0, it holds that
Ut+1 { j} = Ut { j} and thus m j (Ut+1 ) = m j (Ut ). On the bottom level, using that the inequality
|Ut | ≤ cost(Pt ) holds by the LHC property, we have
m0 (Ut+1 ) = 2 · |Ut+1 | = 2 · (|Ut | + 1) ≤ 2 · (cost(Pt ) + 1) = 2 · cost(Pt+1 ) (7.3)
and we get that
m(Ut+1 ) = max j m j (Ut+1 ) = max max j>0 m j (Ut ) , m0 (Ut+1 )
≤ max{m(Ut ), 2 · cost(Pt+1 )} = max{pot(Pt ), 2 · cost(Pt+1 )} (7.4)
which is exactly what we need.
We see that the inequality (7.1) holds in all cases in our case analysis, which proves the lemma.
The lower bound on black-white pebbling price now follows by showing that the final pebble
configuration ({z}, 0)
/ has high potential.
Lemma 7.13. For z the sink of a pyramid Πh of height h, the pebble configuration ({z}, 0)
/ has potential
potΠh ({z}, 0)
/ = h + 2.
Proof. This follows easily from the limited hiding-cardinality property (which says that U can be chosen
so that either U ⊆ {z} or |U| ≤ 0), but let us show that this assumption is not necessary here. The set
U = {z} hides itself and has measure m(U) = mh (U) = h + 2 · 1 = h + 2. Suppose that z is hidden by
some U 0 6= {z}. Without loss of generality U 0 is minimal, i. e., no strict subset of U 0 hides z. Let u be a
vertex in U 0 on minimal level minlevel(U) = L < h. The fact that U 0 is minimal implies that there is a
path P : u z such that (P \ {u}) ∩ U 0 = 0/ (otherwise U 0 \ {u} would hide z). By Observation 7.5, there
must exist h − L converging paths from sources to z that are all blocked by distinct pebbles in U 0 \ {u}. It
follows that
m(U 0 ) ≥ mL U 0 = L + 2 U 0 { L} = L + 2 U 0 ≥ L + 2 · (h + 1 − L) > h + 2
(7.5)
(where we used that U 0 { L} = U 0 since L = minlevel(U)). Thus U = {z} is the unique minimum-
measure hiding set for ({z}, 0), / = h + 2.
/ and the potential is pot({z}, 0)
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 515
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Since [42] proves that pyramids possess the limited hiding-cardinality property, and since there are
pebblings that yield matching upper bounds, we have the following theorem.
Theorem 7.14 ([42]). BW-Peb(Πh ) = h/2 + O(1).
Proof. The upper bound was shown in Lemma 7.2. For the lower bound, Lemma 7.13 says that the
/ in any complete pebbling P of Πh has potential pot({z}, 0)
final pebble configuration ({z}, 0) / = h + 2.
According to Lemma 7.12, pot({z}, 0) / ≤ 2 · cost(P). Thus BW-Peb(Πh ) ≥ h/2 + 1.
In the remainder of this section, we provide a fairly detailed overview of the proof that pyramids do
indeed possess the limited hiding-cardinality property. As was discussed above, the reason for giving
all the details is that we will need to use and modify the construction in non-trivial ways in the next
section, where we will use ideas inspired by Klawe’s paper to prove lower bounds on the pebbling price
of pyramids in the blob-pebble game.
7.3 An exposition of the proof of the limited hiding-cardinality property
We present the proof of that pyramids have the limited hiding-cardinality property in a top-down fashion
as follows.
1. First, we study what hiding sets look like in order to better understand their structure. Along
the way, we make a few definitions and prove some lemmas culminating in Definition 7.20 and
Lemma 7.24.
2. We conclude that it seems like a good idea to try to split our hiding set into disjoint components,
prove the LHC property locally, and then add everything together to get a proof that works
globally. We make an attempt to do this in Theorem 7.25, but note that the argument does not
quite work. However, if we assume a slightly stronger property locally for our disjoint components
(Property 7.27), the proof goes through.
3. We then establish this stronger local property by assuming that pyramid graphs have a certain
spreading property (Definition 7.34 and Theorem 7.35) and showing in Lemmas 7.33 and 7.36 that
the stronger local property holds for such spreading graphs.
4. To clinch the proof, we also need to show that pyramids are indeed spreading. Since we can use
this part from [42] as-is, we do not present a proof here, but instead refer to the original paper or
to [48] for a simplified, more direct argument.
For a start, we need two definitions. The intuition for the first one is that the vertex set U is tight if it
does not contain any “unnecessary” vertex u hidden by the other vertices in U.
Definition 7.15 (Tight vertex set). The vertex set U is tight if for all u ∈ U it holds that u ∈
/ VU \ {u}W.
If x is a vertex hidden by U, we can identify a subset of U that is necessary for hiding x.
Definition 7.16 (Necessary hiding subset). If x ∈ VUW, we define U TxU to be the subset of U such that
for each u ∈ U TxU there is a source path P ending in x for which P ∩ U = {u}.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 516
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
We observe that if U is tight and x ∈ U, then U TxU = {x}. This is not the case for non-tight sets. If we
let U = {x} ∪ pred(x) for some non-source x, Definition 7.16 yields that U TxU = 0. / The vertices in U TxU
must be contained in every subset of U that hides x, since for each v ∈ U TxU there is a source path to x
that intersects U only in v. But if U is tight, the set U TxU is also sufficient to hide x, i. e., x ∈ VU TxUW.
Lemma 7.17 (Lemma 3.1 in [42]). If U is tight and x ∈ VUW, then U TxU hides x and this set is also
contained in every subset of U that hides x.
Proof. The necessity was argued above, so the interesting part is that x ∈ VU TxUW. Suppose not. Let P1
be a source path to x such that P1 ∩ U TxU = 0. / Since U hides x, U blocks P1 . Let v be the highest-level
element in P1 ∩ U (i. e., the vertex on this path closest to x). Since U is tight, U \ {v} does not hide v. Let
P2 be a source path to v such that P2 ∩ (U \ {v}) = 0. / Then going first along P2 and switching to P1 at v
we get a path to x that intersects U only in v. But if so, we have v ∈ U TxU contrary to assumption. Thus,
x ∈ VU TxUW must hold.
Given a vertex set U, the tight subset of U hiding the same elements is uniquely determined.
Lemma 7.18. For any vertex set U in a layered graph G there is a uniquely determined minimal subset
U ∗ ⊆ U such that VU ∗ W = VUW, U ∗ is tight, and for any U 0 ⊆ U with VU 0 W = VUW it holds that U ∗ ⊆ U 0 .
Proof. We construct the set U ∗ bottom-up, layer by layer. We will let Ui∗ be the set of vertices on level i
or lower in the tight hiding set under construction, and Uir be the set of vertices in U strictly above level i
remaining to be hidden.
Let L = minlevel(U). For i < L, we define Ui∗ = 0. / Clearly, all vertices on level L in U must be
∗
present also in U , since no vertices in U{ L} can hide these vertices and vertices on the same level
cannot help hiding each other. Set UL∗ = U{∼ L} = U \U{ L}. Now we can remove from U all vertices
hidden by UL∗ , so set ULr = U \ VUL∗ W. Note that there are no vertices on or below level L left in ULr , i. e.,
ULr = ULr { L}, and that UL∗ hides the same vertices as does U{ L} (since the two sets are equal).
Inductively, suppose we have constructed the vertex sets Ui−1 ∗ and U r . Just as above, set U ∗ =
i−1 i
∗ r r r ∗
Ui−1 ∪ Ui−1 {∼ i} and Ui = Ui−1 \ VUi W. If there are no vertices remaining on level i to be hidden, i. e., if
r {∼ i} = 0,
Ui−1 / nothing happens and we get Ui∗ = Ui−1 ∗ and U r = U r . Otherwise the vertices on level i
i i−1
r are added to U ∗ and all of these vertices, as well as any vertices above in U r now being hidden,
in Ui−1 i i−1
are removed from Ui−1 r resulting in a smaller set U r .
i
To conclude, we set U ∗ = UM∗ for M = maxlevel(U). By construction, the invariant
VUi∗ W = VU{ i}W (7.6)
holds for all levels i. Thus, VU ∗ W = VUW. Also, U ∗ must be tight since if v ∈ U ∗ and level(v) = i, by
construction U ∗ {≺ i} does not hide v, and (as was argued above) neither does U ∗ { i} \ {v}. Finally,
suppose that U 0 ⊆ U is a hiding set for U with U ∗ * U 0 . Consider v ∈ U ∗ \U 0 and suppose level(v) = i.
On the one hand, we have v ∈ ∗ W by construction. On the other hand, by assumption it holds that
/ VUi−1
v ∈ VU 0 {≺ i}W and thus v ∈ VU{≺ i}W. But then by the invariant (7.6) we know that v ∈ VUi−1 ∗ W, which
∗ 0
yields a contradiction. Hence, U ⊆ U and the lemma follows.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 517
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
z z
y1 y2 y1 y2
x1 x2 x3 x1 x2 x3
w1 w2 w3 w4 w1 w2 w3 w4
v1 v2 v3 v4 v5 v1 v2 v3 v4 v5
u1 u2 u3 u4 u5 u6 u1 u2 u3 u4 u5 u6
s1 s2 s3 s4 s5 s6 s7 s1 s2 s3 s4 s5 s6 s7
(a) Hiding set U with large size and measure. (b) Smaller hiding set U ∗ with smaller measure.
Figure 10: Illustration of hiding sets in Example 7.19 (with vertices in hiding sets cross-marked).
We remark that U ∗ can in fact be seen to contain exactly those elements u ∈ U such that u is not
hidden by U \ {u}.
It follows from Lemma 7.18 that if U is a minimum-measure hiding set for P = (B,W ), we can
assume without loss of generality that U ∪ W is tight. More formally, if U ∪ W is not tight, we can
consider minimal subsets U 0 ⊆ U and W 0 ⊆ W such that U 0 ∪ W 0 hides B and is tight, and prove the LHC
property for B and W 0 with respect to this U 0 instead. Then clearly the LHC property holds also for B
and W .
Suppose that we have a set U that together with W hides B. Suppose furthermore that B contains
vertices very far apart in the graph. Then it might very well be the case that U ∪ W can be split into a
number of disjoint subsets Ui ∪ Wi responsible for hiding different parts Bi of B, but which are wholly
independent of one another. Let us give an example of this.
Example 7.19. Suppose we have the pebble configuration (B,W ) = ({x1 , y1 , v5 }, {w3 , s6 , s7 }) and the
hiding set U = {v1 , u2 , u3 , v3 , s5 } in Figure 10(a). Then U ∪ W hides B, but U seems unnecessarily large.
To get a better hiding set U ∗ , we can leave s5 responsible for hiding v5 but replace {v1 , u2 , u3 , v3 } by
{x1 , y1 }. The resulting set U ∗ = {x1 , y1 , s5 } in Figure 10(b) has both smaller size and smaller measure
(we leave the straightforward verification of this fact to the reader).
Intuitively, it seems that the configuration can be split in two components, namely (B1 ,W1 ) =
({x1 , y1 }, {w3 }) with hiding set U1 = {v1 , u2 , u3 , v3 } and (B2 ,W2 ) = ({v5 }, {s6 , s7 }) with hiding set U2 =
{s5 }, and that these two components are independent of one another. To improve the hiding set U, we
need to do something locally about the bad hiding set U1 in the first component, namely replace it with
U1∗ = {x1 , y1 }, but we should keep the locally optimal hiding set U2 in the second component.
We want to formalize this understanding of how vertices in B, W and U depend on one another in a
hiding set U ∪ W for B. The following definition constructs a graph that describes the structure of the
hiding sets that we are studying in terms of these dependencies.
Definition 7.20 (Hiding set graph). For a tight (and non-empty) set of vertices X in G, the hiding set
graph H = H(G, X) is an undirected graph defined as follows:
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 518
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
z
y1 y2 y1
x1 x2 x3 x1 x2
w1 w2 w3 w4 w1 w2 w3
v1 v2 v3 v4 v5 v1 v2 v3 v5
u1 u2 u3 u4 u5 u6 u2 u3 u5 u6
s1 s2 s3 s4 s5 s6 s7 s5 s6 s7
(a) Vertices hidden by U ∪ W . (b) Hiding set graph H(U ∪ W ).
Figure 11: Pebble configuration with hiding set and corresponding hiding set graph.
• The set of vertices of H is V (H) = VXW.
• The set of edges E(H) of H consists of all pairs of vertices (x, y) for x, y ∈ VXW such that
GMx ∩ VX TxUW ∩ GMy ∩ VX TyUW 6= 0.
/
We say that the vertex set X is hiding-connected if H(G, X) is a connected graph.
When the graph G and vertex set X are clear from context, we will sometimes write only H(X) or
even just H. To illustrate Definition 7.20, we give an example.
Example 7.21. Consider again the configuration (B,W ) = ({x1 , y1 , v5 }, {w3 , s6 , s7 }) from Example 7.19
with hiding set U = {v1 , u2 , u3 , v3 , s5 }, where we have shaded the set of hidden vertices in Figure 11(a).
The hiding set graph H(X) for X = U ∪ W = {v1 , u2 , u3 , v3 , w3 , s5 , s6 , s7 } has been drawn in Figure 11(b).
In accordance with the intuition sketched in Example 7.19, H(X) consists of two connected components.
Note that there are edges from the top vertex y1 in the first component to every other vertex in this
component and from the top vertex v5 to every other vertex in the second component. We will prove
presently that this is always the case (Lemma 7.22). Perhaps a more interesting edge in H(X) is, e. g.,
(w1 , x2 ). This edge exists since X Tw1 U = {v1 , u2 , u3 } and X Tx2 U = {u2 , u3 , v3 , w3 } intersect and since as
a consequence of this (which is easily verified) we have ΠMw1 ∩ VX Tw1 UW ∩ ΠMx2 ∩ VX Tx2 UW 6= 0. / For the
same reason, there is an edge (u5 , u6 ) since X Tu5 U = {s5 , s6 } and X Tu6 U = {s6 , s7 } intersect.
Lemma 7.22. Suppose for a tight vertex set X that x ∈ VXW and y ∈ X TxU. Then x and y are in the same
connected component of H(X).
Proof. Note first that x, y ∈ VXW by assumption, so x and y are both vertices in H(X). Since x is above
y we have GMx ⊇ GMy and we get GMx ∩ VX TxUW ∩ GMy ∩ VX TyUW = VX TxUW ∩ GMy ∩ {y} = {y} 6= 0. / Thus,
(x, y) is an edge in H(X), so x and y are certainly in the same connected component.
Corollary 7.23. If X is tight and x ∈ VXW, then x and all of X TxU are in the same connected component
of the hiding set graph H(X).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 519
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
The next lemma says that if H(X) is a hiding set graph with vertex set V = VXW, then the connected
components V1 , . . . ,Vk of H(X) are themselves hiding set graphs defined over the hiding-connected
subsets X ∩ V1 , . . . , X ∩ Vk .
Lemma 7.24 (Lemma 3.3 in [42]). Let X be a tight set and let Vi be one of the connected components in
H(X). Then the subgraph of H(X) induced by Vi is identical to the hiding set graph H(X ∩ Vi ) defined
on the vertex subset X ∩ Vi . In particular, it holds that Vi = VX ∩ Vi W.
Proof. We need to show that Vi = VX ∩ Vi W and that the edges of H(X) in Vi are exactly the edges in
H(X ∩ Vi ). Let us first show that y ∈ Vi if and only if y ∈ VX ∩ Vi W.
(⇒) Suppose y ∈ Vi . Then X TyU ⊆ Vi by Corollary 7.23. Also, by definition it holds that X TyU ⊆ X, so
X TyU ⊆ X ∩ Vi . Since y ∈ VX TyUW by Lemma 7.17, clearly y ∈ VX ∩ Vi W.
(⇐) Suppose y ∈ VX ∩ Vi W. Since X is tight, its subset X ∩ Vi must be tight as well. Applying
Lemma 7.17 twice, we deduce that (X ∩ Vi )TyU hides y and that X TyU ⊆ (X ∩ Vi )TyU since X TyU is contained
in any subset of X that hides y. But then a third appeal to Lemma 7.17 yields that (X ∩ Vi )TyU ⊆ X TyU
since X TyU ⊆ (X ∩ Vi )TyU ⊆ X ∩ Vi and consequently
X TyU = (X ∩ Vi )TyU . (7.7)
By Corollary 7.23, y and all of (X ∩ Vi )TyU = X TyU are in the same connected component. Since X TyU ⊆ Vi
it follows that y ∈ Vi .
This shows that Vi = VX ∩ Vi W. Plugging (7.7) into Definition 7.20, we see that (x, y) is an edge in
H(X) for x, y ∈ Vi if and only if (x, y) is an edge in H(X ∩ Vi ).
Now we are in a position to describe the structure of the proof that pyramid graphs have the LHC
property.
Theorem 7.25 (Analogue of Theorem 3.7 in [42]). Let P = (B,W ) be any black-white pebble configura-
tion on a pyramid Π. Then there is a vertex set U such that U ∪ W hides B, potΠ (P) = m(U) and either
U = B or |U| < |B| + |W |.
The idea is to construct the graph H = H(Π,U ∪ W ), study the different connected components
in H, find good hiding sets locally that satisfy the LHC property (which we prove is true for each local
hiding-connected subset of U ∪ W ), and then add all of these partial hiding sets together to get a globally
good hiding set.
Unfortunately, this does not quite work. Let us nevertheless attempt to do the proof, note where and
why it fails, and then see how Klawe fixes the broken details.
Tentative proof of Theorem 7.25. Let U be a set of vertices in the pyramid graph Π such that U ∪ W
hides B and pot(P) = m(U). Suppose that U has minimal size among all such sets, and furthermore that
among all such minimum-measure and minimum-size sets U has the largest intersection with B.
Assume without loss of generality (Lemma 7.18) that U ∪ W is tight, so that we can construct H.
Let the connected components of H be V1 , . . . ,Vk . For all i = 1, . . . , k, let Bi = B ∩ Vi , Wi = W ∩ Vi ,
and Ui = U ∩ Vi . Lemma 7.24 says that Ui ∪ Wi hides Bi . In addition, all Vi are pairwise disjoint, so
|B| = ∑ki=1 |Bi |, |W | = ∑ki=1 |Wi | and |U| = ∑ki=1 |Ui |.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 520
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Thus, if the LHC property (Property 7.11) does not hold for U globally, there is some hiding-connected
subset Ui ∪ Wi that hides Bi but for which |Ui | ≥ |Bi | + |Wi | and Ui 6= Bi . Note that this implies that
Bi * Ui since otherwise Ui would not be minimal.
Suppose that we would know that the LHC property is true for each connected component. Then
we could find a vertex set Ui∗ with Ui∗ ⊆ Bi or Ui∗ < |Bi | + |Wi | such that Ui∗ ∪ Wi hides Bi and
m Ui∗ ≤ m(Ui ). Setting U ∗ = (U \ Ui ) ∪ Ui∗ , we would get a hiding set with either |U ∗ | < |U| or
|U ∗ ∩ B| > |U ∩ B|. The second inequality would hold since if |U ∗ | = |U|, then Ui∗ = |Ui | ≥ |Bi ∪ Wi |
and this would imply Ui∗ = Bi and thus Ui∗ ∩ Bi > |Ui ∩ Bi |. This would contradict how U was chosen
above, and we would be home.
Almost. We would also need that Ui∗ could be substituted
for Ui in U without increasing the measure,
∗ ∗
i. e., that m Ui ≤ m Ui should imply m (U \Ui ) ∪ Ui ≤ m (U \Ui ) ∪ Ui . And this turns out not to
be true.
The reason that the proof above does not quite work is that the measure in Definition 7.8 is ill-behaved
with respect to unions. Klawe provides the following example of what can happen.
Example 7.26. With vertex labels as in Figures 7 and 9–11, let X1 = {s1 , s2 }, X2 = {w1 } and X3 = {s3 }.
Then m(X1 ) = 4 and m(X2 ) = 5 but taking unions with X3 we get that m(X1 ∪ X3 ) = 6 and m(X2 ∪ X3 ) = 5.
Thus m(X1 ) < m(X2 ) but m(X1 ∪ X3 ) > m(X2 ∪ X3 ).
So it is not enough to show the LHC property locally for each connected component in the graph.
We also need that sets Ui from different components can be combined into a global hiding set while
maintaining measure inequalities. This leads to the following strengthened condition for connected
components of H.
Property 7.27 (Local limited hiding-cardinality property). We say that the pebble configuration P =
(B,W ) has the local limited hiding-cardinality property, or just the local LHC property for short, if for
any vertex set U such that U ∪ W hides B and is hiding-connected, we can find a vertex set U ∗ such that
1. U ∗ is a hiding set for (B,W ),
2. for any vertex set Y with Y ∩ U = 0/ it holds that m Y ∪ U ∗ ≤ m(Y ∪ U),
3. U ∗ ⊆ B or U ∗ < |B| + |W |.
We say that the graph G has the local LHC property if all black-white pebble configurations P = (B,W )
on G do.
Note that if the local LHC property holds, this in particular implies that m U ∗ ≤ m(U) (just choose
Y = 0).
/ Also, we immediately get that the LHC property holds globally.
Lemma 7.28. If G has the local limited hiding-cardinality property (Property 7.27), then G has the
limited hiding-cardinality property (Property 7.11).
Proof. Consider the tentative proof of Theorem 7.25 and look at the point where itbreaks down. If we
∗ ∗
LHC property tofind Ui , this time we get that m Ui ≤ m Ui does indeed imply
instead use the local
∗
m (U \Ui ) ∪ Ui ≤ m (U \Ui ) ∪ Ui , and the theorem follows.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 521
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
An obvious way to get the inequality m(Y ∪ U ∗ ) ≤ m(Y ∪ U) in Property 7.27 would be to require
that m j (U ∗ ) ≤ m j (U) for all j, but we need to be slightly more general. The next definition identifies a
sufficient condition for sets to behave well under unions with respect to the measure in Definition 7.8.
Definition 7.29. We write U -m V if for all j ≥ 0 there is an i ≤ j such that m j (U) ≤ mi (V ).
Note that it is sufficient to verify the condition in Definition 7.29 for j = 1, . . . , maxlevel(U). For
j > maxlevel(U) we get m j (U) = 0 and the inequality trivially holds.
It is immediate that U -m V implies m(U) ≤ m(V ), but the relation -m gives us more information
than that. The usual inequality m(U) ≤ m(V ) holds if and only if for every j we can find an i such that
m j (U) ≤ mi (V ), but in the definition of -m we are restricted to finding such an index i that is less than
or equal to j. So not only is m(U) ≤ m(V ) globally, but we can also explain locally at each level, by
“looking downwards,” why U has smaller measure than V .
In Example 7.26, X1 6-m X2 since the relative cheapness of X1 compared to X2 is explained not by
a lot of vertices in X2 on low levels, but by one single high-level, and therefore expensive, vertex in X2
which is far above X1 . This is why these sets behave badly under union. If we have two sets X1 and X2
with X1 -m X2 , however, reversals of measure inequalities when taking unions as in Example 7.26 can no
longer occur.
Lemma 7.30 (Lemma 3.4 in [42]). If U -m V and Y ∩ V = 0,
/ then m(Y ∪ U) ≤ m(Y ∪ V ).
Proof. To show that m(Y ∪ U) ≤ m(Y ∪ V ), for each level j = 1, . . . , maxlevel(Y ∪ U) we want to find
a level i such that m j (Y ∪ U) ≤ mi (Y ∪ V ). We pick the i ≤ j provided by the definition of U -m V such
that m j (U) ≤ mi (V ). Since V ∩ W = 0/ and i ≤ j implies Y { j} ⊆ Y { i}, we get
m j (Y ∪ U) = j + 2 · |(U ∪ Y ){ j}| ≤ j + 2 · |U{ j}| + 2 · |Y { j}| ≤
i + 2 · |V { i}| + 2 · |Y { i}| = mi (Y ∪ V ) (7.8)
and the lemma follows.
So when locally improving a hiding set U that does not satisfy the LHC property to some set U ∗ that
does, if we can take care that U ∗ -m U in the sense of Definition 7.29 we get the local LHC property. All
that remains is to show that this can indeed be done.
When “improving” U to U ∗ , we will strive to pick hiding sets of minimal size. The next definition
makes this precise.
Definition 7.31. For any set of vertices X, let
L j (X) = min{|Y | : X{ j} ⊆ VY W and Y { j} = Y }
denote the size of a smallest set Y such that all vertices in Y are on level j or higher and Y hides all
vertices in X on level j or higher.
Note that we only require of Y to hide X{ j} and not all of X. Given the condition that Y = Y { j},
this set cannot hide any vertices in X{≺ j}. We make a few easy observations.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 522
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Observation 7.32. Suppose that X is a set of vertices in a layered graph G. Then:
1. L0 (X) is the minimal size of any hiding set for X.
2. If X ⊆ Y , then L j (X) ≤ L j (Y ) for all j.
3. It always holds that L j (X) ≤ |X{ j}| ≤ |X|.
Proof. Part 1 follows from the fact that V { 0} = V for any set V . If X ⊆ Y , then X{ j} ⊆ Y { j} and
any hiding set for X{ j} works also for Y { j}, which yields part 2. Part 3 holds since X{ j} ⊆ X is
always a possible hiding set for itself.
For any vertex set V in any layered graph G, we can always find a set hiding V that has “minimal
cardinality at each level” in the sense of Definition 7.31.
Lemma 7.33 (Lemma 3.5 in [42]). For any vertex set V we can find a hiding set V ∗ such that V ∗ { j} ≤
L j (V ) for all j, and either V ∗ = V or |V ∗ | < |V |.
Proof. If |V { j}| ≤ L j (V ) for all j, we can choose V ∗ = V . Suppose this is not the case, and let
k be minimal such that |V { k}| > Lk (V ). Let V 0 be .a minimum-size hiding set for V { k} with
V 0 = V 0 { k} and V 0 = |Lk (V )| and set V ∗ = V {≺ k} ∪V 0 . Since V {≺ k} hides itself (any set does),
.
we have that V ∗ hides V = V {≺ k} ∪V { k} and that
V ∗ = |V {≺ k}| + |V 0 | < |V {≺ k}| + |V { k}| = |V | . (7.9)
Combining (7.9) with part 1 of Observation 7.32, we see that the minimal index found above must be
k = 0. Going through the same argument as above again, we see that V ∗ { j} ≤ L j (V ) for all j, since
otherwise (7.9) would yield a contradiction to the fact that V 0 = V 0 { 0} was chosen as a minimum-size
hiding set for V .
We noted above that L0 (X) is the cardinality of a minimum-size hiding set of X. For j > 0, the
quantity L j (X) is large if one needs many vertices on level ≥ j to hide X{ j}, i. e., if X{ j} is “spread
out” in some sense. Let us consider a pyramid graph and suppose that X is a tight and hiding-connected
set in which the level-difference maxlevel(X) − minlevel(X) is large. Then it seems that |X| should also
have to be large, since the pyramid “fans out” so quickly. This intuition might be helpful when looking at
the next, crucial definition of Klawe.
Definition 7.34 (Spreading graph). We say that the layered DAG G is a spreading graph if for every
(non-empty) hiding-connected set X in G and every level j = 1, . . . , maxlevel(VXW), the spreading
inequality
|X| ≥ L j (VXW) + j − minlevel(X) (7.10)
holds.
Let us try to give some more intuition for Definition 7.34 by considering two extreme cases in a
pyramid graph:
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 523
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
• For j ≤ minlevel(X), we have that the term j − minlevel(X) is non-positive, X{ j} = X, and
VX{ j}W = VXW. In this case, (7.10) is just the trivial fact that no set that hides VXW need be
larger than X itself.
• Consider j = maxlevel(VXW), and suppose that VX{ j}W is a single vertex x with X TxU = X.
Then (7.10) requires that |X| ≥ 1 + level(x) − minlevel(X), and this can be proven to hold by the
“converging paths” argument of Theorem 7.3 and Observation 7.5.
Very loosely, Definition 7.34 says that if X contains vertices at low levels that help to hide other vertices
at high levels, then X must be a large set. Just as we tried to argue above, the spreading inequality (7.10)
does indeed hold for pyramids.
Theorem 7.35 ([42]). Pyramids are spreading graphs.
Unfortunately, the proof of Theorem 7.35 in [42] is rather involved. The analysis is divided into two
parts, by first showing that a class of so-called nice graphs are spreading, and then demonstrating that
pyramid graphs are nice. We refer to the original paper for the details. An alternative proof, which uses a
more direct argument focusing specifically on pyramids and which might be of independent interest, can
be found in [48].
Accepting Theorem 7.35 on faith, we are ready for the decisive lemma: If our layered DAG is
a spreading graph and if U ∪ W is a hiding-connected set hiding B such that U is too large for the
conditions in the local limited hiding-cardinality property (Property 7.27) to hold, then replacing U by the
minimum-size hiding set in Lemma 7.33 we get a hiding set in accordance with the local LHC property.
Lemma 7.36 (Lemma 3.6 in [42]). Suppose that B,W,U are vertex sets in a layered spreading graph G
such that U ∪ W hides B and is tight and hiding-connected. Then there is a vertex set U ∗ such that
U ∗ ∪ W hides B, U ∗ -m U, and either U ∗ = B or |U ∗ | < |B| + |W |.
Postponing the proof of Lemma 7.36 for a moment, let us note that if we combine this lemma with
Lemma 7.30 and Theorem 7.35, the local limited hiding-cardinality property for pyramids follows.
Corollary 7.37. Pyramid graphs have the local limited hiding-cardinality property (Property 7.27).
Proof of Corollary 7.37. This is more or less immediate, but we write down the details for completeness.
Since pyramids are spreading by Theorem 7.35, Lemma 7.36 says that U ∗ is a hiding set for (B,W ) and
that U ∗ -m U. Lemma 7.30 then yields that m(Y ∪ U ∗ ) ≤ m(Y ∪ U) for all Y with Y ∩ U = 0. / Finally,
Lemma 7.36 also tells us that U ∗ ⊆ B or |U ∗ | < |B| + |W |, and thus all conditions in Property 7.27 are
satisfied.
Continuing by plugging Corollary 7.37 into Lemma 7.28, we get the global LHC property in
Theorem 7.25 on page 520. So all that is needed to conclude Klawe’s proof of the lower bound for
the black-white pebbling price of pyramids is to prove Theorem 7.35 and Lemma 7.36. We attend to
Lemma 7.36 right away but in order to save space we skip the proof of Theorem 7.35 here and instead
refer the reader to the exposition in [48].
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 524
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Proof of Lemma 7.36. If |U| < |B| + |W | we can pick U ∗ = U and be done, so suppose that |U| ≥
|B| + |W |. Intuitively, this should mean that U is unnecessarily large, so it ought to be possible to do
better. In fact, U is so large that we can just ignore W and pick a better U ∗ that hides B all on its own.
Namely, let U ∗ be a minimum-size hiding set for B as in Lemma 7.33. Then either U ∗ = B or
U < |B| ≤ |B| + |W |. To prove the lemma, we also need to show that U ∗ -m U, which will guarantee
∗
that U ∗ behaves well under union with other sets with respect to measure.
Before we do the the formal calculations, let us try to provide some intuition for why
it should be the
case that U ∗ -m U holds, i. e., that for every j we can find an i ≤ j such that m j U ∗ ≤ mi (U). Perhaps
it will be helpful at this point for the reader to look at Example 7.19 again, where the replacement of
U1 = {v1 , u2 , u3 , v3 } in Figure 10(a) by U1∗ = {x1 , y1 } in Figure 10(b) shows Lemmas 7.33 and 7.36 in
action.
Suppose first that j ≤ minlevel(U ∪W ) ≤ minlevel(U). Then the inequality m j (U ∗ ) ≤ m j (U) is
obvious, since U{ j} = U is so large that it can easily pay for all of U ∗ , let alone U ∗ { j} ⊆ U ∗ .
For j > minlevel(U ∪ W ), however, we can worry that although our hiding set U ∗ does indeed have
small size, the vertices in U ∗ might be located on high levels in the graph and be very expensive since
they were chosen without regard to measure. Just throwing away all white pebbles and picking a new set
U ∗ that hides B on its own is quite a drastic move, and it is not hard to construct examples where this is
very bad in terms of potential (say, exchanging s5 for v5 in the hiding set of Example 7.19). The reason
that this nevertheless works is that |U| is so large, that, in addition, U ∪ W is hiding-connected, and that,
finally, the graph under consideration is spreading. Thanks to this, if there are a lot of expensive vertices
in U ∗ { j} on or above some high level j resulting in a large partial measure m j U ∗ , the number of
vertices on or above level L = minlevel(U ∪W ) in U = U{ L} is large enough to yield at least as large
a partial measure mL U .
Let us do the formal proof, divided into the two cases above.
1. j ≤ minlevel(U ∪ W ): Using the lower bound on the size of U and that level j is no higher than
the minimal level of U, we get
m j U ∗ = j + 2 · U ∗ { j} by definition of m j (·)
≤ j + 2 · U∗
since V { j} ⊆ V for any V
by construction of U ∗ in Lemma 7.33
≤ j + 2 · |B|
≤ j + 2 · |U| by assumption |U| ≥ |B| + |W | ≥ |B|
= j + 2 · U{ j} U{ j} = U since j ≤ minlevel(U)
= m j (U) by definition of m j (·)
and we can choose i = j in Definition 7.29.
2. j > minlevel(U ∪ W ): Let L = minlevel(U ∪ W ). The black pebbles in B are hidden by U ∪ W ,
or in formal notation B ⊆ VU ∪ W W, so
L j (B) ≤ L j VU ∪ W W (7.11)
holds by part 2 of Observation 7.32. Moreover, U ∪ W is a hiding-connected set of vertices
in a spreading graph G, so the spreading inequality in Definition 7.34 says that |U ∪ W | ≥
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 525
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
L j VU ∪ W W + j − L, or
j + L j VU ∪ W W ≤ L + |U ∪ W | (7.12)
after reordering. Combining (7.11) and (7.12) we have that
j + L j (B) ≤ L + |U ∪ W | (7.13)
and it follows that
m j (U ∗ ) = j + 2 · U ∗ { j} by definition of m j (·)
≤ j + U ∗ { j} + U ∗
since V { j} ⊆ V for any V
by construction of U ∗ in Lemma 7.33
≤ j + L j (B) + |B|
≤ L + |U ∪ W | + |B| by the inequality (7.13)
≤ L + 2 · |U| by assumption |U| ≥ |B| + |W |
= L + 2 · |U{ L}| U{ L} = U since L ≤ minlevel(U)
= mL (U) by definition of mL (·) .
Thus, the partial measure of U at the minimum level L is always larger than the partial measure of
U ∗ at levels j above this minimum level, and we can choose i = L in Definition 7.29.
Consequently, U ∗ -m U, and the lemma follows.
Thereby, the proof of the lower bound on the black-white pebbling price of pyramid graphs in
Theorem 7.14 on page 516 is complete.
Concluding this subsection, we want to make a comment about Lemmas 7.33 and 7.36 and try to
rephrase what they say about hiding sets. Given a tight set U ∪ W such that B ⊆ VU ∪ W W, we can always
pick a U ∗ as in Lemma 7.33 with U ∗ = B or U ∗ < |B| + |W | and with U ∗ { j} ≤ L j (B) for all j.
This will sometimes be a good idea, and sometimes not. Just as in Lemma 7.36, for j > minlevel(U ∪ W )
we can always prove that
m j (U ∗ ) ≤ minlevel(U ∪ W ) + |U| + (|B| + |W |) . (7.14)
The key message of Lemma 7.36 is that replacing U by U ∗ is a good idea if U is sufficiently large, namely
if |U| ≥ |B| + |W |, in which case we are guaranteed to get m j (U ∗ ) ≤ mL (U) for L = minlevel(U ∪ W ).
8 A tight bound for blob-pebbling the pyramid
Inspired by Klawe’s ideas in the previous section for the standard black-white pebble game, we want
to prove a similar result for our new blob-pebble game. In this section, we do so by showing that
for all layered DAGs Gh of height h that are spreading (in the sense of Definition 7.34), it holds that
Blob-Peb(Gh ) = Θ(h). In particular, this bound holds for pyramids Πh .
The constant factor that we get in our lower bound is moderately small and explicit. In fact, we believe
that it should hold that Blob-Peb(Gh ) ≥ h/2 + O(1) for layered spreading graphs Gh of height h, just as
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 526
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
in the standard black-white pebble game, but we have not been able to prove this. The multiplicative
constant in the proof in this section can improved with a minor effort, but we have not made any real
attempt to optimize the calculations since it seems clear that some additional idea would be needed to
push the constant all the way up to 1/2.
8.1 Definitions and notation for the blob-pebbling price lower bound
Recall that a vertex set U hides a black pebble on b if it blocks all source paths visiting v. We want to
extend this definition to blobs B. While this might not be a priori entirely obvious, it turns out to be
fruitful to do so by requiring that U should block all paths going through all of B. We remind the reader
about the terminology and notation from Definition 4.4 that a black blob B and a path P agree with each
other, or that P is a path via B, if B ⊆ P, and that Pvia (B) denotes the set of all source paths agreeing
with B.
Definition 8.1 (Blocked black blob). A vertex set U blocks a blob B if U blocks all P ∈ Pvia (B).
Note, in particular, that this means that a blob B that is not a chain is vacuously blocked even by
the empty set, since Pvia (B) = 0/ in this case (i. e., there is no path agreeing with B). Again, while we
do not claim that this is obvious, when working with the blob-pebble game one can actually develop
a certain intuition why non-chain blobs should be fairly useless. Definition 8.1 captures this intuition
by specifying that there will be no need to block this kind of blobs when we lift Klawe’s proof to the
blob-pebble game.5
A terminological aside: Recalling the discussion in the beginning of Section 7.2, it seems natural to
say that U blocks a black blob B rather than hides it, since standing at the sources we might “see” the
beginning of B, but if we try to walk any path via B we will fail before reaching the top of B since U
blocks the path. This distinction between hiding and blocking will turn out to be an important one in our
lower bound proof for blob-pebbling price. Of course, if B is an atomic black pebble, i. e., |B| = 1, the
hiding and blocking relations coincide.
Let us next define what it means to block a blob-pebbling configuration.
Definition 8.2 (Unblocked paths). For [B]hW i an blob subconfiguration, the set of unblocked paths for
[B]hW i is
unblocked([B]hW i) = {P ∈ Pvia (B) | W does not block P}
and we say that U blocks [B]hW i if U blocks all paths in unblocked([B]hW i). We say that U blocks the
blob-pebbling configuration S if U blocks all [B]hW i ∈ S. If so, we say that U is a blocker of [B]hW i or S,
respectively, or a blocking set for [B]hW i or S.
Comparing to Section 7.2, note that when blocking a path P ∈ Pvia (B), U can only use the white
pebbles W that are associated with B in [B]hWi. Although there might be white pebbles from other subcon-
figurations [B0 ]hW 0 i 6= [B]hWi that would be really helpful, U cannot enlist the help of the white pebbles
5 In fact, in the preliminary version [50] of this paper, black blobs were declared to be chains by definition. However, while
this was, and is, in some sense intuitively more appealing, it turned out to lead to a number of technical difficulties that are more
easily overcome or even entirely avoided by letting blobs span any set of vertices, chains or not.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 527
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
in W 0 when blocking B. The reason for defining the blocking relation in this way is that these white
pebbles can suddenly disappear due to pebbling moves performed on such subconfigurations [B0 ]hW 0 i.
Reusing the definition of measure in Definition 7.8 on page 512, we generalize the concept of potential
in Definition 7.9 to blob-pebbling configurations as follows.
Definition 8.3 (Blob-pebbling potential). The potential of a blob-pebbling configuration S is
pot(S) = min{m(U) : U blocks S} .
If U is such that U blocks S and U has minimal measure m(U) among all blocking sets for S, we say that
U is a minimum-measure blocking set for S.
To compare blob-pebbling potential with the black-white pebbling potential in Definition 7.9, consider
the following examples with vertex labels as in Figures 7 and 9–11.
Example 8.4. For the blob-pebbling configuration S = [z]hy1 i, [z]hy2 i , the minimum-measure blocking
set is U = {z}. In comparison, the standard black-white pebble configuration P = (B,W ) = ({z}, {y1 , y2 })
has U = 0/ as minimum-measure hiding set.
Example 8.5. For the blob-pebbling configuration S = [z]h0i, / [y1 ]hx1 , x2 i , the minimum-measure
blocker is again U = {z}. In comparison, for the standard black-white pebble configuration P = (B,W ) =
({z, y1 }, {x1 , x2 }) we have the minimum-measure hiding set U = {x3 }.
Remark 8.6. Perhaps it is also worth pointing out that Definition 8.3 is indeed a strict generalization
of Definition 7.9. Given a black-white pebble configuration P = (B,W ) we can construct an equivalent
blob-pebbling configuration S(P) with respect to potential by setting
S(P) = b W ∩ GMb b ∈ B
(8.1)
but as the examples above show going in the other direction is not possible.
Since we have accumulated a number of different minimality criteria for blocking sets, let us pause to
clarify the terminology:
• The vertex set U is a subset-minimal, or just minimal, blocking set for the blob-pebbling configura-
tion S if no strict subset U 0 $ U is a blocking set for S.
• U is a minimum-measure blocking set for S if it has minimal measure among all blocking sets for
S (and thus yields the potential of S).
• U is a minimum-size blocking set for S if it has minimal size among all blocking sets for S.
Note that we can assume without loss of generality that minimum-measure and minimum-size blockers
are both subset-minimal, since throwing away superfluous vertices can only decrease the measure and
size, respectively. However, minimum-measure blockers need not have minimal size and vice versa.
For a simple example
of this, consider (with vertex labels as in Figures 7 and 9–11) the blob-pebbling
configuration S = [z]hw3 , w4 i and the two blocking sets U1 = {z} and U2 = {w1 , w2 }.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 528
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
8.2 A lower bound assuming an extension of the LHC property
When we want to prove lower bounds on the blob-pebbling price of layered graphs, a useful generalization
of Property 7.11 on page 513 turns out to be the following.
Property 8.7 (Generalized limited hiding-cardinality property). We say that a blob-pebbling configura-
tion S on a layered DAG G has the generalized limited hiding-cardinality property with parameter K if
there is a vertex set U such that
1. U blocks S,
2. pot(S) = m(U), i. e., U is a minimum-measure blocker of S,
3. |U| ≤ K · cost(S).
For brevity, in what follows we will just refer to this as the generalized LHC property.
We say that the graph G has the generalized LHC property with parameter K if all blob-pebbling
configurations S on G have the generalized LHC property with parameter K.
When the parameter K is clear from context, we will just write that S or G has the generalized LHC
property.
We claim that for all layered DAGs Gh of height h that have the generalized LHC property and are
spreading, it holds that Blob-Peb(Gh ) = Θ(h). The proof of this fact is very much in the spirit of the
proofs of Lemma 7.12 and Theorem 7.14, although the details are slightly more complicated.
Theorem 8.8 (Analogue of Theorem 7.14). Suppose that Gh is a layered DAG of height h possessing
the generalized LHC
property (Property 8.7) with some fixed parameter K. Then for any unconditional
blob-pebbling P = S0 = 0,
/ S1 , . . . , Sτ of Gh it holds that
pot(St ) ≤ (2K + 1) · max{cost(Ss )} . (8.2)
s≤t
In particular, for any family of layered DAGs Gh that are also spreading in the sense of Definition 7.34,
we have Blob-Peb(Gh ) = Θ(h).
We make two separate observations before presenting the proof.
Observation 8.9. For any layered DAG Gh of height h it holds that Blob-Peb(Gh ) = O(h).
Proof. Any layered DAG Gh can be black-pebbled with h + O(1) pebbles as noted in Theorem 7.2, and
it is easy to see that a blob-pebbling can mimic a black pebbling in the same cost.
Observation 8.10. If Gh is a layered DAG of height h that is spreading in the sense of Definition 7.34,
then potGh ([z]h0i)
/ = h + 2.
Proof. The proof is fairly similar to the corresponding case for pyramids in Lemma 7.13. Note, though,
that in contrast to Lemma 7.13, here we cannot get the statement from the generalized LHC property, but
instead have to prove it directly.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 529
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Since [z] is an atomic blob, the blocking and hiding relations coincide. The set U = {z} hides itself
and has measure h + 2. We show that any other blocking set must have strictly larger measure.
Suppose that z is hidden by some vertex set U 0 6= {z}. This U 0 is minimal without loss of gener-
ality. In particular, we can assume that U 0 is tight in the sense of Definition 7.15 and that 0 0
U = U TzU.
0 0
Then by Corollary 7.23 it holds that U is hiding-connected. Letting L = minlevel U and setting
j = h in the spreading inequality (7.10), we get that U 0 ≥ 1 + h − L and hence m U 0 ≥ mL U 0 ≥
L + 2(1 + h − L) = 2h − L + 2 > h + 2 since L < h.
Proof of Theorem 8.8. The statement in the theorem follows from Observations 8.9 and 8.10 combined
with the inequality (8.2), so just as for Theorem 7.14 the crux of the matter is the induction proof needed
to get this inequality.
Suppose that Ut is such that it blocks St and pot(St ) = m(Ut ). By the inductive hypothesis, we
have that pot(St ) ≤ (2K + 1) · maxs≤t {cost(Ss )}. We want to show for St+1 that pot(St+1 ) ≤ (2K + 1) ·
maxs≤t+1 {cost(Ss )}. Clearly, this follows if we can prove that
pot(St+1 ) ≤ max{pot(St ), (2K + 1) · cost(St )} . (8.3)
We also note that if Ut blocks St+1 we are done, since if so pot(St+1 ) ≤ m(Ut ) = pot(St ).
We make a case analysis depending on the type of move in Definition 4.6 made to get from St to St+1 .
Observe that a technical complication here is that multiple mergers, inflations and erasures can be joined
into one single blob-pebbling move (potentially to avoid paying for expensive intermediate blob-pebbling
configurations), so our proof has to work regardless of how pebbling steps are combined into moves.
This is not really a problem, however. We show below that if S0 S is a pebbling step and U 0
0 0
blocks S , then U also blocks S as long as the pebbling step is not an introduction (just as in the proof
of Lemma 7.12). Therefore, the only case we have reason to worry about is when the pebbling makes
an introduction move—in fact, an introduction move on a source vertex—and for such moves we will
use the generalized LHC property to prove the bound that we need. That is, what we do is in effect to
prove (8.2) but with the maximum on the right-hand side taken only over subconfigurations resulting
from introduction moves. Clearly, this stronger inequality is sufficient to establish the theorem. The
formal proof follows.
Erasure S = S0 \ [B]hWi for [B]hWi ∈ S0 . If U 0 blocks S0 , then obviously U 0 blocks S ⊆ S0 .
Inflation S = S0 ∪ [B]hWi for [B]hWi inflated from some [B0 ]hW 0 i ∈ S0 such that B0 ⊆ B and W 0 ⊆ W .
Again we claim that if U 0 blocks S0 , then U 0 blocks [B]hWi and thus all of S. To see this, suppose
that P is any source path agreeing with B. Then this path also agrees with B0 , and so must be
blocked by U 0 ∪ W 0 by assumption. Hence, it is certainly blocked by U 0 ∪ W ⊇ U 0 ∪ W 0 .
Merger S = S0 ∪ [B]hWi for [B]hWi derived by merger of [B1 ]hW1 i, [B2 ]hW2 i ∈ S0 such that
B1 ∩ W2 = 0/ , (8.4a)
∗
B2 ∩ W1 = {v } , (8.4b)
∗
B = (B1 ∪ B2 ) \ {v } , and (8.4c)
∗
W = (W1 ∪ W2 ) \ {v } . (8.4d)
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 530
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Let us prove that if a set of vertices U 0 blocks two subconfigurations [B1 ]hW1 i and [B2 ]hW2 i, then
it must also block their merger. We have two cases. First, let P be any path via B, and suppose
in addition that P visits the merger vertex v∗ . If so, P agrees with B2 and must be blocked by
U 0 ∪ W2 by assumption. If on the other hand P agrees with B but does not visit v∗ , then it is a
path via B1 that in addition does not pass through the white pebble v∗ in W1 eliminated in the
merger. This means that U 0 ∪ (W1 \ {v∗ }) must block P. In both cases we see that P is blocked by
U 0 ∪ (W1 \ {v∗ }) ∪ W2 = U 0 ∪ (W1 ∪ W2 ) \ {v∗ }.
Introduction St+1 = St ∪ [v]hpred(v)i . (Note that since introduction steps are always pebbling moves,
we write St and St+1 here instead of S0 and S.) Clearly, Ut blocks St+1 if v is a non-source vertex,
i. e., if pred(v) 6= 0,
/ since Ut blocks St and [v]hpred(v)i blocks itself. Hence, the only introduction
moves we have to consider are for source vertices v, so that the subconfiguration introduced
is [v]h0i.
/
As in the proof of Lemma 7.12, Ut does not necessarily block St+1 any longer but Ut+1 = Ut ∪ {v}
clearly does. For j > 0, it holds that Ut+1 { j} = Ut { j} and thus m j (Ut+1 ) = m j (Ut ). On the
bottom level j = 0, using that |Ut | ≤ K · cost(St ) by generalized LHC property (Property 8.7) we
have
m0 (Ut+1 ) = 2 · |Ut+1 | = 2 · (|Ut | + 1) ≤
2 · K · cost(St ) + 1 ≤ 2 · K · cost(St+1 ) + 1 ≤
2 · K · cost(St+1 ) + cost(St+1 ) ≤ 2(K + 1) · cost(St+1 ) (8.5)
and we get that
pot(St+1 ) ≤ m(Ut+1 ) ≤ max j m j (Ut+1 )
≤ max m(Ut ), (2K + 1) · cost(St+1 ) =
max pot(St ), (2K + 1) · cost(St+1 ) (8.6)
which is what is needed for the induction step to go through.
We see that regardless of the pebbling move(s) made in the transition St St+1 , the inequality (8.3)
holds. The theorem follows by the induction principle.
Now in order to prove a lower bound on Blob-Peb(Gh ) for layered spreading graphs Gh , all that
remains is to find some constant K such that these DAGs can be shown to possess the generalized LHC
property (Property 8.7) with parameter K. We do so in Sections 8.3 and 8.4 below.
8.3 Some structural transformations
As we tried to indicate by presenting the small toy blob-pebbling configurations in Examples 8.4 and 8.5,
the potential in the blob-pebble game behaves somewhat differently from the potential in the standard
pebble game. There are (at least) two important differences:
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 531
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
• Firstly, for the white pebbles we have to keep track of exactly which black pebbles they can help to
block. This can lead to slightly unexpected consequences such as the blocking set U and the set of
white pebbles overlapping.
• Secondly, for black blobs there is a much wider choice where to block the blob-pebbles than for
atomic pebbles. It seems that to minimize the potential, blocking black blobs on (reasonably) low
levels should still be a good idea. However, we cannot a priori exclude the possibility that if a lot
of black blobs intersect in some high-level vertex, adding this vertex to a blocking set U might be a
better idea.
In this subsection we address the first of these issues. The second issue, which turns out to be much
trickier, is dealt with in the next subsection.
One simplifying observation is that we do not have to prove Property 8.7 for arbitrary blob-pebbling
configurations. Below, we show that one can do some technical preprocessing of the blob-pebbling
configurations so that it suffices to prove the generalized LHC property for the subclass of configurations
resulting from this preprocessing.6 Throughout this subsection, we assume that the parameter K is some
fixed constant.
We start gently by taking care of a pretty obvious redundancy. Let us say that the blob subconfigu-
ration [B]hWi is self-blocking if W blocks B. The blob-pebbling configuration S is self-blocker-free if
there are no self-blocking subconfigurations in S. That is, if [B]hWi is self-blocking, W needs no extra
help blocking B. Perhaps the simplest example of this is [B]hWi = [v]hpred(v)i for a non-source vertex v.
Another example of a self-blocking subconfiguration [B]hWi is when B is not a chain, as discussed after
Definition 8.1. The following proposition is immediate.
Proposition 8.11. For S any blob-pebbling configuration, let S0 be the blob-pebbling configuration with
all self-blockers in S removed. Then cost(S0 ) ≤ cost(S), pot(S0 ) = pot(S) and any blocking set U 0 for S0
is also a blocking set for S.
Corollary 8.12. Suppose that the generalized LHC property holds for self-blocker-free blob-pebbling
configurations. Then the generalized LHC property holds for all blob-pebbling configurations.
Proof. If S is not self-blocker-free, take the maximal S0 ⊆ S that is and the blocking set U 0 that the
generalized LHC property provides for this S0 . Then U 0 blocks S and since the two configurations S
and S0 have the same blocking sets their potentials are equal, so pot(S) = m(U 0 ). Finally, we have that
|U| ≤ K · cost(S0 ) ≤ K · cost(S). Thus the generalized LHC property holds for S.
Observe that this means that in what follows, we can without loss of generality assume that all
blob-pebbles B are chains. In particular, we can assume (by mild abuse of notation) that bot(B) is not a
set but a single well-defined vertex.
We now move on to a more interesting observation. Looking at S = [z]hy1 i, [z]hy2 i in Example 8.4,
it seems that the white pebbles really do not help at all. One might ask if we could not just throw them
6 Note that we did something similar in Section 7.3 after Lemma 7.18, when we argued that if U is a minimum-measure
hiding set for P = (B,W ), we can assume without loss of generality that U ∪ W is tight. For if not, we just prove the limited
hiding-cardinality property for some tight subset U 0 ∪ W 0 ⊆ U ∪ W instead. This is completely analogous to the reasoning here,
but since matters become more complex we need to be a bit more careful.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 532
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
away? Perhaps somewhat surprisingly, the answer is yes, and we can capture the intuitive concept of
necessary white pebbles and formalize it as follows in the definitions below.
Definition 8.13 (White sharpening). Given S = [Bi ]hWi i i∈[m] , we say that S0 is a white sharpening of
S if S0 = [B0i ]hWi0 i i∈[m] for B0i = Bi and Wi0 ⊆ Wi .
That is, a white sharpening removes white pebbles and thus makes the blob-pebbling configuration
stronger or “sharper” in the sense that the cost can only decrease and the potential can only increase.
Proposition 8.14. If S0 is a white sharpening of S it holds that cost(S0 ) ≤ cost(S) and pot(S0 ) ≥ pot(S).
More precisely, any blocking set U 0 for S0 is also a blocking set for S.
Proof. The statement about cost is immediate from Definition 4.7. The statement about potential clearly
follows from Definition 8.3 since it holds that any blocking set U 0 for S0 is also a blocking set for S.
In the next definition, we suppose that there is some fixed but arbitrary ordering of the vertices in G,
and that the vertices are considered in this order.
Definition 8.15 (White elimination). For [B]hWi a blob subconfiguration and U any blocking set for
[B]hWi, write W = {w1 , . . . , ws }, set W 0 := W and iteratively perform the following for i = 1, . . . , s: If
U ∪ (W i−1 \ {wi }) blocks B, set W i := W i−1 \ {wi }, otherwise set W i := W i−1 . We define the white
elimination of [B]hWi with respect to U to be W-elim([B]hWi,U) = [B]hW s i for W s the final set resulting
from the procedure above.
For S a blob-pebbling configuration and U a blocking set for S, we define
W-elim(S,U) = W-elim([B]hWi,U) [B]hWi ∈ S .
(8.7)
We say that the elimination is strict if S 6= W-elim(S,U). If S = W-elim(S,U) we say that S is white-
eliminated, or W-eliminated for short, with respect to U.
Clearly W-elim(S,U) is a white sharpening of S. And if we pick the right U, we simplify the problem
of proving the generalized LHC property a bit more.
Lemma 8.16. If U is a minimum-measure blocking set for S, then S0 = W-elim(S,U) is a white sharpen-
ing of S such that pot(S0 ) = pot(S) and U blocks S0 .
Proof. Since S0 = W-elim(S,U) is a white sharpening of S (which is easily verified from Definitions 8.13
and 8.15), it holds by Proposition 8.14 that pot(S0 ) ≥ pot(S). Looking at the construction in Defini-
tion 8.15, we also see that the white pebbles are “sharpened away” with care so that U remains a blocking
set. Thus m(U) ≥ pot(S0 ) = pot(S) = m(U), and the lemma follows.
Corollary 8.17. Suppose that the generalized LHC property holds for the set of all blob-pebbling con-
figurations S having the property that for all minimum-measure blocking sets U for S it holds that
S = W-elim(S,U). Then the generalized LHC property holds for all blob-pebbling configurations.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 533
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Proof. This is essentially the same reasoning as in the proof of Corollary 8.12 plus induction. Let S
be any blob-pebbling configuration. Suppose that there exists a minimum-measure blocker U for S
such that S is not W-eliminated with respect to U. Let S1 = W-elim(S,U). Then cost(S1 ) ≤ cost(S) by
Proposition 8.14 and pot(S1 ) = pot(S) by Lemma 8.16.
If there is a minimum-measure blocker U 1 for S1 such that S1 is not W-eliminated with respect to U 1 ,
set S2 = W-elim(S1 ,U 1 ). Continuing in this manner, we get a chain S1 , S2 , S3 , . . . of strict W-eliminations
such that cost(S1 ) ≥ cost(S2 ) ≥ cost(S3 ) . . . and pot(S1 ) = pot(S2 ) = pot(S3 ) = . . . This chain must
terminate at some configuration Sk since the total number of white pebbles (counted with repetitions)
decreases in every round.
Let U k be the blocker that the generalized LHC property provides for Sk . Then U k blocks S,
pot(S) = pot(Sk ) = m(U k ), and |U k | ≤ K · cost(Sk ) ≤ K · cost(S). Thus the generalized LHC property
holds for S.
We note that in particular, it follows from the construction in Definition 8.15 combined with Corol-
lary 8.17 that we can assume without loss of generality for any blocking set U and any blob-pebbling
configuration S that U does not intersect the set of white-pebbled vertices in S.
Proposition 8.18. If S = W-elim(S,U), then in particular it holds that U ∩ W(S) = 0.
/
Proof. Any w ∈ W(S) ∩ U would have been removed in the W-elimination.
8.4 Proof of the generalized limited hiding-cardinality property
We are now ready to embark on the proof of the generalized LHC property for layered spreading DAGs.
Theorem 8.19. All layered DAGs that are spreading possess the generalized limited hiding-cardinality
property (Property 8.7) with parameter K = 13.
Since pyramids are spreading graphs by Theorem 7.35, this is all that we need to get the lower bound
on blob-pebbling price on pyramids from Theorem 8.8. We remark that the parameter K in Theorem 8.19
can easily be improved with a little extra work. However, our main concern here is not optimality of
constants but clarity of exposition.
We prove Theorem 8.19 by applying the preprocessing in the previous subsection and then (almost)
reducing the problem to the standard black-white pebble game. However, some twists are added along the
way since our potential measure for blobs behave differently from Klawe’s potential measure for black
and white pebbles. Let us first exemplify two problems that arise if we try to naively mimic step by step
Klawe’s proof for the standard black-white pebble game.
The first problem is that in the standard black-white pebble game, if U is a minimum-measure hiding
set for P = (B,W ), Lemma 7.18 tells us that we can assume without loss of generality that U ∪ W is tight.
This is not true in the blob-pebble game, not even after the transformations in Section 8.3.
Example 8.20. Consider the configuration S = {[w1 ]hu2 , u3 i, [w4 , x3 ]hu4 , u5 i, [x2 , y2 , z]h0i}
/ with blocking
set U = {x2 , u1 , u6 } in Figure 12(a). It can be verified that U is a minimum-measure blocking set and that
the configuration S is W-eliminated with respect to U, but the set U ∪ W(S) = {u1 , u2 , u3 , u4 , u5 , u6 , x2 }
is not tight (because of x2 ).
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 534
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
z z
y1 y2 y1 y2
x1 x2 x3 x1 x2 x3
w1 w2 w3 w4 w1 w2 w3 w4
v1 v2 v3 v4 v5 v1 v2 v3 v4 v5
u1 u2 u3 u4 u5 u6 u1 u2 u3 u4 u5 u6
s1 s2 s3 s4 s5 s6 s7 s1 s2 s3 s4 s5 s6 s7
(a) Minimum-measure but non-tight blocking set. (b) Tight but non-connected blocker for blob.
Figure 12: Two blob-pebbling configurations with problematic blocking sets.
This can be handled, but a more serious second problem is that even if the set U ∪ W blocking the
chain B is tight, there is no guarantee that the vertices in U ∪ W end up in the same connected component
of the hiding set graph H(U ∪ W ) in Definition 7.20.
Example 8.21. Consider the single-blob configuration S = {[u5 , z]h0i} / in Figure 12(b). It is easy to
verify that U = {v4 , y2 } is a subset-minimal blocker of S and also a tight vertex set. This highlights the
fact that blocking sets for blob-pebbling configurations can have rather different properties than hiding
sets for standard pebbles. In particular, a minimal blocking set for a single blob can have several “isolated”
vertices at large distances from one another. Among other problems, this leads to difficulties in defining
connected components of blocking sets for subconfigurations.
The naive attempt to generalize Definition 7.20 of connected components in a hiding set graph to
blocking sets would place the vertices v4 and y2 in different connected components {v4 } and {y2 }, none
of which blocks S = {[u5 , z]h0i}.
/ This is not what we want (compare Corollary 7.23 for hiding sets for
black-white pebble configurations). We remark that there really cannot be any other sensible definition
that places v4 and y2 in the same connected component either, at least not if we want to appeal to the
spreading properties in Definition 7.34. Since the level difference in U is 3 but the size of the set is only 2,
the spreading inequality (7.10) cannot hold for this set.
To get around this problem, we will instead use connected components defined in terms of hiding the
singleton black pebbles given by the bottom vertices of our blobs. For a start, recalling Definitions 7.6
and 8.1, let us make an easy observation relating the hiding and blocking relations for a blob.
Observation 8.22. If a vertex set V hides some vertex b ∈ B, then V blocks B.
Proof. If V blocks all paths visiting b, then in particular it blocks the subset of paths that not only visits b
but agree with all of B.
We will focus on the case when the unique bottom vertex of a chain blob is hidden.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 535
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Definition 8.23 (Hiding blob-pebbling configurations). We say that the vertex set U hides the subcon-
figuration [B]hWi if B is a chain and U ∪ W hides the vertex bot(B). U is said to hide the blob-pebbling
configuration S if U hides all [B]hWi ∈ S.
If U does not hide [B]hW i, then U blocks [B]hW i only if U ∩ GO
bot(B) does.
Proposition 8.24. Suppose that a vertex set U in a layered DAG G blocks but does not hide the subcon-
bot(B)
figuration [B]hW i and that [B]hW i does not block itself. Then U ∩ GM does not block [B]hW i, but
there is a subset U 0 ⊆ U ∩ GO
bot(B) that blocks [B]hW i.
Proof. Suppose that U ∪ W blocks B but does not hide b = bot(B), and that W does not block B. Then
there is a source path P2 via B such that P2 ∩ W = 0.
/ Also, there is a source path P1 to b such that
P1 ∩ (U ∪ W ) = 0. b O
/ Let P = P1 ∩ GM ∪ P2 ∩ Gb be the source path that starts like P1 and continues
like P2 from b onwards. Clearly,
P ∩ U ∩ GMb ∪ W = P1 ∩ (U ∪ W ) ∪ P2 ∩ W = 0/
(8.8)
so U ∩ GMb does not block [B]hW i.
Suppose that U ∩ GO b does not block [B]hW i. Since U ∪ W does not hide b, there is some source
path P1 to b with P1 ∩ (U ∪ W ) = 0. / Also, since U ∪ W blocks B but U ∩ GO b ∪ W does not, there
is a source path P via B such that P ∩ (U ∪ W ) 6
= 0
/ but P ∩ (U ∪ W ) ∩ G O = 0.
/ But then let P =
2 2 2 b
b O
P1 ∩ GM ∪ P2 ∩ Gb be the source path that starts like P1 and continues like P2 from b onwards. We get
that P agrees with B and that P ∩ (U ∪ W ) = 0,
/ contradicting the assumption that U blocks [B]hW i.
We want to distinguish between subconfigurations that are hidden and subconfigurations that are just
blocked, but not hidden. To this end, let us introduce the notation
SH (S,U) = [B]hWi ∈ S U hides [B]hWi (8.9)
to denote the subconfigurations in S hidden by U and
SB (S,U) = S \ SH (S,U) (8.10)
to denote the subconfigurations that are just blocked. We write
BH (S,U) = {bot(B) | [B]hW i ∈ SH (S,U)} (8.11)
and
BB (S,U) = {bot(B) | [B]hW i ∈ SB (S,U)} (8.12)
to denote the black bottom vertices in these two subsets of subconfigurations and note that we can have
BH (S,U) ∩ BB (S,U) 6= 0. / The white pebbles in these subsets located below the bottom vertices of the
black blobs that they are supporting are denoted
WM b
H (S,U) = W ∩ GM [B]hW i ∈ SH (S,U), b = bot(B) (8.13)
and
WM b
B (S,U) = W ∩ GM [B]hW i ∈ SB (S,U), b = bot(B) . (8.14)
This notation will be used heavily in what follows, so we give a couple of simple but hopefully illuminating
examples before we continue.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 536
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
z z
y1 y2 y1 y2
x1 x2 x3 x1 x2 x3
w1 w2 w3 w4 w1 w2 w3 w4
v1 v2 v3 v4 v5 v1 v2 v3 v4 v5
u1 u2 u3 u4 u5 u6 u1 u2 u3 u4 u5 u6
s1 s2 s3 s4 s5 s6 s7 s1 s2 s3 s4 s5 s6 s7
(a) [s4 , y1 , z]hv2 i, [u3 , w3 ]hs3 i, [w4 , x3 ]hv5 i . / [w2 ,y1 ]hs3 ,u3 ,x1 i, [w4 ]hv5 i .
(b) [s4 ,v4 ,w3 ,x3 ,y2 ]h0i,
Figure 13: Examples of blob-pebbling configurations with hidden and just blocked blobs.
Example 8.25. Consider theblob-pebbling configurations and blocking sets in Figure 13. For the blob-
pebbling configuration S1 = [s4 , y1 , z]hv2 i, [u3 , w3 ]hs3 i, [w4 , x3 ]hv5 i with blocking set U1 = {v3 , v4 } in
Figure 13(a), the vertex set {v4 , v5 } hides w4 = bot([w4 , x3 ]) but [s4 , y1 , z] is blocked but not hidden by
{v2 , v3 , v4 } and [u3 , w3 ] is blocked but not hidden by {v3 }. Thus, we have
SH (S1 ,U1 ) = [w4 , x3 ]hv5 i
SB (S1 ,U1 ) = [s4 , y1 , z]hv2 i, [u3 , w3 ]hs3 i
BH (S1 ,U1 ) = {w4 }
BB (S1 ,U1 ) = {s4 , u3 }
WM
H (S1 ,U1 ) = {v5 }
WM
B (S1 ,U1 ) = {s3 }
in this example. For the configuration S2 = [s4 , v4 , w3 , x3 , y2 ]h0i, / [w2 , y1 ]hs3 , u3 , x1 i, [w4 ]hv5 i with
blocker U2 = {s2 , u4 , u5 } in Figure 13(b), it is straightforward to verify that
SH (S2 ,U2 ) = [w2 , y1 ]hs3 , u3 , x1 i, [w4 ]hv5 i
SB (S2 ,U2 ) = [s4 , v4 , w3 , x3 , y2 ]h0i
/
BH (S2 ,U2 ) = {w2 , w4 }
BB (S2 ,U2 ) = {s4 }
WM
H (S2 ,U2 ) = {s3 , u3 , v5 }
WM
B (S2 ,U2 ) = 0
/
are the corresponding sets.
Let us also use the opportunity to illustrate Definition 8.15. The blob-pebbling configuration S1 is
not W-eliminated with respect to U1 , since U1 also blocks this configuration with the white pebble on
s3 removed. However, a better idea measure-wise is to change the blocking set for S1 to U10 = {s4 , v4 },
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 537
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
which has measure m(U10 ) = 4 < 6 = m(U1 ). The vertex set U2 can be verified to be a minimum-measure
blocker for S2 , but when S2 is W-eliminated with respect to U2 the white pebble on x1 disappears.
For the rest of this section we will assume without loss of generality (in view of Proposition 8.11
and Corollary 8.17) that we are dealing with a blob-pebbling configuration S and a minimum-measure
blocker U of S such that S is free from self-blocking subconfigurations and is W-eliminated with respect
to U. As an aside, we note that it is not hard to show (using Definition 8.15 and Proposition 8.24) that
this implies that WM / We will tend to drop the arguments S and U for SH , SB , BH , BB , WM
B (S,U) = 0. H,
and WB , since from now on the blob-pebbling configuration S and the blocker U will be fixed. With this
M
notation, Theorem 8.19 clearly follows if we can prove the following lemma.
Lemma 8.26. Let S be any blob-pebbling configuration on a layered spreading DAG and U be any
blocking set for S such that
1. pot(S) = m(U), i. e., U is a minimum-measure blocker of S,
2. S is free from self-blocking subconfigurations and is W-eliminated with respect to U, and
3. U has minimal size among all blocking sets U 0 for S such that pot(S) = m(U 0 ).
Then |U| ≤ 13 · BH ∪ BB ∪ WM
H .
The proof is by contradiction, although we will have to work harder than for the corresponding
Theorem 7.25 for black-white pebbling and also use (the proof of) the latter theorem as a subroutine.
Thus, for the rest of this section, let us assume on the contrary that U has all the properties stated in
Lemma 8.26 but that |U| > 13 · BH ∪ BB ∪ WM H . We will show that this leads to a contradiction.
For the subconfiguration in SH that are hidden by U, one could argue that matters should be reasonably
similar to the case for standard black-white pebbling, and hopefully we could apply similar reasoning
as in Section 7.3 to prove something useful about the vertex set hiding these subconfigurations. The
subconfigurations in SB that are just blocked but not hidden, however, seem harder to get a handle on
(compare Example 8.21).
Let UH ⊆ U be a smallest vertex set hiding SH and let UB = U \UH . The set UB consists of vertices
that are not involved in any hiding of subconfigurations in SH , but only in blocking subconfigurations
in SB on levels above their bottom vertices. As a first step towards proving Lemma 8.26, and thus
Theorem 8.19, we want to argue that UB cannot be very large.
Consider the blobs in SB . By definition they are not hidden, but are blocked at some position
above level(bot(B)). Since the vertices in UB are located on high levels, a naive attempt to improve the
blocking set would be to pick some u ∈ UB and replace it by the vertices in BB corresponding to the
subconfigurations in SB that u is involved in blocking, i. e., by the set
Bu = bot(B) U \ {u} does not block [B]hWi ∈ SB .
(8.15)
Note that Bu is lower down in the graph than u, so (U \ {u}) ∪ Bu is obtained from U by moving vertices
downwards and by construction (U \ {u}) ∪ Bu blocks S. But by assumption, U has minimal potential
and cardinality, so this new blocking set cannot be an improvement measure- or cardinality-wise. The
same holds if we extend the construction to subsets U 0 ⊆ UB and the corresponding bottom vertices
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 538
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
0 0
BU ⊆ BB . By assumption we can never find any subset such that (U \ {U 0 }) ∪ BU is a better blocker
than U. It follows that the cost of the blobs that UB helps to block must be larger than the size of UB , and
in particular that |UB | ≤ |BB |. Let us write this down as a lemma and prove it properly.
Lemma 8.27. Let S be any blob-pebbling configuration on a layered DAG and U be any blocking set
for S such that pot(S) = m(U), U has minimal size among all blocking sets U 0 for S with pot(S) = m(U 0 ),
and S is free from self-blocking subconfigurations and is W-eliminated with respect to U. Then if UH ⊆ U
is any smallest set hiding SH and UB = U \UH , it holds that |UB | ≤ |BB |.
Before proving this lemma, we note the immediate corollary that if the whole blocking set U is
significantly larger than cost(S), the lion’s share of U by necessity consists not of vertices blocking
subconfigurations in SB , but of vertices hiding subconfigurations in SH . And recall that we are indeed
assuming, to get a contradiction, that U is large.
Corollary 8.28. Assume that S and U are as in Lemma 8.26 but with |U| > 13 · BH ∪ BB ∪ WM
H . Let
UH ⊆ U be a smallest set hiding SH . Then |UH | > 12 · BH ∪ BB ∪ WH .
M
As was indicated in the informal discussion preceding Lemma 8.27, the proof of the lemma uses the
easy observation that moving vertices downwards can only decrease the measure.
Observation 8.29. Suppose that U, V1 and V2 are vertex sets in a layered DAG such that U ∩ V2 = 0/ and
there is a one-to-one (but not necessarily onto) mapping f : V1 → V2 with the property that level(v) ≤
level( f (v)). Then m(U ∪ V1 ) ≤ m(U ∪ V2 ).
Proof. This follows immediately from Definition 7.8 on page 512 since the mapping f tells us that
|(U ∪ V1 ){ j}| ≤ |U{ j}| + |V1 { j}| ≤ |U{ j}| + | f (V1 { j})|
≤ |U{ j}| + |V2 { j}| ≤ |(U ∪ V2 ){ j}| (8.16)
for all j.
Proof of Lemma 8.27.. Note first that by Proposition 8.24, for every [B]hWi ∈ SB with b = bot(B) it holds
that U ∩ GO O
b = (UH ∪ UB ) ∩ Gb blocks [B]hWi. Therefore, all vertices in UB needed to block [B]hWi
O
can .be found in UB ∩ Gb . Rephrasing this slightly, the blob-pebbling configuration S is blocked by
UH ∪ UB ∩ b∈BB GO
S
b , and since U is subset-minimal we get that
O
UB = UB ∩
S
b∈BB Gb . (8.17)
Consider the bipartite graph with BB and UB as the left- and right-hand vertices, where the neighbours of
each b ∈ BB are the vertices N(b) = UB ∩ GO O
b in UB aboveb. We have that N(BB ) = UB ∩ b∈BB Gb = UB
S
by (8.17). Let B ⊆ BB be a largest set such that N B < B . If B = BB we are done since this is
0 0 0 0
the inequality |UB | < |BB |. Suppose therefore that B0 $ BB and |UB | = |N(BB )| > |BB |.
For all B00 ⊆ BB \ B0 we must have N B00 \ N B0 ≥ B00 , for otherwise B00 could be added to B0
to yield an even larger set B∗ = B0 ∪ B00 with N B∗ < |B∗ | contrary to the assumption that B0 has
maximal size among all sets with this property. It follows by Hall’s
marriage theorem that theremust
exist a matching of BB \ B0 into N BB \ B0 \ N B0 = UB \ N B0 . Thus, BB \ B0 ≤ UB \ N B0 and
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 539
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
in addition it followsfrom the way our bipartite graph is constructed that every b ∈ BB \ B0 is matched to
some u ∈ UB \ N B0 with level(u) ≥ level(b).
Clearly, all subconfigurations in
S1B = [B]hWi ∈ SB bot(B) ∈ BB \ B0
(8.18)
are blocked by BB \ B0 (even hidden by this set, to be precise). Also, as was argued in the beginning
of the proof, every [B]hWi ∈ SB with b = bot(B) is blocked by UH ∪ UB ∩ GO
b = UH ∪ N(b), so all
subconfigurations in
S2B = [B]hWi ∈ SB bot(B) ∈ B0
(8.19)
are blocked by UH ∪ N B0 where N B0 < B0 . And we know that SH is blocked (even hidden) by
UH . It follows that if we let
U ∗ = UH ∪ N B0 ∪ BB \ B0
(8.20)
∗ 1 2 ∗
we get a vertex set U that blocks SH ∪ SB ∪ SB = S, has measure m U ≤ m(U) because of Observa-
tion 8.29, and has size
U ∗ ≤ |UH | + N B0 + BB \ B0 < |UH | + B0 + BB \ B0 = |U|
(8.21)
strictly less than the size of U. But this is a contradiction, since U was chosen to be of minimal size. The
lemma follows.
The idea in the remaining part of the proof is as follows: Fix some smallest subset UH ⊆ U that hides
SH , and let UB = U \UH . Corollary 8.28 says that UH is the overwhelmingly larger part of U and hence
the size of UH must be very big. But UH hides the blob subconfigurations in SH very much in a similar
way as for hiding sets in the standard black-white pebble game. And we know from Section 7.3 that
such sets need not be very large. Therefore we want to use Klawe-like ideas to derive a contradiction
by transforming UH locally into a (much) better blocking set for SH . The problem is that this might
leave some subconfigurations in SB not being blocked any longer (note that in general UB will not on
its own block SB ). However, we have chosen our parameter K = 13 for the generalized LHC property
(Property 8.7) very generously and the transformation in Section 7.3 works even for the (non-generalized)
LHC property with parameter 1. Therefore, we expect our locally transformed blocking set to be so much
cheaper that we can afford to take care of any subconfigurations in SB that are no longer blocked simply
by adding all bottom vertices for all black blobs in these subconfigurations to the blocking set.
We will not be able to pull this off by just making one local improvement of the hiding set as was
done in Section 7.3, though. The reason is that the local improvement to UH could potentially be very
small, but lead to very many subconfigurations in SB becoming unblocked. If so, we cannot afford adding
new vertices blocking these subconfigurations without risking to increase the size and/or potential of
our new blocking set too much. To make sure that this does not happen, we instead make multiple local
improvements of UH simultaneously. Our next lemma says that we can do this without losing control of
how the measure behaves.
Lemma 8.30 (Generalization of Lemma 7.30). Suppose that U1 , . . . ,Uk ,V1 , . . . ,Vk ,Y are vertex sets in
a layered graph such that for all i, j ∈ [k], i 6= j, it holds that Ui -m Vi , Vi ∩ V j = 0,
/ Ui ∩ V j = 0/ and
/ Then m Y ∪ ki=1 Ui ≤ m Y ∪ ki=1 Vi .
Y ∩ Vi = 0.
S S
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 540
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
Proof. By induction over k. The base case k = 1 is Lemma 7.30 on page 522.
For the induction step, let Y 0 = Y ∪ k−1 0
i=1 Ui . Since Uk -m Vk and Y ∩ Vk = 0
S
/ by assumption, we get
from Lemma 7.30 that
m Y ∪ ki=1 Ui = m Y 0 ∪ Uk ≤ m Y 0 ∪ Vk = m Y ∪ i=1
Sk−1
Ui ∪ Vk .
S
(8.22)
Letting Y 00 = Y ∪ Vk , we see that (again by assumption) it holds for all i, j ∈ [k − 1], i 6= j, that Ui -m Vi ,
/ Ui ∩ V j = 0/ and Y 00 ∩ Vi = 0.
Vi ∩ V j = 0, / Hence, by the induction hypothesis we have
00 Si−1 00 Si−1
m Y ∪ k−1
Sk
i=1 Ui ∪ Vk = m Y ∪ k=1 Ui ≤ m Y ∪ k=1 Vi = m Y ∪ i=1 Vi
S
(8.23)
and the lemma follows.
We also need an observation about the white pebbles in SH .
Observation 8.31. For any [B]hW i ∈ SH with b = bot(B) it holds that W = W ∩ GMb .
Proof. This is so since S is W-eliminated with respect to U. Since U ∪ W hides b = bot(B), any vertices
in W ∩ GO b are superfluous and will be removed by the W-elimination procedure in Definition 8.15.
Recalling from (8.13) that WM
b
H = W ∩ GM [B]hW i ∈ SH , b = bot(B) this leads to the next, simple
but crucial observation.
Observation 8.32. The vertex set UH ∪ WM H hides the vertices in BH in the sense of Definition 7.6.
That is, we can consider BH , WM 7
H to be (almost) a standard black-white pebble configuration. This
sets the stage for applying the machinery of Section 7.3..
Appealing to Lemma 7.18 on page 517, let X ⊆ UH ∪ WM H be the unique, minimal tight set such that
.
VXW = VUH ∪ WM
HW (8.24)
and define
WM
T = WH ∩ X
M
(8.25a)
UT = UH ∩ X (8.25b)
to be the vertices in WM
H and UH that remains in X after having applied the bottom-up pruning procedure
of Lemma 7.18. .
Let H = H(G, X) be the hiding set graph of Definition 7.20 for X = UT ∪ WM T . Suppose that V1 , . . . ,Vk
are the connected components of H, and define for i = 1, . . . , k the vertex sets
BiH = BH ∩ Vi (8.26a)
WiH = WMH ∩ Vi (8.26b)
UHi = UH ∩ Vi (8.26c)
7 Not quite, since we might have B ∩ WM 6= 0.
/ But at least we know that UH ∩ WM / by W-elimination and the roles of
H H H =0
U and W in U ∪ W are fairly indistinguishable in Klawe’s proof anyway, so this does not matter.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 541
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
to be the black, white and “hiding” vertices within component Vi , and
WiT = WM
T ∩ Vi (8.26d)
UTi = UT ∩ Vi (8.26e)
to be the vertices of WMH and UH in component Vi that. “survived” when. moving to the tight subset X.
Note that we have the disjoint union equalities WM k Wi , U = Sk U i , et cetera for all of these
S
H = i=1 H H i=1 H
sets.
Let us also generalize Definition 7.8 of measure and partial measure to multi-sets of vertices in
the natural way, where we charge separately for each copy of every vertex. This is our way of doing
the bookkeeping for the extra vertices that might be needed later to block SB in the final step of our
construction.
This brings us to the key lemma stating how we will locally improve the blocking sets.
Lemma 8.33 (Generalization of Lemma 7.36). With the assumptions on the blob-pebbling configuration
S and the vertex set U as in Lemma 8.26 and with notation as above, suppose that UHi ∪ WiH hides BiH ,
that H UTi ∪ WiT is a connected graph, and that
UHi ≥ 6 · BiH ∪ WiH . (8.27)
Then we can find a multi-set U∗i ⊆ VUTi ∪ WiT W that hides thevertices in BiH , has |UHi |/3 extra copies
of some fixed but arbitrary vertex on level LU = maxlevel UHi , and satisfies U∗i -m UHi and U∗i < UHi
(where U∗i is measured and counted as a multi-set with repetitions).
Proof. Let U∗i be the set found in Lemma 7.33 on page 523, which certainly is in VUTi ∪ WiT W, to-
gether with the prescribed extra copies of some (fixed but arbitrary) vertex that we place on level
maxlevel VUH ∪ WH W ≥ LU to be on the safe side. By Lemma 7.33, U∗i hides BiH , and the size of U∗i
i i
counted as a multi-set with repetitions is
U∗i ≤ BiH + |UHi |/3 ≤ 1 1
· UHi < UHi .
6+3 (8.28)
It remains to show that U∗i -m UHi .
The proof of this last measure inequality is very much as in Lemma.
7.36, but with the difference
that .the connected graph that we are dealing with is defined over UTi ∪ WiT , but we count the vertices in
UHi ∪ WiH . Note, however, that by construction these two unions hide exactly the same set of vertices, i. e.,
. .
VUTi ∪ WiT W = VUHi ∪ WiH W . (8.29)
i i
Recall that by Definition 7.29 on page
j i
522,
l i
we need to do in order to show that U∗ -m UH is to find
what
for each j an l ≤ j such that m U∗ ≤ m UH . As in Lemma 7.36, we divide the proof into two cases.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 542
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
1. If j ≤ minlevel UTi ∪ WiT = minlevel UHi ∪ WiH , we get
m j U∗i = j + 2 · U∗i { j} by definition of m j (·)
≤ j + 2 · U∗i
since V { j} ⊆ V for any V
≤ j + 2 · |BiH | + |UHi |/3
by Lemma 7.33 plus extra vertices
< j + 2 · UHi
by the assumption in (8.27)
= j + 2 · UHi { j}
i
UH { j} = UHi since j ≤ minlevel(UHi )
= m j (UHi ) by definition of m j (·)
and we can choose l = j in Definition 7.29.
2. Consider instead j > minlevel UTi ∪ WiT and let L = minlevel UTi ∪ WiT . Since the black
pebbles in BiH are hidden by UTi ∪ WiT , i. e., BiH ⊆ VUTi ∪ WiT W in formal notation, recollecting
Definition 7.31 and Observation 7.32, part 2, we see that
L j BiH ≤ L j VUTi ∪ WiT W
(8.30)
for all j. Also, since UTi ∪ WiT is a hiding-connected vertex set in a spreading graph G, combining
Definition 7.34 with the fact that UTi ∪ WiT ⊆ UHi ∪ WiH we can derive that
j + L j VUTi ∪ WiT W ≤ L + UTi ∪ WiT ≤ L + UHi ∪ WiH .
(8.31)
Together, (8.30) and (8.31) say that
j + L j BiH ≤ L + UHi ∪ WiH
(8.32)
and using this inequality we can show that
m j (U∗i ) = j + 2 · U∗i { j} by definition of m j (·)
≤ j + L j BiH + BiH + 2 · |UHi |/3
by Lemma 7.33 + extra vertices
≤ L + UHi ∪ WiH + BiH + 2 · |UHi |/3
using the inequality (8.32)
≤ L + 53 UHi + BiH + WiH
|A ∪ B| ≤ |A| + |B|
≤ L + 53 UHi + 2 · BiH ∪ WiH
|A| + |B| ≤ 2 · |A ∪ B|
≤ L + 2 · UHi
by the assumption in (8.27)
= L + 2 · |UHi { L}| since L ≤ minlevel(UHi )
= mL (UHi ) by definition of mL (·) .
Thus, the partial measure of UHi at the minimum level L is always at least as large as the partial
measure of U∗i at levels j above this minimum level, and we can choose l = L in Definition 7.29.
Consequently, U∗i -m UHi and the lemma follows.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 543
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Now we want to determine in which connected components of the hiding set graph H we should
apply Lemma 8.33. Loosely put, we want to be sure that changing UHi to U∗i is worthwhile, i. e., that we
gain enough from this transformation to compensate for the extra hassle of reblocking blobs in SB that
turn unblocked when we change UHi . With this in mind, let us define the weight of a component Vi in H as
(
|UHi |/6 if UHi ≥ 6 · BiH ∪ WiH ,
w(Vi ) = (8.33)
0 otherwise.
The idea is that a component Vi has large weight if the hiding set UHi in this component is large compared
to the number of bottom black vertices in BiH hidden and the white pebbles WiH helping UHi to hide BiH .
If we concentrate on changing the hiding sets in components with non-zero weight, we hope to gain more
from the transformation of UHi into U∗i than we lose from then having to reblocking SB . And since UH is
large, the total weight of the non-zero-weight components is guaranteed to be reasonably large.
Proposition 8.34. With notation as above, the total weight of all connected components V1 , . . . ,Vk in the
hiding set graph H = H G,UT ∪ WM i=1 w(Vi ) > BH ∪ BB ∪ WH .
k M
T is ∑
Proof. The total size of the union of all subsets UHi ⊆ UH with sizes UHi < 6 · BiH ∪ WiH resulting in
zero-weight components Vi in H is clearly strictly less than
k
6 · ∑ BiH ∪ WiH = 6 · BH ∪ WM
H ≤ 6 · BH ∪ BB ∪ WH .
M
(8.34)
i=1
Since according to Corollary 8.28 we have that UH ≥ 12 · BH ∪ BB ∪ WM H , it follows that the size of
the union w(Vi )>0 UHi of all subsets UHi corresponding to non-zero-weight components Vi must be strictly
S
larger than 6 · BH ∪ BB ∪ WM H . But then
1
UHi > BH ∪ BB ∪ WM
i [
∑ w(Vi ) ≥ ∑ |UH |/6 ≥ ·
6 H (8.35)
w(Vi )>0 w(V )>0
i w(V )>0
i
as claimed in the proposition.
We have now collected all tools needed to establish the generalized limited hiding-cardinality property
for spreading graphs. Before we wrap up the proof, let us recapitulate
.
what we have shown so far.
We have divided the blocking set U into a disjoint union UH ∪UB of the vertices UH not only blocking
but actually hiding the subconfigurations in SH ⊆ S, and the vertices UB just helping UH to block the
remaining subconfigurations in SB = S \ SH . In Lemma 8.27 and Corollary 8.28, we proved that if U is
large (which we are assuming) then UB must be very small compared to UH , so we can basically just
ignore UB . If we want to do something interesting, it will have to be done with UH .
And indeed, Lemma 8.33 tells us that we can restructure UH to get a new vertex set hiding SH and
make considerable savings, but that this can lead to SB no longer being blocked. By Proposition 8.34,
there is a large fraction of UH that resides in the non-zero-weight components of the hiding set graph H
(as defined in equation (8.33)). We would like to show that by judiciously performing the restructuring of
Lemma 8.33 in these components, we can also take care of SB .
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 544
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
More precisely, we claim that we can combine the hiding sets U∗i from Lemma 8.33 with some subsets
of UH ∪ UB and BB into a new blocking set U ∗ for all of SH ∪ SB = S in such a way that the measure
m U ∗ does not exceed m(U) = pot(S) but so that U ∗ < |U|. But this contradicts the assumptions in
Lemma 8.26. It follows that the conclusion in Lemma 8.26, which we assumed to be false in order to
derive a contradiction, must instead be true. That is, any set U that is chosen as in Lemma 8.26 must have
size |U| ≤ 13 · BH ∪ BB ∪ WM H . This in turn implies Theorem 8.19, i. e., that layered spreading graphs
possess the generalized limited hiding-cardinality property that we assumed in order to get a lower bound
on blob-pebbling price, and we are done.
We proceed to establish this final claim. Our plan is once again to do some bipartite matching with
the help
of Hall’s marriage theorem. To this end, create a weighted bipartite graph with the vertices in
BB = bot(B) [B]hWi ∈ SB on the left-hand side and with the non-zero-weight connected components
among V1 , . . . ,Vk in H in the sense of (8.33) acting as “supervertices” on the right-hand side. Reorder the
indices among the connected components V1 , . . . ,Vk if needed so that the non-zero-weight components
are V1 , . . . ,Vk0 . All vertices in the weighted graphs are assigned weights so that each right-hand side
supervertex Vi gets its weight according to (8.33), and each left-hand vertex has weight 1.8 We define the
neighbours of each fixed vertex b ∈ BB to be
N(b) = Vi w(Vi ) > 0 and maxlevel UHi > level(b) ,
(8.36)
i. e., all non-zero-weight components Vi that contain vertices in the hiding set UH that could possibly
be involved in blocking any subconfiguration [B]hWi ∈ SB having bottom vertex bot(B) = b. This is so
since by Proposition 8.24, any vertex u ∈ UH helping to block such a subconfiguration [B]hWi ∈ SB must
be strictly above b, so if the highest-level vertices in UHi are on a level below b, no vertex in UHi can be
responsible for blocking [B]hWi.
Let B0 ⊆ BB be a largest set such that w N B0 ≤ B0 . We must have
S0
N B0 6= ki=1 Vi (8.37)
S0
since w ki=1 Vi > BH ∪ BB ∪ WM H ≥ BB by Proposition 8.34. For all B ⊆ BB \ B it holds that
00 0
w N B00 \ N B0 ≥ B00
(8.38)
since otherwise B0 would not be of largest size as assumed above. The inequality (8.38) plugged into
Hall’s marriage theorem tells us that there is a matching of the vertices in BB \ B0 to the components in
Sk0
i=1 Vi \ N B 6= 0
0 / with the property that no component Vi gets matched with more than w(Vi ) vertices
from BB \ B .0
Reorder the components in the hiding set graph H so that the matched components are V1 , . . . ,Vm
and the rest of the components are Vm+1 , . . . ,Vk and so that UH1 , . . . ,UHm and UHm+1 , . . . ,UHk are the corre-
sponding subsets of the hiding set UH . Then pick good local blockers U∗i ⊆ Vi as in Lemma 8.33 for all
components V1 , . . . ,Vm . Now the following holds:
Sm i Sk i
1. By construction and assumption, respectively, the vertex set i=1 U∗ ∪ i=m+1 UH blocks (and
even hides) SH .
8 Or, if we like, we can equivalently think of an unweighted graph, where each V is a cloud of w(V ) unique and distinct
i i
vertices, and where N(b) in (8.36) always containing either all or none of these vertices.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 545
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
2. All subconfigurations in
S1B = [B]hWi ∈ SB bot(B) ∈ B0
(8.39)
are blocked by UB ∪ N B0 = UB ∪ ki=m+1 UHi , as we have not moved any elements in U above B0 .
S
3. With notation as in Lemma 8.30, let Y = UB ∪ ki=m+1 UHi and consider U∗i and UHi for i = 1, . . . , m.
S
We have U∗i -m UHi for i = 1, . . . , m by Lemma 8.33. Also, since UH ∩ UB = 0/ and U∗i ⊆ Vi
and UHi ⊆ Vi for V1 , . . . ,Vk pairwise disjoint sets of vertices, it holds for all i, j ∈ [m], i 6= j, that
U∗i ∩ U∗j = 0,
/ UHi ∩ UHj = 0, / U∗i ∩ UHj = 0/ and Y ∩ UHj = 0.
/ Therefore, the conditions in Lemma 8.30
are satisfied and we conclude that
Sm i Sk i
Sm i
m UB ∪ i=1 U∗ ∪ i=m+1 UH =m Y ∪ i=1 U∗
Sm
≤ m Y ∪ i=1 UHi
(8.40)
= m UB ∪ m i Sk i
i=1 UH ∪ i=m+1 UH
S
= m(U) ,
where we note that UB ∪ m i Sk i
i=1 U∗ ∪
S
i=m+1 UH is measured as a multi-set with repetitions. Also,
we have the strict inequality
Sm i Sk i
UB ∪ i=1 U∗ ∪ i=m+1 UH < |U| , (8.41)
where again the multi-set is counted with repetitions.
4. It remains to take care of the potentially unblocked subconfigurations in
S2B = [B]hWi ∈ SB bot(B) ∈ BB \ B0 .
(8.42)
But we derived above that there is a matching of BB \ B0 to V1 , . . . ,Vm such that no Vi is chosen by
more than
w(Vi ) = |UHi |/6 ≤ |UHi |/3
(8.43)
vertices from BB \ B0 (where we used that UHi ≥ 6 if w(Vi ) > 0 to get the last inequality). This
means that there is a spare blocker vertex in U∗i for each b ∈ BB \ B0 that is matched to Vi . Also, by
the definition of neighbours in our weighted bipartite graph, each b is matched to a component with
maxlevel UHi > level(b). By Observation 8.29, lowering these spare vertices from maxlevel UHi
to level(b) can only decrease the measure.
Finally, throw away any remaining multiple copies in our new blocking set, and denote the resulting set
by U ∗ . We have that U ∗ blocks S and that m U ∗ ≤ m(U) but U ∗ < |U|. This is a contradiction since
U was chosen to be of minimal size, and thus Lemma 8.26 must hold. But then Theorem 8.19 follows
immediately as well, as was noted above.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 546
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
8.5 Recapitulation of the proof of Theorem 1.1 and optimality of result
Let us conclude this section by recalling why the tight bound on clause space for refuting pebbling
contradictions in Theorem 1.1 now follows and by showing that the current construction cannot be pushed
to give a better result.
To prove the upper bound in the main theorem, we need the fact that the black pebbling price of G
provides an upper bound for the refutation clause space of PebdG . Let us state this formally as a proposition
and provide a proof for completeness.
Proposition 8.35. For any DAG G with vertex indegrees 0 or 2, Sp(PebdG ` ⊥) ≤ Peb(G) + 4.
Proof. Given a black pebbling of G, we construct a refutation of PebdG such Wdthat if at some point in time
there are black pebbles on a set of vertices V , then we have the clauses i=1 x(v)i | v ∈ V in memory.
Wd
When some new vertex v is pebbled, we derive i=1 x(v)i from the clauses already in memory. We claim
that with a little care, this can be done in constant extra space independent of d. When a black pebble is
removed from v, we erase the clause di=1 x(v)i . We conclude the resolution proof by resolving di=1 x(z)i
W W
for the target z with all target axioms x(z)i , i ∈ [d], in space 3.
It is clear that given our claim about the constant extra space needed when a vertex is black-pebbled,
this yields a resolution refutation in space equal to the pebbling cost plus some constant. In particular,
given an optimal black pebbling of G, we get a refutation in space Peb(G) + O(1).
To prove the claim, note first that it trivially holds for source vertices v, since di=1 x(v)i is an
W
axiom of the formula. Suppose for a non-source vertex r with predecessors p and q that at some
point in time a black pebble is placed on r. Then p and q must be black-pebbled, so by induction we
have the clauses di=1 x(p)i and dj=1 x(q) j in memory. We will use that the clause x(p)i ∨ dl=1 x(r)l
W W W
for any i can be derived in additional space 3 by resolving dj=1 x(q) j with x(p)i ∨ x(q) j ∨ dl=1 x(r)l
W W
Wd
for j ∈ [d], leaving the easy verification of this fact to the reader. To derive l=1 x(r)l , first resolve
Wd
x(p)1 ∨ dl=1 x(r)l to get di=2 x(p)i ∨ dl=1 x(r)l , and then resolve this clause with the
W W W
i=1 x(p)i withW
clauses x(p)i ∨ dl=1 x(r)l for i = 2, . . . , d one by one to get dl=1 x(r)l in total extra space 4.
W
Theorem 8.36 (rephrasing of Theorem 1.1). Suppose that Gh is a layered DAG of height h that is
spreading. Then the clause space of refuting the pebbling contradiction PebdGh of degree d > 1 by
resolution is Sp(PebdGh ` ⊥) = Θ(h).
Proof. The O(h) upper bound on clause space follows from the bound Peb(Gh ) ≤ h + O(1) on the black
pebbling price in Lemma 7.2 on page 509 combined with the bound Sp(PebdG ` ⊥) ≤ Peb(G) + O(1)
from Proposition 8.35.
For the lower bound, we instead consider the pebbling formula *PebdGh with the target axioms
x(z)1 , . . . , x(z)d removed, and use that by Lemma 5.1 on page 495 it holds that Sp PebdGh ` ⊥ =
Sp *PebdGh ` di=1 x(z)i . Fix any resolution derivation π : *PebdGh ` di=1 x(z)i and let Pπ be the com-
W W
plete blob-pebbling
of the graph G associated to π in Theorem 5.3 on page 496 such that cost(Pπ ) ≤
maxC∈π cost(S(C)) + O(1). On the one hand, Theorem 6.5 on page 505 says that cost(S(C)) ≤ |C|
provided that d > 1, so in particular it must hold that cost(Pπ ) ≤ Sp(π) + O(1). On the other hand,
cost(Pπ ) ≥ Blob-Peb(Gh ) by definition, and by Theorems 8.8 and 8.19 it holds that Blob-Peb(Gh ) =
Ω(h). Thus Sp(π) = Ω(h), and the theorem follows.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 547
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
Plugging in pyramid graphs Πh in Theorem 8.36, we get 4-CNF formulas Fn of size Θ(n) with
√
refutation clause space Θ( n). This is the best we can get from pebbling formulas over spreading graphs.
Theorem 8.37. Let G be any layered spreading graph and suppose that PebdG has formula size and
√
number of clauses Θ(n). Then Sp PebdG ` ⊥ = O( n).
Proof. Suppose that G has height h. Then Sp PebdG ` ⊥ = O(h) as was noted above. The size of PebdG ,
as well as the number of clauses, is linear in the number of vertices |V (G)|. We claim that the fact that G
is spreading implies that |V (G)| = Ω h2 , from which the theorem follows.
To prove the claim, let VL denote the vertices of G on level L. Then |V (G)| = ∑hL=0 |VL |. Obviously,
for any L the set VL hides the sink z of G. Fix for every L some arbitrary minimal subset VL0 ⊆ VL hiding z.
Then VL0 is tight, the graph H(VL0 ) is hiding-connected by Corollary 7.23, and setting j = h in the spreading
inequality (7.10) we get that VL0 ≥ 1 + h − L. Hence |V (G)| ≥ ∑hL=0 |VL0 | = Ω h2 .
The proof of Theorem 8.37 can also be extended to cover the original definition in [42] of spreading
graphs that are not necessarily layered, but we omit the details.
9 Conclusion and open problems
We have proven an asymptotically tight bound on the refutation clause space in resolution of pebbling
contradictions over pyramid graphs, improving on previously known separations of length and clause
space in resolution. Also, in contrast to previous polynomial lower bounds on clause space, our result
does not not follow from lower bounds on width for the same formulas. Instead, a corollary of our result
is an exponential improvement of the separation of width and space in [47]. In retrospect, the current
paper can be seen as a crucial step in settling the question of the relationship between length and space
discussed in, e. g., [12, 32, 59, 60], and subsequently resolved in [15].
More technically speaking, we have established that for all graphs G in the class of “layered spreading
DAGs” (including complete binary trees and pyramid graphs) the height h of G, which coincides with the
black-white pebbling price, is an asymptotic lower bound for the refutation clause space Sp PebdG ` ⊥
√
of pebbling contradictions PebdG provided that d ≥ 2. Plugging in pyramid graphs we get a Θ n bound
on space, which is the best one can get for any spreading graph.
An obvious question is whether this lower bound on clause space in terms of black-white pebbling
price is true for arbitrary DAGs. In particular, does it hold for the family of DAGs {Gn }∞ n=1 in [35] of
size O(n) that have maximal black-white pebbling price BW-Peb(Gn ) = Θ(n/ log n) in terms of size?
We conjecture that this is indeed the case.
Conjecture 9.1. Let G be any DAG with constant fan-in and a single sink, and let PebdG denote the
pebbling contradiction of degree d > 1 defined over G. Then the clause space of refuting PebdG in
resolution is Sp(PebdG ` ⊥) ≥ BW-Peb(G).
If this conjecture can be shown to be true, then this would also reprove the asymptotically optimal
length-space separation in [15] with better constant factors.
A natural approach towards proving Conjecture 9.1 would be to extend the lower bounds on pebbling
price in the blob-pebble game used in this paper to the graphs in [35]. It seems challenging to lift the
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 548
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
lower bound argument in [35] from standard black-white pebbling to blob-pebbling, however. While it
appears plausible that the same lower bound should hold, we have not been able to prove this.
If this line of attack could be made to work, it could also be a promising approach towards establishing
the PSPACE-completeness of space requirements for k-CNF formulas in resolution, perhaps building on
the constructions in [34, 38] (as noted before, this problem is easily seen to be in PSPACE).
Open Problem 9.2. Given a k-CNF formula F and a space bound s, is it PSPACE-complete to determine
whether F can be refuted in resolution in clause space s? And is it PSPACE-complete to decide whether
F can be refuted in total space s?
The idea here would be to reduce from the problem of deciding the pebbling price of a graph G
to the problem of deciding the space requirements for the pebbling formula over G. We remark that it
seems unlikely that the techniques in [15] could be used to resolve this question. The reason for this
is that there is an inherent blow-up of a factor at least 2 between the upper and lower bounds one gets
for the version of pebbling formulas used in that paper, and therefore one would need a constant-factor
PSPACE non-approximability gap in the pebbling problem in order to get a meaningful reduction to
refutation space. In contrast, for our pebbling formulas it seems that the true upper and lower bounds
should be within a small additive constant of one another, or should perhaps even coincide. As noted
above, however, the lower bound proven in the current paper appears to be off by a constant multiplicative
factor, and additional ideas seem to be needed to obtain an exact bound.
Returning to the discussion in the introductory section, a third open question is as follows. We know
from [17] that short resolution refutations imply the existence of narrow refutations, and in view of this
an appealing proof search heuristic is to search exhaustively for refutations in minimal width. One serious
drawback of this approach is that there is no guarantee that the short and narrow refutations are the same
one. On the contrary, the narrow refutation π 0 resulting from the proof in [17] is potentially exponentially
longer than the short proof π that we start with. However, we have no examples of formulas where
the refutation in minimum width is actually known to be substantially longer than the minimum-length
refutation. Therefore, it would be very interesting to know whether this increase in length is necessary.
That is, is there a formula family which exhibits a length-width trade-off in the sense that there are
short refutations and narrow refutations, but all narrow refutations have a length blow-up (polynomial or
superpolynomial)? Or is the exponential blow-up in [17] just an artifact of the proof?
Open Problem 9.3. If F is a k-CNF formula over n variables refutable in length L, can one always find
√
a refutation π of F in width W(π) = O n log L with length no more than, say, L(π) = O(L) or at most
poly(L)? Or is there a formula family which necessarily exhibits a length-width trade-off in the sense
that there are short refutations and narrow refutations, but all narrow refutations have a length blow-up
(polynomial or superpolynomial)?
Similar questions can be posed for clause space and total space. Suppose that we have a formula that
is refutable in both small space and short length. Is it then possible to refute the formula in small space
and short length simultaneously, possibly increasing the space by a constant factor or the length by some
polynomial factor? In recent joint work with Ben-Sasson [16], the first author gave a strong negative
answer to this question by proving superpolynomial or even exponential trade-offs for length with respect
to both total space and clause space for space in almost the whole range between constant and linear
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 549
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
in the formula size. Even more recently, Beame et al. [9] established that although any formula can be
refuted in linear clause space (as shown in [31]), there are formulas with refutations in superlinear but
polynomial length and space where bringing the space down to linear incurs a superpolynomial length
blow-up.
However, it still remains open what kind of trade-offs are possible for constant space. Given a formula
refutable in constant clause space, we know that there must exist a refutation in polynomial length as well.
This follows by applying the upper bound on width in terms of clause space from [5], and then noting
that narrow proofs are trivially short. But as in [17], the refutation we end up with is not the same as the
one with which we started. This leads to the following question.
Open Problem 9.4. Given a family of polynomial-size k-CNF formulas {Fn }∞ n=1 with refutation clause
space Sp(Fn ` ⊥) = O(1), are there refutations π : Fn ` ⊥ simultaneously in length L(π) = poly(n) and
clause space Sp(π) = O(1)? Or is it possible that restricting the space to constant can force the length to
be superpolynomial?
We conclude with a brief discussion on resolution space versus clause learning. Given that research
into proof space complexity was originally motivated by SAT solving concerns, we find it an interesting
question whether lower bounds on space can give indications as to which formulas might be hard for
clause learning algorithms and why. On the face of it, space lower bounds might not seem too relevant
since they will never be stronger than linear, and certainly any SAT solver will use linear space to store
the formula in question. Suppose, however, that we know for some CNF formula that its refutation space
is large. What this tells us is that any algorithm, even a non-deterministic one making optimal choices
concerning which clauses to save or throw away at any given point in time, will have to keep a fairly large
number of “active” clauses in memory in order to carry out the refutation. Since this is so, a real-life
deterministic proof search algorithm, which has no sure-fire way of knowing which clauses are the right
ones to concentrate on at any given moment, might have to keep working on a lot of extra clauses in
order to be certain that the fairly large critical set of clauses needed to find a refutation will be among
the “active” clauses. In this sense a (non-deterministic) linear lower bound might imply much stronger
bounds in practice. We remark that indeed, resolution refutation space has been proposed as a measure of
hardness for SAT solvers in [4].
And intriguingly enough, pebbling contradictions might in fact be an example of the phenomenon
discussed in the previous paragraph. We know that these formulas are very easy with respect to length
and width, having constant-width refutations that are essentially as short as the formulas themselves.
But in [57], it was shown that state-of-the-art clause learning algorithms can have serious problems with
even moderately large pebbling contradictions over pyramid graphs.9 And more recent experimental
work involving the first author and reported in [40] indicates that the space complexity of pebbling
contradictions is correlated with how hard or easy the formulas are for CDCL solvers. Although we are
certainly not arguing that this is the whole story—it was also shown in [57] that the branching order is a
critical factor, and that given some extra structural information the algorithm can achieve an exponential
speed-up, and there are some important caveats in the experimental results in [40]—we believe that such
possible connections would be worth investigating further. It would also be interesting to investigate for
9 The “grid pebbling formulas” in [57] are exactly our pebbling contradictions of degree d = 2 over pyramid graphs.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 550
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
the formulas in [9, 16] whether anything similar to the theoretical size-space trade-offs for these formulas
actually shows up as trade-offs between running time and memory consumption in practice.
Acknowledgements
We are thankful to Per Austrin and Mikael Goldmann for generous feedback during various stages of this
work, and to Gunnar Kreitz for quickly spotting some bugs in a preliminary version of the blob-pebble
game. Also, we would like to thank Paul Beame and Maria Klawe for valuable correspondence concerning
their work, Nathan Segerlind for comments and pointers regarding clause learning, and Eli Ben-Sasson
for stimulating discussions about proof complexity in general and the problems in Section 9 in particular.
Finally, we gratefully acknowledge the thoughtful comments of the anonymous reviewers and the patient
and meticulous work of the Theory of Computing editors, which helped us to improve the presentation
considerably.
References
[1] RON A HARONI AND NATHAN L INIAL: Minimal non-two-colorable hypergraphs and minimal
unsatisfiable formulas. J. Combin. Theory Ser. A, 43(2):196–204, 1986. [doi:10.1016/0097-
3165(86)90060-9] 503
[2] M ICHAEL A LEKHNOVICH , E LI B EN -S ASSON , A LEXANDER A. R AZBOROV, AND AVI W IGDER -
SON : Space complexity in propositional calculus. SIAM J. Comput., 31(4):1184–1211, 2002.
Preliminary version in STOC’00. [doi:10.1137/S0097539700366735] 476, 485, 486
[3] M ICHAEL A LEKHNOVICH , JAN J OHANNSEN , T ONIANN P ITASSI , AND A LASDAIR U RQUHART:
An exponential separation between regular and general resolution. Theory of Computing, 3(5):81–
102, 2007. Preliminary version in STOC’02. [doi:10.4086/toc.2007.v003a005] 486
[4] C ARLOS A NSÓTEGUI , M ARÍA L UISA B ONET, J ORDI L EVY, AND F ELIP M ANYÀ: Measuring the
hardness of SAT instances. In Proc. 23rd AAAI Conference on Artificial Intelligence (AAAI’08), pp.
222–228. AAAI Press, 2008. AAAI. [ACM:1620032] 550
[5] A LBERT ATSERIAS AND V ÍCTOR DALMAU: A combinatorial characterization of resolu-
tion width. J. Comput. System Sci., 74(3):323–334, 2008. Preliminary version in CCC’03.
[doi:10.1016/j.jcss.2007.06.025] 476, 550
[6] S VEN BAUMER , J UAN L UIS E STEBAN , AND JACOBO T ORÁN: Minimally unsatisfiable CNF
formulas. Bulletin of the European Association for Theoretical Computer Science, 74:190–192,
2001. 503
[7] ROBERTO J. BAYARDO , J R . AND ROBERT S CHRAG: Using CSP look-back techniques to solve
real-world SAT instances. In Proc. 14th Nat. Conf. on Artificial Intelligence (AAAI’97), pp. 203–208,
1997. CiteSeerX. [ACM:1867406.1867438] 474
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 551
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
[8] PAUL B EAME: Proof complexity. In S TEVEN RUDICH AND AVI W IGDERSON, editors, Computa-
tional Complexity Theory, volume 10 of IAS/Park City Mathematics Series, pp. 199–246. American
Mathematical Society, 2004. Available at author’s home page. 475
[9] PAUL B EAME , C HRISTOPHER B ECK , AND RUSSELL I MPAGLIAZZO: Time-space tradeoffs in
resolution: superpolynomial lower bounds for superlinear space. In Proc. 44th STOC, pp. 213–232.
ACM Press, 2012. [doi:10.1145/2213977.2213999] 550, 551
[10] PAUL B EAME , R ICHARD M. K ARP, T ONIANN P ITASSI , AND M ICHAEL E. S AKS: The efficiency
of resolution and Davis–Putnam procedures. SIAM J. Comput., 31(4):1048–1075, 2002. Preliminary
versions in FOCS’96 and STOC’98. [doi:10.1137/S0097539700369156] 475
[11] PAUL B EAME AND T ONIANN P ITASSI: Propositional proof complexity: Past, present and future.
Bulletin of the European Association for Theoretical Computer Science, 65:66–89, 1998. Available
at author’s home page. See also updated version at ECCC. 475
[12] E LI B EN -S ASSON: Size-space tradeoffs for resolution. SIAM J. Comput., 38(6):2511–2525, 2009.
Preliminary version in STOC’02. [doi:10.1137/080723880] 476, 477, 486, 503, 548
[13] E LI B EN -S ASSON AND N ICOLA G ALESI: Space complexity of random formulae in resolu-
tion. Random Structures & Algorithms, 23(1):92–109, 2003. Preliminary version in CCC’01.
[doi:10.1002/rsa.10089] 476
[14] E LI B EN -S ASSON , RUSSELL I MPAGLIAZZO , AND AVI W IGDERSON: Near optimal separation of
tree-like and general resolution. Combinatorica, 24(4):585–603, 2004. [doi:10.1007/s00493-004-
0036-5] 476, 479, 486
[15] E LI B EN -S ASSON AND JAKOB N ORDSTRÖM: Short proofs may be spacious: An optimal separation
of space and length in resolution. In Proc. 49th FOCS, pp. 709–718. IEEE Comp. Soc. Press, 2008.
[doi:10.1109/FOCS.2008.42] 478, 484, 488, 548, 549
[16] E LI B EN -S ASSON AND JAKOB N ORDSTRÖM: Understanding space in proof complexity: Separa-
tions and trade-offs via substitutions. In Proc. 2nd Symp. Innovations in Computer Science (ICS’11),
pp. 401–416, 2011. ICS’11. 549, 551
[17] E LI B EN -S ASSON AND AVI W IGDERSON: Short proofs are narrow - resolution made simple. J.
ACM, 48(2):149–169, 2001. Preliminary version in STOC’99. [doi:10.1145/375827.375835] 475,
476, 487, 549, 550
[18] A RCHIE B LAKE: Canonical Expressions in Boolean Algebra. Ph. D. thesis, University of Chicago,
1937. 475
[19] M ARÍA L UISA B ONET, J UAN L UIS E STEBAN , N ICOLA G ALESI , AND JAN J OHANNSEN: On the
relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput.,
30(5):1462–1484, 2000. Preliminary version in FOCS’98. [doi:10.1137/S0097539799352474] 486,
487
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 552
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
[20] M ARÍA L UISA B ONET AND N ICOLA G ALESI: Optimality of size-width tradeoffs for res-
olution. Comput. Complexity, 10(4):261–276, 2001. Preliminary version in FOCS’99.
[doi:10.1007/s000370100000] 477
[21] J OSHUA B URESH -O PPENHEIM AND T ONIANN P ITASSI: The complexity of resolution re-
finements. J. Symbolic Logic, 72(4):1336–1352, 2007. Preliminary version in LICS’03.
[doi:10.2178/jsl/1203350790] 486
[22] S AMUEL R. B USS AND G YÖRGY T URÁN: Resolution proofs of generalized pigeonhole principles.
Theoret. Comput. Sci., 62(3):311–317, 1988. [doi:10.1016/0304-3975(88)90072-2] 475
[23] VAŠEK C HVÁTAL AND E NDRE S ZEMERÉDI: Many hard examples for resolution. J. ACM,
35(4):759–768, 1988. [doi:10.1145/48014.48016] 475, 503
[24] S TEPHEN A. C OOK: The complexity of theorem-proving procedures. In Proc. 3rd STOC, pp.
151–158. ACM Press, 1971. [doi:10.1145/800157.805047] 474
[25] S TEPHEN A. C OOK: An observation on time-storage trade off. J. Comput. System Sci., 9(3):308–
316, 1974. Preliminary version in STOC’73. [doi:10.1016/S0022-0000(74)80046-2] 510
[26] S TEPHEN A. C OOK AND ROBERT A. R ECKHOW: The relative efficiency of propositional proof
systems. J. Symbolic Logic, 44(1):36–50, 1979. JSTOR. 474
[27] S TEPHEN A. C OOK AND R AVI S ETHI: Storage requirements for deterministic polynomial time
recognizable languages. J. Comput. System Sci., 13(1):25–37, 1976. Preliminary version in
STOC’74. [doi:10.1016/S0022-0000(76)80048-7] 480, 486, 508
[28] M ARTIN DAVIS , G EORGE L OGEMANN , AND D ONALD W. L OVELAND: A machine program for
theorem-proving. Commun. ACM, 5(7):394–397, 1962. [doi:10.1145/368273.368557] 474, 475
[29] M ARTIN DAVIS AND H ILARY P UTNAM: A computing procedure for quantification theory. J. ACM,
7(3):201–215, 1960. [doi:10.1145/321033.321034] 474, 475
[30] J UAN L UIS E STEBAN , N ICOLA G ALESI , AND J OCHEN M ESSNER: On the complexity of resolution
with bounded conjunctions. Theoret. Comput. Sci., 321(2-3):347–370, 2004. Preliminary version in
ICALP’02. [doi:10.1016/j.tcs.2004.04.004] 476
[31] J UAN L UIS E STEBAN AND JACOBO T ORÁN: Space bounds for resolution. Inform. and Comput.,
171(1):84–97, 2001. Preliminary versions in STACS’99 and CSL’99. [doi:10.1006/inco.2001.2921]
476, 477, 485, 486, 550
[32] J UAN L UIS E STEBAN AND JACOBO T ORÁN: A combinatorial characterization of treelike resolution
space. Inform. Process. Lett., 87(6):295–300, 2003. [doi:10.1016/S0020-0190(03)00345-4] 476,
477, 548
[33] Z VI G ALIL: On resolution with clauses of bounded size. SIAM J. Comput., 6(3):444–459, 1977.
Preliminary version found in STOC’75. [doi:10.1137/0206031] 475
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 553
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
[34] J OHN R. G ILBERT, T HOMAS L ENGAUER , AND ROBERT E NDRE TARJAN: The pebbling problem
is complete in polynomial space. SIAM J. Comput., 9(3):513–524, 1980. Preliminary version in
STOC’79. [doi:10.1137/0209038] 549
[35] J OHN R. G ILBERT AND ROBERT E NDRE TARJAN: Variations of a pebble game on graphs. Technical
Report STAN-CS-78-661, Stanford University, 1978. InfoLab. [ACM:892174] 508, 548, 549
[36] A RMIN H AKEN: The intractability of resolution. Theoret. Comput. Sci., 39:297–308, 1985.
[doi:10.1016/0304-3975(85)90144-6] 475
[37] A LEXANDER H ERTEL: Applications of Games to Propositional Proof Complexity. Ph. D. thesis,
University of Toronto, 2008. Available at author’s home page. [ACM:1925663] 485
[38] P HILIPP H ERTEL AND T ONIANN P ITASSI: The PSPACE-completeness of black-white peb-
bling. SIAM J. Comput., 39(6):2622–2682, 2010. Preliminary version in FOCS’07.
[doi:10.1137/080713513] 549
[39] J OHN E. H OPCROFT, W OLFGANG J. PAUL , AND L ESLIE G. VALIANT: On time versus space. J.
ACM, 24(2):332–337, 1977. Preliminary version in FOCS’75. [doi:10.1145/322003.322015] 477,
486
[40] M ATTI J ÄRVISALO , A RIE M ATSLIAH , JAKOB N ORDSTRÖM , AND S TANISLAV Ž IVNÝ: Relating
proof complexity measures and practical hardness of SAT. In Proc. 18th Internat. Conf. on Principles
and Practice of Constraint Programming (CP’12), pp. 316–331. Springer, 2012. [doi:10.1007/978-
3-642-33558-7_25] 550
[41] H ENRY A. K AUTZ AND BART S ELMAN: The state of SAT. Discr. Appl. Math., 155(12):1514–1524,
2007. [doi:10.1016/j.dam.2006.10.004] 474
[42] M ARIA M. K LAWE: A tight bound for black and white pebbles on the pyramid. J. ACM, 32(1):218–
228, 1985. Preliminary version in FOCS’83. [doi:10.1145/2455.214115] 483, 484, 508, 511, 512,
513, 514, 516, 517, 520, 522, 523, 524, 548
[43] O LIVER K ULLMANN: An application of matroid theory to the SAT problem. In Proc. 15th
IEEE Conf. on Computational Complexity (CCC’00), pp. 116–124. IEEE Comp. Soc. Press, 2000.
[doi:10.1109/CCC.2000.856741] 503
[44] T HOMAS L ENGAUER AND ROBERT E NDRE TARJAN: The space complexity of pebble games on
trees. Inform. Process. Lett., 10(4-5):184–188, 1980. [doi:10.1016/0020-0190(80)90136-2] 508,
510
[45] J OÃO P. M ARQUES -S ILVA: Practical applications of Boolean satisfiability. In
9th Internat. Workshop on Discrete Event Systems (WODES’08), pp. 74–80, 2008.
[doi:10.1109/WODES.2008.4605925] 474
[46] J OÃO P. M ARQUES -S ILVA AND K AREM A. S AKALLAH: GRASP: A search algorithm for propo-
sitional satisfiability. IEEE Trans. Computers, 48(5):506–521, 1999. Preliminary version in
ICCAD’96. [doi:10.1109/12.769433] 474
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 554
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
[47] JAKOB N ORDSTRÖM: Narrow proofs may be spacious: Separating space and width in resolution.
SIAM J. Comput., 39(1):59–121, 2009. Preliminary version in STOC’06. [doi:10.1137/060668250]
476, 477, 484, 508, 548
[48] JAKOB N ORDSTRÖM: New wine into old wineskins: A survey of some pebbling classics with
supplemental results. Manuscript in preparation. To appear in Foundations and Trends in Theoretical
Computer Science. Current draft version available at author’s home page, 2013. 486, 516, 524
[49] JAKOB N ORDSTRÖM: Pebble games, proof complexity and time-space trade-offs. Logical Methods
in Computer Science, 2013. To appear. Available at author’s home page. 484
[50] JAKOB N ORDSTRÖM AND J OHAN H ÅSTAD: Towards an optimal separation of space and length in
resolution. In Proc. 40th STOC, pp. 701–710. ACM Press, 2008. [doi:10.1145/1374376.1374478]
488, 527
[51] N ICHOLAS P IPPENGER: Pebbling. Technical Report RC8258, IBM Watson Research Center, 1980.
Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer
Science, Japan. 486
[52] R AN R AZ: Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115–138,
2004. Preliminary version in STOC’02. [doi:10.1145/972639.972640] 475
[53] R AN R AZ AND P IERRE M C K ENZIE: Separation of the monotone NC hierarchy. Combinatorica,
19(3):403–435, 1999. Preliminary version in FOCS’97. [doi:10.1007/s004930050062] 487
[54] A LEXANDER A. R AZBOROV: Resolution lower bounds for the weak functional pigeonhole prin-
ciple. Theoret. Comput. Sci., 303(1):233–243, 2003. [doi:10.1016/S0304-3975(02)00453-X]
475
[55] A LEXANDER A. R AZBOROV: Resolution lower bounds for perfect matching principles. J. Comput.
System Sci., 69(1):3–27, 2004. Preliminary version in CCC’02. [doi:10.1016/j.jcss.2004.01.004]
475
[56] J OHN A LAN ROBINSON: A machine-oriented logic based on the resolution principle. J. ACM,
12(1):23–41, 1965. [doi:10.1145/321250.321253] 475
[57] A SHISH S ABHARWAL , PAUL B EAME , AND H ENRY A. K AUTZ: Using problem structure for
efficient clause learning. In 6th Internat. Conf. on Theory and Applications of Satisfiability Testing
(SAT’03), pp. 242–256, 2004. [doi:10.1007/978-3-540-24605-3_19] 550
[58] The international SAT Competitions web page. http://www.satcompetition.org. 474
[59] NATHAN S EGERLIND: The complexity of propositional proofs. Bulletin of Symbolic Logic,
13(4):417–481, 2007. Bulletin of Symbolic Logic. 475, 548
[60] JACOBO T ORÁN: Space and width in propositional resolution. Bulletin of the EATCS, 83:86–104,
2004. Universität Ulm. 477, 548
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 555
JAKOB N ORDSTR ÖM AND J OHAN H ÅSTAD
[61] G RIGORI T SEITIN: On the complexity of derivation in propositional calculus. In A. O. S ILENKO,
editor, Structures in Constructive Mathematics and mathematical Logic, Part II, pp. 115–125.
Consultants Bureau, New York-London, 1968. 475
[62] A LASDAIR U RQUHART: Hard examples for resolution. J. ACM, 34(1):209–219, 1987.
[doi:10.1145/7531.8928] 475
AUTHORS
Jakob Nordström
Assistant Professor
KTH Royal Institute of Technology, Stockholm, Sweden jakobn kth se
http://www.csc.kth.se/~jakobn
Johan Håstad
Professor
KTH Royal Institute of Technology, Stockholm, Sweden johanh kth se
http://www.csc.kth.se/~johanh
ABOUT THE AUTHORS
JAKOB N ORDSTRÖM received his Master of Science in Computer Science and Mathematics
from Stockholm University in 2001, and his Ph. D. in Computer Science from KTH
Royal Institute of Technology in 2008, where he was advised by Johan Håstad. During
the academic years 2008-09 and 2009-10 he was a postdoctoral researcher at the Mas-
sachusetts Institute of Technology (MIT). Since 2011 he has been an Assistant Professor
at the School of Computer Science and Communication at KTH. So far, he has worked
mostly on proof complexity and on questions at the intersection of proof complexity and
SAT solving.
In 1997-1998, Jakob served as a military interpreter at the Swedish Armed Forces
Language Institute (Försvarets tolkskola). In parallel with his studies and later his
research, he has worked as a Russian interpreter, engaged among others for His Majesty
the King of Sweden and the Swedish Prime Minister. He also has a Diploma in Choir
Conducting with extended Music Theory from the Tallinn Music Upper Secondary
School, Estonia. During the period 1994-1999, he was the artistic director of Collegium
Vocale Stockholm, a vocal ensemble performing mainly Renaissance and Baroque music.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 556
T OWARDS AN O PTIMAL S EPARATION OF S PACE AND L ENGTH IN R ESOLUTION
J OHAN H ÅSTAD received his Bachelor of Science from Stockholm University in 1981, his
Master of Science from Uppsala University in 1984 and his Ph. D. from MIT in 1986
under the supervision of Shafi Goldwasser. Johan was appointed Associate Professor at
KTH Royal Institute of Technology in Stockholm, Sweden, in 1988 and was promoted
to Professor in 1992. He has been a member of the Swedish Royal Academy of Sciences
since 2001. He has research interests within several subareas of Theory of Algorithms
and Complexity theory but has, in recent years, mainly focused on the inapproximability
of NP-hard optimization problems.
T HEORY OF C OMPUTING, Volume 9 (14), 2013, pp. 471–557 557