Lower Bounds for the Weak Pigeonhole Principle

Beyond Resolution


Albert Atserias Marı́a Luisa Bonet

Juan Luis Esteban

Departament de Llenguatges i Sistemes Informàtics

Universitat Politècnica de Catalunya
C/Jordi Girona Salgado, 1-3, Edif. C6.
08034 Barcelona - Spain.
Tel: +34 93 401 69 94
Fax: +34 93 401 70 14

atserias,bonet,esteban  @[Link]. 

April 2, 2001

Abstract

We work with an extension of Resolution, called Res(2), that allows clauses with conjunc-
tions of two literals. In this system there are rules to introduce and eliminate such conjunctions.
We prove that the weak pigeonhole principle  
 and random unsatisfiable CNF formulas

require exponential-size proofs in this system. This is the strongest system beyond Resolu-
tion for which such lower bounds are known. As a consequence to the result about the weak
pigeonhole principle, Res(log) is exponentially more powerful than Res(2). Also we prove
that Resolution cannot polynomially simulate Res(2), and that Res(2) does not have feasible
monotone interpolation solving an open problem posed by Krajı́ček.

Supported by the CUR, Generalitat de Catalunya, through grant 1999FI 00532.


 Partially supported by MEC through grant PB98-0937-C04 (FRESCO project) and CICYT TIC 98-0410-C02-01.
 Partially supported by MEC through grant PB98-0937-C04 (FRESCO project)
Partially supported by ALCOM-FT, IST-99-14186.

1
1 Introduction
The pigeonhole principle, 
  , expresses that it is not possible to have a one-to-one mapping

from 
 pigeons to  holes. Since it can be formalized in propositional logic, it is natural to
ask in which propositional proof systems such a principle can be proved in polynomial-size, with
respect to the size of the encoding.
A fair amount of information is known about sizes of proofs of 
  in various proof

systems. Haken [12] proved that this principle requires exponential-size proofs in Resolution.
His proof techniques were later extended and simplified [4, 5]. Also Beame et al. [2] proved
that 
  requires exponential-size proofs in bounded-depth Frege systems. Regarding upper

bounds, Buss [8] gave polynomial-size proofs of 
   in unrestricted Frege systems.

The pigeonhole principle can be formulated in more general terms, allowing the number of
pigeons to be greater than   . We call this principle weak pigeonhole principle, or 
 , when

the number of pigeons  is at least  . This simple principle is central to many mathematical
arguments but quite often, it occurs implicitely only. See the introductions in [14, 16] for a nice 
discussion on this. The proof techniques of Haken where extended in [9] to prove that 
 

requires exponential-size proofs in Resolution. A very intriguing and often studied open problem
is to prove exponential-size lower bounds for Resolution proofs of 
  for any  . As a contrast,

the techniques of [2] for proving lower bounds for the pigeonhole principle in bounded-depth Frege
systems can only prove lower bounds for 
 
, and it is again open whether lower bounds can

be proved when the number of pigeons in greater than   . Regarding upper bounds, it is known
that 
  has quasipolynomial-size proofs in bounded-depth Frege [15, 14].

We work with the proof system !#"$&%(' , proposed by Krajı́ček [13], that can be viewed either as
an extension of Resolution, or as a restriction of bounded-depth Frege. In this system the clauses
do not only contain literals, but can also have conjunctions of two literals. The resolution rule gets
modified to be able to- eliminate a conjunction of two literals from a clause. We prove that 



(and in fact 
 &)*,+ ) requires exponential-size proofs in Res(2). This is, to our knowledge, the

first lower bound proof for the weak pigeonhole principle in a subsystem of bounded-depth Frege
that extends Resolution. We note that the quasipolynomial upper bound for bounded-depth Frege
mentioned above can be carried over in depth-.0/21 LK [14], which is equivalent to !#"-$3%547689' (the
analogue of !"$3%:;' when we allow conjunctions of up to polylog literals). As a consequence of
our lower bound, there is an exponential separation between !"$3%:;' and !"$3%<4,6=89' .
We also consider the complexity of refuting random unsatisfiable > -CNF formulas. Chvátal
and Szemerédi [10] proved them hard to refute in Resolution, and the results were improved by
Beame, Karp, Pitassi and Saks [3]. Combining our techniques with those of [3], we also obtain
an exponential-size lower bound for !"$&%;' -refutations of random unsatisfiable > -CNF formulas
with clause density near the threshold. Again, this is the strongest system beyond Resolution for

1
which such a lower bound is known. This result may be considered as a first step towards proving
random > -CNF formulas hard for bounded-depth Frege.
Our techniques are based on the method of random restrictions. The main technical contribu-
tion of our work consists in proving that a relatively short random restriction kills all large formulas
of a !"$3%:;' -refutation. We note that this task is trivial in the case of Resolution because a large
clause is killed by setting a single literal to one. However, our formulas are disjunctions of con-
junctions of two literals, and this task becomes much more involved. The difficulty is in the fact
that we must keep the restriction short not to trivialize the initial clauses of the refutation. In other
words, we overcome the main difficulty in trying to apply switching-like lemmas to prove lower
bounds for the weak pigeonhole principle or random formulas.
Another important question to ask is whether !"$3%:;' is more powerful than Resolution. Here
we prove that Resolution cannot polynomially simulate !"$ %(' , and therefore !"$3%:;' is superpoly-
nomially more efficient than Resolution. As a corollary, we see that !#"-$3%(' does not have feasible
monotone interpolation, solving this way a conjecture of Krajı́ček [13].
Another motivation for working with the system !#"-$3%(' is to see how useful it can be in au-
tomated theorem proving. Given that it is more efficient than Resolution (at least there is a su-
perpolynomial separation), it might be a good idea to try to find good heuristics to find proofs in
!"$3%:;' to be able to use it as a theorem prover.

2 Definitions and Overview of the Lower Bound Proof

A > -term is a conjunction of up to > literals. A > -disjunction is an (unbounded fan-in) disjunction



of > -terms. If is a > -disjunction, a  -term of is also called a free-literal. The refutation system
!"$3%:>' , defined by Krajı́ček [13], works with > -disjunctions. There are three inference rules in

!"$3%:>' : Weakening, -Introduction, and Cut
  
     
    
     
 
 
    
    
  are > -disjunctions, !"$# are sets of indices such that %&! '(#)%+* > , and the   ’s
where and
 
are literals. As usual, if is a literal, denotes its negation. Observe that !#"-$3% ' coincides with
Resolution with the Weakening rule. The size of a !#"$&%>' -refutation is the number of symbols in
it. Mainly, we will work with !"$&%;' .
As we mentioned in the introduction, our arguments are based on random restrictions. In

,


general terms, what we do is the following. Given an unsatisfiable CNF formula F, and an alleged
-
small !"$3%:;' -refutation of , we apply a random restriction , from a suitable distribution, and
we get a refutation ,.% / % /
of . The distribution on restrictions that we choose will satisfy the
following two properties:

