{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:32:46Z","timestamp":1742391166021},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540410539"},{"type":"electronic","value":"9783540453499"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45349-0_12","type":"book-chapter","created":{"date-parts":[[2007,6,7]],"date-time":"2007-06-07T00:54:55Z","timestamp":1181177695000},"page":"143-159","source":"Crossref","is-referenced-by-count":14,"title":["Random 3-SAT: The Plot Thickens"],"prefix":"10.1007","author":[{"given":"Cristian","family":"Coarfa","sequence":"first","affiliation":[]},{"given":"Demetrios D.","family":"Demopoulos","sequence":"additional","affiliation":[]},{"given":"Alfonso San Miguel","family":"Aguirre","sequence":"additional","affiliation":[]},{"given":"Devika","family":"Subramanian","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"12_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"},{"key":"12_CR2","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":"12_CR3","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"},{"issue":"3","key":"12_CR4","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1287\/ijoc.4.3.267","volume":"4","author":"R. E. Bixby","year":"1992","unstructured":"R. E. Bixby. Implementing the Simplex method: The initial basis. ORSA J. on Computing, 4(3):267\u2013284, 1992.","journal-title":"ORSA J. on Computing"},{"key":"12_CR5","series-title":"PhD thesis","volume-title":"Gestion de la dynamicit\u00e9 et \u00e9num\u00e9ration d\u2019implicants premiers: une approche fond\u00e9e sur les Diagrammes de D\u00e9cision Binaire","author":"F. Bouquet","year":"1999","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."},{"key":"12_CR6","unstructured":"A. Z. Broder, A. M. Frieze, and E. Upfal. On the satisfiability and maximum satisfiability of random 3-CNF formulas. In Proc. 4th Annual ACM-SIAM Symp. on Discrete Algorithms, pages 322\u2013330, 1993."},{"issue":"8","key":"12_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":"12_CR8","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0020-0255(90)90030-E","volume":"51","author":"M. Chao","year":"1990","unstructured":"M. Chao and J. V. Franco. Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem. Information Sciences, 51:289\u2013314, 1990.","journal-title":"Information Sciences"},{"key":"12_CR9","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":"12_CR10","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":"12_CR11","unstructured":"J. M. Crawford and L. D. Auton. Experimental results on the crossover point in satisfiability problems. AAAI, pages 21\u201327, 1993."},{"issue":"1\u20132","key":"12_CR12","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":"12_CR13","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Comm. of the ACM, 5:394\u2013397, 1962.","journal-title":"Comm. of the ACM"},{"key":"12_CR14","unstructured":"O. Dubois, Y. Boufkhad, and J. Mandler. Typical random 3-SAT formulae and the satisfiability theshold. In Proc. 11th Annual ACM-SIAM Symp. on Discrete Algorithms, pages 126\u2013127, 2000."},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"1917","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:1917\u20131054, 1999.","journal-title":"J. Amer. Math. Soc."},{"issue":"2","key":"12_CR16","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1006\/jagm.1996.0016","volume":"20","author":"A. Frieze","year":"1996","unstructured":"A. Frieze and S. Suen. Analysis of two simple heuristics for random instances of k-SAT. J. of Algorithms, 20(2):312\u2013355, 1996.","journal-title":"J. of Algorithms"},{"key":"12_CR17","unstructured":"I. P. Gent and T. Walsh. The SAT phase transition. In Proc. European Conf. on Artificial Intelligence, pages 105\u2013109, 1994."},{"key":"12_CR18","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":"12_CR19","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":"12_CR20","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":"12_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","volume":"7","author":"J. N. Hooker","year":"1988","unstructured":"J. N. Hooker. Resolution vs. cutting plane solution of inference problems: Some computational experience. Operations Research Letters, 7:1\u20137, 1988.","journal-title":"Operations Research Letters"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"1297","DOI":"10.1126\/science.264.5163.1297","volume":"264","author":"S. Kirkpatrick","year":"1994","unstructured":"S. Kirkpatrick and B. Selman. Critical behavior in the satisfiability of random formulas. Science, 264:1297\u20131301, 1994.","journal-title":"Science"},{"key":"12_CR23","series-title":"Technical report USCS-CRL-92042","volume-title":"Technical report","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee and Y. Tsuji. Evidence for a satisfiability threshold for random 3CNF formulas. Technical report, University of California, Santa Cruz, 1992. Technical report USCS-CRL-92042."},{"issue":"5","key":"12_CR24","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques Silva","year":"1999","unstructured":"J. P. Marques Silva and K. A. Sakallah. GRASP-A search algorithm for propositional satisfiability. IEEE Trans. on Computers, 48(5):506\u2013521, 1999.","journal-title":"IEEE Trans. on Computers"},{"issue":"1\u20132","key":"12_CR25","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":"12_CR26","series-title":"SRC Technical Note","volume-title":"Technical report","author":"M. Mitzenmacher","year":"1997","unstructured":"M. Mitzenmacher. Tight thresholds for the pure literal rule. Technical report, Digital System Research Center, Palo Alto, California, 1997. SRC Technical Note 1997-011."},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"G. J. Nam, K. A. Sakallah, and R. A. Rutenbar. Satisfiability-based layout revisited: Detailed routing of complex fpgas via search-based boolean sat. In Proc. ACM Int\u2019l Symp. on Field-Programmable Gate Arrays (FPGA\u201999), pages 167\u2013175, 1999.","DOI":"10.1145\/296399.296450"},{"issue":"1\u20132","key":"12_CR28","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":"12_CR29","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":"12_CR30","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0004-3702(95)00052-6","volume":"81\u20132","author":"B. M. Smith","year":"1996","unstructured":"B. M. Smith and M. E. Dyer. Locating the phase transition in binary constraint satisfaction problems. Artificial Intelligence Journal, 8(1\u20132):155\u2013181, 1996.","journal-title":"Artificial Intelligence Journal"},{"key":"12_CR31","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":"4","key":"12_CR32","doi-asserted-by":"publisher","first-page":"3983","DOI":"10.1103\/PhysRevE.59.3983","volume":"59","author":"P. Svenson","year":"1999","unstructured":"P. Svenson and M. G. Nordahl. Relaxation in graph coloring and satisfiability problems. Phys. Rev. E, 59(4):3983\u20133999, 1999.","journal-title":"Phys. Rev. E"},{"key":"12_CR33","series-title":"Lect Notes Comput Sci","first-page":"428","volume-title":"Proc. 8th Int\u2019l Conf. on Computer Aided Verification (CAV\u2019 96)","author":"The VIS Group","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":"12_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/BFb0016843","volume-title":"First Int\u2019l Conf. on Constraints in Computational Logics","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 \u2013 CP 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45349-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:40:20Z","timestamp":1556480420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45349-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410539","9783540453499"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-45349-0_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}