{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:17:28Z","timestamp":1725585448009},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642215803"},{"type":"electronic","value":"9783642215810"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_3","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:30:19Z","timestamp":1307698219000},"page":"5-18","source":"Crossref","is-referenced-by-count":3,"title":["Parameterized Complexity of DPLL Search Procedures"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"given":"Nicola","family":"Galesi","sequence":"additional","affiliation":[]},{"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"1347","DOI":"10.1137\/06066850X","volume":"38","author":"M. Alekhnovich","year":"2008","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. SIAM Journal on Computing\u00a038(4), 1347\u20131363 (2008)","journal-title":"SIAM Journal on Computing"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s00037-010-0288-y","volume":"19","author":"K. Amano","year":"2010","unstructured":"Amano, K.: Subgraph isomorphism on AC0 circuits. Computational Complexity\u00a019(2), 183\u2013210 (2010)","journal-title":"Computational Complexity"},{"issue":"3","key":"3_CR3","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s00037-007-0230-0","volume":"16","author":"P. Beame","year":"2007","unstructured":"Beame, P., Impagliazzo, R., Sabharwal, A.: The resolution complexity of independent sets and vertex covers in random graphs. Comput. Complex.\u00a016(3), 245\u2013297 (2007)","journal-title":"Comput. Complex."},{"issue":"4","key":"3_CR4","doi-asserted-by":"publisher","first-page":"1048","DOI":"10.1137\/S0097539700369156","volume":"31","author":"P. Beame","year":"2002","unstructured":"Beame, P., Karp, R.M., Pitassi, T., Saks, M.E.: The efficiency of resolution and Davis-Putnam procedures. SIAM J. Comput.\u00a031(4), 1048\u20131075 (2002)","journal-title":"SIAM J. Comput."},{"key":"3_CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res.\u00a022, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Proc. 37th IEEE Symposium on the Foundations of Computer Science, pp. 274\u2013282 (1996)","DOI":"10.1109\/SFCS.1996.548486"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1112\/plms\/s3-73.1.1","volume":"73","author":"P.W. Beame","year":"1996","unstructured":"Beame, P.W., Impagliazzo, R., Kraj\u00ed\u010dek, J., Pitassi, T., Pudl\u00e1k, P.: Lower bounds on Hilbert\u2019s Nullstellensatz and propositional proofs. Proc. London Mathematical Society\u00a073(3), 1\u201326 (1996)","journal-title":"Proc. London Mathematical Society"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E. Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. Journal of the ACM\u00a048(2), 149\u2013169 (2001)","journal-title":"Journal of the ACM"},{"key":"3_CR9","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: Hardness of parameterized resolution. Technical Report TR10-059, Electronic Colloquium on Computational Complexity (2010)"},{"issue":"23","key":"3_CR10","doi-asserted-by":"publisher","first-page":"1074","DOI":"10.1016\/j.ipl.2010.09.007","volume":"110","author":"O. Beyersdorff","year":"2010","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Information Processing Letters\u00a0110(23), 1074\u20131077 (2010)","journal-title":"Information Processing Letters"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M., Razborov, A.: Parameterized bounded-depth Frege is not optimal. Technical Report TR10-198, Electronic Colloquium on Computational Complexity (2010)","DOI":"10.1007\/978-3-642-22006-7_53"},{"key":"3_CR12","unstructured":"Blake, A.: Canonical expressions in boolean algebra. PhD thesis, University of Chicago (1937)"},{"issue":"5","key":"3_CR13","doi-asserted-by":"publisher","first-page":"1462","DOI":"10.1137\/S0097539799352474","volume":"30","author":"M.L. Bonet","year":"2000","unstructured":"Bonet, M.L., Esteban, J.L., Galesi, N., Johannsen, J.: On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Journal on Computing\u00a030(5), 1462\u20131484 (2000)","journal-title":"SIAM Journal on Computing"},{"issue":"4","key":"3_CR14","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s000370100000","volume":"10","author":"M.L. Bonet","year":"2001","unstructured":"Bonet, M.L., Galesi, N.: Optimality of size-width tradeoffs for resolution. Computational Complexity\u00a010(4), 261\u2013276 (2001)","journal-title":"Computational Complexity"},{"issue":"1","key":"3_CR15","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.apal.2007.09.003","volume":"151","author":"Y. Chen","year":"2008","unstructured":"Chen, Y., Flum, J.: The parameterized complexity of maximality and minimality problems. Annals of Pure and Applied Logic\u00a0151(1), 22\u201361 (2008)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"4","key":"3_CR16","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. J. ACM\u00a035(4), 759\u2013768 (1988)","journal-title":"J. ACM"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S.A. Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic\u00a044(1), 36\u201350 (1979)","journal-title":"The Journal of Symbolic Logic"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Dantchev, S.S., Martin, B., Szeider, S.: Parameterized proof complexity. In: Proc. 48th IEEE Symposium on the Foundations of Computer Science, pp. 150\u2013160 (2007)","DOI":"10.1109\/FOCS.2007.53"},{"issue":"7","key":"3_CR19","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.W.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 210\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"14","key":"3_CR21","doi-asserted-by":"publisher","first-page":"1343","DOI":"10.1016\/j.artint.2009.06.005","volume":"173","author":"Y. Gao","year":"2009","unstructured":"Gao, Y.: Data reductions, fixed parameter tractability, and random weighted d-CNF satisfiability. Artificial Intelligence\u00a0173(14), 1343\u20131366 (2009)","journal-title":"Artificial Intelligence"},{"key":"3_CR22","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. Theor. Comput. Sci.\u00a039, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR23","doi-asserted-by":"publisher","DOI":"10.1002\/9781118032718","volume-title":"Random Graphs","author":"S. Janson","year":"2000","unstructured":"Janson, S., \u0141uczak, T., Ruci\u0144ski, A.: Random Graphs. Wiley, Chichester (2000)"},{"key":"3_CR24","unstructured":"Pudl\u00e1k, P., Impagliazzo, R.: A lower bound for DLL algorithms for SAT. In: Proc. 11th Symposium on Discrete Algorithms, pp. 128\u2013136 (2000)"},{"key":"3_CR25","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Rossman, B.: On the constant-depth complexity of k-clique. In: Proc. 40th ACM Symposium on Theory of Computing, pp. 721\u2013730 (2008)","DOI":"10.1145\/1374376.1374480"},{"key":"3_CR27","first-page":"193","volume-title":"Proc. 51th IEEE Symposium on the Foundations of Computer Science","author":"B. Rossman","year":"2010","unstructured":"Rossman, B.: The monotone complexity of k-clique on random graphs. In: Proc. 51th IEEE Symposium on the Foundations of Computer Science, pp. 193\u2013201. IEEE Computer Society, Los Alamitos (2010)"},{"issue":"5","key":"3_CR28","doi-asserted-by":"publisher","first-page":"1171","DOI":"10.1137\/S0097539703428555","volume":"33","author":"N. Segerlind","year":"2004","unstructured":"Segerlind, N., Buss, S.R., Impagliazzo, R.: A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM Journal on Computing\u00a033(5), 1171\u20131200 (2004)","journal-title":"SIAM Journal on Computing"},{"key":"3_CR29","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s002360050044","volume":"33","author":"G. Stalmark","year":"1996","unstructured":"Stalmark, G.: Short resolution proofs for a sequence of tricky formulas. Acta Informatica\u00a033, 277\u2013280 (1996)","journal-title":"Acta Informatica"},{"issue":"1","key":"3_CR30","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM\u00a034(1), 209\u2013219 (1987)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T12:20:54Z","timestamp":1560255654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}