{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T02:32:07Z","timestamp":1767839527496,"version":"3.49.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,11,26]],"date-time":"2014-11-26T00:00:00Z","timestamp":1416960000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Algorithmica"],"published-print":{"date-parts":[[2016,1]]},"DOI":"10.1007\/s00453-014-9958-5","type":"journal-article","created":{"date-parts":[[2014,12,2]],"date-time":"2014-12-02T16:57:57Z","timestamp":1417539477000},"page":"540-557","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Backdoors to q-Horn"],"prefix":"10.1007","volume":"74","author":[{"given":"Serge","family":"Gaspers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":"Saket","family":"Saurabh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,11,26]]},"reference":[{"key":"9958_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.A.: Satisfiability, branch-width and Tseitin tautologies. In: Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science (FOCS\u201902), pp. 593\u2013603 (2002)","DOI":"10.1109\/SFCS.2002.1181983"},{"issue":"3","key":"9958_CR2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett. 8(3), 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9958_CR3","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 457\u2013481. IOS Press (2009)"},{"key":"9958_CR4","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009)"},{"key":"9958_CR5","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification: 13th International Conference, CAV 2001, Paris, France, July 18\u201322, 2001, Proceedings, pp. 454\u2013464 (2001)","DOI":"10.1007\/3-540-44585-4_44"},{"key":"9958_CR6","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF01531068","volume":"1","author":"E Boros","year":"1990","unstructured":"Boros, E., Crama, Y., Hammer, P.L.: Polynomial-time inference of all valid implications for horn and related formulae. Ann. Math. Artif. Intell. 1, 21\u201332 (1990)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"9958_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0166-218X(94)90033-7","volume":"55","author":"E Boros","year":"1994","unstructured":"Boros, E., Hammer, P.L., Sun, X.: Recognition of $$q$$ q -Horn formulae in linear time. Discret. Appl. Math. 55(1), 1\u201313 (1994)","journal-title":"Discret. Appl. Math."},{"key":"9958_CR8","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual Symposium on Theory of Computing, pp. 151\u2013158. Shaker Heights, Ohio (1971)","DOI":"10.1145\/800157.805047"},{"issue":"3","key":"9958_CR9","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0166-218X(96)00028-5","volume":"75","author":"Y Crama","year":"1997","unstructured":"Crama, Y., Ekin, O., Hammer, P.L.: Variable and term removal from Boolean formulae. Discret. Appl. Math. 75(3), 217\u2013230 (1997)","journal-title":"Discret. Appl. Math."},{"key":"9958_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0515-9","volume-title":"Parameterized Complexity. Monographs in Computer Science","author":"RG Downey","year":"1999","unstructured":"Downey, R.G., Fellows, M.R.: Parameterized Complexity. Monographs in Computer Science. Springer, New York (1999)"},{"key":"9958_CR11","doi-asserted-by":"crossref","unstructured":"Downey, R.G., Fellows, M.R., McCartin, C.: Parameterized approximation problems. In: Parameterized and Exact Computation, Second International Workshop, IWPEC 2006, volume 4169 of Lecture Notes in Computer Science, pp. 121\u2013129. Springer, Berlin (2006)","DOI":"10.1007\/11847250_11"},{"issue":"4","key":"9958_CR12","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1016\/j.dam.2006.06.020","volume":"156","author":"E Fischer","year":"2008","unstructured":"Fischer, E., Makowsky, J.A., Ravve, E.R.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discret. Appl. Math. 156(4), 511\u2013529 (2008)","journal-title":"Discret. Appl. Math."},{"key":"9958_CR13","volume-title":"Parameterized Complexity Theory, volume XIV of Texts in Theoretical Computer Science. An EATCS Series","author":"J Flum","year":"2006","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory, volume XIV of Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2006)"},{"key":"9958_CR14","doi-asserted-by":"crossref","first-page":"399","DOI":"10.4153\/CJM-1956-045-5","volume":"8","author":"LR Ford Jr","year":"1956","unstructured":"Ford Jr, L.R., Fulkerson, D.R.: Maximal flow through a network. Can. J. Math. 8, 399\u2013404 (1956)","journal-title":"Can. J. Math."},{"key":"9958_CR15","unstructured":"Ganian, R., Hlinen\u00fd, P., Obdrz\u00e1lek, J.: Better algorithms for satisfiability problems for formulas of bounded rank-width. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15\u201318, 2010, Chennai, India, volume 8 of LIPIcs, pp. 73\u201383 (2010)"},{"key":"9958_CR16","doi-asserted-by":"crossref","unstructured":"Gaspers, S., Szeider, S.: Backdoors to satisfaction. In: Bodlaender, H.L., Downey, R., Fomin, F.V., Marx, D. (eds.) The Multivariate Algorithmic Revolution and Beyond\u2014Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday volume 7370 of Lecture Notes in Computer Science, pp. 287\u2013317. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-30891-8_15"},{"key":"9958_CR17","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation, volume 3 of Foundations of Artificial Intelligence, pp. 89\u2013134. Elsevier, Amsterdam (2008)","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"9958_CR18","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings ECAI, pp. 359\u2013363 (1992)"},{"issue":"1","key":"9958_CR19","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"HR Lewis","year":"1978","unstructured":"Lewis, H.R.: Renaming a set of clauses as a Horn set. J. ACM 25(1), 134\u2013135 (1978)","journal-title":"J. ACM"},{"issue":"2","key":"9958_CR20","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"AGM Prasad","year":"2005","unstructured":"Prasad, A.G.M., Biere, A.: A survey of recent advances in SAT-based formal verification. Softw. Tools Technol. Transf. 7(2), 156\u2013173 (2005)","journal-title":"Softw. Tools Technol. Transf."},{"key":"9958_CR21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.4086\/toc.2010.v006a005","volume":"6","author":"D Marx","year":"2010","unstructured":"Marx, D.: Can you beat treewidth? Theory Comput. 6, 85\u2013112 (2010)","journal-title":"Theory Comput."},{"key":"9958_CR22","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Proceedings of SAT 2004 (Seventh International Conference on Theory and Applications of Satisfiability Testing, 10\u201313 May, 2004, Vancouver, BC, Canada), pp. 96\u2013103 (2004)"},{"key":"9958_CR23","doi-asserted-by":"crossref","unstructured":"Ramanujan, M.S., Saurabh, S.: Linear time parameterized algorithms via skew-symmetric multicuts. In: Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5\u20137, 2014, pp. 1739\u20131748 (2014)","DOI":"10.1137\/1.9781611973402.126"},{"issue":"8","key":"9958_CR24","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1016\/j.jcss.2009.04.002","volume":"75","author":"I Razgon","year":"2009","unstructured":"Razgon, I., O\u2019Sullivan, B.: Almost 2-SAT is fixed parameter tractable. J. Comput. Syst. Sci. 75(8), 435\u2013450 (2009)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"9958_CR25","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/j.jda.2009.06.002","volume":"8","author":"M Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discret. Algorithms 8(1), 50\u201364 (2010)","journal-title":"J. Discret. Algorithms"},{"key":"9958_CR26","doi-asserted-by":"crossref","unstructured":"Schaefer, T.J.: The complexity of satisfiability problems. In: Conference Record of the Tenth Annual ACM Symposium on Theory of Computing (San Diego, Calif., 1978), pp. 216\u2013226. ACM (1978)","DOI":"10.1145\/800133.804350"},{"issue":"2","key":"9958_CR27","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"MN Velev","year":"2003","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2), 73\u2013106 (2003)","journal-title":"J. Symb. Comput."},{"key":"9958_CR28","unstructured":"Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI, 2003, pp. 1173\u20131178 (2003)"}],"container-title":["Algorithmica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-014-9958-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00453-014-9958-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-014-9958-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T02:24:40Z","timestamp":1566095080000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00453-014-9958-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,26]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["9958"],"URL":"https:\/\/doi.org\/10.1007\/s00453-014-9958-5","relation":{},"ISSN":["0178-4617","1432-0541"],"issn-type":[{"value":"0178-4617","type":"print"},{"value":"1432-0541","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,26]]}}}