Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR18-024 | 1st February 2018 18:50

The Riis Complexity Gap for QBF Resolution


Authors: Olaf Beyersdorff, Judith Clymo, Stefan Dantchev, Barnaby Martin
Publication: 5th February 2018 17:40
Downloads: 701


We give an analogue of the Riis Complexity Gap Theorem for Quanti fied Boolean Formulas (QBFs). Every fi rst-order sentence $\phi$ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like Q-Resolution are either of polynomial size (if $\phi$ has no models) or at least exponential in size (if $\phi$ has some in finite model). However, di fferently from the translations to propositional logic, the translation to QBF must be given additional structure in order for the polynomial upper bound to hold in tree-like Q-Resolution. This extra structure is not needed in the system tree-like $\forall$Exp+Res, where we see the complexity gap on a natural translation to QBF.

ISSN 1433-8092 | Imprint