Lower Bounds: From Circuits to QBF Proof Systems

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 vertical bar for all 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+for all red that parallels the well-studied propositional hierarchy of C-Frege systems, where lines in proofs are restricted to belong to a circuit class C. Building on earlier work for resolution [Beyersdorff, Chew and Janota, 2015a] 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+for all red. By using the full spectrum of state-of-the-art circuit lower bounds, our new lower bound method leads to very strong lower bounds for QBF \FREGE systems: (i) exponential lower bounds and separations for the QBF proof system AC(0)[p]-Frege+for all red for all primes p; (ii) an exponential separation of AC(0)[p]-Frege+for all red from TC0-Frege+for all red; (iii) an exponential separation of the hierarchy of constant-depth systems AC(0)/d-Frege+for all red by formulas of depth independent of d. In the propositional case, all these results correspond to major open problems.