Institute of Theoretical Computer Science Research Projects
Nonclassical Logics: Parameterised Complexity and Enumeration
List of selected publications

Project Description

In the area of parameterised complexity theory one primary studies problems that cannot be solved in polynomial time. As the name suggests, one studies parameters of the problem relevant for practice. One aims for parameters such that the problem can be solved in a runtime that is a product of a polynomial in the input length and a computable function in the parameter. Problems that can be solved with such a runtime are called fixed-parameter tractable.

Backdoors

A very intriguing parameter are so-called backdoor sets. Such sets are intuitively mimicking a short-cut to an efficient sub-case of the problem. In temporal logics---a fundamental tool in the area of program verification---we studied already the concept of backdoors [paper reference to journal LTL-backdoors paper]. Currently, we want to refocus on that parameter and find a better definition of backdoor sets which are more relevant to practice. Also in default logic, a nonmonotonic logic used in artificial intelligence, a fitting definition has been found [cite DL-Backdoor conference paper]. Now, we want to improve the classification regarding matching upper and lower bounds. Furthermore, we will study how QBF-solvers could improve in this context our results. QBF-solvers are programs which investigate the satisfiability of a more complex kind of propositional formulas. Such kind of formulas presumably can formalise stronger problems. Research on such solvers is young compared to highly optimised SAT-solvers.

(Parameterised) Enumeration and Dependence Logic

Dependencies on a functional level play a significant role in the area of databases. However, also in other areas as, for instance, game theory or physics make use of this concept. Currently, no parameterised analyses of problems in such logics of dependence and independence exist. We want to initiate a systematic study and start with the propositional variant. Also, the study of (parameterised) enumeration complexity is a part of our investigations. Here, the cheapest or k-th solution could be of interest requiring the study of ordered enumeration instead.