arXiv 1504.041152015-04cs.LOcs.DM

宽度有界偏序集上的FO模型检验

FO Model Checking on Posets of Bounded Width

Jakub Gajarský, Petr Hliněný, Daniel Lokshtanov, Jan Obdržálek, Sebastian Ordyniak, M. S. Ramanujan, Saket Saurabh

备注：: Minor correction, p.5, def. of τ_{s+1}: instead of an induced subdigraph of D_s, we use the appropriate relational structure formed from this subdigrph

摘要：

在过去的二十年中，研究一阶（FO）模型检验算法的主要焦点一直是稀疏关系结构-最终由Grohe，Kreutzer和Siebertz提出的FPT算法，用于对无处密集的图类进行FO模型检验[STOC'14]，密集结构最近才开始引起人们的注意。Bova，Ganian和Szeider [LICS'14]发起了对偏序集（偏序集）上FO模型检验复杂性的研究。Bova、Ganian和Szeider证明了模型检验存在FO逻辑在有界宽度的偏序集上是固定参数可处理的（FPT），其中偏序集的宽度是偏序集中最大反链的大小。然而，对于有界宽度偏序集上的一般FO模型检验，FPT算法的存在性仍然是开放的。我们给出了一个算法，它以宽度为$w$的$n$元偏序集$\cal P$和FO逻辑公式$ϕ$为输入，判定$ϕ$在时间$f(ϕ,w)\cdot n^2$上是否在$\cal P$上成立.

英文摘要：

Over the past two decades the main focus of research into first-order (FO) model checking algorithms have been sparse relational structures-culminating in the FPT-algorithm by Grohe, Kreutzer and Siebertz for FO model checking of nowhere dense classes of graphs [STOC'14], with dense structures starting to attract attention only recently. Bova, Ganian and Szeider [LICS'14] initiated the study of the complexity of FO model checking on partially ordered sets (posets). Bova, Ganian and Szeider showed that model checking existential FO logic is fixed-parameter tractable (FPT) on posets of bounded width, where the width of a poset is the size of the largest antichain in the poset. The existence of an FPT algorithm for general FO model checking on posets of bounded width, however, remained open. We resolve this question in the positive by giving an algorithm that takes as its input an $n$-element poset $\cal P$ of width $w$ and an FO logic formula $ϕ$, and determines whether $ϕ$ holds on $\cal P$ in time $f(ϕ,w)\cdot n^2$.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

摘要：

英文摘要：

相关论文