Parameterised complexity of model checking and satisfiability in propositional dependence logic. (English) Zbl 1534.68108
Summary: Dependence Logic was introduced by J. Väänänen [Dependence logic. A new approach to independence friendly logic. Cambridge: Cambridge University Press (2007; Zbl 1117.03037)]. We study a propositional variant of this logic (\(\mathcal{PDL}\)) and investigate a variety of parameterisations with respect to central decision problems. The model checking problem (MC) of \(\mathcal{PDL}\) is NP-complete [J. Ebbing and P. Lohmann, Lect. Notes Comput. Sci. 7147, 226–237 (2012; Zbl 1298.68170)].
The subject of this research is to identify a list of parameterisations (formula-size, formula-depth, treewidth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that the number of disjunctions or the arity of dependence atoms (dep-arity) as a parameter both yield a paraNP-completeness result. Then, we consider the satisfiability problem (SAT) which classically is known to be NP-complete as well [P. Lohmann and H. Vollmer, Stud. Log. 101, No. 2, 343–366 (2013; Zbl 1432.03043)]. There we are presenting a different picture: under team-size, or dep-arity SAT is paraNP-complete whereas under all other mentioned parameters the problem is FPT. Finally, we introduce a variant of the satisfiability problem, asking for a team of a given size, and show for this problem an almost complete picture.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q27 | Parameterized complexity, tractability and kernelization |
| 68R07 | Computational aspects of satisfiability |
References:
| [1] | Abramsky, S.; Kontinen, J.; Väänänen, J.; Vollmer, H., Dependence Logic, Theory and Applications (2016), Berlin: Springer, Berlin · Zbl 1348.03004 · doi:10.1007/978-3-319-31803-5 |
| [2] | Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM J. Algebraic Discrete Methods 8(2), 277-284 (1987). doi:10.1137/0608024 · Zbl 0611.05022 |
| [3] | Beeri, C., Dowd, M., Fagin, R., Statman, R.: On the structure of armstrong relations for functional dependencies. J. ACM 31(1), 30-46 (1984). doi:10.1145/2422.322414 · Zbl 0629.68096 |
| [4] | Bläsius, T., Friedrich, T., Schirneck, M.: The Parameterized Complexity of Dependency Detection in Relational Databases. In: Guo, J., Hermelin, D. (eds.) 11th International Symposium on Parameterized and Exact Computation (IPEC 2016), Leibniz International Proceedings in Informatics (LIPIcs). doi:10.4230/LIPIcs.IPEC.2016.6. http://drops.dagstuhl.de/opus/volltexte/2017/6920, vol. 63, pp 6:1-6:13. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017) · Zbl 1398.68215 |
| [5] | Bodlaender, H.L.: A tourist guide through treewidth. Acta Cybern. 11(1-2), 1-21 (1993). https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3417 · Zbl 0804.68101 |
| [6] | Chen, H., Mengel, S.: A trichotomy in the complexity of counting answers to conjunctive queries. In: Arenas, M., Ugarte, M. (eds.) 18th International Conference on Database Theory, ICDT 2015, March 23-27, 2015, Brussels, Belgium, LIPIcs. doi:10.4230/LIPIcs.ICDT.2015.110, vol. 31, pp 110-126. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015) · Zbl 1365.68199 |
| [7] | Chen, H., Mengel, S.: Counting answers to existential positive queries: A complexity classification. In: Milo, T., Tan, W. (eds.) Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2016. doi:10.1145/2902251.2902279, pp 315-326. ACM, San Francisco (2016) |
| [8] | Chen, H., Mengel, S.: The logic of counting query answers. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pp. 1-12. IEEE Computer Society, Reykjavik (2017). doi:10.1109/LICS.2017.8005085 · Zbl 1457.68197 |
| [9] | Chen, H., Müller, M.: The fine classification of conjunctive queries and parameterized logarithmic space. TOCT 7(2), 7:1-7:27 (2015). doi:10.1145/2751316 · Zbl 1347.68179 |
| [10] | Ciardelli, I., Groenendijk, J., Roelofsen, F.: Towards a logic of information exchange - an inquisitive witness semantics. In: Logic, Language, and Computation - 9th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2011, Kutaisi, Revised Selected Papers, pp. 51-72 (2011). doi:10.1007/978-3-642-36976-6∖_6 · Zbl 1383.03038 |
| [11] | Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. doi:10.1145/800157.805047, pp 151-158. ACM, Shaker Heights (1971) · Zbl 0253.68020 |
| [12] | Cygan, M., Fomin, F.V., Kowalik, L., Lokshtanov, D., Marx, D., varPilipczuk, M., varPilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer (2015). doi:10.1007/978-3-319-21275-3 · Zbl 1334.90001 |
| [13] | Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer (2013). doi:10.1007/978-1-4471-5559-1 · Zbl 1358.68006 |
| [14] | Durand, A., Hannula, M., Kontinen, J., Meier, A., Virtema, J.: Approximation and dependence via multiteam semantics. Ann. Math. Artif. Intell. 83(3-4), 297-320 (2018). doi:10.1007/s10472-017-9568-4doi:10.1007/s10472-017-9568-4 · Zbl 1459.03032 |
| [15] | Durand, A., Hannula, M., Kontinen, J., Meier, A., Virtema, J.: Probabilistic team semantics. In: Ferrarotti, F., Woltran, S. (eds.) Foundations of Information and Knowledge Systems - 10th International Symposium, FoIKS 2018, Proceedings, Lecture Notes in Computer Science. doi:10.1007/978-3-319-90050-6∖_11, vol. 10833, pp 186-206. Springer, Budapest (2018) · Zbl 1508.03057 |
| [16] | Durand, A., Mengel, S.: Structural tractability of counting of solutions to conjunctive queries. Theory Comput. Syst. 57(4), 1202-1249 (2015). doi:10.1007/s00224-014-9543-y · Zbl 1352.68080 |
| [17] | Dvořák, W., Ordyniak, S., Szeider, S.: Augmenting tractable fragments of abstract argumentation. 186, 157-173 (2012). doi:10.1016/j.artint.2012.03.002 · Zbl 1251.68225 |
| [18] | Ebbing, J., Lohmann, P.: Complexity of model checking for modal dependence logic. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012: Theory and Practice of Computer Science - 38th Conference on Current Trends in Theory and Practice of Computer Science, Proceedings, Lecture Notes in Computer Science. doi:10.1007/978-3-642-27660-6∖_19, vol. 7147, pp 226-237. Springer, Špindlerův Mlýn (2012) · Zbl 1298.68170 |
| [19] | Fagin, R., Vardi, M.Y.: Armstrong databases for functional and inclusion dependencies. Inf. Process. Lett. 16(1), 13-19 (1983). doi:10.1016/0020-0190(83)90005-4 · Zbl 0501.68056 |
| [20] | Fichte, J.K., Meier, A., Schindler, I.: Strong backdoors for default logic. In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Proceedings, pp. 45-59, Bordeaux (2016). doi:10.1007/978-3-319-40970-2∖_4 · Zbl 1475.68366 |
| [21] | Fichte, J.K., Szeider, S.: Backdoors to normality for disjunctive logic programs. ACM Trans. Comput. Log. 17(1), 7:1-7:23 (2015). doi:10.1145/2818646 · Zbl 1367.68032 |
| [22] | Fichte, J.K., Szeider, S.: Backdoors to tractable answer set programming. Artif. Intell. 220, 64-103 (2015). doi:10.1016/j.artint.2014.12.001 · Zbl 1328.68040 |
| [23] | Flum, J., Grohe, M.: Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer (2006). doi:10.1007/3-540-29953-X · Zbl 1143.68016 |
| [24] | Galliani, P.: Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Ann. Pure Appl. Logic 163(1), 68-84 (2012). doi:10.1016/j.apal.2011.08.005 · Zbl 1250.03047 |
| [25] | Gaspers, S., Misra, N., Ordyniak, S., Szeider, S., Zivny, S.: Backdoors into heterogeneous classes of SAT and CSP. J. Comput. Syst. Sci. 85, 38-56 (2017). doi:10.1016/j.jcss.2016.10.007 · Zbl 1356.68097 |
| [26] | Grädel, E.: Model-checking games for logics of imperfect information. Theor. Comput. Sci. 493, 2-14 (2013). doi:10.1016/j.tcs.2012.10.033 · Zbl 1358.68191 |
| [27] | Grädel, E., Kontinen, J., Väänänen, J., Vollmer, H.: Logics for Dependence and Independence (Dagstuhl Seminar 15261). Dagstuhl Reports 5(6), 70-85 (2016). doi:10.4230/DagRep.5.6.70. http://drops.dagstuhl.de/opus/volltexte/2016/5508 |
| [28] | Grohe, M., Schwentick, T., Segoufin, L.: When is the evaluation of conjunctive queries tractable?. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Proceedings on 33rd Annual ACM Symposium on Theory of Computing. doi:10.1145/380752.380867, pp 657-666. ACM, Heraklion (2001) · Zbl 1323.68251 |
| [29] | Hannula, M., Kontinen, J., Virtema, J.: Polyteam semantics. In: Artëmov, S.N., Nerode, A. (eds.) Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings, Lecture Notes in Computer Science. doi:10.1007/978-3-319-72056-2∖_12, vol. 10703, pp 190-210. Springer, Deerfield Beach (2018) · Zbl 1505.03070 |
| [30] | Hannula, M., Kontinen, J., Virtema, J., Vollmer, H.: Complexity of propositional logics in team semantic. ACM Trans. Comput. Log. 19(1), 2:1-2:14 (2018). doi:10.1145/3157054 · Zbl 1407.68291 |
| [31] | Hella, L., Kuusisto, A., Meier, A., Virtema, J.: Model checking and validity in propositional and modal inclusion logics. J. Log. Comput (2019). doi:10.1093/logcom/exz008 · Zbl 1475.68187 |
| [32] | Kontinen, J., Müller, J., Schnoor, H., Vollmer, H.: Modal independence logic. J. Log. Comput. 27(5), 1333-1352 (2017). doi:10.1093/logcom/exw019 · Zbl 1444.03064 |
| [33] | Krebs, A., Meier, A., Virtema, J.: A team based variant of CTL. In: Grandi, F., Lange, M., Lomuscio, A. (eds.) 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015. doi:10.1109/TIME.2015.11, pp 140-149. IEEE Computer Society, Kassel (2015) |
| [34] | Krebs, A., Meier, A., Virtema, J., Zimmermann, M.: Team semantics for the specification and verification of hyperproperties. In: Potapov, I., Spirakis, P.G., Worrell, J. (eds.) 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, LIPIcs. doi:10.4230/LIPIcs.MFCS.2018.10, vol. 117, pp 10:1-10:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Liverpool (2018) · Zbl 1510.68043 |
| [35] | Kronegger, M., Ordyniak, S., Pfandler, A.: Variable-deletion backdoors to planning. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, pp. 3305-3312, Austin (2015). http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9885 · Zbl 1478.68323 |
| [36] | Levin, L.: Universal search problems. Problems of Information Transmission 9(3), 115-116 (1973) · Zbl 0313.02026 |
| [37] | Lohmann, P.; Vollmer, H., Complexity results for modal dependence logic, Studia Logica, 101, 2, 343-366 (2013) · Zbl 1432.03043 · doi:10.1007/s11225-013-9483-6 |
| [38] | Lück, M., Meier, A., Schindler, I.: Parameterised complexity of satisfiability in temporal logic. ACM Trans. Comput. Log. 18(1), 1:1-1:32 (2017). doi:10.1145/3001835 · Zbl 1367.68111 |
| [39] | Mahmood, Y., Meier, A.: Parameterised complexity of model checking and satisfiability in propositional dependence logic. In: Herzig, A., Kontinen, J. (eds.) Foundations of Information and Knowledge Systems - 11th International Symposium, FoIKS 2020, Proceedings, Lecture Notes in Computer Science. doi:10.1007/978-3-030-39951-1∖_10, vol. 12012, pp 157-174. Springer, Dortmund (2020) · Zbl 07266051 |
| [40] | Meier, A., Ordyniak, S., Sridharan, R., Schindler, I.: Backdoors for linear temporal logic. In: 11th International Symposium on Parameterized and Exact Computation, IPEC 2016, pp. 23:1-23:17, Aarhus (2016). doi:10.4230/LIPIcs.IPEC.2016.23 · Zbl 1398.68257 |
| [41] | Meier, A., Reinbold, C.: Enumeration complexity of poor man’s propositional dependence logic. In: Ferrarotti, F., Woltran, S. (eds.) Foundations of Information and Knowledge Systems - 10th International Symposium, FoIKS 2018, Proceedings, Lecture Notes in Computer Science. doi:10.1007/978-3-319-90050-6∖_17, vol. 10833, pp 303-321. Springer, Budapest (2018) · Zbl 1508.68092 |
| [42] | Pfandler, A., Rümmele, S., Szeider, S.: Backdoors to abduction. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13), pp 1046-1052, Beijing (2013) |
| [43] | varPippenger, N.: Theories of computability. Cambridge University Press (1997) · Zbl 0879.03013 |
| [44] | Robertson, N., Seymour, P.D.: Graph minors. v. excluding a planar graph. J. Comb. Theory, Ser. B 41(1), 92-114 (1986). doi:10.1016/0095-8956(86)90030-4 · Zbl 0598.05055 |
| [45] | Samer, M., Szeider, S.: Fixed-parameter tractability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. doi:10.3233/978-1-58603-929-5-425, vol. 185, pp 425-454. IOS Press (2009) · Zbl 1183.68568 |
| [46] | Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithm. 8(1), 50-64 (2010) · Zbl 1214.05166 |
| [47] | Väänänen, J.A.: Dependence Logic - A New Approach to Independence Friendly Logic, London Mathematical Society student texts, vol. 70. Cambridge University Press (2007). http://www.cambridge.org/de/knowledge/isbn/item1164246/?site · Zbl 1117.03037 |
| [48] | Väänänen, J.A.: Modal dependence logic. In: Apt, K., van Rooij, R. (eds.) New Perspectives on Games and Interaction. Amsterdam University Press (2008) · Zbl 1377.03011 |
| [49] | Virtema, J.: Complexity of validity for propositional dependence logics. Inf. Comput. 253, 224-236 (2017). doi:10.1016/j.ic.2016.07.008 · Zbl 1362.68114 |
| [50] | Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, pp. 1173-1178 (2003) |
| [51] | Yang, F., Väänänen, J.: Propositional logics of dependence. Ann. Pure Appl. Logic 167(7), 557-589 (2016). doi:10.1016/j.apal.2016.03.003 · Zbl 1355.03021 |
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.
