{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:18:31Z","timestamp":1759637911580},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584674"},{"type":"electronic","value":"9783540489795"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58467-6_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:13:44Z","timestamp":1330254824000},"page":"355-366","source":"Crossref","is-referenced-by-count":5,"title":["The hardest random SAT problems"],"prefix":"10.1007","author":[{"given":"Ian P.","family":"Gent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toby","family":"Walsh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"B. Aspvall, M.F. Plass, and R.E. Tarjan. A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters, 8:121\u2013123, 1979.","journal-title":"Information Processing Letters"},{"key":"31_CR2","unstructured":"P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the really hard problems are. In Proceedings of the 12th IJCAI, pages 163\u2013169. International Joint Conference on Artificial Intelligence, 1991."},{"key":"31_CR3","unstructured":"J.M. Crawford and L.D. Auton. Experimental results on the crossover point in satisfiability problems. In Proceedings of the Eleventh National Conference on Artificial Intelligence, pages 21\u201327. AAAI Press\/The MIT Press, 1993."},{"key":"31_CR4","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. J. Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"J. Association for Computing Machinery"},{"key":"31_CR5","unstructured":"O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier. SAT versus UNSAT. In Proceedings of the Second DIMACS Challenge, 1993."},{"key":"31_CR6","volume-title":"Research Paper 642","author":"I. P. Gent","year":"1993","unstructured":"Ian P. Gent and Toby Walsh. Easy problems are sometimes hard. Research Paper 642, Dept. of Artificial Intelligence, Edinburgh, June 27 1993."},{"key":"31_CR7","unstructured":"I.P. Gent and T. Walsh. The SAT phase transition. Proceedings of ECAI-94, 1994."},{"key":"31_CR8","unstructured":"T. Hogg and C. Williams. The Hardest Constraint Problems: A Double Phase Transition. Technical report, Dynamics of Computation Group, Xerox Palo Alto Research Center, 1993. PARC Preprint."},{"key":"31_CR9","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BF01531074","volume":"1","author":"J. N. Hooker","year":"1990","unstructured":"J. N. Hooker and C. Fedjki. Branch-and-cut solution of inference problems in propositional logic. Annals of Mathematics and Artificial Intelligence, 1:123\u2013139, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"4","key":"31_CR10","doi-asserted-by":"crossref","first-page":"943","DOI":"10.1137\/0214067","volume":"14","author":"P. Walton Purdom Jr.","year":"1985","unstructured":"Paul Walton Purdom Jr. and Cynthia A. Brown. The pure literal rule and polynomial average time. SIAM Journal of Computing, 14(4):943\u2013953, November 1985.","journal-title":"SIAM Journal of Computing"},{"key":"31_CR11","volume-title":"Technical Report UCSC-CRL-92-42","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee and Y. Tsuji. Evidence for a Satisfiability Threshold for Random 3CNF Formulas. Technical Report UCSC-CRL-92-42, Baskin Center for Computer Engineering and Information Sciences, University of California, Santa Cruz, 1992."},{"key":"31_CR12","unstructured":"David Mitchell, Bart Selman, and Hector Levesque. Hard and easy distributions of SAT problems. In Proceedings, 10th National Conference on Artificial Intelligence. AAAI Press\/The MIT Press, July 12\u201316 1992."},{"key":"31_CR13","unstructured":"Bart Selman, Hector Levesque, and David Mitchell. A new method for solving hard satisfiability problems. In Proceedings, 10th National Conference on Artificial Intelligence. AAAI Press\/The MIT Press, 1992."}],"container-title":["Lecture Notes in Computer Science","KI-94: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58467-6_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:16:26Z","timestamp":1619558186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58467-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584674","9783540489795"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-58467-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}