{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,13]],"date-time":"2025-07-13T04:10:07Z","timestamp":1752379807121,"version":"3.41.2"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1023\/a:1025671026963","type":"journal-article","created":{"date-parts":[[2003,9,23]],"date-time":"2003-09-23T18:47:08Z","timestamp":1064342828000},"page":"243-261","source":"Crossref","is-referenced-by-count":9,"title":["Random 3-SAT: The Plot Thickens"],"prefix":"10.1007","volume":"8","author":[{"given":"Cristian","family":"Coarfa","sequence":"first","affiliation":[]},{"given":"Demetrios D.","family":"Demopoulos","sequence":"additional","affiliation":[]},{"given":"Alfonso","family":"San Miguel Aguirre","sequence":"additional","affiliation":[]},{"given":"Devika","family":"Subramanian","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5124072_CR1","doi-asserted-by":"crossref","unstructured":"Achlioptas, D. (2000). 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-;37.","DOI":"10.1145\/335305.335309"},{"key":"5124072_CR2","doi-asserted-by":"crossref","unstructured":"Achlioptas, D., Bemame, P., & Molloy, M. (2001). A sharp threshold in proof complexity. In Proc. 33rd ACM Symp. on Theory of Computing, pages 337-;346.","DOI":"10.1145\/380752.380820"},{"key":"5124072_CR3","doi-asserted-by":"crossref","unstructured":"Beame, P., Karp, R. M., Pitassi, T., & Saks, M. E. (1998). On the complexity of unsatisfiability proofs for random k-;CNF formulas. In Proc. 30th ACM Symp. on Theory of Computing, pages 561-;571.","DOI":"10.1145\/276698.276870"},{"key":"5124072_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., & Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Proc. 36th Conf. on Design Automation, pages 317-;320.","DOI":"10.1145\/309847.309942"},{"issue":"3","key":"5124072_CR5","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1287\/ijoc.4.3.267","volume":"4","author":"R. E. Bixby","year":"1992","unstructured":"Bixby, R. E. (1992). Implementing the Simplex method: the initial basis. ORSA J. on Computing, 4(3): 267-;284.","journal-title":"ORSA J. on Computing"},{"issue":"1","key":"5124072_CR6","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1287\/ijoc.6.1.15","volume":"6","author":"R. E. Bixby","year":"1994","unstructured":"Bixby, R. E. (1994). Progress in linear programming. ORSA J. on Computing, 6(1): 15-;22.","journal-title":"ORSA J. on Computing"},{"key":"5124072_CR7","unstructured":"Bouquet, F. (1999). Gestion de la dynamicite\u00b4 et e\u00b4nume\u00b4ration d'implicants premiers: une approche fonde\u00b4e sur les Diagrammes de De\u00b4cision Binaire. PhD thesis, Universite\u00b4 de Provence, France."},{"key":"5124072_CR8","unstructured":"Broder, A. Z., Frieze, A. M., & Upfal, E. (1993). On the satisfiability and maximum satisfiability of random 3-;CNF formulas. In Proc. 4th Annual ACM-;SIAM Symp. on Discrete Algorithms, pages 322-;330."},{"issue":"8","key":"5124072_CR9","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E. (1986). Graph-;based algorithms for Boolean function manipulation. IEEE Trans. On Computers, 35(8): 677-;691.","journal-title":"IEEE Trans. On Computers"},{"issue":"2","key":"5124072_CR10","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., & Hwang, L. J. (1992). Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2): 142-;170 (June).","journal-title":"Information and Computation"},{"key":"5124072_CR11","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0020-0255(90)90030-E","volume":"51","author":"M. Chao","year":"1990","unstructured":"Chao, M., & Franco, J. V. (1990). Probabilistic analysis of a generation of the unit-;clause literal selection heuristics for the k-;satisfiability problem. Information Sciences, 51: 289-;314.","journal-title":"Information Sciences"},{"key":"5124072_CR12","unstructured":"Cheeseman, P., Kanefsky, B., & Taylor, W. M. (1991). Where the really hard problems are. In Proc. 12th Int'l Joint Conf. on Artificial Intelligence (IJCAI '91), pages 331-;337."},{"issue":"4","key":"5124072_CR13","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., & Szemer\u00e9di, E. (1988). Many hard examples for resolution. J. of the ACM, 35(4): 759-;768.","journal-title":"J. of the ACM"},{"key":"5124072_CR14","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s100510170101","volume":"22","author":"S. Cocco","year":"2001","unstructured":"Cocco, S., & Monasson, R. (2001). Statistical physics analysis of the computational complexity of solving random satisfiability problems using backtrack algorithms. European Physical Journal B, 22: 505-;531.","journal-title":"European Physical Journal B"},{"key":"5124072_CR15","doi-asserted-by":"crossref","unstructured":"Cook, S. A., & Mitchell, D. G. (1997). Finding hard instances of the satisfiability problem: a survey. In Du, Gu, & Pardalos, eds., Satisfiability Problem: Theory and Applications, Volume 35 of Dimacs Series in Discrete Math. and Theoretical Computer Science. AMS.","DOI":"10.1090\/dimacs\/035\/01"},{"key":"5124072_CR16","unstructured":"Crawford, J. M., & Auton, L. D. (1993). Experimental results on the crossover point in satisfiability problems. AAAI, pages 21-;27."},{"issue":"1-2","key":"5124072_CR17","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0004-3702(95)00046-1","volume":"81","author":"J. M. Crawford","year":"1996","unstructured":"Crawford, J. M., & Auton, L. D. (1996). Experimental results on the crossover point in random 3-;SAT. Artificial Intelligence, 81(1-;2): 31-;57.","journal-title":"Artificial Intelligence"},{"key":"5124072_CR18","first-page":"1092","volume":"2","author":"J. M. Crawford","year":"1994","unstructured":"Crawford, J. M., & Baker, A. B. (1994). Experimental results on the application of satisfiability algorithms to scheduling problems. AAAI, 2: 1092-;1097.","journal-title":"AAAI"},{"key":"5124072_CR19","unstructured":"Cullberson, J., & Gent, I. P., (2000). Frozen development in graph coloring. Technical report, Department of Computer Science, University of St. Andrews. APES Research Report APES-;19-;20004."},{"key":"5124072_CR20","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem proving. Comm. of the ACM, 5: 394-;397.","journal-title":"Comm. of the ACM"},{"key":"5124072_CR21","unstructured":"Dubois, O., Boufkhad, Y., & Mandler, J. (2000). Typical random 3-;SAT formulae and the satisfiability threshold. In Proc. 11th Annual ACM-;SIAM Symp. on Discrete Algorithms, pages 126-;127."},{"key":"5124072_CR22","doi-asserted-by":"crossref","first-page":"1917","DOI":"10.1090\/S0894-0347-99-00305-7","volume":"12","author":"E. Friedgut","year":"1999","unstructured":"Friedgut, E. (1999). Necessary and sufficient conditions for sharp threshold of graph properties and the k-;SAT problem. J. Amer. Math. Soc., 12: 1917-;1054.","journal-title":"J. Amer. Math. Soc."},{"issue":"2","key":"5124072_CR23","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1006\/jagm.1996.0016","volume":"20","author":"A. Frieze","year":"1996","unstructured":"Frieze, A., & Suen, S. (1996). Analysis of two simple heuristics for random instances of k-;SAT. J. of Algorithms, 20(2): 312-;355.","journal-title":"J. of Algorithms"},{"key":"5124072_CR24","volume-title":"Computers and Intractability, A Guide to the Theory of NP-;Completeness","author":"M. R. Garey","year":"1979","unstructured":"Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability, A Guide to the Theory of NP-;Completeness. New York, NY: W. H. Freeman."},{"issue":"1-2","key":"5124072_CR25","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0004-3702(94)90109-0","volume":"70","author":"I. P. Gent","year":"1994","unstructured":"Gent, I. P., & Walsh, T. (1994). Easy problems are sometimes hard. Artificial Intelligence, 70(1-;2): 335-;345.","journal-title":"Artificial Intelligence"},{"key":"5124072_CR26","unstructured":"Gent, I. P., & Walsh, T. (1994). The SAT phase transition. In Proc. Euroropean Conf. on Artificial Intelligence, pages 105-;109."},{"key":"5124072_CR27","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00121264","volume":"8","author":"J. F. Groote","year":"1996","unstructured":"Groote, J. F. (1996). Hiding propositional constants in BDDs. Formal Methods in System Design, 8: 91-;96.","journal-title":"Formal Methods in System Design"},{"key":"5124072_CR28","doi-asserted-by":"crossref","unstructured":"Groote, J. F., & Zantema, H. (2000). Resolution and binary decision diagrams cannot simulate each other polynomially. Technical report, Department of Computer Science, Utrecht University. Technical Report UUCS-;2000-;14.","DOI":"10.1007\/3-540-45575-2_5"},{"issue":"1-2","key":"5124072_CR29","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1016\/0004-3702(94)90088-4","volume":"69","author":"T. Hogg","year":"1994","unstructured":"Hogg, T., & Williams, C. P. (1994). The hardest constraint problems: a double phase transition. Artificial Intelligence, 69(1-;2): 359-;377.","journal-title":"Artificial Intelligence"},{"key":"5124072_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","volume":"7","author":"J. N. Hooker","year":"1988","unstructured":"Hooker, J. N. (1988). Resolution vs. cutting plane solution of inference problems: some computational experience. Operations Research Letters, 7: 1-;7.","journal-title":"Operations Research Letters"},{"key":"5124072_CR31","doi-asserted-by":"crossref","unstructured":"Jha, S., Lu, Y., Minea, M., & Clarke, E. M. (1997). Equivalence checking using abstract BDDs. In Proc. 1997 Int'l Conf. on Computer Design, pages 332-;337.","DOI":"10.1109\/ICCD.1997.628891"},{"key":"5124072_CR32","unstructured":"Bayardo, Roberto J. Jr., & Schrag, Robert. (1997). Using CSP look-;back techniques to solve real-;world SAT instances. In AAAI\/IAAI, pages 203-;208."},{"key":"5124072_CR33","unstructured":"Kautz, H., & Selman, B. (1992). Planning as satisfiability. In Proc. European Conference on Artificial Intelligence, pages 359-;379."},{"key":"5124072_CR34","volume-title":"Statistics: An introduction","author":"R. E. Kirk","year":"1999","unstructured":"Kirk, R. E. (1999). Statistics: An introduction, fourth edition. Harcourt Brace, Fort Worth.","edition":"fourth edition"},{"key":"5124072_CR35","doi-asserted-by":"crossref","first-page":"1297","DOI":"10.1126\/science.264.5163.1297","volume":"264","author":"S. Kirkpatrick","year":"1994","unstructured":"Kirkpatrick, S., & Selman, B. (1994). Critical behavior in the satisfiability of random formulas. Science, 264: 1297-;1301.","journal-title":"Science"},{"key":"5124072_CR36","unstructured":"Larrabee, T., & Tsuji, Y. (1992). Evidence for a satisfiability threshold for random 3CNF formulas. Technical report, University of California, Santa Cruz. Technical report USCS-;CRL-;92042."},{"key":"5124072_CR37","unstructured":"Chu Min Li, & Anbulagan. (1997). Heuristics based on unit propagation for satisfiability problems. In IJCAI (1), pages 366-;371."},{"issue":"5","key":"5124072_CR38","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques Silva","year":"1999","unstructured":"Marques Silva, J. P., & Sakallah, K. A. (1999). GRASP-;A search algorithm for propositional satisfiability. IEEE Trans. on Computers, 48(5): 506-;521.","journal-title":"IEEE Trans. on Computers"},{"issue":"1-2","key":"5124072_CR39","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0004-3702(95)00049-6","volume":"81","author":"D. G. Mitchell","year":"1996","unstructured":"Mitchell, D. G., & Levesque, H. J. (1996). Some pitfalls for experimenters with random SAT. Artificial Intelligence, 81(1-;2): 111-;125.","journal-title":"Artificial Intelligence"},{"key":"5124072_CR40","unstructured":"Mitzenmacher, M. (1997). Tight thresholds for the pure literal rule. Technical report, Digital System Research Center, Palo Alto, California. SRC Technical Note 1997-;011."},{"key":"5124072_CR41","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1038\/22055","volume":"400","author":"R. Monasson","year":"1999","unstructured":"Monasson, R., Zecchina, R., Kirkpatrick, S., Selman B., & Troyansky, L. (1999). Determining computational complexity from characteristic \u2018phase transitions\u2019. Nature, 400: 133-;137.","journal-title":"Nature"},{"key":"5124072_CR42","doi-asserted-by":"crossref","unstructured":"Nam, G. J., Sakallah, K. A., & Rutenbar, R. A. (1999). Satisfiability-;based layout revisited: Detailed routing of complex FPGAs via search-;based boolean sat. In Proc. ACM Int'l Symp. on Field-;Programmable Gate Arrays (FPGA'99), pages 167-;175.","DOI":"10.1145\/296399.296450"},{"issue":"1-2","key":"5124072_CR43","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(95)00056-9","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., & Kirkpatrick, S. (1996). Critical behavior in the computational cost of satisfiability testing. Artificial Intelligence, 81(1-;2): 273-;295.","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"5124072_CR44","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., Mitchell, D. G., & Levesque, H. J. (1996). Generating hard satisfiability problems. Artificial Intelligence, 81(1-;2): 17-;29.","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"5124072_CR45","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0004-3702(95)00052-6","volume":"8","author":"B. M. Smith","year":"1996","unstructured":"Smith, B. M., & Dyer, M. E. (1996). Locating the phase transition in binary constraint satisfaction problems. Artificial Intelligence Journal, 8(1-;2): 155-;181.","journal-title":"Artificial Intelligence Journal"},{"key":"5124072_CR46","unstructured":"Somenzi, F. (1998). CUDD: CU Decision Diagram package. release 2.3.0. Dept. of Electrical and Computer Engineering. University of Colorado at Boulder."},{"issue":"4","key":"5124072_CR47","doi-asserted-by":"crossref","first-page":"3983","DOI":"10.1103\/PhysRevE.59.3983","volume":"59","author":"P. Svenson","year":"1999","unstructured":"Svenson, P., & Nordahl, M. G. (1999). Relaxation in graph coloring and satisfiability problems. Phys. Rev. E, 59(4): 3983-;3999.","journal-title":"Phys. Rev. E"},{"key":"5124072_CR48","unstructured":"The VIS Group. (1996). VIS: a system for verification and synthesis. In Alur, R., & Henziger, T., eds., Proc. 8th Int'l Conf. on Computer Aided Verification (CAV '96), LNCS 1102, pages 428-;432."},{"key":"5124072_CR49","doi-asserted-by":"crossref","unstructured":"Theil, H. (1979). The measurement of inequality by component of income. Economics Letter, 2.","DOI":"10.1016\/0165-1765(79)90173-3"},{"key":"5124072_CR50","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/BFb0016843","volume":"845","author":"T. E. Uribe","year":"1994","unstructured":"Uribe, T. E., & Stickel, M. E. (1994). Ordered binary decision diagrams and the Davis-;Putnam procedure. In First Int'l Conf. on Constraints in Computational Logics, Vol. 845 of Lecture Notes in Computer Science, pages 34-;39, Munich: Springer-;Verlag (September).","journal-title":"First Int'l Conf. on Constraints in Computational Logics"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025671026963.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1025671026963\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025671026963.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,13]],"date-time":"2025-07-13T03:47:39Z","timestamp":1752378459000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1025671026963"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["5124072"],"URL":"https:\/\/doi.org\/10.1023\/a:1025671026963","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}