{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:26Z","timestamp":1761597026924},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430759"},{"type":"electronic","value":"9783540455752"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45575-2_5","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T21:30:22Z","timestamp":1180560622000},"page":"33-38","source":"Crossref","is-referenced-by-count":10,"title":["Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially"],"prefix":"10.1007","author":[{"given":"Jan Friso","family":"Groote","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Zantema","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,12,18]]},"reference":[{"key":"5_CR1","unstructured":"Ben-Sasson, E., and Wigderson, A. Short proofs are narrow-resolution made simple. In Proceedings of the 31st Annual ACM Symposium on Theory of Computing (1999), pp. 517\u2013526."},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"8","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35, 8 (1986), 677\u2013691.","journal-title":"IEEE Transactions on Computers C-35"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Groote, J. F., and Zantema, H. Resolution and binary decision diagrams cannot simulate each other polynomially. Journal of Discrete Applied Mathematics (2001). To appear.","DOI":"10.1007\/3-540-45575-2_5"},{"key":"5_CR4","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 39 (1985), 297\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Meinel, C., and Theobald, T. Algorithms and Data Structures in VLSI Design: OBDD\u2014 Foundations and Applications. Springer, 1998.","DOI":"10.1007\/978-3-642-58940-9"},{"key":"5_CR6","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic","author":"G. Tseitin","year":"1968","unstructured":"Tseitin, G. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, part 2 (1968), pp. 115\u2013125. Reprinted in J. Siekmann and G. Wrightson (editors),Automation of reasoning vol. 2, pp. 466\u2013483.,Springer-Verlag Berlin, 1983."},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/BFb0016843","volume-title":"Ordered binary decision diagrams and the Davis-Putnam procedure","author":"T. E. Uribe","year":"1994","unstructured":"Uribe, T. E., and Stickel, M. E. Ordered binary decision diagrams and the Davis-Putnam procedure. In First conference on Constraints in Computational Logic(1994), J.-P. Jouannaud, Ed., vol. 845of Lecture Notes in Computer Science, Springer, pp. 34\u201349."},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"1","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A. Hard examples for resolution. Journal of the ACM 34, 1 (1987), 209\u2013219.","journal-title":"Journal of the ACM 34"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"4","author":"A. Urquhart","year":"1995","unstructured":"Urquhart, A. The complexity of propositional proofs. The Bulletin of Symbolic Logic 1, 4 (1995), 425\u2013467.","journal-title":"The Bulletin of Symbolic Logic 1"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Zantema, H., and van de Pol, J. C. A rewriting approach to binary decision diagrams. Journal of Logic and Algebraic Programming (2001). To appear.","DOI":"10.1016\/S1567-8326(01)00013-3"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45575-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T20:09:42Z","timestamp":1550347782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45575-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430759","9783540455752"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-45575-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}