REVERSIBLE PEBBLE GAMES AND THE RELATION BETWEEN TREE-LIKE AND GENERAL RESOLUTION SPACE

Toran Jacobo; Woerz Florian

首页> 外文期刊>Computational complexity >REVERSIBLE PEBBLE GAMES AND THE RELATION BETWEEN TREE-LIKE AND GENERAL RESOLUTION SPACE

【24h】

REVERSIBLE PEBBLE GAMES AND THE RELATION BETWEEN TREE-LIKE AND GENERAL RESOLUTION SPACE

机译：REVERSIBLE PEBBLE GAMES AND THE RELATION BETWEEN TREE-LIKE AND GENERAL RESOLUTION SPACE

获取原文

获取原文并翻译 | 示例

掌桥外文数据库（机构版） >>

开具论文收录证明 >>

文献代查 >>

页面导航

摘要
著录项
相关主题

摘要

We show a new connection between the clause space measure in tree-like resolution and the reversible pebble game on graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the clause space complexity measure in tree-like and general resolution. We also provide upper bounds for tree-like resolution clause space in terms of general resolution clause and variable space. In particular, we show that for any formula F, its tree-like resolution clause space is upper bounded by space(pi) log (time(pi)), where pi is any general resolution refutation of F. This holds considering as space(pi) 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(pi) log n, where n is the number of vertices of the corresponding graph.

著录项

来源
《Computational complexity》 |2021年第1期|7.1-7.37|共37页
作者
Toran Jacobo; Woerz Florian;
展开▼
作者单位

Univ Ulm, D-89081 Ulm, Germany;

展开▼
收录信息
原文格式 PDF
正文语种英语
中图分类
关键词
Proof complexity; Resolution; Tree-like resolution; Pebble game; Reversible pebbling; Prover-Delayer game; Raz-McKenzie game; Clause space; Variable space;

REVERSIBLE PEBBLE GAMES AND THE RELATION BETWEEN TREE-LIKE AND GENERAL RESOLUTION SPACE

摘要

著录项

相关主题

期刊订阅