2
 (i)

%/ satisfies certain expansion properties,

(ii) Every  -disjunction in , %/ is short (measured by the number of literals that occur).

The argument will be complete since these two conditions will be shown to be contradictory.
As a contrast with the lower bound arguments for Resolution, the most difficult part of our
proof is showing that property (ii) is satisfied. The conjunctions make this task more involved. In
order to overcome this, we split the restriction into two parts
- - -
 . Then, the main contribution
, %/
is showing that every large clause in  contains many free literals. That allows us show, by a
standard argument, that no large clause remains in   . ,.% / /
For the sake of clarity of exposition, we explain this outline again in the particular case of
the Weak Pigeonhole Principle. Let



' "
% 
' be a bipartite graph on the sets  and 
of cardinality  and  respectively, where    . The - 
  , defined by Ben-Sasson and

Wigderson [5], states that there is no matching of  into  . For every edge %   ' , let   "
be a propositional variable meaning that  is mapped to  . The principle is then formalized as the
conjunction of the following set of clauses:
  "  " / / / "$#&%

% '
"! 

  
         (1)
    
'(  " "
) * ,+-. %/9' "0.
1 2+7/ (2)
 
Here,  %/3' denotes the set of neighbors of 3 in . Observe that if is the complete bipartite

graph 4  , then - 
  coincides with the usual pigeonhole principle 
 . It is easy to see
   
that a lower bound for the size of !"$3%:;' -refutations of - 
  implies the same lower bound

for the size of !#"-$3%(' -refutations of 
  .
 
Ben-Sasson and Wigderson proved that whenever is expanding in a sense defined next, every

Resolution refutation of - 
  must contain a clause with many literals. We observe that this

result is not unique to Resolution and holds in a more general setting. Before we state the precise
result, let us recall the definition of expansion:

Definition 1 [5] Let


' "
% 
' be a bipartite graph where 5
 , and 5
 . For % .% % %
 +76  , the boundary of  , denoted by 89 + , is the set of vertices in  that have exactly one
% %
neighbor in  + ; that is, 8: +
"! )<; 5%/9'>=7 +
$% . We say that is %  ? &@ ' -expanding " " "

if every subset  +-A  of size at most ? is such that 89 + >BC@ D + . % % % %
The proof of the following statement is the same as in [5] for Resolution.

Theorem 1 [5] Let E be a sound refutation system with all rules having fan-in at most two. Then,

" " " 
if is %  ? &@ ' -expanding, every E -refutation of - 
 must contain a formula that involves

at least ?$@:F distinct literals.

3
With these definitions, we are ready to outline the argument of the lower bound proof. In sec-
tion 3.1, we will prove the existence of a bipartite graph

%  ' with 5
3 + and' " % .%
% %
5
 + such that if we remove a small random subset of nodes from  , and the corresponding
 '
" " "
edges, the resulting graph is %:  &? &@ ' -expanding for certain  ,  , ? and @ . Then we will argue
that - 

 ' requires exponential-size !"$3%:;' -refutations as follows. Assume, for contradiction,

  '
that is a small refutation of - 

 ' . We say that a  -disjunction in is large if it contains




at least
?$@:F distinct literals. We apply a random restriction  to the refutation such that for -
every large , either   %/
 contains many free literals, or the total number of literals in  is less  %&/
 -
than . Then we extend  to a new random restriction - -
 that knocks out all those large 
 %/
such that  contains many free literals, ignoring those that are not free. After applying , we -

-
obtain a refutation of % 9' -
  where all  -disjunctions have less than ? @:F literals and % 9'


-
" " "
is %  &? @ ' -expanding. This contradicts Theorem 1.

3 Lower Bound for the Weak Pigeonhole Principle

3.1 Random Graphs and Restrictions

In this section we will prove the existence of a bipartite graph as claimed in Section 2. The

principle - 
  will require exponential size !"$3%:;' -proofs.

 " "
Let %  ' denote the distribution on bipartite graphs on sets  and  of sizes  and 

respectively, with edge probability independently for each edge.

Lemma 1 If

is drawn from %" "' , then
 9"  ;  -F 0"8 %/9'  B
  
  + .
Proof : Fix a vertex   . Then, 0" 8 %/9'"!$#&%(' %"' , so that )  0" 8 %  ' 
 . By Chernoff
