Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR16-005 | 22nd January 2016 13:23

Extension Variables in QBF Resolution

RSS-Feed




TR16-005
Authors: Olaf Beyersdorff, Leroy Chew, Mikolas Janota
Publication: 22nd January 2016 13:46
Downloads: 471
Keywords: 


Abstract:

We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Jussila et al. '07 who give experimental evidence that extended Q-resolution is stronger than weak extended Q-resolution.

Here we prove an exponential separation between the two systems, thereby confirming the conjecture of by Jussila et al. '07. Conceptually, this separation relies on showing strategy extraction for weak extended Q-resolution by bounded-depth circuits. In contrast, we show that this strong strategy extraction result fails in extended Q-resolution.



ISSN 1433-8092 | Imprint