Solving and Proof Complexity for SAT and QBF

Prof. Olaf Beyersdorff - Friedrich Schiller University, Jena
Date and time
Thursday, October 3, 2019 at 4:30 PM - Sala Verde
Programme Director
External reference
Publication date
September 2, 2019
Computer Science  


SAT and QBF solvers have become ubiquitous tools for the solution of hard computational problems from almost all application domains. In this talk we explain the underlying algorithmic principles of solving, both for propositional satisfiability (SAT) and for the more complex case of quantified Boolean formulas (QBF). Particular emphasis will be placed on how these solving approaches can be modelled proof theoretically and which techniques are available to evaluate their proof complexity.
Since 2018 Olaf Beyersdorff is Professor of Theoretical Computer Science at the Friedrich Schiller University Jena. His research interests are in algorithms, complexity, computational logic, and in particular proof complexity. Before coming to Jena he spent six years at the University of Leeds, as Professor of Computational Logic (2017-18), Associate Professor (2015-17), and Lecturer (2012-15). Since 2018 he is visiting professor at the University of Leeds. Before that he was a visiting professor (2011/12) and visiting researcher (2009/10) at Sapienza University Rome, Lecturer at Leibniz University Hanover (2007-12) and postdoc at Humboldt University Berlin (2006/07). Beyersdorff obtained a PhD from Humboldt University Berlin in 2006 and completed the habilitation at Leibniz University Hanover in 2011.
Contact person: Peter Schuster 

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234