面向平面性与一阶逻辑图修改的算法元定理

一般而言，图修改问题由图修改操作$\boxtimes$和目标图性质${\cal P}$定义。通常，修改操作$\boxtimes$可以是顶点删除、边删除、边收缩或边添加，问题是给定图$G$和整数$k$，是否在$G$上应用$k$次操作$\boxtimes$后能将$G$变换为属于${\cal P}$的图。该问题已针对$\boxtimes$和${\cal P}$的特定实例化被广泛研究。本文我们考虑一般性质${\cal P}_{{\phi}}$：既是平面的，且是某个一阶逻辑句子${\phi}$（一个FOL句子）的模型。我们称相应的元问题为图$\boxtimes$-修改至平面性与${\phi}$，并证明如下算法元定理：存在函数$f:\Bbb{N}^{2}\to\Bbb{N}$，使得对每个$\boxtimes$和每个FOL句子${\phi}$，图$\boxtimes$-修改至平面性与${\phi}$可在$f(k,|{\phi}|)\cdot n^2$时间内求解。证明构成了图算法中两种不同经典技术的混合。其一是无关顶点技术，通常用于图子式语境并处理如平面性或曲面可嵌入性（不可由FOL表达）的性质；其二是Gaifman局部性定理的使用，该定理是FOL可表达问题的元算法研究的理论基础。