Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Revision(s):

Revision #1 to TR19-097 | 13th February 2020 17:37

#### Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space

Revision #1
Authors: Jacobo Toran, Florian Wörz
Accepted on: 13th February 2020 17:37
Keywords:

Abstract:

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($\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.

Changes to previous version:

The major changes are:
* We corrected a small parameter mistake in Thm. 39. We also extended the proof, providing more details.
* A typing error in the proof of Thm. 40 was fixed.
* The proof of Thm. 43 was extended, explaining an important detail of the argument.

### Paper:

TR19-097 | 4th July 2019 16:08

#### Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space

TR19-097
Authors: Jacobo Toran, Florian Wörz
Publication: 24th July 2019 15:09
Keywords:

Abstract:

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.

### Comment(s):

Comment #1 to TR19-097 | 28th July 2019 11:17

Authors: Florian Wörz
Accepted on: 28th July 2019 11:17
Keywords:

Comment:

In this comment, we provide a readable version of the abstract, replacing the question marks with $\pi$. The abstract should read:

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 $\mathrm{space}(\pi)\log \big(\mathrm{time}(\pi) \big)$ where $\pi$ is any general resolution refutation of $F$. This holds considering as $\mathrm{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 $\mathrm{space}(\pi) \log n$, where $n$ is the number of vertices of the corresponding graph.''

ISSN 1433-8092 | Imprint