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)