Printer Friendly

Short Proofs Are Narrow--Resolution Made Simple.

Abstract. The width of a Resolution proof is defined to be the maximal number of literals in any clause of the proof. In this paper, we relate proof width to proof length (=size), in both general Resolution, and its tree-like variant. The following consequences of these relations reveal width as a crucial "resource" of Resolution proofs.

In one direction, the relations allow us to give simple, unified proofs for almost all known exponential lower bounds on size of resolution proofs, as well as several interesting new ones. They all follow from width lower bounds, and we show how these follow from natural expansion property of clauses of the input tautology.

In the other direction, the width-size relations naturally suggest a simple dynamic programming procedure for automated theorem proving--one which simply searches for small width proofs. This relation guarantees that the running time (and thus the size of the produced proof) is at most quasi-polynomial in the smallest tree-like proof. This algorithm is never much worse than any of the recursive automated provers (such as DLL) used in practice. In contrast, we present a family of tautologies on which it is exponentially faster.

Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--proof theory; 1.2.3 [Artificial Intelligence]: Deduction and Theorem Proving

General Terms: Algorithms, Theory

1. Introduction

The central task of Proof-Complexity theory is to prove nontrivial lower bounds on the length (=size) of proofs, for nontrivial propositional proof-systems. This is done for three interrelated reasons.

(1) By the famous theorem of Cook and Reckhow [1979] NP = Co-NP iff there exists a propositional proof system, which can prove every tautology [Tau] in length polynomial in |[Tau]|. Thus, super-polynomial size lower bounds for stronger and stronger proof systems hopefully brings us somewhat closer to asserting NP [is not equal to] Co-NP.

(2) Automated Theorem Proving is essential for various aspects of (mainly practical) computer science. It is usually implemented with simple propositional proof systems. Discovering hard tautologies sheds light on the possibilities and usefulness of various Automated Theorem Proving techniques.

(3) Simple propositional systems are nonuniform analogs of natural fragments of Peano Arithmetic, most notably the various Bounded Arithmetic systems, which capture in some sense "polynomial time reasoning." Thus, lower bounds in the former yields independence results in the latter. Stunning evidence of Razborov [1995] and Razborov and Rudich [1994] show that the reasoning Complexity theory applied so far for proving circuit lower bounds lies within these fragments. Thus, such lower bounds may clarify the limits of our (human, rather than automated) proof techniques.

Despite some very recent impressive successes in proving super-polynomial lower bounds on a variety of propositional proof systems, it is probably fair to say that we are still far from understanding the reasoning power of very simple ones.

The Resolution proof system, which is the focus of this paper, is perhaps the simplest nontrivial one. All assertions in this proof system are clauses (namely disjunction of literals). A tautology is represented by its negation--as a set of contradicting clauses. (This is always possible by the NP-completeness of SAT.) The proof (or refutation) uses a simple deduction rule to generate more clauses from these "axioms clauses" until a contradiction is reached in the form of the empty (FALSE) clause. Resolution forms the basis of many automated theorem proving procedures used in practice.

Being so simple and fundamental, Resolution was a natural system to attack. However, proving size lower bounds even for it turned out to be very challenging. The first super-polynomial lower bounds were presented by Tseitin [1968]. Only 20 years later did the first exponential lower bounds appear, in the seminal work of Haken [1985]. Other examples soon followed [Urquhart 1987; Chvatal and Szemeredi 1988], based on Haken's method of proof. All of them seemed to require a significant array of technical tools and calculations (most notably, random restrictions). Very basic questions regarding Resolution are still open, and attempts to resolve them and simplify existing proofs are part of the current line of research (e.g., Razborov et al. [1997], Buss and Pitassi [1997], and Beame et al. [2000]).

The main message of this paper is that Resolution is best studied when we focus on width. Like size, width is a "resource" of proofs we may want to minimize. It is defined to be the number of literals in the largest clause of the proof.

The main observation of this paper is a relation between these two fundamental resources:

--If a contradiction [Tau] over n variables, has a tree-like refutation of size [S.sub.T], then it has a refutation of maximal width [log.sub.2] [S.sub.T].

--If [Tau] has a general resolution refutation of size S, then it has a refutation of maximal width O([square root of n log S]).

Both the notion of width and the relations above, gradually surfaced in previous papers and we merely make them explicit. Reading through the existing lower bound proofs, it is evident that wide clauses play a central role, with the following logic: If a Resolution proof is short, then random restrictions will "kill" all wide clauses with high probability. But a separate argument shows that they still have to exist even in refutations of the restricted tautology. Thus, the proof has to be long. This notion was originally made explicit by Galil [1977] that used linear lower bounds on width for proving exponential lower bounds on the Restricted Width algorithm described in Section 8.

Moreover, identical functional relations as those we obtain for width vs. size, appear in Clegg et al. [1996] between degree in Polynomial Calculus proofs, and size of Resolution proofs, and we simply observe that their argument actually applies to give these stronger relations. That paper, and the subsequent [Beame and Pitassi 1996], were the main inspiration for our work.

The first major application of our explicit width-size relations is significant simplification and unification of almost all known exponential lower bounds on Resolution proof length. Naturally, this understanding leads to new lower bounds as well. The main point is that now, to prove size lower bounds, it is sufficient to prove width lower bounds. It removes the need for random restrictions, and allows us to concentrate on the original tautology rather than restricted forms of it.

We develop a general strategy for proving width lower bounds, which follows Haken's original proof technique but for the above reason is now simple and clear. It reveals that large width is implied by certain natural expansion properties of the clauses (axioms) of the tautology in question. We show that in the classical examples of the Pigeonhole Principle, Tseitin graph tautologies, and random k-CNF's, these expansion properties are quite simple to prove (indeed, they comprised in some implicit way the simple part of the existing lower bound proofs).

We further illustrate the power of this approach by proving new exponential lower bounds to two different restricted versions of the pigeon-hole principle. One restriction allows the encoding of the principle to use arbitrarily many extension variables in a structured way (completely unstructured extension variables make the proof system as strong as Extended Frege, for which no lower bounds are known). The second restriction allows every pigeon to choose a hole from some constant size set of holes.

The second major application of our relations is in automatization results for the Resolution proof system. This is the basic problem faced in the analysis of automatic provers searching for a proof; how long will they run, as a function of the shortest existing proof of the input tautology.

The relations suggest the use of the following simple (dynamic programming) algorithm: Set i = 1. Start with the axioms, and try to derive all clauses of width at most i. If the empty clause is derived, we are done. If not, increase i by 1 and repeat.

This algorithm has been originally suggested and investigated by Galil [1977] who proved exponential lower bounds for natural inputs, using linear lower bounds on width.

Clearly, the running time on any tautology [Tau] over n variables is at most [n.sup.O(w)], when w is the minimal width of a proof of [Tau]. By the relations above, this time is at most [S.sub.T][([Tau]).sup.O(log n)] (namely, quasi-polynomial in the minimal tree-like Resolution proof length), and at most exp([square root of n log S([Tau]))] (namely, subexponential in the minimal general Resolution proof length). These bounds were already obtained by Beame and Pitassi [1996] who adopted the Clegg et al. [1996] algorithm from the Polynomial Calculus system to resolution.

