{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:18Z","timestamp":1759638978484},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2006,8,15]],"date-time":"2006-08-15T00:00:00Z","timestamp":1155600000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2006,10,5]]},"DOI":"10.1007\/s10817-005-9006-x","type":"journal-article","created":{"date-parts":[[2006,8,14]],"date-time":"2006-08-14T09:02:36Z","timestamp":1155546156000},"page":"51-72","source":"Crossref","is-referenced-by-count":28,"title":["Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas"],"prefix":"10.1007","volume":"35","author":[{"given":"Michael","family":"Alekhnovich","sequence":"first","affiliation":[]},{"given":"Edward A.","family":"Hirsch","sequence":"additional","affiliation":[]},{"given":"Dmitry","family":"Itsykson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,8,15]]},"reference":[{"key":"9006_CR1","unstructured":"Achlioptas, D., Beame, P. and Molloy, M.: A sharp threshold in proof complexity, J. Comput. Syst. Sci. (2003)."},{"key":"9006_CR2","unstructured":"Achlioptas, D., Beame, P. and Molloy, M.: Exponential bounds for DPLL below the satisfiability threshold, in Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA'04, 2004, pp. 139\u2013140."},{"key":"9006_CR3","doi-asserted-by":"crossref","unstructured":"Achlioptas, D. and Sorkin, G. B.: Optimal myopic algorithms for random 3-SAT, in Proceedings of the 41st Annual IEEE Symposium on Foundations of Computer Science, FOCS'00, 2000.","DOI":"10.1109\/SFCS.2000.892327"},{"key":"9006_CR4","unstructured":"Alekhnovich, M. and Ben-Sasson, E.: Analysis of the random walk algorithm on random 3-CNFs, Manuscript, 2002."},{"key":"9006_CR5","unstructured":"Alekhnovich, M., Ben-Sasson, E., Razborov, A. and Wigderson, A.: Pseudorandom generators in propositional complexity, in Proceedings of the 41st Annual IEEE Symposium on Foundations of Computer Science, FOCS'00, Journal version is to appear in SIAM Journal on Computing, 2000."},{"key":"9006_CR6","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Borodin, A., Buresh-Oppenheim, J., Impagliazzo, R., Magen, A. and Pitassi, T.: Toward a model for backtracking and dynamic programming, in Proceedings of the 20th Annual Conference on Computational Complexity, 2005, pp. 308\u2013322.","DOI":"10.1109\/CCC.2005.32"},{"key":"9006_CR7","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M. and Razborov, A.: Lower bounds for the polynomial calculus: Non-binomial case, in Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science, 2001.","DOI":"10.1109\/SFCS.2001.959893"},{"issue":"2","key":"9006_CR8","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E. Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E. and Wigderson, A.: Short proofs are narrow \u2013 resolution made simple, J. ACM 48(2) (2001), 149\u2013169.","journal-title":"J. ACM"},{"key":"9006_CR9","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G. and Loveland, D.: A machine program for theorem-proving, Commun. ACM 5 (1962), 394\u2013397.","journal-title":"Commun. ACM"},{"key":"9006_CR10","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. ACM 7 (1960), 201\u2013215.","journal-title":"J. ACM"},{"issue":"1\/2","key":"9006_CR11","doi-asserted-by":"crossref","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, J. Autom. Reason. 24(1\/2) (2000), 127\u2013143. Also reprinted in \u201cHighlights of Satisfiability Research in the Year 2000\u201d, Volume 63 in Frontiers in Artificial Intelligence and Applications, IOS.","journal-title":"J. Autom. Reason."},{"key":"9006_CR12","unstructured":"Iwama, K. and Tamaki, S.: Improved upper bounds for 3-SAT, in Proceedings of the Fifteenth Annual ACM\u2013SIAM Symposium on Discrete Algorithms, SODA'04, 2004, pp. 328\u2013328."},{"key":"9006_CR13","first-page":"139","volume":"293","author":"S. I. Nikolenko","year":"2002","unstructured":"Nikolenko, S. I.: Hard satisfiable formulas for DPLL-type algorithms, Zap. Nauc. Semin. POMI 293 (2002), 139\u2013148. English translation is to appear in Journal of Mathematical Sciences: Consultants Bureau, N.Y., March 2005, Vol. 126, No. 3, pp. 1205\u20131209.","journal-title":"Zap. Nauc. Semin. POMI"},{"key":"9006_CR14","unstructured":"Pudl\u00e1k, P. and Impagliazzo, R.: A lower bound for DLL algorithms for k-SAT, in Proceedings of the 11th Annual ACM\u2013SIAM Symposium on Discrete Algorithms, SODA'00, 2000."},{"key":"9006_CR15","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/s10472-005-0424-6","volume":"43","author":"L. Simon","year":"2005","unstructured":"Simon, L., Le Berre, D. and Hirsch, E. A.: The SAT 2002 Competition, Ann. Math. Artif. Intell. 43 (2005), 307\u2013342.","journal-title":"Ann. Math. Artif. Intell."},{"key":"9006_CR16","first-page":"234","volume":"8","author":"G. S. Tseitin","year":"1968","unstructured":"Tseitin, G. S.: On the complexity of derivation in the propositional calculus, Zap. Nauc. Semin. LOMI 8 (1968), 234\u2013259. English translation of this volume: Consultants Bureau, N.Y., 1970, pp. 115\u2013125.","journal-title":"Zap. Nauc. Semin. LOMI"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9006-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-9006-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9006-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:46Z","timestamp":1559265706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-9006-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8,15]]},"references-count":16,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2006,10,5]]}},"alternative-id":["9006"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-9006-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8,15]]}}}