Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR14-131 | 7th October 2014 15:01

A game characterisation of tree-like Q-Resolution size

RSS-Feed




TR14-131
Authors: Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
Publication: 18th October 2014 17:00
Downloads: 1556
Keywords: 


Abstract:

We provide a characterisation for the size of proofs in tree-like Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF proof systems.
We apply our technique to show the hardness of two classes of formulas for tree-like Q-Resolution. In particular, we give a proof of the hardness of the formulas of Kleine Buning et al. for tree-like Q-Resolution.



ISSN 1433-8092 | Imprint