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.