Paper Info
Title
Lower Bounds for Space in Resolution
Abstract
Resolution space measures the maximum number of clauses that need to be simultaneously active in a resolution refutation. This complexity measure was defined by Kleine Büning and Lettmann in [8] and slightly modified recently [6] to make it suitable for comparisons with other measures. Since its definition, only trivial lower bound for the resolution space, measured in terms of the number of initial clauses were known. In this paper we prove optimal lower bounds for the space needed in the resolution refutation of two important families of formulas. We show that Tseitin formulas associated to a certain kind of expander graphs of n nodes need resolution space n - c for some constant c. Measured on the number of clauses, this result is best possible since the mentioned formulas have O(n) clauses, and the number of clauses is an upper bound for the resolution space. We also show that the formulas expressing the general Pigeonhole Principle with n holes and more than n pigeons, need space n + 1 independently of the number of pigeons. Since a matching space upper bound of n + 1 for these formulas exist, the obtained bound is exact. These results point to a possible connection between resolution space and resolution width, another measure for the complexity of resolution refutations.
Year
DOI
Venue
1999
10.1007/3-540-48168-0_26
CSL
Keywords
Field
DocType
need space n,resolution space,n hole,n node,matching space,resolution refutation,resolution space n,resolution width,lower bounds,maximum number,n pigeon,lower bound,upper bound,expander graph
Discrete mathematics,Combinatorics,Expander graph,Upper and lower bounds,Propositional calculus,Information complexity,Mathematics,Computational complexity theory,Pigeonhole principle
Conference
Volume
ISSN
ISBN
1683
0302-9743
3-540-66536-6
Citations 
PageRank 
References 
12
0.69
10
Authors
1
Name
Order
Citations
PageRank
Jacobo Torán156449.26