The logic of search algorithms: Theory and applications

  • Ian P. Gent
  • Judith L. Underwood
Session 2a
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1330)


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.


Constraint Satisfaction Problem Recursive Call Correctness Proof Partial Assignment Unit Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.Google Scholar
  2. 2.
    R.J. Bayardo and R.C. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings, AAAI-97, 1997.Google Scholar
  3. 3.
    P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the really hard problems are. In Proceedings of the 12th IJCAI, pages 331–337, 1991.Google Scholar
  4. 4.
    R. Constable et al. Implementing Mathematics with The Nuprl Development System. Prentice-Hall, New Jersey, 1986.Google Scholar
  5. 5.
    M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Comms. ACM, 5:394–397, 1962.Google Scholar
  6. 6.
    M. Davis and H. Putnam. A computing procedure for quantification theory. J. Association for Computing Machinery, 7:201–215, 1960.Google Scholar
  7. 7.
    J. Frank and C. Martel. Phase transitions in random graphs. In Proceedings, Workshop on Studying and Solving Really Hard Problems, CP-95, 1995.Google Scholar
  8. 8.
    M.L. Ginsberg. Dynamic backtracking. Journal of AI Research, 1:25–46, 1993.Google Scholar
  9. 9.
    J. Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge Tracts in Computer Science, Vol. 7. Cambridge University Press, 1989.Google Scholar
  10. 10.
    S.A. Grant and B.M. Smith. The phase transition behaviour of maintaining arc consistency. In Proceedings of ECAI-96, pages 175–179, 1996.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    G. Kondrak and P. van Beek. A theoretical evaluation of selected backtracking algorithms. Artificial Intelligence, 89:365–387, 1997.Google Scholar
  14. 14.
    Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.Google Scholar
  15. 15.
    S. Martello. An enumerative algorithm for fording Hamiltonian circuits in a directed graph. ACM Transactions on Mathematical Software, 9:131–138, 1983.Google Scholar
  16. 16.
    C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. (TR 89-1151).Google Scholar
  17. 17.
    C. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, 1991.Google Scholar
  18. 18.
    R. Pollack. The Theory of Lego. PhD thesis, University of Edinburgh, 1995. Available as report ECS-LFCS-95-323.Google Scholar
  19. 19.
    P. Prosser. Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence, 9:268–299, 1993.Google Scholar
  20. 20.
    P. Prosser. Maintaining arc-consistency with conflict-directed backjumping. Res. rep. 95-177, Dept. of Computer Science, University of Strathclyde, UK, 1995.Google Scholar
  21. 21.
    P. Prosser. An empirical study of phase transitions in binary constraint satisfaction problems. Artificial Intelligence, 81:127–154, 1996.Google Scholar
  22. 22.
    D. Sabin and E.C. Freuder. Contradicting conventional wisdom in constraint satisfaction. In Proceedings of ECAI-94. pages 125–129, 1994.Google Scholar
  23. 23.
    J. Underwood. Aspects of the Computational Content of Proofs. PhD thesis, Cornell University, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Ian P. Gent
    • 1
  • Judith L. Underwood
    • 2
  1. 1.APES Research Group, Department of Computer ScienceUniversity of StrathclydeGlasgowUK
  2. 2.BeAUTy Research Group, Department of Computing ScienceUniversity of GlasgowGlasgowUK

Personalised recommendations