{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:41:27Z","timestamp":1740109287350,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T00:00:00Z","timestamp":1537228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P26696"],"award-info":[{"award-number":["P26696"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"name":"German Research Fundation","award":["ME 4279\/1-1"],"award-info":[{"award-number":["ME 4279\/1-1"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Algorithmica"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s00453-018-0515-5","type":"journal-article","created":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T18:50:29Z","timestamp":1537296629000},"page":"476-496","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Backdoors for Linear Temporal Logic"],"prefix":"10.1007","volume":"81","author":[{"given":"Arne","family":"Meier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1935-651X","authenticated-orcid":false,"given":"Sebastian","family":"Ordyniak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. S.","family":"Ramanujan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Irena","family":"Schindler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,18]]},"reference":[{"issue":"7","key":"515_CR1","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1016\/j.jcss.2009.09.002","volume":"76","author":"FN Abu-Khzam","year":"2010","unstructured":"Abu-Khzam, F.N.: A kernelization algorithm for d-hitting set. J. Comput. Syst. Sci. 76(7), 524\u2013531 (2010)","journal-title":"J. Comput. Syst. Sci."},{"key":"515_CR2","doi-asserted-by":"crossref","unstructured":"Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: The complexity of clausal fragments of LTL. In: Proc. 19th LPAR, LNCS, vol. 8312 (2013)","DOI":"10.1007\/978-3-642-45221-5_3"},{"issue":"1","key":"515_CR3","first-page":"1","volume":"5","author":"M Bauland","year":"2009","unstructured":"Bauland, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H.: The complexity of generalized satisfiability for linear temporal logic. LMCS 5(1), 1\u201321 (2009)","journal-title":"LMCS"},{"issue":"3","key":"515_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(93)90014-Z","volume":"45","author":"CC Chen","year":"1993","unstructured":"Chen, C.C., Lin, I.P.: The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic. IPL 45(3), 131\u2013136 (1993)","journal-title":"IPL"},{"issue":"2","key":"515_CR5","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1016\/j.ic.2005.05.001","volume":"201","author":"J Chen","year":"2005","unstructured":"Chen, J., Chor, B., Fellows, M., Huang, X., Juedes, D., Kanji, I., Xia, G.: Tight lower bounds for certain parameterized NP-hard problems. Inf. Comput. 201(2), 216\u2013231 (2005)","journal-title":"Inf. Comput."},{"issue":"40\u201342","key":"515_CR6","doi-asserted-by":"publisher","first-page":"3736","DOI":"10.1016\/j.tcs.2010.06.026","volume":"411","author":"J Chen","year":"2010","unstructured":"Chen, J., Kanj, I.A., Xia, G.: Improved upper bounds for vertex cover. Theor. Comput. Sci. 411(40\u201342), 3736\u20133756 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"515_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. Logic of Programs. LNCS, vol. 131, pp. 52\u201371. Springer, Berlin (1981)"},{"issue":"1","key":"515_CR8","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.2001.3094","volume":"174","author":"S Demri","year":"2002","unstructured":"Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1), 84\u2013103 (2002)","journal-title":"Inf. Comput."},{"key":"515_CR9","doi-asserted-by":"crossref","unstructured":"Dilkina, B.N., Gomes, C.P., Sabharwal, A.: Tradeoffs in the complexity of backdoor detection. In: Proc. 13th CP, Lecture Notes in Computer Science, vol. 4741, pp. 256\u2013270. Springer (2007)","DOI":"10.1007\/978-3-540-74970-7_20"},{"key":"515_CR10","doi-asserted-by":"crossref","unstructured":"Dilkina, B.N., Gomes, C.P., Sabharwal, A.: Backdoors in the context of learning. In: Proc. 12th SAT, Lecture Notes in Computer Science, vol. 5584, pp. 73\u201379. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02777-2_9"},{"key":"515_CR11","unstructured":"Dixon, C., Fisher, M., Konev, B.: Tractable temporal reasoning. In: Proc. of IJCAI, pp. 318\u2013323 (2007)"},{"key":"515_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5559-1","volume-title":"Fundamentals of Parameterized Complexity","author":"RG Downey","year":"2013","unstructured":"Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. Springer, London (2013)"},{"key":"515_CR13","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.artint.2012.03.002","volume":"186","author":"W Dvor\u00e1k","year":"2012","unstructured":"Dvor\u00e1k, W., Ordyniak, S., Szeider, S.: Augmenting tractable fragments of abstract argumentation. Artif. Intell. 186, 157\u2013173 (2012)","journal-title":"Artif. Intell."},{"issue":"1","key":"515_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"EA Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30(1), 1\u201324 (1985)","journal-title":"Journal of Computer and System Sciences"},{"key":"515_CR15","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M Fisher","year":"1997","unstructured":"Fisher, M.: A normal form for temporal logic and its application in theorem-proving and execution. J. Logic Comput. 7, 429\u2013456 (1997)","journal-title":"J. Logic Comput."},{"issue":"1","key":"515_CR16","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Logic 2(1), 12\u201356 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"515_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013976","volume-title":"Temporal Logic: Mathematical Foundations and Computational Aspects","author":"DM Gabbay","year":"1994","unstructured":"Gabbay, D.M., Hodkinsion, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press, Inc., New York (1994)"},{"key":"515_CR18","doi-asserted-by":"crossref","unstructured":"Gaspers, S., Szeider, S.: Backdoors to satisfaction. In: The Multivariate Algorithmic Revolution and Beyond - Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday, LNCS, vol. 7370, pp. 287\u2013317. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-30891-8_15"},{"key":"515_CR19","doi-asserted-by":"crossref","unstructured":"Gaspers, S., Szeider, S.: Strong backdoors to bounded treewidth SAT. In: Proc. 54th FOCS, pp. 489\u2013498. IEEE Computer Society (2013)","DOI":"10.1109\/FOCS.2013.59"},{"key":"515_CR20","doi-asserted-by":"crossref","unstructured":"Kottler, S., Kaufmann, M., Sinz, C.: A new bound for an NP-hard subclass of 3-SAT using backdoors. In: Proc. 11th SAT, Lecture Notes in Computer Science, pp. 161\u2013167. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-79719-7_16"},{"key":"515_CR21","first-page":"84","volume":"16","author":"S Kripke","year":"1963","unstructured":"Kripke, S.: Semantical considerations on modal logic. Acta philosophica Fennica 16, 84\u201394 (1963)","journal-title":"Acta philosophica Fennica"},{"key":"515_CR22","doi-asserted-by":"crossref","unstructured":"Kronegger, M., Ordyniak, S., Pfandler, A.: Backdoors to planning. In: Proc. 28th AAAI, pp. 2300\u20132307. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.9033"},{"key":"515_CR23","doi-asserted-by":"crossref","unstructured":"Kronegger, M., Ordyniak, S., Pfandler, A.: Variable-deletion backdoors to planning. In: Proc. 29th AAAI, pp. 2300\u20132307. AAAI Press (2014)","DOI":"10.1609\/aaai.v29i1.9662"},{"issue":"3","key":"515_CR24","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001). https:\/\/doi.org\/10.1023\/A:1011254632723","journal-title":"Formal Methods Syst. Des."},{"key":"515_CR25","unstructured":"LeBras, R., Bernstein, R., Gomes, C.P., Selman, B., van Dover, R.B.: Crowdsourcing backdoor identification for combinatorial optimization. In: Proc. 23rd IJCAI. AAAI (2013)"},{"key":"515_CR26","doi-asserted-by":"publisher","unstructured":"L\u00fcck, M., Meier, A.: LTL Fragments are hard for standard parameterizations. In: Proc. of TIME, pp. 59\u201368 (2015). https:\/\/doi.org\/10.1109\/TIME.2015.9","DOI":"10.1109\/TIME.2015.9"},{"issue":"6\u20137","key":"515_CR27","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/s00236-003-0136-5","volume":"40","author":"N Markey","year":"2004","unstructured":"Markey, N.: Past is for free: on the complexity of verifying linear temporal properties with past. Acta Informatica 40(6\u20137), 431\u2013458 (2004)","journal-title":"Acta Informatica"},{"key":"515_CR28","unstructured":"Meier, A., Ordyniak, S., Sridharan, R., Schindler, I.: Backdoors for linear temporal logic. In: J.\u00a0Guo, D.\u00a0Hermelin (eds.) 11th International Symposium on Parameterized and Exact Computation (IPEC 2016), vol. 63, pp. 23:1\u201323:17. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2017)"},{"key":"515_CR29","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00713542","volume":"39","author":"H Ono","year":"1980","unstructured":"Ono, H., Nakamura, A.: On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica 39, 325\u2013333 (1980)","journal-title":"Studia Logica"},{"key":"515_CR30","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.tcs.2012.12.039","volume":"481","author":"S Ordyniak","year":"2013","unstructured":"Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of acyclic and almost acyclic CNF formulas. Theor. Comput. Sci. 481, 85\u201399 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"515_CR31","unstructured":"Pfandler, A., R\u00fcmmele, S., Szeider, S.: Backdoors to abduction. In: Proc. 23rd IJCAI (2013)"},{"key":"515_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. of FOCS, pp. 46\u201357. IEEE Comp. Soc. Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"515_CR33","unstructured":"Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: Proc. 19th IAAI, pp. 124\u2013130. AAAI Press (2004)"},{"issue":"1","key":"515_CR34","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77\u201397 (2009)","journal-title":"J. Autom. Reason."},{"key":"515_CR35","first-page":"425","volume-title":"Handbook of Satisfiability, chap 13","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Fixed-parameter tractability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap 13, pp. 425\u2013454. IOS Press, Amsterdam (2009)"},{"key":"515_CR36","doi-asserted-by":"crossref","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. In: Proc. of STOC, pp. 159\u2013168. ACM (1982)","DOI":"10.1145\/800070.802189"},{"key":"515_CR37","doi-asserted-by":"crossref","unstructured":"Szeider, S.: On fixed-parameter tractable parameterizations of SAT. In: Proc. of SAT, pp. 188\u2013202 (2003)","DOI":"10.1007\/978-3-540-24605-3_15"},{"key":"515_CR38","unstructured":"Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. 18th IJCAI, pp. 1173\u20131178. Morgan Kaufmann (2003)"}],"container-title":["Algorithmica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00453-018-0515-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-018-0515-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-018-0515-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T21:36:34Z","timestamp":1662068194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00453-018-0515-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,18]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["515"],"URL":"https:\/\/doi.org\/10.1007\/s00453-018-0515-5","relation":{},"ISSN":["0178-4617","1432-0541"],"issn-type":[{"type":"print","value":"0178-4617"},{"type":"electronic","value":"1432-0541"}],"subject":[],"published":{"date-parts":[[2018,9,18]]},"assertion":[{"value":"31 May 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 September 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 September 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}