中文

固定参数可处理性、可定义性与模型检测

计算复杂性 2007-05-23 v2 计算机科学中的逻辑

摘要

本文从逻辑、更具体地从描述复杂性理论的角度研究参数化复杂性理论。我们提出将各片段一阶逻辑的参数化模型检测问题视为一般性参数化问题,并展示该方法在研究固定参数可处理性与难处理性中的用处。例如,我们建立了存在一阶逻辑的模型检测、关系结构的同态问题以及子结构同构问题之间的等价性。我们的主要可处理性结果显示,当限制于具有排斥次图的输入结构类时,一阶公式的模型检测是固定参数可处理的。在难处理性方面,对每个 t >= 0,我们证明具有 t 次量词交替的一阶公式的模型检测与具有 t 次交替的交错图灵机的参数化停机问题之间的等价性。我们讨论了该交替层次与 Downey 和 Fellows 的 W-层次之间的密切联系。在更抽象的层面上,我们考虑两种称为 Fagin 可定义性与按片可定义性的可定义性形式,它们适用于描述参数化问题。我们给出了所有固定参数可处理问题类 FPT 在有限变量最小不动点逻辑中按片可定义性下的刻画,这令人联想到 Immerman-Vardi 定理在最小不动点逻辑可定义性下对 PTIME 类的刻画。

关键词

引用

@article{arxiv.cs/9910001,
  title  = {Fixed-parameter tractability, definability, and model checking},
  author = {Joerg Flum and Martin Grohe},
  journal= {arXiv preprint arXiv:cs/9910001},
  year   = {2007}
}

备注

To appear in SIAM Journal on Computing