Authors Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, Alasdair Urquhart,
License CC-BY-ND-2.0
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102
http://theoryofcomputing.org
An Exponential Separation between Regular
and General Resolution
Michael Alekhnovich Jan Johannsen∗ Toniann Pitassi†
Alasdair Urquhart‡
Received: August 15, 2006; published: May 1, 2007.
Dedicated to the memory of Misha Alekhnovich
Abstract: This paper gives two distinct proofs of an exponential separation between
regular resolution and unrestricted resolution. The previous best known separation between
these systems was quasi-polynomial.
ACM Classification: F.2.2, F.2.3
AMS Classification: 03F20, 68Q17
Key words and phrases: resolution, proof complexity, lower bounds
1 Introduction
Propositional proof complexity is currently a very active area of research. In the realm of the theory of
feasible proofs it plays a role analogous to the role played by Boolean circuit complexity in the theory
of computational complexity.
∗ Supported by the DFG Emmy Noether-Programme grant No. Jo 291/2-1.
† Supported by NSERC.
‡ Supported by NSERC.
Authors retain copyright to their work and grant Theory of Computing unlimited rights
to publish the work electronically and in hard copy. Use of the work is permitted as
long as the author(s) and the journal are properly acknowledged. For the detailed
copyright statement, see http://theoryofcomputing.org/copyright.html.
c 2007 Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart DOI: 10.4086/toc.2007.v003a005
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
The motivation to study the complexity of propositional proof systems comes from two sides. First,
it was shown in the seminal paper of Cook and Reckhow [10] that the existence of “strong” systems in
which all tautologies have proofs of polynomial size is tightly connected to the NP vs. coNP problem.
This direction explains the considerable efforts spent in proving super-polynomial lower bounds for
proof systems that are as strong as possible.
The second motivation concerns automated theorem proving. The main goal is to investigate the
efficiency of heuristics for testing satisfiability, and to give some theoretical justification for them. It
turns out that the more sophisticated our propositional proof system is the harder it is to find proofs
of near-optimal size. The most thoroughly studied and oldest class of algorithms for satisfiability is
based on simple proof systems such as resolution, or even on restricted subsystems of resolution. This
partially explains why it is of interest to study such simple and weak proof systems and investigate how
they relate to each other.
A lot of recent research has concentrated on the separation between different variants of resolution.
In a series of papers [13, 14, 6, 4] the following relationships were studied: tree-like resolution vs.
resolution, Davis-Putnam resolution vs. general resolution, regular resolution vs. general resolution. For
all pairs except the latter, exponential gaps have been produced.
The regularity restriction was first introduced by Grigory Tseitin in a ground-breaking article [23],
the published version of a talk given in 1966 at a Leningrad seminar. This restriction is very natural,
in the sense that algorithms such as that of Davis, Logemann and Loveland [11] (often described as
the “Davis-Putnam procedure” and the prototype of almost all satisfiability algorithms used in practice
today) can be understood as a search for a regular refutation of a set of clauses. If refutations are
represented as trees, rather than directed acyclic graphs, then minimal-size refutations are regular, as
can be proved by a simple pruning argument [24, p. 436].
The main result of Tseitin’s paper [23] is an exponential lower bound for regular resolution refuta-
tions of contradictory CNF formulas based on graphs. Tseitin makes the following remarks about the
heuristic interpretation of the regularity restriction:
The regularity condition can be interpreted as a requirement for not proving intermediate
results in a form stronger than that in which they are later used (if A and B are disjunctions
such that A ⊆ B, then A may be considered to be the stronger assertion of the two); if the
derivation of a disjunction containing a variable ξ involves the annihilation of the latter, then
we can avoid this annihilation, some of the disjunctions in the derivation being replaced by
“weaker” disjunctions containing ξ .
These heuristic remarks of Tseitin suggest that there is always a regular resolution refutation of min-
imal size, as in the case of tree resolution. Consequently, some authors tried to extend Tseitin’s results
to general resolution by showing that regular resolution can simulate general resolution efficiently. The
results of Goerdt [14] and the present paper show that these attempts were doomed to failure. However,
it remains an open question whether this simulation might not hold for some special cases. In the con-
clusion of the paper, we make a conjecture to the effect that for the formulas of Tseitin, as well as other
well-known families of examples, there is always a minimal-size regular refutation.
The first example of a contradictory CNF formula whose shortest resolution refutation is irregular
was given by Wenqi Huang and Xiangdong Yu [16]. Andreas Goerdt [14] gave the first super-polynomial
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 82
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
separation between regular resolution and unrestricted resolution by constructing a family of formulas
that have polynomial-size resolution proofs, but require quasipolynomial-size regular resolution refuta-
tions.
In this paper, we present two new families of formulas, and prove that they have simple polynomial-
size resolution refutations, but require exponential-size regular resolution refutations. Our first example
is technically simpler, and results in a stronger lower bound. The second example has a natural combina-
torial interpretation, and the corresponding lower bound technique may be useful for other applications.
The paper is organized in the following way. Section 2 contains definitions necessary for both
examples. We give these examples independently in Sections 3, 4, and 5.
2 Preliminaries
A literal is a propositional variable x or its negation ¬x. A clause is a set of literals. The resolution
principle says that if C and D are clauses and x is a variable, then any assignment that satisfies both
of the clauses C ∨ x and D ∨ ¬x also satisfies C ∨ D. The clause C ∨ D is said to be a resolvent of the
clauses C ∨ x and D ∨ ¬x derived by resolving on the variable x. A resolution derivation of a clause C
from a CNF formula F consists of a sequence of clauses in which each clause is either a clause of F,
or a resolvent of two previous clauses, and C is the last clause in the sequence; it is a refutation of F if
C is the empty clause Λ. The size of a refutation is the number of resolvents in it. We can represent it
as a directed acyclic graph (dag) where the nodes are the clauses in the refutation, each clause of F has
out-degree 0, and any other clause has two arcs pointing to the two clauses that produced it. The arcs
pointing to C ∨ x and D ∨ ¬x are labeled with the literals x and ¬x respectively. It is well known that
resolution is a sound and complete propositional proof system, i. e., a formula F is unsatisfiable if and
only if there is a resolution refutation for F.
A resolution refutation is regular if on any path from Λ to a clause in F (in the directed acyclic graph
associated with the refutation), each variable is resolved on at most once along the path.
An assignment for a formula F (sometimes we call it also a restriction) is a Boolean assignment
to some of the variables in the formula; the assignment is total if all the variables in the formula are
assigned values. If C is a clause, and σ an assignment, then we write Cdσ for the result of applying
the assignment to C, that is, Cdσ = 1 if σ (l) = 1 for some literal l in C, otherwise, Cdσ is the result of
removing all literals set to 0 by σ from C (with the convention that the empty clause is identified with
the Boolean value 0). If F is a CNF formula, then Fdσ is the conjunction of all the clauses Cdσ , C a
clause in F.
If R = C1 , . . . ,Ck is a resolution derivation from a formula F, and σ an assignment to the variables
in F, then we write Rdσ for the sequence C1 dσ , . . . ,Ck dσ .
Lemma 2.1. If R is a regular resolution derivation of C from a formula F, and σ an assignment, then
there is a subsequence of Rdσ that is a regular resolution derivation of a subclause of Cdσ from Fdσ .
Proof. This is a straightforward induction on the length of the derivation from F.
Every regular resolution refutation can be represented by a read-once branching program [17]. Al-
though we prefer to speak in terms of refutations rather than branching programs, we nevertheless need
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 83
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
some ideas from the latter framework. A path in a resolution refutation can be considered as determined
by the answers to a series of queries. That is to say, starting at the root of the refutation, let us follow
a path in the proof according to the following recipe. If a node ν in the refutation is labeled with a
clause C ∨ D derived from clauses C ∨ x and D ∨ ¬x, then we say that the variable x is queried at ν. If
we extend the path to the node labeled with C ∨ x, then we say that we have answered the query with
“x,” while in the other case, we have answered with “¬x.” Thus every path π in the refutation from the
root to a node in the proof corresponds to a set of literals constituting the set of answers to the queries
in the path; conversely the set of literals constituting the answers uniquely determines the path. The
assignment defined by setting all of the literals in this set to 0 falsifies all the clauses labeling nodes in
the path.
For any node in a regular refutation we can define an important set of forgotten variables:
Definition 2.2. For every node ν in a regular refutation labeled with a clause C, we say that a variable
is forgotten at ν if it does not occur in C, but is queried on some path from the root to ν.
The intuition behind this definition is given by the following lemma.
Lemma 2.3. If the variable x is forgotten at a node ν in a regular refutation, then no axiom reachable
from ν can contain x. In particular, the clause labeling ν must be inferred from initial clauses that do
not contain x.
Proof. If x is forgotten at ν, but there is an axiom reachable from ν containing x, then x must have been
removed by resolution by some inference on the path from ν to this axiom. However, this contradicts
the regularity restriction.
Clearly this result only applies to the case of a regular refutation. This corollary will be a central
point in our lower bounds for regular resolution. Our strategy will be to find a node ν with a forgotten
variable x and show that all initial clauses free of x do not imply the clause Cν even semantically; to
show this we produce an assignment σ that falsifies only clauses containing x, while Cν dσ = 0.
3 0 formulas
First example: GTn,ρ
Our first example is based on the ordering principle first considered by Krishnamurthy [18].
Definition 3.1. Let X be the set of variables xi j for i, j ∈ [n], i 6= j. The contradiction GTn consists of
the following axioms:
xi j ↔ ¬x ji 1≤i< j≤n ,
¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 for any distinct i1 , i2 , i3 ∈ [n] ,
_
xk j j ∈ [n] .
k∈[n] , k6= j
Our version of the contradiction GTn differs slightly from the one considered in the literature, since
the transitivity axioms are usually written in the form xi1 i2 ∧ xi2 i3 → xi1 i3 (that is to say, (¬xi1 i2 ∨ ¬xi2 i3 ∨
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 84
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
xi1 i3 )). It is more convenient for us to write these axioms in the symmetric form ¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ;
these representations are equivalent in the presence of the axioms xi j ↔ ¬x ji . Note that there are exactly
two such transitivity axioms for any set of three distinct elements i1 , i2 , i3 ∈ [n].
This contradictory principle can have several semantical interpretations; our proof will essentially
depend upon the following one. Consider the variable xi j as a predicate i j. The first two groups of
axioms assure that is a total linear ordering on the set [n]. The principle GTn claims that any such
ordering never has a maximum. Krishnamurthy [18] conjectured that GTn requires superpolynomial-
size resolution refutations. This conjecture was refuted by Gunnar Stålmarck, who proved the following
result.
Theorem 3.2. There exist regular resolution refutations of GTn of size O(n3 ).
Proof. The paper of Stålmarck [22] exhibits an explicit refutation of GTn of this size. Since the number
of clauses in GTn is also O(n3 ), the size of the refutation is linear in the number of clauses. It is easy to
check that Stålmarck’s refutation is in fact regular.
This contradiction was later used by Bonet and Galesi [5] to show the optimality of the size-width
relationship. By a slight modification of Stålmarck’s construction, they showed that the refutation in the
preceding theorem can be taken as an ordered resolution refutation (or “Davis-Putnam” refutation).
We modify GTn to make it harder for regular resolution, but preserve its unrestricted resolution
complexity. For that we replace some axioms C with a pair C ∨ xC , C ∨ ¬xC . The variable xC should be
chosen in a certain precise way to simplify our lower bound.
Definition 3.3. Let X be the set of variables xi j i, j ∈ [n], i 6= j; the cardinality of X is n(n − 1). Let T
n
be the set of all triples (i, j, k), i 6= j 6= k, i, j, k ∈ [n]. The cardinality of T is clearly 3 . Let us fix a
function ρ from T to X.
The set of clauses GTn,ρ 0 consists of the following axioms:
xi j ↔ ¬x ji 1≤i< j≤n ,
_
xk j j ∈ [n] ,
k∈[n] , k6= j
¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ∨ ρ(i1 , i2 , i3 ) for (¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ) ∈ GTn ,
¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ∨ ¬ρ(i1 , i2 , i3 ) for (¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ) ∈ GTn .
0
For each transitivity axiom in the original set GTn involving vertices i1 , i2 , i3 , the set of clauses GTn,ρ
contains exactly two axioms produced by adding a new literal ρ(i1 , i2 , i3 ) or its negation ¬ρ(i1 , i2 , i3 ).
In the definition above, the condition “for (¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ) ∈ GTn ” must be understood relative
to a choice of ordering of the literals in the clause in question. That is to say, in defining the new
set of clauses, we need to make an arbitrary choice of the three possible representations of the clause
{¬xi1 i2 , ¬xi2 i3 , ¬xi3 i1 } as an ordered disjunction.
0 in general resolution of size O(n3 ).
Corollary 3.4. For any ρ, there is a refutation of GTn,ρ
0 in general resolution in O(n3 )
Proof. It is easy to see that the principle GTn can be inferred from GTn,ρ
steps. Hence, the Corollary follows by Theorem 3.2.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 85
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
The refutation of the preceding corollary is irregular. By contrast, the main theorem of this section
0 has exponential size. Before proving this lower
shows that for certain ρ, any regular refutation of GTn,ρ
bound, we require some definitions and lemmas.
Definition 3.5. For an assignment α on X let Supp(α) be the set of all i ∈ [n] such that α assigns a value
to either xi j or x ji for some j.
Recall the notion of critical assignment for GTn [5]. We generalize it to the case of partial critical
assignments:
Definition 3.6. For a subset of vertices S ⊂ [n] a partial critical assignment for S is an arbitrary assign-
ment α that gives values to all variables xi j , i, j ∈ S and for any clause C of the original principle GTn ,
Cdα 6≡ 0.
Thus an assignment is critical iff it does not violate the properties of the linear ordering (recall that
we associate variable xi j with a predicate i j). Hence partial critical assignments α are in one-to-one
correspondence with all linear orderings on the set Supp(α). This semantical interpretation is essential
and we will use it throughout the proof.
Lemma 3.7. Assume that α is a critical partial assignment with | Supp(α)| < n − 2 and the variable
xi j is unassigned by α. Then for any ε ∈ {0, 1}, α can be extended to a critical assignment α 0 with
| Supp(α 0 )| ≤ | Supp(α)| + 2 such that α 0 (xi j ) = ε.
Proof. The proof becomes trivial after the decoding of the definitions: we have a linear ordering on a set
S with |S| < n − 2. We need to extend this ordering on one or two new elements (depending on whether
i or j is already contained in S). Clearly we can set i ≺ j as well as i j and extend our ordering in the
correct way.
Lemma 3.8. Assume that α is a critical partial assignment with | Supp(α)| < n − 2 and i1 , i2 , i3 are
distinct elements from [n] \ Supp(α). Then α can be extended to a total assignment for X so that all
axioms of the original principle GTn except the axiom ¬xi1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 are satisfied.
Proof. We need to extend the linear ordering on Supp(α) to some total (contradictory) ordering on [n].
For that we extend α to some arbitrary partial critical assignment on [n] \ {i1 , i2 , i3 }, then set i1 i2
i3 i1 and make i1 , i2 , i3 greater than the rest of the vertices.
Lemma 3.9. For n sufficiently large, there exists a restriction ρ such that for every S and xi j , where S
0 , there exist three distinct
is a subset of [n] of size at most n/100 and xi j is a variable underlying GTn,ρ
elements i1 , i2 , i3 ∈ [n] \ S such that ρ(i1 , i2 , i3 ) = xi j .
Proof. Fix a set S, |S| ≤ εn, ε = 1/100, and fix some xi j . Choose ρ uniformly at random from all
functions mapping T to X. Then the probablity that ρ is bad for (S, xi j ) is
n−εn 3 3 3
n(n − 1) − 1 ( 3 ) 1 (n−εn) /12 1 n (1−ε) /12
3
≤ 1− 2 = 1− 2 ≤ e−n(1−ε) /12 .
n(n − 1) n n
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 86
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
Thus the probability that a given ρ is bad for all (S, xi j ) is at most
n 3 3 3
n(n − 1) · · e−n(1−ε) /12 ≤ n2 · eH(ε)n · e−n(1−ε) /12 = n2 · e(H(ε)−(1−ε) /12)n ≤ n2 · e−.0248n .
εn
n
≤ eH(ε)n where H(x) = −x ln x − (1 − x) ln(1 − x) is
The first inequality follows from the fact that εn
the entropy function. The last inequality follows by choosing ε = 1/100. The above quantity is clearly
less than 1 for n sufficiently large, and thus there exists a ρ satisfying the conditions of the lemma.
Theorem 3.10. For n sufficiently large, there exists ρ such that any regular resolution refutation of
0 has size greater than 2n/200 .
GTn,ρ
Proof. Fix a good ρ such that the above lemma holds. Let R be a regular resolution refutation of GTn,ρ 0 .
We will single out a particular set of distinct paths in the refutation, and then show that this set has
exponential size. These paths are defined by successive extensions; at each node ν along these paths we
define an auxiliary critical assignment αν that falsifies the clause in ν.
Initially we start with a single path at the root and α is empty. Now assume that we have defined
l distinct paths up to the nodes ν1 , . . . , νl . For each node νk with | Supp(ανk )| < n/100 we extend the
corresponding path in the following way:
• If a variable xi j is queried at νk and its value is already defined by α then we extend our path
according to this value; α does not change.
• If a variable xi j is queried at νk and either i or j does not belong to Supp(ανk ) then νk is a branching
node and we proceed in the following way. Assume that the answer 0 to xi j leads to the vertex
νk0 and 1 to νk1 . We extend the existing path up to both νk0 and νk1 . For each ε ∈ {0, 1} we
extend ανk by Lemma 3.7 to an arbitrary partial critical assignment ανkε such that ανkε (xi j ) = ε
and | Supp(ανkε )| ≤ | Supp(ανk )| + 2.
We use this strategy to extend paths till every path leads to a node with | Supp(α)| ≥ n/100. Since
the value of | Supp(α)| can increase at most by 2 in branching nodes, every path has at least n/200
branching nodes, hence there are at least 2n/200 distinct paths. It is left to show that they do not intersect
each other.
For the sake of contradiction, assume that two distinct paths diverge in the node ν1 and then merge
again in the node ν2 . Assume that the variable xi j is queried in ν1 . The key observation is that xi j is
forgotten in ν2 (because the clause in ν2 cannot contain both literals xi j and ¬xi j ). By Lemma 3.9 we
can choose three vertices i1 , i2 , i3 6∈ Supp(αν2 ) such that ρ(i1 , i2 , i3 ) = xi, j . Now let us set by Lemma 3.8
0 except A = ¬x
the rest of variables so that all axioms of GTn,ρ 0 i1 i2 ∨ ¬xi2 i3 ∨ ¬xi3 i1 ∨ xi j or A1 = ¬xi1 i2 ∨
¬xi2 i3 ∨ ¬xi3 i1 ∨ ¬xi j are satisfied. We produce a total assignment that falsifies the clause Cν2 labeling ν2
(because it is an extension of αν2 ) and all violated clauses contain the forgotten xi j . The contradiction
with Lemma 2.3 proves the Theorem.
The same procedure can be applied to the set of clauses MGTn [5] that results from GTn if we replace
all wide clauses with equivalent 3-CNF’s, thus yielding a bounded width separation between regular and
general resolution.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 87
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
We note that the above lower bound could have been made for an explicit ρ, rather than a random
ρ. For example, we could define ρ(x1 , x2 , x3 ) by n(i1 + i2 ) + i1 + i3 (mod n2 ). However, for simplicity
of presentation, we chose to use a random ρ. Note that the above argument actually shows that GTn,ρ 0 is
hard for almost all ρ.
4 Second example: the stone formulas
4.1 Definitions
Our second example will be a generalization of the implication graph formulas, first introduced by Raz
and McKenzie [21], and also used in subsequent papers [4, 6, 7]. Let G be a directed, acyclic graph, with
fan-in 2, n vertices, and a single sink vertex; we shall call a graph satisfying these conditions a pointed
graph. We shall use the phrase “decorated graph” to refer to a pair (G,U), where G = (V, E) is a pointed
graph, and U is a subset of V not containing the sink.
The implication graph formulas encode the following contradictory statement: “All of the source
vertices and the vertices in U are colored red, the sink is colored blue, and if both the predecessors of a
vertex are red, so is the vertex itself.” In order to make the formulas difficult for regular resolution, we
express this statement somewhat indirectly, so that instead of speaking directly of colored vertices, we
introduce extra variables speaking of the placement of colored stones on the vertices.
The decorated graph (G,U) can be viewed as a board for a board game such as Othello. Additionally
we assume that we have a set S of m ≥ n stones that are to be placed on the board, each of which can be
colored red or blue. (The reader might picture these stones as similar to the discs in the game of Othello,
being red on one side and blue on the other; thus they can be red or blue depending on which side is up.)
Our “stone formulas,” Stone(G,U, S), are defined as follows. Let (G,U) be a decorated graph, where
G = (V, E), |V | = n, and S is a set of m ≥ n stones. Let Sources(G) be the source vertices of G. The
variables of the formula are Pi, j , i ∈ (V \ U) and j ∈ S, and R j , j ∈ S. The variable Pi, j says “Vertex i
contains stone j,” or “Stone j is placed on vertex i,” while R j says “Stone j is colored red,” and ¬R j says
“Stone j is colored blue.” We call a variable Pi, j an edge variable, and a variable R j a stone variable.
For a vertex i ∈ V , and a stone t ∈ S, let Di,t be 1 if i ∈ U, otherwise, Di,t is the formula (Pi,t ∧ Rt ). The
clauses are as follows. For clarity, some clauses are expressed in implicational form.
{Pi, j | j ∈ S}, i ∈ V \ U. These clauses express the fact that every vertex contains some stone
W
(i)
(the vertices in U should be thought of as containing a particular red stone).
(ii) For all vertices k ∈ Sources(G) \U and stones j, (Pk, j → R j ).
(iii) For the sink vertex s and stone j, (Ps, j → ¬R j ).
(iv) For all vertices i, j, k such that (i, k) and ( j, k) are edges in G, where k ∈ V \U, and for all stones
t, u, v, (Di,t ∧ D j,u ∧ Pk,v → Rv ). That is, if the stones t, u, v are placed on the vertices i, j, k, and t
and u are both red, then the stone v must also be red. Since this clause expresses an induction rule,
we shall refer to it as an “induction clause” associated with the vertex k.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 88
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
We write Stone(G, S) for the special case of the stone formulas where U = 0.
/ It is not hard to check
that the number of variables in Stone(G, S) is (n + 1)m, and the number of clauses in the formula is
O(m3 n).
Lemma 4.1. For all m and all directed acyclic graphs G, Stone(G, S) has a resolution refutation of size
O(m3 n).
Proof. For a vertex k with predecessors i and j, we will say that k is colored red if we have derived
all clauses of type (ii) for k. The refutation proceeds inductively from the source vertices to the sink,
deriving all clauses of type (ii) for every k in the graph.
Let us assume that both predecessors i and j of a vertex k are colored red. We first derive all of
the clauses (¬Pi,t ∨ ¬Pj,u ∨ ¬Pk,v ∨ Rv ) for t, u, v ∈ S, by resolving clauses of type (ii) against appropriate
induction clauses. There are m3 such clauses, and each can be derived in two steps, so this part of the
proof takes O(m3 ) steps. Next, we derive all clauses of the form (¬Pj,u ∨ ¬Pk,v ∨ Rv ), by resolving the
previously obtained clauses against clauses of type (i). There are m2 such clauses, each of which takes
m steps to obtain, so this part of the proof also takes O(m3 ) steps. We then repeat this pattern to derive
all clauses of the form (¬Pkv ∨ Rv ), in O(m2 ) steps, completing the induction step.
Finally, when the sink s is colored red, we can derive the empty clause from Rs and ¬Rs in O(m)
steps. The entire refutation takes O(m3 n) steps.
The refutation constructed in the preceding lemma is highly irregular since, at each induction step,
we resolve on all the stone variables, so that there are paths in the derivation in which a stone variable is
resolved on over and over again. The regularity restriction rules out a refutation of this type, and (as we
shall see below), any regular refutation has to be exponentially large.
4.2 Graph pebbling
In order to prove an exponential lower bound for the stone formulas, we will need to begin with a graph
G with high pebbling number. The next definition describes a slight generalization of the usual concept
of pebbling number.
Definition 4.2. Let (G,U) be a decorated graph. A configuration is a subset of V . A pebbling of a
vertex v from U in G is a sequence C0 ,C1 , . . . ,C` of configurations, with C0 = 0/ and v ∈ C` , in which
each configuration Ci+1 follows from Ci by one of the following rules:
1. Any vertex u ∈ U ∪ Sources(G) can be added to Ci , i. e. Ci+1 = Ci ∪ {u}.
2. A vertex u can be added to Ci to get Ci+1 = Ci ∪ {u}, if all immediate predecessors of u are in Ci .
3. Vertices can be removed, so that Ci+1 ⊂ Ci .
The complexity of a pebbling of v from U is the maximal size of any configuration in the sequence. The
pebbling number Peb(G,U) of a decorated graph (G,U) is the minimal number n for which there exists
a pebbling of the sink of G from U with complexity n. The pebbling number Peb(G) of a pointed graph
is the pebbling number of the decorated graph (G, 0).
/
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 89
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
Pointed graphs requiring large pebbling number were constructed in a paper by Celoni, Paul and
Tarjan, based on a construction of Valiant.
Lemma 4.3 (Celoni, Paul and Tarjan [8]). There is a constant β > 0 such that for all sufficiently large
n, there is a pointed graph G with n vertices that has pebbling number Peb(G) ≥ β n/ log n.
The following definition is useful in describing the effect of restrictions on stone formulas.
Definition 4.4. For a pointed graph G = (V, E) and v ∈ V , let G[v] denote the induced subgraph of G on
those vertices u from which v is reachable, i. e. there is a directed path from u to v.
The next lemma shows that if we add a new “free” vertex to a decorated graph with high pebbling
number, then we can always find a subgraph with high pebbling number.
Lemma 4.5. Let (G,U) be a decorated graph with pebbling number p + 1, and i an vertex of G not in
U. Then either (G,U ∪ {i}) or (G[i],U ∩ G[i]) has pebbling number at least p.
Proof. Assume that both (G,U ∪ {i}) and (G[i],U ∩ G[i]) have pebbling number at most p − 1. Then
there is a legal pebbling C0 , . . . ,Cl = {i} of G[i] from U ∩ G[i] and a legal pebbling D0 , . . . , Dm of G from
U ∪ {i} each of complexity at most p − 1. Then
C0 , . . . ,Cl , D1 ∪ {i}, . . . , Dm ∪ {i}
is a legal pebbling of (G,U) from U of complexity at most p, contradicting the assumption that (G,U)
has pebbling number p + 1.
The next definition picks out a type of vertex that plays a central role in the restrictions described in
the following subsection.
Definition 4.6. Let (G,U) be a decorated graph. A vertex v ∈ G is important if there is a path from v to
s not containing any vertex in U, otherwise v is unimportant.
Lemma 4.7. If Peb(G,U) = p, then there exist at least p − 2 important vertices in G.
Proof. We prove the lemma by showing that if (G,U) is a decorated graph, then there is a legal pebbling
of the sink of G from U in which at most two unimportant vertices occur in every configuration. Let
C0 , . . . ,C` be a legal pebbling of the sink s from U, and D0 , . . . , D` the sequence obtained by setting Di =
(Ci \ J), where J is the set of unimportant vertices in the pebbling. We argue by induction, proceeding
backwards from D` to D0 , that the resulting sequence of configurations (with no unimportant vertices)
can be converted into a legal pebbling of s from U, by using at most two additional vertices from U to
go from one configuration to another in the sequence.
By definition, s is important, so we only need to examine the case where Ci+1 is obtained from Ci
by an appropriate rule. Let us suppose that Ci+1 was obtained from Ci by the Rule 2 in Definition 4.2,
and that the vertex u is important, but one or both of the predecessors of u is unimportant. This can
only happen if each predecessor in question is in U. Hence, we can obtain Di+1 from Di by one or two
applications of Rule 1 in Definition 4.2, followed by an application of Rule 2, followed by a deletion of
the one or two vertices added when applying Rule 1.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 90
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
4.3 Critical assignments for stone formulas
In the remainder of the paper, we concentrate on certain special assignments for the formulas
Stone(G,U, S). These assignments are determined by two items, a mapping from (some of the) ver-
tices to stones, and a coloring of some of the stones.
Definition 4.8. Let G = (V, E) be a pointed graph, and S a set of stones, where |S| ≥ |V |. A restriction
ρ = hµ, κi for (G, S) is determined by
1. A bijective map µ from a subset of V to S;
2. A coloring κ assigning a subset of S to the set {R, B} (i. e., we assign the colors red and blue to
some of the stones).
The assignment σ determined by ρ is defined by setting:
• σ (Pi, j ) = 1 if hi, ji ∈ µ, σ (Pi, j ) = 0 if i or j are in Dom(µ) ∪ Ran(µ), but hi, ji 6∈ µ;
• σ (R j ) = 1 if κ( j) = R, σ (R j ) = 0 if κ( j) = B;
• If j is in the domain of κ, but not in the range of µ, then Pi, j = 0, for all i ∈ V .
Thus ρ is a restriction on the decorated graph, and σ is a corresponding restriction on the proposi-
tional formula. If |µ| = r and |κ| = s, then we say that σ is a restriction with parameters r and s. To
simplify notation, we shall identify a restriction with the assignment that it determines.
There are two special types of restrictions that are important in what follows. The first type is one in
which none of the stones placed on vertices are assigned colors, that is to say, Ran(µ) ∩ Dom(κ) = 0, /
and furthermore, the parameters r and s are equal. In this case, we shall describe ρ = hµ, κi as an r-
restriction. The second special type of restriction is one in which all of the stones placed on vertices are
assigned colors, that is, Ran(µ) ⊆ Dom(κ). This second type of restriction we call a clamping.
Definition 4.9. Let (G,U) be a decorated graph, k a vertex in G, and χ a partial coloring of G, that is,
χ is a map from a subset of V to {R, B}. We say that χ is a k-based coloring of (G,U) if the following
conditions hold:
1. If i ∈ U, then χ(i) = R;
2. There is a path π in G from k to the sink of G so that the vertices in the path are exactly those to
which χ assigns the color blue;
3. If a vertex i is not in G[k] ∪ π, then χ(i) = R.
We say that χ is k-critical if it is a total coloring of G.
Lemma 4.10. If (G,U) is a decorated graph and k an important vertex of G, then there is a k-critical
coloring of (G,U).
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 91
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
Proof. By assumption, there is a path from k to the sink not passing through any vertices in U. Color all
the vertices in this path blue, and all other vertices in G red. Since k is the only blue vertex in G, all of
whose predecessors are colored red, this is a k-critical coloring of (G,U).
If χ is a coloring of a decorated graph (G,U), then a clamping ρ = hµ, κi is said to be compatible
with χ if Dom(χ) = Dom(µ), and for any vertex in Dom(χ) = Dom(µ), κ(µ(i)) = χ(i). If χ is a
k-based coloring, then we say that ρ is a k-based clamping, and that it is k-critical if it is compatible
with a k-critical coloring. The reader can easily check that if ρ is a k-critical clamping of (G,U), then
it forces all the clauses in Stone(G,U, S) to true, except for a single induction clause, which is forced to
false. In addition, we say that a restriction is compatible with a k-based coloring χ if it can be extended
to a clamping compatible with χ.
The next two lemmas, which are straightforward to prove, are used repeatedly in the rest of the
proof.
Lemma 4.11. Let (G,U) be a decorated graph, and χ a partial coloring of G = (V, E). In addition, let
S be a set of stones with |S \ Dom(κ)| ≥ |V |, and ρ = hµ, κi a restriction for (G, S) so that Dom(µ) ⊆
Dom(χ), and κ(µ(i)) = χ(i), whenever i ∈ Dom(µ) ∩ Dom(χ) and κ(µ(i)) is defined. Then ρ is
compatible with χ.
Proof. Extend µ to a bijection µ 0 from Dom(χ) to S \ Dom(κ), and then set the colors of stones in the
range of µ 0 by setting κ 0 (µ(i)) = χ(i) for all i ∈ Dom(χ) = Dom(µ 0 ). Then ρ 0 = hµ 0 , κ 0 i is a clamping
compatible with χ.
The next lemma follows readily from the definitions.
Lemma 4.12. If ρ = hµ, κi is a k-based clamping of Stone(G,U, S) with parameters r, s, then
Stone(G,U, S)dρ = Stone(G[k],U 0 , S0 ) ,
where U 0 = G[k] ∩ (U ∪ Dom(µ)) and S0 = S \ Dom(κ).
Lemma 4.13. Let ρ = hµ, κi be an r-restriction for (G, S), where G has pebbling number N, and
|S| ≥ |V |. Then there is a vertex k ∈ G and ρ 0 = hµ, κ 0 i so that:
1. ρ 0 = hµ, κ 0 i is a k-based clamping of (G, S), with κ ⊆ κ 0 ;
2. (G[k],U) has pebbling number at least N − r, where U = G[k] ∩ Dom(µ).
Proof. We construct ρ 0 by first constructing an appropriate k-based coloring χ of G, with Dom(χ) =
Dom(µ), and then using Lemma 4.11 to find the required k-based clamping. At each stage in the
construction, we are given a designated vertex k ∈ G, and a k-based coloring χ of G. Initially, no vertices
in G are assigned colors, and we choose the sink as the designated vertex. In successive stages, we
choose a new designated vertex k0 ∈ G, and a new coloring χ 0 , and we make these choices in such a way
as to maximize the pebbling number of the decorated graph (G[k0 ], G[k0 ] ∩U(k0 , χ 0 )), where U(k0 , χ 0 ) is
the set of vertices in G[k0 ] mapped to R by χ 0 .
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 92
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
To be more precise, let us suppose that we have µ(i) = t, and that the stone t has not yet been
assigned a color. Let U = U(k, χ). Compare the two values
p1 = Peb(G[k],U ∪ {i}) and p2 = Peb(G[i],U ∩ G[i]) .
If p1 ≥ p2 , then set k0 = k and extend χ by setting χ 0 (i) = R and χ 0 (i0 ) = R for all i0 that are unimportant
in (G[k],U ∪ {i}). If p1 < p2 then set k0 = i, choose a path in G from i to k, and extend χ to an i-based
coloring, χ 0 , of (G,U ∩ G[i]). Letting U 0 = U(k0 , χ 0 ), by Lemma 4.5, Peb(G[k0 ],U 0 ) ≥ Peb(G[k],U) − 1.
Let k and χ be the designated vertex and k-based coloring produced at the end of this process, that is,
when Dom(χ) = Dom(µ). By Lemma 4.11, ρ is compatible with χ, so that there is a a k-based clamping
ρ 0 = hµ, κ 0 i compatible with χ. By definition, U(k, χ) = G[k] ∩ Dom(µ), and since the construction has
r steps, (G[k], G[k] ∩ Dom(µ)) has pebbling number at least N − r.
5 The lower bound for stone formulas
The general structure of the proof of the lower bound is similar to that of Beame and Pitassi’s [3]
simplified lower bound proof for the pigeonhole principle. That is, we will assume for the sake of
contradiction that we have a short (sub-exponential) refutation of a stone formula. We will first show that
we can apply a restriction to some (but not too many) of the variables such that the resulting refutation,
after the restriction, is still a refutation of a stone formula on a reduced set of variables, that contains
no complex clauses. Secondly, we argue separately that any regular resolution refutation of the formula
must contain a complex clause, and thus we reach a contradiction.
Definition 5.1. A clause C is called d-complex if one of the following holds:
1. C contains at least d distinct stone variables, or
2. There is a matching of size at least d from vertices to stones such that C contains the negative edge
literals ¬Pi, j for each pair (i, j) in the matching.
3. There is a subset W of at least d vertices, such that for all i ∈ W there is a subset Pi of at least d
stones, such that all literals Pi, j , i ∈ W , j ∈ Pi are present in C.
There are three parameters in our lower bound, γ, δ , and ε. The lower bound is of the form
3
2δ n/(log n) ; the parameter associated with a complex clause is εn/ log n and the size of the restriction
is γn/ log n.
Lemma 5.2 (Restriction Lemma). Let γ, δ , ε be constants such that 0 < γ, δ , ε < 1 and 3δ /ε 2 ≤ γ ≤
ε/2. Let G = (V, E) be a pointed graph with |V | = n, and let R be a resolution refutation of Stone(G, S),
3
|S| = 3n, of size at most s = 2δ n/(log n) . Then there exists an r-restriction ρ, r = γn/ log n, such that Rdρ
has no (εn/ log n)-complex clauses.
Proof. We will divide up the complex clauses into those of the first type and those of type two or three.
For those of type two or three, we will greedily choose a matching between vertices and stones that
forces all complex clauses of these types to true.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 93
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
The total number of pairs in V × S to choose from is 3n2 ; each complex clause of the third type can
be forced to true by choosing a Pi, j from (εn/ log n)2 pairs; each complex clause of the second type can
be forced to true by choosing a Pi, j from (ε(3n − 1)n)/ log n ≥ (εn/ log n)2 pairs. Thus, by averaging,
there exists a Pi, j such that at least s(εn/ log n)2 /3n2 ≥ s(ε 2 /3(log n)2 ) complex clauses of the second
and third type are forced to true.
Hence to force all the complex clauses of these types to true we need to choose a matching of size
log s δ n / (log n)3 3δ n γn
ε 2 ≤ ε 2 / 3(log n)2 ≤ ε 2 log n ≤ log n .
log 1/ 1 − 3(log n)2
Now for the clauses of the first type, notice that there are 3n − γn/ log n ≥ 2n stones left that are
untouched by the matching chosen above, and any complex clause of the first type still contains (ε −
γ)n/ log n ≥ εn/2 log n literals corresponding to these stones, since γ ≤ ε/2.
Since the refutation has size at most s, there are at most s clauses of the first type, each containing
εn/2 log n distinct stone variables that have not been set by the restriction already chosen. Each of these
is thus set to one by εn/2 log n out of at least 4n choices of stone literals.
By averaging, there must be one stone literal that forces s(ε/8 log n) of the complex clauses of type
one to true. Thus to force all complex clauses of this type to true we need to set
log s δ n / (log n)3 8δ n γn
≤ ≤ 2
≤
ε
log 1 / 1 − 8 log n
ε / 8 log n ε(log n) log n
stone literals.
Our last lemma shows the existence of a complex clause for any initial graph with sufficiently large
pebbling number. This is the only part of the proof in which the regularity restriction is used.
Lemma 5.3 (Complex Clause Lemma). Let (G,U) be a decorated graph with
Peb(G,U) = N = Ω(n/ log n) ,
where G has n vertices. Then for |S| = m = 2n, and n sufficiently large, any regular resolution refutation
of Stone(G,U, S) contains an (N/16)-complex clause.
Proof. Let R be a regular resolution refutation of Stone(G,U, S). We will follow a particular path π
partway through the refutation; this path will be determined by giving a strategy for answering queries.
The path is defined by successive extensions; at each stage in the definition, we define three auxiliary
objects. First, at each stage, we single out a designated vertex k in G, second, we define a k-based
coloring χ of G, third, we define a restriction ρ compatible with χ. The answers given along the path at
each stage are compatible with the partial assignment, σ , determined by ρ. At each stage, the designated
node k and the coloring χ determine the subgraph G[k] of G, together with a subset U of G[k], consisting
of the vertices i of G[k] with χ(i) = R.
Initially, we start the path at the root of the refutation. The designated vertex is the sink s of G,
χ(u) = R for u ∈ U, and χ(s) = B. Now assume that we have defined the path up to a node ν, together
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 94
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
with a designated vertex k, a k-based coloring χ, and a restriction ρ compatible with χ. In addition,
let (Gν ,Uν ) be the decorated graph (G[k],U), where U is the set of vertices in G[k] colored red by χ.
We want to extend the path by providing an appropriate answer to the variable queried at the node ν;
we need also to define a new designated vertex k0 , a new k0 -based coloring χ 0 and a new restriction ρ 0
compatible with χ 0 . In each case, the answers to the queries will be given as an extension of the current
restriction ρ – unless the current restriction answers the query already, as can happen in the last case
below.
• If a stone variable R j is queried at ν and it is not currently placed on a vertex, i. e. for no vertex i
do we have ρ(Pi, j ) = 1, then extend ρ by coloring j red or blue arbitrarily. Set k0 = k, χ 0 = χ.
• If a stone variable R j is queried at ν, and it is already placed on a vertex i, i. e. ρ(Pi, j ) = 1, then
we answer as follows:
– If i is colored by χ then answer accordingly. That is, if χ(i) = R, then set ρ(R j ) = 1, and if
χ(i) = B, then set ρ(R j ) = 0. Then set k0 = k and χ 0 = χ.
– If i is not assigned a color by χ, but is not important with respect to (Gν ,Uν ), then set
ρ(R j ) = 1. Extend χ by setting χ 0 (i) = R, and set k0 = k.
– Otherwise, answer to maximize the pebbling number of the associated decorated graph. That
is, compare the two values
p1 = Peb(Gν ,Uν ∪ {i}) and p2 = Peb(Gν [i],Uν ∩ G[i]) .
If p1 ≥ p2 , then set k0 = k, extend χ by setting χ 0 (i) = R and χ 0 (i0 ) = R for all i0 that are
unimportant in (Gν ,Uν ∪ {i}), and set ρ(R j ) = 1.
If p1 < p2 then set Gξ = Gν [i], choose a path in Gν from i to k, extend χ to an i-based
coloring of G, and set ρ(R j ) = 0.
• If an edge Pi, j is queried at ν, but the assignment, σ , defined by ρ is not defined at Pi, j , then set
ρ(Pi, j ) = 1 Otherwise, answer consistent with σ , the assignment defined by ρ. Set k0 = k and
χ 0 = χ.
Claim 5.4. There is a node on the path defined above where exactly N/2 stones are queried.
The path can only end in an initial clause of type (i) or an induction clause of type (iv). The former
case can only occur if all the stones have received colors, and thus all stones must have been queried.
In the latter case, note that at the root, we have Peb(Gν ,Uν ) = N, by Lemma 4.5 the pebbling number
decreases by at most 1 with each answer to a query, and only at nodes where a stone is queried. But when
we reach an induction clause, the pebbling number has decreased to 0. Therefore the path followed by
the above strategy will not finish until at least N stones are asked about. Thus, there is some node ξ on
the path where exactly N/2 stones are queried.
The pair (Gξ ,Uξ ) associated with ξ has pebbling number at least N/2. This follows from the fact
that the pebbling number decreases by at most 1 at each stone query, and we have queried exactly N/2
stones. By Lemma 4.7, there are at least N/2 − 2 important vertices in (Gξ ,Uξ ).
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 95
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
Claim 5.5. The clause Cξ attached to the node ξ must be N/16 complex.
Let ρ = hµ, κi be the restriction associated with ξ . Let I be the set of important vertices in (Gξ ,Uξ ).
If at least N/8 of the vertices in I are mapped by µ and the mapping is remembered, i. e., the corre-
sponding edge variables set to 1 by ρ occur negated in Cξ , then Cξ is an N/8-complex clause of type
two. Hence, in the remainder of the proof, we shall assume that there is a subset I 0 ⊂ I of at least N/8
vertices that are either unmapped by µ or are mapped by µ but all of the edge variables corresponding
to this part of the mapping are forgotten.
There are several cases. We will introduce some terminology to help with these cases. We partition
the set of N/2 stones queried on the path to ξ into the free stones, F, and the attached stones, A. F
consists of those stones queried along the path to ξ that are not in the range of µ; A are those stones
queried on the path to ξ that are in the range of µ. There are two general cases to consider. The first
case (which is slightly easier) is when |F| ≥ N/4 and the second case is when |A| ≥ N/4.
Assume first that |F| ≥ N/4. We will show that the clause Cξ attached to the node ξ must be N/16-
complex. The first subcase is when at least N/8 of the stones in F occur in Cξ . In this case, Cξ is an
N/8-complex clause of type one. If this subcase does not occur, then at least N/8 of the stones in F are
forgotten at the node ξ . Let F 0 ⊂ F be this set of at least N/8 forgotten free stones. Now we claim that
for every i ∈ I 0 and t ∈ F 0 , the literal Pi,t must occur in Cξ , and thus Cξ is an N/8-complex clause of type
three.
Suppose that the literal Pi,t does not occur in Cξ for some i ∈ I 0 , t ∈ F 0 . Then we can modify the
restriction ρ to ρ 0 by mapping i to t, and if ρ(i) = u, where u 6= t, then we assign a color to u, if it was
not colored already. Because i ∈ I 0 , we know that for all j ¬Pi, j does not occur in Cξ ), and thus it follows
that ρ 0 (Cξ ) = 0. Since i is important, there is an i-based coloring extending the coloring χ associated
with ξ , and this i-based coloring can be extended to an i-critical coloring. Let σ be an i-critical clamping
compatible with this coloring, extending the restriction ρ 0 , in which σ (Pi,t ) = 1 and σ (Cξ ) = 0. The only
initial clause falsified by σ is an induction clause associated with i, containing the variable Rt . However,
by Corollary 2.4, Cξ was inferred from clauses none of which contain the forgotten variable Rt . This is
a contradiction, so it follows that Cξ must contain the variables Pi,t .
We will now argue the second case, when |A| ≥ N/4. Let B be the subset of vertices that are mapped
by ρ to stones in A. Clearly, |B| = |A|. The first subcase, 2a, is when at least N/16 of the stones in A are
remembered. In this case, Cξ is an N/16-complex clause of type one.
The second subcase, 2b, is when for at least N/16 of the vertices i in B, the mapping of i into A
is remembered, i. e., the negative edge literal ¬Pi, j where j = µ(i) occurs in Cξ . In this case, Cξ is an
N/16-complex clause of type two.
The third subcase, 2c, is when for at least N/16 of the vertices i in B, at least N/2 zero-edges
containing i are remembered. That is, the edge variable Pi, j occurs in Cξ for at least N/2 distinct j’s. In
this case, Cξ is an N/16-complex clause of type three.
If none of the subcases 2a, 2b or 2c occur, then there are sets B0 ⊂ B and A0 ⊂ A each of size exactly
N/16 such that ρ defines a mapping from B0 to A0 but the mapping is forgotten; the color of each stone
in A0 is forgotten, and for every i ∈ B0 , at most N/2 zero-edges out of i are remembered at ξ . We claim
that for every i ∈ I 0 − B0 and t ∈ A0 , the literal Pi,t must occur in Cξ .
Suppose that this is not the case and let Pi,t be some literal that does not occur in Cξ , where i ∈ I 0 ,
t ∈ A0 and let i0 ∈ B0 be the vertex that is mapped to t by ρ. Then we will modify the restriction ρ to
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 96
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
obtain ρ 0 as follows. First, ρ 0 will map i to t. Secondly, ρ 0 will map i0 to some unqueried stone t 0 such
that the edge from i0 to t 0 has not already been remembered to be 0. Further, the color associated with t 0
will be chosen to be the same as the color given to t by ρ; that is, the underlying coloring of the graph
will be the same for ρ and for ρ 0 . It will still be the case that ρ 0 (Cξ ) = 0 since we have not tampered with
any of the literals that are remembered (i. e., that occur in Cξ .) Now as in Case 1, we will extend ρ 0 to
an i-critical coloring, σ , extending the restriction ρ 0 . Since the only initial clause falsified by σ contains
the variable Rt , and Rt is not remembered, we have reached a contradiction, and thus Cξ must contain
all such variables Pi,t , showing that it is an N/16-complex clause of the third type. This completes the
proof of the complex clause lemma.
We are ready to state the main theorem of this section.
Theorem 5.6. Let G be a pointed graph with n vertices and pebbling number N = Ω(n/ log n). Then
any regular resolution refutation of Stone(G, S), where |S| = 3n requires size 2Ω(n/(log n) ) .
3
Proof. We start with a pointed graph G with n vertices and pebbling number Peb(G) ≥ β n/ log n, in
accordance with Lemma 4.3. Set ε = β /32, γ = ε/2 = β /32 and δ = ε 3 /6 = β 3 /199608, so that we
have 3δ /ε 2 ≤ γ ≤ ε/2. Now assume that there is a regular resolution refutation R of Stone(G, S), with
3
size at most S = 2δ n/(log n) . By Lemma 5.2 (the Restriction Lemma), there is a restriction ρ of size
r = γn/ log n, such that Rdρ has no (εn/ log n)-complex clauses.
By Lemma 4.13, there is a vertex k ∈ G and ρ 0 = hµ, κ 0 i so that ρ 0 is a k-based clamping of (G, S),
with κ ⊆ κ 0 , and (G[k], G[k] ∩ Dom(µ)) has pebbling number at least N − r ≥ N/2. By Lemma 5.3 (the
Complex Clause Lemma), the refutation Rdρ must contain a (β n/32 log n)-complex clause, contradict-
ing the conclusion of the previous paragraph.
6 Open problems
The present paper gives a separation between regular and general resolution that seems close to opti-
mal. Nevertheless, there are still mysteries surrounding the exact effect of the regularity restriction. As
mentioned in the introduction, it was widely believed in the early years of research on the complexity
of resolution that optimal proofs are always regular. This belief would be justified, in a sense, if the
conjecture formulated below were proved to be true.
The most deeply investigated family of tautologies are those based on matchings in graphs, of which
the best known are the pigeonhole formulas. These examples are based on graphs G for which no
perfect matching exists; the corresponding contradictory CNF formula F(G) asserts that G has a perfect
matching. For example, the pigeonhole formula PHPn can be understood as the formula F(H), where H
is the complete bipartite graph K(n + 1, n). Other well-studied examples are the graph-based formulas
of Tseitin [23]. For both of these families of examples, the shortest known resolution refutations are
regular.
Conjecture 6.1. For contradictory formulas expressing matching principles in graphs, and also for the
graph-based examples of Tseitin, there is always a regular refutation of minimal size.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 97
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
A proof (or disproof) of this conjecture would shed light on the question of exactly when the reg-
ularity restriction helps in searching for short refutations. For the pigeonhole formulas, we can make
an even more specific conjecture, derived from Cook [9], who gives the size of the shortest known
resolution refutation of PHPn – the proof in question is in fact regular.
Conjecture 6.2. Let PHPn be the set of clauses asserting that there is an injective mapping from a set of
size n + 1 into a set of size n, expressed as in Haken’s paper [15]. Then the minimum size of a refutation
of PHPn is n(n + 3)2n−2 .
A second open problem concerns the relative complexity of DPLL proofs augmented with clause
learning. The most successful complete satisfiability solvers are based on performing a simple back-
tracking procedure, often called DPLL search, augmented with a form of caching known as clause
learning [19, 12, 20, 2]. It is known that clause learning is at least as efficient as regular resolution [1],
and it is an important open problem to resolve the complexity of clause learning with respect to unre-
stricted resolution. In particular, it is known that Resolution polynomially simulates clause learning, but
does clause learning also polynomially simulate Resolution? We believe that the answer is no, and we
conjecture that the two families of formulas presented in this paper require superpolynomial-size clause
learning proofs.
7 Acknowledgments
The first author is grateful to A. A. Razborov for his helpful comments. The authors would also like
to thank Allen van Gelder for pointing out some errors and unclear passages in the original version.
Finally, we would like to thank an anonymous referee for many very useful suggestions.
References
[1] * FAHIEM BACCHUS , P HILIPP H ERTEL , AND T ONIANN P ITASSI: The complexity of resolution
with caching. 2006. Unpublished manuscript. 6
[2] * PAUL B EAME , H ENRY K AUTZ , AND A SHISH S ABHARWAL: Towards understanding and har-
nessing the potential of clause learning. Journal of Artifical Intelligence Research, 22:319–351,
2004. 6
[3] * PAUL B EAME AND T ONIANN P ITASSI: Simplified and improved resolution
lower bounds. In Proc. 37th FOCS, pp. 274–282. IEEE Comp. Soc. Press, 1996.
[FOCS:10.1109/SFCS.1996.548486]. 5
[4] * E LI B EN -S ASSON , RUSSELL I MPAGLIAZZO , AND AVI W IGDERSON: Near-optimal separation
of tree-like and general resolution. ECCC TR00-005, 2000. [ECCC:TR00-005]. 1, 4.1
[5] * M. B ONET AND N. G ALESI: A study of proof search algorithms for resolution and
polynomial calculus. In Proc. 40th FOCS, pp. 422–432. IEEE Comp. Soc. Press, 1999.
[FOCS:10.1109/SFFCS.1999.814614]. 3, 3, 3
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 98
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
[6] * M ARIA L UISA B ONET, J UAN L UIS E STEBAN , N ICOLA G ALESI , AND JAN J OHANNSEN: On
the relative complexity of resolution restrictions and cutting planes proof systems. SIAM Journal
of Computing, 30:1462–1484, 2000. [SICOMP:10.1137/S0097539799352474]. 1, 4.1
[7] * J OSHUA B URESH -O PPENHEIM , M ATTHEW C LEGG , RUSSELL I MPAGLIAZZO , AND T O -
NIANN P ITASSI : Homogenization and the polynomial calculus. In Proc. 27th Interna-
tional Colloquium on Automata, Languages and Programming, pp. 926–937. Springer, 2000.
[ICALP:fvxybba423y153b8]. 4.1
[8] * JAMES C ELONI , W OLFGANG PAUL , AND ROBERT TARJAN: Space bounds for a game on
graphs. Mathematical Systems Theory, 10:239–251, 1977. [Springer:u32u2r202jv33611]. 4.3
[9] * S TEPHEN A. C OOK: A short proof of the pigeon hole principle using extended resolution.
SIGACT News, 8(4):28–32, 1976. [SIGACT:10.1145/1008335.1008338]. 6
[10] * S TEPHEN A. C OOK AND ROBERT A. R ECKHOW: The relative efficiency of propositional proof
systems. Journal of Symbolic Logic, 6:169–184, 1979. 1
[11] * M ARTIN DAVIS , G EORGE L OGEMANN , AND D ONALD L OVELAND: A machine program for
theorem proving. Communications of the Association for Computing Machinery, 5:394–397, 1962.
[ACM:10.1145/368273.368557]. 1
[12] * N IKLAS E EN AND N IKLAS S ÖRENSSON: An extensible SAT-solver. In Proc. 6th International
Conference on Theory and Applications of Satisfiability Testing, pp. 502–518. Springer, 2003.
[Springer:x9uavq4vpvqntt23]. 6
[13] * A NDREAS G OERDT: Davis-Putnam resolution versus unrestricted resolution. Annals of Mathe-
matics and Artificial Intelligence, 6:169–184, 1992. [Springer:k008110v05867897]. 1
[14] * A NDREAS G OERDT: Regular resolution versus unrestricted resolution. SIAM Journal of Com-
puting, 22:661–683, 1993. [SICOMP:10.1137/0222044]. 1
[15] * A RMIN H AKEN: The intractability of resolution. Theoretical Computer Science, 39:297–308,
1985. [TCS:10.1016/0304-3975(85)90144-6]. 6.2
[16] * W ENQI H UANG AND X IANGDONG Y U: A DNF without regular shortest consensus path. SIAM
Journal on Computing, 16:836–840, 1987. [SICOMP:10.1137/0216054]. 1
[17] * JAN K RAJ Í ČEK: Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge
University Press, 1995. 2
[18] * BALAKRISHNAN K RISHNAMURTHY: Short proofs for tricky formulas. Acta Informatica,
22:253–274, 1985. [ActaInf:mp65776636126242]. 3, 3
[19] * M ATTHEW M OSKEWICZ , C ONOR M ADIGAN , Y ING Z HAO , L INTAO Z HANG , AND S HARAD
M ALIK: Chaff: Engineering an efficient SAT solver. In Proc. 38th Design Automation Conference,
pp. 530–535. ACM Press, 2001. [ACM:10.1145/378239.379017]. 6
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 99
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
[20] * A LEXANDER NADEL: Backtrack search algorithms for propositional logic satisfiability: Review
and innovations. Master’s thesis, Hebrew University, 2002. 6
[21] * R AN R AZ AND P IERRE M C K ENZIE: Separation of the monotone NC hierarchy.
Combinatorica, 19:403–435, 1999. Preliminary Version in: Proc. 38th FOCS, 1997.
[Springer:h4prxbwxpn1c8xqh]. 4.1
[22] * G UNNAR S T ÅLMARCK: Short resolution proofs for a sequence of tricky formulas. Acta Infor-
matica, 33:277–280, 1996. [ActaInf:lhrhe2glkmgflbu1]. 3
[23] * G. S. T SEITIN: On the complexity of derivation in propositional calculus. In A. O. S LISENKO,
editor, Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125. Con-
sultants Bureau, New York, 1970. 1, 6
[24] * A LASDAIR U RQUHART: The complexity of propositional proofs. The Bulletin of Symbolic
Logic, 1:425–467, 1995. 1
AUTHORS
Michael Alekhnovich [About the author]
University of California, San Diego
Jan Johannsen [About the author]
Institut für Informatik
jjohanns informatik uni-muenchen de
Toniann Pitassi [About the author]
University of Toronto
toni cs toronto edu
Alasdair Urquhart [About the author]
University of Toronto
urquhart cs toronto edu
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 100
A N E XPONENTIAL S EPARATION BETWEEN R EGULAR AND G ENERAL R ESOLUTION
ABOUT THE AUTHORS
M IKHAIL (M ISHA ) A LEKHNOVICH was born on October 26, 1978 in Moscow, USSR and
died on August 5, 2006 in a kayaking accident during a Class 6 whitewater expedition
in Russia. From 1995 to 2000, he was a student in the Department of Mathematics and
Mechanics at Moscow State University, where he was awarded Diploma with Honours.
His diploma thesis, Pseudorandom generators in propositional proof complexity, was
written under the supervision of Alexander A. Razborov. In 2000, he was a member in
the special program on Computational Complexity at the Institute for Advanced Study,
in Princeton.
From 2001 to 2003, he was a graduate student in the Department of Mathematics of the
Massachusetts Insitute of Technology. His doctoral thesis, written under the supervision
of Madhu Sudan, is entitled Propositional Proof Systems: Efficiency and Automatizabil-
ity. From 2003 to 2005 he held a postdoc position at the Institute for Advanced Study in
Princeton, where his host was Avi Wigderson. From 2005 onwards, he was an assistant
professor in the Department of Mathematics, University of California at San Diego.
Although only 27 years old at the time of his tragic death, Misha Alekhnovich already
had an impressive string of research accomplishments to his credit, including major pa-
pers on propositional proof complexity, inapproximability, and computational learning
theory.
His premature death has robbed the theory community of one of its brightest young
stars.
This biographical sketch was written by Alasdair Urquhart and Toniann Pitassi. It is an
adaptation of a longer obituary by A. Razborov, appearing in ACM SIGACT News 38/1
(March 2007), pp. 70-71. Misha’s IAS home page will be maintained indefinitely.
JAN J OHANNSEN obtained his doctoral degree from the University of Erlangen in 1996.
After a two-year postdoc at UCSD he became an Emmy Noether junior research group
leader at LMU Munich. Currently he teaches in the Computer Science Department of
the LMU Munich and heads the departmental administration. His research interests are
logic and computational complexity, in particular bounded arithmetic and propositional
proof complexity, and their relation to the complexity of satisfiability.
T ONIANN P ITASSI studied chemistry and computer science as an undergraduate at Pennsyl-
vania State University. After working for several years at Bell Laboratories, she pursued
graduate work at the University of Toronto, with advisor Stephen Cook, receiving her
Ph. D. in 1992. After a postdoc position at UCSD and faculty positions at the University
of Pittsburgh and the University of Arizona, she returned to Toronto as a faculty member
in 2000.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 101
M. A LEKHNOVICH , J. J OHANNSEN , T. P ITASSI , AND A. U RQUHART
A LASDAIR U RQUHART studied philosophy as an undergraduate in Edinburgh, Scotland,
then did his undergraduate work at the University of Pittsburgh, where he received a
Ph. D. in the Philosophy Department under the supervision of Nuel D. Belnap in 1973.
Since 1970, he has been a faculty member in the Philosophy Department at the Univer-
sity of Toronto, where he is also cross-appointed in the Computer Science Department.
His research interests include algebraic logic, non-classical logic, history of logic, and
the complexity of propositional proofs.
T HEORY OF C OMPUTING, Volume 3 (2007), pp. 81–102 102