Note that the relation to tree-like proofs is of particular importance, due to the fact that the most popular automated provers such as Davis et al. [1962] produce tree-like Resolution proofs. Thus, our algorithm never runs much longer than these provers on any tautology. Our final contribution, described below, is a new collection of natural tautologies, for which our algorithm is exponentially faster than such provers.

We give a construction which associates to every directed graph G on n edges a tautology [Tau](G) with the following properties.

(1) [Tau](G) has O(n) variables and O(n) clauses.

(2) [Tau](G) has general Resolution proofs of length O(n).

(3) [Tau](G) has Resolution proofs of width O(1).

(4) Every tree-like Resolution proof of [Tau](G) has length at least exp(P(G)), where P(G) is the classical pebbling number of the graph G.

The construction itself is motivated by a special case of it for the Pyramid graph of Bonet et al. [2000], which was in turn motivated by Raz and McKenzie [2000]. However, the simple adaptation of the pebbling bound into a tree-like Resolution lower bound for the Pyramid does not directly extend to arbitrary graphs, and we believe that the general connection in (4) is of independent interest. The proofs of the main claims are presented in Ben-Sasson et al. [2000].

At any rate, this construction allows us to use much harder graphs to pebble than Pyramids. Specifically, Celoni et al. [1977] explicitly construct for every n a graph [G.sub.n] of size O(n) satisfying P([G.sub.n]) = [Omega](n/log n). For these graphs, (4) implies exponential runtime for any tree-like automated prover, while (3) guarantees polynomial runtime for our dynamic programming algorithm, giving the desired exponential separation of the two automated proof search methods.

The paper is organized as follows: Section 3 states and proves the Size-Width relations. Section 4 summarizes the lower bounds on width for Tseitin formulas, random k-CNF's and the Pigeonhole Principle and its variants. Section 5 presents the general strategy for proving width lower bounds, and Section 6 applies the strategy to obtain the main results presented in Section 4. Section 7 discusses the tightness of the trade-off. Finally, Section 8 discusses the efficiency of the Automated Theorem Proving algorithm based on the Size-Width trade-off.

2. Definitions

