9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Exponential separations between restricted resolution and cutting planes proof systems

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

Maria Luisa Bonet Juan Luis Estebany Nicola Galesiz , , Dept. Llenguatges i Sistemes Informatics Universitat Politecnica de Catalunya fbonet,esteban,galesig@lsi.upc.es Abstract

We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like proofs for both Cutting Planes and resolution; in both cases only superpolynomial separations were known before [30, 20, 10]. In order to prove this, we extend the lower bounds on the depth of monotone circuits of Raz and McKenzie [26] to monotone real circuits. In the case of resolution, we further improve this result by giving an exponential separation of tree-like resolution from (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Putnam resolution proof. This extends the corresponding superpolynomial separation of [30]. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known [14].

Jan Johannsenx Dept. of Mathematics UCSD johannsn@math.ucsd.edu

1. Introduction

The motivation to work on the proof length of propositional proof systems comes from two sides. First, by the work of Cook and Reckhow [12], we know that the claim that for every propositional proof system there is a class of tautologies that requires superpolynomial proof size is equivalent to NP 6= co-NP . This connection explains the interest in developing combinatorial techniques to prove

Partially supported by projects SPRIT 20244 ALCOM-IT and TIC 971475-CE y Partially supported by project KOALA:DGICYT:PB95-0787 z Supported by an European Community grant under the TMR project x Supported by DFG grant No. Jo 291/1-1

lower bounds for different proof systems. The second motivation comes from the interest in studying ef?ciency issues in Automated Theorem Proving. The question is which proof systems have ef?cient algorithms to ?nd proofs. The most widely used proof system in implementations is resolution or restrictions of resolution. What we will show in this paper is that proving propositional proof complexity lower bounds has something to say about the non-ef?ciency of various strategies for ?nding proofs. Haken [17] was the ?rst who proved exponential lower bounds for unrestricted resolution. Later Urquhart [29] found another class of tautologies that require exponential size resolution proofs, and Chv? tal and Szemer? di [8] a e showed that in some sense, almost all classes of tautologies require exponential size resolution proofs (see [3, 4] for simpli?ed versions of these results). These exponential lower bounds are bad news for automated theorem provers, since they mean that often the time used in ?nding proofs will be exponentially long in the size of the tautology, given that the shortest proofs are. The next question is what about the classes of tautologies that have polynomial size proofs? Can we ?nd these proofs ef?ciently? [3, 9, 4] give weakly exponential time (2on ) algorithms for ?nding resolution proofs. But, can we do better? [19, 1] give weak evidence that the answer is negative. Formally, we say that a propositional proof system S is automatizable, if there is an algorithm that for every tautology F ?nds a proof of F in S in time polynomial in the length of the shortest proof of F in S . The only propositional proof systems that we know are automatizable are algebraic proof systems like Hilbert’s Nullstellensatz [2] and Polynomial Calculus [9]. On the other hand bounded-depth Frege proof systems are not automatizable, assuming factoring is hard [24, 7, 5]. Since Frege systems and Extended Frege systems polynomiallysimulates bounded-depth Frege systems, they are also not automatizable under the same assumptions. A commonly used strategy for ?nding proofs is to reduce the search space by de?ning restricted versions of resolution 1

that are still complete. One possibility is to restrict to proofs that are tree-like, which would be a good strategy, given that [3, 9, 4] have quasipolynomial algorithms for ?nding treelike proofs. Here we prove an exponential separation between tree-like resolution and resolution, showing that ?nding tree-like resolution proofs cannot be an ef?cient strategy for ?nding resolution proofs. Until now only superpolynomial separations were known [30, 10]. Many strategies for ?nding resolution proofs are described in [28], but very little theoretical work has been done until now. Goerdt [15, 14, 16] gave several superpolynomial separations between resolution and some restricted versions of it. In particular, he gave a separation between Davis-Putnam resolution and unrestricted resolution. We improve this result by giving an exponential separation between Davis-Putnam and unrestricted resolution, showing that using the Davis-Putnam restriction is not, in general, a good strategy for ?nding resolution proofs. The Cutting Planes proof system (CP ) is a refutation system based on manipulating integer linear inequalities for which the task of ?nding hard-to-prove tautologies is solved. [18] were the ?rst to show such a result in the restricted case of CP proofs whose underlying graph is a tree. Pudl? k [25] a and Cook and Haken [11] give general circuit complexity results from which a exponential lower bounds for CP follow. Nothing is known about automatization of CP proofs. Since there is an exponential separation between CP and Resolution (CP is more ef?cient) it would be nice to ?nd an ef?cient algorithm for ?nding CP proofs. A question to ask is if trying to ?nd tree-like CP proofs would be an ef?cient strategy for ?nding Cutting Planes proofs. One of the authors [20] gave a superpolynomial separation between tree-like CP and dag-like CP (this was previously known for a restricted form of CP from [6]). Here we improve that separation to exponential. This means again that trying to ?nd tree-like proofs is not a good strategy. This exponential separation is a consequence of extending the lower bounds of [26] to the case of real monotone circuits. As in [26] we prove an n lower bound on the depth of monotone real circuits computing a certain monotone function G EN n in P . This also implies an 2n lower bound on the size of monotone real formulas computing G ENn . This latter result allows us to obtain an exponential lower bound for the size of tree-like CP proofs for a formula associated to G ENn , using the interpolation technique of [23, 25]. The paper is organized as follows: in Section 2 we give basic de?nitions of the proof systems we consider. Section 3 has the de?nitions of monotone real circuits, and the proof of the depth separation for them, extending the results of Raz and McKenzie. Section 4 gives the exponential separations between tree-like CP and CP , tree-like Resolution and Resolution and tree-like CP and bounded-depth Frege

systems, and also the exponential separation between treelike resolution and regular resolution. Finally section 5 has the exponential separation between Davis-Putnam resolution and unrestricted Resolution.

2. The Proof Systems

Resolution is a refutation proof system for formulas in CNF based on the following inference rule:

A Resolution refutation for an inital set of clauses is a derivation of the empty clause from using the above inference rule. Several restrictions of the resolution proof system are known. Here we consider the following two: (1) the regular resolution system in which the proofs are restricted in such a way that any variable can be eliminated at most once in any path from an initial clause to the empty clause; (2) the Davis Putnam resolution system in which the proofs are restricted in such a way that there exists a sequence of the variables such that if a variable x is eliminated before a variable y on any path from an initial clause to the empty clause, then x is before y in the sequence. Cutting Planes (CP ) is a P system operating with linproof ear inequalities of the form i2I ai xi k, where the coef?cients ai and k are integers. The rules of CP are addition of two inequalities, multiplication of an inequality by a positive integer and the following division rule:

P P

C _x D_x : C _D

where b is a positive integer that evenly divides all ai , i 2 I . A CP refutation of a set E of inequalities is a derivation of 0 1 from the inequalities in E and the axioms x 0 and ,x ,1 for every variable x, using the rules of CP . It can be shown that a set of inequalities has a CP -refutation iff it has no f0; 1g-solution. Cutting Planes can be used as a refutation system for propositional W formulas in conjunctive normal form: note W that a clause i2P xP j 2N xj is satis?able iff the ini_ P equality i2P xi , j 2N xj 1 , jN j has a f0; 1gsolution. It is also well-known that CP can simulate Resolution [13]. A proof system is tree-like if the proofs are restricted so that every line in a proof is used at most once as a premise of an inference. Otherwise we will call it dag-like.

i2I ai xi k ai k i2I b xi b

;

3. Monotone Real Circuits

A monotone real circuit is a circuit of fan-in 2 computing with real numbers where every gate computes a nondecreasing real function. This class of circuits was introduced by

Pudl? k [25]. We require that monotone real circuits output a 0 or 1 on every input of zeroes and ones only, so that they are a generalization of monotone boolean circuits. Rosenbloom [27] shows that they are strictly more powerful than monotone boolean circuits. The depth and size of a monotone real circuit are de?ned as usual, and we call it a formula if every gate has fan-out at most 1. For a monotone boolean function f , we denote by d f the minimal depth of a monotone real circuit computing f , and by s f the minimal size of a monotone real formula computing f . The method of proving lower bounds on the depth of monotone boolean circuits using communication complexity was used by Karchmer and Wigderson [21] to give an log2 n lower bound on the monotone depth of stconnectivity. Using the notion of real communication complexity introduced by Kraj?cek [22], one of the authors [20] ?ˇ showed the same lower bound for monotone real circuits. The monotone function G EN n of n3 inputs ta;b;c , 1 a; b; c n is de?ned as follows: For c n, we de?ne the relation ` c (c is generated) recursively by

R

R

xi = 1 and yi = 0 The Karchmer-Wigderson game for f is de?ned as follows: Player I receives an input x 2 X and Player II an input y 2 Y . They have to agree on a position i 2 n such that x; y; i 2 Rf . Sometimes we will say that Rf is the Karchmer-Wigderson game for the function f . There

iff

then we say that the protocol solves R in k rounds. The real communication complexity CC R is the minimal number k such that there is a real communication protocol solving R in k rounds. For a natural number n, let n denote the set f1; : : : ; ng. Let f : f0; 1gn ! f0; 1g be a monotone boolean function, let X := f ,1 1 and Y := f ,1 0, and let the multifunction Rf X Y n be de?ned by

R

x; y; i 2 Rf

Rf and the depth of a monotone real circuit or the size of a monotone real formula computing f , similar to the boolean

case: Lemma 2 (Kraj?cek [22]) Let ?ˇ function. Then

is a relation between the real communication complexity of

f

be a monotone boolean

Recently, Raz and McKenzie [26] gave a lower bound of n for some 0 on the depth of monotone boolean circuits computing G ENn . We show that their method applies to monotone real circuits: Theorem 1 For some

c = 1 or there are a; b n with ` a ; ` b and ta;b;c = 1 : Finally G EN n~ = 1 iff ` n. From now on we will write t a; b ` c for ta;b;c = 1.

iff

`c

CC Rf d f and CC Rf log3=2 s f :

For a proof see [22] or [20]. Hence to establish Theorem 1, it suf?ces to prove: Theorem 3 For some

R

R

R

R

0 and suf?ciently large n CC RG n n :

3.2. DART games and structured protocols

Raz and McKenzie [26] introduced a special kind of communication games, called DART games, and a special class of communication protocols, the structured protocols, for solving them. For m; k 2 N, the set of communication games DARTm; k is de?ned as follows:

R

EN

0 and suf?ciently large n d G ENn n and s G ENn 2 n :

3.1. Real Communication Complexity

Let R X Y Z be a multifunction, i.e. for every pair x; y 2 X Y , there is a z 2 Z with x; y; z 2 R. A real communication protocol for R is executed by two players I and II , where I computes a function fI : X f0; 1g ! R and II computes a function fII : Y f0; 1g ! R. Given inputs x 2 X , y 2 Y , the players generate a sequence w of bits as follows:

R

R

X = m k.

w0 := wk+1 :=

wk 0 wk 1

if fI x; wk else

fII y; wk

If there is a function g

: f0; 1gk ! Z such that

8x 2 X 8y 2 Y x; y; gwk 2 R ;

Y = f0; 1gmk . That is the inputs for the Player II are k-tuples of binary colorings yi for m . For all i = 1; : : : ; k let ei = yi xi (i.e. ei is the xi-th bit in yi ). The relation Rx; y; z X Y Z de?ning the game, only depends on e1 ; : : : ; ek and z . This means that we can describe Rx; y; z by Re1 ; : : : ; ek ; z Re1 ; : : : ; ek ; z must be a DNF-Search-Problem. This means that always exists a tautology FR de?ned over the variables e1 ; : : : ; ek such that Z is the set of terms de?ning FR and Re1 ; : : : ; ek ; z is true if and only if z 2 Z is the satis?ed term of FR .

That is the inputs for the Player I are ktuples of elements xi 2 m .

A structured protocol for a DART game is a communication protocol for solving the relation R, where player I gets input x 2 X , player II gets input y 2 Y , and in each round, player I reveals the value xi for some i, and II replies with yi xi . The structured communication complexity of R 2 DARTm; k, denoted by SCR, is the minimal number of rounds in a structured protocol solving R. The main theorem of [26] showed that for suitable m and k, the deterministic communication comlexity of a DART game cannot be much smaller than that of a structured protocol. We shall show the same for its real communication complexity. Obviously, a structured protocol solving R in r rounds can be simulated by a real communication protocol solving R in r dlog me + 1 rounds. Conversely, the following holds: Theorem 4 For every relation R m k14,

For a relation R 2 DARTm; k, A X and B Y , let CC R; A; B be the real communication complexity of R restricted to A B . Fix a large m 2 N. A triple R; A; B is called an 1 ; ; `-game if R 2 DARTm; k for some k m 14 with SCR `, A X with jAj 2, jX j and 14 ThicknessA m 11 , and B Y with jB j 2, jY j. 1 Lemma 8 For every ; ; ` 0 with m 7 and every ; ; `-game R; A; B, 13 1. if for every 1 j k, AV DEGj A 8m 14 , then 0 ; A0; B 0 with there is an + 2; + 1; `-game R CC R0 ; A0; B 0 CC R; A; B , 1 :

R

R

R

2

DARTm; k, where

2. if `

CC R SCR log m

To prove this, ?rst we need some combinatorial notions and results from [26]. Let A m k and 1 j k. For x 2 m k,1, let degj x; A be the number of 2 m such that x1 ; : : : ; xj ,1; ; xj ; : : : ; xk,1 2 A. Then we de?ne

R

1 and for some 1 j k, AV DEGj A 13 8m 14 , then there is an + 3 , log m ; + 1; ` , 114 game R0 ; A0; B 0 with CC R0 ; A0; B 0 CC R; A; B :

R

R

To prove Theorem 3 from the lemma, we show that for every ; ; `-game R; A; B,

CC R; A; B ` log m , 4 , + : 42 3 3 The case = = 0 gives the theorem. 7 For ` = 0 and m 1 , is trivial, since the right hand side gets negative for large m. We proceed inductively: Let R; A; B be an ; ; `-game, and assume that holds for all 0 ; 0 ; `0-games with `0 ` and 0 . For sake of contradiction, suppose that CC R; A; B

` log m , 4 , + . Then either for every 1 j k, 42 3 3 14 AV DEGj A 8m 13 , and Lemma 8 gives an +2; + 0; A0 ; B 0 with 1; `-game R CC R0; A0 ; B 0 CC R; A; B , 1

` log m , 4 , + 2 + + 1 ; 42 3 3 14 or for some 1 j k, AV DEGj A 8m 13 , then Lemma 8 gives an + 3 , log m ; + 1; ` , 1-game 14 R0 ; A0; B 0 with

4 CC R0; A0 ; B 0 ` logm , 3 , + 42 3

logm 4 + 3 , log m + + 1 14 = ` , 1 42 , 3 , ; 3

A j := x 2 m k,1 ; degj x; A 0 j AV DEGj A := jAAjj j MINDEGj A := xminj degj x; A 2A ThicknessA := 1j k MINDEGj A : min

R

The following lemmas about these notions were proved in [26]:

R

A0 A and 1 j k, 0 AV DEGj A0 jjA jj AV DEGj A (1) A ThicknessA j ThicknessA (2) Lemma 6 If for every 1 j k, AV DEGj A m for some 0 1, then for every 0 there is A0 A with jA0j 1 , jAj and 1 m ThicknessA0 k1 + , 1 ln ,1 : ,

Lemma 5 For every

1 = 1 and = 4m, 14 , we get 2 Corollary 7 If m k14 and for every 1 j k, 14 AV DEGj A 4m 13 , then there is A0 A with jA0j 11 1 jAj and ThicknessA m 14 . 2

R

R

R

In particular, setting

both contradicting the assumption. Proof of Lemma 8: For part 1, we ?rst show that CC R; A; B 0. Assume otherwise, then there is

R

a term Cz in the DNF tautology de?ning R that is satis?ed for every x; y 2 A B . Therefore yj xj is constant for some 1 j k. If denote the number of possible values of xj in elements of A, then this implies that jB j 2mk, . On the other hand, jB j 2mk, , hence it follows that 1 , which is a contradiction since 13 m 7 , whereas 13 AV DEGj A 8m 14 implies 8m 14 . Now let an optimal real communication protocol solving R restricted to A B be given. For a 2 A and b 2 B , let a and b be the real numbers played by I and II in the ?rst round on input a and b, respectively. W.l.o.g. we can assume that these are jAj + jB j distinct real numbers. Now consider a f0; 1g-matrix of size jAj jB j with columns indexed by the a and rows indexed by the b , where the entry in position a ; b is the outcome of the ?rst round when these numbers are played. Then it is obvious that either the upper right quadrant or the lower left quadrant must form a monochromatic rectangle. Hence there are A A and B 0 B with jA j 1 jAj and jB 0 j 1 jB j such that R restricted to A B 0 2 2 can be solved in one round fewer than the original proto13 col. By Lemma 5 (1), AV DEGj A 4m 14 for every 1 j k, hence by Corollary 7 there is A0 11 with A 1 jA0j 1 jA j 4 jAj and ThicknessA0 m 14 . Thus 2 R; A0; B 0 is an + 2; + 1; `-game. Part 2 is proved exactly like the corresponding lemma in [26], with the numbers slightly adjusted.

SCP YRG EN m; d d. Hence by Theorem 4, we get CC P YR G EN m; d d logm for m d28.

Lemma 9

R

The following lemma shows that the real communication complexity of P YR G EN m; d is bounded by the real communication complexity of the Karchmer-Wigderson game for G ENn for a suitable n.

, Lemma 10 For n := m d+1 + 2, 2

CC P YRG EN m; d CC G EN n:

Proof : We interpret the elements between 2 and n , 1 as triples i; j; k, where i; j 2 Pyrd and k 2 m . Now player I computes from his input x : Pyrd ! m an input ~x to G EN n with G ENn ~x = 1 by setting the folt t lowing:

R

R

1; 1 ` ad;j a1;1; a1;1 ` n ai+1;j ; ai+1;j +1 ` ai;j

for 1 j

d

for i; j 2 Pyrd,1

3.3. A DART game related to GENn

The communication game P YR G EN m; d is de?ned as follows: Let Pyrd := f i; j ; 1 j i d g. We regard the indices as elements of Pyrd , so that the inputs for the two players I and II are respectively sequences of elements xi;j 2 m and yi;j 2 f0; 1gm with i; j 2 Pyrd , and we picture these as laid out in a pyramidal form with 1; 1 at the top and d; j, 1 j d and the bottom. The goal of the game is to ?nd either an element colored 0 at the top of the pyramid, or an element colored 1 at the bottom of the pyramid, or an element colored 1 with the two elements below it colored 0, i.e. to ?nd indices i; j such that one of the following holds: 1. 2. 3.

t where ai;j := i; j; xi;j . This completely determines ~x . Likewise Player II computes from his input y : Pyrd ! 2 m a coloring c of the elements from n by setting col1 = 0, coln = 1 and coli; j; k = yi;j k. From t this, he computes an input ~y by setting a; b ` c iff it is not the case that colc = 1 and cola = colb = 0. Obviously G EN n~y = 0. t Playing the Karchmer-Wigderson game for G ENn now yields a triple a; b; c such that a; b ` c in ~x and a; b 6` c in t ~y . By de?nition of ~y , this means that cola = colb = 0 t t and colc = 1, and by de?nition of ~x one of the following t cases must hold: a = b = 1 and c = ad;j for some j d. By de?nition of col, yd;j xd;j = 1. c = n and a = b = a1;1. In this case, y1;1x1;1 = 0. a = ai+1;j , b = ai+1;j +1 and c = ai;j . Then we have yi;j xi;j = 1, and yi+1;j xi+1;j = yi+1;j +1xi+1;j +1 = 0. In either case, the players have solved P YR G EN m; d with-

i = j = 1 and y1;1x1;1 = 0, or yi;j xi;j = 1 and yi+1;j xi+1;j = 0 yi+1;j +1xi+1;j +1 = 0, or i = d and yd;j xd;j = 1.

,

and

Obviously, P YR G EN m; d is a game in DARTm; d+1 . 2 The following lower bound on the structured communication complexity of P YR G EN m; d was proved in [26]:

out any additional communication. Now the lower bound on CC P YR G EN m; d obtained from Lemma 9 and Theorem 4, together with 1 Lemma 10 immediately imply Theorem 3 with = 30 by 28. taking m = d t Let ~ be an input to G ENn . We say that n is generated in t a depth-d pyramidal fashion by ~ if there is a mapping m : Pyrd ! n such that 1; 1 ` md; j for every j d, mi+ 1; j; mi + 1; j + 1 ` mi; j for every i; j 2 Pyrd,1

R

and m1; 1; m1; 1 ` n (recall that a; b ` c means ta;b;c = 1). As the reduction in Lemma 10 produces only inputs from G EN,1 1 which have the additional property that n is genn erated in a depth-d pyramidal fashion, we can state the following strengthening of Theorem 1: Corollary 11 Let n; d be as above. Every monotone real formula that outputs 1 on every input to G ENn for which n is generated in a depth-d pyramidal fashion, and outputs 0 on all inputs where G ENn is 0, has to be of size 2n . The other consequences drawn from Theorem 4 and Lemma 9 in [26] apply to monotone real circuits as well, e.g. we just state without proof the following result: Theorem 12 There are constants ; c 0 such that for every function dn n , there is a family of monotone functions fn : f0; 1gn ! f0; 1g that can be computed by monotone boolean circuits of size nO1 and depth dn, but cannot be computed by monotone real circuits of depth less than c dn. The method also gives a simpler proof of the lower bounds in [20], in the same way as [26] simpli?es the lower bound of [21].

a coloring of the elements by 0; 1 such that 1 is colored 0, n is colored 1 and the elements colored 0 are closed under generation. The sets of clauses Gen~; ~ and Col~;~ are de?ned pq pr in Table 1. Obviously, if Gen~; ~ is satis?able for a ?xed tq 3 vector ~ 2 f0; 1gn , then n is generated in a depth-d pyramit dal fashion, and if Col~;~ is satis?able, then G EN ~ = 0. tr t Since the variables p occur only positively in Gen~; ~ and ~ pq only negatively in Col~;~, Theorem 13 is applicable, and pr the formula obtained from this application satis?es the conditions of Corollary 11. Hence we can conclude:

0, tree-like CP refutations of Theorem 14 For some the clauses Gen~; q Col~;~ have to be of size 2 n . p~ pr

On the other hand, there are polynomial size dag-like resolution refutations of these clauses. Theorem 15 There are (dag-like) resolution refutations of size nO1 of the clauses Gen~; ~ Col~;~. pq pr As the proof is very similar to that of Theorem 18 below, we omit it. The following corollary follows by the last two Theorems and well-known simulation results: Corollary 16 The clauses Gen~; q Col~;~ exponenp~ pr tially separate the following proof systems: Tree-like from dag-like Resolution, tree-like Cutting Planes from dag-like Cutting Planes and tree-like Cutting Planes from boundeddepth Frege systems.

4. Separation between tree-like and dag-like versions of Resolution and Cutting Planes

Cutting Planes refutations are linked to monotone real circuits by the following interpolation theorem due to Pudl? k: a

4.1. Separation of tree-like CP from regular resolution

We now modify the clauses Col~;~, so that the modpr i?ed clauses allow small regular resolutions, but in such a way that the lower bound proof still applies. We replace the variables ra by ra;i;D for a 2 n , 1 i d and D 2 fL; Rg, giving the coloring of element a, with auxiliary indices i being a row in the pyramid and D distinguishing whether an element is used as a left or right predecessor in the generation process. The set RCol~;~ is de?ned in Table 2. Due to the pr clauses (13) and (14), the variables ra;i;D are equivalent for all values of the auxiliary indices i; D. Hence a satisfying assignment for RCol~;~ still codes a coloring of n such pr that elements that can be generated from 1 are colored 0, the elements from which n can be generated are colored 1, and the 0-colored elements are closed under generation. Hence if RCol~;~ is satis?able, then G EN ~ = 0. tr t Hence any interpolant for the clauses Gen~; q p~ RCol~;~ satis?es the assumptions of Corollary 11, and pr we can conclude Theorem 17 Tree-like CP refutations of the Gen~; q RCol~;~ have to be of size 2 n . p~ pr clauses

p~r Theorem 13 (Pudl? k [25]) Let ~; q;~ be disjoint vectors of a variables, and let A~; ~ and B~;~ be sets of inequalities pq pr in the indicated variables such that the variables ~ either p have only nonnegative coef?cients in A~; ~ or have only pq nonpositive coef?cients in B~;~. pr Suppose there is a CP refutation R of A~; ~ B~;~. pq pr Then there is a monotone real circuit C~ of size OjRj p p such that for any vector ~ 2 f0; 1gj~j a C~ = 0 ! A~ ; ~ is unsatis?able a aq C~ = 1 ! B~ ;~ is unsatis?able a ar

Furthermore, if R is tree-like, then C~ is a monotone real p formula. We now de?ne an unsatis?able set of clauses related to G ENn . The variables pa;b;c for a; b; c 2 n represent the input to G EN n. Variables qi;j;a for i; j 2 Pyrd and a 2 n encode a pyramid where the element a is assigned to the position i; j by a certain mapping m : Pyrd ! n (cf. Corollary 7). Finally the variables ra for a 2 n represent

qi;j;a 1an qd;j;a _ p1;1;a q1;1;a _ pa;a;n qi+1;j;a _ qi+1;j +1;b _ qi;j;c _ pa;b;c r1 rn ra _ rb _ pa;b;c _ rc

Table 1. The set

_

for i; j 2 Pyrd for 1 j d and a 2 n for a 2 n for i; j 2 Pyrd,1 and a; b; c 2 for a; b; c 2

(3) (4) (5) (6) (7) (8) (9)

n

n Col~;~ pr

by

Gen~; ~ pq

is given by

(3) - (6), and

(7) - (9).

n and D 2 fL; Rg n and D 2 fL; Rg for i; j 2 Pyrd,1 ; a; b; c 2 n ra;i+1;L _ rb;i+1;R _ pa;b;c _ rc;i;D and D 2 fL; Rg ra;i;D _ ra;i;D for 1 i d and D 2 fL; Rg ra;i;D _ ra;j;D for 1 i; j d and D 2 fL; Rg p1;1;a _ ra;d;D pa;a;n _ ra;1;D

Table 2. The set of clauses

for a 2 for a 2

(10) (11) (12) (13) (14)

RCol~;~ pr

.

On the other hand, we have the following upper bound on (dag-like) regular resolution refutations of these clauses: Theorem 18 There are (dag-like) regular resolution refutap~ pr tions of the clauses Gen~; q RCol~;~ of size nO1 . Proof : First we resolve clauses (4) and (10) to get

which we have by induction, to give

qi+1;j;a _ qi+1;j +1;b _ qi;j;c _ rc;i;D

for every 1 a; b n. Finally, we have in particular q1;1;a _ ra;1;L, which we re solve against (16) to get q1;1;a for every a n. From these and an instance of (3) we get the empty clause. A proof of the upper bound in Theorem 15 can be obtained from this by simply omitting the auxiliary indices from the variables ra;i;D . Note that the refutation given in the proof of Thm. 18 is actually a Davis-Putnam refutation: It respects the following elimination order All of these are then resolved against two instances of (3), and we get the desired qi;j;c _ rc;i;D .

qd;j;a _ ra;d;D for 1 j d, 1 a n and D 2 fL; Rg.

resolve (5) and (11) to get

(15) Next we

we obtain

q1;1;a _ ra;1;D (16) for 1 a n and D 2 fL; Rg. Finally, from (6) and (12) qi+1;j;a _ qi+1;j +1;b _ qi;j;c _ ra;i+1;L _ rb;i+1;R _ rc;i;D

(17)

for 1 j i d, 1 a; b; c n and D 2 fL; Rg. Now we want to derive qi;j;a _ ra;i;D for every i; j 2 Pyrd , 1 a n and D 2 fL; Rg, by induction on i downward from d to 1. The induction base is just (15). For the inductive step, resolve (17) against the clauses

p1;1;1 : : : pn;n;n r1;d;L r1;d;R : : : rn;d;L rn;d;R q1;d;1 : : : q1;d;n : : : qd;d;1 : : : qd;d;n r1;d,1;L : : : rn;d,1;R q1;d,1;1 : : : qd,1;d,1;n

. . .

qi+1;j;a _ ra;i+1;L

and

qi+1;j +1;b _ rb;i+1;R ;

r1;1;L r1;1;R q1;1;1 : : : q1;1;n :

5. Lower bound for Davis-Putnam resolutions

Goerdt [14] gives a superpolynomial separation of DavisPutnam resolution from unrestricted resolution. The lower bound he gives is of the order n log log n . By applying his method to a modi?cation of the clauses Gen~; q p~ Col~;~, we can improve the separation to exponential. pr We modify the clauses Gen~; ~ in such a way as to pq make small Davis-Putnam resolution refutations impossible, while still allowing for small unrestricted resolutions. The lower bound is proved by a bottleneck counting argument similar to that used in [14], which is based on the original argument of [17]. Let d 8 be divisible by 4 and let n = d3, and choose a mapping : d d ! Pyrd such that no element from 2 column i is mapped to rows between i , 1 between i+1, i.e. if i; j = i0 ; j 0 , then i0 2 fi , 1; i; i + 1g, and such that = no two elements from the same column are mapped to the same position, i.e. if j1 6= j2, then i; j1 6= i; j2. Such mappings are easy to construct; note that we do not require to be injective. The set of clauses DPGen~; q is built from Gen~; ~ p~ pq by adding additional literals to some of the clauses (4) and d (6). The clauses (4) for 1 j d and a 2 are replaced by

A position i ; j every a 2 n . A mapping m

2 Pyrd with qi ;j ;a = 0 for

: Pyrd n fi ; j g ! n such that – every triangle is consistent with G , i.e. for every i; j 2 Pyrd,1 such that i ; j 2 fi; j; i + = 1; j; i + 1; j + 1g m i + 1; j; m i + 1; j + 1; m i; j is in G . – if i ; j 6= 1; 1, then m 1; 1; m 1; 1; n 2 G . – 1; 1; m d; j 2 G for every j such that d; j 6= i ; j . Then qi;j;m i;j = 1 and qi;j;b = 0 for all b 6= m i; j, for every i; j 6= i ; j .

A critical assignment satis?es all clauses from and all clauses from DPGen~; ~ except pq for a2 n qi ;j ;a .

Col~;~, p W r

Theorem 20 (Dag-like) Davis-Putnam resolution refutations of the clauses DPGen~; q Col~;~ have to be of p~ pr size

1 2 4 n 3 . 1

qi ;j ;b _ qd;j;a _ p1;1;a

0 0

(18)

for every b 2 n , where i0 ; j 0 = d; a. The clauses (6) for i; j 2 Pyrd,1 , a; b 2 n and 1 c d are replaced 2 by

qi ;j ;e _ qi+1;j;a _ qi+1;j +1;b _ qi;j;c _ pa;b;c

0 0

(19)

for every e 2 n , where i0 ; j 0 = i; c. All other clauses remain unchanged. Proposition 19 There are (dag-like) unrestricted resolution refutations of the clauses DPGen~; ~ Col~;~ of size pq pr nO1. Proof : First, from the clauses (18) and (3) derive the original clauses (4), and from (19) and (3) derive (6). Then apply the refutations from the proof of Theorem 15, which of course work for any values of n and d. De?nition: A critical assignment is given by

Proof : Let an elimination order hx1; : : : ; xN i be given, , where N = n3 + d+1 n + n is the number of vari2 ables, and a Davis-Putnam refutation R of DPGen~; ~ pq Col~;~ respecting this elimination order be given. For pr i; Pyrd and s N , let Si; j; s := j d 2 a 2 ; qi;j;a 2 fx1; : : : ; xsg . Let i0 ; j0 denote the unique position in Pyrd such that there is an index s0 N with jSi0 ; j0; s0 j = d , and for all i; j 6= i0 ; j0, 4 jSi; j; s0 j d . In other words, i0 ; j0 is the ?rst po4 sition in Pyrd for which d variables qi0;j0 ;a with a d 4 2 are eliminated. Let fa1 ; : : : ; a d g denote Si0 ; j0 ; s0. For 4 each 1 k d , let ik ; jk denote i0 ; ak , and de?ne 4 d Rk := 2 n Sik ; jk ; s0 , i.e. Rk is the set of those a d 2 for which qik;jk ;a is eliminated later than any qi0 ;j0;a` for d 1 ` d . Note that jRk j 4 by de?nition of i0 ; j0 4 and by the ?rst requirement for . A critical assignment is 0-critical if i ; j = i0 ; j0 and m ik ; jk 2 Rk , and furthermore the following conditions hold

col 2 2 n such that col 1 = 0 and col n = 1. The values ra are assigned according to col a. a set of triples G n 3 such that for no triple a; b; c 2 G , col a = col b = 0 and col c = 1. Values pa;b;c are assigned according to G .

a coloring

m i0 +1; j0; m i0 +1; j0 +1; ak 2 G if i0 6= d = or 1; 1; ak 2 G if i0 = d = if i0 ; j0 1, then m i0 ; j0 , 1; ak ; m i0 , 1; j0 , 1 2 G if i0 1 and j0 i0 , then ak ; m i0 ; j0 + 1; m i0 , 1; j0 2 G

for every 1 k d . 4 The next lemma shows that there are many 0-critical assignments. Lemma 21 For every choice of pairwise distinct values b1; : : : ; b 4 with bk 2 Rk , there is a 0-critical assignment d with m ik ; jk = bk for 1 k d . 4 Proof : The assignment 1. If i0 2. is constructed as follows: 0

J J Js

J J J 1 J

0

J J

0

J J J

d, then values m i0 +1; j0 = c1 and m i0 + 1; j0 + 1 = c2 are assigned with d c1; c2 d. 2 For each i; j 6= i0 ; j0 for which no value m i; j has been assigned yet, i.e. i; j 2 = fi1 ; j1; : : : ; i d ; j d ; i0 + 1; j0; i0 + 1; j0 + 1g, 4 4 assign a value n , id m i; j n , i , 1d, such

that no value is assigned twice.

J J

Figure 1. the black dot indicates

i0 ; j0

.

3. Put all triples occurring in the pyramid and those required by the de?nition of 0-critical into G , and no others, i.e. G contains the triple m 1; 1; m 1; 1; n, all triples 1; 1; m d; j for d; j 2 Pyrd n fi ; j g and all triples

4.

m i + 1; j; m i + 1; j + 1; m i; j such that fi; j; i + 1; j; i + 1; j + 1g Pyrd n fi ; j g, and for i0 1, all triples m i0 ; j0 , 1; ak; m i0 , 1; j0 , 1 if j0 1 and ak ; m i0 ; j0 + 1; m i0 , 1; j0 if j0 i0 . Color all elements in rows i ; : : : ; d by 0, and also all

elements that are thereby forced to have color 0 by the second clause in the de?nition of critical assignment, i.e. if a; b; c 2 G and a; b have already been colored 0, then also c is colored 0. Color all remaining elements by 1.

n fa1 ; : : : ; a d g and does not satisfy C . This 4 clause exists because determines a path through R from W 1an qi0 ;j0 ;a to the empty clause such that does not satisfy any clause on that path. The variables qi0;j0 ;a with a d are eliminated along that path, and qi ;j ;a ; : : :qi ;j ;a 0 0 1 0 0 d=4 2 are the ?rst among them in the elimination order. The following lemma shows that the clauses C have a certain complexity, which implies that the mapping 7! C does not map too many 0-critical assignments to the same clause.

Lemma 22 Let be a 0-critical assignment and bk := d m ik ; jk . Then for every 1 k 4 , the literal qik ;jk ;bk occurs in C . Proof : Let 0 be the assignment de?ned by 0qi0 ;j0 ;ak := 1 and 0x := x for all other variables x. As qi0;j0 ;ak does not occur in C , 0 does not satisfy C either. If i0 d, the only clause from DPGen~; q Col~;~ that is not p~ pr satis?ed by

d 2

0 is

qik ;jk ;bk _ qi0 +1;j0 ;c1 _ qi0+1;j0 +1;c2 _ qi0 ;j0 ;ak _ pc1 ;c2 ;ak

where c1 := m i0 + 1; j0 and c2 := m i0 + 1; j0 + 1. If i0 = d, then the only clause not satis?ed by 0 is

To verify that is 0-critical, observe that the only elements d appearing in the pyramid are the bk , so this is the only 2 way that the values ak can occur in the pyramid.. If i0 d, then as n = d3 d2 +d, the elements c1 ; c2 do not appear in the pyramid anywhere else but at i0 +1; j0; i0 +1; j0 +1, hence no triple c1; c2; ak gets put into G . If i0 = d, then ik 6= d for every k, so no triple 1; 1; ak gets put into G . The elements m i0 ; j0 , 1 and m i0 ; j0 + 1, if de?ned, cannot occur adjacent to any ak , and so the elements m i0 , 1; j0 , 1 and m i0 , 1; j0 are not forced to be colored 0, hence they get colored 1. Therefore everything that is above these positions in the pyramid gets colored 1 also, as indicated in Figure 1. In particular, if m 1; 1 is de?ned, it is colored 1, and thus n is colored 1. Hence is critical, and by the remarks above, 0-critical. Now we map 0-critical assignments to certain clauses in the proof. For a 0-critical assignment , let C be the ?rst d clause in R such that a 2 ; qi0;j0 ;a occurs in C =

qik;jk ;bk _ qi0;j0 ;ak _ p1;1;ak :

The ?rst item in the de?nition of 0-critical guarantees that these clauses are not satis?ed, and the other two make sure that the other possible candidates, i.e. instances of (6) or (19) with i0 ; j0 at the bottom of the triangle, are satis?ed. In both cases there is a path through R leading from the clause in question to C . The variable that is eliminated in the last inference on that path must be one of the qi0;j0 ;a` for 1 ` d . Since bk 2 Rk , the variable qik ;jk;bk is later in 4 the elimination order, so it cannot be eliminated on that path. Hence the literal qik;jk ;bk still occurs in C . Now let ; be two 0-critical assignments such that bk := m ik ; jk 6= m ik ; jk for some 1 k d , 4 so that qik ;jk ;bk = 0. By Lemma 22, the literal qik ;jk ;bk occurs in C , therefore satis?es C and hence C 6= C .

By Lemma 21, there are at least d ! distinct 0-critical as4 signments that differ in the values m ik ; jk . Thus R cond

1 1

d tains at least d ! 4e 4 = 2 4 n 3 different clauses of 4 the form C , which proves the theorem.

Acknoweldgements

We would like to thank R. Raz for reading a previous version of this work and discovering an error, A. Goerdt for sending us copies of his papers, S. Buss for helpful discussions and ?nally P. Clote for suggestions about resolution separations.

References

[1] M. Alekhnovich, S. R. Buss, S. Moran, and T. Pitassi. Minimum propositional proof length is NP-hard to linearly approximate. In MFCS ’98. Springer LNCS, 1998. [2] P. Beame, R. Impagliazzo, J. Kraj?cek, T. Pitassi, and ?ˇ P. Pudl? k. Lower bounds on Hilbert’s Nullstellensatz and a propositional proofs. Proceedings of the London Mathematical Society, 73:1–26, 1996. [3] P. Beame and T. Pitassi. Simpli?ed and improved resolution lower bounds. In Proc. 28th STOC, 1996. [4] E. Ben-Sasson and A. Wigderson. Resolution refutation size vs. width. Manuscript, 1998. [5] M. L. Bonet, C. Domingo, R. Gavalda, A. Maciel, and T. Pitassi. Non-automatizability of bounded-depth Frege proofs. Manuscript, 1998. [6] M. L. Bonet, T. Pitassi, and R. Raz. Lower bounds for cutting planes proofs with small coef?cients. Journal of Symbolic Logic, 62:708–728, 1997. Preliminary version in Proc. 27th STOC, 1995. [7] M. L. Bonet, T. Pitassi, and R. Raz. No feasible interpolation for TC 0 -Frege proofs. In Proc. 38th FOCS, pages 254–263, 1997. [8] V. Chv? tal and E. Szemer? di. Many hard examples for resoa e lution. Journal of the ACM, 35:759–768, 1988. [9] M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner basis algorithm to ?nd proofs of unsatis?ability. In Proc. 28th STOC, pages 174–183, 1996. [10] P. Clote and A. Setzer. On PHP , st-connectivity and odd charged graphs. In P. Beame and S. R. Buss, editors, Proof Complexity and Feasible Arithmetics, pages 93–117. AMS DIMACS Series Vol. 39, 1998. [11] S. Cook and A. Haken. An exponential lower bound for the size of monotone real circuits. To appear in J. Comp. System Sciences, 1998.

[12] S. A. Cook and R. A. Reckhow. The relative ef?ciency of propositional proof systems. Journal of Symbolic Logic, 44:36–50, 1979. [13] W. Cook, C. Coullard, and G. Tur? n. On the complexity of a cutting plane proofs. Discrete Applied Mathematics, 18:25– 38, 1987. [14] A. Goerdt. Davis-Putnam resolution versus unrestricted resolution. Annals of Mathematics and Arti?cial Intelligence, 6:169–184, 1992. [15] A. Goerdt. Unrestricted resolution versus N-resolution. Theoretical Computer Science, 93:159–167, 1992. [16] A. Goerdt. Regular resolution versus unrestricted resolution. SIAM Journal of Computing, 22:661–683, 1993. [17] A. Haken. The intractability of resolution. Theoretical Computer Science, 39:297–308, 1985. [18] R. Impagliazzo, T. Pitassi, and A. Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In Proc. 9th LICS, pages 220–228, 1994. [19] K. Iwama. Complexity of ?nding short resolution proofs. In MFCS ’97, pages 309–318. Springer LNCS 1295, 1997. [20] J. Johannsen. Lower bounds for monotone real circuit depth and formula size and tree-like cutting planes. Information Processing Letters, 67:37–41, 1998. [21] M. Karchmer and A. Wigderson. Monotone circuits for connectivity require super-logarithmic depth. SIAM Journal on Discrete Mathematics, 3:255–265, 1990. Preliminary version in Proc. 20th STOC, 1988. [22] J. Kraj?cek. Interpolation by a game. To appear in Math. ?ˇ Logic Quarterly, 1997. [23] J. Kraj?cek. Interpolation theorems, lower bounds for proof ?ˇ systems and independence results for bounded arithmetic. Journal of Symbolic Logic, 62:457–486, 1997. [24] J. Kraj?cek and P. Pudl? k. Some consequences of cryp?ˇ a 1 tographical conjectures for S2 and EF . Information and Computation, 140:82–94, 1998. Preliminary version in D. Leivant, ed., LCC ’94, Springer LNCS 960, 1995. [25] P. Pudl? k. Lower bounds for resolution and cutting plane a proofs and monotone computations. Journal of Symbolic Logic, 62:981–998, 1997. [26] R. Raz and P. McKenzie. Separation of the monotone NC hierarchy. In Proc. 38th FOCS, pages 234–243, 1997. [27] A. Rosenbloom. Monotone real circuits are more powerful than monotone boolean circuits. Information ProcessingLetters, 61:161–164, 1997. [28] U. Sch¨ ning. Logic for Computer Scientists. Birkh¨ user, o a 1989. [29] A. Urquhart. Hard examples for resolution. Journal of the ACM, 34:209–219, 1987. [30] A. Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic, 1:425–467, 1995.

赞助商链接

- Power law and exponential decay of inter contact times between mobile devices
- EXPANDED PROOF OF THE RELATION BETWEEN DESCRIPTION COMPLEXITY AND ALGORITHMIC PROBABILITY
- Equivalences and separations between quantum and classical learnability
- Bounded-error quantum state identification and exponential separations in communication com
- Discretely ordered modules as a first-order extension of the cutting planes proof system
- Proof by Induction Bridging the Gap between Proof Theory and Practical Automated Proof Syst
- On the relative complexity of resolution refinements and cutting planes proof systems
- Relationship between Cutting Parameters and Bit
- An exponential separation between regular and general resolution
- 2009 Human genetics of infectious diseases between proof of principle and paradigm
- Transmission-Line Properties of a Strip Line Between Parallel Planes
- Relationship between dynamical heterogeneities and stretched exponential relaxation
- Power law and exponential decay of inter contact times between mobile devices
- The Completeness of Propositional Resolution A Simple and Constructive Proof
- 05_292_Baraniuk_A simple proof of the restricted isometry property for random matrices

更多相关文章：
更多相关标签：