Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR12-161 | 20th November 2012 20:19

A Characterization of Tree-Like Resolution Size

RSS-Feed




TR12-161
Authors: Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
Publication: 21st November 2012 02:06
Downloads: 3849
Keywords: 


Abstract:

We explain an asymmetric Prover-Delayer game which precisely characterizes proof size in tree-like Resolution. This game was previously described in a parameterized complexity context to show lower bounds for parameterized formulas and for the classical pigeonhole principle. The main point of this note is to show that the asymmetric game in fact characterizes tree-like Resolution proof size, i.e. in principle our proof method allows to always achieve the optimal lower bounds. This is in contrast with previous techniques described in the literature. We also provide a very intuitive information-theoretic interpretation of the game.



ISSN 1433-8092 | Imprint