首页    期刊浏览 2024年11月24日 星期日
登录注册

文章基本信息

  • 标题:A game characterisation of tree-like Q-Resolution size
  • 本地全文:下载
  • 作者:Olaf Beyersdorff ; Leroy Chew ; Karteek Sreenivasaiah
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2014
  • 卷号:2014
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    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.

  • 关键词:lower bound ; prover delayer game ; Q-Resolution ; quantified Boolean formula
国家哲学社会科学文献中心版权所有