Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR15-133 | 12th August 2015 11:08

Lower bounds: from circuits to QBF proof systems


Authors: Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
Publication: 16th August 2015 22:11
Downloads: 2069


A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from circuit complexity to proof complexity has been effective, a formal connection between the two areas has never been established so far.
Here we provide such a formal relation between lower bounds for circuit classes and lower bounds for Frege systems for quantified Boolean formulas (QBF).

Starting from a propositional proof system P we exhibit a general method how to obtain a QBF proof system P+$\forall$red, which is inspired by the transition from resolution to Q-resolution. For us the most important case is a new and natural hierarchy of QBF Frege systems C-Frege+$\forall$red that parallels the well-studied propositional hierarchy of C-Frege systems, where lines in proofs are restricted to a circuit class C.

Building on earlier work for resolution (Beyersdorff, Chew, Janota STACS'15), we establish a lower bound technique via strategy extraction that transfers arbitrary lower bounds for the circuit class C to lower bounds in C-Frege+$\forall$red.

ISSN 1433-8092 | Imprint