AAAI Publications, Workshops at the Thirtieth AAAI Conference on Artificial Intelligence

Font Size: 
Extension Variables in QBF Resolution
Olaf Beyersdorf, Leroy Chew, Mikolas Janota

Last modified: 2016-03-29


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 Wintersteiger et al, 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 Wintersteiger et al. 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.


QBF, separation, complexity, resolution

Full Text: PDF