{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T17:53:59Z","timestamp":1777398839822,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":64,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,5,19]],"date-time":"2012-05-19T00:00:00Z","timestamp":1337385600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2012,5,19]]},"DOI":"10.1145\/2213977.2214000","type":"proceedings-article","created":{"date-parts":[[2012,5,21]],"date-time":"2012-05-21T15:20:35Z","timestamp":1337613635000},"page":"233-248","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["On the virtue of succinct proofs"],"prefix":"10.1145","author":[{"given":"Trinh","family":"Huynh","sequence":"first","affiliation":[{"name":"Swiss Federal Institute of Technology, Zurich, Switzerland"}]},{"given":"Jakob","family":"Nordstrom","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2012,5,19]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_3_2_2_2_1","first-page":"18","article-title":"Lower bounds for polynomial calculus: Non-binomial case","volume":"242","author":"Alekhnovich M.","year":"2003","unstructured":"M. Alekhnovich and A. A. Razborov . Lower bounds for polynomial calculus: Non-binomial case . Proceedings of the Steklov Institute of Mathematics , 242 : 18 -- 35 , 2003 . Available at http:\/\/people.cs.uchicago.edu\/ razborov\/files\/misha.pdf. Preliminary version appeared in FOCS '01. M. Alekhnovich and A. A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics, 242:18--35, 2003. Available at http:\/\/people.cs.uchicago.edu\/ razborov\/files\/misha.pdf. Preliminary version appeared in FOCS '01.","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2016945.2016955"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2003.11.006"},{"key":"e_1_3_2_2_6_1","first-page":"203","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97)","author":"Bayardo R. J.","year":"1997","unstructured":"R. J. Bayardo Jr . and R. Schrag . Using CSP look-back techniques to solve real-world SAT instances . In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97) , pages 203 - 208 , July 1997 . R. J. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97), pages 203-208, July 1997."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502097"},{"key":"e_1_3_2_2_8_1","series-title":"IAS\/Park City Mathematics Series","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1090\/pcms\/010\/07","volume-title":"Computational Complexity Theory","author":"Beame P.","year":"2004","unstructured":"P. Beame . Proof complexity . In S. Rudich and A. Wigderson, editors, Computational Complexity Theory , volume 10 of IAS\/Park City Mathematics Series , pages 199 - 246 . American Mathematical Society , 2004 . P. Beame. Proof complexity. In S. Rudich and A. Wigderson, editors, Computational Complexity Theory, volume 10 of IAS\/Park City Mathematics Series, pages 199-246. American Mathematical Society, 2004."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2213999"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806689.1806703"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/060654645"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_4"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.42"},{"key":"e_1_3_2_2_17_1","first-page":"401","volume-title":"Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11)","author":"Ben-Sasson E.","year":"2011","unstructured":"E. Ben-Sasson and J. Nordstr\u00f6m . Understanding space in proof complexity: Separations and trade-offs via substitutions . In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11) , pages 401 -- 416 , Jan. 2011 . Full-length version available at http:\/\/eccc.hpi-web.de\/report\/ 2010\/125\/. E. Ben-Sasson and J. Nordstr\u00f6m. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11), pages 401--416, Jan. 2011. Full-length version available at http:\/\/eccc.hpi-web.de\/report\/2010\/125\/."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_3_2_2_19_1","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","author":"Biere A.","year":"2009","unstructured":"A. Biere , M. J. H. Heule , H. van Maaren , and T. Walsh , editors . Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications . IOS Press , Feb. 2009 . A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, Feb. 2009."},{"key":"e_1_3_2_2_20_1","volume-title":"Canonical Expressions in Boolean Algebra. D thesis","author":"Blake A.","year":"1937","unstructured":"A. Blake . Canonical Expressions in Boolean Algebra. D thesis , University of Chicago , 1937 . A. Blake. Canonical Expressions in Boolean Algebra. D thesis, University of Chicago, 1937."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225275"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370100000"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.02.017"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2008.11.043"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/874063.875561"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(76)80048-7"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595391.1595392"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.004"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2012.27"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316069"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_3_2_2_42_1","volume-title":"Relating proof complexity measures and practical hardness of SAT. Submitted","author":"J\u00e4rvisalo M.","year":"2012","unstructured":"M. J\u00e4rvisalo , A. Matsliah , J. Nordstr\u00f6m , and S. Zivn\u00fd . Relating proof complexity measures and practical hardness of SAT. Submitted , 2012 . M. J\u00e4rvisalo, A. Matsliah, J. Nordstr\u00f6m, and S. Zivn\u00fd. Relating proof complexity measures and practical hardness of SAT. Submitted, 2012."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/264772"},{"key":"e_1_3_2_2_45_1","volume-title":"14th RCRA workshop Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA '07)","author":"Le Berre D.","year":"2007","unstructured":"D. Le Berre and A. Parrain . On extending SAT solvers for PB problems . In 14th RCRA workshop Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA '07) , July 2007 . Available at http:\/\/pst.istc.cnr.it\/RCRA07\/articoli\/P14-leberre-parrain-RCRA07.pdf. D. Le Berre and A. Parrain. On extending SAT solvers for PB problems. In 14th RCRA workshop Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA '07), July 2007. Available at http:\/\/pst.istc.cnr.it\/RCRA07\/articoli\/P14-leberre-parrain-RCRA07.pdf."},{"key":"e_1_3_2_2_46_1","volume-title":"Guangzhou Symposium on Satisfiability and its applications","author":"Berre D. Le","year":"2004","unstructured":"D. Le Berre , A. Parrain , and O. Roussel . The long way from conflict driven clause learning to conflict driven constraint learning . In Guangzhou Symposium on Satisfiability and its applications , Sept. 2004 . Available at http:\/\/www.cril.univ-artois.fr\/spip\/publications\/kanton04.pdf. D. Le Berre, A. Parrain, and O. Roussel. The long way from conflict driven clause learning to conflict driven constraint learning. In Guangzhou Symposium on Satisfiability and its applications, Sept. 2004. Available at http:\/\/www.cril.univ-artois.fr\/spip\/publications\/kanton04.pdf."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0895480192233867"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/244522.244560"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1137\/0220062"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1137\/060668250"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.06.006"},{"key":"e_1_3_2_2_52_1","volume-title":"A survey of some pebbling classics with supplemental results. Manuscript in preparation. To appear in Foundations and Trends in Theoretical Computer Science. Current draft version","author":"Nordstr\u00f6m J.","year":"2012","unstructured":"J. Nordstr\u00f6m . New wine into old wineskins : A survey of some pebbling classics with supplemental results. Manuscript in preparation. To appear in Foundations and Trends in Theoretical Computer Science. Current draft version available at http:\/\/www.csc.kth.se\/ jakobn\/research\/, 2012 . J. Nordstr\u00f6m. New wine into old wineskins: A survey of some pebbling classics with supplemental results. Manuscript in preparation. To appear in Foundations and Trends in Theoretical Computer Science. Current draft version available at http:\/\/www.csc.kth.se\/ jakobn\/research\/, 2012."},{"key":"e_1_3_2_2_53_1","volume-title":"Logical Methods in Computer Science","author":"Nordstr\u00f6m J.","year":"2012","unstructured":"J. Nordstr\u00f6m . Pebble games , proof complexity and time-space trade-offs . Logical Methods in Computer Science , 2012 . To appear. Available at http:\/\/www.csc.kth.se\/ jakobn\/research\/. J. Nordstr\u00f6m. Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science, 2012. To appear. Available at http:\/\/www.csc.kth.se\/ jakobn\/research\/."},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1374376.1374478"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"e_1_3_2_2_56_1","volume-title":"IBM Watson Research Center, 1980. Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan.","author":"Pippenger N.","unstructured":"N. Pippenger . Pebbling. Technical Report RC8258 , IBM Watson Research Center, 1980. Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan. N. Pippenger. Pebbling. Technical Report RC8258, IBM Watson Research Center, 1980. Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/795663.796321"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_2_61_1","unstructured":"The international SAT Competitions. http:\/\/www.satcompetition.org.  The international SAT Competitions. http:\/\/www.satcompetition.org."},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703428555"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"}],"event":{"name":"STOC'12: Symposium on Theory of Computing","location":"New York New York USA","acronym":"STOC'12","sponsor":["SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the forty-fourth annual ACM symposium on Theory of computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2213977.2214000","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2213977.2214000","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:20:54Z","timestamp":1750238454000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2213977.2214000"}},"subtitle":["amplifying communication complexity hardness to time-space trade-offs in proof complexity"],"short-title":[],"issued":{"date-parts":[[2012,5,19]]},"references-count":64,"alternative-id":["10.1145\/2213977.2214000","10.1145\/2213977"],"URL":"https:\/\/doi.org\/10.1145\/2213977.2214000","relation":{},"subject":[],"published":{"date-parts":[[2012,5,19]]},"assertion":[{"value":"2012-05-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}