{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T10:47:46Z","timestamp":1794480466639,"version":"4.9.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319092836","type":"print"},{"value":"9783319092843","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_1","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:43:21Z","timestamp":1404279801000},"page":"1-6","source":"Crossref","is-referenced-by-count":2,"title":["A (Biased) Proof Complexity Survey for SAT Practitioners"],"prefix":"10.1007","author":[{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM Journal on Computing\u00a031(4), 1184\u20131211 (2002), preliminary version appeared in STOC 2000","DOI":"10.1137\/S0097539700366735"},{"key":"1_CR2","unstructured":"Alekhnovich, M., Razborov, A.A.: Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics\u00a0242, 18\u201335 (2003), http:\/\/people.cs.uchicago.edu\/razborov\/files\/misha.pdf , Preliminary version appeared in FOCS 2001"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Atserias, A., Dalmau, V.: A combinatorial characterization of resolution width. Journal of Computer and System Sciences\u00a074(3), 323\u2013334 (2008), preliminary version appeared in CCC 2003","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Atserias, A., Lauria, M., Nordstr\u00f6m, J.: Narrow proofs be maximally long. In: Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC 2014) (to appear, Jun 2014)","DOI":"10.1109\/CCC.2014.36"},{"key":"1_CR5","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203\u2013208 (July 1997)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. In: Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pp. 213\u2013232 (May 2012)","DOI":"10.1145\/2213977.2213999"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Beck, C., Nordstr\u00f6m, J., Tang, B.: Some trade-off results for polynomial calculus. In: Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 813\u2013822 (May 2013)","DOI":"10.1145\/2488608.2488711"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Galesi, N.: Space complexity of random formulae in resolution. Random Structures and Algorithms\u00a023(1), 92\u2013109 (2003), preliminary version appeared in CCC 2001","DOI":"10.1002\/rsa.10089"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Short proofs be spacious: An optimal separation of space and length in resolution. In: Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2008), pp. 709\u2013718 (October 2008)","DOI":"10.1109\/FOCS.2008.42"},{"key":"1_CR10","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Understanding space in proof complexity: Separations and trade-offs via substitutions. In: Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS 2011), pp. 401\u2013416 (January 2011), full-length version available at http:\/\/eccc.hpi-web.de\/report\/2010\/125\/"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow\u2014resolution made simple. Journal of the ACM\u00a048(2), 149\u2013169 (2001), preliminary version appeared in STOC 1999","DOI":"10.1145\/375827.375835"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Biere, A., Berre, D.L., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014) (to appear, July 2014)","DOI":"10.1007\/978-3-319-09284-3_22"},{"key":"1_CR13","unstructured":"Blake, A.: Canonical Expressions in Boolean Algebra. Ph.D. thesis. University of Chicago (1937)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Bonacina, I., Galesi, N.: Pseudo-partitions, transversality and locality: A combinatorial characterization for the space measure in algebraic proof systems. In: Proceedings of the 4th Conference on Innovations in Theoretical Computer Science (ITCS 2013), pp. 455\u2013472 (January 2013)","DOI":"10.1145\/2422436.2422486"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Bonet, M.L., Galesi, N.: Optimality of size-width tradeoffs for resolution. Computational Complexity\u00a010(4), 261\u2013276 (2001), preliminary version appeared in FOCS 1999","DOI":"10.1007\/s000370100000"},{"issue":"4","key":"1_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. Journal of the ACM\u00a035(4), 759\u2013768 (1988)","journal-title":"Journal of the ACM"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC 1996), pp. 174\u2013183 (May 1996)","DOI":"10.1145\/237814.237860"},{"issue":"1","key":"1_CR18","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.: The relative efficiency of propositional proof systems. Journal of Symbolic Logic\u00a044(1), 36\u201350 (1979)","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"Cook, W., Coullard, C.R., Turn, G.: On the complexity of cutting-plane proofs. Discrete Applied Mathematics\u00a018(1), 25\u201338 (1987)","journal-title":"Discrete Applied Mathematics"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Esteban, J.L., Torn, J.: Space bounds for resolution. Information and Computation\u00a0171(1), 84\u201397 (2001), preliminary versions of these results appeared in STACS 1999 and CSL 1999","DOI":"10.1006\/inco.2001.2921"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-39206-1_37","volume-title":"Automata, Languages, and Programming","author":"Y. Filmus","year":"2013","unstructured":"Filmus, Y., Lauria, M., Mik\u0161a, M., Nordstr\u00f6m, J., Vinyals, M.: Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract). In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part I. LNCS, vol.\u00a07965, pp. 437\u2013448. Springer, Heidelberg (2013)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Filmus, Y., Lauria, M., Nordstr\u00f6m, J., Thapen, N., Ron-Zewi, N.: Space complexity in polynomial calculus (extended abstract). In: Proceedings of the 27th Annual IEEE Conference on Computational Complexity (CCC 2012), pp. 334\u2013344 (June 2012)","DOI":"10.1109\/CCC.2012.27"},{"key":"1_CR23","unstructured":"Gs, M., Pitassi, T.: Communication lower bounds via critical block sensitivity. In: Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC 2014) (to appear, May 2014)"},{"issue":"2-3","key":"1_CR24","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. Theoretical Computer Science\u00a039(2-3), 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Huynh, T., Nordstr\u00f6m, J.: On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity (extended abstract). In: Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pp. 233\u2013248 (May 2012)","DOI":"10.1145\/2213977.2214000"},{"issue":"2","key":"1_CR26","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s000370050024","volume":"8","author":"R. Impagliazzo","year":"1999","unstructured":"Impagliazzo, R., Pudl\u00e1k, P., Sgall, J.: Lower bounds for the polynomial calculus and the Gr\u00f6bner basis algorithm. Computational Complexity\u00a08(2), 127\u2013144 (1999)","journal-title":"Computational Complexity"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-33558-7_25","volume-title":"Principles and Practice of Constraint Programming","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Matsliah, A., Nordstr\u00f6m, J., \u017divn\u00fd, S.: Relating proof complexity measures and practical hardness of SAT. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 316\u2013331. Springer, Heidelberg (2012)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD 1996), pp. 220\u2013227 (November 1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Mik\u0161a, M., Nordstr\u00f6m, J.: Long proofs of (seemingly) simple formulas. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014) (to appear, July 2014)","DOI":"10.1007\/978-3-319-09284-3_10"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science\u00a09, 15:1\u201315:63 (2013)","DOI":"10.2168\/LMCS-9(3:15)2013"},{"issue":"3","key":"1_CR32","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic\u00a062(3), 981\u2013998 (1997)","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"1_CR33","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. Journal of the ACM\u00a034(1), 209\u2013219 (1987)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T12:52:10Z","timestamp":1746276730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_1","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}