{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:10:56Z","timestamp":1743102656294,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540428633"},{"type":"electronic","value":"9783540455783"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45578-7_9","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T06:34:25Z","timestamp":1180334065000},"page":"121-136","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Random 3-SAT and BDDs: The Plot Thickens Further"],"prefix":"10.1007","author":[{"given":"Alfonso San Miguel","family":"Aguirre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MosheY.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,19]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"D. Achlioptas. Setting two variables at a time yields a new lower bound for random 3-SAT. In Proc. 32th ACM Symp. on Theory of Computing, pages 28\u201337, 2000.","DOI":"10.1145\/335305.335309"},{"issue":"3","key":"9_CR2","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/0022-0000(90)90025-G","volume":"41","author":"J. Balcazar","year":"1990","unstructured":"J. Balcazar. Self-reducibility. Journal of Computer and System Sciences, 41(3):367\u2013388, 1990.","journal-title":"Journal of Computer and System Sciences"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"P. Beame, R. M. Karp, T. Pitassi, and M. E. Saks. On the complexity of unsatisfiability proofs for random k-CNF formulas. In Proc. 30th ACM Symp. on Theory of Computing, pages 561\u2013571, 1998.","DOI":"10.1145\/276698.276870"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. 36th Conf. on Design Automation, pages 317\u2013320, 1999.","DOI":"10.1145\/309847.309942"},{"key":"9_CR5","unstructured":"M. Block, C. Gr\u00f6pl, H. Preu\\, H. L. Pro\u00f6mel, and A. Srivastav. Efficient ordering of state variables and transition relation partitions in symbolic model checking. Technical report, Institute of Informatics, Humboldt University of Berlin, 1997."},{"key":"9_CR6","unstructured":"F. Bouquet. Gestion de la dynamicit\u00e9 et \u00e9num\u00e9ration d\u2019implicants premiers: une approche fond\u00e9e sur les Diagrammes de D\u00e9cision Binaire. PhD thesis, Universit\u00e9 de Provence, France, 1999."},{"issue":"8","key":"9_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers, 35(8):677\u2013691, 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"9_CR8","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In Proc. IFIP TC10\/WG 10.5 Int\u2019l Conf. on Very Large Scale Integration, Edinburgh, Scotland (VLSI\u201991), pages 49\u201358, 1991."},{"issue":"2","key":"9_CR9","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"P. Chatalic and L. Simon. The old Davis-Putnam procedure meets ZBDDs. In D. McAllester, editor, 17th Int\u2019l Conf. on Automated Deduction (CADE\u201917), volume 1831 of Lecture Notes in Artificial Intelligence, pages 449\u2013454, 2000.","DOI":"10.1007\/10721959_35"},{"key":"9_CR11","unstructured":"P. Cheeseman, B. Kanefsky, and W. M. Taylor. Where the really hard problems are. In Proc. 12th Int\u2019l Joint Conf. on Artificial Intelligence (IJCAI\u2019 91), pages 331\u2013337, 1991."},{"issue":"4","key":"9_CR12","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"V. Chv\u00e1tal and E. Szemer\u00e9di. Many hard examples for resolution. J. of the ACM, 35(4):759\u2013768, 1988.","journal-title":"J. of the ACM"},{"key":"9_CR13","series-title":"Lect Notes Comput Sci","first-page":"143","volume-title":"Random 3-SAT: The plot thickens","year":"2000","unstructured":"C. Coarfa, D. D. Demopolous, A. San Miguel Aguirre, D. Subramanian, and M. Y. Vardi. Random 3-SAT: The plot thickens. In R. Dechter, editor, Proc. Principles and Practice of Constraint Programming (CP\u20192000), Lecture Notes in Computer Science 1894, pages 143\u2013159, 2000."},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"1654","DOI":"10.1103\/PhysRevLett.86.1654","volume":"86","author":"S. Cocco","year":"2001","unstructured":"S. Cocco and R. Monasson. Trajectories in phase diagrams, growth processes and computational complexity: how search algorithms solve the 3-Satisfiability problem. Phys. Rev. Lett., 86:1654\u20131657, 2001.","journal-title":"Phys. Rev. Lett."},{"issue":"1\u20132","key":"9_CR15","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0004-3702(95)00046-1","volume":"81","author":"J. M. Crawford","year":"1996","unstructured":"J. M. Crawford and L. D. Auton. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, 81(1\u20132):31\u201357, 1996.","journal-title":"Artificial Intelligence"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Comm. of the ACM, 5:394\u2013397, 1962.","journal-title":"Comm. of the ACM"},{"key":"9_CR17","unstructured":"O. Dubois, Y. Boufkhad, and J. Mandler. Typical random 3-SAT formulae and the satisfiability threshold. In Proc. 11th Annual ACM-SIAM Symp. on Discrete Algorithms, pages 126\u2013127, 2000."},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"1017","DOI":"10.1090\/S0894-0347-99-00305-7","volume":"12","author":"E. Friedgut","year":"1999","unstructured":"E. Friedgut. Necessary and sufficient conditions for sharp threshold of graph properties and the k-SAT problem. J. Amer. Math. Soc., 12:1017\u20131054, 1999.","journal-title":"J. Amer. Math. Soc."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"D. Geist and H. Beer. Efficient model checking by automated ordering of transition relation partitions. In Proc. 6th Int\u2019l Conf. on Computer Aided Verification (CAV\u2019 94), pages 299\u2013310, 1994.","DOI":"10.1007\/3-540-58179-0_63"},{"issue":"1\u20132","key":"9_CR20","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0004-3702(94)90109-0","volume":"70","author":"I. P. Gent","year":"1994","unstructured":"I. P. Gent and T. Walsh. Easy problems are sometimes hard. Artificial Intelligence, 70(1\u20132):335\u2013345, 1994.","journal-title":"Artificial Intelligence"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00121264","volume":"8","author":"J. F. Groote","year":"1996","unstructured":"J. F. Groote. Hiding propositional constants in BDDs. Formal Methods in System Design, 8:91\u201396, 1996.","journal-title":"Formal Methods in System Design"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"J. F. Groote and H. Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. Technical report, Department of Computer Science, Utrecht University, 2000. Technical Report UU-CS-2000-14.","DOI":"10.1007\/3-540-45575-2_5"},{"issue":"1\u20132","key":"9_CR23","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/0004-3702(94)90088-4","volume":"69","author":"T. Hogg","year":"1994","unstructured":"T. Hogg and C. P. Williams. The hardest constraint problems: A double phase transition. Artificial Intelligence, 69(1\u20132):359\u2013377, 1994.","journal-title":"Artificial Intelligence"},{"key":"9_CR24","unstructured":"R. Hojati, S. C. Krishnan, and R. K. Brayton. Early quantification and partitioned transition relations. In Proc. 1996 Int\u2019l Conf. on Computer Design, pages 12\u201319, 1996."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"S. Jha, Y. Lu, M. Minea, and E. M. Clarke. Equivalence checking using abstract BDDs. In Proc. Int\u2019l Conf. on Computer Design (ICCD\u201997), pages 332\u2013337, 1997.","DOI":"10.1109\/ICCD.1997.628891"},{"key":"9_CR26","unstructured":"T. Larrabee and Y. Tsuji. Evidence for a satisfiability threshold for random 3CNF formulas. In Working Notes of AAAI 1993 Spring Symposium: AI and NP-Hard Problems, pages 112\u2013118, 1993."},{"issue":"5","key":"9_CR27","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. M. Silva","year":"1999","unstructured":"J. P. Marques Silva and K. A. Sakallah. GRASP-A search algorithm for propositional satis-fiability. IEEE Trans. on Computers, 48(5):506\u2013521, 1999.","journal-title":"IEEE Trans. on Computers"},{"issue":"1\u20132","key":"9_CR28","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/0004-3702(95)00049-6","volume":"81","author":"D. G. Mitchell","year":"1996","unstructured":"D. G. Mitchell and H. J. Levesque. Some pitfalls for experimenters with random SAT. Artificial Intelligence, 81(1\u20132):111\u2013125, 1996.","journal-title":"Artificial Intelligence"},{"key":"9_CR29","unstructured":"R. K. Ranjan, A. A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient formal design verification: Data structure + algorithms. Technical report, University of California at Berkeley, 1994. Tech. Rep. UCB\/ERL M94\/100."},{"issue":"1\u20132","key":"9_CR30","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(95)00056-9","volume":"81","author":"B. Selman","year":"1996","unstructured":"B. Selman and S. Kirkpatrick. Critical behavior in the computational cost of satisfiability testing. Artificial Intelligence, 81(1\u20132):273\u2013295, 1996.","journal-title":"Artificial Intelligence"},{"issue":"1\u20132","key":"9_CR31","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"B. Selman, D. G. Mitchell, and H. J. Levesque. Generating hard satisfiability problems. Artificial Intelligence, 81(1\u20132):17\u201329, 1996.","journal-title":"Artificial Intelligence"},{"key":"9_CR32","unstructured":"F. Somenzi. CUDD: CU Decision Diagram package. release 2.3.0., 1998. Dept. of Electrical and Computer Engineering. University of Colorado at Boulder."},{"issue":"3","key":"9_CR33","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1137\/0213035","volume":"13","author":"R. E. Tarjan","year":"1984","unstructured":"R. E. Tarjan and M. Yannakakis. Simple linear-time algorithms to tests chordiality of graphs, tests acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM J. on Computing, 13(3):566\u2013579, 1984.","journal-title":"SIAM J. on Computing"},{"key":"9_CR34","series-title":"Lect Notes Comput Sci","first-page":"428","volume-title":"A system for verification and synthesis","year":"1996","unstructured":"The VIS Group. VIS: A system for verification and synthesis. In Proc. 8th Int\u2019l Conf. on Computer Aided Verification (CAV\u2019 96), pages 428\u2013432, 1996. LNCS 1102. Ed. by R. Alur and T. Henziger."},{"key":"9_CR35","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":"T. E. Uribe and M. E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. In First Int\u2019l Conf. on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 34\u201349, Munich, September 1994. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2014 CP 2001"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45578-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:36:32Z","timestamp":1737052592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45578-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540428633","9783540455783"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-45578-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"19 November 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}