Theory of Computing, 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 papers and grant “Theory of Computing” unlimited rights to publish the paper electronically and in hard copy. Use of the article 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.

\begin{matrix}c \\ ◯ \end{matrix} 2007 Michael Alekhnovich and Jan Johannsen and Toniann Pitassi and Alasdair Urquhart

M. Alekhnovich, J. Johannsen, T. Pitassi, and A. Urquhart

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 refutations 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 minimal 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 conclusion 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.

An Exponential Separation between Regular and General Resolution

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 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 refutations.

In this paper, we present two new families of formulas, and prove that they have simple polynomialsize 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 combinatorial 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 C⌈σ for the result of applying the assignment to C, that is, C⌈σ = 1 if σ(l) = 1 for some literal l in C, otherwise, C⌈σ 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 F ⌈σ is the conjunction of all the clauses C⌈σ, C a clause in F.

If R = C_{1},...,C_{k} is a resolution derivation from a formula F, and σ an assignment to the variables in F, then we write R⌈σ for the sequence C_{1}⌈σ,...,C_{k}⌈σ.

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 R⌈σ that is a regular resolution derivation of a subclause of C⌈σ from F ⌈σ.

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]. Although we prefer to speak in terms of refutations rather than branching programs, we nevertheless need 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_{ν}⌈σ = 0.

3 First example: GT′_{n,ρ} formulas

Our first example is based on the ordering principle first considered by Krishnamurthy [18].

Definition 3.1. Let X be the set of variables x_{ij} for i,j ∈ [n], i ≠ j. The contradiction GT_{n} consists of the following axioms:

x_{ij} ↔ ¬x_{ji}  1 ≤ i < j ≤ n ,
¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}}  for any distinct i_{1},i_{2},i_{3} ∈ [n] ,
⋁_{k∈[n],k≠j} x_{kj}  j ∈ [n] .

Our version of the contradiction GT_{n} differs slightly from the one considered in the literature, since the transitivity axioms are usually written in the form x_{i_{1}i_{2}} ∧ x_{i_{2}i_{3}} → x_{i_{1}i_{3}} (that is to say, (¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ x_{i_{1}i_{3}})). It is more convenient for us to write these axioms in the symmetric form ¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}}; these representations are equivalent in the presence of the axioms x_{ij} ↔ ¬x_{ji}. Note that there are exactly two such transitivity axioms for any set of three distinct elements i_{1},i_{2},i_{3} ∈ [n].

This contradictory principle can have several semantical interpretations; our proof will essentially depend upon the following one. Consider the variable x_{ij} as a predicate i ≻ j. The first two groups of axioms assure that ≻ is a total linear ordering on the set [n]. The principle GT_{n} claims that any such ordering never has a maximum. Krishnamurthy [18] conjectured that GT_{n} requires superpolynomialsize resolution refutations. This conjecture was refuted by Gunnar Stålmarck, who proved the following result.

Theorem 3.2. There exist regular resolution refutations of GT_{n} of size O(n^{3}).

Proof. The paper of Stålmarck [22] exhibits an explicit refutation of GT_{n} of this size. Since the number of clauses in GT_{n} is also O(n^{3}), 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 GT_{n} to make it harder for regular resolution, but preserve its unrestricted resolution complexity. For that we replace some axioms C with a pair C ∨ x_{C}, C ∨ ¬x_{C}. The variable x_{C} should be chosen in a certain precise way to simplify our lower bound.

Definition 3.3. Let X be the set of variables x_{ij} i,j ∈ [n], i ≠ j; the cardinality of X is n(n − 1). Let T be the set of all triples (i,j,k), i ≠ j ≠ k, i,j,k ∈ [n]. The cardinality of T is clearly \binom{n}{3}. Let us fix a function ρ from T to X.

The set of clauses GT′_{n,ρ} consists of the following axioms:

