{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:39:53Z","timestamp":1752460793446},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540637530"},{"type":"electronic","value":"9783540696421"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0017431","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:22:46Z","timestamp":1132644166000},"page":"77-91","source":"Crossref","is-referenced-by-count":2,"title":["The logic of search algorithms: Theory and applications"],"prefix":"10.1007","author":[{"given":"Ian P.","family":"Gent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judith L.","family":"Underwood","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,10]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"R.J. Bayardo and R.C. Schrag. Using CSP look-back techniques to solve exceptionally hard SAT instances. In CP-96, pages 46\u201360. Springer, 1996.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"R.J. Bayardo and R.C. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings, AAAI-97, 1997.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"7_CR3","unstructured":"P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the really hard problems are. In Proceedings of the 12th IJCAI, pages 331\u2013337, 1991."},{"key":"7_CR4","volume-title":"Implementing Mathematics with The Nuprl Development System","author":"R. Constable","year":"1986","unstructured":"R. Constable et al. Implementing Mathematics with The Nuprl Development System. Prentice-Hall, New Jersey, 1986."},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Comms. ACM, 5:394\u2013397, 1962.","journal-title":"Comms. ACM"},{"key":"7_CR6","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":"7_CR7","unstructured":"J. Frank and C. Martel. Phase transitions in random graphs. In Proceedings, Workshop on Studying and Solving Really Hard Problems, CP-95, 1995."},{"key":"7_CR8","first-page":"25","volume":"1","author":"M.L. Ginsberg","year":"1993","unstructured":"M.L. Ginsberg. Dynamic backtracking. Journal of AI Research, 1:25\u201346, 1993.","journal-title":"Journal of AI Research"},{"key":"7_CR9","unstructured":"J. Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge Tracts in Computer Science, Vol. 7. Cambridge University Press, 1989."},{"key":"7_CR10","unstructured":"S.A. Grant and B.M. Smith. The phase transition behaviour of maintaining arc consistency. In Proceedings of ECAI-96, pages 175\u2013179, 1996."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"T. Griffin. A formulas-as-types notion of control. In Proc. of the Seventeeth Annual Symp. on Principles of Programming Languages, pages 47\u201358, 1990.","DOI":"10.1145\/96709.96714"},{"key":"7_CR12","unstructured":"W. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1016\/S0004-3702(96)00027-6","volume":"89","author":"G. Kondrak","year":"1997","unstructured":"G. Kondrak and P. van Beek. A theoretical evaluation of selected backtracking algorithms. Artificial Intelligence, 89:365\u2013387, 1997.","journal-title":"Artificial Intelligence"},{"key":"7_CR14","unstructured":"Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994."},{"key":"7_CR15","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/356022.356030","volume":"9","author":"S. Martello","year":"1983","unstructured":"S. Martello. An enumerative algorithm for fording Hamiltonian circuits in a directed graph. ACM Transactions on Mathematical Software, 9:131\u2013138, 1983.","journal-title":"ACM Transactions on Mathematical Software"},{"key":"7_CR16","unstructured":"C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. (TR 89-1151)."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"C. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, 1991.","DOI":"10.1109\/LICS.1991.151634"},{"key":"7_CR18","unstructured":"R. Pollack. The Theory of Lego. PhD thesis, University of Edinburgh, 1995. Available as report ECS-LFCS-95-323."},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"P. Prosser. Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence, 9:268\u2013299, 1993.","journal-title":"Computational Intelligence"},{"key":"7_CR20","series-title":"Res. rep. 95-177","volume-title":"Maintaining arc-consistency with conflict-directed backjumping","author":"P. Prosser","year":"1995","unstructured":"P. Prosser. Maintaining arc-consistency with conflict-directed backjumping. Res. rep. 95-177, Dept. of Computer Science, University of Strathclyde, UK, 1995."},{"key":"7_CR21","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0004-3702(95)00048-8","volume":"81","author":"P. Prosser","year":"1996","unstructured":"P. Prosser. An empirical study of phase transitions in binary constraint satisfaction problems. Artificial Intelligence, 81:127\u2013154, 1996.","journal-title":"Artificial Intelligence"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"D. Sabin and E.C. Freuder. Contradicting conventional wisdom in constraint satisfaction. In Proceedings of ECAI-94. pages 125\u2013129, 1994.","DOI":"10.1007\/3-540-58601-6_86"},{"key":"7_CR23","unstructured":"J. Underwood. Aspects of the Computational Content of Proofs. PhD thesis, Cornell University, 1994."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming-CP97"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0017431","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:53:05Z","timestamp":1586573585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0017431"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540637530","9783540696421"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0017431","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}