Solving and Proof Complexity for SAT and QBF

Relatore:  Prof. Olaf Beyersdorff - Friedrich Schiller University, Jena
  giovedì 3 ottobre 2019 alle ore 16.30 Sala Verde
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 


Data pubblicazione
2 settembre 2019

Offerta formativa