x_{ij} ↔ ¬x_{ji}  1 ≤ i < j ≤ n ,
⋁_{k∈[n],k≠j} x_{kj}  j ∈ [n] ,
¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}} ∨ ρ(i_{1},i_{2},i_{3})  for (¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}}) ∈ GT_{n} ,
¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}} ∨ ¬ρ(i_{1},i_{2},i_{3})  for (¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}}) ∈ GT_{n} .

For each transitivity axiom in the original set GT_{n} involving vertices i_{1},i_{2},i_{3}, the set of clauses GT′_{n,ρ} contains exactly two axioms produced by adding a new literal ρ(i_{1},i_{2},i_{3}) or its negation ¬ρ(i_{1},i_{2},i_{3}). In the definition above, the condition “for (¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}}) ∈ GT_{n}” 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 {¬x_{i_{1}i_{2}},¬x_{i_{2}i_{3}},¬x_{i_{3}i_{1}}} as an ordered disjunction.

Corllary 3.4. For any ρ, there is a refutation of GT′_{n,ρ} in general resolution of size O(n^{3}).

Proof. It is easy to see that the principle GT_{n} can be inferred from GT′_{n,ρ} in general resolution in O(n^{3}) steps. Hence, the Corollary follows by Theorem 3.2.

The refutation of the preceding corollary is irregular. By contrast, the main theorem of this section shows that for certain ρ, any regular refutation of GT′_{n,ρ} has exponential size. Before proving this lower 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 x_{ij} or x_{ji} for some j.

Recall the notion of critical assignment for GT_{n} [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 assignment α that gives values to all variables x_{ij}, i,j ∈ S and for any clause C of the original principle GT_{n}, C⌈α ≢ 0.

Thus an assignment is critical iff it does not violate the properties of the linear ordering (recall that we associate variable x_{ij} 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 x_{ij} is unassigned by α. Then for any ϵ ∈ {0,1}, α can be extended to a critical assignment α′ with |Supp(α′)| ≤ |Supp(α)| + 2 such that α′(x_{ij}) = ϵ.

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 i_{1},i_{2},i_{3} are distinct elements from [n] \ Supp(α). Then α can be extended to a total assignment for X so that all axioms of the original principle GT_{n} except the axiom ¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}} 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] \ {i_{1},i_{2},i_{3}}, then set i_{1} ≻ i_{2} ≻ i_{3} ≻ i_{1} and make i_{1},i_{2},i_{3} greater than the rest of the vertices.

Lemma 3.9. For n sufficiently large, there exists a restriction ρ such that for every S and x_{ij}, where S is a subset of [n] of size at most n/100 and x_{ij} is a variable underlying GT′_{n,ρ}, there exist three distinct elements i_{1},i_{2},i_{3} ∈ [n] \ S such that ρ(i_{1},i_{2},i_{3}) = x_{ij}.

Proof. Fix a set S, |S| ≤ ϵn, ϵ = 1/100, and fix some x_{ij}. Choose ρ uniformly at random from all functions mapping T to X. Then the probablity that ρ is bad for (S,x_{ij}) is

( \frac{n(n − 1) − 1}{n(n − 1)} ) ^{\binom{n−ϵn}{3}} ≤ ( 1 − \frac{1}{n^{2}}) ^{(n−ϵn)^{3}/12} = ( 1 − \frac{1}{n^{2}}) ^{n^{3}(1−ϵ)^{3}/12} ≤ e^{−n(1−ϵ)^{3}/12} .

Thus the probability that a given ρ is bad for all (S,x_{ij}) is at most

n(n − 1) · \binom{n}{ϵn} · e^{−n(1−ϵ)^{3}/12} ≤ n^{2}· e^{H(ϵ)n}· e^{−n(1−ϵ)^{3}/12} = n^{2}· e^{(H(ϵ)−(1−ϵ)^{3}/12)n} ≤ n^{2}· e^{−.0248n} .

