{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:11:11Z","timestamp":1794381071478,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540228493","type":"print"},{"value":"9783540278368","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27836-8_10","type":"book-chapter","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T18:53:21Z","timestamp":1284576801000},"page":"84-96","source":"Crossref","is-referenced-by-count":8,"title":["Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas"],"prefix":"10.1007","author":[{"given":"Michael","family":"Alekhnovich","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edward A.","family":"Hirsch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitry","family":"Itsykson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Achlioptas, D., Beame, P., Molloy, M.: A sharp threshold in proof complexity. JCSS (2003)"},{"key":"10_CR2","unstructured":"Achlioptas, D., Beame, P., Molloy, M.: Exponential bounds for DPLL below the satisfiability threshold. In: SODA 2004 (2004)"},{"key":"10_CR3","unstructured":"Achlioptas, D., Sorkin, G.B.: Optimal myopic algorithms for random 3-SAT. In: FOCS 2000 (2000)"},{"key":"10_CR4","unstructured":"Alekhnovich, M., Ben-Sasson, E.: Analysis of the random walk algorithm on random 3-CNFs (2002) (manuscript)"},{"key":"#cr-split#-10_CR5.1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Ben-Sasson, E., Razborov, A., Wigderson, A.: Pseudorandom generators in propositional complexity. In: FOCS 2000 (2000);","DOI":"10.1109\/SFCS.2000.892064"},{"key":"#cr-split#-10_CR5.2","unstructured":"Journal version is to appear in SIAM J. Comp."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.: Lower bounds for the polynomial calculus: non-binomial case. In: FOCS 2001 (2001)","DOI":"10.1109\/SFCS.2001.959893"},{"issue":"2","key":"10_CR7","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 \u2014 resolution made simple. JACM\u00a048(2), 149\u2013169 (2001)","journal-title":"JACM"},{"key":"10_CR8","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 theoremproving. Comm. ACM\u00a05, 394\u2013397 (1962)","journal-title":"Comm. ACM"},{"key":"10_CR9","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. JACM\u00a07, 201\u2013215 (1960)","journal-title":"JACM"},{"issue":"1\/2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1023\/A:1006318521185","volume":"24","author":"E.A. Hirsch","year":"2000","unstructured":"Hirsch, E.A.: SAT local search algorithms: Worst-case study. JAR\u00a024(1\/2), 127\u2013143 (2000)","journal-title":"JAR"},{"key":"10_CR11","first-page":"139","volume":"293","author":"S.I. Nikolenko","year":"2002","unstructured":"Nikolenko, S.I.: Hard satisfiable formulas for DPLL-type algorithms. Zapiski nauchnyh seminarov POMI\u00a0293, 139\u2013148 (2002); English translation is to appear in Journal of Mathematical Sciences","journal-title":"Zapiski nauchnyh seminarov POMI"},{"key":"10_CR12","unstructured":"Pudl\u00e1k, P., Impagliazzo, R.: A lower bound for DLL algorithms for k-SAT. In: SODA 2000 (2000)"},{"key":"10_CR13","unstructured":"Simon, L., Le Berre, D., Hirsch, E.A.: The SAT 2002 Competition. To appear in AMAI (2002)"},{"key":"10_CR14","first-page":"234","volume":"8","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Zapiski nauchnykh seminarov LOMI\u00a08, 234\u2013259 (1968); English translation of this volume: Consultants Bureau, N.Y., pp. 115\u2013125 (1970)","journal-title":"Zapiski nauchnykh seminarov LOMI"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27836-8_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:23:48Z","timestamp":1605741828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27836-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540228493","9783540278368"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27836-8_10","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b99859","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}