{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:59:08Z","timestamp":1725728348574},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385353"},{"type":"electronic","value":"9783642385360"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38536-0_11","type":"book-chapter","created":{"date-parts":[[2013,6,3]],"date-time":"2013-06-03T01:03:04Z","timestamp":1370221384000},"page":"127-138","source":"Crossref","is-referenced-by-count":3,"title":["Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Luke","family":"Friedman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yixin","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Achlioptas, D.: Random satisfiability. In: Handbook of Satisfiability, pp. 245\u2013270 (2009)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M.: Lower bounds for k-DNF resolution on random 3-CNFs. In: Proceedings of the 37th Annual ACM Symposium on Theory of Computing, pp. 251\u2013256 (2005)","DOI":"10.1145\/1060590.1060628"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-30201-8_9","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"A. Atserias","year":"2004","unstructured":"Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint propagation as a proof system. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 77\u201391. Springer, Heidelberg (2004)"},{"issue":"9","key":"11_CR4","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers\u00a045(9), 993\u20131002 (1996)","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computing\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computing"},{"issue":"4","key":"11_CR6","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Sz\u00e9meredi, E.: Many hard examples for resolution. Journal of the ACM\u00a035(4), 759\u2013768 (1988)","journal-title":"Journal of the ACM"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. Cook","year":"1979","unstructured":"Cook, S., Reckhow, R.: The relative efficiency of propositional proof systems. Journal of Symbolic Logic\u00a044, 36\u201350 (1979)","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR8","unstructured":"Dubois, O., Boufkhad, Y., Mandler, J.: Typical random 3-sat formulae and the satisfiability threshold. Tech. Rep (10)003, ECCC (2003)"},{"key":"11_CR9","unstructured":"Dubois, O., Mandler, J.: The 3-XORSAT threshold. In: Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science, pp. 769\u2013778 (2002)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Friedman, L., Xu, Y.: Exponential lower bounds for refuting random formulas using ordered binary decision diagrams. Tech. Rep. TR13-018, Electronic Colloquium on Computational Complexity (2013)","DOI":"10.1007\/978-3-642-38536-0_11"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0166-218X(02)00403-1","volume":"130","author":"J.F. Groote","year":"2003","unstructured":"Groote, J.F., Zantema, H.: Resolution and binary decision diagrams cannot simulate each other polynomially. Discrete Applied Mathematics\u00a0130, 157\u2013171 (2003)","journal-title":"Discrete Applied Mathematics"},{"key":"11_CR12","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1112\/jlms\/s1-10.37.26","volume":"10","author":"P. Hall","year":"1935","unstructured":"Hall, P.: On representatives of subsets. J. London Math. Soc.\u00a010, 26\u201330 (1935)","journal-title":"J. London Math. Soc."},{"key":"11_CR13","unstructured":"Huang, J., Darwiche, A.: Toward good elimination ordering for symbolic SAT solving. In: Proceedings of the Sixteenth IEEE Conference on Tools with Artificial Intelligence, pp. 566\u2013573 (2004)"},{"key":"11_CR14","unstructured":"Kraj\u00ed\u010dek, J.: An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. Tech. Rep. (07)007, Electronic Colloquium on Computational Complexity (2007)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11527695_19","volume-title":"Theory and Applications of Satisfiability Testing","author":"G. Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 235\u2013250. Springer, Heidelberg (2005)"},{"key":"11_CR16","unstructured":"Razborov, A.A.: Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution (2003) (manuscript)"},{"key":"11_CR17","first-page":"40","volume":"54","author":"N. Segerlind","year":"2007","unstructured":"Segerlind, N.: The complexity of propositional proofs. Bulletin of Symbolic Logic\u00a054, 40\u201344 (2007)","journal-title":"Bulletin of Symbolic Logic"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1142\/S0129626493000022","volume":"3","author":"D. Seiling","year":"1993","unstructured":"Seiling, D., Wegener, I.: NC-algorithms for operations on binary decision diagrams. Parallel Processing Letters\u00a03(1), 3\u201312 (1993)","journal-title":"Parallel Processing Letters"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Tveretina, O., Sinz, C., Zantema, H.: An exponential lower bound on OBDD refutations for pigeonhole formulas. In: Athens Colloquium on Algorithms and Complexity. Electronic Proceedings in Theoretical Computer Science (2009)","DOI":"10.4204\/EPTCS.4.2"},{"key":"11_CR20","doi-asserted-by":"crossref","first-page":"35","DOI":"10.3233\/SAT190074","volume":"7","author":"O. Tveretina","year":"2010","unstructured":"Tveretina, O., Sinz, C., Zantema, H.: Ordered binary decision diagrams, pigeonhole formulas and beyond. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 35\u201338 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38536-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,27]],"date-time":"2020-07-27T15:09:13Z","timestamp":1595862553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38536-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385353","9783642385360"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38536-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}