Proof Complexity of Quantified Boolean Formulas
Speaker:
Olaf Beyersdorff, University of Leeds
Date and Time:
Thursday, August 18, 2016 - 2:30pm to 3:00pm
Location:
Bahen Building, Room 1200
Abstract:
This talk will give an overview of the relatively young field of QBF proof complexity. We explain the main resolution-based proof systems for QBF, modelling CDCL and expansion-based solving. In the main part of the talk we will give an overview of current lower bound techniques (and their limitations) for QBF systems. In particular, we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths of proofs lower bounds.