Abstract

This work is a contribution to the field of Proof Complexity, which studies the complexity of proof systems in terms of the resources needed to prove or refute propositional formulas. Proof Complexity is an interesting field which has several connections to other fields of Computer Science like Computational Complexity or Automatic Theorem Proving among others. This work focuses in complexity measures for refutational proof systems for CNF formulas. We consider several proof systems, namely Resolution, R(k) and Cutting Planes and our results concern mainly to the size and space complexity measures.

We improve previous size separations between treelike and general versions of Resolution and Cutting Planes. To do so we extend a size lower bound for monotone boolean circuits by Raz and McKenzie, to monotone real circuits. This kind of separations is interesting because some automated theorem provers rely on the treelike version of proof systems, so the separations show that is not always a good idea to restrict to the treelike version. What we do is to prove treelike Cutting Planes exponential lower bounds for certain formulas via the feasible monotone interpolation property, which clearly are also lower bounds for treelike Resolution. To get the separation we show Resolution polynomial size upper bounds for the same formulas, which clearly are also upper bounds for Cutting Planes. In fact we can separate not only treelike Resolution from Resolution, also we can separate treelike Resolution from certain restrictions of Resolution like regular Resolution and negative Resolution. The separation result for treelike Resolution and Resolution was later improved by Ben-Sasson, Impagliazzo and Wigderson.

After the recent apparition of R(k) which is a proof system lying between Resolution and bounded-depth Frege it was important to study how powerful it is and its relation with other proof systems. We solve an open problem posed by Krajícek, namely we show that R(2) does not have the feasible monotone interpolation property. To do so, we show that R(2) is strictly more powerful than Resolution. We give a R(2) polynomial size upper bound for a certain Clique-Coclique Principle reducing it to a Pigeonhole Principle with parameters that ensures polynomial size Resolution refutations. But as Resolution has the feasible monotone interpolation property, and it is known that circuits separating cliques from cocliques require superpolynomial size, then Resolution refutations for this Clique-Coclique Principle also require superpolynomial size. As now we know that R(2) is more powerful that Resolution and treelike R(2) more powerful than treelike Resolution, a natural question is to find out whether we can separate successive levels of R(k) or treelike R(k). We show exponential separations between successive levels of what we can call now the treelike R(k) hierarchy. That means that there are formulas that require exponential size R(k) refutations whereas they have polynomial size R(k+1) refutations. Segerlind, Buss and Impagliazzo extended this result to R(k). We also prove that Resolution dominates treelike R(k). This is a particular case of a known simulation due to Krajícek, but we show that an increment by factor 2, independent of k, suffices.

We have proposed a new definition for Resolution space improving a previous one from Kleine-Büning and Lettmann. There is also an equivalent definition of Resolution space from Alekhnovich, Ben-Sasson, Razborov and Wigderson. We give general results for Resolution and treelike Resolution space, namely that any CNF with n variables requires at most space n+1 and relationships between space and size among others. We also give a combinatorial characterization of treelike Resolution space via a Player-Adversary game over CNF formulas. The characterization allows to prove lower bounds for treelike Resolution space with no need to use the concept of Resolution or Resolution refutations at all. For a long time it was not known whether Resolution space and treelike Resolution space coincided or not. We have answered this question in the negative because we give the first space separation from Resolution to treelike Resolution. We have also studied space for R(k). We show that, as happened with respect to size, treelike R(k) forms a hierarchy respect to space. So, there are formulas that require nearly linear space for treelike R(k) whereas they have constant space treelike R(k+1) refutations. We extend all known Resolution space lower bounds to R(k) in an easier and unified way, that also holds for Resolution, using the concept of dynamical satisfiability introduced in this work.

Table of Contents

1. Introduction and definitions
1.1 Proof Systems
1.2 Complexity Measures
1.3 Formulas
1.4 Circuit Complexity
1.5 Overview of results in the area
1.6 Summary of results and organization of this work

2. Size
2.1 Size separation between CP* and R(1)
2.2 R(2) has not the monotone interpolation property
2.3 R(2) and PHP(n²,n)
2.4 Size and R*(k)

3. Space and width
3.1 Space for R(1)
3.2 Combinatorial characterization of R*(1) space
3.3 Separation between R(1) space and R*(1) space
3.4 Space separations for R*(k)
3.5 Space lower bounds for R(k)

4. Recapitulation