{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:29Z","timestamp":1725533909414},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_14","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"128-140","source":"Crossref","is-referenced-by-count":2,"title":["An Exponential Lower Bound for Width-Restricted Clause Learning"],"prefix":"10.1007","author":[{"given":"Jan","family":"Johannsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"81","DOI":"10.4086\/toc.2007.v003a005","volume":"3","author":"M. Alekhnovich","year":"2007","unstructured":"Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory of Computing\u00a03, 81\u2013102 (2007)","journal-title":"Theory of Computing"},{"key":"14_CR2","unstructured":"Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solver real-world SAT instances. In: Proc. 14th Natl. Conference on Artificial Intelligence, pp. 203\u2013208 (1997)"},{"issue":"4","key":"14_CR3","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s00493-004-0036-5","volume":"24","author":"E. Ben-Sasson","year":"2004","unstructured":"Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near-optimal separation of general and tree-like resolution. Combinatorica\u00a024(4), 585\u2013604 (2004)","journal-title":"Combinatorica"},{"issue":"4","key":"14_CR4","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"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Logical Methods in Computer Science\u00a04(4) (2008)","DOI":"10.2168\/LMCS-4(4:13)2008"},{"issue":"7","key":"14_CR6","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. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"14_CR7","first-page":"283","volume-title":"Proceedings of the 23rd AAAI Conference on Artificial Intelligence, AAAI 2008","author":"P. Hertel","year":"2008","unstructured":"Hertel, P., Bacchus, F., Pitassi, T., van Gelder, A.: Clause learning can effectively p-simulate general propositional resolution. In: Fox, D., Gomes, C.P. (eds.) Proceedings of the 23rd AAAI Conference on Artificial Intelligence, AAAI 2008, pp. 283\u2013290. AAAI Press, Menlo Park (2008)"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B. Krishnamurthy","year":"1985","unstructured":"Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica\u00a022, 253\u2013274 (1985)","journal-title":"Acta Informatica"},{"key":"14_CR9","unstructured":"Letz, R.: Personal communication"},{"issue":"5","key":"14_CR10","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":"14_CR11","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proc. IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s002360050044","volume":"33","author":"G. St\u00e5lmarck","year":"1996","unstructured":"St\u00e5lmarck, G.: Short resolution proofs for a sequence of tricky formulas. Acta Informatica\u00a033, 277\u2013280 (1996)","journal-title":"Acta Informatica"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"14_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1007\/11591191_40","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Gelder van","year":"2005","unstructured":"van Gelder, A.: Pool resolution and its relation to regular resolution and DPLL with clause learning. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 580\u2013594. Springer, Heidelberg (2005)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: Proc. IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pp. 279\u2013285 (2001)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T22:58:06Z","timestamp":1558393086000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}