bounds, * +,
0"8 %/9'0B  - *.   0/213 and * +20" 8 %/9' * 4-F *.  0/215 . By a union bound,
* 6(72 ;00" 8 %  ' *  F- 0 " 8 %/9' B =4- *   8/213   8/215 * =9  0/,15 , and so
* 6:  <; 4-F;0"8 %/9'" = B <    8/215 . => (of lemma 1)
Lemma 2 Let 
>9 , 
@?BA >#4C' %
'F , D
 F and @
 FFE . Let be drawn from


%" "' . Then,

6  is %" "GD "&@ ' -expanding B $F- .
Proof : Fix  +A  of size ( H *ID  , and   . Then, * J  8: + 
HG % K 'ML   . Let
N
* 6   89 +  . Let O  be the indicator random variable for the event that  C8: + . Then,
% 8: + %
QP 
R O  . Observe that O  and O  ' are independent whenever 
1  + . Hence, % 89 + %S!
#&%(' %" N ' , so that )  % 89 + % 
 N . By Chernoff bound, *  % 89 + % *  N F  *  2T 15 . On the other
hand,  N
8HG % UV  'WL  BXH  % + 'ZY  . Moreover, % + '[Y 
% < '  1\/ approaches  F]
4
for sufficiently large  . Therefore,  N B;H-F
. It follows that  N F B;H @ and   2T 15 *  L /21  .
We conclude that *  % % % + %  * * 6 % 8: + %*  N F *   2T 15 *   L /21  . Finally, we
89 + <@

5

bound the probability that is not % " "GD "&@ ' -expanding by
Y  Y  Y 

   L
2
/ 1  *  L   L  /21
 * %:    /21
 ' L /
L H

L  L 
(3)

Recall that 
?BA > 4(' %

' F- and 
>9 . So     /21
 *     2
  6 $F ? . Hence the
sum in (3) is bounded by P
L   *  . => (of lemma 2)
Let

" "
be a fixed bipartite graph on !  / / / % and !  / / / :% . A restriction (for ) is a
" " " 



" " " "   - 
sequence of pairs
% %/  ' / / / %/ # & # ' ' such that %/  ' % ' , and all  ’s are distinct.
 
We let  # % ' be the set of restrictions of length ? . We define a distribution  # % ' on  # % '
"  " 
 " "
as follows: Let 
!  / // 9% ; for every   !  / / / &? % in increasing order, choose a hole 
 
   
uniformly at random in 
 , choose a pigeon  uniformly at random in  %  ' , and let 

" " " "
!  % . The final restriction is % %  & ' / / / % ,# &$# ' ' .



" "  "     
"- -
We define a distribution  %:  &?' on the set of pairs % 9' with  # % ' : the graph
 " "  - 
is drawn from %  ? ' first, and then is drawn from  # % ' . In other words, if %  ' is a "
fixed pair with .  # %!
' , then

 - 8  "!$#% % '%    "&#%$%' %!

' %   /

J 


#
#

If is a bipartite graph on the vertex sets  " // / "  and  " / / / "  , and - is a restriction
 ! !
% ? %

 "  ' " / //" % " ' ' ( % ' , then % 9- ' denotes the graph that results from deleting  " / // "
 
% %  &  # & #  #  & #

from , and renaming nodes in an order-preserving way. With this definitions we are ready to
prove:

Lemma 3 Let 
>9 ,  
?BA >#4C' %

'F , D
 F and @
-FE . Let %

" -9' be drawn from
 %:  " " "
&?' . Then, * + % -9' is %"  "GD "&@ ' -expandingB $ F- .
 be the event that % 9' is % 

- " "GD "
 @ ' -expanding. Let )
!  A !  / // 
" "

+   P
* +  ' -
Proof : Let


? %; %' - %
? % . Then,
+*
, . -
- / % 9'
 / % 9'
 . The proof that  * J: ' - 
* 6 - 1/ ' -
0

% 9'
 B  F is the same as the proof of Lemma 2 replacing  by  2 . The result 
follows. => (of lemma 3)

Lemma 4 Let 
>9 ,
 Q? A >4(' %:'F , D
$F-4 - FE

and @
 F . For every ?  , there *
exists a bipartite graph  on !  " / / / "  % and !  "/ / / "  ? % such that the following two properties
hold:

(i)  F- * 0"8 %  ' * =4 for every " / // "    ! ? % ,
#
(ii) * 63% -9' is %"  " D " ' -expanding  4 "
&@ B $F

5
when - is drawn from  # % ' .
Proof : Let %

"-
9' be drawn from  %  &?' . We have " ""
% 9' is %:   &@ ' -expanding B * +  - " "GD " 

+
$F- by Lemma 3. Moreover, 97 ;  -F 0"8 %/9'  B  %: .?' 
B 1>F 4   " - "   0/21 E
by Lemma 1. Let %
 
"- 
9' be the event that % 9' is expanding and every right-node in has degree -
 4
between  F- and = . Combining both equations above we have that %

9' B  F
.
 "- 
On the other hand, %

9'
*  %

9' -" - Z
- 


P
 * J
where  ranges "-  * 6 
#
over all bipartite graphs on  and 
C? nodes. Therefore, there exists some fixed  such that
* 6 %
 - 
"-
9' -
 B  F
. Moreover,  %
 - 
9' -
 equals * <
%!  ' when  is "-  * + " Z
drawn from  # %!
' . Finally, since this probability is strictly positive, it must be the case that 
satisfies property (i) in the lemma since it is independent of  . (of lemma 4) =>
3.2 The Lower Bound Argument
Before we state and prove our main theorem, we will give some definitions and lemmas.

Let us first give a normal form for !"$3%:;' -refutations of - 
  . We claim that every !"$3%:;' -
 
refutation of - 
  can be turned into a !#"$&%(' -refutation of similar size in which no  -term

is of the form    
 
'(  with 
1  + . To check this, observe that such a  -term must have been
  
  
  
introduced at some point by the rule of -introduction with, say,   and ,
'(  . Cutting

subsumes
  
them with the axiom - 

2 '   we get
% ,  ,
'(  ' .
that can be used to continue the proof because it

Let  be a  -disjunction, and let %/ &9'  % ' . We let


"   be the result of assigning  %
2 
 and , '   . for every  +   %/9'

!
 
"     
 % to , and simplifying as much as possible.

       
This includes replacing subformulas of the form
% + ' by
%
+ in some specified order; here and + are literals. Given a restriction
 
+ ' by , and subformulas of the form

-
" " " "  %/ "  " " "
-
% %   &  ' / // %  # & # ' ' , we let be the result of applying %   ' / / / %/ # & # ' successively in
 
" "
this order. For every    / / / &? % , we let
% %/  &  ' / / / %  & ' ' .
! " " " "
Let us now study in more detail the result of applying a pair of a restriction to a 2-disjunction.
First we give some definitions. We say that a pair %  & '  % ' hits

" 
if either    occurs

positively in , or ,
'   occurs negatively in for some  +  %/9'  !  % . Equivalently, %/ &9' * "
 
hits if it sets some literal of to  . If the literal is free, it knocks out the  -disjunction. If
the literal is part of a conjunction, it will locally create a free literal. In general, we say that
" 
  % 
%/ &9'0 % ' knocks if       . We say that %/ &9'0 % ' is a bad choice for if it does " 
not knock it and there exists  +   %  ' 
! % such that %   ' knocks . A bad choice may or
+ " 
may not be a hit.


Lemma 5 Let be a simplified  -disjunction, and %/ &9'  % " 
'. If %/ "&9' hits  and is not a
knock or a bad choice, then   has more free literals than .  % 

6
 "
Proof : First notice that the literals that %/ &9' sets to  are in a conjunction, otherwise %  "
 ' is a
knock. Such literals can appear positive or negative. We will discuss the two cases:

(i) The literal is ,  and appears in a conjunction of the form    

. The pair %/ &9' does not "
set to  otherwise we would have a knock. Also, it does not set it to . either, otherwise

, '   and such a conjunction is not allowed in the normal form. On the other hand,

does not appear free because is a simplified  -disjunction. Finally no free literal of 
" 
desapears when we apply %/ &9' to , otherwise %/ &9' would be a bad choice. "
(ii) The literal is , '   , and it appears in a conjunction of the form   '   
. Because %/ &9' is not "
"
a knock, it does not set to  . Also, %   ' does not set to . either, otherwise it would be
a bad choice, given that the indegree of  is or more. As in the previous case and for the

same reasons, does not appear free in , and no free literal of desapears when we apply 
"
%   ' .
The lemma follows. =>
Theorem 2 Let   be a constant. For all sufficiently large  , every !"$&%;' -refutation of 


 
 1 
has size at least  1&   .

Proof : Let >
  , ?
:F ,  +
 ? , and 
> 
3 + . Let
%  ' with D

 ' " % .%
% %

? be the bipartite  graph of Lemma 4. We show that every !#"-$3%(' -refutation of
 1  
and 5

- 
 has size at least  $   . This will imply the Theorem since a !"$ %(' -refutation of



  ' ' gives a !#"-$3%(' -refutation of -
 of no bigger size.

that - 
 has a !"$&%;' -refutation of size )


 $   . ; 1  
Let us assume, for contradiction,


We will use the following concepts. We say that is large if it contains at least
:F(  
 
distinct literals; otherwise, is small. We say that is wide if it contains at least
:F(%54768  ' H

free literals; otherwise, is narrow.
- 
In all probabilities that follow, is drawn from the distribution  # % ' . Our main goal is to



prove that the probability that a fixed  -disjunction of remains large is exponentially small;
that is, we aim for a proof that

* J  % / is large *   11&   

/ (4)

This will suffice because then * U(7  

;4 % / is large * )"   11&   
 $F
, and also
* 6  % -9' not %"  "GD  "@ ' -expanding  * >F
by Lemma 4. This means that there exists
a re-
striction -   # % ' such that % -9' is %"  " D "&@ ' -expanding and every  -disjunction in % / has


less than 
D  @9F- literals. This is a contradiction with Theorem 1.

7
 " "   be the event that  % / is large, and let   be the event that  % /
For  !  / / /
narrow. Recall that -
&? %


, let
 
% %  "  ' " / / / " % " ' ' . Then,
/ & / 


is

 

*   % / is large *
   *    * #   
#   

 #
1  #
1
* J       *  #  

#
* 
  
/


#
1 
 #
1
*     
We will show that every term in this expression is exponentially small. The bound on terms of the
form   will be proven in Lemma 7. For the last term, we use an argument similar in

 *   1 &    + .
spirit to the one by Beame and Pitassi [4]:
*   #    #
1
 
 be the indicator random variable for the event that %  "  ' knocks  % /
Lemma 6
Proof : Let ) / &
  . Then,
 

*    * *  . 
#   )  

 

  



 #
1 #
1  
 #
1 -

)    -
*





.  
-
-
-
 ) 
. 

#
1 

 #
1 -
- #
1  


)   )    ---
-
*  

.  ) 
. 
*
#
1 -
-
1 #




) 
- )


