Faster Existential FO Model Checking on Posets

TL;DR

This paper presents a more efficient fixed-parameter tractable algorithm for existential FO model checking on posets, improving previous results in runtime and simplicity, and also discusses kernelization limitations.

Contribution

It improves the runtime and simplicity of existing FPT algorithms for existential FO model checking on posets and analyzes kernelization complexity.

Findings

Algorithm runtime is O(f(|φ|,w))·n^2 for posets of width w.

Previous algorithms had runtime O(g(|φ|))·n^{h(w)}.

Existential FO model checking likely has no polynomial kernel under certain assumptions.

Abstract

We prove that the model checking problem for the existential fragment of first-order (FO) logic on partially ordered sets is fixed-parameter tractable (FPT) with respect to the formula and the width of a poset (the maximum size of an antichain). While there is a long line of research into FO model checking on graphs, the study of this problem on posets has been initiated just recently by Bova, Ganian and Szeider (CSL-LICS 2014), who proved that the existential fragment of FO has an FPT algorithm for a poset of fixed width. We improve upon their result in two ways: (1) the runtime of our algorithm is O(f(|{\phi}|,w).n^2) on n-element posets of width w, compared to O(g(|{\phi}|). n^{h(w)}) of Bova et al., and (2) our proofs are simpler and easier to follow. We complement this result by showing that, under a certain complexity-theoretical assumption, the existential FO model checking problem does not have a polynomial kernel.