Intro to QBF Solving and Proof Complexity

19^th October 2023, 11:00
Friedrich Slivovsky

Abstract

This talk introduces two of the main paradigms in QBF solving: search and expansion. It presents their underlying proof systems, showcases results on their proof complexity, and discusses a connection between proofs and strategies known as 'strategy extraction'. The presentation will also highlight two open questions in the realm of strategy extraction.