*  

.
-
-
-    ) 
. 
/
#
1 - #
1  

Fix  "/ / / "
   holds,
! ? F and let  be the set of holes that occur in a free literal of    .
&? %  %/
Given that
  %/

  is wide which means that there are at least free literals. Therefore H
% % ;H
 B F , where 
= 4 
is an upper bound on the right-degree of . Moreover, every   
gives a possible knock, and different holes give different knocks. The reason is the following: if
"
2  is a free literal, then %  & ' is a knock; and if    is a free literal, then %/ +  ' is a knock for
 "
B 
every  +  %/9' ! % , which is non-empty since the right-degree of is at least two. Therefore,
-

* )  )  %' % H
-


-
-
-   ) 
. 
B
%: 6 '
B

/
1    ? 
- #

Therefore,


*  #  
  
* ( H

#
1 *  
   *    1 $   + /

1
 # 

8
=>
* J       *   1 $     .
(of lemma 6)

.*
*

Lemma 7 Let be such that ? F C? . Then,
  % /  % /

Proof : Recall that  is the event that is large, and  is the event that
We let ) be the indicator random variable for the event that %/ & ' hits
  , where
is narrow.
"   %/ - 
" " "   "   P  



% %   &  ' / // %   &  ' ' . Let )


) . Then, for every , 
*      *       2 ) 
  
       ) B  *

 

* * 6    )   * J      ) B =/

*    2)   *.   1 $  
and *        ) B  *   1 $     which is clearly enough
We show that each term in this expression is exponentially small. More precisely, we show that

to prove Lemma 7.


  )    *   1 $  
.
9F %54768  '  . Then, * 6 

P      . Observe that  implies   for every

Claim 1 Let

Proof : Let
%  " / / / " ' . " 
 

!   ! % ; % 

 *
because if  % / is large, so is  % / for every  * . Then,
    

 *  )    
 *  )    

 

* 6  )  







   
  -  

   * )    ---  )     *
- 






  
-
* 
  * )         ---    )     *

-




   
* 
  * )    ---         )    /
- 
-



 

   " / / / " . Let  be the set of holes that occur in  % /  . We have %  %  - given that
Fix   ! ,%   B F 
 is an upper bound to the right-degree of . Moreover, every   

  holds. Again, 

gives a possible hit, and different holes give different hits (the reason is the same as in Lemma 6
for knocks). Therefore,
  
   ) 
* ) 
% %
-
-
-  /
-    


%: <  '
-


B
 ?
B


Since there are at least  zeros in %  " / / / " ' , we obtain 

 
   
 
!
"  $ #% & '
!
"  ( #% 

*   )  * 
  *  *
 
   *
 

      
 


  

* ")+*  ]E ,#4768% 9' 4,68% '  *    1 &   

/

 



9
=> (of claim 1)

Claim 2
6       )   *    1 &     .
B


 
For every   !  / / / &? % , let  !


Proof : During this proof we will drop the subindex in  and  since it will always be the same.
" " " "'
% be a random variable indicating whether %/ & ' is a
" 
knock, a bad choice, or none of the previous respectively for    . For * !
  %/  " "' 
indicator random variable for the event that
 , and let ) 


)  . Thus, ) is the number

% , let ) be the
P 

  -  " 
of knocks and ) is the number of bad choices of . 

- " " " "

Fix
% %/  &  ' / / / %  # & # ' ' such that 2) B holds under . Observe that %  & '  -
 %/
does not knock
  for any   !  / / / ,% since " "
must be large. Hence, ) 
. under .  % / -
Let

%   H
' F %  ' . We now claim that ) 7B
. Suppose for contradiction that the number " 
of bad choices is less than
. Every bad choice %/ & ' removes at most  free literals since at

" 
most those many literals about hole  may appear. Moreover, since there are no knocks, every hit
%/ & ' that is not a bad choice increases the number of free literals by at least one (see lemma 5).
It follows that the number of free literals in is at least %) 2) '  ) 
  % /
% '

,    +  H
a contradiction with the fact that holds under . We have proved that ) B - *     .*
* 6 ) 
 
. 2) 7B
. The intuition behind why this probability is small is that every bad choice
could have been a knock. This makes unlikely that produces many bad choices and no knocks. -
, * J  - " " -    
In what follows, we will prove this intuition using martingales.
For   !
 " "' " "
% and   !  / / / 2% , let  be the random variable
-

 -  / //

.
O   , 
We define a martingale  // / O " "  O
 with respect to  // /  - " " -
as follows: Let 
O
. , and   O
)  . Recall that ) is the indicator random variable for the event that
  

 . So


)  O  -- -  " // / " -       
% O 6,  ' ,  % O ,  ' % ,  '


  

  

 
% O ,  ' % ,  6,  ' ,  O /


Hence, O
  is a martingale with respect to -   . Observe also that O )  P
 , . 
! %
Similarly, we define
 " / / / "
as follows: Let


 )   ,   . It is also
, and

! % 

easy to see that

  is a martingale with respect to -   . Again,

)   P   ,    .
! %
 .

! %







Subclaim 1 ,  % -9'
 
, % -9' for every -  % ' and  "/ / / " .
*B F   #

0 ! 2%

" // / " and - % %  "  ' " // /" % " ' ' . We want to show that ,  % -9'

,  % 9- ' . Define three sets as follows: let  % " 9' % '
Proof : Fix   ! 2%
/ &  # & # .B

 " / / / "   , let   be

! / & *  ! 
 F  ;2. 1 & %>%
