DIMACS Discrete Math--Theory of Computing Seminar
Speaker: Alexander Razborov, Steklov Mathematical Institute and Princeton University
Title: Space Complexity in Propositional Calculus
Date: Tuesday, November 16
Time: 4:30-5:30
Place: CORE Building seminar room (431), Rutgers University, Piscataway, NJ

Abstract:

Complexity of propositional proofs plays as important a role in the theory of feasible proofs as the role played by the complexity of Boolean circuits in the theory of efficient computations. By now it has become quite an established area where a number of strong and deep results have been proven. However, most of the research in the proof-complexity area concentrated so far on complexity measures related to the amount of time taken by the proof.

Very recently, Esteban and Toran proposed a convenient definition of space complexity for the most popular propositional proof system, Resolution. Our main goal is to generalize the natural notion of space complexity to stronger propositional proof systems, and research its properties. Besides Resolution, we consider Polynomial Calculus and Frege systems, and we are interested in two different space measures, corresponding to the maximal number of bits, and clauses/monomials that need be kept in the memory simultaneously. We prove a number of lower and upper bounds in these models for such important principles as Pigeonhole principle and Tseitin tautologies, as well as for "universal" tautologies. We also establish some structural results concerning the clause space for Resolution and Frege Systems.

Joint work with M. Alekhnovich, E. Ben-Sasson and A. Wigderson; text of the paper is available at ftp://ftp.eccc.uni-trier.de/pub/eccc/reports/1999/TR99-040/index.html