Abstracts

Quantified Boolean Formulas (QBF) and their proof complexity are not as well understood aspropositional formulas, yet remain an area of interest due to their relation to QBF solving. Proofsystems for QBF provide a theoretical underpinning for the performance of these solvers. We definea novel calculus IR-calc, which enables unification of the principal existing resolution-based QBFcalculi and applies to the more powerful Dependency QBF (DQBF).We completely reveal the relative power of important QBF resolution systems, settling inparticular the relationship between the two different types of resolution-based QBF calculi. Themost challenging part of this comparison is to exhibit hard formulas that underlie the exponentialseparations of the proof systems. In contrast to classical proof complexity we are currently shortof lower bound techniques for QBF proof systems. To this end we exhibit a new proof techniquefor showing lower bounds in QBF proof systems based on strategy extraction. We also find thatthe classical lower bound techniques of the prover-delayer game and feasible interpolation can belifted to a QBF setting and provide new lower bounds.We investigate more powerful proof systems such as extended resolution and Frege systems. Wedefine and investigate new QBF proof systems that mix propositional rules with a reduction rule,we find the strategy extraction technique also works and directly lifts lower bounds from circuitcomplexity. Such a direct transfer from circuit to proof complexity lower bounds has often beenpostulated, but had not been formally established for propositional proof systems prior to this work.This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponentiallower bound for QBF Frege systems operating with AC0[p] circuits. In contrast, any non-triviallower bound for propositional AC0[p]-Frege constitutes a major open problem.