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+ 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+ 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+ red.
展开▼
