% ToC v003/a005 (ToC#265), 
% by A. Alekhnovich, J. Johannsen, T. Pitassi, A. Urquhart
%
% acr May 1, 2pm EST: Incorporated Laci's changes, implemented a box
%                     around Michael Alekhnovich's name in author list.
% acr April 16 8am EST: Second ToC editorial pass.

\documentclass{toc}

\tocdetails{%
	volume=3, number=5, year=2007, firstpage=81,
	received={August 15, 2006},
	published={May 1, 2007}
}

\runningauthor{M.~Alekhnovich, J.~Johannsen, T.~Pitassi,
  and A.~Urquhart}

\runningtitle{An Exponential Separation between Regular and General Resolution}

\copyrightauthor{Michael Alekhnovich and Jan Johannsen and Toniann
  Pitassi and Alasdair Urquhart}

\bibliographystyle{tocplain}
\newcommand\st{~\,|\,~}
\def\matcal#1{{\cal #1}}

\newcommand\Hajos{Haj\'{o}s\ }
\newcommand\Pudlak{Pudl\'{a}k\ }
\newcommand\Krajicek{Kraj\'{\i}\v{c}ek\ }
\newcommand\Chvatal{Chv\'{a}tal}
\newcommand\Szemeredi{Szemer\'{e}di}
\newcommand\Turan{Tur\'{a}n }


\DeclareMathOperator{\Supp}{Supp}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                             %
%%% |\/\/\/|                                                    %
%%% |      |                                                    %
%%% |      |                                                    %
%%% | (o)(o)                                                    %
%%% C      _)                                                   %
%%% | ,___|  ----     REVISION HISTORY                          %
%%% |    /                                                      %
%%%      \                                                      %
%%% ______\_                                                    %
%%%%%%%%%%% Original version from August 3 2001.                %
%%%%%%%%%%% Journal version:  AU started work October 26 2004;  %
%%%%%%%%%%% AU abandons work November 29 2004.                  %
%%%%%%%%%%% July 8 2006:  Toni informs Alasdair that she is     % 
%%%%%%%%%%% "on a mission" to get out the journal version.      %
%%%%%%%%%%% Alasdair starts work again July 8 2006.             %
%%%%%%%%%%% Errors introduced in Section 4.2 by AU corrected by %
%%%%%%%%%%% rolling back to previous version of Section 4.2     %
%%%%%%%%%%% In spite of serious efforts, Alasdair was unable to %
%%%%%%%%%%% understand the last two sentences in Misha's proof  %
%%%%%%%%%%% of Lemma 3.9.  After an abortive attempt to patch   %
%%%%%%%%%%% up the Lemma to accord with his own dim ideas,      %
%%%%%%%%%%% Alasdair rolled back the version to Misha's original%
%%%%%%%%%%% The only change in Section 3 is that Alasdair       %
%%%%%%%%%%% added some explanatory notes to Definition 3.3, in  %
%%%%%%%%%%% response to the remarks of Allen van Gelder.        %
%%%%%%%%%%% Alasdair passed on the torch to Toni July 13 2006   %
%%%%%%%%%%% a few days after Italy won the World Cup.           %
%%%%%%%%%%%                 TO BE CONTINUED ...                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frontmatter}[classification=text]

\title{An Exponential Separation between Regular and General Resolution}
% Dedicated to the memory of Misha Alekhnovich
\tocpdftitle{An Exponential Separation between Regular and General
  Resolution}
\tocpdfauthor{Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart}

\author[Misha]{\framebox{Michael Alekhnovich}}
\author[Jan]{Jan Johannsen\thanks{ Supported by the DFG Emmy
          Noether-Programme grant No.\ Jo 291/2-1.}}
\author[Toniann]{Toniann Pitassi\thanks{Supported by NSERC.}}
\author[Alasdair]{Alasdair Urquhart\thanks{Supported by NSERC.}}

\begin{dedication}
% \centering
\begin{flushright}
 Dedicated to the memory of Misha Alekhnovich
\end{flushright}
% This article is a dedicated to Michael Alekhnovich.
\end{dedication}

\begin{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.
\end{abstract}

\tockeywords{resolution, proof complexity, lower bounds}
\tocams{03F20, 68Q17}
\tocacm{F.2.2, F.2.3}

\end{frontmatter}

\section{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. 

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~\cite{cr79} that the existence of ``strong'' systems
in which all tautologies have proofs of polynomial size is tightly
connected to the \textrm{NP} vs. \textrm{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~\cite{g92,goe93,bonestgaljoh00,benimpwig00}
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~\cite{ts70},
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~\cite{dll62}
(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~\cite[p.\ 436]{urq95}.

The main result of Tseitin's paper~\cite{ts70} 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:
\begin{quotation}
\noindent
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 \subseteq B$, then $A$ may be considered to be the stronger 
assertion of the two);
if the derivation of a disjunction containing a variable $\xi$ 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 $\xi$.
\end{quotation}

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~\cite{goe93} 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.

The first example of a contradictory CNF formula whose shortest
resolution refutation is irregular was given by  Wenqi Huang
and Xiangdong Yu~\cite{huang87}.
Andreas Goerdt~\cite{goe93} 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 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
combinatorial interpretation, and
the corresponding lower bound technique may be useful
for other applications. 

The paper is organized in the following way. \expref{Section}{pre}
contains definitions necessary for both examples. We give
these examples independently in Sections~\ref{first}, \ref{secpre},
and~\ref{seclower}.


\section{Preliminaries}\label{pre}

A \emph{literal} is a propositional variable $x$ or its negation $\lnot
x$.  A \emph{clause} is a set of literals.  The \emph{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 \lor
x$ and $D \lor \lnot x$ also satisfies $C \lor D$.  The clause $C \lor D$ is said
to be a \emph{resolvent} of the clauses $C \lor x$ and $D \lor \lnot x$ derived
by \emph{resolving on} the variable $x$.  A \emph{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 \emph{refutation} of $F$ if $C$ is the empty clause
$\Lambda$.  The \emph{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 \lor x$ and $D \lor \lnot x$
are labeled with the literals $x$ and $\lnot x$ respectively.  It is well
known that resolution is a \emph{sound} and \emph{complete}
propositional proof system, \ie, a formula $F$ is unsatisfiable if
and only if there is a resolution refutation for $F$.

A resolution refutation is \emph{regular} if on any path from $\Lambda$ 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 \emph{assignment} for a formula $F$ (sometimes we call it also a
\emph{restriction}) is a Boolean assignment to some of the variables
in the formula; the assignment is \emph{total} if all the variables in
the formula are assigned values.  If $C$ is a clause, and $\sigma$ an
assignment, then we write $C \lceil \sigma$ for the result of applying the
assignment to $C$, that is, $C \lceil \sigma = 1$ if $\sigma(l) = 1$ for some literal
$l$ in $C$, otherwise, $C \lceil \sigma$ is the result of removing all literals
set to 0 by $\sigma$ from $C$ (with the convention that the empty clause is
identified with the Boolean value 0).  If $F$ is a CNF formula, then
$F \lceil \sigma$ is the conjunction of all the clauses $C \lceil \sigma$, $C$ a clause in
$F$.


If $R = C_1, \ldots, C_k$ is a resolution derivation from a formula $F$,
and $\sigma$ an assignment to the variables in $F$, then we write $R \lceil \sigma$
for the sequence $C_1 \lceil \sigma, \ldots, C_k \lceil \sigma$.

\begin{lemma}
\label{proofrestrictionlemma}
If $R$ is a regular resolution derivation of $C$ from a formula $F$,
and $\sigma$ an assignment, then there is a subsequence of $R \lceil \sigma$ that is
a regular resolution derivation of a subclause of $C \lceil \sigma$ from $F \lceil
\sigma$.
\end{lemma}

\begin{proof}
This is a straightforward induction on the length of the derivation
from $F$.
\end{proof}

Every regular resolution refutation can be represented by a read-once
branching program~\cite{kraj95}.  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 $\nu$ in the refutation is labeled with a clause $C \lor D$
derived from clauses $C \lor x$ and $D \lor \lnot x$, then we say that the
variable $x$ is \emph{queried} at $\nu$.  If we extend the path to the
node labeled with $C \lor x$, then we say that we have answered the query
with ``$x$,'' while in the other case, we have answered with ``$\lnot
x$.''  Thus every path $\pi$ 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 \emph{forgotten} variables:

\begin{definition}
For every node $\nu$ in a regular refutation labeled
with a clause $C$, we say that a variable is 
\emph{forgotten at $\nu$} if it does not occur in $C$, 
but is queried on some path from the root to $\nu$.
\end{definition}

The intuition behind this definition is given by the following
lemma.

\begin{lemma}\label{forgotten}
If the variable $x$ is forgotten at a node $\nu$ in
a regular refutation, then no axiom 
reachable from $\nu$ can contain $x$. In particular,
the clause labeling $\nu$ must be inferred from initial
clauses that do not contain $x$.
\end{lemma}
\begin{proof}
If $x$ is forgotten at $\nu$, but there is an axiom reachable
from $\nu$ containing $x$, then $x$ must have been removed
by resolution by some inference on the path from $\nu$ to this
axiom.  
However, this contradicts the regularity restriction.
\end{proof}

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 $\nu$ with a forgotten variable $x$ and show that 
all initial clauses free of $x$
do not imply the clause $C_\nu$ even semantically; to show this
we produce an assignment $\sigma$ that falsifies only clauses
containing $x$, while $C_\nu\lceil \sigma = 0.$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%% First example %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\renewcommand{\mod}{\mbox{\rm mod}}
\section{First example: $GT_{n,\rho}'$ formulas}
\label{first}

Our first example is based on the ordering principle first considered
by Krishnamurthy~\cite{krish85}.
\allowdisplaybreaks

\begin{definition}\label{gt}
Let $X$ be the set of variables $x_{ij}$ for $i,j\in [n],$ $i\not =j$.
The contradiction $GT_n$ consists of the following axioms:
\begin{align*}
  &x_{ij} \leftrightarrow \lnot x_{ji} & &1\leq i< j\leq n\enspace, \\
  &\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1} & &\text{for any distinct
  } i_1,i_2,i_3\in [n]\enspace,\\
  &\bigvee_{k\in [n] \, , \, k\neq j} x_{k j} & &j\in [n]\enspace.
\end{align*}
\end{definition}

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}\land x_{i_2 i_3}\to x_{i_1 i_3}$
(that is to say, $(\lnot x_{i_1 i_2} \lor \lnot x_{i_2 i_3} \lor x_{i_1 i_3})$).  It
is more convenient for us to write these axioms in the symmetric form
$\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}$; these representations
are equivalent in the presence of the axioms $x_{ij} \leftrightarrow \lnot x_{ji}$.
Note that there are exactly two such transitivity axioms for any set
of three distinct elements $ i_1,i_2,i_3\in [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 \succ j$. The first
two groups of axioms assure that $\succ$ is a total linear ordering on the
set $[n]$. The principle $GT_n$ claims that any such ordering never
has a maximum.  Krishnamurthy~\cite{krish85} conjectured that $GT_n$
requires superpolynomial-size resolution refutations.  This conjecture
was refuted by Gunnar St\r{a}lmarck, who proved the following result.


\begin{theorem}
\label{GTnupperbound}
There exist regular resolution refutations of $GT_n$ of size $O(n^3)$.
\end{theorem}
\begin{proof}
The paper of St\r{a}lmarck~\cite{stalmarck96}
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\r{a}lmarck's refutation is in fact regular.
\end{proof}

This contradiction was later used by Bonet
and Galesi~\cite{bg99} to show the optimality of the size-width
relationship.
By a slight modification of St\r{a}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\lor x_C$, $C\lor \lnot x_C.$ The variable $x_C$ should
be chosen in a certain precise way to simplify our lower bound.

\begin{definition}\label{gtprime}
Let $X$ be the set of variables $x_{ij}$ $i,j\in [n],$ $i\not =j$;
the cardinality of $X$ is $n(n-1)$.  
Let $T$ be the set of all triples $(i,j,k)$, $i \neq j \neq k$,
$i,j,k \in [n]$. The cardinality of $T$ is clearly $\binom{n}{3}$.
Let us fix a function $\rho$ from $T$ to $X$.

The set of clauses $GT_{n,\rho}'$ consists of the following axioms:
\begin{align*}
  &x_{i j} \leftrightarrow \lnot x_{j i} & &1\leq i< j\leq n\enspace, \\
  &\bigvee_{k\in [n]\, , \, k\neq j} x_{k j} & &j\in [n]\enspace, \\
  &\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}
\lor \rho(i_1,i_2,i_3)  & &\text{for } (\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}) \in GT_n\enspace, \\[0.3em]
&\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}
\lor \lnot \rho(i_1,i_2,i_3)  & &\text{for } (\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}) \in GT_n \enspace.
\end{align*}
\end{definition}

%Thus $GT_{n,\rho}'$ is defined up to an arbitrary enumeration of the set $X$. 
For each transitivity axiom in the original set $GT_n$ involving
vertices $i_1, i_2, i_3$, the set of clauses $GT_{n,\rho}'$
contains exactly two axioms produced by adding a new literal $ \rho(i_1,i_2,i_3) $
or its negation $ \lnot \rho (i_1,i_2,i_3) $.
In the definition above, the condition 
``for  $(\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}) \in 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
$\{ \lnot x_{i_1 i_2},  \lnot x_{i_2 i_3},  \lnot x_{i_3 i_1} \}$
as an ordered disjunction.

\begin{corollary}
For any $\rho$, there is a refutation of $GT_{n,\rho}'$ in general resolution
of size $O(n^3)$.
\end{corollary}
\begin{proof}
It is easy to see that the principle $GT_n$ can be inferred 
from $GT_{n,\rho}'$ in general resolution in $O(n^3)$ steps.
Hence, the Corollary follows by \expref{Theorem}{GTnupperbound}.
\end{proof}

The refutation of the preceding corollary is irregular.
By contrast, the main theorem of this section shows that for certain $\rho$,
any regular refutation of $GT_{n,\rho}'$ has exponential size.
Before proving this lower bound, we require some definitions
and lemmas.

\begin{definition}
For an assignment $\alpha$ on  $X$
let $\Supp(\alpha)$ be the set of all $i\in [n]$ such 
that $\alpha$ assigns a value to either $x_{ij}$ or $x_{ji}$
for some $j$.
\end{definition}

Recall the notion of \emph{critical assignment} for $GT_n$~\cite{bg99}.
We generalize it to the case of \emph{partial} critical assignments:

\begin{definition}
For a subset of vertices $S\subset [n]$ a \emph{partial critical assignment}
for $S$ is an arbitrary assignment $\alpha$
that gives values to all variables $x_{ij}$, $i,j\in S$
and for any clause $C$ of the original principle $GT_n$, 
$C\lceil \alpha\not \equiv 0.$
\end{definition}

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\succ j$).
Hence partial critical assignments $\alpha$ are in one-to-one
correspondence with all linear orderings on the set $\Supp(\alpha)$.
This semantical interpretation is essential 
and we will use it throughout the proof.

\begin{lemma}\label{extend}
Assume that $\alpha$  is a critical partial assignment with 
$|\Supp(\alpha)|<n-2$ and the variable $x_{ij}$ is unassigned
by $\alpha$. Then for any $\epsilon\in\{0,1\}$, 
$\alpha$ can be extended to 
a critical assignment $\alpha'$ 
with $|\Supp(\alpha')|\leq |\Supp(\alpha)|+2$
such that $\alpha'(x_{ij})=\epsilon$. 
\end{lemma}
\begin{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\prec j$ as well as $i\succ j$ and extend
our ordering in the correct way.
\end{proof}

\begin{lemma}\label{extend2}
Assume that $\alpha$  is a critical partial assignment with 
$|\Supp(\alpha)| < n-2$ and $i_1,i_2,i_3$ are distinct
elements from $[n]\setminus \Supp(\alpha).$
Then $\alpha$ can be extended to a total assignment for $X$ so that
all axioms of the original principle $GT_n$ 
except the axiom 
$\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}$
are satisfied.
\end{lemma}
\begin{proof}
We need to extend the linear ordering on $\Supp(\alpha)$
to some total (contradictory) ordering on $[n]$. For that
we extend $\alpha$ to some arbitrary partial critical
assignment on $[n]\setminus \{i_1,i_2,i_3\}$,
then set $i_1\succ i_2\succ i_3\succ i_1$ and make $i_1,i_2, i_3$
greater than the rest of the vertices. 
\end{proof}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%NEW STATEMENT OF LEMMA
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{lemma}\label{sum}
For $n$ sufficiently large, there exists a 
restriction $\rho$ 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,\rho}'$,
there exist three distinct elements
$i_1,i_2,i_3\in [n]\setminus S$ such 
that $\rho(i_1,i_2,i_3) = x_{ij}$. 
\end{lemma}

\begin{proof}
  Fix a set $S$, $|S| \leq \epsilon n$, $\epsilon=1/100$, and fix some $x_{ij}$.
  Choose $\rho$ uniformly at random from all functions mapping $T$ to
  $X$.  Then the probablity that $\rho$ is bad for $(S,x_{ij})$ is
\[
{ \left( \frac {{n (n-1)}-1} {{n (n-1)}}  \right) }^{{\binom{n - \epsilon n}{3}}} \leq \left( 1-\frac{1}{n^2} \right) ^{(n-\epsilon n)^3/12} =
\left( 1-\frac{1}{n^2} \right) ^{n^3 (1-\epsilon)^3 /12} \leq  e^{-n (1-\epsilon)^3/12}\enspace.
\]
Thus the probability that a given $\rho$ is bad
for all $(S, x_{ij})$ is at most
\[ n (n-1) \cdot \binom{n}{\epsilon n} \cdot e^{- n (1-\epsilon)^3 /12}  \leq  n^2 \cdot e^{H(\epsilon)n} \cdot
	e^{-n(1-\epsilon)^3 /12} =  n^2 \cdot e^{(H(\epsilon) - (1-\epsilon)^3/12)n}  \leq  n^2 \cdot e^{-.0248n}\enspace.
\]
The first inequality  follows from the fact that
$\binom{n}{\epsilon n} \leq e^{H(\epsilon)n}$ where
$H(x)= -x \ln x - (1-x) \ln (1-x)$ is the entropy function.
The last inequality follows by choosing $\epsilon=1/100$.
The above quantity is clearly less than $1$ for $n$ sufficiently large,
and thus there exists a $\rho$ satisfying the conditions of the lemma.
\end{proof}


\begin{theorem}\label{lower1}
For $n$ sufficiently large, there exists $\rho$
such that any regular resolution refutation of $GT_{n,\rho}'$ has size greater than
$2^{n/200}$.
\end{theorem}

\begin{proof}
Fix a good $\rho$ such that the above lemma holds.
Let $R$ be a regular resolution refutation of $GT_{n,\rho}'$.
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 $\nu$ along these paths
we define an auxiliary critical assignment $\alpha_\nu$
that falsifies the clause in $\nu$.

Initially we start with a single path at the root and 
$\alpha$ is empty. Now assume that we have defined $l$ distinct paths 
up to the nodes $\nu_1, \ldots ,\nu_l$. For each node $\nu_k$ 
with $|\Supp(\alpha_{\nu_k})|<n/100$ we 
extend the corresponding path in the following way:

\begin{itemize}
\item If a variable $x_{ij}$ is queried at $\nu_k$ and
its value is already defined by $\alpha$ then we extend our
path according to this value; $\alpha$ does not change.

\item 
If a variable $x_{ij}$ is queried at $\nu_k$ and
 either $i$ or $j$ does not belong to $\Supp(\alpha_{\nu_k})$
then $\nu_k$ is a \emph{branching node} and we proceed in the following way.
Assume that the answer $0$ to $x_{ij}$ leads
to the vertex $\nu_{k_0}$ and $1$ to $\nu_{k_1}$.
We extend the existing path up to
both $\nu_{k_0}$ and $\nu_{k_1}$.
For each $\epsilon\in\{0,1\}$ 
we extend $\alpha_{\nu_k}$ by \expref{Lemma}{extend} 
to an arbitrary partial critical assignment
$\alpha_{\nu_{k_\epsilon}}$ such that 
$\alpha_{\nu_{k_\epsilon}}(x_{ij})=\epsilon$ and 
$|\Supp(\alpha_{\nu_{k_\epsilon}})|\leq |\Supp(\alpha_{\nu_k})|+2$.
\end{itemize}

We use this strategy to extend paths till every path leads to a node
with $|\Supp(\alpha)|\geq n/100$. Since the value of $|\Supp(\alpha)|$
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 $\nu_1$ and then merge again in the node $\nu_2$. Assume
that the variable $x_{ij}$ is queried in $\nu_1$. The key observation
is that $x_{ij}$ is forgotten in $\nu_2$ (because the clause in
$\nu_2$ cannot contain both literals $x_{ij}$ and $\lnot x_{ij}$).
%Choose any $r$ such that $i=i(r)$ and $j=j(r)$ (see
%Definition~\ref{gtprime}).
By \expref{Lemma}{sum} we can choose three
vertices $i_1,i_2,i_3\not \in \Supp(\alpha_{\nu_2})$ such that
$\rho(i_1,i_2,i_3) = x_{i,j}$.
%n(i_1+i_2)+i_1+i_3 = r\ (\mod\ n^2)$. 
Now let us set by
\expref{Lemma}{extend2} the rest of variables so that all axioms of
$GT_{n,\rho}'$ except $A_0=\lnot x_{i_1 i_2}\lor \lnot x_{i_2 i_3}\lor \lnot
x_{i_3 i_1}\lor x_{i j}$ or $A_1=\lnot x_{i_1 i_2}\lor \lnot x_{i_2
  i_3}\lor \lnot x_{i_3 i_1}\lor \lnot x_{i j}$ are satisfied. We
produce a total assignment that falsifies the clause $C_{\nu_2}$
labeling $\nu_2$ (because it is an extension of $\alpha_{\nu_2}$) and
all violated clauses contain the forgotten $x_{ij}$.  The
contradiction with \expref{Lemma}{forgotten} proves the Theorem.
\end{proof}

The same 
procedure can be applied to the set of clauses $MGT_n$~\cite{bg99}
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. 

%Namely, the set $MGT_n$ as defined by Bonet and Galesi \cite{bg99}
%contains, instead of the clauses $\bigvee_{k=1, k\not =j}^n x_{k,j}$,
%the following axioms over the auxiliary variables $y_{0,j}, \ldots
%,y_{n,j}$:
%$$\lnot y_{0,j}\land \bigwedge_{i=1,i\not=j}^n(y_{i-1,j}\lor x_{i,j}
%\lor\lnot y_{i,j})\land y_{n,j}\; .$$
%
%
%Let us substitute $0$ for all $y_{0,j}$ so that 
%in all we have a set  $Y$ of $n^2$ auxiliary variables. 
%Now we replace each axiom 
%$C=\lnot x_{i_1,i_2}\lor \lnot x_{i_2 i_3}\lor \lnot x_{i_3 i_1}$
%with a clause
%%$C\lor x_r^{\epsilon_1}\lor y_r^{\epsilon_2},$ where 
%%$r=n(i_1+i_2)+i_1+i_3\ (\mod\ n^2)$.
%$C \lor (\rho(x_{i_1},x_{i_2},x_{i_3}))^{\epsilon_1} \lor (\rho(y_{i_1},y_{i_2},y_{i_3}))^{\epsilon_2}$.
%Obviously the resulting principle $MGT_n'$ has a polynomial-size
%refutation in resolution, and its hardness 
%for regular resolution can be shown 
%essentially in the same way as in the proof of Theorem~\ref{lower1}.


We note that the above lower bound could have been made for
an explicit $\rho$, rather than a random $\rho$.
For example, we could define $\rho(x_1,x_2,x_3)$ by
$n(i_1 + i_2) + i_1 + i_3 \pmod{\binom{n}{2}} $.
However, for simplicity of presentation, we chose to use a random $\rho$.
Note that the above argument actually shows that $GT_{n,\rho}'$
is hard for almost all $\rho$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%  The Stone Formulas!!  8-) %%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Second example: the stone formulas}
\label{secpre}

\subsection{Definitions}
\label{stoneformuladefinitions}

Our second example will be a generalization of the implication graph
formulas, first introduced by Raz and McKenzie~\cite{razmck99}, and
also used in subsequent papers~\cite{benimpwig00,bonestgaljoh00,burcleimppit00}. 
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 \emph{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\geq 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,'' $\mathit{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 \geq n$ stones.  Let $\mathrm{Sources}(G)$ be
the source vertices of $G$.  The variables of the formula are
$P_{i,j}$, $i \in (V \setminus U)$ and $j \in S$, and $R_j$, $j \in
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 $\lnot R_j$ says ``Stone $j$ is colored blue.''
We call a variable $P_{i,j}$ an \emph{edge variable}, and a variable
$R_j$ a \emph{stone variable}.  For a vertex $i \in V$, and a stone $t
\in S$, let $D_{i,t}$ be $1$ if $i \in U$, otherwise, $D_{i,t}$ is the
formula $(P_{i,t} \land R_t)$.  The clauses are as follows.
For clarity, some clauses are expressed in implicational form.

\begin{itemize}
\item[(i)] 
        $\bigvee \{ P_{i,j} \mid j \in S \}$, $i \in V \setminus 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).
\item[(ii)] 
        For all vertices $k \in \mathrm{Sources}(G) \setminus U$ and
        stones $j$, $(P_{k,j} \to R_j)$.
\item[(iii)] 
        For the sink vertex $s$ and stone $j$, $(P_{s,j} \to \lnot R_j)$.
\item[(iv)] 
        For all vertices $i$, $j$, $k$ such that $(i,k)$ and $(j,k)$ are
        edges in $G$, where $k \in V \setminus U$,
        and for all stones $t,u,v$, 
        $(D_{i,t} \land D_{j,u} \land P_{k,v} \to 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$.
\end{itemize}

We write $\mathit{Stone}(G,S)$ for the special case
of the stone formulas where $U = \emptyset$.
It is not hard to check that the number of
variables in $\mathit{Stone}(G,S)$ is $(n+1)m$,
and the number of clauses in the formula is
$O(m^3 n)$.

\begin{lemma}
\label{upperboundlemma}
For all $m$ and all directed acyclic graphs $G$,
$\mathit{Stone}(G,S)$ has a resolution refutation of size $O(m^3 n)$.
\end{lemma}

\begin{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 
$(\lnot P_{i,t}  \lor \lnot P_{j,u} \lor \lnot P_{k,v} \lor R_{v} )$
for $t,u,v \in 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 
$(\lnot P_{j,u} \lor \lnot P_{k,v} \lor 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 $(\lnot P_{kv} \lor 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 $\lnot R_s$ in $O(m)$ steps.
The entire refutation takes $O(m^3 n)$ steps.
\end{proof}

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.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  ALL YOU WANTED TO KNOW ABOUT GRAPH PEBBLINGS  %%%%%%%%%%%%%%%%%%%%%%
%%%  (BUT WERE AFRAID TO ASK)  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{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.

\begin{definition} \label{defpeb}
Let $(G,U)$ be a decorated graph.
A configuration is a subset of $V$.
A \emph{pebbling} of a vertex $v$ from $U$ in $G$ is a sequence 
$C_0 , C_1 , \ldots  , C_\ell$ of configurations, with $C_0 = \emptyset$ and 
$v \in C_\ell$, in which each configuration $C_{i+1}$ follows
from $C_i$ by one of the following rules:
\begin{enumerate}
\item 
  Any vertex $u \in U \cup \mathrm{Sources}(G)$ can be added to $C_i$, 
  \ie\ $C_{i+1} = C_i \cup \{ u \}$.
\item 
  A vertex $u$ can be added to $C_i$ to get $C_{i+1} = C_i
  \cup \{ u \}$, if all immediate predecessors of $u$ are in $C_i$. 
\item
  Vertices can be removed, so that $C_{i+1} \subset C_i$.
\end{enumerate}
The \emph{complexity} of a   pebbling of $v$ from $U$ is the maximal
size of any configuration in the sequence.
The \emph{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 \emph{pebbling number} $Peb(G)$ of a pointed graph is
the pebbling number of the decorated graph $(G,\emptyset)$.
\end{definition}

Pointed graphs requiring large pebbling number were constructed in a paper 
by Celoni, Paul and Tarjan, based on a construction
of Valiant.

\begin{lemma}[Celoni, Paul and Tarjan~\cite{cpt77}]
\label{pebblinglemma}
There is a constant $\beta>0$ such that for all sufficiently large $n$,
there is a pointed graph $G$ with $n$ vertices that has pebbling
number $Peb(G) \geq \beta n / \log n$.   
\end{lemma}

The following definition is useful in describing the effect
of restrictions on stone formulas.
\begin{definition}
\label{inducedsubgraphdefinition}
  For a pointed graph $G=(V,E)$ and $v\in V$, let $G[v]$ denote the induced
  subgraph of $G$ on those vertices $u$ from which $v$ is reachable,
  \ie\ there is a directed path from $u$ to $v$.
\end{definition}


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.

\begin{lemma}
\label{pebblingfact}
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 \cup \{i\})$ or $(G[i], U
\cap G[i])$ has pebbling number at least $p$.
\end{lemma}

\begin{proof}
  Assume that both $(G, U \cup \{i\})$ and $(G[i], U \cap G[i])$ have pebbling
  number at most $p-1$.  Then there is a legal pebbling $C_0, \ldots , C_l
  = \{ i \}$ of $G[i]$ from $U \cap G[i]$ and a legal pebbling $D_0, \ldots ,
  D_m$ of $G$ from $U \cup \{ i \}$ each of complexity at most $p-1$.  Then
  \[
  C_0, \ldots , C_l, D_1 \cup \{i\}, \ldots , D_m \cup \{ 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$.
\end{proof}

The next definition picks out a type of vertex that plays a central
role in the restrictions described in the following subsection.

\begin{definition}
\label{importantnodedefinition}
Let $(G,U)$ be a decorated graph. A vertex $v \in G$ is
\emph{important} if there is a path from $v$ to $s$ not
containing any vertex in $U$, otherwise $v$ is \emph{unimportant}.
\end{definition}

\begin{lemma}
\label{importantnodelemma}
If $Peb(G,U) = p$,
then there exist at least $p-2$ important vertices in $G$.
\end{lemma}

\begin{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, \ldots , C_\ell$ be a legal pebbling of the sink $s$ from $U$,
and $D_0, \ldots, D_\ell$ the sequence obtained by setting
$D_i = (C_i \setminus J)$, where $J$ is the set of unimportant vertices
in the pebbling.
We argue by induction, proceeding backwards from $D_\ell$ 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 \expref{Definition}{defpeb}, 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 \expref{Definition}{defpeb}, followed by an application of 
Rule 2, followed by a deletion of the one or two vertices added
when applying Rule 1.
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  HOME IMPROVEMENT:  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  ON COLORING AND CLAMPING  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\subsection{Critical assignments for stone formulas}

\begin{sloppypar}
In the remainder of the paper, we concentrate on certain special assignments
for the formulas $\mathit{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.
\end{sloppypar}

\begin{definition}
\label{restrictiondefinition}
Let $G = (V,E)$ be a pointed graph, and $S$ a set of stones,
where $|S| \geq |V|$.
A \emph{restriction} $\rho = \langle \mu, \kappa \rangle$ 
for $(G,S)$ is determined by 
\begin{enumerate}
\item
A bijective map $\mu$ from a subset of $V$ to $S$;
\item
A coloring $\kappa$ assigning a subset of $S$ to the set $\{ R,B \}$
(\ie, we assign the colors red and blue to 
some of the stones).
\end{enumerate}
The \emph{assignment $\sigma$ determined by $\rho$} is defined by setting:
\begin{itemize}
\item $\sigma(P_{i,j}) = 1$ if $\langle i,j \rangle \in \mu$,
  $\sigma(P_{i,j}) = 0$ if $i$ or $j$ are in $\text{Dom}(\mu) \cup
  \text{Ran}(\mu)$, but $\langle i,j \rangle \not\in \mu$;
\item
$\sigma(R_j) = 1$ if $\kappa(j) = R$, 
$\sigma(R_j) = 0$ if $\kappa(j) = B$;
\item 
If $j$ is in the domain of $\kappa$, but not in the range
of $\mu$, then $P_{i,j} = 0$, for all $i \in V$.
\end{itemize}

Thus $\rho$ is a restriction on the decorated graph, and $\sigma$
is a corresponding restriction on the propositional formula.
If $|\mu| = r$ and $|\kappa| = s$, then we say that $\sigma$ is a
restriction with \emph{parameters} $r$ and $s$.  
To simplify
notation, we shall identify a restriction with the assignment that it
determines.
\end{definition}

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, 
$\text{Ran}(\mu) \cap \text{Dom}(\kappa) = \emptyset$,
and furthermore, the parameters $r$ and $s$ are equal.
In this case, we shall describe $\rho = \langle \mu, \kappa \rangle$
as an \emph{$r$-restriction}.
The second special type of restriction is one in which \emph{all}
of the stones placed on vertices are assigned colors,
that is, $\text{Ran}(\mu) \subseteq \text{Dom}(\kappa)$.
This second type of restriction we call a \emph{clamping}.

\begin{definition}
  Let $(G,U)$ be a decorated graph, $k$ a vertex in $G$, and $\chi$
  a partial coloring of $G$, that is, $\chi$ is a map from a subset
  of $V$ to $\{R, B\}$.  We say that $\chi$ is a \emph{$k$-based
    coloring} of $(G,U)$ if the following conditions hold:
\begin{enumerate}
\item
If $i \in U$, then $\chi(i) = R$;
\item
There is a path $\pi$ in $G$ from $k$ to the sink of $G$ so
that the vertices in the path are exactly those to which
$\chi$ assigns the color blue;
\item
If a vertex $i$ is not in $G[k] \cup \pi$, then $\chi(i) = R$.
\end{enumerate}
We say that $\chi$ is \emph{$k$-critical} if it is a total
coloring of $G$.
\end{definition}

\begin{lemma}
\label{existenceofcriticalcoloringslemma}
If $(G,U)$ is a decorated graph and 
$k$ an important vertex of $G$,
then there is a $k$-critical coloring of $(G,U)$.
\end{lemma}

\begin{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)$.
\end{proof}


If $\chi$ is a coloring of a decorated graph
$(G,U)$, then a clamping $ \rho = \langle \mu, \kappa \rangle$
is said to be \emph{compatible}
with $\chi$ if $\text{Dom}(\chi) = \text{Dom}(\mu)$, and
for any vertex in $\text{Dom}(\chi) = \text{Dom}(\mu)$, 
$\kappa(\mu(i)) = \chi(i)$.
If $\chi$ is a $k$-based coloring, then we say that $\rho$ is a 
\emph{$k$-based} clamping, and that it is 
\emph{$k$-critical} if it
is compatible with a $k$-critical coloring.
The reader can easily check that if $\rho$ is a $k$-critical clamping
of $(G,U)$, then it forces all the clauses
in $\mathit{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 $\chi$ if it can be extended to a clamping compatible with $\chi$.

The next two lemmas, which are straightforward to prove, are used repeatedly
in the rest of the proof.

\begin{lemma}
\label{compatibilitylemma}
Let $(G,U)$ be a decorated graph, and $\chi$ a partial coloring
of $G = (V,E)$.
In addition, let $S$ be a set of stones with 
$|S \setminus \text{Dom}(\kappa)| \geq |V|$, and
$\rho = \langle \mu, \kappa \rangle$ a restriction for 
$(G,S)$ so that $\text{Dom}(\mu) \subseteq \text{Dom}(\chi)$, and
$\kappa(\mu(i)) = \chi(i)$, whenever
$i \in \text{Dom}(\mu) \cap \text{Dom}(\chi)$ and
$\kappa(\mu(i))$ is defined.
Then $\rho$ is compatible with $\chi$.
\end{lemma}

\begin{proof}
Extend $\mu$ to a bijection $\mu'$ from $\text{Dom}(\chi)$
to $S \setminus \text{Dom}(\kappa)$, and then set the colors of
stones in the range of $\mu'$ by setting $\kappa'(\mu(i)) = \chi(i)$
for all $i \in \text{Dom}(\chi) = \text{Dom}(\mu')$.
Then $\rho' = \langle \mu', \kappa' \rangle$ is a clamping
compatible with $\chi$.
\end{proof}

The next lemma follows readily from the definitions.

\begin{lemma}
\label{clampinglemma}
If  $\rho = \langle \mu, \kappa \rangle$ is a $k$-based clamping of 
$\mathit{Stone}(G,U,S)$ with parameters $r,s$, 
then 
\[
\mathit{Stone}(G,U,S) \lceil \rho = \mathit{Stone}(G[k],U',S')\enspace,
\]
where 
$U' = G[k] \cap (U \cup \text{Dom}(\mu))$ and 
$S' = S \setminus \text{Dom}(\kappa)$.
\end{lemma}


\begin{lemma}
\label{clampingextensionlemma}
Let $ \rho = \langle \mu, \kappa \rangle$ 
be an $r$-restriction for $(G,S)$, where $G$ has
pebbling number $N$, and $|S| \geq |V|$.
Then there is a vertex $k \in G$ and 
$\rho' = \langle \mu, \kappa' \rangle$ so that:
\begin{enumerate}
\item
$\rho'= \langle \mu, \kappa' \rangle$ is a $k$-based clamping of $(G, S)$, 
with $\kappa \subseteq \kappa'$;
\item
$(G[k], U)$ has pebbling number at least $N - r$,
where $U = G[k] \cap \text{Dom}(\mu)$.
\end{enumerate}
\end{lemma}

\begin{proof}
We construct $\rho'$ by first constructing an appropriate $k$-based
coloring $\chi$ of $G$, with $\text{Dom}(\chi) = \text{Dom}(\mu)$, 
and then using \expref{Lemma}{compatibilitylemma} to 
find the required $k$-based clamping.
At each stage in the construction, we are given a designated vertex $k \in G$,
and a $k$-based coloring $\chi$ 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' \in G$, 
and a new coloring $\chi'$,
and we make these choices in such a way as to 
maximize the pebbling number of the decorated graph 
$(G[k'], G[k'] \cap U(k', \chi'))$, where $U(k', \chi')$ is the 
set of vertices in $G[k']$ mapped to $R$ by $\chi'$.

To be more precise, let us suppose that we have $\mu(i) = t$,
and that the stone $t$ has not yet been assigned a color.
Let $U = U(k, \chi)$.
Compare the two values
   \[ p_1 = Peb(G[k],U \cup\{i\}) \qquad \text{ and } \qquad 
      p_2 = Peb(G[i], U \cap G[i]) \enspace . \] 
   If $p_1 \geq p_2$, then set $k' = k$ and extend
   $\chi$ by setting $\chi'(i) = R$ and $\chi'(i') =
   R$ for all $i'$ that are unimportant in $(G[k],U \cup\{i\})$.
   If $p_1 < p_2$ then set $k' = i$, choose a path in
   $G$ from $i$ to $k$, and extend $\chi$ to an $i$-based
   coloring, $\chi'$, of $(G, U \cap G[i])$.
   Letting $U'=U(k',\chi')$, by \expref{Lemma}{pebblingfact},
   $Peb(G[k'],U') \geq Peb(G[k],U)-1$.
   
   Let $k$ and $\chi$ be the designated vertex and $k$-based
   coloring produced at the end of this process, that is, when
   $\text{Dom}(\chi) = \text{Dom}(\mu)$.  By \expref{Lemma}{compatibilitylemma}, $\rho$ is compatible with $\chi$, so
   that there is a a $k$-based clamping $\rho' = \langle \mu, \kappa'
   \rangle$ compatible with $\chi$.  By definition,
   $U(k,\chi) = G[k] \cap Dom(\mu)$, and since the construction has
   $r$ steps, $(G[k], G[k] \cap \text{Dom}(\mu))$ has pebbling number at 
   least $N -r$.
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  THE STONE LOWER BOUND!! 8-)       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{The lower bound for stone formulas}\label{seclower}

The general structure of the proof of the lower bound is similar to
that of Beame and Pitassi's~\cite{beapit96b} 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.


\begin{definition}
\label{complexclausedefinition}
A clause $C$ is called \emph{$d$-complex} 
if one of the following holds:
\begin{enumerate}
\item $C$ contains at least $d$ distinct stone variables, or
\item There is a matching of size at least $d$ from vertices to stones
  such that $C$ contains the negative edge literals $\lnot P_{i,j}$ for
  each pair $(i,j)$ in the matching.
\item There is a subset $W$ of at least $d$ vertices, 
  such that for all $i \in W$ there is a subset 
  $P_i$ of at least $d$ stones, such that all literals $P_{i,j}$,
  $i \in W$, $j \in P_i$ are present in $C$.
\end{enumerate}
\end{definition}


There are three parameters in our lower bound,
$\gamma$, $\delta$, and $\epsilon$.
The lower bound is of the form $2^{\delta n / (\log n)^3}$;
the parameter associated with a complex clause is 
$\epsilon n / \log n$ and the size of the restriction
is $\gamma n / \log n$.

\begin{lemma}
[Restriction Lemma]
\label{restrictionlemma}
  Let $\gamma$, $\delta$, $\epsilon$ be constants such that
  $0 < \gamma, \delta, \epsilon < 1$ and
  $3 \delta / \epsilon^2 \leq \gamma \leq
  \epsilon / 2$. Let $G=(V,E)$ be a pointed graph with $|V|=n$, and 
  let $R$ be a resolution refutation of
   $\mathit{Stone}(G,S)$, $|S| = 3n$, 
   of size at most $s=2^{\delta n / (\log n)^3}$.  
  Then there exists an $r$-restriction $\rho$, 
  $r = \gamma n / \log n$, such that $R \lceil \rho$ has
  no $(\epsilon n / \log n)$-complex clauses.
\end{lemma}

\begin{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 \times 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 $(\epsilon n / \log n)^2$
pairs; each complex clause of the second type can
be forced to true by choosing a $P_{i,j}$ from 
$(\epsilon(3n-1)n) / \log n \geq (\epsilon n / \log n)^2$ pairs. 
Thus, by averaging, there exists a $P_{i,j}$ such that at least
$s(\epsilon n / \log n)^2 /3n^2 \geq s(\epsilon^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
\begin{equation*}
  \frac{\log s}
       {\log \left( 1 / \bigl( 1-\frac{\epsilon^2}{3 (\log n)^2}
           \bigr) \right) }  
        \leq
  \frac{\delta n \, / \, (\log n)^3 } { \epsilon^2 \, / \, 3 (\log n)^2 }
        \leq 
  \frac{3\delta n}{\epsilon^2 \log n} 
        \leq 
  \frac{\gamma n}{\log n} \enspace . 
\end{equation*}

Now for the clauses of the first type, notice that there are $3n -
\gamma n/\log n \geq 2n$ stones left that are untouched by the
matching chosen above, and any complex clause of the first type still
contains $(\epsilon - \gamma) n / \log n \geq \epsilon n / 2 \log n$
literals corresponding to these stones, since $\gamma \leq
\epsilon/2$.

Since the refutation has size at most $s$,
there are at most $s$ clauses of the first type, each containing
$\epsilon 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 $\epsilon n / 2\log n$ out
of at least $4n$ choices of stone literals.

By averaging, there must be one stone literal that forces 
$s(\epsilon / 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
\[ \frac{\log s}{\log \left( 1 \: / \, \bigl( 1-\frac{\epsilon}{8 \log
          n} \bigr) \right) } \leq \frac{\delta n \, / \, (\log n)^3
      }{ \epsilon \, / \, 8 \log n } \leq \frac{8 \delta n}{\epsilon
      (\log n)^2} \leq \frac{\gamma n}{\log n}  \]
stone literals.
\end{proof} 


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.


\begin{lemma}[Complex Clause Lemma]
\label{complexclauselemma}
Let $(G,U)$ be a decorated graph with
\[
Peb(G,U) = N = \Omega(n/\log n)\enspace,
\]
where $G$ has $n$ vertices.  Then for $|S| = m = 2n$, and $n$
sufficiently large, any regular resolution refutation of
$\mathit{Stone}(G,U,S)$ contains an $(N/16)$-complex clause.
\end{lemma}

\begin{proof}
Let $R$ be a regular resolution refutation of
$\mathit{Stone}(G,U,S)$.
We will follow a particular path $\pi$ 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 \emph{designated vertex} $k$
in $G$, second, we define a $k$-based coloring $\chi$ of $G$, third,
we define a restriction $\rho$ compatible with $\chi$.
The answers given along the path at each stage are compatible with
the partial assignment, $\sigma$, determined by $\rho$.
%That is to say, if the literal $l$ occurs as a label
%on the path, then $\rho(l) = 0$.
At each stage, the designated node $k$ and the coloring $\chi$
determine the subgraph $G[k]$ of $G$, together with a subset
$U$ of $G[k]$, consisting of the vertices $i$ of $G[k]$ 
with $\chi(i) = R$.

Initially, we start the path at the root of the refutation. The designated vertex is
the sink $s$  of $G$, $\chi(u) = R$ for $u \in U$, and 
$\chi(s) = B$.
Now assume that we have defined the path up to a node $\nu$, together
with a designated vertex $k$, a $k$-based coloring $\chi$, 
and a restriction $\rho$ compatible with $\chi$.
In addition, let $(G_\nu, U_\nu)$ be the 
decorated graph $(G[k], U)$, where $U$ is the set of vertices in $G[k]$
colored red by $\chi$.
We want to extend the path by providing an appropriate answer to the variable
queried at the node $\nu$; we need also to define a new
designated vertex $k'$, a new $k'$-based coloring $\chi'$
and a new restriction $\rho'$ compatible with $\chi'$.
In each case, the answers to the queries will be given as an extension
of the current restriction $\rho$ -- unless the current restriction
answers the query already, as can happen in the last case below.

\begin{itemize}
\item If a stone variable $R_j$ is queried at $\nu$ 
  and it is not currently placed on a vertex, \ie\ for no vertex
  $i$ do we have $\rho(P_{i,j})=1$, then 
  extend $\rho$ by coloring $j$ red or blue arbitrarily.
  Set $k'= k$, $\chi' = \chi$.
\item If a stone variable $R_j$ is queried at $\nu$, and it is already placed
  on a vertex $i$, \ie\ $\rho(P_{i,j})=1$, 
  then we answer as follows:
  \begin{itemize}
  \item If $i$ is colored by $\chi$ then
   answer accordingly. That is, if $\chi(i)=R$, then set $\rho(R_j)=1$,  
    and if $\chi(i)=B$, then set $\rho(R_j)=0$. 
    Then set $k' = k$ and $\chi' = \chi$. 
  \item  If $i$ is not assigned a color by $\chi$, but
         is not important with respect to
      $(G_\nu,U_\nu)$, then set $\rho(R_j) = 1$. Extend $\chi$ by
      setting $\chi'(i)=R$, and set $k' = k$.
  \item Otherwise, answer to maximize the pebbling number of the
    associated decorated graph.
   That is, compare the two values
   \[ p_1 = Peb(G_{\nu},U_\nu\cup\{i\}) \qquad \text{ and } \qquad 
      p_2 = Peb(G_{\nu}[i], U_\nu \cap G[i]) \enspace . \] 
   If $p_1 \geq p_2$, then set $k' = k$, extend
   $\chi$ by setting $\chi'(i) = R$ and $\chi'(i') =
   R$ for all $i'$ that are unimportant in $(G_\nu,U_{\nu}\cup\{
   i\})$, and set $\rho(R_j) = 1$.

   If $p_1 < p_2$ then set $G_{\xi} = G_\nu[i]$, choose a path in
   $G_\nu$ from $i$ to $k$, extend $\chi$ to an $i$-based
   coloring of $G$, and set $\rho(R_j) = 0$.
   \end{itemize} 
\item If an edge $P_{i,j}$ is queried at $\nu$, but 
    the assignment, $\sigma$, defined by $\rho$ is not defined at $P_{i,j}$,
     then set $\rho(P_{i,j})=1$
     Otherwise, answer consistent with $\sigma$, the assignment defined by $\rho$.
     Set $k' = k$ and $\chi' = \chi$.
\end{itemize}

\begin{claim}
There is a node on the path defined above where exactly $N/2$
stones are queried.
\end{claim}

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_\nu,U_\nu)
= N$, by \expref{Lemma}{pebblingfact} 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 $\xi$ on the path where
exactly $N/2$ stones are queried.

The pair $(G_\xi,U_\xi)$ associated with $\xi$
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 \expref{Lemma}{importantnodelemma}, there are at least 
$N/2 - 2$ important vertices in $(G_\xi, U_\xi)$.

\begin{claim}
The clause $C_\xi$ attached to the node $\xi$
must be $N/16$ complex.  
\end{claim}

Let $\rho = \langle \mu, \kappa \rangle$ be the restriction associated with $\xi$.
Let $I$ be the set of important vertices in
$(G_\xi, U_\xi)$.  If at least $N/8$ of the vertices in $I$ are
mapped by $\mu$ and the mapping is remembered, \ie, the corresponding
edge variables set to 1 by $\rho$ occur negated in $C_\xi$, then
$C_\xi$ 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'
\subset I$ of at least $N/8$ vertices that are either unmapped by
$\mu$ or are mapped by $\mu$ 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 $\xi$
into the {\it free} stones, $F$,
and the {\it attached} stones, $A$.
$F$ consists of those stones queried along the path to $\xi$
that are not in the range of $\mu$;
$A$ are those stones queried on the path to $\xi$ that are
in the range of $\mu$.
There are two general cases to consider. The first case
(which is slightly easier) is when $|F| \geq N/4$
and the second case is when $|A| \geq N/4$.

Assume first that $|F| \geq N/4$.
We will show that the clause $C_\xi$ attached to the node $\xi$
must be $N/16$-complex. The first subcase is when at least
$N/8$ of the stones in $F$ occur in $C_\xi$. In this case,
$C_\xi$ 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 $\xi$.
Let $F' \subset F$ be this set of at least $N/8$ forgotten free stones.
Now we claim that for every $i \in I'$ and
$t \in F'$, the literal $P_{i,t}$ must occur in
$C_\xi$, and thus $C_\xi$ is an $N/8$-complex clause of type three.

Suppose that the literal $P_{i,t}$ does not occur in $C_\xi$ for some $i\in I'$,
$t\in F'$. Then we can modify the restriction
$\rho$ to $\rho '$ by mapping $i$ to $t$,
and if $\rho(i) = u$, where $u \neq t$, then we assign a color
to $u$, if it was not colored already.
Because $i \in I'$, we know that for all $j$
$\lnot P_{i,j}$ does not occur in $C_\xi$), and
thus it follows that $\rho '(C_\xi) =0$. Since $i$ is important,
there is an $i$-based coloring extending the coloring $\chi$
associated with $\xi$, and this $i$-based coloring can be
extended to an $i$-critical coloring.
Let $\sigma$ be an $i$-critical clamping compatible with this coloring,
extending the restriction $\rho '$, in which $\sigma(P_{i,t})=1$
and $\sigma(C_\xi)=0$. The only initial clause falsified by $\sigma$
is an induction clause associated with $i$,
containing the variable $R_t$. However, by Corollary 2.4,
$C_\xi$ was inferred from clauses none of which contain the forgotten
variable $R_t$. This is a contradiction, so it follows
that $C_\xi$ must contain the variables $P_{i,t}$.

We will now argue the second case, when $|A| \geq N/4$.
Let $B$ be the subset of vertices that are mapped by $\rho$
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_\xi$ 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, \ie, the
negative edge literal $\lnot P_{i,j}$ where $j=\mu(i)$ occurs in
$C_\xi$. In this case, $C_\xi$ 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_\xi$ for at least
$N/2$ distinct $j$'s.
In this case, $C_\xi$ is an $N/16$-complex clause of type three.

If none of the subcases 2a, 2b or 2c occur, then
there are sets $B' \subset B$ and $A' \subset A$
each of size exactly $N/16$ such that $\rho$ 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 \in B'$, at most
$N/2$ zero-edges out of $i$ are remembered at $\xi$.
We claim that for every $i \in I'- B'$ and $t \in A'$,
the literal $P_{i,t}$ must occur in $C_\xi$.

Suppose that this is not the case and let $P_{i,t}$
be some literal that does not occur in $C_\xi$, where
$i \in I'$, $t \in A'$ and let $i' \in B'$ be the vertex
that is mapped to $t$ by $\rho$.
Then we will modify the
restriction $\rho$ to obtain $\rho'$ as follows.
First, $\rho '$ will map $i$ to $t$.
Secondly, $\rho '$ 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 $\rho$; that is,
the underlying coloring of the graph will be the same for
$\rho$ and for $\rho '$.
It will still be the case that $\rho '(C_\xi)=0$ since we have
not tampered with any of the literals that are remembered (\ie, that
occur in $C_\xi$.)
Now as in Case 1, we will extend $\rho '$ to an $i$-critical coloring,
$\sigma$,
extending the restriction $\rho '$.
Since the only initial clause falsified by $\sigma$
contains the variable $R_t$, and $R_t$ is not remembered,
we have reached a contradiction, and thus $C_\xi$ 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.
\end{proof}


We are ready to state the main theorem of this section.

\begin{theorem}
\label{maintheorem}
Let $G$ be a pointed graph with $n$
 vertices and pebbling number
$N=\Omega(n/\log n)$.
Then any regular resolution refutation of
$\mathit{Stone}(G,S)$, where $|S| = 3n$ requires
size $2^{\Omega(n / (\log n)^3)}$.
\end{theorem}

\begin{proof}
 We start with a pointed graph $G$ with $n$ vertices and pebbling number
 $Peb(G) \geq \beta n / \log n$, in accordance with \expref{Lemma}{pebblinglemma}.
 Set 
 $\epsilon = \beta/32$, 
 $\gamma = \epsilon/2 = \beta/32$ and 
 $\delta = \epsilon^3/6 = \beta^3/199608$, 
 so that we have
 $3\delta / \epsilon^2 \leq \gamma \leq \epsilon / 2$.
 Now assume that there is a regular resolution refutation $R$ of
 $\mathit{Stone}(G,S)$, with size at most $S=2^{\delta n / (\log n)^3}$.
 By \expref{Lemma}{restrictionlemma} (the Restriction Lemma),
 there is a restriction $\rho$ of 
 size $r = \gamma n / \log n$, such that $R \lceil \rho$ has
 no $(\epsilon n / \log n)$-complex clauses.

 By \expref{Lemma}{clampingextensionlemma}, 
there is a vertex $k \in G$ and 
$\rho' = \langle \mu, \kappa' \rangle$ so that
$\rho'$ is a $k$-based clamping of $(G, S)$, 
with $\kappa \subseteq \kappa'$, and 
$(G[k], G[k] \cap \text{Dom}(\mu))$ has pebbling number at least 
$N - r \geq N/2$.
By \expref{Lemma}{complexclauselemma} (the Complex Clause Lemma), 
the refutation $R \lceil \rho$ must contain a $(\beta n / 32 \log
n)$-complex clause, 
contradicting the conclusion of the previous paragraph.
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Open Problem Section %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{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~\cite{ts70}.
For both of these families of examples, the shortest known resolution
refutations are regular.

\begin{conjecture}
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.
\end{conjecture}

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~\cite{cook76},
who gives the size of the shortest known resolution refutation
of $PHP_n$ -- the proof in question is in fact regular.

\begin{conjecture}
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~\cite{hak85}.
Then the minimum size of a refutation of $PHP_n$ is $n(n+3)2^{n-2}$.
\end{conjecture}

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~\cite{zchaff,minisat,nadel,beame-kautz}.
It is known that clause learning is at least as efficient as
regular resolution~\cite{bhp}, 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.


\section{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. 


\bibliography{a005}

\begin{tocauthors}

\begin{tocinfo}[Misha]
Michael Alekhnovich \tocabout\\
University of California, San Diego
\end{tocinfo}

\begin{tocinfo}[Jan]
Jan Johannsen \tocabout\\
Institut f\"ur Informatik\\
jjohanns\tocat{}informatik\tocdot{}uni-muenchen\tocdot{}de
\end{tocinfo}

\begin{tocinfo}[Toniann]
Toniann Pitassi \tocabout\\
University of Toronto\\
toni\tocat{}cs\tocdot{}toronto\tocdot{}edu
\end{tocinfo}

\begin{tocinfo}[Alasdair]
Alasdair Urquhart \tocabout\\
University of Toronto\\
urquhart\tocat{}cs\tocdot{}toronto\tocdot{}edu
\end{tocinfo}
\end{tocauthors}

%% ToC#265 bio sketches
%% updated by laci at midnight Apr 11/12 EDT;
%% includes SIGACT reference.

\begin{tocaboutauthors}
\begin{tocabout}[Misha]
  \textsc{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 \href{http://www.msu.ru/en/}{Moscow State University},
  where he was awarded Diploma with Honours.  His diploma thesis,
  \emph{Pseudorandom generators in propositional proof complexity},
  was written under the supervision of
  \href{http://www.mi.ras.ru/~razborov/}{Alexander A. Razborov}.  In
  2000, he was a member in the special program on Computational
  Complexity at the \href{http://www.ias.edu/}{Institute for Advanced
    Study}, in Princeton.

\noindent
{}From 2001 to 2003, he was a graduate student in the 
\href{http://math.mit.edu}{Department of Mathematics} 
of the \href{http://www.mit.edu}{Massachusetts Insitute of Technology}.  
His doctoral thesis, written under the
supervision of Madhu Sudan, is entitled 
\emph{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
\href{http://www.math.ias.edu/~avi/}{Avi Wigderson}.
{}From 2005 onwards, he was an assistant professor in 
the \href{http://math.ucsd.edu/}{Department of Mathematics},
\href{http://www.ucsd.edu/}{University of California at San Diego}.

\noindent
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.  

\noindent
His premature death has robbed the theory community of one of 
its brightest young stars.  

\medskip
\noindent
\begin{small} \textsf{This biographical sketch was written by Alasdair Urquhart and
Toniann Pitassi. It is an adaptation of a longer
\href{http://www.mi.ras.ru/~razborov/misha_sigact.pdf}{obituary
by A. Razborov}, appearing in
\href{http://sigact.acm.org/sigactnews/online.html}{
 ACM SIGACT News} 38/1 (March 2007), pp. 70-71.
\href{http:www.math.ias.edu/~misha}{Misha's IAS home page}
will be maintained indefinitely.}
\end{small}
\end{tocabout}

\begin{tocabout}[Jan]
  \textsc{Jan Johannsen} obtained his doctoral degree from the
  \href{http://www.uni-erlangen.org/university/}{University of
    Erlangen} in 1996.  After a two-year postdoc at
  \href{http://www.ucsd.edu}{UCSD} he became an Emmy Noether junior
research group leader at
\href{http://www.en.uni-muenchen.de/index.html}{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.
\end{tocabout}

\begin{tocabout}[Toniann]
  \textsc{Toniann Pitassi} studied chemistry and computer science as
  an undergraduate at \href{http://www.psu.edu}{Pennsylvania State
    University}.  After working for several years at \href{http:www.bell-labs.com/}{Bell
  Laboratories}, she pursued graduate work at the \href{http://www.utoronto.ca/}{University of
  Toronto}, with advisor \href{http://www.cs.toronto.edu/~sacook/}{Stephen Cook}, receiving her \phd\ in 1992.
  After a postdoc position at \href{http:www.ucsd.edu}{UCSD} and faculty positions at the
  \href{http://www.pitt.edu/}{University of Pittsburgh} and the \href{http:www.arizona.edu}{University of Arizona}, she returned
  to Toronto as a faculty member in 2000.
\end{tocabout}

\begin{tocabout}[Alasdair]
  \textsc{Alasdair Urquhart} studied philosophy as an undergraduate in
  Edinburgh, Scotland, then did his undergraduate work at the
  \href{http://www.pitt.edu/}{University of Pittsburgh}, where he
  received a \phd\ in the
  \href{http://www.pitt.edu/~philosop/}{Philosophy Department} under
  the supervision of \href{http://www.pitt.edu/~belnap/}{Nuel D.
    Belnap} in 1973.  Since 1970, he has been a faculty member in the
  \href{http://philosophy.utoronto.ca/}{Philosophy Department} at the
  \href{http://www.utoronto.ca/}{University of Toronto}, where he is
  also cross-appointed in the
  \href{http://www.cs.toronto.edu/dcs/index.html}{Computer Science
    Department}.  His research interests include algebraic logic,
  non-classical logic, history of logic, and the complexity of
  propositional proofs.
\end{tocabout}
\end{tocaboutauthors}

\end{document}