Oliver Kullmann

Oliver Kullmann is an Associate Professor at Swansea University (UK), in the Computer Science department. He is interested in the theoretical and practical aspects of solving hard problems, around SAT and extensions.

Oliver started his career in the field of worst-case upper bounds for SAT algorithms, creating the paradigm which today is known as measure-and-conquer. He discovered the cube-and-conquer scheme, which was successfully applied to solve various hard problems. Another outcome of this early work are practical versions of Extended Resolution, as underlying proof systems of SAT solving.

A different stream of his research connects SAT with various combinatorial theories. Autarky theory (generalised satisfying assignments) and the classification of minimally unsatisfiable CNFs are the two main fields of interest here. Since two years the extensions to DQCNF (dependency quantified CNFs) are investigated.

He is also engaged in solver and software development. The most recent development concerns generators for random DQCNFs.

For the year 2021 the main focus is on solving hard combinatorial problems and putting the cube-and-conquer scheme on a solid theoretical and practical footing.