{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T17:40:14Z","timestamp":1743529214734,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":103,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642308901"},{"type":"electronic","value":"9783642308918"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30891-8_15","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T09:24:05Z","timestamp":1340011445000},"page":"287-317","source":"Crossref","is-referenced-by-count":27,"title":["Backdoors to Satisfaction"],"prefix":"10.1007","author":[{"given":"Serge","family":"Gaspers","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"7","key":"15_CR1","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1016\/j.jcss.2009.09.002","volume":"76","author":"F.N. Abu-Khzam","year":"2010","unstructured":"Abu-Khzam, F.N.: A kernelization algorithm for d-hitting set. J. of Computer and System Sciences\u00a076(7), 524\u2013531 (2010)","journal-title":"J. of Computer and System Sciences"},{"issue":"3","key":"15_CR2","doi-asserted-by":"publisher","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. Information Processing Letters\u00a08(3), 121\u2013123 (1979)","journal-title":"Information Processing Letters"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and Bayesian inference. In: 44th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2003), pp. 340\u2013351 (2003)","DOI":"10.1109\/SFCS.2003.1238208"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Baroni, P., Giacomin, M.: Semantics of abstract argument systems. In: Rahwan, I., Simari, G. (eds.) Argumentation in Artificial Intelligence, pp. 25\u201344. Springer (2009)","DOI":"10.1007\/978-0-387-98197-0_2"},{"issue":"10-15","key":"15_CR5","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1016\/j.artint.2007.05.001","volume":"171","author":"T.J.M. Bench-Capon","year":"2007","unstructured":"Bench-Capon, T.J.M., Dunne, P.E.: Argumentation in artificial intelligence. Artificial Intelligence\u00a0171(10-15), 619\u2013641 (2007)","journal-title":"Artificial Intelligence"},{"key":"15_CR6","first-page":"197","volume-title":"Proceedings of 12th International Conference Software Product Lines Workshops, SPLC 2008","author":"D.L. Berre","year":"2008","unstructured":"Berre, D.L., Parrain, A.: On SAT technologies for dependency management and beyond. In: Thiel, S., Pohl, K. (eds.) Proceedings of 12th International Conference Software Product Lines Workshops, SPLC 2008, Limerick, Ireland, September 8-12, vol.\u00a02, pp. 197\u2013200. Lero Int. Science Centre, University of Limerick, Ireland (2008)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Besnard, P., Hunter, A.: Elements of Argumentation. The MIT Press (2008)","DOI":"10.7551\/mitpress\/9780262026437.001.0001"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 454\u2013464. Springer, Heidelberg (2001)"},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1142\/S0129054194000049","volume":"5","author":"H.L. Bodlaender","year":"1994","unstructured":"Bodlaender, H.L.: On disjoint cycles. International Journal of Foundations of Computer Science\u00a05(1), 59\u201368 (1994)","journal-title":"International Journal of Foundations of Computer Science"},{"issue":"8","key":"15_CR10","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1016\/j.jcss.2009.04.001","volume":"75","author":"H.L. Bodlaender","year":"2009","unstructured":"Bodlaender, H.L., Downey, R.G., Fellows, M.R., Hermelin, D.: On problems without polynomial kernels. J. of Computer and System Sciences\u00a075(8), 423\u2013434 (2009)","journal-title":"J. of Computer and System Sciences"},{"issue":"1-2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0004-3702(97)00015-5","volume":"93","author":"A. Bondarenko","year":"1997","unstructured":"Bondarenko, A., Dung, P.M., Kowalski, R.A., Toni, F.: An abstract, argumentation-theoretic approach to default reasoning. Artificial Intelligence\u00a093(1-2), 63\u2013101 (1997)","journal-title":"Artificial Intelligence"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-22300-6_11","volume-title":"Algorithms and Data Structures","author":"P. Bonsma","year":"2011","unstructured":"Bonsma, P., Lokshtanov, D.: Feedback Vertex Set in Mixed Graphs. In: Dehne, F., Iacono, J., Sack, J.-R. (eds.) WADS 2011. LNCS, vol.\u00a06844, pp. 122\u2013133. Springer, Heidelberg (2011)"},{"issue":"1","key":"15_CR13","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"issue":"2","key":"15_CR14","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/s00453-008-9223-x","volume":"57","author":"L. Cai","year":"2010","unstructured":"Cai, L., Huang, X.: Fixed-parameter approximation: Conceptual framework and approximability results. Algorithmica\u00a057(2), 398\u2013412 (2010)","journal-title":"Algorithmica"},{"issue":"6-7","key":"15_CR15","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/j.artint.2007.11.002","volume":"172","author":"M. Chavira","year":"2008","unstructured":"Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artificial Intelligence\u00a0172(6-7), 772\u2013799 (2008)","journal-title":"Artificial Intelligence"},{"issue":"1-3","key":"15_CR16","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.tcs.2004.12.034","volume":"337","author":"J. Chen","year":"2005","unstructured":"Chen, J., Kanj, I.A.: On approximating minimum vertex cover for graphs with perfect matching. Theoretical Computer Science\u00a0337(1-3), 305\u2013318 (2005)","journal-title":"Theoretical Computer Science"},{"issue":"7","key":"15_CR17","doi-asserted-by":"publisher","first-page":"1188","DOI":"10.1016\/j.jcss.2008.05.002","volume":"74","author":"J. Chen","year":"2008","unstructured":"Chen, J., Fomin, F.V., Liu, Y., Lu, S., Villanger, Y.: Improved algorithms for feedback vertex set problems. J. of Computer and System Sciences\u00a074(7), 1188\u20131198 (2008)","journal-title":"J. of Computer and System Sciences"},{"issue":"2","key":"15_CR18","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1006\/jagm.2001.1186","volume":"41","author":"J. Chen","year":"2001","unstructured":"Chen, J., Kanj, I.A., Jia, W.: Vertex cover: further observations and further improvements. J. Algorithms\u00a041(2), 280\u2013301 (2001)","journal-title":"J. Algorithms"},{"issue":"40\u201342","key":"15_CR19","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. Theoretical Computer Science\u00a0411(40\u201342), 3736\u20133756 (2010)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"15_CR20","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1411509.1411511","volume":"55","author":"J. Chen","year":"2008","unstructured":"Chen, J., Liu, Y., Lu, S., O\u2019Sullivan, B., Razgon, I.: A fixed-parameter algorithm for the directed feedback vertex set problem. J. of the ACM\u00a055(5), Art. 21, 19 (2008)","journal-title":"J. of the ACM"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/11847250_10","volume-title":"Parameterized and Exact Computation","author":"Y.-J. Chen","year":"2006","unstructured":"Chen, Y.-J., Grohe, M., Gr\u00fcber, M.: On Parameterized Approximability. In: Bodlaender, H.L., Langston, M.A. (eds.) IWPEC 2006. LNCS, vol.\u00a04169, pp. 109\u2013120. Springer, Heidelberg (2006)"},{"key":"15_CR22","first-page":"151","volume-title":"Proc. 3rd Annual Symp. on Theory of Computing","author":"S.A. Cook","year":"1971","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proc. 3rd Annual Symp. on Theory of Computing, pp. 151\u2013158. Shaker Heights, Ohio (1971)"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Cook, S.A., Mitchell, D.G.: Finding hard instances of the satisfiability problem: a survey. In: Satisfiability problem: theory and applications, Piscataway, NJ. American Mathematical Society, pp. 1\u201317 (1997)","DOI":"10.1090\/dimacs\/035\/01"},{"key":"15_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/11518655_28","volume-title":"Symbolic and Quantitative Approaches to Reasoning with Uncertainty","author":"S. Coste-Marquis","year":"2005","unstructured":"Coste-Marquis, S., Devred, C., Marquis, P.: Symmetric Argumentation Frameworks. In: Godo, L. (ed.) ECSQARU 2005. LNCS (LNAI), vol.\u00a03571, pp. 317\u2013328. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"15_CR25","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S0166-218X(00)00221-3","volume":"108","author":"B. Courcelle","year":"2001","unstructured":"Courcelle, B., Makowsky, J.A., Rotics, U.: On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discr. Appl. Math.\u00a0108(1-2), 23\u201352 (2001)","journal-title":"Discr. Appl. Math."},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Courcelle, B.: Graph rewriting: an algebraic and logic approach. In: Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 193\u2013242. Elsevier Science Publishers, North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50010-X"},{"issue":"3","key":"15_CR27","doi-asserted-by":"publisher","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. Discr. Appl. Math.\u00a075(3), 217\u2013230 (1997)","journal-title":"Discr. Appl. Math."},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-22006-7_38","volume-title":"Automata, Languages and Programming","author":"M. Cygan","year":"2011","unstructured":"Cygan, M., Pilipczuk, M., Pilipczuk, M., Wojtaszczyk, J.O.: Subset Feedback Vertex Set Is Fixed-Parameter Tractable. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol.\u00a06755, pp. 449\u2013461. Springer, Heidelberg (2011)"},{"issue":"3","key":"15_CR29","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"J. of the ACM"},{"key":"15_CR30","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74970-7_20","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"B.N. Dilkina","year":"2007","unstructured":"Dilkina, B.N., Gomes, C.P., Sabharwal, A.: Tradeoffs in the Complexity of Backdoor Detection. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 256\u2013270. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"15_CR32","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/S0304-3975(96)80707-9","volume":"170","author":"Y. Dimopoulos","year":"1996","unstructured":"Dimopoulos, Y., Torres, A.: Graph theoretical structures in logic programs and default theories. Theoretical Computer Science\u00a0170(1-2), 209\u2013244 (1996)","journal-title":"Theoretical Computer Science"},{"key":"15_CR33","series-title":"Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0515-9","volume-title":"Parameterized Complexity","author":"R.G. Downey","year":"1999","unstructured":"Downey, R.G., Fellows, M.R.: Parameterized Complexity. Monographs in Computer Science. Springer, New York (1999)"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/11847250_11","volume-title":"Parameterized and Exact Computation","author":"R.G. Downey","year":"2006","unstructured":"Downey, R.G., Fellows, M.R., McCartin, C.: Parameterized Approximation Problems. In: Bodlaender, H.L., Langston, M.A. (eds.) IWPEC 2006. LNCS, vol.\u00a04169, pp. 121\u2013129. Springer, Heidelberg (2006)"},{"issue":"2","key":"15_CR35","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0004-3702(94)00041-X","volume":"77","author":"P.M. Dung","year":"1995","unstructured":"Dung, P.M.: On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence\u00a077(2), 321\u2013357 (1995)","journal-title":"Artificial Intelligence"},{"issue":"10-15","key":"15_CR36","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/j.artint.2007.03.006","volume":"171","author":"P.E. Dunne","year":"2007","unstructured":"Dunne, P.E.: Computational properties of argument systems satisfying graph-theoretic constraints. Artificial Intelligence\u00a0171(10-15), 701\u2013729 (2007)","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"15_CR37","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0004-3702(02)00261-8","volume":"141","author":"P.E. Dunne","year":"2002","unstructured":"Dunne, P.E., Bench-Capon, T.J.M.: Coherence in finite argument systems. Artificial Intelligence\u00a0141(1-2), 187\u2013203 (2002)","journal-title":"Artificial Intelligence"},{"issue":"3-4","key":"15_CR38","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01536399","volume":"15","author":"T. Eiter","year":"1995","unstructured":"Eiter, T., Gottlob, G.: On the computational cost of disjunctive logic programming: propositional case. Ann. Math. Artif. Intell.\u00a015(3-4), 289\u2013323 (1995)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"3","key":"15_CR39","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.tcs.2005.10.005","volume":"351","author":"M.R. Fellows","year":"2006","unstructured":"Fellows, M.R., Szeider, S., Wrightson, G.: On finding short resolution refutations and small unsatisfiable subsets. Theoretical Computer Science\u00a0351(3), 351\u2013359 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"15_CR40","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s00453-008-9199-6","volume":"57","author":"H. Fernau","year":"2010","unstructured":"Fernau, H.: A top-down approach to search-trees: Improved algorithmics for 3-hitting set. Algorithmica\u00a057(1), 97\u2013118 (2010)","journal-title":"Algorithmica"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Fichte, J.K.: The good, the bad, and the odd: Cycles in answer-set programs. In: ESSLII 2011 (2011)","DOI":"10.1007\/978-3-642-31467-4_6"},{"key":"15_CR42","unstructured":"Fichte, J.K., Szeider, S.: Backdoors to tractable answer-set programming. Technical Report 1104.2788, Arxiv.org (2012), Extended and updated version of a paper that appeared in the proceedings of IJCAI 2011. The 22nd International Joint Conference on Artificial Intelligence (2012)"},{"issue":"4","key":"15_CR43","doi-asserted-by":"publisher","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. Discr. Appl. Math.\u00a0156(4), 511\u2013529 (2008)","journal-title":"Discr. Appl. Math."},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Fortnow, L., Santhanam, R.: Infeasibility of instance compression and succinct PCPs for NP. In: Dwork, C. (ed.) Proceedings of the 40th Annual ACM Symposium on Theory of Computing, Victoria, British Columbia, Canada, May 17-20, pp. 133\u2013142. ACM (2008)","DOI":"10.1145\/1374376.1374398"},{"key":"15_CR45","volume-title":"Computers and Intractability","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.R.: Computers and Intractability. W. H. Freeman and Company, New York (1979)"},{"key":"15_CR46","unstructured":"Gaspers, S., Szeider, S.: Backdoors to acyclic SAT. In: Proceedings of ICALP 2012 (Track A: Algorithms, Complexity and Games), the 39th International Colloquium on Automata, Languages and Programming, University of Warwick, UK, July 9-13. LNCS. Springer (to appear, 2012)"},{"key":"15_CR47","unstructured":"Gaspers, S., Szeider, S.: Strong backdoors to nested satisfiabiliy. In: Proceedings of SAT 2012, the 15th International Conference on Theory and Applications of Satisfiability Testing, Trento, Italy, June 17-20, 2012. LNCS. Springer (to appear, 2012)"},{"key":"15_CR48","doi-asserted-by":"crossref","unstructured":"Gaspers, S., Szeider, S.: Strong backdoors to bounded treewidth SAT. Technical report 1204.6233, Arxiv.org (2012)","DOI":"10.1109\/FOCS.2013.59"},{"issue":"3\/4","key":"15_CR49","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BF03037169","volume":"9","author":"M. Gelfond","year":"1991","unstructured":"Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Comput.\u00a09(3\/4), 365\u2013386 (1991)","journal-title":"New Generation Comput."},{"key":"15_CR50","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation. Foundations of Artificial Intelligence, vol.\u00a03, pp. 89\u2013134. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03002-7"},{"issue":"3","key":"15_CR51","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1093\/comjnl\/bxm056","volume":"51","author":"G. Gottlob","year":"2006","unstructured":"Gottlob, G., Szeider, S.: Fixed-parameter algorithms for artificial intelligence, constraint satisfaction, and database problems. The Computer Journal\u00a051(3), 303\u2013325 (2006); survey paper","journal-title":"The Computer Journal"},{"key":"15_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-28639-4_15","volume-title":"Parameterized and Exact Computation","author":"J. Guo","year":"2004","unstructured":"Guo, J., H\u00fcffner, F., Niedermeier, R.: A Structural View on Parameterizing Problems: Distance from Triviality. In: Downey, R., Fellows, M., Dehne, F. (eds.) IWPEC 2004. LNCS, vol.\u00a03162, pp. 162\u2013173. Springer, Heidelberg (2004)"},{"key":"15_CR53","doi-asserted-by":"crossref","unstructured":"Hertli, T.: 3-SAT faster and simpler - unique-SAT bounds for PPSZ hold in general. In: Ostrovsky, R. (ed.) Proceedings of the 52nd Annual IEEE Symposium on Foundations of Computer Science (FOCS 2011). IEEE (2011)","DOI":"10.1109\/FOCS.2011.22"},{"issue":"2","key":"15_CR54","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1137\/0218026","volume":"18","author":"K. Iwama","year":"1989","unstructured":"Iwama, K.: CNF-satisfiability test by counting and polynomial average time. SIAM J. Comput.\u00a018(2), 385\u2013391 (1989)","journal-title":"SIAM J. Comput."},{"key":"15_CR55","doi-asserted-by":"crossref","unstructured":"Kakimura, N., Kawarabayashi, K., Kobayashi, Y.: Erd\u00f6s-P\u00f3sa property and its algorithmic applications: parity constraints, subset feedback set, and subset packing. In: Rabani, Y. (ed.) Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2012, Kyoto, Japan, January 17-19, pp. 1726\u20131736. SIAM (2012)","DOI":"10.1137\/1.9781611973099.137"},{"key":"15_CR56","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings ECAI 1992, pp. 359\u2013363 (1992)"},{"key":"15_CR57","unstructured":"Kawarabayashi, K., Kobayashi, Y.: Fixed-parameter tractability for the subset feedback set problem and the s-cycle packing problem. Technical report, University of Tokyo, Japan (2010); see also [55]"},{"key":"15_CR58","volume-title":"Propositional logic: deduction and algorithms","author":"H.K. B\u00fcning","year":"1999","unstructured":"B\u00fcning, H.K., Lettman, T.: Propositional logic: deduction and algorithms. Cambridge University Press, Cambridge (1999)"},{"issue":"1","key":"15_CR59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02983372","volume":"28","author":"D.E. Knuth","year":"1990","unstructured":"Knuth, D.E.: Nested satisfiability. Acta Informatica\u00a028(1), 1\u20136 (1990)","journal-title":"Acta Informatica"},{"key":"#cr-split#-15_CR60.1","doi-asserted-by":"crossref","unstructured":"Kolaitis, P.G., Vardi, M.Y.: Conjunctive-query containment and constraint satisfaction. J. of Computer and System Sciences\u00a061(2), 302-332 (2000)","DOI":"10.1006\/jcss.2000.1713"},{"key":"#cr-split#-15_CR60.2","unstructured":"Special issue on the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, Seattle, WA (1998)"},{"issue":"3","key":"15_CR61","first-page":"265","volume":"9","author":"L. Levin","year":"1973","unstructured":"Levin, L.: Universal sequential search problems. Problems of Information Transmission\u00a09(3), 265\u2013266 (1973)","journal-title":"Problems of Information Transmission"},{"issue":"1","key":"15_CR62","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H.R. Lewis","year":"1978","unstructured":"Lewis, H.R.: Renaming a set of clauses as a Horn set. J. of the ACM\u00a025(1), 134\u2013135 (1978)","journal-title":"J. of the ACM"},{"key":"15_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-21043-3_33","volume-title":"Advances in Artificial Intelligence","author":"Z. Li","year":"2011","unstructured":"Li, Z., van Beek, P.: Finding Small Backdoors in SAT Instances. In: Butz, C., Lingras, P. (eds.) Canadian AI 2011. LNCS, vol.\u00a06657, pp. 269\u2013280. Springer, Heidelberg (2011)"},{"issue":"2","key":"15_CR64","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"A. Gupta","year":"2005","unstructured":"Gupta, A., Prasad, M., Biere, A.: A survey of recent advances in SAT-based formal verification. Software Tools for Technology Transfer\u00a07(2), 156\u2013173 (2005)","journal-title":"Software Tools for Technology Transfer"},{"key":"15_CR65","doi-asserted-by":"crossref","unstructured":"Marek, V.W., Truszczynski, M.: Stable models and an alternative logic programming paradigm. In: The Logic Programming Paradigm: a 25-Year Perspective, pp. 169\u2013181. Springer (1999)","DOI":"10.1007\/978-3-642-60085-2_17"},{"issue":"1","key":"15_CR66","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/s00453-009-9326-z","volume":"58","author":"D. Marx","year":"2010","unstructured":"Marx, D., Schlotter, I.: Parameterized complexity and local search approaches for the stable marriage problem with ties. Algorithmica\u00a058(1), 170\u2013187 (2010)","journal-title":"Algorithmica"},{"issue":"1","key":"15_CR67","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.disopt.2010.07.004","volume":"8","author":"D. Marx","year":"2011","unstructured":"Marx, D., Schlotter, I.: Stable assignment with couples: parameterized complexity and local search. Discrete Optim.\u00a08(1), 25\u201340 (2011)","journal-title":"Discrete Optim."},{"key":"15_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-77120-3_25","volume-title":"Algorithms and Computation","author":"S. Mishra","year":"2007","unstructured":"Mishra, S., Raman, V., Saurabh, S., Sikdar, S., Subramanian, C.R.: The Complexity of Finding Subgraphs Whose Matching Number Equals the Vertex Cover Number. In: Tokuyama, T. (ed.) ISAAC 2007. LNCS, vol.\u00a04835, pp. 268\u2013279. Springer, Heidelberg (2007)"},{"issue":"3-4","key":"15_CR69","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I. Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4, I.: Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell.\u00a025(3-4), 241\u2013273 (1999); Logic programming with non-monotonic semantics: representing knowledge and its computation","journal-title":"Ann. Math. Artif. Intell."},{"key":"15_CR70","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, Vancouver, BC, Canada, May 10-13, pp. 96\u2013103 (2004)"},{"issue":"7-8","key":"15_CR71","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/s00236-007-0056-x","volume":"44","author":"N. Nishimura","year":"2007","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. Acta Informatica\u00a044(7-8), 509\u2013523 (2007)","journal-title":"Acta Informatica"},{"key":"15_CR72","unstructured":"Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of acyclic and almost acyclic CNF formulas. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, Chennai, India, December 15-18. LIPIcs, vol.\u00a08, pp. 84\u201395. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)"},{"key":"15_CR73","unstructured":"Ordyniak, S., Szeider, S.: Augmenting tractable fragments of abstract argumentation. In: Walsh, T. (ed.) Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 2011, pp. 1033\u20131038. AAAI Press (2011)"},{"key":"15_CR74","unstructured":"Otwell, C., Remshagen, A., Truemper, K.: An effective QBF solver for planning problems. In: Proceedings of MSV\/AMCS, pp. 311\u2013316. CSREA Press (2004)"},{"key":"15_CR75","unstructured":"Pan, G., Vardi, M.Y.: Fixed-parameter hierarchies inside PSPACE. In: Proceedings of 21th IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, WA, USA, August 12-15, pp. 27\u201336. IEEE Computer Society Press (2006)"},{"key":"15_CR76","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley (1994)"},{"issue":"3","key":"15_CR77","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1093\/logcom\/13.3.347","volume":"13","author":"S. Parsons","year":"2003","unstructured":"Parsons, S., Wooldridge, M., Amgoud, L.: Properties and complexity of some formal inter-agent dialogues. J. Logic Comput.\u00a013(3), 347\u2013376 (2003)","journal-title":"J. Logic Comput."},{"issue":"4","key":"15_CR78","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1016\/S0022-0000(03)00078-3","volume":"67","author":"K. Pietrzak","year":"2003","unstructured":"Pietrzak, K.: On the parameterized complexity of the fixed alphabet shortest common supersequence and longest common subsequence problems. J. of Computer and System Sciences\u00a067(4), 757\u2013771 (2003)","journal-title":"J. of Computer and System Sciences"},{"issue":"1","key":"15_CR79","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(92)90103-5","volume":"57","author":"J.L. Pollock","year":"1992","unstructured":"Pollock, J.L.: How to reason defeasibly. Artificial Intelligence\u00a057(1), 1\u201342 (1992)","journal-title":"Artificial Intelligence"},{"key":"15_CR80","doi-asserted-by":"crossref","unstructured":"Rahwan, I., Simari, G.R. (eds.): Argumentation in Artificial Intelligence. Springer (2009)","DOI":"10.1007\/978-0-387-98197-0"},{"issue":"3","key":"15_CR81","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1159892.1159898","volume":"2","author":"V. Raman","year":"2006","unstructured":"Raman, V., Saurabh, S., Subramanian, C.R.: Faster fixed parameter tractable algorithms for finding feedback vertex sets. ACM Transactions on Algorithms\u00a02(3), 403\u2013415 (2006)","journal-title":"ACM Transactions on Algorithms"},{"issue":"8","key":"15_CR82","doi-asserted-by":"publisher","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. of Computer and System Sciences\u00a075(8), 435\u2013450 (2009)","journal-title":"J. of Computer and System Sciences"},{"issue":"4","key":"15_CR83","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/j.orl.2003.10.009","volume":"32","author":"B. Reed","year":"2004","unstructured":"Reed, B., Smith, K., Vetta, A.: Finding odd cycle transversals. Oper. Res. Lett.\u00a032(4), 299\u2013301 (2004)","journal-title":"Oper. Res. Lett."},{"key":"15_CR84","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing conditional plans by a theorem-prover. J. Artif. Intell. Res.\u00a010, 323\u2013352 (1999)","journal-title":"J. Artif. Intell. Res."},{"issue":"3","key":"15_CR85","doi-asserted-by":"publisher","first-page":"929","DOI":"10.2307\/121059","volume":"150","author":"N. Robertson","year":"1999","unstructured":"Robertson, N., Seymour, P.D., Thomas, R.: Permanents, Pfaffian orientations, and even directed circuits. Ann. of Math (2)\u00a0150(3), 929\u2013975 (1999)","journal-title":"Ann. of Math. (2)"},{"issue":"1-2","key":"15_CR86","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(94)00092-1","volume":"82","author":"D. Roth","year":"1996","unstructured":"Roth, D.: On the hardness of approximate reasoning. Artificial Intelligence\u00a082(1-2), 273\u2013302 (1996)","journal-title":"Artificial Intelligence"},{"key":"15_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/11814948_35","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A. Sabharwal","year":"2006","unstructured":"Sabharwal, A., Ansotegui, C., Gomes, C.P., Hart, J.W., Selman, B.: QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 382\u2013395. Springer, Heidelberg (2006)"},{"key":"15_CR88","unstructured":"Samer, M., Szeider, S.: Backdoor trees. In: Twenty-Third Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, July 13\u201317, pp. 363\u2013368. AAAI Press (2008)"},{"issue":"1","key":"15_CR89","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. Journal of Automated Reasoning\u00a042(1), 77\u201397 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR90","unstructured":"Samer, M., Szeider, S.: Fixed-parameter tractability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol.\u00a0ch. 13, pp. 425\u2013454. IOS Press (2009)"},{"issue":"1","key":"15_CR91","doi-asserted-by":"publisher","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. Discrete Algorithms\u00a08(1), 50\u201364 (2010)","journal-title":"J. Discrete Algorithms"},{"key":"15_CR92","unstructured":"Sang, T., Beame, P., Kautz, H.A.: Performing bayesian inference by weighted model counting. In: Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, Pittsburgh, Pennsylvania, USA, July 9-13, pp. 475\u2013482. AAAI Press \/ The MIT Press (2005)"},{"key":"15_CR93","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., pp. 216\u2013226. ACM (1978)","DOI":"10.1145\/800133.804350"},{"key":"15_CR94","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proc. Theory of Computing, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"15_CR95","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-24605-3_15","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Szeider","year":"2004","unstructured":"Szeider, S.: On Fixed-Parameter Tractable Parameterizations of SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 188\u2013202. Springer, Heidelberg (2004)"},{"key":"#cr-split#-15_CR96.1","doi-asserted-by":"crossref","unstructured":"Szeider, S.: Backdoor sets for DLL subsolvers. Journal of Automated Reasoning\u00a035(1-3), 73-88 (2005)","DOI":"10.1007\/s10817-005-9007-9"},{"key":"#cr-split#-15_CR96.2","doi-asserted-by":"crossref","unstructured":"Reprinted as Giunchiglia, E., Walsh, T.(eds.): SAT 2005 - Satisfiability Research in the Year 2005, ch. 4. Springer Verlag (2006)","DOI":"10.1007\/978-1-4020-5571-3"},{"key":"15_CR97","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190059","volume":"6","author":"S. Szeider","year":"2008","unstructured":"Szeider, S.: Matched formulas and backdoor sets. J. on Satisfiability, Boolean Modeling and Computation\u00a06, 1\u201312 (2008)","journal-title":"J. on Satisfiability, Boolean Modeling and Computation"},{"key":"15_CR98","first-page":"93","volume-title":"Proceedings of the Twenty-Fifth Conference on Artificial Intelligence, AAAI 2011","author":"S. Szeider","year":"2011","unstructured":"Szeider, S.: Limits of preprocessing. In: Proceedings of the Twenty-Fifth Conference on Artificial Intelligence, AAAI 2011, pp. 93\u201398. AAAI Press, Menlo Park (2011)"},{"issue":"2","key":"15_CR99","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"M.N. 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. Symbolic Comput.\u00a035(2), 73\u2013106 (2003)","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"15_CR100","first-page":"93","volume":"20","author":"D.S. Weld","year":"1999","unstructured":"Weld, D.S.: Recent advances in AI planning. AI Magazine\u00a020(2), 93\u2013123 (1999)","journal-title":"AI Magazine"},{"key":"15_CR101","unstructured":"Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI 2003, pp. 1173\u20131178. Morgan Kaufmann (2003)"}],"container-title":["Lecture Notes in Computer Science","The Multivariate Algorithmic Revolution and Beyond"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30891-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T16:58:45Z","timestamp":1743526725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30891-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308901","9783642308918"],"references-count":103,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30891-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}