Paper Info
Title
A combinatorial characterization of treelike resolution space
Abstract
We show that the Player-Adversary game of Pudlák and Impagliazzo [A lower bound for DLL algorithms for k-SAT, in: Proc. 11th Annual ACM-SIAM Symposium on Discrete Algorithms, 2000, pp. 128-136] played over CNF propositional formulas gives an exact characterization of the space needed in treelike resolution refutations. This characterization is purely combinatorial and independent of the notion of resolution. We use this characterization to give for the first time a separation between the space needed in treelike and general resolution.
Year
DOI
Venue
2003
10.1016/S0020-0190(03)00345-4
Electronic Colloquium on Computational Complexity (ECCC)
Keywords
DocType
Volume
treelike resolution refutation,exact characterization,discrete algorithms,annual acm-siam symposium,player-adversary game,treelike resolution space,cnf propositional formula,combinatorial characterization,dll algorithm,general resolution,lower bound,theory of computation
Journal
87
Issue
ISSN
Citations 
6
0020-0190
18
PageRank 
References 
Authors
0.73
13
2
Name
Order
Citations
PageRank
Juan Luis Esteban120911.27
Jacobo Torán256449.26