We consider the problem of identifying failure nodes in networks under the Boolean Network Tomography ( BNT ) approach, which is based on end-to-end measurements routed in a network along paths and producing a boolean (failure/not-failure) outcome. Such end-to-end measurements paths are usually described by an incidence boolean matrix M with m rows (the measurements paths) and n columns (the nodes of the network). A key notion used in practice in this approach is that of k - identifiability . Loosely speaking, a set of m boolean measurements paths over n nodes is k -identifiable, where k is a non-negative integer, if, whenever there are fewer than k + 1 failures, it is always possible to identify unambiguously and uniquely which nodes are failing. Following the focus of some recent results analyzing maximal identifiability from a theoretical point of view, this work establishes the complexity of the optimization problem that determines the maximal k for which a set of measurement paths is k -identifiable ( MID ). We prove that such problem is NP -hard by a reduction from the Minimum Hitting Set problem and we prove that its decision version is in NP . We further consider the following extremal combinatoric question, which is also of practical relevance: given the number n of nodes of the network and a non-negative integer value k for the identifiability, what is the minimal number m of measurement paths over the n nodes to consider in such a way that the maximal identifiability is at least k ? A folklore result shows that to have maximal identifiability at least 1, then m ≥ log ( n + 1 ) (or, equivalently, that if n > 2 m − 1 , then the maximal identifiability is less than or equal 0). In this work we answer this question for each n ∈ N and for each k ≥ 2 , proving that, there is constant C such that if n > C m 1 + m k − 1 , then the maximal identifiability value is strictly smaller than k (and when k = 2 , n > C m m suffices). Finally, we study upper and lower bounds on the number of unambiguously identifiable nodes, introducing new identifiability conditions which strictly imply and are strictly implied by unambiguous identifiability. We use these new conditions to design algorithmic heuristics to count defective nodes in a fine-grained way. In particular we introduce a random model to study lower bounds on the number of unambiguously identifiable defective nodes and we use this model to estimate lower bounds on the number of identifiable nodes on real networks by a maximum likelihood estimate approach.

Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system. For size lower bounds these are established by monotone circuit arguments, while for depth these are found via communication complexity and protection. As such these bounds apply for lifted versions of combinatorial statements. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner’s Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon’s combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.

Abstract. We consider proof complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this proof complexity with the normal unary encoding in several refutation systems, based on Resolution and Sherali–Adams. We first consider [Formula: see text], which is an extension of Resolution working on [Formula: see text]-DNFs (Disjunctive Normal Form formulas). We prove an exponential lower bound of [Formula: see text] for the size of refutations of the binary version of the [Formula: see text]-Clique Principle in [Formula: see text], where [Formula: see text] and [Formula: see text] is a doubly exponential function. Our result improves that of Lauria et al., who proved a similar lower bound for [Formula: see text], i.e., Resolution. For the [Formula: see text]-Clique and other principles we study, we show how lower bounds in Resolution for the unary version follow from lower bounds in [Formula: see text] for the binary version, so we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the (weak) Pigeonhole Principle [Formula: see text]. We prove that for any [Formula: see text], [Formula: see text] requires refutations of size [Formula: see text] in [Formula: see text] for [Formula: see text]. Our lower bound cannot be improved substantially with the same method since for [Formula: see text] we can prove there are [Formula: see text] size refutations of [Formula: see text] in [Formula: see text]. This is a consequence of the same upper bound for the unary weak Pigeonhole Principle of Buss and Pitassi. We contrast unary versus binary encoding in the Sherali–Adams (SA) refutation system where we prove lower bounds for both rank and size. For the unary encoding of the Pigeonhole Principle and the Ordering Principle, it is known that linear rank is required for refutations in SA, although both admit refutations of polynomial size. We prove that the binary encoding of the (weak) Pigeonhole Principle [Formula: see text] requires exponentially sized (in [Formula: see text]) SA refutations, whereas the binary encoding of the Ordering Principle admits logarithmic rank, polynomially sized SA refutations. We continue by considering a natural refutation system we call “SA+Squares,” which is intermediate between SA and Lasserre (Sum-of-Squares). This has been studied under the name static-[Formula: see text] by Grigoriev et al. In this system, the unary encoding of the Linear Ordering Principle [Formula: see text] requires [Formula: see text] rank while the unary encoding of the Pigeonhole Principle becomes constant rank. Since Potechin has shown that the rank of [Formula: see text] in Lasserre is [Formula: see text], we uncover an almost quadratic separation between SA+Squares and Lasserre in terms of rank. Grigoriev et al. noted that the unary Pigeonhole Principle has rank 2 in SA+Squares and therefore polynomial size. Since we show the same applies to the binary [Formula: see text], we deduce an exponential separation for size between SA and SA+Squares.

