超越MSO的简化算法元定理：树宽与邻域多样性
Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
AI总结：
本文研究了MSO逻辑扩展在树宽和邻域多样性图上的计算复杂性，提出多项式时间算法并展示了通过CSP形式化的新方法。
摘要：
本文确定了在两个图类上几种MSO逻辑扩展的模型检查计算复杂性：具有界树宽的图和具有界邻域多样性的图。Courcelle的经典定理指出，任何在MSO中可定义的图性质都能在具有界树宽的图上以线性时间决定。类似Courcelle的算法元定理用于推广各种图类上的已知正结果。我们探讨并扩展了三种之前研究的MSO扩展：全局和局部基数约束（CardMSO和MSO-LCC）以及优化公平目标函数（fairMSO）。首先，我们展示了这些MSO扩展在表达能力上的相互关系。此外，我们强调了某些新引入扩展的某种“线性”特性，这在后续中发挥了重要作用。其次，我们为上述结构参数提供了参数化算法。在邻域多样性方面，我们展示了如何将局部和全局基数约束的线性变体结合起来，同时保持线性（FPT）运行时间，但若移除其中的线性特性则不可能。此外，我们为所研究的最强大的扩展，即全局和局部约束的结合，提供了多项式时间（XP）算法。此外，我们还为具有界树宽的图提供了相同的扩展的多项式时间（XP）算法。此外，我们提出了一种通过形式化为约束满足问题（CSP）来推导具有界树宽的图的XP算法的一般过程。这展示了与标准动态规划形式化不同的另一种方法。
英文摘要：
This paper settles the computational complexity of model checking of several extensions of the monadic second order (MSO) logic on two classes of graphs: graphs of bounded treewidth and graphs of bounded neighborhood diversity. A classical theorem of Courcelle states that any graph property definable in MSO is decidable in linear time on graphs of bounded treewidth. Algorithmic metatheorems like Courcelle's serve to generalize known positive results on various graph classes. We explore and extend three previously studied MSO extensions: global and local cardinality constraints (CardMSO and MSO-LCC) and optimizing the fair objective function (fairMSO). First, we show how these extensions of MSO relate to each other in their expressive power. Furthermore, we highlight a certain "linearity" of some of the newly introduced extensions which turns out to play an important role. Second, we provide parameterized algorithm for the aforementioned structural parameters. On the side of neighborhood diversity, we show that combining the linear variants of local and global cardinality constraints is possible while keeping the linear (FPT) runtime but removing linearity of either makes this impossible. Moreover, we provide a polynomial time (XP) algorithm for the most powerful of studied extensions, i.e. the combination of global and local constraints. Furthermore, we show a polynomial time (XP) algorithm on graphs of bounded treewidth for the same extension. In addition, we propose a general procedure of deriving XP algorithms on graphs on bounded treewidth via formulation as Constraint Satisfaction Problems (CSP). This shows an alternate approach as compared to standard dynamic programming formulations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
