{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:18:14Z","timestamp":1743085094446,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540220046"},{"type":"electronic","value":"9783540248408"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24840-8_20","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T18:58:39Z","timestamp":1281293919000},"page":"277-291","source":"Crossref","is-referenced-by-count":0,"title":["On Selection Strategies for the DPLL Algorithm"],"prefix":"10.1007","author":[{"given":"Morten","family":"Irgens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William S.","family":"Havens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"20_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Pass, M.F., Tarjan, R.E.: A linear time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters\u00a08(3), 121\u2013123 (1979)","journal-title":"Information Processing Letters"},{"issue":"11","key":"20_CR2","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1145\/361219.361224","volume":"18","author":"J.R. Bitner","year":"1975","unstructured":"Bitner, J.R., Reingold, E.M.: Backtrack programming techniques. Communications of the ACM\u00a018(11), 651\u2013656 (1975)","journal-title":"Communications of the ACM"},{"issue":"4","key":"20_CR3","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1145\/359094.359101","volume":"22","author":"D. Brelaz","year":"1979","unstructured":"Brelaz, D.: New methods to color the vertices of a graph. Communications of the ACM\u00a022(4), 251\u2013256 (1979)","journal-title":"Communications of the ACM"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"20_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"3","key":"20_CR6","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1145\/3828.3830","volume":"32","author":"R. Dechter","year":"1985","unstructured":"Dechter, R., Pearl, J.: Generalized best-first search strategies and the optimality of A*. Journal of the ACM\u00a032(3), 505\u2013536 (1985)","journal-title":"Journal of the ACM"},{"issue":"1","key":"20_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(87)90002-6","volume":"34","author":"R. Dechter","year":"1988","unstructured":"Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artificial Intelligence\u00a034(1), 1\u201338 (1988)","journal-title":"Artificial Intelligence"},{"issue":"3","key":"20_CR8","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0004-3702(89)90037-4","volume":"38","author":"R. Dechter","year":"1989","unstructured":"Dechter, R., Pearl, J.: Tree clustering for constraint networks. Artificial Intelligence\u00a038(3), 353\u2013366 (1989)","journal-title":"Artificial Intelligence"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","volume":"5","author":"J. Franco","year":"1983","unstructured":"Franco, J., Paull, M.: Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics\u00a05, 77\u201387 (1983)","journal-title":"Discrete Applied Mathematics"},{"issue":"1","key":"20_CR10","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/322290.322292","volume":"29","author":"E.C. Freuder","year":"1982","unstructured":"Freuder, E.C.: A sufficient condition for backtrack-free search. Journal of the ACM\u00a029(1), 24\u201332 (1982)","journal-title":"Journal of the ACM"},{"issue":"3","key":"20_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0004-3702(80)90051-X","volume":"14","author":"R. Haralick","year":"1980","unstructured":"Haralick, R., Elliot, G.: Increasing tree search efficiency for constraintsatisfaction problems. Artificial Intelligence Journal\u00a014(3), 263\u2013313 (1980)","journal-title":"Artificial Intelligence Journal"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF00881805","volume":"15","author":"J.N. Hooker","year":"1995","unstructured":"Hooker, J.N., Vinay, V.: Branching rules for satisfiability. Journal of Automated Reasoning\u00a015, 359\u2013383 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR13","unstructured":"H\u00f6lldobler, S., Hoos, H., Strohmaier, A., Wei\u00df, A.: The gsat\/sa-familiy - relating greedy satisifability testing to simulated annealing (1994)"},{"key":"20_CR14","unstructured":"Irgens, M.: The Satisfiability Problem. PhD thesis, Simon Fraser University (2001) ISBN 3-89601-215-0"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R.G. Jeroslow","year":"1990","unstructured":"Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence\u00a01, 167\u2013187 (1990)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"20_CR16","unstructured":"Joslin, D., Pollack, M.: Least cost-flow repair: A plan refinement strategy for partial order planning. In: Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI 1994), Seattle, Washington, pp. 1004\u20131009 (1994), American Association for Artificial Intelligence"},{"key":"20_CR17","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D.W. Loveland","year":"1978","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland Publishing Co., Amsterdam (1978)"},{"key":"20_CR18","unstructured":"Mitchell, D., Selman, B., Levesque, H.: Hard and easy distributions of sat problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI 1992), Menlo Park, California, July 1992, pp. 440\u2013446 (1992), The American Association for Artificial Intelligence"},{"key":"20_CR19","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0004-3702(83)80007-1","volume":"21","author":"P.W. Purdom","year":"1983","unstructured":"Purdom, P.W.: Search rearrangement backtracking and polynomial average time. Artificial Intelligence Journal\u00a021, 117\u2013133 (1983)","journal-title":"Artificial Intelligence Journal"},{"key":"20_CR20","unstructured":"Smith, B., Grant, S.A.: Trying harder to fail first. In: Prade, H. (ed.) Proceedings of the European Confernece on Artificial Intelligence, pp. 249\u2013253. The European Coordinating Committee on Artificial Intelligence, John Wiley & Sons, Inc, Chichester (1998)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63912-8_103","volume-title":"Recent Advances in AI Planning","author":"R. Tsuneto","year":"1997","unstructured":"Tsuneto, R., Nau, D., Hendler, J.: Plan-refinement strategies and search-space size. In: Steel, S. (ed.) ECP 1997. LNCS, vol.\u00a01348, Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24840-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:02:33Z","timestamp":1558285353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24840-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540220046","9783540248408"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24840-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}