一句话：证明在有界局部团宽图类的一阶解释类上，一阶模型检测存在 FPT 算法。
论文研究一阶模型检测在何种图类上可有效判定。解释（interpretation）通过一阶公式重定义边关系，将输入图映射为输出图，可统一刻画取补图或固定幂等操作。作者证明：若图类可由有界局部团宽图类经一阶解释得到，则其上一阶模型检测问题是固定参数可解的（FPT）。该结果覆盖平面图及一般有界亏格图类的解释。为证明此结论，作者在 NIP 类这一极一般框架下开发了新工具，作者认为该工具对未来获得类似结果具有重要价值。
An interpretation is an operation that maps an input graph to an output graph by redefining its edge relation using a first-order formula. This rich framework includes operations such as taking the complement or a fixed power of a graph as (very) special cases. We prove that there is an FPT algorithm for the first-order model checking problem on classes of graphs which are first-order interpretable in classes of graphs with bounded local cliquewidth. Notably, this includes interpretations of planar graphs, and of classes of bounded genus in general. To obtain this result we develop a new tool which works in a very general setting of NIP classes and which we believe can be an important ingredient in obtaining similar results in the future.
@inproceedings{BonnetDGKMST22,
title = {Model Checking on Interpretations of Classes of Bounded Local Cliquewidth},
author = {Édouard Bonnet and Jan Dreier and Jakub Gajarský and Stephan Kreutzer and Nikolas Mählmann and Pierre Simon and Szymon Toruńczyk},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533367}
}