Abgeschlossene Forschungsprojekte

Abstract: In the usual lecture format, a large number of people come together and spend most of the time in reception mode. The teacher is at the front presenting the material. In mathematical lectures where proofs are presented, it is almost impossible to find the right pace for all listeners to follow. After the lecture, everyone goes home and questions arise while revising the material. The concept of the flipped lecture or inverted classroom starts right here, in order to use the time spent in class more meaningfully and effectively. With the help of videos and other learning materials, the material is worked on and understood in small learning groups or alone before the actual event, so that the questions that arise can then be discussed and gaps in understanding can be closed during the time spent in class. This concept is didactically recognised. [1]
In this project, the course ‘Complexity of Algorithms’, which is part of the compulsory curriculum of the computer science and technical computer science degree programmes at Leibniz Universität Hannover, was taught using this method. Around 300 students took part in the course. Traditionally, the module consisted of lecture and exercise units. In the summer semester of 2019, a pilot phase was conducted with old lecture recordings in the course ‘Complexity of Algorithms’. The accompanying evaluation using the Teaching Analysis Poll (TAP), two teaching visits by didacticians and the teaching evaluation showed a highly positive acceptance by the students due to the improvement of the learning situation. As part of this project, videos and learning materials were prepared in a didactically meaningful way and parts of the course were optimised.

[1] J. Werner, S. Bayer, C. Ebel and C. Spannagel, Hrsg., Flipped Classroom - Zeit für deinen Unterricht, Bertelsmann Stiftung, 2018.

Abstract: The theory of parameterised complexity (Downey, Fellows 1999) considers so-called parameterisations in order to better understand the inherent difficulty of problems. A simple example of such a parameterisation for the satisfiability problem of propositional formulas (SAT) is the number of variables of a given formula. Under this parameterisation, SAT can be solved in a runtime of 2•|Vars(F)|•|F|, where F is the given formula. Such runtimes are said to be ‘fixed-parameter tractable’ (or, in short, FPT). This means that, when the parameter is considered constant, the runtime is polynomial and the degree of the polynomial does not depend on the value of the parameter. In contrast to this are running times of the form n•f(k), where the corresponding problems are summarised in the class XP (for input length n). A hierarchy of so-called ‘Weft’ classes W[i] exists between FPT and XP. It is not known whether any of the inclusions from W[i] to W[i+1] is strict or whether FPT is strictly contained in W[1].

Counting problems have played a key role in many breakthroughs in structural complexity theory. A decade ago, Flum and Grohe (2002) developed a theory of parameterised counting problems. Flum and Grohe showed that counting cycles of length k in an oriented graph is #P=W[1]-complete (which is the counting version of class W[1]; usually, the number of accepting paths is counted here). Furthermore, cycle counting of solutions of model-checking problems for first-order logic was used to characterise the so-called #A hierarchy. Despite intensive research efforts, so far there has been no success in translating classical results, such as the Toda theorem, into the parameterised world.

In descriptive complexity theory, complexity classes are characterised by sets of formulas. In a groundbreaking result, Fagin (1973) showed that the class NP coincides with the set of all existential second-order formulas. Immerman (1982) provided a characterisation of the class P and showed that regular languages can be characterised by monadic second-order formulas (MSO). Saluja and Subrahmaniam (1998) achieved a logical characterisation of #P by counting models of an FO formula. Furthermore, Kontinen (2008) classified the counting hierarchy by logics with generalized quantifiers. In 2003, Flum and Grohe showed that logical characterizations of classical complexity classes, such as P, NP and PSPACE, can also be transferred to the parameterized approach. Furthermore, in 2007 they gave a logical characterization of the W* hierarchy.

In this project, we want to characterise parameterised decision and counting classes in terms of sets of logical formulas. We divide the project into two sections.

Characterisation of parameterised complexity classes
As already mentioned, the W* hierarchy has a Fagin-type characterisation by logical formulas. However, there is no such approach for the W hierarchy, for FPT or for other classes that are restricted with respect to parallelism and space. We plan to find logical characterisations of FPT and parameterised variants of complexity classes, such as para-AC[0], para-WNC[1], para-WL and para-WNL, which were defined by Elberfeld, Stockhusen and Tantau (2015).
Characterisation of parameterised counting classes
So far, no logical characterisations of the parameterised counting classes introduced by Flum and Grohe are known. We aim to describe classes within the #W[P] hierarchy. More precisely, we will work on the following questions:
Find characterisations of #W[1] and #W[P] with respect to counting in FO or other associated logics.
Find logical characterisations of the parameterised analogues of Montoya's polynomial time hierarchy (2008).
Attempt to transfer the logical characterisation of Kontinen's counting hierarchy (2009) to the parameterised setting.
Within both sections, we will study parameterisations of natural counting problems, such as counting paths in directed graphs or paths in pushdown automata. Furthermore, the question arises as to how tools from finite model theory (locality, Ehrenfeucht-Fraïssé games, zero-one laws,...) can be used to find answers to the above questions.

Abstract: The theory of parameterised complexity is primarily concerned with problems that cannot be solved in polynomial time. As the name suggests, the aim is to investigate parameterisations of the problem that are relevant in practice. The goal is to find a parameter such that the problem can be solved in a runtime that can be represented as a product of a polynomial of the input length and an arbitrary function in the parameter. In this case, the problem is said to be fixed parameter tractable.

Backdoors
A very interesting parameter is backdoors. These backdoors are supposed to provide a figurative shortcut to a sub-problem that can be solved efficiently. In the previous project, such backdoors were investigated in temporal logic, which is a fundamental tool in the field of program verification. In the follow-up project, further research will now be conducted on this concept. The aim is to find a suitable definition that is more practical and more closely interwoven with the temporal concepts. In the previous project, a coherent definition was also found in default logic, a non-monotonic logic used in the fields of artificial intelligence. Now, in addition to a precise classification of the problems parameterised in this way, the applicability of so-called QBF solvers is to be investigated. QBF solvers are programs that attempt to solve a more complex type of propositional logic formula. These types of formulas can (presumably, that is, under reasonable complexity-theoretic assumptions) formalise significantly stronger problems. Research on QBF solvers is still quite young compared to the highly optimised SAT solvers (which solve the prominent problem of the satisfiability of propositional formulas).

(Parametrised) Enumeration and Dependency Logic
Dependencies, whether on a functional level, play a role in the area of databases. However, other areas, such as game theory or physical properties, can also be modelled with this tool. So far, there have been no investigations into the parameterised complexity of problems in this logic. We would now like to analyse a propositional variant of this logic in more detail. In this section, we also want to address the algorithmic question of (parameterised) enumeration. Often it is interesting to know the most favourable solution or the k-th solution with respect to a certain order. Enumeration for non-classical logics, as we are investigating in this project, has so far been the subject of very little research. We want to close this gap and classify certain non-monotone formalisms in this regard. This analysis also serves to better understand enumeration as a task in itself.