the set of knocks for  % /  in  , and let  be the set of bad choices for  % /  in  . Observe that
,  % 9- ' %  % %  %   and ,   % 9- ' %   % %  %   . On the other hand, every bad choice % " 9' 






 / & 
gives a possible knock % " 9'   by definition. Moreover, bad choices with different hole
/ + & 

10
 % % % %
, - , -
components give different possible knocks. Grouping  by holes, we have that   B DF  .
Consequently,  % 9' B  % 9' F  as required. (of subclaim 1) =>
%O   O   % *

To complete the proof of claim 2 we will need the following form of Azuma’s Inequality: Let
O "
 / //


"O
 be a martingale such that   ; then,   B


    for * + % O  O %  *  1
every  . [11]. Now,
* 6 ) 
.  ) B

* J3) 
. 2) B
 O  B
F- 
*  ) 
. 2) B
 O  
F /

The first summand is bounded by *  O  B
F-  *    1 
by Azuma’s Inequality. The second

 P   ,   P   ,   
-  *
summand is bounded by
* ) 
.

B
F-  * *  ) 
.

B F  

* * 
* 
-  *    1 /  F 



The first inequality follows from Subclaim 1, and the third follows from Azuma’s Inequality again.
The addition of the two summands is then bounded by    1 $   as required. => (of claim 2 and


lemma 7)

We are ready to complete the proof of our goal: equation (4). We have shown that

   1 &         1 $   + *    1 $   

/
 #
*   % / large  * 

#
1
=> (of theorem 2)

By a different setting of parameters, it is easy to see that the strongest lower bound for 
 
 "  %


A 

is of the form
 
)  

+ . Namely, put ?
:F ,
 F(% % 4,68 
' 4768 ' and


-
F  for 3 H 
that calculation. Therefore the best result is an exponential lower bound for 
 3)*7+ .

We conclude this section with a separation result. Given that !"$&%54,6=80' and depth- .0/21  are
polynomially equivalent, and given that 
  has quasipolynomial-size proofs in depth- .0/ 1

[14], we obtain:
Corollary 1 There is an exponential separation between !#"-$ %:;' and !#"-$3%547689' .

4 Lower Bound for Random CNF Formulas

4.1 Random Formulas and Restrictions
The model of random > -CNF formulas that we use is the one considered in [10, 3]. The distribu-

tion is denoted   and consists in choosing  clauses of exactly > literals independently with


replacement. Most of the next definitions are taken and adapted from [3].

11
Definition 2 For a real number  , a set of clauses is  -sparse if % % *  % % ' % where %

  ' is the
set of variables appearing in .
 

Definition 3 If is a set of clauses and is a literal, we say that is pure in
contains and no clause of contains .
 if some clause of

Definition 4 For H*  and * %. "  ' , the following properties are defined for  

formulas

:
  %ZH' : Every set of * H clauses of
is 1-sparse.
?


 %H' : For such that H -K *@H , every subset of

? F ? ? clauses of

has at least ? pure
literals.

For a given refutation system E , we say that an E -refutation is > -bounded if all formulas of the
refutation involve at most > distinct literals.

Proposition 1 [3] Let E be a sound refutation system with all rules of fan-in at most two. Let
H
 . be an integer and

be a CNF formula. If properties % ' and % ' both hold for , then
 ZH  H

H
has no  F- -bounded E -refutation.

"
A restriction is a sequence of pairs %/ &9' where  is a variable and  is either ?  or @ . For   H 
a  -disjunction let  %: %
be the number of distinct literals occurring in it. Let  be a probability
distribution on restrictions. We say that  satisfies property  % ' if and only if for every  "
 -disjunction , >B *  %  % / % ] *
$F
 . We will consider two probability distributions.

chooses a permutation of the variables uniformly at random, then chooses each variable

with probability &F in the order of the permutation. The values assigned to the variables are
chosen uniformly at random from ?  and @ . 8   H]

chooses ? , the length of the restriction, with a binomial distribution of parameters &F

and  . Then chooses uniformly at random any sequence of variables of length ? without
8
 H 
repetitions. The values assigned to the variables are chosen uniformly at random from ? 
and @ .

We prove that   and  are the same distribution of probability. Obviously both distributions
produce exactly the same restriccions. We only must show that any restriction has the same -
probability in both distributions of probability.

Lemma 8 For every   "/ / / "& # and   " / / / "& # ,

/
 -


% %   "&  ' " / //$" %  # "& # ' ' 
/ *  -


% %/  "&  ' " / // " %/ "
# & # '' /

12
Proof : The probability
/    -
% %   "  ' " / //$" % "
&  # & # '' is easy to find:




# 
<
  # 
/
?        %   '  / / / %:    ' 
?
(5)

The first part corresponds to the probability of choosing the value ? from a binomial distribution.
Remember that ? is the length of the restriction. The rest of the expression is the probability of
choosing the ? correct pairs %/ & ' .
" 
The probability 

/ "&-
% %/    ' / / / %  # & # ' ' is a little trickier. We will compute the " " " " 
probability of finding a permutation of the variables that is compatible with %   / / / & # ' , that is, " "
" "
the variables !  / / / & # % appear in that order. Then we multiply this probability by the probability

of choosing the exact places where the variables in are and choosing the right value for them: -


 # %:  ?  '


# 
<   #  / (6)
  
%    #

We first choose ? places to put the variables in , then we fill the gaps with the permutations of the -

other  ? variables. These are the favorable cases, those that are compatible. With straightforward
manipulations it is easy to see that (5) and (6) are equal. (of lemma 8) =>
The following is adapted from [3], with a minor change in the probability distribution.

>  .   ,  
Lemma 9 For each integer
holds. Let  ,  , ,  with  H

B
 
and
for 





B ! 

- ! .
, there are constants
, such that the following
. Let    and 



If  +*   :F 
 1
 and H *  9F  

 1    , then % / satisfies %H' with probability <(%  ' in
H.

If H " *  


 9F 
 Z% H ' with probability ;%  ' in H .
M1    


 , then

%/ satisfies


Theorem 3 Let  be a distribution over > -CNF formulas. Let H "  and . and let   B * be a
distribution over restrictions that satisfies  % H - " ' . Then,  F 

*   H
'    *  * 
% / does not satisfy  %H' 


/ 
 0
 % ? F






 
* /   % / does not satisfy %H' "
  


 





where  H0% ' is the minimum size of a !"$3%:;' -refutation of .

?


Proof : For a fixed unsatisfiable > -CNF , let , be a minimal-size !#"-$3%(' -refutation of

. Let
- !  .
* J
% / satisfies  %ZH'   %H' *
 ,.% / is not H  bounded 
 F

*
 7S , %  % /% H -   ;   F

*  H0%
'  / ?


13
The first inequality follows by Proposition 1, the second is immediate, and the third follows by
union bound and the fact that  satisfies  %  F-  ' . H "
To finish, let

 %
 Z% H'[ * 
