文章基本信息

标题：Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space
本地全文：下载
作者：Jacobo Tor{'a}n ; Florian W{"o}rz
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：154
页码：60:1-60:18
DOI：10.4230/LIPIcs.STACS.2020.60
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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 not far from 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 space 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.
关键词：Proof Complexity; Resolution; Tree-like Resolution; Pebble Game; Reversible Pebbling; Prover-Delayer Game; Raz - McKenzie Game; Clause Space; Variable Space