参数复杂性、SAT求解器和树宽度

Parameterized complexity is a very active subfield of theoretical computer science. Compared to classical theory of algorithms and complexity which is built on the central notion of polynomial time computability, it provides more flexibility for algorithm design and more refined framework for complexity analysis by allowing exponential time algorithms whose superpolynomial behavior is confined to some small parameters. In the last 20 years it has found numerous successful applications in graph algorithms, databases, bioinformatics, etc. Nevertheless, many problems remain unsolved, and many potential areas unexplored. The proposed project is to study the following new problems, more or less centered on the well-known notion of treewidth. 1) Parameterized complexity analysis of SAT solvers. SAT is one of the most important NP-complete problems, with very important applications in industry. Many SAT solvers prove to be very efficient in practice, despite the problem's general NP-hardness. We propose to analyze those SAT solvers from the parameterized complexity perspective. In particular we want to understand whether there are hidden parameters for practical SAT instances that make those SAT solvers efficient. One good starting point is treewidth. 2) Treewidth plays a ubiquitous role in parameterized complexity. In particular, for many problems it provides a precise borderline between tractability and hardness. There are still many open problems concerning treewidth. Due to its applications in algorithmic meta-theorems, we want to study how edge deletion affects the treewidth; for analysis in programming languages, we look for axiomazation of graphs with bounded treewidth; to understand the expressive power of monadic second-order logic, we look at the order-invariant MSO.

参数复杂性是目前在理论计算机科学中非常活跃的一个分支。相比以多项式时间算法为核心的经典算法和复杂性理论，通过允许超多项式行为局限于某些小参数的指数时间算法，它为算法设计提供了更多的灵活性和复杂性分析更为精细的框架。我们计划研究以下的一些基于树宽度的比较新颖的参数复杂性问题。1)SAT问题在工业界有着极为重要的应用。虽然其在一般意义上是NP难的，但许多SAT问题的求解器在实际使用中非常高效。我们计划从参数复杂性角度来分析这些SAT求解器。特别的是，我们希望理解对于实际应用中出现的SAT实例是否存在一些隐藏的参数，它们导致求解器的高效。该研究一个很好的起点就是树宽度有界的实例。2)对于很多参数计算问题，树宽度给出了高效可解和计算困难间的精确边界。但还有一些关于树宽度及其相关的算法问题仍有待解决。如：我们希望研究删点操作对树宽度的影响；针对程序语言的研究，我们试图给出树宽度有界图的公理系统；为了理解monadic二阶逻辑(MSO)的表达能力，我们计划考察独立于序的MSO。

本项目的主题是参数复杂性、SAT求解器和树宽度的研究，其总体目标是利用参数复杂性的观点来分析一些基于逻辑和图论问题比经典复杂性更精细的算法和复杂性。在参数复杂性框架下每个计算问题的输入都包含了一部分较小的参数，例如逻辑问题中的逻辑公式和图论问题中所求节点集的大小。作为主要结果，我们在以下几个问题上取得重要进展。..1. 我们解决了基于树宽度的子图同构问题参数复杂性猜想的重要特例-grid图和wall图。子图同构问题包含了很多自然的算法图论问题，如团问题、路径问题。因此理解它的复杂性有重要的理论和应用价值。人们猜想这个问题难易完全取决于子图的树宽度。我们的结果对彻底理解这个问题又迈出了重要的一步。..2. 对于SAT问题我们证明了如果不可满足的CNF公式的incidence graph的树宽度有界，那么它就等价于一个有FPT大小消解证明的3CNF公式，这为理解SAT求解器在树宽度有界的CNF公式上的行为建立了一定的基础。..3. 我们证明了参数支配集问题的常数近似是W[1]难的。支配集问题是一个重要的NP完全的图论问题，它的参数版本是W[2]完全的。目前关于它的一个重要研究方向是参数近似算法，即在固定参数时间下能否就算一个接近最优解的支配集。我们的结果是这个领域的一个重要进展。..4. 我们研究了一些比FPT更小的参数复杂性类，包括参数对数空间和参数AC0类，建立一系列图论和逻辑问题相对这些类的上下界。相比固定参数可解类(FPT)，关于这些类的研究还处于初级阶段。我们得到相对于参数AC0类几个下界是这个方向最早的一批结果。而对于参数对数空间，我们建立著名的Savitch定理和参数空间复杂性的关联。