Foundations of Efficient Model Checking for Counting Logics on Structurally Sparse Graph Classes

• Applicant: Professor Dr. Peter Rossmanith
• Subject Area: Theoretical Computer Science
• Term: from 2019 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 426003173

Many decision and optimization problems on graphs and databases can be expressed in the language of logic. Meta-algorithms are algorithms that are not restricted to one particular problem. They can solve all problems that can be expressed by certain logical formulas, which makes them a very flexible tool.Several such meta-algorithms are already known. For first order logic the corresponding problems can be solved on certain graph classes as long as the graph classes have specific structural properties. For the more powerful monadic second order logic such algorithms exist, too, but work only on more restricted graph classes.In counting problems the number and sizes of sets play an important role. Such problems cannot be expressed in first order logic or only in a restricted way, but are practically highly relevant. To model counting problems it is possible to define corresponding counting logics. In the last years some results were achieved in this area, but many questions are still open.The goal of this project is to investigate which counting problems can be solved on what graph classes by efficient meta-algorithms. Here we want to distinguish between exact and approximate counting and also work on related problems like enumeration. Besides designing efficient algorithms we also want to find matching lower bounds. This line of research will be initiated by the following three problems that form a corner stone of the project:We consider a powerful counting logic, for which we already know that efficient evaluation is impossible even on very restricted graph classes. We want to design an efficient approximate evaluation algorithm for this logic.Furthermore we want to find meta-algorithms for counting problems with parity conditions by investigating first order logic with modulo counting.The partial dominating set problem is to find a set of vertices that dominate half of the graph. We investigate a counting logic that ispowerful enough to handle this and similar problems. In that way we want efficiently to solve several domination- and covering problems on graph classes that are as general as possible.

• DFG Programme: Research Grants