The first inequality follows from the fact that \binom{n}{ϵn} ≤ e^{H(ϵ)n} where H(x) = −xlnx − (1 − x)ln(1 − x) is 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 GT′_{n,ρ} has size greater than 2^{n/200}.

Proof. Fix a good ρ such that the above lemma holds. Let R be a regular resolution refutation of GT′_{n,ρ}. 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 x_{ij} 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 x_{ij} 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 x_{ij} leads to the vertex ν_{k_{0}} and 1 to ν_{k_{1}}. We extend the existing path up to both ν_{k_{0}} and ν_{k_{1}}. For each ϵ ∈ {0,1} we extend α_{ν_{k}} by Lemma 3.7 to an arbitrary partial critical assignment α_{ν_{kϵ}} such that α_{ν_{kϵ}}(x_{ij}) = ϵ 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 2^{n/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 x_{ij} is queried in ν_{1}. The key observation is that x_{ij} is forgotten in ν_{2} (because the clause in ν_{2} cannot contain both literals x_{ij} and ¬x_{ij}). By Lemma 3.9 we can choose three vertices i_{1},i_{2},i_{3} ∉ Supp(α_{ν_{2}}) such that ρ(i_{1},i_{2},i_{3}) = x_{i,j}. Now let us set by Lemma 3.8 the rest of variables so that all axioms of GT′_{n,ρ} except A_{0} = ¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}} ∨ x_{ij} or A_{1} = ¬x_{i_{1}i_{2}} ∨ ¬x_{i_{2}i_{3}} ∨ ¬x_{i_{3}i_{1}} ∨ ¬x_{ij} 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 x_{ij}. The contradiction with Lemma 2.3 proves the Theorem.

The same procedure can be applied to the set of clauses MGT_{n} [5] that results from GT_{n} if we replace all wide clauses with equivalent 3-CNF’s, thus yielding a bounded width separation between regular and general resolution.