In this paper we combine many of the standard and more recent algebraic techniques for testing isomorphism of finite groups (GpI) with combinatorial techniques that have typically been applied to Graph Isomorphism. In particular, we show how to combine several state-of-the-art GpI algorithms for specific group classes into an algorithm for general GpI, namely: composition series isomorphism (Rosenbaum-Wagner, Theoret. Comp. Sci., 2015; Luks, 2015), recursively-refineable filters (Wilson, J. Group Theory, 2013), and low-genus GpI (Brooksbank-Maglione-Wilson, J. Algebra, 2017). Recursively-refineable filters -- a generalization of subgroup series -- form the skeleton of this framework, and we refine our filter by building a hypergraph encoding low-genus quotients, to which we then apply a hypergraph variant of the k-dimensional Weisfeiler-Leman technique. Our technique is flexible enough to readily incorporate additional hypergraph invariants or additional characteristic subgroups.

Abstract We introduce a novel take on sum-of-squares that is able to reason with complex numbers and still make use of polynomial inequalities. This proof system might be of independent interest since it allows to represent multivalued domains both with Boolean and Fourier encoding. We show degree and size lower bounds in this system for a natural generalization of knapsack: the vanishing sums of roots of unity. These lower bounds naturally apply to polynomial calculus as-well.

Stabbing Planes is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system established via communication complexity arguments. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner’s Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon’s combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.

Res(s) is an extension of Resolution working on s-DNFs. We prove tight n^{Omega(k)} lower bounds for the size of refutations of the binary version of the k-Clique Principle in Res(o(log log n)). Our result improves that of Lauria, Pudlák et al. [Massimo Lauria et al., 2017] who proved the lower bound for Res(1), i.e. Resolution. The exact complexity of the (unary) k-Clique Principle in Resolution is unknown. To prove the lower bound we do not use any form of the Switching Lemma [Nathan Segerlind et al., 2004], instead we apply a recursive argument specific for binary encodings. Since for the k-Clique and other principles lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for their binary version we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the weak Pigeonhole Principle Bin-PHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, Bin-PHP^m_n requires proofs of size 2^{n^{1-delta}} in Res(s) for s=o(log^{1/2}n). Our lower bound is almost optimal since for m >= 2^{sqrt{n log n}} there are quasipolynomial size proofs of Bin-PHP^m_n in Res(log n). Finally we propose a general theory in which to compare the complexity of refuting the binary and unary versions of large classes of combinatorial principles, namely those expressible as first order formulae in Pi_2-form and with no finite model.

We show that if a k-CNF requires width w to refute in resolution, then it requires space square root of √ω to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is the first analogue, in polynomial calculus, of Atserias and Dalmau's result lower-bounding clause space in resolution by resolution width. As a by-product of our new approach to space lower bounds we give a simple proof of Bonacina's recent result that total space in resolution (the total number of variable occurrences that must be kept in memory) is lower-bounded by the width squared. As corollaries of the main result we obtain some new lower bounds on the PCR space needed to refute specific formulas, as well as partial answers to some open problems about relations between space, size, and degree for polynomial calculus.

We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2^{tw(G)^{O(1/d)}} poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

We study maximal identifiability, a measure recently introduced in Boolean Network Tomography to characterize networks' capability to localize failure nodes in end-to-end path measurements. Under standard assumptions on topologies and on monitors placement, we prove tight upper and lower bounds on the maximal identifiability of failure nodes for specific classes of network topologies, such as trees, bounded-degree graphs, d-dimensional grids, in both directed and undirected cases. Among other results we prove that directed d-dimensional grids with support n have maximal identifiability d using nd monitors; and in the undirected case we show that 2d monitors suffice to get identifiability of d-1. We then study identifiability under embeddings: we establish relations between maximal identifiability, embeddability and dimension when network topologies are modelled as DAGs. Through our analysis we also refine and generalize results on limits of maximal identifiability recently obtained in [12] and [1]. Our results suggest the design of networks over N nodes with maximal identifiability Ω(√log N) using 2√log N monitors and heuristics to place monitors and edges in a network to boost maximal identifiability.

We show quadratic lower bounds on the total space used in resolution refutations of random $k$-CNFs over $n$ variables and of the graph pigeonhole principle and the bit pigeonhole principle for $n$ holes. This answers the open problem of whether there are families of $k$-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.

