Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR17-032 | 17th February 2017 00:04

Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds


Authors: Olaf Beyersdorff, Joshua Blinkhorn
Publication: 19th February 2017 09:29
Downloads: 1047


We devise a new technique to prove lower bounds for the proof size in resolution-type calculi for quantified Boolean formulas (QBF). The new technique applies to the strong expansion system IR-calc and thereby also to the most studied QBF system Q-Resolution.

Our technique exploits a clear semantic paradigm, showing the hardness of a QBF family by demonstrating that
(1) the formulas require large witnessing functions for the universal variables, and (2) in the game semantics of QBF, the universal player is forced to make many responses on a set of variables that we identify as critical.

Based on these two conditions, our technique yields a weight for a QBF formula, which provides an absolute lower bound for the size of its IR-calc proofs (and hence also its Q-Resolution proofs).

We exemplify our technique on a couple of known and new instances, among them the prominent formulas of Kleine B√ľning et al. (Inform. Comput. 1995), for which our method provides a hardness proof that is considerably simpler than previous approaches.

Our technique also provides the first separations for QBF dependency calculi. In particular, we construct a simple class of formulas that are hard for Q-Resolution, but easy in Q-Resolution parameterized by the reflexive resolution path dependency scheme, thus answering a question posed by Slivovsky and Szeider (SAT 2014).

ISSN 1433-8092 | Imprint