This talk will start with an overview of the relatively young field of QBF proof complexity, explaining QBF proof systems (including QBF resolution) and an assessment of which lower bound techniques are available for QBF proof systems. In the main part of the talk, I will explain hardness characterisations for QBF proof systems in terms of circuit complexity, yielding very direct connections between circuit lower bounds and QBF proof system lower bounds. The talk will also cover the relations between QBF resolution and QCDCL solving algorithms. Modelling QCDCL as proof systems we show that QCDCL and Q-Resolution are incomparable.

This talk is based on two recent papers, joint with Joshua Blinkhorn and Meena Mahajan (LICS'20) and with Benjamin Boehm (ITCS'21).