论文标题
再次重新审视路径宽的一阶逻辑
First Order Logic on Pathwidth Revisited Again
论文作者
论文摘要
Courcelle的著名定理指出，所有可表达的属性都可以在有界树宽的图表上以线性时间来确定。不幸的是，该定理暗示的隐藏常数是指数的塔，其高度随着公式中的每个量词交替而增加。更毁灭性的是，即使我们考虑了在树木上确定可表达的fo可表达特性的更受限制的问题，也无法改善这一点。 在本文中，我们重新审视了这个经过充分研究的主题，并确定了一个自然的特殊情况，实际上，Courcelle定理的依赖性可以改善。具体而言，我们表明，如果输入图具有有界路径（而不是TreeWidth），则可以用对输入公式的基本依赖性来确定所有FO-可表达的属性。这是具有不同复杂性行为的树宽和路径宽度的罕见例子。我们的结果也与有界路径图的MSO逻辑形成鲜明对比，在标准假设下，依赖性必须是非元素的。我们的作品建立在Gajarsk {ou}和Hlin {ě} N {}的基础上，并概括了相应的元理论，用于有限的树深度的图表。
Courcelle's celebrated theorem states that all MSO-expressible properties can be decided in linear time on graphs of bounded treewidth. Unfortunately, the hidden constant implied by this theorem is a tower of exponentials whose height increases with each quantifier alternation in the formula. More devastatingly, this cannot be improved, under standard assumptions, even if we consider the much more restricted problem of deciding FO-expressible properties on trees. In this paper we revisit this well-studied topic and identify a natural special case where the dependence of Courcelle's theorem can, in fact, be improved. Specifically, we show that all FO-expressible properties can be decided with an elementary dependence on the input formula, if the input graph has bounded pathwidth (rather than treewidth). This is a rare example of treewidth and pathwidth having different complexity behaviors. Our result is also in sharp contrast with MSO logic on graphs of bounded pathwidth, where it is known that the dependence has to be non-elementary, under standard assumptions. Our work builds upon, and generalizes, a corresponding meta-theorem by Gajarsk{ý} and Hlin{ě}n{ý} for the more restricted class of graphs of bounded tree-depth.
