{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T17:57:02Z","timestamp":1773511022329,"version":"3.50.1"},"reference-count":39,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1996,3,1]],"date-time":"1996-03-01T00:00:00Z","timestamp":825638400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T00:00:00Z","timestamp":1374710400000},"content-version":"vor","delay-in-days":6355,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1996,3]]},"DOI":"10.1016\/0004-3702(95)00045-3","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T14:46:00Z","timestamp":1027608360000},"page":"17-29","source":"Crossref","is-referenced-by-count":160,"title":["Generating hard satisfiability problems"],"prefix":"10.1016","volume":"81","author":[{"given":"Bart","family":"Selman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David G.","family":"Mitchell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hector J.","family":"Levesque","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/0004-3702(95)00045-3_BIB1","first-page":"119","article-title":"Outliers","volume":"25","author":"Beckman","year":"1983","journal-title":"Technometrics"},{"key":"10.1016\/0004-3702(95)00045-3_BIB2","author":"Bollobas","year":"1985"},{"key":"10.1016\/0004-3702(95)00045-3_BIB3","series-title":"Proceedings Fourth Annual ACM-SIAM Symposium on Discrete Algorithms","first-page":"322","article-title":"On the satisfiability and maximum satisfiability of random 3-CNF formulas","author":"Broder","year":"1993"},{"key":"10.1016\/0004-3702(95)00045-3_BIB4","article-title":"Report on a SAT competition","author":"Buro","year":"1992"},{"key":"10.1016\/0004-3702(95)00045-3_BIB5","first-page":"23","article-title":"Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem","volume":"51","author":"Chao","year":"1990","journal-title":"Inform. Sci."},{"key":"10.1016\/0004-3702(95)00045-3_BIB6","series-title":"Proceedings FOCS-92","first-page":"620","article-title":"Mick gets some (the odds are on his side)","author":"Chvatal","year":"1992"},{"issue":"4","key":"10.1016\/0004-3702(95)00045-3_BIB7","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","article-title":"Many hard examples for resolution","volume":"35","author":"Chvatal","year":"1988","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(95)00045-3_BIB8","series-title":"Proceedings IJCAI-91","first-page":"163","article-title":"Where the really hard problems are","author":"Cheeseman","year":"1991"},{"key":"10.1016\/0004-3702(95)00045-3_BIB9","series-title":"Proceedings 3rd Annual ACM Symposium on the Theory of Computing","first-page":"151","article-title":"The complexity of theorem-proving procedures","author":"Cook","year":"1971"},{"key":"10.1016\/0004-3702(95)00045-3_BIB10","series-title":"Proceedings AAAI-93","article-title":"Experimental results on the cross-over point in satisfiability problems","author":"Crawford","year":"1993"},{"key":"10.1016\/0004-3702(95)00045-3_BIB11","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. ACM"},{"key":"10.1016\/0004-3702(95)00045-3_BIB12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(95)00045-3_BIB13","article-title":"On random 2SAT","author":"de la Vega","year":"1992","journal-title":"Manuscript"},{"key":"10.1016\/0004-3702(95)00045-3_BIB14","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","article-title":"Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem","volume":"5","author":"Franco","year":"1983","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/0004-3702(95)00045-3_BIB15","article-title":"Analysis of three simple heuristics on a random instance of K-SAT","author":"Frieze","year":"1992","journal-title":"Manuscript"},{"key":"10.1016\/0004-3702(95)00045-3_BIB16","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0304-3975(77)90054-8","article-title":"On the complexity of regular resolution and the Davis-Putnam procedure","volume":"4","author":"Galil","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0004-3702(95)00045-3_BIB17","author":"Garey","year":"1979"},{"key":"10.1016\/0004-3702(95)00045-3_BIB18","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0004-3702(94)90109-0","article-title":"Easy problems are sometimes hard","volume":"70","author":"Gent","year":"1994","journal-title":"Artiy. Intell."},{"key":"10.1016\/0004-3702(95)00045-3_BIB19","author":"Goerdt","year":"1991","journal-title":"A threshold for unsatisfiability, Manuscript"},{"key":"10.1016\/0004-3702(95)00045-3_BIB20","article-title":"On the complexity of the satisfiability problem","author":"Goldberg","year":"1979"},{"key":"10.1016\/0004-3702(95)00045-3_BIB21","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/0004-3702(95)00045-3_BIB22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","article-title":"Resolution vs. cutting plane solution of inference problems: some computational experience","volume":"7","author":"Hooker","year":"1988","journal-title":"Oper. Res. Lett."},{"key":"10.1016\/0004-3702(95)00045-3_BIB23","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BF01531074","article-title":"Branch-and-cut solution of inference problems in propositional logic","volume":"1","author":"Hooker","year":"1990","journal-title":"Ann. Math. Artif. Intell."},{"key":"10.1016\/0004-3702(95)00045-3_BIB24","series-title":"Proceedings Integer Programming and Combinatorial Optimization","first-page":"333","article-title":"Computational experience with an interior point algorithm on the satisfiability problem","author":"Kamath","year":"1990"},{"key":"10.1016\/0004-3702(95)00045-3_BIB25","series-title":"Proceedings FOCS-94","article-title":"Tail bounds for occupancy and the satisfiability threshold conjecture","author":"Kamath","year":"1994"},{"key":"10.1016\/0004-3702(95)00045-3_BIB26","doi-asserted-by":"crossref","first-page":"1297","DOI":"10.1126\/science.264.5163.1297","article-title":"Critical behavior in the satisfiability of random Boolean expressions","volume":"264","author":"Kirkpatrick","year":"1994","journal-title":"Science"},{"key":"10.1016\/0004-3702(95)00045-3_BIB27","series-title":"Proceedings AAAI Spring Symposium on AI and NP-hard problems","article-title":"Evidence for a satisfiability threshold for random 3CNF formulas","author":"Larrabee","year":"1993"},{"key":"10.1016\/0004-3702(95)00045-3_BIB28","doi-asserted-by":"crossref","unstructured":"D.G. Mitchell and H.J. Levesque, Some pitfalls for experimenters with random SAT, Artif. Intell.81 111\u2013125 (this volume).","DOI":"10.1016\/0004-3702(95)00049-6"},{"key":"10.1016\/0004-3702(95)00045-3_BIB29","series-title":"Proceedings AAAI-92","first-page":"459","article-title":"Hard and easy distributions of SAT problems","author":"Mitchell","year":"1992"},{"issue":"4","key":"10.1016\/0004-3702(95)00045-3_BIB30","article-title":"A survey of average time analyses of satisfiability algorithms","volume":"13","author":"Purdom","year":"1990","journal-title":"J. Inform. Process."},{"key":"10.1016\/0004-3702(95)00045-3_BIB31","series-title":"Proceedings IJCAI-95","article-title":"Stochastic search and phase transitions: Al meets physics","author":"Selman","year":"1995"},{"key":"10.1016\/0004-3702(95)00045-3_BIB32_1","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1090\/dimacs\/026\/25","article-title":"Local search strategies for satisfiability testing","author":"Selman","year":"1996"},{"key":"10.1016\/0004-3702(95)00045-3_BIB32_2","series-title":"Proceedings AAAI-94","first-page":"337","author":"Selman","year":"1994"},{"key":"10.1016\/0004-3702(95)00045-3_BIB33","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(95)00056-9","article-title":"Critical behavior in the computational cost of satisfiability testing","volume":"81","author":"Selman","year":"1996","journal-title":"Artif. Intell."},{"key":"10.1016\/0004-3702(95)00045-3_BIB34","series-title":"Proceedings AAAI-92","first-page":"440","article-title":"GSAT: a new method for solving hard satisfiability problems","author":"Selman","year":"1992"},{"key":"10.1016\/0004-3702(95)00045-3_BIB35","article-title":"The complexity of automated reasoning","author":"Vellino","year":"1989"},{"key":"10.1016\/0004-3702(95)00045-3_BIB36","series-title":"Proceedings AAAI-92","first-page":"472","article-title":"Using deep structure to locate hard problems","author":"Williams","year":"1992"},{"key":"10.1016\/0004-3702(95)00045-3_BIB37","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0020-0190(92)90177-W","article-title":"Solving the satisfiability problem by using randomized approach","volume":"41","author":"Wu","year":"1992","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0004-3702(95)00045-3_BIB38","series-title":"Proceedings AAAI-88","first-page":"155","article-title":"A rearrangement search strategy for determining propositional satisfiability","author":"Zabih","year":"1988"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370295000453?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370295000453?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T17:57:38Z","timestamp":1578592658000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0004370295000453"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":39,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["0004370295000453"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(95)00045-3","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}