A Practical Approach to Courcelle's Theorem
A Practical Approach to Courcelle's Theorem
复制标题
DOI：
10.1016/j.entcs.2009.08.028
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
Joachim Kneis;Alexander Langer
中科院分区：
文献类型：
--
作者：
Joachim Kneis;Alexander Langer
1990年，Courcelle证明了在一元二阶逻辑（Monadic Second-Order Logic，MSO）中定义的每个问题都可以在有界树宽的图上线性时间内解决。这一强大而重要的定理是其他几个固定参数易处理性结果的基础。Courcelle定理的标准证明是构造一个有限的自下而上的树自动机来识别图的树分解。然而，自动机的大小，通常在朗道符号中隐藏为常数，可以变得非常大，并且不能被任何基本函数限制，除非P=NP（弗里克和Grohe，2004）。这使得这个问题在实践中很难解决，因为不可能构造树自动机。针对一个实际的实现，给出了Courcelle定理限制于形式为optU <$Vφ（U）的扩展MSO公式的证明，其中φ是一个带有词汇（adj，U）的一阶公式，且opt∈{min，max}.注意，许多优化问题，如最小顶点覆盖，最小支配集和最大独立集，可以用这样的公式表示。证明使用了一种新的技术，基于使用Hintikka游戏的动态规划的属性。为了证明这种方法的可用性，我们提出了一个实现，解决了这样的公式的图与小路径宽度。事实证明，大常数可以在不太复杂的图上绕过。
In 1990, Courcelle showed that every problem definable in Monadic Second-Order Logic (MSO) can be solved in linear time on graphs with bounded treewidth. This powerful and important theorem is amongst others the foundation for several fixed parameter tractability results. The standard proof of Courcelle's Theorem is to construct a finite bottom-up tree automaton that recognizes a tree decomposition of the graph. However, the size of the automaton, which is usually hidden as a constant in the Landau-notation, can become extremely large and cannot be bounded by any elemental function unless P=NP (Frick and Grohe, 2004). This makes the problem hard to tackle in practice, because it is just impossible to construct the tree automata. Aiming for a practical implementation, we give a proof of Courcelle's Theorem restricted to Extended MSO formulas of the form optU⊆Vφ(U), where φ is a first-order formula with vocabulary (adj, U) and opt∈{min,max}. Note that many optimization problems such as Minimum Vertex Cover, Minimum Dominating Set, and Maximum Independent Set can be expressed by such formulas. The proof uses a new technique based on using Hintikka game properties in dynamic programming. To demonstrate the usability of this approach, we present an implementation that solves such formulas on graphs with small pathwidth. It turns out that the large constants can be circumvented on graphs that are not too complex.