% / does not satisfy  %H'Z/

/ 
% / 
'

/ does not satisfy

Then, ] H  % '6


 implies that * /  % / satisfies %H' 
 %H'   , and so  %
'  - . 
?


Therefore, *   H0% '   * *  %
'   *    %
' by Markov’s inequality.
  ?
 F
 F 7 F
F  $F

The result follows. => (of theorem 3)

4.2 The Lower Bound Argument

For simplicity, we only state the lower bound for the case  3    .
Theorem 4 Let

!  3    . Then, !#"-$3%(' -refutations of

require size
  

*

11&    

 almost
surely.

Proof : Let  =1  , > 
, fix an arbitrary   %. "  ' , and put 
 3 :F(%:1 '  1[3
 +  M13 and H

%C' 3 
"  3  9F-
1 M1   ' . Observe that these numbers satisfy the two hypothesis in Lemma 9.
Let
 % 9F1 



  *
1 $
     . If we could prove that
 satisfies property  %  H F "  ' , then *  ?] H0% "' 
 F-  2 % ' by Theorem 3. Since  % ' is (%  ' according to Lemma 9, the Theorem would
follow.
It remains to prove that  satisfies property  %  F- ' . In the following, we think of as H " -
drawn from . We let
% %  & ' / / / %  #  # ' ' .
   - " " " "
A 2-disjunction is large if it contains at least
 F literals, otherwise it is small. A 2-  H
" 
disjunction is wide if it contains at least 3
&F %54,6=8 %  ' ' free literals, otherwise it is narrow. We
say that %  & ' knocks a 2-disjunction if it makes it true. We say that %/ & ' hits a 2-disjunction
" 
" 
if it makes true a literal in it. Notice that every knock is a hit, but a hit might not be a knock. We

- " "  "   "  

say that %  & ' is a bad choice if it does not knock the 2-disjunction but could have knocked it just
by giving the opposite value to the variable. For  ? , we let be % %   &  ' / / / %  & ' ' . When )*
possible we simplify  -disjunctions: we substitute subformulas of the form
     % + ' by and
   
subformulas of the form % + ' by + . We aim for a proof that

* J  % / is large *  "  

" * % %  "
 
(7)

 
where is an arbitrary simplified  -disjunction.
  /  .
Let be the event that  contains at least  %/  distinct literals. Let be the event

*   
*    % - % &F  *   (
 % - %>B &F / (8)

14
Obviously *   (
 % - %S  * *  % - %S  F-  which is smaller than    15 by Chernoff bounds,
&F-

A% ' *.    
"* 
% * 6  -- % - % B &F- (/
so 
 -
We show now that * + - % - % B &F-  is exponentially small. For every  such that &F ? *  * &F- ,
let
  be the event that  % /
is narrow, that is, it contains less than 3 free literals. Let be the
event that %- % >B &F . Then,
- -

    1  *     1 
 

J 
 -  -
-
- 
 -
-
-

 -
-
-

/ (9)
  1   
1 
- -

? * * 
We show that both terms in (9) are exponentially small. For every  such that  F  &F , let
be the indicator random variable for the event that %/ & ' is a knock. Then the second term in (9)
" 
is
- -

*     1 
1 
 


-
-
- 
* *   1 
.   
-
-
- 


- -
  1   1     1
 - 
-  -

1  1  -  
  * .   
. 

*



-
- 
- 
 1    1 -   1
 -

 

1  -


 *
.    ----   
.  
*
 1   -   1 
1  - )  


 *
. ----      
.  
*


 1   1 

*   1  0%:  3   '  *  < =3    1  *



 1   

*   + 
  "  
" * % %
/


The first term in (9) is also exponentially small. Observe that

 -  -

*     
1 - 1    --- 

*   %  ' -
 - 
 - 


(10)
-
  1    1 
- -

*    1 * +      --  / (11)
  1 
The last inequality is true because
 implies
  for any * &F .

15
    

is such that &F ? *
*  *  "  

" * % %  .

  , then
J   -
Lemma 10 If &F -

*    " 
Proof : For every 
 %/
let ) be the indicator random variable for the event that %  & ' hits
"

  , that is, that %/ & ' gives value  ?  to a literal in
  . Let )
8
) . We divide  %/ P  

the calculation in two parts: what happens when the number of hits is less than a certain

&F(%<4,68%  ' ' and what happens otherwise.

* J      -
- 
* J       )  -
-  * J       ) 
B
-
- 
We start by the easiest part. The intuition is that if the 2-disjunction is large it would be extremely
difficult to hit it only a few times.


Sublemma 1 * <
  )  - *  " " * % %  .
 -
  




Proof : Let

%  " / / / " '
! . "   P      . Observe that  implies   for every
! %

;

% 

 *
because if  % / is large, so is  % / . Then,

   --
 *    )  --- 


* 6  )  - 
-


    --

  *    )  --- 








  


     --   )      *
 -


    -  

2 )  


-
-
 
* 
 
  2)  ---    )      *
 


 -




   
* 
 
)    ---         )      /
- 
-




 
" / / / " .
!

  --    
Fix   2%

* )  ---      )      0%:    ' =  /


B B



16
Since there are at least  zeros in %  " / / / "  ' , we obtain
   -  * 
 6     *
 

J  )  - 


(#% $#%
*      !"   *     !"   *

  

  9% 
 ' 

* ") *  = ,#4768% 9' 4,68% '  *




*  !  " .  

% *   " "* %% /
 


 





=> (of sublemma 1)

The last thing to do is to see what happens when the number of hits is big.
 

Sublemma 2 * 
  2)  -  *  " " * % % .
-  


 B



Proof : For every  *  *  - , let

 
"  " ' be a random variable indicating whether %  "  '

"  " ' , let ) 
F  ! % / &
is a knock, a bad choice, or none of the previous respectively for  %&/  . For 
be the indicator random variable for the event that
  , and let )  P  )  . Thus, ) is the






 ! %


number of knocks and ) is the number of bad choices of - . For the rest of the proof we will skip
     )  . Note that the


the condition on and the subindices from and . Fix - satisfying  .B

number of knocks is 0 because the 2-disjunction still exists, so )  . . Now let be
%U   ' - ,

3 F
we now claim that )
 

. Suppose for contradiction that the number of bad choices is less than
B

. Every bad choice % " ' removes at most one free literal. Moreover, since there are no knocks,
  / &
every hit % " ' that is not a bad choice increases the number of free literals by at least one. The
 

 
reason is that such a hit turns a conjunction into a free literal. Remember that we simplify the
2-disjunction when possible, and so the literal was not free before the hit % " ' is applied. It  &
follows then that the number of free literals in  % / is at least %)  ) '
 )   


contradiction with the fact that holds under - .
,a 
3

So far we have proved that *  

   )   * *  ) .  ) 
 . The intuition B
B
behind why this probability is small is that every bad choice could have been a knock. This makes
it unlikely that - produces many bad choices and no knocks. In what follows, we will prove this
intuition using martingales.

