Alladi Ramakrishnan Hall

Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

Olaf Beyersdorff

Leeds Univ, UK

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 a new semantically-grounded lower bound technique that applies to a whole class of QBF proof systems. We will use this technique to obtain lower bounds for random formulas in QBF analogues of resolution, cutting planes, and polynomial calculus.

The new technique and its application to random formulas are joint work with Joshua Blinkhorn and Luke Hinde.