一句话:证明有界路径宽度图上的 FO 性质可在线性时间判定,且对公式依赖为初等,推广有界树深元定理。
Courcelle 定理指出有界树宽图上所有 MSO 可表达性质可线性时间判定,但其隐含常数是随量词交替增长的指数塔,且在树上判定 FO 性质时该非初等下界标准假设下不可改进。本文重新审视该问题,寻找可改进的自然特例。作者证明:当输入图具有有界路径宽度(而非树宽)时,所有 FO 可表达性质都可在对输入公式初等依赖下判定。该结果推广了 Gajarský 与 Hliněný 针对有界树深图的元定理,并显示树宽与路径宽度在复杂度行为上存在罕见差异;同时与有界路径宽度上 MSO 已知需非初等依赖形成鲜明对比。
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.