* % %
 
Claim 3
 ) 
.  ) B
 *  " "
 


.

Proof : For 
   !
" " '
and  !  / // % " " , let ,  denote the random variable
 
2%

- -  " / / / " - O " // / " O with respect to -  " / // " - as follows: Let
-

 . We define a martingale   

17
O 

, and . O  
O  +)   ,  . Recall that )  is the indicator random variable for the

 . Observe that
event that

)  O   -- -  " // / " -  
 6,  ' ,  % O  ,  ' % ,  '
       


 %O
 

% O ,  ' % ,  6,  ' ,  O /

Hence, O
  is a martingale with respect to -   . Observe also that O )  P
 , . 
! %
Similarly, we define
 " / / / "
as follows: Let


 )   ,   . It is also
, and

! % 

easy to see that

  is a martingale with respect to -   . Again,

)   P   ,    .
! %
. 

! %







We will use the following form of Azuma’s Inequality: Let O  " / / / " O
  % *  ; then,
& % O VO  %
* B   1  for every
. .  In the next calculation
that % O  O
be a martingale such
  -  ' ,  % 9- ' for every - and   " // / " .
we will also use the fact that ,  % 9

>B
!

 2%

* 6 )  .  )
 * J3)  . 2 )
 O
- 

B

B  B F

*  )  . 2  )
 O 
  /
B  F


The first summand is bounded by *  O
-  *    1 by Azuma’s Inequality. The second

 B F
summand is bounded by

*  ) 
.  P   , 

B
F-  * *  P   ,    ) 
.

B
F -  *
* * +
 *
-  *  F

*    1 " 

 

by Azuma’s Inequality again. ?

Therefore, the sum is bounded by   " "

  

% %  *   "
" * % %
 



as
=>
required. (of claim 3 and sublemma 2).

With both sublemmas proved, so is Lemma 10. We are ready to complete the proof of our goal
(7). We have shown that

*   % / is large *    
"*  %   "  
" * % %
 1   "  
" * % %  *   "  
" * % % 
        
/
  1 
=> (of theorem 4)

We give another proof of claim 3 that does not require martingales.

Claim 4
6 )
.  ) B G *   

18
Proof : Let us call a restriction favorable if it has
or more bad choices and no knocks. By
modifying a favorable restriction, we can get    restrictions with one knock or more just by 
changing the value of the variables that form the set of bad choices. Let us call these restrictions
knock restrictions.
We will show now that no different favorable restrictions generate the same knock restrictions.
Let us consider two favorable restrictions, say @  and @ . Both restrictions must have the same
variables in the same order, otherwise they cannot form the same knock restriction. Now, let us
call  the first variable such that @  %/ '
1 @ %/ ' . Let us suppose that  is a bad choice for @  . This
is impossible because @  and @ are equal up to the variable preceeding  , so if  is a bad choice

for @ , then  is a knock for @ , so @ is not favorable. The same argument applies for @ . If 

is neither a bad choice for @ nor for @ then the value of  must coincide if we intend to build
the same knock restriction, because we are only changing the value of variables that produce bad
choices. We must conclude @
@ .




Now let us call the set of favorable restrictions and 4 the set of knock restrictions generated

%
by the restricions in . So

*  )
.  ) B

favorable %
* %
% % (%

possible 54
  


# 54


% (% % %    
5F





 
=> (of claim 4)

5 Separation between Res(2) and Resolution

In this section we prove that Resolution cannot polynomially simulate !"$ %;' . More precisely,
we prove that a certain Clique-Coclique principle, as defined by Bonet, Pitassi and Raz in [6], has
polynomial-size !"$3%:;' -refutations, but every !"$ -refutation requires quasipolynomial size.
The Clique-Coclique principle that we use,  
   ' , is the conjunction of the following J)  
set of clauses:
       *  * >
  
    (12)


    * * > "  *
".* " 
1


 


 
  * " *+ *  "  
* > " 


1
(13)

  '
     * *
+


+ (14)

   * " * * " 
 ' (15)

  * > +" 
1

 


  

   
'

'     * "
+

+* )* > "  *  ".*  "   " 

* > "  +
+

1
+

1
(16)
(17)

We start with a reduction from

 


J)   to 
  that can be carried over in !"$3%:;' :
 ' '

19
Theorem 5 Let > +  *
>  . If 
 ' has Resolution refutations of size ) , then
 
  +)    ' has
!"$3%:;' -refutations of size ) 
for some constant   . .
+)   

Proof : We use the following !#"-$3%(' -reduction to transform the formula 
    ' into 
 ' .
The meaning of variable   is that pigeon  sits in hole . We perform the following substitutions:

   


%    
  ,'
    


%/  
   '(  '
     ' 


First we show how to get clauses (1) from clauses (12) and (15). If we expand clause (1) for a
certain  we have:

%/   
 
 %   '  %   '   %   '   

%  
 %    '  %  3   3 '   %      '   '     /  
 
/  

%  
 %   '  %  3  3 '   %     ' 
/   '

 '
   /  
 
/  

3 /
3 33

 3 3    /   /   (18)

   
 
%    ' %   ' % 3   3'

/
/

/
  %    ' ' /  '   '
 
  '
 
We apply successively for  *
    along variables  * and> theand
.
 -introduction rule to clauses    + 
   '
 and
 

 
  
  get:  

  
%    ' %   '
  %    '      . 
/ 
         '     (19)

Observe that the conjuctions in (19) form the first column in (18). To add the second column of
. 
.**    

along variables   and  and get:

(18) to (19) we apply successively for  > + the -rule to clauses   '( and (19)

%/   
   %     %    ' 
.

%/   ' 
 % 
  
'   %      '   
.
  '
   (20)

 '     ' 3   '    


           . We
Now it is clear how to get (18).

           
Now we will show how to get the initial clauses (2). Let us consider the clause
  
first generate    ' and     ' . Let us rewrite them as:

  '  %   '  %   '   %   '  
%   

 
 
 3  3         / (21)      /  

  ' %   ' % 3  3'

%     %   '
   
(22)  /   

   

              and  is   $     $   . For
where is  
      
               '

as abbreviation of the 2-disjuction it denotes. It is clear that      

,  7
    '
the sake of brevity we use 
  , that is:    

is

             7                 7    

 
 
.
 '  
 
   

  '

20
      
   

Now we will get
  for  *  *  ,
1
from (21), (22) and (17). We apply the cut rule to (22) and 
 , and get:
   

     %    '   (23)    /   

Solving it with  
   we get       . Solving this clause with (21) we get
  
 
     

