Simplified algorithmic metatheorems beyond MSO: treewidth and neighborhood diversity. (English) Zbl 1427.68125
Summary: This paper settles the computational complexity of model checking of several extensions of the monadic second order (MSO) logic on two classes of graphs: graphs of bounded treewidth and graphs of bounded neighborhood diversity.
A classical theorem of Courcelle states that any graph property definable in MSO is decidable in linear time on graphs of bounded treewidth. Algorithmic metatheorems like Courcelle’s serve to generalize known positive results on various graph classes. We explore and extend three previously studied MSO extensions: global and local cardinality constraints (CardMSO and MSO-LCC) and optimizing the fair objective function (fairMSO).
First, we show how these extensions of MSO relate to each other in their expressive power. Furthermore, we highlight a certain “linearity” of some of the newly introduced extensions which turns out to play an important role. Second, we provide parameterized algorithm for the aforementioned structural parameters. On the side of neighborhood diversity, we show that combining the linear variants of local and global cardinality constraints is possible while keeping the linear (FPT) runtime but removing linearity of either makes this impossible assuming \(\mathsf{FPT}\neq\mathsf{W[1]}\). Moreover, we provide a polynomial time (XP) algorithm for the most powerful of studied extensions, i.e. the combination of global and local constraints. Furthermore, we show a polynomial time (XP) algorithm on graphs of bounded treewidth for the same extension. In addition, we propose a general procedure of deriving XP algorithms on graphs on bounded treewidth via formulation as Constraint Satisfaction Problems (CSPs). This shows an alternate approach as compared to standard dynamic programming formulations.
A classical theorem of Courcelle states that any graph property definable in MSO is decidable in linear time on graphs of bounded treewidth. Algorithmic metatheorems like Courcelle’s serve to generalize known positive results on various graph classes. We explore and extend three previously studied MSO extensions: global and local cardinality constraints (CardMSO and MSO-LCC) and optimizing the fair objective function (fairMSO).
First, we show how these extensions of MSO relate to each other in their expressive power. Furthermore, we highlight a certain “linearity” of some of the newly introduced extensions which turns out to play an important role. Second, we provide parameterized algorithm for the aforementioned structural parameters. On the side of neighborhood diversity, we show that combining the linear variants of local and global cardinality constraints is possible while keeping the linear (FPT) runtime but removing linearity of either makes this impossible assuming \(\mathsf{FPT}\neq\mathsf{W[1]}\). Moreover, we provide a polynomial time (XP) algorithm for the most powerful of studied extensions, i.e. the combination of global and local constraints. Furthermore, we show a polynomial time (XP) algorithm on graphs of bounded treewidth for the same extension. In addition, we propose a general procedure of deriving XP algorithms on graphs on bounded treewidth via formulation as Constraint Satisfaction Problems (CSPs). This shows an alternate approach as compared to standard dynamic programming formulations.
MSC:
| 68Q25 | Analysis of algorithms and problem complexity |
| 03B16 | Higher-order logic |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68R10 | Graph theory (including graph drawing) in computer science |
References:
| [1] | Sancrey R. Alves, Konrad K. Dabrowski, Lu´erbio Faria, Sulamita Klein, Ignasi Sau, and U´everton dos Santos Souza. On the (parameterized) complexity of recognizing well-covered (r, l)-graphs. In · Zbl 1483.68247 |
| [2] | N.R. Aravind, Subrahmanyam Kalyanasundaram, Anjeneya S. Kare, and Juho Lauri. Algorithms and hardness results for happy coloring problems. 2017. arXiv:1705.08282. · Zbl 1454.68092 |
| [3] | Ren´e van Bevern, Andreas E. Feldmann, Manuel Sorge, and Ondˇrej Such´y. On the parameterized complexity of computing balanced partitions in graphs. Theory of Computing Systems, 57(1):1-35, 2015. doi:10.1007/s00224-014-9557-5. · Zbl 1329.68150 |
| [4] | Hans L. Bodlaender. A linear time algorithm for finding tree-decompositions of small treewidth. In STOC, pages 226-234, 1993. doi:10.1145/167088.167161. · Zbl 1310.05194 |
| [5] | Hans L. Bodlaender. Treewidth: characterizations, applications, and computations. In WG, volume 4271 of Lecture Notes in Computer Science, pages 1-14. Springer, 2006. doi:10.1007/11917496_1. · Zbl 1167.68404 |
| [6] | ´Edouard Bonnet and Florian Sikora. The graph motif problem parameterized by the structure of the input graph. Discrete Applied Mathematics, 231:78-94, 2017. doi:10.1016/j.dam.2016.11.016. · Zbl 1369.05195 |
| [7] | Robert Bredereck, Piotr Faliszewski, Rolf Niedermeier, Piotr Skowron, and Nimrod Talmon. Elections with few candidates: Prices, weights, and covering problems. In ADT, volume 9346 of Lecture Notes in · Zbl 1403.68075 |
| [8] | Michele Conforti, G´erard Cornu´ejols, and Giacomo Zambelli. Extended formulations in combinatorial optimization. Annals OR, 204(1):97-143, 2013. doi:10.1007/s10479-012-1269-0. · Zbl 1273.90170 |
| [9] | Bruno Courcelle. The monadic second-order logic of graphs I: Recognizable sets of finite graphs. Information and Computation, 85:12-75, 1990. doi:10.1016/0890-5401(90)90043-H. · Zbl 0722.03008 |
| [10] | Bruno Courcelle. The monadic second-order logic of graphs VI: On several representations of graphs by relational structures. Discrete Applied Mathematics, 54(2-3):117-149, 1994. doi:10.1016/0166-218X(94) 90019-1. · Zbl 0809.03005 |
| [11] | Bruno Courcelle. The monadic second-order logic of graphs XIV: Uniformly sparse graphs and edge set quantifications. Theoretical Computer Science, 299(1-3):1-36, 2003. doi:10.1016/S0304-3975(02) 00578-9. · Zbl 1038.68048 |
| [12] | Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems, 33(2):125-150, 2000. doi:10.1007/ s002249910009. · Zbl 1009.68102 |
| [13] | Bruno Courcelle and Mohamed Mosbah. Monadic second-order evaluations on tree-decomposable graphs. Theoretical Computer Science, 109(1-2):49-82, 1993. doi:10.1016/0304-3975(93)90064-Z. · Zbl 0789.68083 |
| [14] | Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, D´aniel Marx, Marcin Pilipczuk, Micha l Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. doi:10.1007/ 978-3-319-21275-3. · Zbl 1334.90001 |
| [15] | Pavel Dvoˇr´ak, Duˇsan Knop, and Tom´aˇs Toufar. Target set selection in dense graph classes. In ISAAC, volume 123 of LIPIcs, pages 18:1-18:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. doi:10.4230/LIPIcs.ISAAC.2018.18. · Zbl 1533.68234 |
| [16] | Pavel Dvoˇr´ak, Duˇsan Knop, and Tom´aˇs Masaˇr´ık. Anti-path cover on sparse graph classes. In MEMICS, volume 233 of Electronic Proceedings in Theoretical Computer Science, pages 82-86. Open Publishing Association, 2016. doi:10.4204/EPTCS.233.8. |
| [17] | Michael R. Fellows, Guillaume Fertin, Danny Hermelin, and St´ephane Vialette. Upper and lower bounds for finding connected motifs in vertex-colored graphs. Journal of Computer and System Sciences, 77(4):799-811, 2011. doi:10.1016/j.jcss.2010.07.003. · Zbl 1210.68060 |
| [18] | Jiˇr´ı Fiala, Tom´aˇs Gavenˇciak, Duˇsan Knop, Martin Kouteck´y, and Jan Kratochv´ıl. Parameterized complexity of distance labeling and uniform channel assignment problems. Discrete Applied Mathematics, 248:46-55, 2018. doi:10.1016/j.dam.2017.02.010. · Zbl 1395.05143 |
| [19] | Eugene C. Freuder. Complexity of K-tree structured constraint satisfaction problems. In AAAI, pages 4-9. AAAI Press, 1990. URL: http://dl.acm.org/citation.cfm?id=1865499.1865500. |
| [20] | Markus Frick and Martin Grohe. The complexity of first-order and monadic second-order logic revisited. Annals of Pure and Applied Logic, 130(1-3):3-31, 2004. doi:10.1016/j.apal.2004.01.007. · Zbl 1062.03032 |
| [21] | Robert Ganian. Using neighborhood diversity to solve hard problems. 2012. arXiv:1201.3091. |
| [22] | Robert Ganian and Jan Obdrˇz´alek. Expanding the expressive power of monadic second-order logic on restricted graph classes. In IWOCA, volume 8288 of Lecture Notes in Computer Science, pages 164-177. Springer, 2013. doi:10.1007/978-3-642-45278-9. · Zbl 1284.68463 |
| [23] | Luisa Gargano and Adele A. Rescigno. Complexity of conflict-free colorings of graphs. Theoretical Computer Science, 566:39-49, 2015. doi:10.1016/j.tcs.2014.11.029. · Zbl 1317.68071 |
| [24] | Georg Gottlob, Reinhard Pichler, and Fang Wei. Monadic datalog over finite structures with bounded · Zbl 1351.68110 |
| [25] | Martin Grohe and Stephan Kreutzer. Methods for algorithmic meta theorems. Model Theoretic Methods in Finite Combinatorics, 558:181-206, 2011. · Zbl 1278.68099 |
| [26] | Ton Kloks. Treewidth: Computations and Approximations, volume 842 of Lecture Notes in Computer Science. Springer, 1994. doi:10.1007/BFb0045375. · Zbl 0825.68144 |
| [27] | Joachim Kneis, Alexander Langer, and Peter Rossmanith. Courcelle’s theorem - A game-theoretic approach. Discrete Optimization, 8(4):568-594, 2011. doi:10.1016/j.disopt.2011.06.001. · Zbl 1235.68103 |
| [28] | Duˇsan Knop, Martin Kouteck´y, Tom´aˇs Masaˇr´ık, and Tom´aˇs Toufar. Simplified algorithmic metatheorems beyond MSO: treewidth and neighborhood diversity. In WG, volume 10520 of Lecture Notes in Computer Science, pages 344-357. Springer, 2017. doi:10.1007/978-3-319-68705-6_26. · Zbl 1484.68072 |
| [29] | Duˇsan Knop, Tom´aˇs Masaˇr´ık, and Tom´aˇs Toufar. Parameterized complexity of fair vertex evaluation problems. In MFCS, volume 138 of LIPIcs, pages 33:1-33:16. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2019. doi:10.4230/LIPIcs.MFCS.2019.33. · Zbl 1541.68292 |
| [30] | Phokion G. Kolaitis and Moshe Y. Vardi. Conjunctive-query containment and constraint satisfaction. Journal of Computer and System Sciences, 61(2):302-332, 2000. doi:10.1006/jcss.2000.1713. · Zbl 0963.68059 |
| [31] | Petr Kolman, Martin Kouteck´y, and Hans R. Tiwary. Extension complexity, MSO logic, and treewidth, 2016. Short version presented at SWAT 2016. URL: http://arxiv.org/abs/1507.04907. · Zbl 1378.68178 |
| [32] | Petr Kolman, Bernard Lidick´y, and Jean-S´ebastien Sereni. On Fair Edge Deletion Problems, 2009. URL: https://kam.mff.cuni.cz/ kolman/papers/kls09.pdf. |
| [33] | Michael Lampis. Algorithmic meta-theorems for restrictions of treewidth. Algorithmica, 64(1):19-37, 2012. doi:10.1007/s00453-011-9554-x. · Zbl 1252.68154 |
| [34] | Michael Lampis. Model checking lower bounds for simple graphs. Logical Methods in Computer Science, 10(1):1-21, 2014. doi:10.2168/LMCS-10(1:18)2014. · Zbl 1326.68152 |
| [35] | Hendrik W. Lenstra Jr. Integer programming with a fixed number of variables. Mathematics of Operations Research, 8(4):538-548, 1983. doi:10.1287/moor.8.4.538. · Zbl 0524.90067 |
| [36] | Leonid Libkin. Elements of Finite Model Theory. Springer-Verlag, Berlin, 2004. doi:10.1007/ 978-3-662-07003-1. · Zbl 1060.03002 |
| [37] | Tom´aˇs Masaˇr´ık and Tom´aˇs Toufar. Parameterized complexity of fair deletion problems. Discrete Applied Mathematics, in press, 2019. doi:10.1016/j.dam.2019.06.001. · Zbl 1437.05227 |
| [38] | Jiˇr´ı Matouˇsek and Jaroslav Neˇsetˇril. Invitation to Discrete Mathematics (2. ed.). Oxford University Press, 2009. · Zbl 1152.05002 |
| [39] | Micha l Pilipczuk. Problems parameterized by treewidth tractable in single exponential time: A logical approach. In MFCS, volume 6907 of Lecture Notes in Computer Science, pages 520-531. Springer, 2011. doi:10.1007/978-3-642-22993-0. · Zbl 1343.68120 |
| [40] | Stefan Szeider. Monadic second order · Zbl 1173.03300 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
