论文标题
双宽度I：可拖动的FO模型检查
Twin-width I: tractable FO model checking
论文作者
论文摘要
受到Guillemot和Marx [Soda '14]的排列定义的宽度不变的启发，我们在图和矩阵上介绍了双宽度的概念。适当的小关闭类，有限的等级宽度图，地图图，$ k_t $ - 免费的单位$ d $ - 维数球图，具有有界尺寸的抗小节的posets和Dimension-2 posets的适当子类均具有有限的双宽度。在所有这些类（没有几何嵌入的地图图除外），我们展示了如何在多项式时间计算$ d $ - 扣除的序列，见证双宽度最多是$ d $。我们表明，FO模型检查，即确定给定的一阶公式$ ϕ $是否对给定的二进制结构$ g $在域上$ d $评估为true，如果有证人的给予，则在有限的双胞胎宽度上为$ | ϕ | $。更准确地说，我们的算法在时间$ f（d，| ϕ |）\ cdot | d | $中给出了$ d $ - 收集序列，其中$ f $是可计算但非元素的功能。我们还证明，有界的双宽度是通过FO解释和转导（允许诸如平方或补充图）的操作来保留的。这统一并显着扩展了对非单调类别的FO模型检查的固定参数障碍的知识，例如Gajarský等人在有界宽度POSET上的FPT算法。 [FOCS '15]。
Inspired by a width invariant defined on permutations by Guillemot and Marx [SODA '14], we introduce the notion of twin-width on graphs and on matrices. Proper minor-closed classes, bounded rank-width graphs, map graphs, $K_t$-free unit $d$-dimensional ball graphs, posets with antichains of bounded size, and proper subclasses of dimension-2 posets all have bounded twin-width. On all these classes (except map graphs without geometric embedding) we show how to compute in polynomial time a sequence of $d$-contractions, witness that the twin-width is at most $d$. We show that FO model checking, that is deciding if a given first-order formula $ϕ$ evaluates to true for a given binary structure $G$ on a domain $D$, is FPT in $|ϕ|$ on classes of bounded twin-width, provided the witness is given. More precisely, being given a $d$-contraction sequence for $G$, our algorithm runs in time $f(d,|ϕ|) \cdot |D|$ where $f$ is a computable but non-elementary function. We also prove that bounded twin-width is preserved by FO interpretations and transductions (allowing operations such as squaring or complementing a graph). This unifies and significantly extends the knowledge on fixed-parameter tractability of FO model checking on non-monotone classes, such as the FPT algorithm on bounded-width posets by Gajarský et al. [FOCS '15].