%  '   %   ' (  (24) /  

. 
  
   
  ' " / / / " %   ' as we did with %   ' .
Now we can get rid successively of %
   
It remains to show how to simulate a normal resolution step. We have 
 . and        and    /   /  

we want to get
(  . We expand both clauses:  

%
  '  %   '  %   '   %   '   . 
/ 

 
 (25) /    / 
3  
3 / 

 


%/   
 
 %   '  %   '   %   '   

%  
 %    '  %  3   3 '   %      '   '
 '
    /  
 
/  
/ 
3 3       /   /  

  
%     ' %     ' % 3    3'
 
/
/ /
  %    
/ 

%     ' %   ' % 3   3 '
/ 



  


 
%     '
   '
 (26)
/
/






/
/







/
/







%   '  %    '  %  / / /   '   %    '   

 
/


3 3 '
  /  ' /  ' /  '
 
If we get clauses    
 for  *
 *    as desired.
We will show how to get  
     . We solve (26) with     ,  of course. With these
    
, we solve them all with (25) and get
   
1

we get rid of the first column of (26) and we add a literal   . We can get rid of the rest of columns
     

by solving enough times with clauses 

     ,   , and we get       . => (of theorem 5)
1
 
 
 
    
 
We will use the Monotone Interpolation Theorem for Resolution together with the following
result of Alon and Boppana [1] establishing a lower bound to the size of monotone circuits that
separate large cliques from small cocliques. In the following, % > > + ' is the set of monotone

" "
functions that separate > -cliques from > + -cocliques on  nodes.

Theorem 6 [1] If @

%: " > " > + ' where * > + * > and > > + * F(% A 4,68 
' , then
   (1
'
  

"
)  % @ '*B A ?> > + 4768  

where )  %/@ ' is the monotone circuit size of @ .

21
Theorem 7 Let >
 and > +
%54,6=8
' F 4768 4,68  . Then, (i) 
 A J)    ' has !#"$&%(' -
refutations of size polynomial in  , and (ii) every Resolution refutation of 
 J)    ' has size at
)+*
least " %
% %54768 
' F 47684,6=8 
' ' .
Proof : Regarding (i), we have that > + 4768> +  %54,6=8 ' , and so 
 *  

> . On the
   *
' '
1


other hand, Buss and Pitassi [7] proved that 
 ' has Resolution refutations of size polynomial
  
in > whenever >B 

' '
. Therefore, by Theorem 5, 
   '  has !"$3%:;' -refutations of + )
size polynomial in  . Regarding (ii), we apply the feasible monotone interpolation theorem for
Resolution. We have
,4 6=8 
4,6=84,68 
* > + * 4,6=8 /
Therefore, by Theorem 6, if @

%" > " > + ' is a monotone interpolant, then
 



 

 
 
 

  

 

  "
 
 

)  %/@ 'B A ?  5% 4768 

' 
B A 
 3 1 
which is " )+* %
% %54768
' F 4,6=84,68  ' ' . => (of theorem 7)

As a corollary, we solve an open problem posed by Krajı́ček [13].

Corollary 2 !#"-$3%(' does not have the feasible monotone interpolation property.

6 Discussion and Open Problems

In the paper we proved that there is a quasipolynomial separation between Resolution and !"$3%:;' .
It is an open question whether the separation could be exponential, or a quasipolynomial simulation
of !#"$&%(' by Resolution exists. It is important to notice, that our lower bound for 
 would not

follow from such a simulation. Indeed, the lower bound that would follow from that would be of
the form   .
The previous separation was obtained using a lower bound for Resolution proved via the mono-
tone interpolation theorem. It is open whether the separation (or a stronger one) could be obtained
via the size-width trade-off [5] as a method for proving lower bounds for Resolution. It would also
be interesting to see what would that mean in terms of possible size-width trade-offs for !"$3%:;' .
We conjecture that !#"-$3%(' does not have a strong size-width trade-off. Notice that !"$&%54,6=89'
does not have it. This is because (a) !"$3%<4,6=89' is equivalent to depth- .0/21 LK, (b) 
  has

quasipolynomial-size proofs in depth- . /21 LK [14], and (c) 
  has % ' width lower bounds

for !#"-$ %<4,6=89' .
In this paper we extended the width lower bound technique beyond Resolution. A very inter-
esting open question is to see whether the technique can also be extended to give lower bounds for

22
 ! "$&% ? ' " / // " #
!"$3% ;' " # ! "-$ %<4,6=89' . It seems that some new ideas need to be developed to do that. This
question is related to the optimality of the !"$3%<4,6=89' upper bound for 
 

  .
Finally, we note that exponential-size lower bounds for 
  in !"$3%:>' implies lower
 
bounds for 
  in Resolution for some  . This is a long-standing open question.


References
[1] N. Alon and R. Boppana. The monotone circuit complexity of boolean functions. Combina-
torica, 7(1):1–22, 1987.

[2] P. Beame, R. Impagliazzo, J. Krajı́ček, T. Pitassi, P. Pudlák, and A. Woods. Exponential

lower bounds for the pigeonhole principle. In Proc. of the 24th Annual ACM STOC, pages
200–220, 1992.

[3] P. Beame, R. Karp, T. Pitassi, and M. Saks. The efficiency of resolution and Davis-Putnam
procedures. Submitted. Previous version in STOC’98, 1999.

[4] P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In Proc. of the
37th Annual IEEE FOCS, pages 274–282, 1996.

[5] E. Ben-Sasson and A. Wigderson. Short proofs are narrow: Resolution made simple. In Proc.
of the 31st Annual ACM STOC, pages 517–527, 1999. Revised version (2000).

[6] M. Bonet, T. Pitassi, and R. Raz. Lower bounds for cutting planes proofs with small coeffi-
cients. The Journal of Symbolic Logic, 62(3):708–728, Sept. 1997.

[7] S. Buss and T. Pitassi. Resolution and the weak pigeonhole principle. In CSL: 11th Workshop
on Computer Science Logic. LNCS, Springer-Verlag, 1997.

[8] S. R. Buss. Polynomial size proofs of the propositional pigeonhole principle. The Journal of
Symbolic Logic, 52(4):916–927, Dec. 1987.

[9] S. R. Buss and G. Turán. Resolution proofs on generalized pigeonhole principles. Theoretical
Computer Science, 62(3):311–317, Dec. 1988.

[10] V. Chvátal and E. Szemerédi. Many hard examples for resolution. J. ACM, 35(4):759–768,
1988.

[11] G. R. Grimmet and D. R. Stirzaker. Probability and Random Processes. Oxford Science
Publications, 1982.

23
[12] A. Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297–308,
Aug. 1985.

[13] J. Krajı́ček. On the weak pigeonhole principle. To appear in Fundamenta Mathematicæ,

2000.

[14] A. Maciel, T. Pitassi, and A. Woods. A new proof of the weak pigeonhole principle. In Proc.
of the 32nd Annual ACM STOC, pages 368–377, 2000.

[15] J. B. Paris, A. J. Wilkie, and A. R. Woods. Provability of the pigeonhole principle and the
existence of infinitely many primes. The Journal of Symbolic Logic, 53(4):1235–1244, 1988.

[16] T. Pitassi and R. Raz. Regular resolution lower bounds for the weak pigeonhole principle. to
appear in STOC’2001, 2001.

24