{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:00:24Z","timestamp":1725796824078},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319092836"},{"type":"electronic","value":"9783319092843"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_8","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"85-102","source":"Crossref","is-referenced-by-count":5,"title":["Fixed-Parameter Tractable Reductions to SAT"],"prefix":"10.1007","author":[{"given":"Ronald","family":"de Haan","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Atserias, A., Oliva, S.: Bounded-width QBF is PSPACE-complete. In: Portier, N., Wilke, T. (eds.) 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, Kiel, Germany, February 27 - March 2. LIPIcs, vol.\u00a020, pp. 44\u201354. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)","key":"8_CR1"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.: Qubos: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 187\u2013201. Springer, Heidelberg (2002)"},{"issue":"2","key":"8_CR3","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A. Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/11527695_4","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M., Bernardini, S.: Incremental compilation-to-SAT procedures. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 46\u201358. Springer, Heidelberg (2005)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 457\u2013481. IOS Press (2009)","key":"8_CR6"},{"doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS\/ETAPS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)","key":"8_CR7","DOI":"10.1007\/3-540-49059-0_14"},{"unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)","key":"8_CR8"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-19488-6_110","volume-title":"Automata, Languages and Programming","author":"H.L. Bodlaender","year":"1988","unstructured":"Bodlaender, H.L.: Dynamic programming on graphs with bounded treewidth. In: Lepist\u00f6, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol.\u00a0317, pp. 105\u2013118. Springer, Heidelberg (1988)"},{"issue":"1-2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00228-4","volume":"209","author":"H.L. Bodlaender","year":"1998","unstructured":"Bodlaender, H.L.: A partial k-arboretum of graphs with bounded treewidth. Theoretical Computer Science\u00a0209(1-2), 1\u201345 (1998)","journal-title":"Theoretical Computer Science"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-30891-8_12","volume-title":"The Multivariate Algorithmic Revolution and Beyond","author":"H.L. Bodlaender","year":"2012","unstructured":"Bodlaender, H.L.: Fixed-parameter tractability of treewidth and pathwidth. In: Bodlaender, H.L., Downey, R., Fomin, F.V., Marx, D. (eds.) Fellows Festschrift 2012. LNCS, vol.\u00a07370, pp. 196\u2013227. Springer, Heidelberg (2012)"},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1137\/S0097539790178069","volume":"25","author":"R. Chang","year":"1996","unstructured":"Chang, R., Kadin, J.: The Boolean Hierarchy and the Polynomial Hierarchy: A closer connection. SIAM J. Comput.\u00a025(2), 340\u2013354 (1996)","journal-title":"SIAM J. Comput."},{"key":"8_CR13","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)"},{"issue":"0","key":"8_CR14","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/j.artint.2013.10.001","volume":"206","author":"W. Dvo\u0159\u00e1k","year":"2014","unstructured":"Dvo\u0159\u00e1k, W., J\u00e4rvisalo, M., Wallner, J.P., Woltran, S.: Complexity-sensitive decision procedures for abstract argumentation. Artificial Intelligence\u00a0206(0), 53\u201378 (2014)","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Fichte, J.K., Szeider, S.: Backdoors to normality for disjunctive logic programs. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2013, pp. 320\u2013327. AAAI Press (2013)","key":"8_CR15","DOI":"10.1609\/aaai.v27i1.8624"},{"issue":"2","key":"8_CR16","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0890-5401(03)00161-5","volume":"187","author":"J. Flum","year":"2003","unstructured":"Flum, J., Grohe, M.: Describing parameterized complexity classes. Information and Computation\u00a0187(2), 291\u2013319 (2003)","journal-title":"Information and Computation"},{"key":"8_CR17","series-title":"An EATCS Series","volume-title":"Parameterized Complexity Theory, Texts in Theoretical Computer Science","author":"J. Flum","year":"2006","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory, Texts in Theoretical Computer Science. An EATCS Series, vol.\u00a0XIV. Springer, Berlin (2006)"},{"key":"8_CR18","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)"},{"issue":"6","key":"8_CR19","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1016\/j.ic.2008.03.002","volume":"206","author":"J. Goldsmith","year":"2008","unstructured":"Goldsmith, J., Hagen, M., Mundhenk, M.: Complexity of DNF minimization and isomorphism testing for monotone formulas. Information and Computation\u00a0206(6), 760\u2013775 (2008)","journal-title":"Information and Computation"},{"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)","key":"8_CR20","DOI":"10.1016\/S1574-6526(07)03002-7"},{"issue":"2","key":"8_CR21","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0004-3702(93)90069-N","volume":"61","author":"G. Gottlob","year":"1993","unstructured":"Gottlob, G., Ferm\u00fcller, C.G.: Removing redundancy from a clause. Artificial Intelligence\u00a061(2), 263\u2013289 (1993)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.artint.2009.10.003","volume":"174","author":"G. Gottlob","year":"2010","unstructured":"Gottlob, G., Pichler, R., Wei, F.: Bounded treewidth as a key to tractability of knowledge representation and reasoning. Artificial Intelligence\u00a0174(1), 105\u2013132 (2010)","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, E., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2008), Daytion, Ohio, USA, November 3-5 , pp. 74\u201383. IEEE Computer Society (2008)","key":"8_CR23","DOI":"10.1109\/ICTAI.2008.39"},{"unstructured":"de Haan, R., Szeider, S.: The parameterized complexity of reasoning problems beyond NP. In: Baral, C., De Giacomo, G., Eiter, T. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, Vienna, Austria, July 20-24. AAAI Press (2014)","key":"8_CR24"},{"issue":"1","key":"8_CR25","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(90)90191-J","volume":"71","author":"J. Hartmanis","year":"1990","unstructured":"Hartmanis, J.: New developments in structural complexity theory. Theoretical Computer Science\u00a071(1), 79\u201393 (1990)","journal-title":"Theoretical Computer Science"},{"issue":"1&2","key":"8_CR26","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0743-1066(93)90018-C","volume":"15","author":"J.N. Hooker","year":"1993","unstructured":"Hooker, J.N.: Solving the incremental satisfiability problem. J. Logic Programming\u00a015(1&2), 177\u2013186 (1993)","journal-title":"J. Logic Programming"},{"key":"8_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0045375","volume-title":"Treewidth: Computations and Approximations","author":"T. Kloks","year":"1994","unstructured":"Kloks, T.: Treewidth: Computations and Approximations. Springer, Berlin (1994)"},{"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\u2013332 (2000), special issue on the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (Seattle, WA, 1998)","key":"8_CR28","DOI":"10.1145\/275487.275511"},{"doi-asserted-by":"crossref","unstructured":"Krajicek, J.: Bounded arithmetic, propositional logic and complexity theory. Cambridge University Press (1995)","key":"8_CR29","DOI":"10.1017\/CBO9780511529948"},{"issue":"3","key":"8_CR30","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1016\/0022-0000(88)90039-6","volume":"36","author":"M.W. Krentel","year":"1988","unstructured":"Krentel, M.W.: The complexity of optimization problems. J. of Computer and System Sciences\u00a036(3), 490\u2013509 (1988)","journal-title":"J. of Computer and System Sciences"},{"issue":"8","key":"8_CR31","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S. Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability from theoretical hardness to practical success. Communications of the ACM\u00a052(8), 76\u201382 (2009)","journal-title":"Communications of the ACM"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-39799-8_39","volume-title":"Computer Aided Verification","author":"J. Marques-Silva","year":"2013","unstructured":"Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in Boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 592\u2013607. Springer, Heidelberg (2013)"},{"key":"8_CR33","series-title":"Oxford Lecture Series in Mathematics and its Applications","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566076.001.0001","volume-title":"Invitation to Fixed-Parameter Algorithms","author":"R. Niedermeier","year":"2006","unstructured":"Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and its Applications. Oxford University Press, Oxford (2006)"},{"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 (2006)","key":"8_CR34"},{"unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley (1994)","key":"8_CR35"},{"unstructured":"Pfandler, A., R\u00fcmmele, S., Szeider, S.: Backdoors to abduction. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013. AAAI Press\/IJCAI (2013)","key":"8_CR36"},{"unstructured":"Prestwich, S.D.: CNF encodings. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, pp. 75\u201397. IOS Press (2009)","key":"8_CR37"},{"key":"8_CR38","first-page":"96","volume":"103","author":"K.A. Sakallah","year":"2011","unstructured":"Sakallah, K.A., Marques-Silva, J.: Anatomy and empirical evaluation of modern SAT solvers. Bulletin of the European Association for Theoretical Computer Science\u00a0103, 96\u2013121 (2011)","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"issue":"2","key":"8_CR39","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.jcss.2009.04.003","volume":"76","author":"M. Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Constraint satisfaction with bounded treewidth revisited. J. of Computer and System Sciences\u00a076(2), 103\u2013114 (2010)","journal-title":"J. of Computer and System Sciences"},{"issue":"1","key":"8_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L.J. Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theoretical Computer Science\u00a03(1), 1\u201322 (1976)","journal-title":"Theoretical Computer Science"},{"unstructured":"Umans, C.: Approximability and Completeness in the Polynomial Hierarchy. Ph.D. thesis. University of California, Berkeley (2000)","key":"8_CR41"},{"issue":"5","key":"8_CR42","doi-asserted-by":"publisher","first-page":"833","DOI":"10.1137\/0219058","volume":"19","author":"K.W. Wagner","year":"1990","unstructured":"Wagner, K.W.: Bounded query classes. SIAM J. Comput.\u00a019(5), 833\u2013846 (1990)","journal-title":"SIAM J. Comput."},{"doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: A new incremental satisfiability engine. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, pp. 542\u2013545. ACM (2001)","key":"8_CR43","DOI":"10.1145\/378239.379019"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,14]],"date-time":"2023-07-14T22:57:29Z","timestamp":1689375449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}