We note that the above lower bound could have been made for an explicit ρ, rather than a random ρ. For example, we could define ρ(x_{1},x_{2},x_{3}) by n(i_{1}+ i_{2}) + i_{1}+ i_{3} (mod \binom{n}{2}). However, for simplicity of presentation, we chose to use a random ρ. Note that the above argument actually shows that GT′_{n,ρ} 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 P_{i,j}, i ∈ (V \ U) and j ∈ S, and R_{j}, j ∈ S. The variable P_{i,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 P_{i,j} an edge variable, and a variable R_{j} a stone variable. For a vertex i ∈ V, and a stone t ∈ S, let D_{i,t} be 1 if i ∈ U, otherwise, D_{i,t} is the formula (P_{i,t}∧ R_{t}). The clauses are as follows. For clarity, some clauses are expressed in implicational form.

(i) ⋁ {P_{i,j} | j ∈ S}, i ∈ V \ U. These clauses express the fact that every vertex contains some stone (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, (P_{k,j} → R_{j}).

(iii) For the sink vertex s and stone j, (P_{s,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, (D_{i,t}∧ D_{j,u} ∧ P_{k,v}→ R_{v}). 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.

We write Stone(G,S) for the special case of the stone formulas where U = ∅. 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(m^{3}n).

Lemma 4.1. For all m and all directed acyclic graphs G, Stone(G,S) has a resolution refutation of size O(m^{3}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 (¬P_{i,t}∨ ¬P_{j,u} ∨ ¬P_{k,v}∨ R_{v}) for t,u,v ∈ S, by resolving clauses of type (ii) against appropriate induction clauses. There are m^{3} such clauses, and each can be derived in two steps, so this part of the proof takes O(m^{3}) steps. Next, we derive all clauses of the form (¬P_{j,u} ∨ ¬P_{k,v}∨ R_{v}), by resolving the previously obtained clauses against clauses of type (i). There are m^{2} such clauses, each of which takes m steps to obtain, so this part of the proof also takes O(m^{3}) steps. We then repeat this pattern to derive all clauses of the form (¬P_{kv}∨ R_{v}), in O(m^{2}) steps, completing the induction step.

Finally, when the sink s is colored red, we can derive the empty clause from R_{s} and ¬R_{s} in O(m) steps. The entire refutation takes O(m^{3}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 C_{0},C_{1},...,C_{ℓ} of configurations, with C_{0} = ∅ and v ∈ C_{ℓ}, in which each configuration C_{i+1} follows from C_{i} by one of the following rules:

1. Any vertex u ∈ U ∪ Sources(G) can be added to C_{i}, i. e. C_{i+1} = C_{i}∪ {u}.

2. A vertex u can be added to C_{i} to get C_{i+1} = C_{i}∪ {u}, if all immediate predecessors of u are in C_{i}.

3. Vertices can be removed, so that C_{i+1} ⊂ C_{i}.

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,∅).

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/logn.

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 C_{0},...,C_{l} = {i} of G[i] from U ∩G[i] and a legal pebbling D_{0},...,D_{m}of G from U ∪ {i} each of complexity at most p − 1. Then

C_{0},...,C_{l},D_{1}∪ {i},...,D_{m}∪ {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 C_{0},...,C_{ℓ} be a legal pebbling of the sink s from U, and D_{0},...,D_{ℓ} the sequence obtained by setting D_{i} = (C_{i}\ J), where J is the set of unimportant vertices in the pebbling. We argue by induction, proceeding backwards from D_{ℓ} to D_{0}, 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 C_{i+1} is obtained from C_{i} by an appropriate rule. Let us suppose that C_{i+1} was obtained from C_{i} 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 D_{i+1} from D_{i} 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.

An Exponential Separation between Regular and General Resolution

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) vertices 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 ρ = ⟨μ,κ⟩ 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:

• σ(P_{i,j}) = 1 if ⟨i,j⟩ ∈ μ, σ(P_{i,j}) = 0 if i or j are in Dom(μ) ∪ Ran(μ), but ⟨i,j⟩ ∉ μ;

• σ(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 P_{i,j} = 0, for all i ∈ V.

Thus ρ is a restriction on the decorated graph, and σ is a corresponding restriction on the propositional 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(κ) = ∅, and furthermore, the parameters r and s are equal. In this case, we shall describe ρ = ⟨μ,κ⟩ as an rrestriction. 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).

Theory of Computing, Volume 3 (2007), pp. 81–102 91

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 ρ = ⟨μ,κ⟩ 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 ρ = ⟨μ,κ⟩ 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 μ′from Dom(χ) to S \ Dom(κ), and then set the colors of stones in the range of μ′by setting κ′(μ(i)) = χ(i) for all i ∈ Dom(χ) = Dom(μ′). Then ρ′= ⟨μ′,κ′⟩ is a clamping compatible with χ.

The next lemma follows readily from the definitions.

Lemma 4.12. If ρ = ⟨μ,κ⟩ is a k-based clamping of Stone(G,U,S) with parameters r,s, then

Stone(G,U,S)⌈ρ = Stone(G[k],U′,S′) ,

where U′= G[k] ∩ (U ∪ Dom(μ)) and S′= S \ Dom(κ).

Lemma 4.13. Let ρ = ⟨μ,κ⟩ be an r-restriction for (G,S), where G has pebbling number N, and |S| ≥ |V |. Then there is a vertex k ∈ G and ρ′= ⟨μ,κ′⟩ so that:

1. ρ′= ⟨μ,κ′⟩ is a k-based clamping of (G,S), with κ ⊆ κ′;

2. (G[k],U) has pebbling number at least N − r, where U = G[k] ∩ Dom(μ).

Proof. We construct ρ′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 k′∈ G, and a new coloring χ′, and we make these choices in such a way as to maximize the pebbling number of the decorated graph (G[k′],G[k′] ∩ U(k′,χ′)), where U(k′,χ′) is the set of vertices in G[k′] mapped to R by χ′.

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

p_{1} = Peb(G[k],U ∪ {i})  and  p_{2} = Peb(G[i],U ∩ G[i]) .

If p_{1} ≥ p_{2}, then set k′= k and extend χ by setting χ′(i) = R and χ′(i′) = R for all i′that are unimportant in (G[k],U ∪ {i}). If p_{1} < p_{2} then set k′= i, choose a path in G from i to k, and extend χ to an i-based coloring, χ′, of (G,U ∩G[i]). Letting U′= U(k′,χ′), by Lemma 4.5, Peb(G[k′],U′) ≥ 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 ρ′= ⟨μ,κ′⟩ 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 ¬P_{i,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 P_{i} of at least d stones, such that all literals P_{i,j}, i ∈ W, j ∈ P_{i} are present in C.

There are three parameters in our lower bound, γ, δ, and ϵ. The lower bound is of the form 2^{δn/(logn)^{3}}; the parameter associated with a complex clause is ϵn/logn and the size of the restriction is γn/logn.

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), |S| = 3n, of size at most s = 2^{δn/(logn)^{3}}. Then there exists an r-restriction ρ, r = γn/logn, such that R⌈ρ has no (ϵn/logn)-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.

The total number of pairs in V × S to choose from is 3n^{2}; each complex clause of the third type can be forced to true by choosing a P_{i,j} from (ϵn/logn)^{2} pairs; each complex clause of the second type can be forced to true by choosing a P_{i,j} from (ϵ(3n − 1)n)/logn ≥ (ϵn/logn)^{2} pairs. Thus, by averaging, there exists a P_{i,j} such that at least s(ϵn/logn)^{2}/3n^{2} ≥ s(ϵ^{2}/3(logn)^{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

\frac{logs}{log( 1/(1 − \frac{ϵ^{2}}{3(logn)^{2}}))} ≤ \frac{δn/(logn)^{3}}{ϵ^{2}/3(logn)^{2}} ≤ \frac{3δn}{ϵ^{2}logn} ≤ \frac{γn}{logn} .

Now for the clauses of the first type, notice that there are 3n − γn/logn ≥ 2n stones left that are untouched by the matching chosen above, and any complex clause of the first type still contains (ϵ − γ)n/logn ≥ ϵn/2logn 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/2logn distinct stone variables that have not been set by the restriction already chosen. Each of these is thus set to one by ϵn/2logn out of at least 4n choices of stone literals.

By averaging, there must be one stone literal that forces s(ϵ/8logn) of the complex clauses of type one to true. Thus to force all complex clauses of this type to true we need to set

\frac{logs}{log( 1 /(1 − \frac{ϵ}{8logn}))} ≤ \frac{δn/(logn)^{3}}{ϵ /8logn} ≤ \frac{8δn}{ϵ(logn)^{2}} ≤ \frac{γn}{logn}

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/logn) ,

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 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 k′, a new k′-based coloring χ′and a new restriction ρ′ compatible with χ′. 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 ρ(P_{i,j}) = 1, then extend ρ by coloring j red or blue arbitrarily. Set k′= k, χ′= χ.

• If a stone variable R_{j} is queried at ν, and it is already placed on a vertex i, i. e. ρ(P_{i,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 k′= k and χ′= χ.

– 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 χ′(i) = R, and set k′= k.

– Otherwise, answer to maximize the pebbling number of the associated decorated graph. That is, compare the two values

p_{1} = Peb(G_{ν},U_{ν} ∪ {i})  and  p_{2} = Peb(G_{ν}[i],U_{ν} ∩ G[i]) .

If p_{1} ≥ p_{2}, then set k′= k, extend χ by setting χ′(i) = R and χ′(i′) = R for all i′that are unimportant in (G_{ν},U_{ν} ∪ {i}), and set ρ(R_{j}) = 1. If p_{1} < p_{2} 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 P_{i,j} is queried at ν, but the assignment, σ, defined by ρ is not defined at P_{i,j}, then set ρ(P_{i,j}) = 1 Otherwise, answer consistent with σ, the assignment defined by ρ. Set k′= k and χ′= χ.

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_{ξ}).

Claim 5.5. The clause C_{ξ} attached to the node ξ must be N/16 complex.

Let ρ = ⟨μ,κ⟩ 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 corresponding 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′⊂ 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/16complex. 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′⊂ F be this set of at least N/8 forgotten free stones. Now we claim that for every i ∈ I′and t ∈ F′, the literal P_{i,t} must occur in C_{ξ}, and thus C_{ξ} is an N/8-complex clause of type three.

Suppose that the literal P_{i,t} does not occur in C_{ξ} for some i ∈ I′, t ∈ F′. Then we can modify the restriction ρ to ρ′by mapping i to t, and if ρ(i) = u, where u ≠ t, then we assign a color to u, if it was not colored already. Because i ∈ I′, we know that for all j ¬P_{i,j} does not occur in C_{ξ}), and thus it follows that ρ′(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 ρ′, in which σ(P_{i,t}) = 1 and σ(C_{ξ}) = 0. The only initial clause falsified by σ is an induction clause associated with i, containing the variable R_{t}. However, by Corollary 2.4, C_{ξ} was inferred from clauses none of which contain the forgotten variable R_{t}. This is a contradiction, so it follows that C_{ξ} must contain the variables P_{i,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 ¬P_{i,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 P_{i,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 B′⊂ B and A′⊂ A each of size exactly N/16 such that ρ defines a mapping from B′to A′but the mapping is forgotten; the color of each stone in A′is forgotten, and for every i ∈ B′, at most N/2 zero-edges out of i are remembered at ξ. We claim that for every i ∈ I′− B′and t ∈ A′, the literal P_{i,t} must occur in C_{ξ}.

Suppose that this is not the case and let P_{i,t} be some literal that does not occur in C_{ξ}, where i ∈ I′, t ∈ A′and let i′∈ B′be the vertex that is mapped to t by ρ. Then we will modify the restriction ρ to obtain ρ′as follows. First, ρ′will map i to t. Secondly, ρ′will map i′to some unqueried stone t′such that the edge from i′to t′has not already been remembered to be 0. Further, the color associated with t′ 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 ρ′. It will still be the case that ρ′(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 ρ′to an i-critical coloring, σ, extending the restriction ρ′. Since the only initial clause falsified by σ contains the variable R_{t}, and R_{t} is not remembered, we have reached a contradiction, and thus C_{ξ} must contain all such variables P_{i,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/logn). Then any regular resolution refutation of Stone(G,S), where |S| = 3n requires size 2^{Ω(n/(logn)^{3})}.

Proof. We start with a pointed graph G with n vertices and pebbling number Peb(G) ≥ βn/logn, 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 size at most S = 2^{δn/(logn)^{3}}. By Lemma 5.2 (the Restriction Lemma), there is a restriction ρ of size r = γn/logn, such that R⌈ρ has no (ϵn/logn)-complex clauses.

By Lemma 4.13, there is a vertex k ∈ G and ρ′= ⟨μ,κ′⟩ so that ρ′is a k-based clamping of (G,S), with κ ⊆ κ′, 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 R⌈ρ must contain a (βn/32logn)-complex clause, contradicting the conclusion of the previous paragraph.

6 Open problems

The present paper gives a separation between regular and general resolution that seems close to optimal. 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 PHP_{n} 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.

A proof (or disproof) of this conjecture would shed light on the question of exactly when the regularity 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 PHP_{n} – the proof in question is in fact regular.

Conjecture 6.2. Let PHP_{n} 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 PHP_{n} is n(n + 3)2^{n−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 backtracking 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 unrestricted 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, Philipp Hertel, and Toniann Pitassi: The complexity of resolution with caching. 2006. Unpublished manuscript. 6

[2] * Paul Beame, Henry Kautz, and Ashish Sabharwal: Towards understanding and harnessing the potential of clause learning. Journal of Artifical Intelligence Research, 22:319–351, 2004. 6

[3] * Paul Beame and Toniann Pitassi: 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] * Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson: Near-optimal separation of tree-like and general resolution. ECCC TR00-005, 2000. [ECCC:TR00-005]. 1, 4.1

[5] * M. Bonet and N. Galesi: 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 [6] * Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen: 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] * Joshua Buresh-Oppenheim, Matthew Clegg, Russell Impagliazzo, and Toniann Pitassi: Homogenization and the polynomial calculus. In Proc. 27th International Colloquium on Automata, Languages and Programming, pp. 926–937. Springer, 2000. [ICALP:fvxybba423y153b8]. 4.1

[8] * James Celoni, Wolfgang Paul, and Robert Tarjan: Space bounds for a game on graphs. Mathematical Systems Theory, 10:239–251, 1977. [Springer:u32u2r202jv33611]. 4.3

[9] * Stephen A. Cook: 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] * Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 6:169–184, 1979. 1

[11] * Martin Davis, George Logemann, and Donald Loveland: A machine program for theorem proving. Communications of the Association for Computing Machinery, 5:394–397, 1962. [ACM:10.1145/368273.368557]. 1

[12] * Niklas Een and Niklas 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] * Andreas Goerdt: Davis-Putnam resolution versus unrestricted resolution. Annals of Mathematics and Artificial Intelligence, 6:169–184, 1992. [Springer:k008110v05867897]. 1

[14] * Andreas Goerdt: Regular resolution versus unrestricted resolution. SIAM Journal of Computing, 22:661–683, 1993. [SICOMP:10.1137/0222044]. 1

[15] * Armin Haken: The intractability of resolution. Theoretical Computer Science, 39:297–308, 1985. [TCS:10.1016/0304-3975(85)90144-6]. 6.2

[16] * Wenqi Huang and Xiangdong Yu: A DNF without regular shortest consensus path. SIAM Journal on Computing, 16:836–840, 1987. [SICOMP:10.1137/0216054]. 1

[17] * Jan Krajíček: Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press, 1995. 2

[18] * Balakrishnan Krishnamurthy: Short proofs for tricky formulas. Acta Informatica, 22:253–274, 1985. [ActaInf:mp65776636126242]. 3, 3

[19] * Matthew Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik: Chaff: Engineering an efficient SAT solver. In Proc. 38th Design Automation Conference, pp. 530–535. ACM Press, 2001. [ACM:10.1145/378239.379017]. 6 [20] * Alexander Nadel: Backtrack search algorithms for propositional logic satisfiability: Review

and innovations. Master’s thesis, Hebrew University, 2002. 6

[21] * Ran Raz and Pierre McKenzie: Separation of the monotone NC hierarchy. Combinatorica, 19:403–435, 1999. Preliminary Version in: Proc. 38th FOCS, 1997. [Springer:h4prxbwxpn1c8xqh]. 4.1

[22] * Gunnar Stålmarck: Short resolution proofs for a sequence of tricky formulas. Acta Informatica, 33:277–280, 1996. [ActaInf:lhrhe2glkmgflbu1]. 3

[23] * G. S. Tseitin: On the complexity of derivation in propositional calculus. In A. O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125. Consultants Bureau, New York, 1970. 1, 6

[24] * Alasdair Urquhart: 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 ABOUT THE AUTHORS

Mikhail (Misha) Alekhnovich 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 Automatizability. 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 papers 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 Johannsen 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.

Toniann Pitassi studied chemistry and computer science as an undergraduate at Pennsylvania 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.

Alasdair Urquhart 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 University 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.