# Departmental Seminar

Thursday, September 10th, 2019, 16:30, Sala Verde.

Olaf Beyersdorff (Friedrich Schiller University, Jena)

*Solving and Proof Complexity for SAT and QBF*

*Abstract:* 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.

*Bio:* 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 a 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.