一句话：研究 MSO 扩展在树宽与邻域多样性图上的模型检测复杂度，给出 FPT/XP 算法与 CSP 归约方法。
本文研究 MSO 若干扩展在有界树宽图与有界邻域多样性图上的模型检测复杂度。经典 Courcelle 定理表明 MSO 性质在有界树宽图上可线性时间判定。作者考察全局/局部基数约束（CardMSO、MSO-LCC）与公平目标优化（fairMSO），厘清其表达力关系与线性变体，并给出参数化算法。在邻域多样性上，证明线性局部与全局约束可结合且保持线性 FPT，去掉任一线性性则不可行；对最强扩展给出 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.Comment: An extended abstract appeared in Proceedings of WG 2017
@article{paperbot740,
title = {Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity},
author = {Dušan Knop and Martin Koutecký and Tomáš Masařík and Tomáš Toufar},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:12)2019}
}