We study the proof complexity of Paris-Harrington’s Large Ramsey Theorem for bi-colorings of graphs and of off-diagonal Ramsey’s Theorem. For Paris-Harrington, we prove a non-trivial conditional lower bound in Resolution and a non-trivial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in R es (2). We show that under such an assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced off-diagonal Ramsey principle is established. This is obtained by adapting some constructions due to Erdős and Mills. We prove a non-trivial Resolution lower bound for a family of such off-diagonal Ramsey principles.

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.

Algebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove Ω( n ) space lower bounds in PC/PCR for random k -CNFs ( k ≥ 4) in n variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph.

We show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables, and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the long-standing open problem of whether there are families of k-CNF formulas of polynomial size which require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.

We devise a new combinatorial framework for proving space lower bounds in algebraic proof systems like Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr). Our method can be thought as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials instead that clauses as in the case of Resolution. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution.

We study the performance of DPLL algorithms on parameterized problems. In particular, we investigate how difficult it is to decide whether small solutions exist for satisfiability and other combinatorial problems. For this purpose we develop a Prover-Delayer game that models the running time of DPLL procedures and we establish an information-theoretic method to obtain lower bounds to the running time of parameterized DPLL procedures. We illustrate this technique by showing lower bounds to the parameterized pigeonhole principle and to the ordering principle. As our main application we study the DPLL procedure for the problem of deciding whether a graph has a small clique. We show that proving the absence of a k -clique requires n Ω(k) steps for a nontrivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked by Beyersdorff et al. [2012] of understanding the Resolution complexity of this family of formulas.

We study the proof complexity of Paris-Harrington's Large Ramsey Theorem for bi-colorings of graphs. We prove a non-trivial conditional lower bound in Resolution and a quasi-polynomial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in RES(2). We show that under such assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by adapting some constructions due to Erdos and Mills.

A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider [9]. There the authors concentrate on tree-like Parameterized Resolution—a parameterized version of classical Resolution—and their gap complexity theorem implies lower bounds for that system. The main result of the present paper significantly improves upon this by showing optimal lower bounds for a parameterized version of bounded-depth Frege. More precisely, we prove that the pigeonhole principle requires proofs of size n Ω(k) in parameterized bounded-depth Frege, and, as a special case, in dag-like Parameterized Resolution. This answers an open question posed in [9]. In the opposite direction, we interpret a well-known technique for FPT algorithms as a DPLL procedure for Parameterized Resolution. Its generalization leads to a proof search algorithm for Parameterized Resolution that in particular shows that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF’s.

There are methods to turn short refutations in polynomial calculus (Pc) and polynomial calculus with resolution (Pcr) into refutations of low degree. Bonet and Galesi [1999, 2003] asked if such size-degree tradeoffs for Pc [Clegg et al. 1996; Impagliazzo et al. 1999] and Pcr [Alekhnovich et al. 2004] are optimal. We answer this question by showing a polynomial encoding of the graph ordering principle on m variables which requires Pc and Pcr refutations of degree Ω(√ m ). Tradeoff optimality follows from our result and from the short refutations of the graph ordering principle in Bonet and Galesi [1999, 2001]. We then introduce the algebraic proof system Pcr k which combines together polynomial calculus and k-DNF resolution (Res k ). We show a size hierarchy theorem for Pcr k : Pcr k is exponentially separated from Pcr k+1 . This follows from the previous degree lower bound and from techniques developed for Res k . Finally we show that random formulas in conjunctive normal form (3-CNF) are hard to refute in Pcr k .

We describe a system LK(c[/spl lambda/]) for refuting CNF formulae, as a restriction of the sequent calculus in which every formula in a sequent is defined over at most /spl lambda/ variables. This further generalizes the system Res(k), a generalization of Resolution to k-DNF introduced in (Krajicek, 2001). We adapt the Pudlak-Impagliazzo game (Pudlak and Impagliazzo, 2000) to prove lower bounds for treelike LK(c[/spl lambda/]). We show that dynamic satisfiability, which was introduced in (Esteban et al., 2002) to study resolution space complexity, is a sufficient "but not necessary" condition to obtain exponential lower bounds.

We present a new method for proving rank lower bounds for Cutting Planes (CP) and several procedures based on lifting due to Lovasz and Schrijver (LS), when viewed as proof systems for unsatisfiability. We apply this method to obtain the following new results: first, we prove near-optimal rank bounds for Cutting Planes and Lovasz-Schrijver proofs for several prominent unsatisfiable CNF examples, including random kCNF formulas and the Tseitin graph formulas. It follows from these lower bounds that a linear number of rounds of CP or LS procedures when applied to relaxations of integer linear programs is not sufficient for reducing the integrality gap. Secondly, we give unsatisfiable examples that have constant rank CP and LS proofs but that require linear rank resolution proofs. Thirdly, we give examples where the CP rank is O(log n) but the LS rank is linear. Finally, we address the question of size versus rank: we show that, for both proof systems, rank does not accurately reflect proof size. Specifically, there are examples with polynomial-size CP/LS proofs, but requiring linear rank.

