ALCOMFT-TR-02-132

Albert Atserias
The Complexity of Resource-Bounded Propositional Proofs
Barcelona. Work package 4. May 2002.

Abstract: Propositional Proof Complexity is an active area of research whose main focus is the study of the length of proofs in propositional logic. There are several motivations for such a study, the main of which is probably its connection to the P vs NP problem in Computational Complexity.

The experience in the field has revealed that the most interesting parameter of a proof system is the set of allowed formulas. The exact set of rules and axioms of the system is often irrelevant as long as they remain sound and reasonable. This parameterization by the set of allowed formulas establishes a link with the field of Boolean complexity where bounds are imposed on different computational resources as a classification tool. This idea is adopted in the proof complexity setting too. In this thesis we study the complexity of several 'resource-bounded' proof systems.

The first set of results of the thesis is about a resource-bounded proof system that we call the Monotone Sequent Calculus (MLK). This is the standard propositional Gentzen Calculus (LK) when negation is not allowed in the formulas. The main result is that the use of negation does not yield exponential savings in the length of proofs. More precisely, we show that MLK quasipolynomially simulates LK on monotone sequents. We also show that, as refutation systems, MLK is polynomially bounded if and only if LK is. These results are in sharp contrast with the situation in Boolean complexity where the use of negations provably yields an exponential gap in computational power.

The second set of results is about a proof system extending Resolution by allowing disjunctions of conjunctions of two literals and not only disjunctions of literals. We prove that the Weak Pigeonhole Principle with twice as many pigeons than holes, and random 3-CNF formulas, require exponential-size proofs in this system. The interest of our results is that we break the barrier of one alternation of disjunctions and conjunctions in the context of the weak pigeonhole principle and random 3-CNF formulas for the first time. The techniques that we employ combine old ideas with new arguments using powerful tools from probability theory.

The third and final set of results is about the exact complexity of the Weak Pigeonhole Principle with twice as many pigeons than holes. We show that all previously known quasipolynomial-size proofs of bounded-depth are not optimal in terms of size. As a consequence of our result, we obtain Bounded Arithmetic proofs that there are infinitely many primes from 'large number assumptions' that are provably weaker than previously needed.

Postscript file: ALCOMFT-TR-02-132.ps.gz (228 kb).