{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:45:09Z","timestamp":1725493509052},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001959"},{"type":"electronic","value":"9783540361848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36184-7_7","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T06:08:01Z","timestamp":1193551681000},"page":"57-65","source":"Crossref","is-referenced-by-count":0,"title":["On Determining the Minimum Length, Tree-Like Resolution Refutation of 2SAT, and Extended 2SAT Formulas"],"prefix":"10.1007","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Achlioptas, Beame, and Molloy. A sharp threshold in proof complexity. In STOC: ACM Symposium on Theory of Computing (STOC), 2001.","DOI":"10.1145\/380752.380820"},{"key":"7_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Mathematical Foundations of Computer Science (MFCS)","author":"M. Alekhnovich","year":"1998","unstructured":"M. Alekhnovich, S. Buss, S. Moran, and T. Pitassi. Minimum propositional proof length is np-hard to linearly approximate. In Mathematical Foundations of Computer Science (MFCS). Springer-Verlag, 1998. Lecture Notes in Computer Science."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bengt Aspvall, Michael F. Plass, and Robert Tarjan. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, (3), 1979.","DOI":"10.1016\/0020-0190(79)90002-4"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Alexander Bockmayr and Friedrich Eisnbrand. Combining logic and optimization in cutting plane theory. In Proceedings of Frontiers of Combining Systems (FROCOS) 2000, pages 1\u201317. Springer-Verlag. Lecure Notes in Artificial Intelligence.","DOI":"10.1007\/10720084_1"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Azer Bestavros and Victor Fay-Wolfe, editors. Real-Time Database and Information Systems, Research Advances. Kluwer Academic Publishers, 1997.","DOI":"10.1007\/978-1-4615-6069-2"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine Buning","year":"1995","unstructured":"H. Kleine Buning, M. Karpinski, and A. Flogel. Resolution for quantified boolean formulas. Information and Computation, 117:12\u201318, 1995.","journal-title":"Information and Computation"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In 37th Annual Symposium on Foundations of Computer Science, pages 274\u2013282, Burlington, Vermont, 14-16 October 1996. IEEE.","DOI":"10.1109\/SFCS.1996.548486"},{"key":"7_CR8","first-page":"66","volume":"65","author":"P. Beame","year":"1998","unstructured":"Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, future. Bulletin of the EATCS, 65:66\u201389, June 1998.","journal-title":"Bulletin of the EATCS"},{"key":"7_CR9","unstructured":"Samuel Buss. personal communication."},{"issue":"4","key":"7_CR10","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1016\/S0022-0000(73)80029-7","volume":"7","author":"S. A. Cook","year":"1973","unstructured":"Stephen A. Cook and Robert A. Reckhow. Time bounded random access machines. Journal of Computer and System Sciences, 7(4):354\u2013375, August 1973.","journal-title":"Journal of Computer and System Sciences"},{"issue":"2-3","key":"7_CR11","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297\u2013308, August 1985.","journal-title":"Theoretical Computer Science"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"K. Iwama and E. Miyano. Intractability of read-once resolution. In Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC\u2019 95), pages 29\u201336, Los Alamitos, CA, USA, June 1995. IEEE Computer Society Press.","DOI":"10.1109\/SCT.1995.514725"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"K. Iwama. Complexity of finding short resolution proofs. Lecture Notes in Computer Science, 1295:309\u2013319, 1997.","DOI":"10.1007\/BFb0029974"},{"key":"7_CR14","volume-title":"Computational Complexity","author":"C. H. Papadimitriou","year":"1994","unstructured":"Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, New York, 1994."},{"issue":"3","key":"7_CR15","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pavel Pudl\u00e1k. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981\u2013998, September 1997.","journal-title":"The Journal of Symbolic Logic"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Alexander A. Razborov. Lower bounds for propositional proofs and independence results in bounded arithmetic. In Friedhelm Meyer auf der Heide and Burkhard Monien, editors, Automata, Languages and Programming, 23rd International Colloquium, volume 1099 of Lecture Notes in Computer Science, pages 48\u201362, Paderborn, Germany, 8-12 July 1996. Springer Verlag.","DOI":"10.1007\/3-540-61440-0_116"},{"issue":"4","key":"7_CR17","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"Alasdair Urquhart. The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1(4):425\u2013467, December 1995.","journal-title":"The Bulletin of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36184-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T02:27:43Z","timestamp":1556936863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36184-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001959","9783540361848"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-36184-7_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}