2.1. GENERAL. x will denote a Boolean variable, ranging over {0, 1}. Throughout this paper we shall identify 1 with True and 0 with False. A literal over x is either x (denoted also as [x.sup.1]) or [bar]x (denoted also as [x.sup.0]). A clause is a disjunction of literals. We say that a variable x appears in C (denoted x [element of] C) if a literal over x appears in C. A CNF formula is a conjunction of clauses. Let F = {[C.sub.1], [C.sub.2] ... [C.sub.m]} be a CNF formula over n variables, a Resolution derivation [Pi] of a clause A from F is a sequence of clauses [Pi] = {[D.sub.1], [D.sub.2] ... [D.sub.S} such that the last clause is A and each line [D.sub.i] is either some initial clause [C.sub.j] [element of] F or is derived from the previous lines using one of the following derivation rules:

(1) The Resolution Rule:

E [disjunction] x F [disjunction] [bar]x/E [disjunction] F

(2) The Weakening Rule:

E/E [disjunction] F

where x [element of] {[x.sub.1], [x.sub.2], ..., [x.sub.n]} and E, F are arbitrary clauses. The Weakening Rule is not essential, as even without it the Resolution proof system is complete with respect to refutations, but we add it for the sake of simplicity. A resolution refutation is a resolution derivation of the empty clause 0. The graph [G.sub.[Pi]] of a derivation [Pi] is a DAG with the clauses of the derivation as nodes, and for derivation step edges are added from the assumption clauses to the consequence clause. A derivation [Pi] is called tree-like if [G.sub.[Pi]] is a tree; we may make copies of the original clauses in F in order to make a proof tree-like. The size of the derivation [Pi] is the number of lines (clauses) in it, denoted [S.sub.[Pi]]. S(F) ([S.sub.T](F)) is the minimal size of a (Tree-like) refutation of F.

2.2. RESTRICTIONS. For C a clause, x a variable and a [element of] {0, 1}, the restriction of x on a is:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Similarly, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. For [Pi] = {[C.sub.1], ... [C.sub.s]} a derivation of [C.sub.s] from F and a [element of] {0, 1}, let [Pi][|.sub.x=a] = {[C'.sub.1], ... [C'.sub.s]} be the restriction of [Pi] on x = a, defined inductively by:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The consequence of resolving a clause B with 1 is defined to be B. We shall assume without loss of generality that [Pi][|.sub.x=a] does not contain the clause 1, by removing all such clauses from [Pi][|.sub.x=a].

2.3. WIDTH. The width of a clause C, denoted w(C), is defined to be the number of literals appearing in it. The width of a set of clauses is the maximal width of a clause in the set, that is, w(F) = [max.sub.C [element of] F] {w(C)}. In most cases, input tautologies F will have w(F) = O(1).

The width of deriving a clause A from the formula F, denoted w(F [assertion sign] A) is defined by [min.sub.[Pi]{w([Pi])} where the minimum is taken over all derivations [Pi] of A from F. We also use the notation F [[assertion sign].sub.w] A to mean that A can be derived from F in width w. We will be mainly interested in the width of refutations, namely in w (F [assertion sign] 0).

3. The Size-Width Relations

The following lemmata and theorems are a direct translation of Clegg et al. [1996] to Resolution derivations. Stated informally, they say that if F has a short resolution refutation then it has a refutation with small width.

LEMMA 3.1. For a [element of] {0, 1}, if F[|.sub.x=a] [[assertion sign].sub.w] A then F [[assertion sign].sub.w+1] A [disconjunction] [x.sup.1-a].

PROOF. F[|.sub.x=a] is created from F by disposing of all initial clauses that include the literal [x.sup.a] and removing the literal [x.sup.1-a] from all other initial clauses where it appears. Let F' be the set of initial clauses containing the literal [x.sup.1-a], and let [Pi] be a width w derivation of A from [F.sub.x=a]. Add the literal [x.sup.1-a] to all clauses in [Pi] and call the new derivation [Pi]'. We claim that [Pi]' is a legal resolution derivation. If C [element of] F' then C [disconjunction] [x.sup.1-a] is an initial clause of F. If C [element of] F\F' then C [disconjunction] [x.sup.1-a] can be derived from C by a single weakening step. Finally, if C was derived from A, B via a resolution step, then C [disconjunction] [x.sup.1-a] is the resolution consequence of A [disconjunction] [x.sup.1-a], B [disconjunction] [x.sup.1-a]. It is easy to see that the width of each clause in [Pi]' is larger by 1 than the matching clause in [Pi]. []

LEMMA 3.2. For a [element of] {0, 1}, define [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] as the set of all clauses in F containing the literal [x.sup.a]. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF. According to Lemma 3.1, if F[|.sub.x=a] [[assertion sign].sub.k-1] 0, then F [[assertion sign].sub.k] [x.sup.1-a]. We now resolve the clause [x.sup.1-a] with all clauses in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and derive F[|.sub.x=1-a]. This part will have width [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Finally, by the assumption, we can refute F[|.sub.x=1-a] with width k. []

THEOREM 3.3. w(F [assertion sign] 0) [is less than or equal to] w(F) + log [S.sub.T](F).

PROOF. We prove by induction on b and n, the number of variables, that if [S.sub.T](F) [is less than or equal to] [2.sup.b] then w(F [assertion sign] 0) [is less than or equal to] w(F) + b. If b = 0, then 0 [element of] F, and we're done. Otherwise, the last derivation is

x [bar]x/0,

where x, [bar]x were derived by tree-like derivations [T.sub.x], [T.sub.[bar]x] of sizes [S.sub.x], [S.sub.[bar]x], respectively, and [S.sub.T] = [S.sub.x] + [S.sub.[bar]x] + 1. [T.sub.x][|.sub.x=0] ([T.sub.x][|.sub.x=1]) is a tree-like refutation of F[|.sub.x=0] (F[|.sub.x=1) of size at most [S.sub.x] ([S.sub.[bar]x]). Assume without loss of generality, [S.sub.x] [is less than or equal to] [2.sup.b-1]. By induction on b, w(F[|.sub.x=0] [assertion sign] 0) [is less than or equal to] w(F) + b - 1 and by induction on n, w(F[|.sub.x=1] [assertion sign] 0) [is less than or equal to] w(F) + b. Applying Lemma 3.2 completes the proof. []

COROLLARY 3.4. [S.sub.T](F) [is greater than or equal to] [2.sup.(w(F [assertion sign] 0)-w(F))]

THEOREM 3.5. w(F [assertion sign] 0) [is less than or equal to] w(F) + O([square root of n ln S(F))].

PROOF. Let [Pi] be a minimal size refutation of F, of size S. Let k = w(F). If S = 1, then 0 [element of] F, and we're done. Otherwise, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let [Pi]* be the set of fat clauses in [Pi], having width greater than d. We prove by induction on b and n, that if |[Pi]*| [is less than] [a.sup.b] then w(F [assertion sign] 0) [is less than or equal to] d + k + b. The base case (b = 0) is trivially true. For the induction step, there are 2n literals, so by the Pigeonhole Principle there is some literal (without loss of generality) x appearing in [is greater than or equal to] d/2n [multiplied by] |[Pi]*| fat clauses. Restricting x = 1 removes all the clauses in which x appears, and leaves us with a refutation of F[|.sub.x=1] with at most (1 - (d/2n)) [multiplied by] |[Pi]*| [is less than] [a.sup.b-1] fat clauses. F[|.sub.x=1] [[assertion sign].sub.d+k+b-1] 0, by induction on b, F[|.sub.x=0] [[assertion sign].sub.d+k+b] 0, by induction on n. Applying Lemma 3.2 completes the proof. []

COROLLARY 3.6.

S(F) = exp([Omega][(w(F [assertion sign] 0) - w(F)).sup.2]n

If w(F) ~ #Variables, Corollaries 3.4 and 3.6 are useless for obtaining lower bounds. This will not be a problem in practice, since all the formulas we shall consider, either have constant initial width (i.e., Tseitin formulas, random k-CNF's), or can be reduced to such formulas (i.e., the Pigeonhole Principle).

4. Results

Over the past 30 years, several exponential lower bounds on size have been obtained, for several different contradictions. We wish to provide new and simple lower bounds for most of these tautologies, and we organize this section as follows. We start each subsection with a definition of the contradiction, and discuss its initial size and width. This is followed by a lower bound on the width of the refutation. Exponential lower bounds on size of refutations, via Corollaries 3.4 and 3.6, conclude the discussion.

4.1. TSEITIN FORMULAS

4.1.1. Definition. A Tseitin contradiction is an unsatisfiable CNF capturing the basic combinatorial principle that for every graph, the sum of degrees of all vertices is even.

Definition 4.1 (Tseitin Formulas). Fix G a finite connected graph, with |V(G)| = n. f: V(G) [right arrow] {0, 1} is said to have odd-weight if [[Sigma].sub.v[element of]V(G)] f(v) [equivalent] 1 (mod 2). Denote by [d.sub.G](v) the degree of v in G (i.e., the number of edges incident with v). Fix f an odd-weight function. Assign a distinct variable [x.sub.e] to each edge e [element of] E(G). For v [element of] V(G), define [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (mod 2)). The Tseitin Contradiction of G and f is:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

If the maximal degree of G is constant, then the initial size and width of [Tau](G, f) is small as well:

LEMMA 4.2. If d is the maximal degree of G, then [Tau](G, f) is a d-CNF with at most n [multiplied by] [2.sup.d-1] clauses, and nd/2 variables.

4.1.2. Width Lower Bound. The width of refuting [Tau](G, f) is bounded from below by the expansion of the graph G, hereby defined.

Definition 4.3 (Expansion). For G a finite connected graph, the Expansion of G is

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The main claim of this section is (for a proof, see Section 6.1):

THEOREM 4.4. For G a connected graph and f an odd-weight function on V(G), w([Tau](G,f) [assertion sign] 0) [is greater than or equal to] e(G).

COROLLARY 4.5 [URQUHART 1987]. For G a 3-regular connected Expander (i.e., e(G) = [Omega](|V|)), and f an odd-weight function on V(G), S([Tau](G,f)) = [2.sup.[Omega](|[Tau](G,f)|).

4.2. THE PIGEONHOLE PRINCIPLE

4.2.1. Definition. The Pigeonhole Principle with m pigeons and n pigeonholes, states that there is no 1-1 map from m to n, as long as m [is greater than] n. This can be stated by a formula on n [multiplied by] m variables [x.sub.ij], 1 [is less than or equal to] i [is less than or equal to] m, 1 [is less than or equal to] j [is less than or equal to] n, where [x.sub.ij] = 1 means that i is mapped to j.

Definition 4.6 [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the conjunction of the following set of clauses:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Whenever m [is greater than] n, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an unsatisfiable CNF with m [multiplied by] n [is greater than] [n.sup.2] variables, O([m.sup.2]) Clauses and initial width n.

The large initial width of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and its large number of variables does not allow the derivation of size lower bounds directly from width lower bounds. In the next two subsections, we generalize these pigeonhole tautologies in two different ways--the first reducing the width using extension variables, and the second reducing the number of variables but fixing most of them. The lower bounds for both are new and of independent interest.

4.2.2. Width Lower Bound for Tree-Like Resolution. It is easy to check that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. This means that using the standard formulation of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] one cannot achieve a lower bound on size via the Size-Width trade-off. Therefore, we shall need to reduce [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to a constant width analog, and prove [Omega](n) lower bounds on width for this formulation.

Definition 4.7 ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]). For f(x) a Boolean function, a Nondeterministic Extension of f is a function g(x, y) such that f(x) = 1 iff [exists]yg(x, y) = 1. The x variables are called Original variables, and the y are called Extension variables.

A Row-Extension of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], denoted [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is derived by replacing every row axiom [P.sub.i] with some nondeterministic extension CNF formula [EP.sub.i], using distinct extension variables [y.sub.i] for distinct rows.

One standard extension is:

Example 4.8. Replace every [P.sub.i] with the following 3-CNF over n + 2 clauses and 2n + 1 variables:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The main claim of this section is (for a proof of the following theorem and Corollary 4.10, see Section 6.2):

THEOREM 4.9. For m [is greater than or equal to] n, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

COROLLARY 4.10. For all m [is greater than] n and any Row Extension of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

As [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a legitimate Row Extension of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we get:

COROLLARY 4.11 [BUSS AND PITASSI 1997]. For all m [is greater than] n, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

4.2.3. Width Lower Bound for General Resolution. The number of variables of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is quadratic in the width of its refutation. Hence, in order to apply Corollary 3.6 and derive exponential lower bounds on size for general resolution, we shall need the following generalization, which restricts [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by limiting the number of holes into which a pigeon may enter. This will decrease the number of underlying variables, while leaving the width lower bound in place.

Definition 4.12 (G - PHP). Let G = ((V ?? U), E) be a bipartite graph, |V| = m, |U| = n. Assign each edge a distinct variable [x.sub.e]. G - PHP is the conjunction of the following clauses:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

G - PHP is a natural generalization of the Pigeonhole Principle, because [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. This generalization will prove useful by the following observation, presented here without a proof:

LEMMA 4.13. For any two bipartite graphs G, G' over the same vertex set, if E(G') [subset or equal to] E(G), then S(G' - PHP) [is less than or equal to] S(G - PHP).

The width of refuting G - PHP is bounded from below by the expansion of G, for the following bipartite version of expansion (we define it already with the parameters that will yield linear width, but this can be generalized):

Definition 4.14 (Bipartite Expansion). For a vertex u [element of] U, let N(u) be its set of neighbors. For a subset V' [subset] V let its boundary be

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In words, the boundary of V' is the set of vertices in U that have exactly one neighbor in V'.

We call a bipartite graph G an (m, n, d, r, e)-expander if |V| = m, |U| = n, the degree of vertices in V is at most d, and for all V' [subset] V, |V'| [is less than or equal to] r |[differential]V'| [is greater than or equal to] e|V'| (in words: every small set has large boundary).

The main theorem of this section is (for a proof, see Section 6.2):

THEOREM 4.15. For every bipartite graph G that is an (m, n, d, r, e)-expander, w(G - PHP [assertion sign] 0) [is greater than or equal to] (r [multiplied by] e)/2.

For m = n + 1, a simple union bound calculation shows that there exist bipartite graphs which are (m, n, 5, n/c, 1)-expanders, for some constant c [is greater than] 1, yielding:

COROLLARY 4.16 [HAKEN 1985]. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The best-known lower bound for the Weak Pigeonhole Principle (i.e., when m is much larger than n) is [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [Buss and Turan 1988]. When m [much greater than] n, the same simple calculation shows that there exists a (m, n, log m, [Omega](n/log m), 3/4 log m)-expander, yielding a slightly less than optimal lower bound:

COROLLARY 4.17 [BUSS AND TURAN 1988]. [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

4.3. RANDOM k-CNF's

4.3.1. Definition. We start with a formal definition of a random k-CNF:

Definition 4.18 (Random k-CNF's). Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] a denote that F is a random k-CNF formula on n variables and m = [Delta] [multiplied by] n clauses, chosen at random by picking [Delta] [multiplied by] n clauses i.i.d from the set of all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] clauses, with repetitions. [Delta] is called the clause density.

In their seminal paper, Chvatal and Szemeredi [1988] showed that for k [is greater than or equal to] 3 whp a random k-CNF formula with constant clause density [Delta] [is greater than or equal to] ln 2 [multiplied by] [2.sup.k], is unsatisfiable and requires an exponential length refutation.

4.3.2. Width Lower Bounds. For the sake of simplicity, we shall work only with k = 3, and these bounds can be easily extended to any fixed k (see, e.g., Beame et al. [2000]). The following is proven by use of a straightforward Union bound (for a proof, see Section 6.3):

THEOREM 4.19. For any 0 [is less than or equal to] [Epsilon] [is less than or equal to] 1/2, if [Delta] = [n.sup.(1/2)-[Epsilon]] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then whp

w(F [assertion sign] 0) = [Omega]([[Delta].sup.-2/(1 - [Epsilon]]) [multiplied by] n).

Using this width lower bound, we easily obtain the best currently known lower bounds on size:

COROLLARY 4.20 [BEAME ET AL. 2000]. For any 0 [is less than or equal to] [Epsilon] [is less than or equal to] 1/2, if [Delta] = [n.sup.(1/2)-[Epsilon]] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then whp

S(F) = exp([Omega]([[Delta].sup.-4/(1 - [Epsilon]]) [multiplied by] n)).

5. Proof Strategy

All lower bounds on width follow the same strategy:

(1) Define a complexity measure [Mu]: {Clauses} [right arrow] N such that [Mu](Axiom) [is less than or equal to] 1.

(2) Prove [Mu](0) is large.

(3) Infer that in any refutation there is some clause C with medium size [Mu](C).

(4) Prove that if [Mu](C) is medium, then w(C) is large.

We shall now formalize and explain this strategy. First, we will define a measure that will satisfy conditions (1)-(3).

Definition 5.1. ([[Mu].sub.A]) for f a Boolean function, let Vars(f) denote the set of variables appearing in f. Let [Alpha] [element of] [{0, 1}.sup.Vars(f)] be an assignment to f. We say that [Alpha] satisfies f, if f([Alpha]) = 1. For C a clause and [Gamma] a set of Boolean functions, let V = Vars([Gamma]) [union] Vars(C). We say that [Gamma] implies C, denoted [Gamma] [satisfies] C, if every assignment satisfying every function [Gamma] [element of] [Gamma] satisfies C as well.

Let A be an unsatisfiable set of Boolean functions, that is, A [satisfies] 0, and let C be a clause.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

[[Mu].sub.A] is a subadditive complexity measure with respect to resolution steps:

LEMMA 5.2. Suppose D was inferred from B, C by a single resolution step. Then for any set of Boolean functions A:

[[Mu].sub.A] (D) [is less than or equal to] [[Mu].sub.A] (B) + [[Mu].sub.A](C).

In order to assure Condition 1 of the strategy, we want [Mu](Axiom) to be small:

Definition 5.3 (Compatibility). For F a nonsatisfiable CNF we say that A is compatible with F if A [satisfies] 0 and [inverted] AC [element of] F [Mu](C) [is less than or equal to] 1.

We will always pick a compatible A and use it to define [Mu] = [[Mu].sub.A]. Note that part 2 of the strategy puts another requirement on A, namely that no "small" subset of it is contradictory. However, this would be intuitively easy to achieve with "hard" tautologies.

We now claim that part 3 is deduced from the definitions:

LEMMA 5.4. If A is compatible with F, then in every refutation of F there must be a clause C with

[Mu](0)/3 [is less than or equal to] [Mu] (C) [is less than or equal to] 2[Mu](0)/3.

The rest of the section is devoted to proving the connection between Condition 4 and the expansion properties of a set of sensitive functions which is compatible with the input formula:

Definition 5.5 (Sensitivity). A Boolean function f is called Sensitive if any two distinct falsifying assignments [Alpha], [Beta] [element of] [f.sup.-1] (0), have Hamming distance greater than 1. Examples of Sensitive functions are PARITY and OR.

For A a set of Boolean functions, and f [element of] A, a Critical Assignment for f is an assignment [Alpha] [element of] [{0, 1}.sup.Vars(A)] such that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

For [Alpha], [Beta] [element of] [{0, 1}.sup.Vars(A)], we say that [Beta] is the result of flipping [Alpha] on the variable x, if

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We shall define the expansion of a CNF formula in terms of its minimal boundary:

Definition 5.6 (Boundary). For f a Boolean function and x a variable, we say that f is dependent on x if there is some assignment [Alpha] such that f([Alpha]) = 0, but flipping [Alpha] on x satisfies f.

For A set of Boolean functions, the Boundary of A, denoted [differential]A, is the set of variables x such that there is a unique function f [element of] A that is dependent on x.

A critical assignment to a sensitive function can be easily changed to a satisfying assignment, by flipping a boundary variable. Formally:

LEMMA 5.7. If f [element of] A is Sensitive, [Alpha] is a Critical Assignment for f, and x [element of] Vars(f) [intersection] [differential]A, then flipping [Alpha] on x yields an assignment [Beta] that satisfies A.

We define the expansion of F to be the minimal boundary of a medium size subformula of F:

Definition 5.8 (Expansion). For A [satisfies] 0, let k = [[Mu].sub.A](0). Define the Expansion of A to be:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The main tool, used in proving most lower bounds on width, presents the connection between width and expansion:

THEOREM 5.9. For F an unsatisfiable CNF,

w(F [assertion sign] 0) [is greater than or equal to] max e(A),

where the maximum is taken over all sets A of sensitive functions, compatible with F.

PROOF. Fix some A that is compatible with F, and let [[Mu].sub.A](0) = k. By Lemma 5.4, there must exist some clause C such that k/3 [is less than or equal to] [[Mu].sub.A](C) [is less than or equal to] 2k/3. Let A' [subset] A be a minimal set such that A' [satisfies] C. We claim that any variable x [element of] [differential]A' must appear in C. To see this, notice that, for every f [element of] A', there is some assignment [[Alpha].sub.f] such that [[Alpha].sub.f](C) = [[Alpha].sub.f](f) = 0 and [[Alpha].sub.f](g) = 1 for all g [element of] A' g [is not equal to] f. This follows from the minimality of A', for otherwise A'\f [satisfies] C. Suppose, for the sake of contradiction, that x [element of] [differential]A [intersection] Vars(f) but x [element of] C. By Lemma 5.7, flipping [Alpha] on x satisfies A', but the new assignment agrees with [Alpha] on Vars(C). Hence, A' ?? C, contradiction. []

6. Proof of Main Results

6.1. TSEITIN FORMULAS. We start with a proof of Theorem 4.4, to illustrate the simplicity of the strategy. We shall need the following lemma from Urquhart [1995]:

LEMMA 6.1 [URQUHART 1995]. If G is connected, then [Tau](G, f) is contradictory iff f is an odd weight function.

PROOF (THEOREM 4.4). We use the notation of Section 5. Set [A.sub.V] = {[PARITY.sub.v]:v [element of] V(G)} and denote [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Every axiom C is one of the defining axioms of [PARITY.sub.v]. Clearly, for this very same v [PARITY.sub.v] [satisfies] C. Hence for any axiom C, [Mu](C) = 1. So far we have shown that [A.sub.v] is compatible for [Tau](G, f). Next we claim that [Mu](0) = |V(G)|, because for any |V'| [is less than] |V(G)| [A.sub.V]' is satisfiable. This latter claim is seen by the following reasoning: Let v be some vertex in V\V'. Look at the formula [Tau](G, f') for

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

By Lemma 6.1, [Tau](G, f') is satisfiable, [A.sub.V'], is a subformula of [Tau](G, f'), and hence satisfiable as well. [A.sub.V(G)] is a collection of PARITY functions, which are Sensitive. Finally, for V' [subset or equal to] V, [differential][A.sub.V'] = {[x.sub.e]:e [element of] E(V', V\V')}. This is true because, if e = (v, u), v [element of] V', u [element of] V\V', then [PARITY.sub.v] is the only function of [A.sub.V'] dependent on [x.sub.e]. Hence, e([A.sub.V]) [is greater than or equal to] e(G) and we apply Theorem 5.9 to complete the proof. []

6.2. THE PIGEONHOLE PRINCIPLE. In this section, we give the proofs of the main results regarding the Pigeonhole Principle, that is, Theorem 4.9, Corollary 4.10, and Theorem 4.15.

PROOF (THEOREM 4.9). The proof follows the strategy presented in Section 5, and we shall use the same notation, but the notion of Boundary has to be altered slightly. Define A = {[A.sub.i]: 1 [is less than or equal to] i [is less than or equal to] m} where [A.sub.i] is the conjunction of [EP.sub.i] and all hole axioms [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let us denote [A.sub.I] = [[conjunction].sub.i [element of] I] [A.sub.i]. Set [Mu](C) = [[Mu].sub.A](C).

Clearly, [Mu](Axiom) [is less than or equal to] 1, [Mu](0) = n + 1, and [Mu] is subadditive. Hence, in every refutation [Pi] there must be a clause C with n/3 [is less than or equal to] [Mu](C) [is less than] 2n/3. Fix such a C and fix a minimal I [subset] [m] such that [A.sub.I] [satisfies] C. Let R(C) the set of rows who have a literal in C.

If |C| [is greater than or equal to] n/3, we are done. Otherwise, there must be some i [element of] I\R(C). Take any assignment [Alpha] such that [A.sub.I\i]([Alpha]) = 1, [A.sub.i]([Alpha]) = C([Alpha]) = 0, which must exist by the minimality of I. Without loss of generality, a sets all variables outside R(C) [union] I\i to 0. By the definition of the [A.sub.k]'s the 1's of original variables in [Alpha] must be a partial matching. But as |C| [is less than] n/3 and |I| [is less than or equal to] 2n/3, there must be a column j in which no original variable is set to 1. Flip the assignment a to set [x.sub.ij] to 1, and extend the nondeterministic variables [y.sub.i] in any way to set [EP.sub.i] to 1. Call this new assignment [Beta]. It is easy to verify that [A.sub.I]([Beta]) = 1, C([Beta]) = 0, contradiction. []

PROOF (COROLLARY 4.10). If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we apply Corollary 3.4. If this is not the case, one can replace every clause with a nondeterministic 3-CNF extension, in the manner described in Example 4.8. Call this new formulation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. It is easy to verify that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is still a legal Row Extension of the Pigeonhole Principle. It is also easy to verify that if [Tau] is the nondeterministic extension of a clause C, derived as described in 4.8, one can derive C from [Tau] in (C) tree like resolution steps. Hence, the exponential lower bound for treelike refutations of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] carries over to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. []

PROOF (THEOREM 4.15). Similar to the previous proof of Theorem 4.9. Define A = {[A.sub.v]:v [element of] V with [A.sub.v] as the conjunction of [P.sub.v] and all hole axioms [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let us denote [A.sub.V'] = [[conjunction].sub.v [element of] V]', [A.sub.v]. Set [Mu](C) = [[Mu].sub.A](C).

Again, [Mu](Axiom) [is less than or equal to] 1, [Mu](0) = r (because every V' of size |V'| [is less than or equal to] r has a matching into U), and [Mu] is subadditive. Hence, in every refutation [Pi] there must be a clause C with r/2 [is less than or equal to] [Mu](C) [is less than] r. Fix such a C and fix a minimal V' [subset] V such that [A.sub.V]' [satisfies] C.

We claim that for each u [element of] [differential]V', there must appear in C some variable [x.sub.(v,u)], for some v [element of] V (but not necessarily in V'). Indeed, for such a boundary u, let v be its only neighbor in V'. Assume for the sake of contradiction that C has no variable [x.sub.(v,u)]. Let a be the assignment satisfying [A.sub.V'\{v}] and falsifying [A.sub.v] and C. Clearly [Alpha] assigns zero to [x.sub.v,u]. We assume without loss of generality that [Alpha] sets to zero all variables [x.sub.(v,u)], because this cannot falsify any axiom [P.sub.v'], for v' [element of] V' (recall that [x.sub.(v, u)] is a boundary variable). Thus, we may flip [Alpha] on [x.sub.(v, u)], and get an assignment satisfying [A.sub.V'], without changing the value of C (zero), contradiction. Hence, the width of C is at least the size of its boundary, and the theorem is proven. []

6.3. RANDOM k-CNF's. In this section, we prove Theorem 4.19. In order to prove lower bounds on width of refuting a random formula F, it is enough to look at the expansion properties of the following hypergraph. The vertex set is the set of variables, and each clause defines an edge. Formally:

Definition 6.2. For F a 3-CNF formula on n variables and m clauses, let [H.sub.F] denote the 3-uniform hypergraph on n vertices and m = [Delta] [multiplied by] n edges defined by

V([H.sub.F]) = {1, 2, ..., n}

E([H.sub.F]) = {([i.sub.1], [i.sub.2], [i.sub.3]) [exists]C [element of] F such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

For any subset V' of vertices, let E(V') denote the set of edges within V' (i.e., for any e [element of] E(V'), all 3 vertices are in V'), and similarly for any subset E' of edges, let V(E') denote the set of vertices covered by E'.

We shall need a generalized definition of expansion, suited for hypergraphs. We do not attempt to optimize constants.

Definition 6.3 (Hypergraph Expansion). For H a 3-uniform hypergraph, with [Delta]n edges, where [Delta] = [n.sup.1/2-[Epsilon]], 0 [is less than or equal to] [Epsilon] [is less than or equal to] 1/2, the expansion of H is

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Positive expansion by itself is not enough to ensure high refutation width, and we need to be sure that F does not include a "small" unsatisfiable subformula. For this, we need the following definition.

Definition 6.4 (Partial Matchability). H, a 3-uniform Hypergraph, with [Delta]n edges, where [Delta] = [n.sup.1/2-[Epsilon]], 0 [is less than or equal to] [Epsilon] [is less than or equal to] 1/2, is called Partially matchable if [inverted] AE' [subset] E such that |E'| [is less than or equal to] 2n [multiplied by] [(80[Delta]).sup.-2/(1-[Epsilon])] we have |V(E')| [is greater than or equal to] |E'|.

The main theorem of this section states that if [H.sub.F] is partially matchable, then the expansion bounds the width from below:

THEOREM 6.5. For an unsatisfiable 3-CNF, such that [H.sub.F] is partially matchable: w(F [assertion sign] 0) [is greater than or equal to] e([H.sub.F]).

PROOF. We use the notation of Section 5. Set A to be F and let [Mu] = [[Mu].sub.A]. Clearly [Mu](Axiom) = 1. Thus, F is a set of sensitive functions, compatible with F. By the matchability of [H.sub.F], [Mu](0) [is greater than or equal to] 2n [multiplied by] [(80[Delta]).sup.-2/(1-[Epsilon])], since we can find a matching from every small size subformula F' [subset] F, |F'| [is less than or equal to] 2n [multiplied by] [(80[Delta]).sup.-2/(1-[Epsilon])] into Vars(F'), and use this matching to find an assignment satisfying F'. Finally, |[differential]F'| [is greater than or equal to] 2|V(E')|-3|E'|, where E' = E([H.sub.F']), because every variable (vertex) outside the boundary of F' (E') must be covered by at least 2 clauses (hyperedges), so |V(E')| [is less than or equal to] |[differential]F'| + 1/2(3|E'| - |[differential]F'|). Applying Theorem 5.9 completes the proof. []

Thus, we have reduced Theorem 4.19 to proving high expansion and partial matchability of the underlying hypergraph. For the proper clause density, a random F conforms to the conditions of the previous theorem, and the following lemma, which states this explicitly, completes the proof of Theorem 4.19. This lemma was originally proved by Beame et al. [2000]. The proof uses a simple union bound calculation, and is presented in the appendix, for the sake of completeness.

LEMMA 6.6 [BEAME ET AL. 2000]. For every 0 [is less than or equal to] [Epsilon] [is less than or equal to] 1/2, if [Delta] = [n.sup.(1/2)-[Epsilon]] and H is a random 3-uniform hypergraph on n vertices and [Delta]n edges, then whp:

(1) e(H) [is greater than or equal to] [Epsilon]n [(80[Delta]).sup.-2/(1-[Epsilon])].

(2) H is partially matchable.

7. Tightness of the Bounds

7.1. TIGHTNESS FOR TREE-LIKE RESOLUTION. How large can be the gap between [S.sub.T]([Tau]) and w([Tau] [assertion sign] 0)?

Our answer is that the gap can be very large. Specifically, we shall show a family of tautologies that can be refuted in constant width, but for which the minimal tree-like refutation has size that is exponential in the input size. This family of contradictions, which is a generalization of Raz and McKenzie [1999] and Bonet et al. [1998], is presented in the following definition. For these contradictions, we prove a connection between pebbling and tree-like Resolution size, and they provide us with an exponential gap between general Resolution and tree-like Resolution (Corollary 7.4).

Definition 7.1. A circuit G is a DAG with a single target, in which each vertex has fan-in 2 or 0. A vertex with fan-in 0 is called a source and a vertex with fan-out 0 is called a target. Associate a pair of Boolean variables x[(v).sub.0], x[(v).sub.1] with every vertex v [element of] V(G). [Peb.sub.G], the Pebbling Contradiction of G is the conjunction of:

Source Axioms: x[(s).sub.0] [disjunction] x[(s).sub.1] for s a Source vertex.

Target Axioms: [bar]x[(t).sub.0] [conjunction] [bar]x[(t).sub.1] for t a Target (Two singleton clauses per target vertex).

Pebbling Axioms: (x[([u.sub.1]).sub.a]) [conjunction] x[([u.sub.2]).sub.b]) [right arrow] (x[(v).sub.0] [disjunction] x[(v).sub.1]) for [u.sub.1], [u.sub.2] the sons of v, and all a, b [element of] {0, 1}.

Notice that Peb(G) is a nonsatisfiable 4-CNF over 2|V| variables, with O(|V|) clauses.

For G a circuit, let P(G) be the pebbling measure of G, which is the minimal space needed to carry out the calculation of the circuit G, assuming the output of each node requires one memory cell. For a thorough survey of pebbling see Pippenger Pebbling [1980].

All proofs of the following claims appear in Ben-Sasson et al. [2000].

LEMMA 7.2. For G a circuit, S([Peb.sub.G]) = O(|V|) and w([Peb.sub.G] [assertion sign] 0) [is less than or equal to] 6.

THEOREM 7.3. [S.sub.D]([Peb.sub.G]) = [2.sup.[Omega](P(G))].

Celoni et al. [1977] present for every n explicit constructions of [G.sub.n] with |V(G)| = O(n) and P(G) = [Omega](n/log n). The Pebbling contradictions of these graphs provide the best-known separation between treelike and general Resolution, improving the recent exp([square root of n])-separation of Bonet et al. [1998].

COROLLARY 7.4. For all large enough n, there exist formulas [F.sub.n] of size [F.sub.n] = n, such that S([F.sub.n]) = O(n), and w([F.sub.n] [assertion sign] 0) = O(1), but [S.sub.T]([F.sub.n]) = [2.sup.[Omega](n/log n)].

7.2. TIGHTNESS FOR GENERAL RESOLUTION. Recently, it has been shown by Bonet and Galesi [1999] that the trade-off of Theorem 3.5 is as tight as one can hope for. Specifically, Bonet and Galesi [1999] present a natural family of graph-based k-CNF contradictions (k is constant), [[Tau].sub.n], for which S([[Tau].sub.n]) = [n.sup.O(1)], but w([[Tau].sub.n] [assertion sign] O) = [Omega]([square root of n]).

8. Automated Theorem Proving

One of the most extensively used and investigated methods for proving unsatisfiability of CNF formulas, are commonly called Davis-Putnam procedures. Actually, these procedures are derived from a system devised by Davis, Logemann and Loveland [1962], and hence we will refer to them as DLL Procedures. A DLL procedure relies on choosing a variable x, and trying to refute F[|.sub.x=T] and F[|.sub.x=F] recursively. If F is unsatisfiable, DLL(F) terminates providing a tree-like resolution refutation of F.

An immediate consequence of the Size-Width trade-off is a different procedure for refuting unsatisfiable formulas. This Algorithm is a known heuristic in the AI community. Galil [1977] investigated this algorithm, and used linear width lower bounds for proving its inefficiency for Tseitin formulas. Recently, this algorithm was suggested in Beame and Pitassi [1996], based on the Groebner Basis (GB) algorithm [Clegg et al. 1996]. The essence of this procedure is seeking a minimal width refutation, and can be described schematically by the following algorithm:
A (F)
Fix w = 0
Repeat {
       f 0 [element of] F end
       End {
           Increase w
           Derive all resolution consequences of width
            [is less than or equal to] w
           }
       }


Algorithm A has running time bounded by [n.sup.O(w(F [assertion sign] 0]))], as this is the maximal number of different clauses that will be encountered. For example, if F has a polysize treelike refutation, then RunTime(A (F)) = [|F|.sup.O(log|F|)]. Moreover, the previous section (Corollary 7.4) provides concrete examples for tautologies where Algorithm A exponentially outperforms DLL procedures:

THEOREM 8.1. There exist unsatisfiable formulas such that Time(DLL(F)) is exponentially larger than Time(B(F)).

PROOF. We use the notation of Section 7.1. Take F = Peb(G) for G with P(G) = |V|/log|V|. By Lemma 7.2, RunTime(A(F)) = [|V|.sup.O(1)] = [|F|.sup.O(1)], while by Theorem 7.3 any tree-like refutation of F, for example, a DLL procedure, must have RunTime = [2.sup.[Omega](|F|/log|F|)]. []

9. Open Problems

9.1. Is RESOLUTION AUTOMATIZABLE? A proof system P is called Automatizable if there exists an algorithm [A.sub.P], which, when presented with a tautology (contradiction) F, produces a proof (refutation) [Pi] of F in the system P and the running time of [A.sub.P] is polynomial in the size of the minimal proof of A in P, that is, Time([A.sub.P](F)) [is less than or equal to] [([S.sub.P](F)).sup.O(1)]. Similarly, P is called Quasi-Automatizable if the running time of the above mentioned [A.sub.P] is Quasi-Polynomial in the size of the minimal proof, that is, Time([A.sub.P](F)) [is less than or equal to] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The algorithm of the previous section shows finds a Resolution proof in time quasi-polynomial in the size of the smallest Tree-like Resolution proof. The following questions remain open:

Is General Resolution Automatizable? Quasi-Automatizable? Is Tree-like Resolution Automatizable? Quasi-Automatizable?

9.2. IMPROVING THE LOWER BOUND FOR RANDOM k-CNF's. The present lower bounds for random k-CNF's in Beame et al. [2000] follow from a lower bound on the Boundary size for random k-Uniform Hypergraphs. This is obtained via the Union bound. One possible method for improving the lower bound on size of refutations of random formulas would be to replace this Union bound with a finer analysis of the probability of a random hypergraph having a small boundary.

Appendix A

PROOF [LEMMA 6.6]. The proof of the lemma, originally presented by Beame et al. [2000], is done by calculating a simple Union bound. We start by proving part (1). For a subset of edges E' [subset or equal to] E, let the expansion constant of E' be

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In order to prove that whp e(H) [is greater than or equal to] [Epsilon]n [(80[Delta]).sup.-2/(1-[Epsilon])], it is enough to show that whp

min{[e.sub.E']: E' [subset] E, n[(80[Delta]).sup.-2/(1 - [Epsilon]) [is less than or equal to] |E'| [is less than or equal to] 2n [(80[Delta]).sup.-2/(1 - [Epsilon])} [is greater than or equal to] [Epsilon].

Let [A.sub.i] denote the event that a set of edges of size i has an expansion constant of less than [Epsilon], that is,

|V(E')| [is less than] 3 + [Epsilon]/2 [multiplied by] |E'|.

Denote.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

and

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We wish to bound the probability that |V(E')| [is less than] [Lambda]|E'|, for any edge set of size i, where i = k ... 2k. This is done by summing over all possible edge sets--there are ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) such sets, and all possible small vertex sets--there are ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) such sets, the probability that all edges fall in this small vertex set. The probability for a single edge to fall within the small vertex set is

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(because [Lambda]i [is less than] n), and this must happen i times independently. Thus, we get

(1) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Using the standard estimation

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

we get

(2) Pr[[A.sub.i]] [is less than or equal to] [(e[Delta]n/i).sup.i] [(en/[Lambda]i).sup.[Lambda]i] [([Lambda]i/n).sup.3i]

(3) [is less than or equal to] [[e.sup.1+[Lambda]] [multiplied by] [[Lambda].sup.3-[Lambda]] [multiplied by] [Delta] [multiplied by] [(i/n).sup.2-[Lambda]].sup.i].

Notice that since 0 [is less than] [Epsilon] [is less than or equal to] 1/2, we get [e.sup.1+[Lambda]] [multiplied by] [[Lambda].sup.3-[Lambda]] [is less than] 20. Using the definition [Delta] = [n.sup.(1/2)-[element of]], we derive

(4) Pr[[A.sub.i]] [is less than or equal to] [[20 [multiplied by] [Delta] [(i/n).sup.(1-[Epsilon])/2]].sup.i]

(5) [is less than or equal to] [[20 [multiplied by] [n.sup.-[element of]/2] [multiplied by] [i.sup.(1-[Epsilon])/2]].sup.i].

Finally, summing over all possible i [element of] {k, ..., 2k}, and plugging in the definition of k, we get

(6) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(7) [is less than or equal to] k [[20/40 [multiplied by] [n.sup.-[Epsilon]/2 + ([Epsilon]/(1-[Epsilon]) [multiplied by] (1-[element of])/2)]].sup.k]

(8) [is less than or equal to] k [multiplied by] [2.sup.-k]

Thus, whp, as n tends to infinity, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] tends to zero.

Next we turn to part (2) of the lemma, concerning the partial matchability property. H does not have this property iff there is a set of edges E', |E'| [is less than or equal to] n [multiplied by] [(80[Delta]).sup.-2/(1-[Epsilon])], such that |V(E')| [is less than] |E'|. Let [B.sub.i] be the event that for a set E' of i edges, |V(E')| [is less than] |E'|.

(9) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(10) [is less than or equal to] [[[e.sup.2][Delta]i/n].sup.i]

(11) [is less than or equal to] [[[e.sup.2][n.sup.-((1/2) + [Epsilon]))]i].sup.i]

We need to sum over all i [is less than or equal to] 2k, and we split this sum into two parts, and bound each. Let k' = [n.sup.[Epsilon]/4(1-[Epsilon])].

(12) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We start with the first sum.

(13) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(14) [is less than or equal to] [n.sup.[element of]/4(1-[element of])] [multiplied by] [e.sup.2] [multiplied by] [n.sup.-((1/2)+[element of])] [multiplied by] [n.sup.[element of]/4(1-(element of])]

Recalling that 0 [is less than or equal to] [Epsilon] [is less than or equal to] 1/2, it is easy to verify that [Epsilon]/2(1 - [Epsilon]) [is less than] 1/2 + [Epsilon], and thus, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for some [Delta] [is greater than] 0, and this probability tends to 0 as n tends to infinity.

For the second sum, we first look at Eq. (11) and note that by the definition of k, [e.sup.2][n.sup.-((1/2)+[Epsilon])] i [is less than or equal to] [e.sup.2][n.sup.-((1/2)+[Epsilon])] 2k [is less than] 1/2, and hence

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Once again, this sum tends to zero as n tends to infinity, and the lemma is proven. []

ACKNOWLEDGMENTS. We thank Albert Atserias Peri, Juan Luis Esteban Angeles, and Maria Luisa Bonet Carbonell for carefully reading and commenting on an earlier version of the paper.

REFERENCES

BEAME, P., KARP, R., PITASSI, T., AND SAKS, M. 2000. On the complexity of unsatisfiability proofs for random k-CNF formulas. Submitted.

BEAME, P., AND PITASSI, T. 1996. Simplified and improved resolution lower bounds. In Proceedings of the 37th Annual Symposium on Foundations of Computer Science (Burlington, Vt., Oct.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 274-282.

BEN-SASSON, E., IMPAGLIAZZO, R., AND WIGDERSON, A. 2000. Optimal separation of tree-like and general resolution. In Electronic Colloquium on Computational Complexity Report Series. Tech. Rep. TR00-005.

BONET, M. L., ESTEBAN, J. L., GALESI, N., AND JOHANNSEN, J. 1998. On the relative complexity of resolution refinements and cutting planes proof systems. In Electronic Colloquium on Computational Complexity Report Series. Tech. Rep. TR98-035.

BONET, M. L., AND GALESI, N. 1999. A study of proof search algorithms for resolution and polynomial calculus. In Proceedings of the 40th Symposium of Foundations of Computer Science. IEEE Computer Society, Los Alamitos, Calif., pp. 422-431.

BUSS, S., AND PITASSI, T. 1997. Resolution and the weak pigeonhole principle. In Proceedings of the Conference for Computer Science Logic.

BUSS, S. R., AND TURAN, G. 1988. Resolution proof of generalized pigeonhole principles. Theoret. Comput. Sci. 62, 311-317.

CELONI, R., PAUL, W. J., AND TARJAN, R. E. 1977. Space bounds for a game on graphs. Math. Syst. Theory 10, 239-251.

CHVATAL, V., AND SZEMEREDI, E. 1988. Many hard examples for resolution. J. ACM 35, 4 (Oct.), 759 -768.

CLEGG, M., EDMONDS, J., AND IMPAGLIAZZO, R. 1996. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (Philadelphia, Pa., May 22-24). ACM, New York, pp. 174-183.

COOK, S. A., AND RECKHOW, R. 1979. The relative efficiency of propositional proof systems. J. Symb. Logic 44, 36-50.

DAVIS, M., LOGEMANN, G., AND LOVELAND, D. 1962. A machine program for theorem-proving. Commun. ACM 5, 7 (July), 394-397.

GALIL, Z. 1977. On resolution with clauses of bounded size. SIAM J. Comput. 6, 444-459.

HAKEN, A. 1985. The intractibility of resolution. Theoret. Comput. Sci. 39, 297-308.

IMPAGLIAZZO, R., PUDLAK, P., AND SGALL, J. 1997. Lower bounds for the polynomial-calculus and the groebner basis algorithm. Tech. Rep. TR97-042. Found at Electronic Colloqium on Computational Complexity, Reports Series 1997. Available at http://www.eccc.uni-trier.de/eccc/.

PIPPENGER PEBBLING, N. 1980. IBM Reserach Report RC8258. Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan.

RAZ, R., AND MCKENZIE, P. 1999. Separation of the monotone NC hierarchy. Combinatorica 19, 3, 403-435.

RAZBOROV, A. A. 1995. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izv. RAN 59, 1, 201-222.

RAZBOROV, A. A., AND RUDICH, S. 1994. Natural proofs. In Proceedings of the 26th Annual ACM Symposium on Theory of Computing (Montreal, Que., Canada, May 23-25). ACM, New York, pp. 204-213.

RAZBOROV, A. A., WIGDERSON, A., AND YAO, A. 1997. Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus. In Proceedings of the 29th Annual ACM Symposium on Theory of Computing (El Paso, Tex., May 4-6). ACM, New York, pp. 739-748.

TSEITIN, G. S. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2. Consultants Bureau, New York-London, pp. 115-125.

URQUHART, A. 1987. Hard examples for resolution. J. ACM 34, 1 (Jan.), 209-219.

URQUHART, A. 1995. The complexity of propositional proofs. Bull. Symb. Logic 1, 4, 425-467.

RECEIVED JUNE 1999; REVISED JULY 2000; ACCEPTED JULY 2000

ELI BEN SASSON AND AVI WIGDERSON Hebrew University, Jerusalem, Israel

This research was supported by grant number 69/96 of the Israel Science Foundation, founded by the Israel Academy for Sciences and Humanities.

Authors' present addresses: E. Ben-Sasson, 150 Stockton Street, Princeton, NJ 08540; A. Wigderson, Institute of Computer Science, Hebrew University, Jerusalem, Israel, e-mail: avi@cs.huji.ac.il.
COPYRIGHT 2001 Association for Computing Machinery, Inc.
No portion of this article can be reproduced without the express written permission from the copyright holder.
Copyright 2001 Gale, Cengage Learning. All rights reserved.

Article Details
Printer friendly Cite/link Email Feedback
Title Annotation:mathematical logic
Author:BEN-SASSON, ELI; WIGDERSON, AVI
Publication:Journal of the Association for Computing Machinery
Geographic Code:1USA
Date:Mar 1, 2001
Words:10640
Previous Article:Erratum: A Counterexample to W. Bibel's and E. Eder's Strong Completeness Result for Connection Graph Resolution.
Next Article:Improved Master Theorems for Divide-and-Conquer Recurrences.
Topics:

Terms of use | Privacy policy | Copyright © 2019 Farlex, Inc. | Feedback | For webmasters