一句话：证明在排除固定拓扑子式的图类上，带不相交路径谓词的一阶逻辑模型检测是固定参数可处理的。
论文研究扩充一阶逻辑 FO+DP 的模型检测问题。该逻辑在 FO 上加入原子谓词 dpk[(x1,y1),…,(xk,yk)]，表达各点对之间存在内部顶点不相交路径。作者证明：对任意排除某个固定图作为拓扑子式的图类，FO+DP 的模型检测问题是固定参数可处理的（FPT）。这推广了 Golovach 等 [SODA 2023] 对 minor-closed 图类的算法。结合已知在未排除拓扑子式的 subgraph-closed 图类上的困难性（在编码效率的温和条件下），该结果基本刻画了此类封闭图类上该逻辑可处理模型检测的边界。
Disjoint-paths logic, denoted FO+ DP, extends first-order logic (FO) with atomic predicates dpk[(x1, y1), …, (xk, yk)], expressing the existence of internally vertex-disjoint paths between xi and yi, for 1 ≤ i ≤ k. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+ DP is fixed-parameter tractable. This extends the model checking algorithm of Golovach et al. [SODA 2023] for FO+ DP for minor-closed graph classes. It also essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition on efficiency of encoding).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{SchirrmacherSST24,
title = {Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes},
author = {Nicole Schirrmacher and Sebastian Siebertz and Giannos Stamoulis and Dimitrios M. Thilikos and Alexandre Vigny},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662089}
}