A Tutorial on Time and Space Bounds in Tree-Like Resolution - Perspectives in Computational Complexity - page 158

(1) Deleting a clause from F i .
(2) Adding the resolvent of two clauses from F i .
(3) Adding a clause from F (initial clause).
The space needed for the resolution refutation of an unsatisfiable formula is the
minimum k for which the formula has a refutation bounded by space k . Note that
initial clauses do not need much space because they can be added at any moment
and at most two of them are needed simultaneously. The only clauses that consume
space are the ones derived at intermediate stages. From the proof of Theorem 1.1, it
can be observed that the space needed in a refutation of a formula with n variables is
at most n 1. In [ Tor99 , ET01 , ABRW02 ] it is shown that the refutations for certain

families of formulas need linear space in the number of variables. It was observed in
[ ET01 ] that the space required for the refutation of a CNF formula F , corresponds to
the minimum number of pebbles needed in the following game played on the graph
of a refutation of F .
Definition 1.5 Given a connected directed acyclic graph G with one sink the aim
of the pebble game is to put a pebble on the sink of the graph, the only node with no
outgoing edges, following this set of rules:
(1) A pebble can be placed in any initial node, that is, a node with no predecessors.
(2) Any pebble can be removed from any node at any time.
(3) A node can be pebbled provided all its predecessors are pebbled.
(4) If all the predecessors of node are pebbled, instead of placing a new pebble on
it, one can shift a pebble from a predecessor.
We denote by Peb

+

the minimum number of pebbles needed in order to put a
pebble on the sink of G following the above rules.
Exercise 1.6 Show that for a complete binary tree of depth d, T d (with the directed
edges pointing to the root), Peb

( G )

1 . Show that this is also true for any tree
T with the property that d is the depth of the biggest complete binary tree embedded 1
in T .
Lemma 1.7 [ ET01 ] Let F be an unsatisfiable CNF formula. The space needed in
a resolution refutation of F coincides with the number of pebbles needed for the
pebble game played on the graph of a resolution refutation of F .
In this tutorial we will concentrate on tree-like refutations. The size of such a
refutation is the number of nodes in the resolution tree, and the space is the number
of pebbles needed to play the game in such a refutation tree. There is also a way to
define the space measure for tree-like resolution without using the pebbling game
[ ET01 ].
There is a relation between the space and size in tree-like resolution. As the
following result shows, a lower bound on the tree-like space of a formula implies an
exponentially larger lower bound on the size of a tree-like resolution refutation.

( T d ) = d +

1 We say that a graph G is embedded in another graph H if H can be obtained from G by adding
new vertices and edges and placing new vertices in the middle of an edge.