Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with tree-like resolution:
TR99-041 | 22nd August 1999
Oliver Kullmann

Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs

Revisions: 2

A relativized hierarchy of conjunctive normal forms
is introduced, recognizable and SAT decidable in polynomial
time. The corresponding hardness parameter, the first level
of inclusion in the hierarchy, is studied in detail, admitting
several characterizations, e.g., using pebble games, the space
complexity of (relativized) tree-like ... more >>>

TR07-001 | 19th November 2006
Stefan S. Dantchev, Barnaby Martin, Stefan Szeider

Parameterized Proof Complexity: a Complexity Gap for Parameterized Tree-like Resolution

Revisions: 2

We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter tractable. We consider proofs that witness that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter. One could separate the ... more >>>

TR19-097 | 4th July 2019
Jacobo Toran, Florian Wörz

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

Revisions: 1 , Comments: 1

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 ... more >>>

TR21-033 | 7th March 2021
Susanna de Rezende

Automating Tree-Like Resolution in Time $n^{o(\log n)}$ Is ETH-Hard

We show that tree-like resolution is not automatable in time $n^{o(\log n)}$ unless ETH is false. This implies that, under ETH, the algorithm given by Beame and Pitassi (FOCS 1996) that automates tree-like resolution in time $n^{O(\log n)}$ is optimal. We also provide a simpler proof of the result of ... more >>>

ISSN 1433-8092 | Imprint