Invited Talk: Proof Complexity of Quantified Boolean Formulas
by Olaf Beyersdorff
Abstract
In this talk we give an overview of the relatively young field of QBF proof complexity. One of the main drivers of the field is the analysis of QBF solvers: powerful algorithms that efficiently solve the classically hard problem of QBF for large classes of practically relevant formulas. 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.Short Bio
Olaf Beyersdorff is Associate Professor for Algorithms and Complexity at the University of Leeds. He received his PhD from Humboldt University Berlin and completed his Habilitation at Leibniz University Hanover. Olaf's main area of research is proof complexity and its connections to computational complexity, logic and solving. In the past few years he worked on QBF proof complexity, proof complexity of non-classical logics, and parameterised proof complexity.Talk slides: PDF
Program
Session 1: 9:00 - 10:30 | |
Florian Lonsing, Martina Seidl | Opening Remarks |
Olaf Beyersdorff | Proof Complexity of Quantified Boolean Formulas (invited talk) |
Gergely Kovásznai | A Survey on DQBF: Formulas, Applications, Solving Approaches |
Coffee Break: 10:30-11:00 | |
Session 2: 11:00-12:30 | |
Paolo Marin, Massimo Narizzano, Luca Pulina, Armando Tacchella and Enrico Giunchiglia | Old Challenges and New Solutions: a Comprehensive Assessment of State-of-the-Art QBF Solvers |
Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe and Leander Tentrup | Encodings of Reactive Synthesis |
Andrew Reynolds, Jasmin Christian Blanchette and Cesare Tinelli | Model Finding for Recursive Functions in SMT |
Haniel Barbosa and Pascal Fontaine | Congruence Closure with Free Variables |
Discussion and closing remarks |
Accepted Contributions
Jakub Szymanik | Quantifiers, Computation, and Cognition (PDF) |
Andrew Reynolds, Jasmin Christian Blanchette and Cesare Tinelli | Model Finding for Recursive Functions in SMT (PDF) (SLIDES) |
Paolo Marin, Massimo Narizzano, Luca Pulina, Armando Tacchella and Enrico Giunchiglia | Old Challenges and New Solutions: a Comprehensive Assessment of State-of-the-Art QBF Solvers (PDF) (SLIDES) |
Haniel Barbosa and Pascal Fontaine | Congruence Closure with Free Variables (Work in Progress) (PDF) (SLIDES) |
Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe and Leander Tentrup | Encodings of Reactive Synthesis (PDF) (SLIDES) |
Gergely Kovásznai | A Survey on DQBF: Formulas, Applications, Solving Approaches (PDF) (SLIDES) |