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 (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)\cdot n^2)\) on \(n\)-element posets of width \(w\), compared to \(O(g(|\phi |)\cdot 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.
Research funded by the Czech Science Foundation under grant 14-03501S.
Sebastian Ordyniak: Research funded by Employment of Newly Graduated Doctors of Science for Scientific Excellence (CZ.1.07/2.3.00/30.0009).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alon, N., Gutin, G., Kim, E., Szeider, S., Yeo, A.: Solving MAX-r-SAT above a tight lower bound. Algorithmica 61(3), 638–655 (2011)
Bodlaender, H.L.: Kernelization: New Upper and Lower Bound Techniques. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 17–37. Springer, Heidelberg (2009)
Bodlaender, H.L., Downey, R., Fellows, M., Hermelin, D.: On problems without polynomial kernels. J. Comput. System Sci. 75(8), 423–434 (2009)
Bova, S., Ganian, R., Szeider, S.: Model checking existential logic on partially ordered sets. In: CSL-LICS 2014 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Article No. 21. ACM, New York (2014), http://dx.doi.org/10.1145/2603088.2603110, ISBN: 978-1-4503-2886-9
Cai, L., Chen, J., Downey, R., Fellows, M.: Advice classes of parameterized tractability. Ann. Pure Appl. Logic 84(1), 119–138 (1997)
Downey, R., Fellows, M.: Parameterized complexity. Monographs in Computer Science. Springer (1999)
Felsner, S., Raghavan, V., Spinrad, J.: Recognition algorithms for orders of small width and graphs of small dilworth number. Order 20(4), 351–364 (2003)
Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer (2006)
Gajarský, J., Hliněný, P., Obdržálek, J., Ordyniak, S.: Faster existential FO model checking on posets. http://arxiv.org/abs/1409.4433 (2014)
Grohe, M., Kreutzer, S., Siebertz, S.: Deciding first-order properties of nowhere dense graphs. In: STOC 2014, pp. 89–98. ACM (2014)
Jeavons, P., Cohen, D., Gyssens, M.: Closure properties of constraints. J. ACM 44(4), 527–548 (1997)
Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford Lecture Ser. Math. Appl. OUP (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gajarský, J., Hliněný, P., Obdržálek, J., Ordyniak, S. (2014). Faster Existential FO Model Checking on Posets. In: Ahn, HK., Shin, CS. (eds) Algorithms and Computation. ISAAC 2014. Lecture Notes in Computer Science(), vol 8889. Springer, Cham. https://doi.org/10.1007/978-3-319-13075-0_35
Download citation
DOI: https://doi.org/10.1007/978-3-319-13075-0_35
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-13074-3
Online ISBN: 978-3-319-13075-0
eBook Packages: Computer ScienceComputer Science (R0)