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

结构稀疏图类计数逻辑的高效模型检查基础

• 批准号: 426003173
• 负责人: Professor Dr. Peter Rossmanith
• 金额: --
• 依托单位: Informatik 1 - Lehrgebiet Theoretische Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2019
• 资助国家: 德国
• 起止时间: 2018-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/426003173?language=en
• 关键词: Foundations; Efficient; Model; Checking; Counting

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.

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