{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:57:05Z","timestamp":1725566225826},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230717"},{"type":"electronic","value":"9783540286394"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-28639-4_20","type":"book-chapter","created":{"date-parts":[[2010,9,20]],"date-time":"2010-09-20T16:25:35Z","timestamp":1284999935000},"page":"223-234","source":"Crossref","is-referenced-by-count":0,"title":["On Finding Short Resolution Refutations and Small Unsatisfiable Subsets"],"prefix":"10.1007","author":[{"given":"Michael R.","family":"Fellows","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]},{"given":"Graham","family":"Wrightson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1016\/0097-3165(86)90060-9","volume":"43","author":"R. Aharoni","year":"1986","unstructured":"Aharoni, R., Linial, N.: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. J. Combin. Theory Ser. A\u00a043, 196\u2013204 (1986)","journal-title":"J. Combin. Theory Ser. A"},{"issue":"1","key":"20_CR2","doi-asserted-by":"publisher","first-page":"171","DOI":"10.2307\/2694916","volume":"66","author":"M. Alekhnovich","year":"2001","unstructured":"Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate. J. Symbolic Logic\u00a066(1), 171\u2013191 (2001)","journal-title":"J. Symbolic Logic"},{"key":"20_CR3","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1109\/SFCS.2001.959895","volume-title":"42nd IEEE Symposium on Foundations of Computer Science (FOCS 2001)","author":"M. Alekhnovich","year":"2001","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: 42nd IEEE Symposium on Foundations of Computer Science (FOCS 2001), pp. 210\u2013219. IEEE Computer Soc., Los Alamitos (2001)"},{"key":"20_CR4","first-page":"42","volume-title":"Current trends in theoretical computer science","author":"P. Beame","year":"2001","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present, and future. In: Current trends in theoretical computer science, pp. 42\u201370. World Sci. Publishing, River Edge (2001)"},{"issue":"1-2","key":"20_CR5","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. Theoret. Comput. Sci.\u00a0209(1-2), 1\u201345 (1998)","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04943-3","volume-title":"Boolean functions and computation models","author":"P. Clote","year":"2002","unstructured":"Clote, P., Kranakis, E.: Boolean functions and computation models. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"20_CR7","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":"20_CR8","doi-asserted-by":"crossref","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. Springer, Heidelberg (1999)"},{"key":"20_CR9","volume-title":"Finite model theory. Perspectives in Mathematical Logic","author":"H.-D. Ebbinghaus","year":"1999","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite model theory. Perspectives in Mathematical Logic, 2nd edn. Springer, Heidelberg (1999)","edition":"2"},{"issue":"6","key":"20_CR10","doi-asserted-by":"publisher","first-page":"1184","DOI":"10.1145\/504794.504798","volume":"48","author":"M. Frick","year":"2001","unstructured":"Frick, M., Grohe, M.: Deciding first-order properties of locally treedecomposable structures. Journal of the ACM\u00a048(6), 1184\u20131206 (2001)","journal-title":"Journal of the ACM"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoret. Comput. Sci.\u00a039, 297\u2013308 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BFb0029974","volume-title":"Mathematical Foundations of Computer Science 1997","author":"K. Iwama","year":"1997","unstructured":"Iwama, K.: Complexity of finding short resolution proofs. In: Privara, I., Ru\u017ei\u010dka, P. (eds.) MFCS 1997. LNCS, vol.\u00a01295, pp. 309\u2013318. Springer, Heidelberg (1997)"},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0166-218X(94)90143-0","volume":"52","author":"J. Kratochv\u00edl","year":"1994","unstructured":"Kratochv\u00edl, J.: A special planar satisfiability problem and a consequence of its NP-completeness. Discr. Appl. Math.\u00a052, 233\u2013252 (1994)","journal-title":"Discr. Appl. Math."},{"key":"20_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements of Finite Model Theory. Texts in Theoretical Computer Science","author":"L. Libkin","year":"2004","unstructured":"Libkin, L.: Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"issue":"2","key":"20_CR15","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1137\/0211025","volume":"11","author":"D. Lichtenstein","year":"1982","unstructured":"Lichtenstein, D.: Planar formulae and their uses. SIAM J. Comput.\u00a011(2), 329\u2013343 (1982)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"20_CR16","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1006\/jcss.1999.1626","volume":"58","author":"C.H. Papadimitriou","year":"1999","unstructured":"Papadimitriou, C.H., Yannakakis, M.: On the complexity of database queries. J. of Computer and System Sciences\u00a058(3), 407\u2013427 (1999)","journal-title":"J. of Computer and System Sciences"},{"key":"20_CR17","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)"},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0166-218X(84)90081-7","volume":"8","author":"C.A. Tovey","year":"1984","unstructured":"Tovey, C.A.: A simplified NP-complete satisfiability problem. Discr. Appl. Math.\u00a08(1), 85\u201389 (1984)","journal-title":"Discr. Appl. Math."},{"key":"#cr-split#-20_CR19.1","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Zap. Nauchn. Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR??8, 23???41 (1968);"},{"key":"#cr-split#-20_CR19.2","unstructured":"Russian. English translation in J. Siekmann and G. Wrightson (eds.) Automation of Reasoning. Classical Papers on Computer Science 1967???1970, pp. 466???483. Springer, Heidelberg (1983)"}],"container-title":["Lecture Notes in Computer Science","Parameterized and Exact Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-28639-4_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:26:45Z","timestamp":1605742005000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-28639-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230717","9783540286394"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-28639-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}