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

图和数据库上的许多决策和优化问题都可以用逻辑语言来表示。元算法是不限于某一特定问题的算法。它们可以解决所有可以用某些逻辑公式表示的问题，这使得它们成为一个非常灵活的工具。对于一阶逻辑，可以在某些图类上解决相应的问题，只要这些图类具有特定的结构性质。对于功能更强大的一元二阶逻辑，也存在这样的算法，但只适用于更受限制的图类。在计数问题中，集合的数量和大小起着重要作用。这样的问题不能用一阶逻辑表达，也不能只用有限的方式表达，但实际上是高度相关的。为了对计数问题进行建模，可以定义相应的计数逻辑。在过去的几年里，这一领域已经取得了一些成果，但仍有许多问题有待解决。本项目的目标是研究在哪些图类上可以用高效的元算法来解决哪些计数问题。在这里，我们希望区分精确计数和近似计数，并解决相关问题，如枚举。除了设计高效的算法外，我们还希望找到匹配的下界。这一研究将由以下三个问题开始，这三个问题构成了该项目的基石：我们考虑了一个强大的计数逻辑，对于这个逻辑，我们已经知道即使在非常有限的图类上也不可能进行有效的计算。我们希望为这一逻辑设计一种有效的近似求值算法，并通过对一阶模数逻辑的研究，找到满足奇偶条件的计数问题的元算法。部分支配集问题就是寻找控制图的一半的顶点集。我们研究了一种足够强大的计数逻辑来处理这个和类似的问题。通过这种方式，我们希望有效地解决几个控制问题--以及尽可能通用的图类上的覆盖问题。

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.