Faster Existential FO Model Checking on Posets

We improve upon (and give a simpler proof of) a recent result of Bova, Ganian and Szeider (CSL-LICS 2014), which states that the model checking problem for the existential fragment of first order logic and partially ordered sets is fixed-parameter tractable if the width (size of the largest antichain) of the poset is fixed. We give two algorithms which show that the problem is fixed-parameter tractable not only in the size of the formula, but also in the width of the poset. The first algorithm is based on a natural, and easy to understand, reduction to a CSP instance of a special kind, while the second algorithm, with better time complexity, uses a reduction to a restricted variant of the multicoloured clique problem, which is then efficiently solved. We complement these results by showing that, under a certain complexity-theoretical assumption, the existential FO model-checking problem does not have a polynomial kernel.

Authors

• Jan Obdržálek

Keywords

No keywords are indexed for this paper.