{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T14:11:38Z","timestamp":1781014298886,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141850","type":"print"},{"value":"9783642141867","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-14186-7_4","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:20:37Z","timestamp":1278613237000},"page":"16-29","source":"Crossref","is-referenced-by-count":6,"title":["Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas"],"prefix":"10.1007","author":[{"given":"Eli","family":"Ben-Sasson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Johannsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"#cr-split#-4_CR1.1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory of Computing\u00a03, 81\u2013102 (2007);","DOI":"10.4086\/toc.2007.v003a005"},{"key":"#cr-split#-4_CR1.2","unstructured":"Preliminary Version in Proc. 34th ACM Symposium on Theory of Computing (2002)"},{"key":"4_CR2","volume-title":"The Probabilistic Method","author":"N. Alon","year":"2002","unstructured":"Alon, N., Spencer, J.: The Probabilistic Method. John Wiley and Sons, Chichester (2002)"},{"key":"#cr-split#-4_CR3.1","doi-asserted-by":"crossref","unstructured":"Atserias, A., Dalmau, V.: A combinatorial characterization of resolution width. Journal of Computer and System Sciences\u00a074, 323\u2013334 (2008);","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"#cr-split#-4_CR3.2","unstructured":"Preliminary version in Proc. 18th IEEE Conference on Computational Complexity (2003)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-02777-2_13","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A. Atserias","year":"2009","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause learning algorithms with many restarts and bounded-width resolution. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 114\u2013127. Springer, Heidelberg (2009)"},{"key":"4_CR5","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)"},{"key":"4_CR6","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. Journal of Artificial Intelligence Research\u00a022, 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"#cr-split#-4_CR7.1","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow \u2014 resolution made simple. Journal of the ACM\u00a048 (2001);","DOI":"10.1145\/375827.375835"},{"key":"#cr-split#-4_CR7.2","unstructured":"Preliminary Version in Proc. 31st ACM Symposium on Theory of Computing (1999)"},{"issue":"4","key":"4_CR8","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":"4_CR9","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":"4_CR10","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":"4_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Principles and Practice of Constraint Programming - CP97","author":"C.P. Gomes","year":"1997","unstructured":"Gomes, C.P., Selman, B., Crato, N.: Heavy-tailed distributions in combinatorial search. In: Smolka, G. (ed.) CP 1997. LNCS, vol.\u00a01330. Springer, Heidelberg (1997)"},{"key":"4_CR12","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":"4_CR13","unstructured":"Hoffmann, J.: Resolution proofs and DLL-algorithms with clause learning. Diploma Thesis, LMU M\u00fcnchen (2007)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-46632-0_14","volume-title":"Algorithms and Computations","author":"K. Iwama","year":"1999","unstructured":"Iwama, K., Miyazaki, S.: Tree-like resolution is superpolynomially slower than dag-like resolution for the pigeonhole principle. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol.\u00a01741, p. 133. Springer, Heidelberg (1999)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-02777-2_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"J. Johannsen","year":"2009","unstructured":"Johannsen, J.: An exponential lower bound for width-restricted clause learning. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 128\u2013140. Springer, Heidelberg (2009)"},{"key":"#cr-split#-4_CR16.1","doi-asserted-by":"crossref","unstructured":"Kolaitis, P.G., Vardi, M.Y.: On the expressive power of Datalog: Tools and a case study. Journal of Computer and System Sciences\u00a051(1), 110\u2013134 (1990);","DOI":"10.1006\/jcss.1995.1055"},{"key":"#cr-split#-4_CR16.2","unstructured":"Preliminary version in Proc. 9th ACM Symposium on Principles of Database Systems (1990)"},{"key":"4_CR17","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"},{"issue":"3","key":"4_CR18","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF02126799","volume":"8","author":"A. Lubotzky","year":"1988","unstructured":"Lubotzky, A., Phillips, R., Sarnak, P.: Ramanujan graphs. Combinatorica\u00a08(3), 261\u2013277 (1988)","journal-title":"Combinatorica"},{"key":"4_CR19","first-page":"39","volume":"24","author":"G.A. Margulis","year":"1988","unstructured":"Margulis, G.A.: Explicit group-theoretical constructions of combinatorial schemes and their application to the design of expanders and concentrators. Problems of Information Transmission\u00a024, 39\u201346 (1988)","journal-title":"Problems of Information Transmission"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1007\/978-3-642-04244-7_51","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K. Pipatsrisawat","year":"2009","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers with restarts. In: Gent, I.P. (ed.) CP 2009. LNCS, vol.\u00a05732, pp. 654\u2013668. Springer, Heidelberg (2009)"},{"key":"#cr-split#-4_CR21.1","doi-asserted-by":"crossref","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);","DOI":"10.1137\/S0097539703428555"},{"key":"#cr-split#-4_CR21.2","unstructured":"Preliminary version in Proc. 43rd IEEE Symposium on Foundations of Computer Science (2002)"},{"key":"4_CR22","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":"4_CR23","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":"4_CR24","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"4_CR25","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 \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:31:35Z","timestamp":1559241095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}