Abstract
Many search algorithms have been introduced without correctness proofs, or proved only with respect to an informal semantics of the algorithm. We address this problem by taking advantage of the correspondence between programs and proofs. We give a single proof of the correctness of a very general search algorithm, for which we provide Scheme code. It is straightforward to implement service functions to implement algorithms such as Davis-Putnam for satisfiability or forward checking (FC) for constraint satisfaction, and to incorporate conflict-directed backjumping (CBJ) and heuristics for variable and value ordering. By separating the search algorithm from problem features, our work should enable the much speedier implementation of sophisticated search methods such as FC-CBJ in new domains, and we illustrate this by sketching an implementation for the Hamiltonian Circuit problem.
Judith Underwood is supported by EPSRC award GR/L/15685. We thank members of APES, particularly Patrick Prosser and Toby Walsh for their code. We especially thank Mr Denis Magnus for his invaluable contributions to our research.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.J. Bayardo and R.C. Schrag. Using CSP look-back techniques to solve exceptionally hard SAT instances. In CP-96, pages 46–60. Springer, 1996.
R.J. Bayardo and R.C. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings, AAAI-97, 1997.
P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the really hard problems are. In Proceedings of the 12th IJCAI, pages 331–337, 1991.
R. Constable et al. Implementing Mathematics with The Nuprl Development System. Prentice-Hall, New Jersey, 1986.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Comms. ACM, 5:394–397, 1962.
M. Davis and H. Putnam. A computing procedure for quantification theory. J. Association for Computing Machinery, 7:201–215, 1960.
J. Frank and C. Martel. Phase transitions in random graphs. In Proceedings, Workshop on Studying and Solving Really Hard Problems, CP-95, 1995.
M.L. Ginsberg. Dynamic backtracking. Journal of AI Research, 1:25–46, 1993.
J. Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge Tracts in Computer Science, Vol. 7. Cambridge University Press, 1989.
S.A. Grant and B.M. Smith. The phase transition behaviour of maintaining arc consistency. In Proceedings of ECAI-96, pages 175–179, 1996.
T. Griffin. A formulas-as-types notion of control. In Proc. of the Seventeeth Annual Symp. on Principles of Programming Languages, pages 47–58, 1990.
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–490. Academic Press, 1980.
G. Kondrak and P. van Beek. A theoretical evaluation of selected backtracking algorithms. Artificial Intelligence, 89:365–387, 1997.
Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.
S. Martello. An enumerative algorithm for fording Hamiltonian circuits in a directed graph. ACM Transactions on Mathematical Software, 9:131–138, 1983.
C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. (TR 89-1151).
C. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, 1991.
R. Pollack. The Theory of Lego. PhD thesis, University of Edinburgh, 1995. Available as report ECS-LFCS-95-323.
P. Prosser. Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence, 9:268–299, 1993.
P. Prosser. Maintaining arc-consistency with conflict-directed backjumping. Res. rep. 95-177, Dept. of Computer Science, University of Strathclyde, UK, 1995.
P. Prosser. An empirical study of phase transitions in binary constraint satisfaction problems. Artificial Intelligence, 81:127–154, 1996.
D. Sabin and E.C. Freuder. Contradicting conventional wisdom in constraint satisfaction. In Proceedings of ECAI-94. pages 125–129, 1994.
J. Underwood. Aspects of the Computational Content of Proofs. PhD thesis, Cornell University, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gent, I.P., Underwood, J.L. (1997). The logic of search algorithms: Theory and applications. In: Smolka, G. (eds) Principles and Practice of Constraint Programming-CP97. CP 1997. Lecture Notes in Computer Science, vol 1330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017431
Download citation
DOI: https://doi.org/10.1007/BFb0017431
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63753-0
Online ISBN: 978-3-540-69642-1
eBook Packages: Springer Book Archive