首页    期刊浏览 2024年10月06日 星期日
登录注册

文章基本信息

  • 标题:Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space
  • 本地全文:下载
  • 作者:Jacobo Toran ; Florian Wörz
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2019
  • 卷号:2019
  • 页码:1-21
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    We show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations are almost optimal by proving upper bounds for tree-like resolution space in terms of general resolution clause and variable space. In particular we show that for any formula F, its tree-like resolution is upper bounded by space(?)log time(?) where ? is any general resolution refutation of F. This holds considering as space(?) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas we are able to improve this bound to the optimal bound space(?)log(n), where n is the number of vertices of the corresponding graph.

  • 关键词:Clause Space ; pebble game ; Proof Complexity ; Prover;Delayer Game ; Raz;McKenzie Game ; Resolution ; reversible pebbling ; tree;like resolution ; Variable Space
国家哲学社会科学文献中心版权所有