We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis /spl and/, V) can be turned into a proof containing only monotone formulas of size m/sup O(log m)/ and with the number of proof lines polynomial in m. Also we show that some interesting special cases, namely the functional and the onto versions of PHP and a version of the matching principle, have polynomial size monotone proofs.

We study the space complexity of refuting unsatisfiable random k-CNFs in the resolution proof system. We prove that for any large enough /spl Delta/, with high probability a random k-CNF over n variables and /spl Delta/n clauses requires resolution clause space of /spl Omega/(n/spl middot//spl Delta//sup -1+/spl epsiv//k-2-/spl epsiv//), for any 0>/spl radic/n. This bound is nearly tight. Specifically, we show that with high probability, a random 3-CNF with /spl Delta/n clauses requires tree-like refutation size of exp(/spl Omega/(n//spl Delta//sup 1+/spl epsiv//1-/spl epsiv//)), for any 0</spl epsiv/<1/2. Our space lower bound is the consequence of three main contributions. 1. We introduce a 2-player matching game on bipartite graphs G to prove that there are no perfect matchings in G. 2. We reduce lower bounds for the clause space of a formula F in resolution to lower bounds for the complexity of the game played on the bipartite graph G(F) associated with F. 3. We prove that the complexity of the game is large whenever G is an expander graph. Finally, a simple probabilistic analysis shows that for a random formula F, with high probability G(F) is an expander. We also extend our result to the case of G-PHP, a generalization of the pigeonhole principle based on bipartite graphs G. We prove that the clause space for G-PHP can be reduced to the game complexity on G.

An exponential lower bound for the size of tree-like cutting planes refutations of a certain family of conjunctive normal form (CNF) formulas with polynomial size resolution refutations is proved. This implies an exponential separation between the tree-like versions and the dag-like versions of resolution and cutting planes. In both cases only superpolynomial separations were known [A. Urquhart, Bull. Symbolic Logic, 1 (1995), pp. 425--467; J. Johannsen, Inform. Process. Lett., 67 (1998), pp. 37--41; P. Clote and A. Setzer, in Proof Complexity and Feasible Arithmetics, Amer. Math. Soc., Providence, RI, 1998, pp. 93--117]. In order to prove these separations, the lower bounds on the depth of monotone circuits of Raz and McKenzie in [ Combinatorica, 19 (1999), pp. 403--435] are extended to monotone real circuits. An exponential separation is also proved between tree-like resolution and several refinements of resolution: negative resolution and regular resolution. Actually, this last separation also provides a separation between tree-like resolution and ordered resolution, and thus the corresponding superpolynomial separation of [A. Urquhart, Bull. Symbolic Logic, 1 (1995), pp. 425--467] is extended. Finally, an exponential separation between ordered resolution and unrestricted resolution (also negative resolution) is proved. Only a superpolynomial separation between ordered and unrestricted resolution was previously known [A. Goerdt, Ann. Math. Artificial Intelligence, 6 (1992), pp. 169--184].

The paper is concerned with the complexity of proofs and of searching for proofs in two propositional proof systems: Resolution and Polynomial Calculus (PC). For the former system we show that the recently proposed algorithm of E. Ben-Sasson and A. Wigderson (1999) for searching for proofs cannot give better than weakly exponential performance. This is a consequence of showing optimality of their general relationship, referred to as size-width trade-off. We moreover obtain the optimality of the size width trade-off for the widely used restrictions of resolution: regular, Davis-Putnam, negative, positive and linear. As for the second system, we show that the direct translation to polynomials of a CNF formula having short resolution proofs, cannot be refuted in PC with degree less than /spl Omega/ (log n). A consequence of this is that the simulation of resolution by PC of M. Clegg, J. Edmonds and R. Impagliazzo (1996) cannot be improved to better than quasipolynomial in the case where we start with small resolution proofs. We conjecture that the simulation of M. Clegg et al. is optimal.

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. In order to prove this, we extend the lower bounds on the depth of monotone circuits of R. Raz and P. McKenzie (1997) to monotone real circuits. In the case of resolution, we further improve this result by giving an exponential separation of tree-like resolution front (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Puatam resolution proof. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separations was previously known.