Nonclassical logics: parametrised and enumeration complexity

• Applicant: Privatdozent Dr. Arne Meier
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 247444366

In parameterised complexity, one primary considers problems which cannot be solved in polynomial time. As the name suggests, one investigates parametrisations of the problem which are relevant for practice. Mainly, aiming for a parameter which allows for solving the problem in a runtime which can be modelled as a product of a polynomial in the input length and an arbitrary computable function in the parameter. In such a case, the problem is said to be fixed parameter tractable. A fascinating parametrisation, backdoors, depicts a shortcut to an efficiently solvable subcase of the problem. In temporal logic, which is a fundamental tool in the area of program verification, we investigated such backdoors in the previous project. In this follow-up project, we want to do more research on this concept. We aim for finding a fitting definition which is practical and is closer connected to the temporal formalisms. As well in default logic, a nonmonotonic logic, which is used in artificial intelligence, we found a good notion of backdoors in the previous project. Now we want to precisely classify the parametrised problems and also study how QBF-solvers can be applied in this context. QBF-solvers are programs which operate on a more complex kind of propositional formulas. This kind of formulas can formalise (presumably, that is, under reasonable complexity-theoretic assumptions) considerably more challenging problems. The research on QBF-solvers is very young compared to the highly optimised SAT-solvers (which solve the prominent problem of satisfiability of propositional formulas). The second half of the project deals with dependence logic. Dependencies, for instance on a functional level, play an important role for database problems. However, also other areas of research, e.g. game theory or physical properties can be modeled with this kind of tools. Until today there exists no investigation of the parametrised complexity of problems in this logic. We want to analyse a propositional variant more closely. In this part, we also want to consider the algorithmic task of (parametrised) enumeration. Often it is required to compute the cheapest solution or the $k$-th solution on a given ordering. The enumeration in nonclassical logics, how we consider in this project, is not much treated in research. We want to close this gap and want to classify the enumeration complexity of specific nonmonotonic problems. This analysis will also improve the understanding of enumeration itself.

• DFG Programme: Research Grants