Skip to main content
SpringerLink
Log in

On Selection Strategies for the DPLL Algorithm

  • Conference paper
Book cover Advances in Artificial Intelligence (Canadian AI 2004)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3060))

  • 1544 Accesses

Abstract

This paper discusses selection strategies for constructive search algorithms. Existing selection strategies have been based on a belief that it is better to search where solutions are more likely to be, or that it is better to search where the search space is smallest. While we give evidence for both strategies, we also show that they are likely to give modest results. We introduce the utility strategy, show that utility heuristics are superior, and that there is an optimal utility balance. We have focused this work on how the Davis-Putnam-Logeman-Loveland algorithm (“DPLL”) uses heuristics in solving satisfiability problems. Empirical results are given to justify our conclusions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aspvall, B., Pass, M.F., Tarjan, R.E.: A linear time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters 8(3), 121–123 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bitner, J.R., Reingold, E.M.: Backtrack programming techniques. Communications of the ACM 18(11), 651–656 (1975)

    Article  MATH  Google Scholar 

  3. Brelaz, D.: New methods to color the vertices of a graph. Communications of the ACM 22(4), 251–256 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  4. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  5. Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  6. Dechter, R., Pearl, J.: Generalized best-first search strategies and the optimality of A*. Journal of the ACM 32(3), 505–536 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  7. Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artificial Intelligence 34(1), 1–38 (1988)

    Article  MathSciNet  Google Scholar 

  8. Dechter, R., Pearl, J.: Tree clustering for constraint networks. Artificial Intelligence 38(3), 353–366 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  9. Franco, J., Paull, M.: Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics 5, 77–87 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  10. Freuder, E.C.: A sufficient condition for backtrack-free search. Journal of the ACM 29(1), 24–32 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  11. Haralick, R., Elliot, G.: Increasing tree search efficiency for constraintsatisfaction problems. Artificial Intelligence Journal 14(3), 263–313 (1980)

    Article  Google Scholar 

  12. Hooker, J.N., Vinay, V.: Branching rules for satisfiability. Journal of Automated Reasoning 15, 359–383 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  13. Hölldobler, S., Hoos, H., Strohmaier, A., Weiß, A.: The gsat/sa-familiy - relating greedy satisifability testing to simulated annealing (1994)

    Google Scholar 

  14. Irgens, M.: The Satisfiability Problem. PhD thesis, Simon Fraser University (2001) ISBN 3-89601-215-0

    Google Scholar 

  15. Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1, 167–187 (1990)

    Article  MATH  Google Scholar 

  16. 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–1009 (1994), American Association for Artificial Intelligence

    Google Scholar 

  17. Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland Publishing Co., Amsterdam (1978)

    MATH  Google Scholar 

  18. 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–446 (1992), The American Association for Artificial Intelligence

    Google Scholar 

  19. Purdom, P.W.: Search rearrangement backtracking and polynomial average time. Artificial Intelligence Journal 21, 117–133 (1983)

    Article  Google Scholar 

  20. Smith, B., Grant, S.A.: Trying harder to fail first. In: Prade, H. (ed.) Proceedings of the European Confernece on Artificial Intelligence, pp. 249–253. The European Coordinating Committee on Artificial Intelligence, John Wiley & Sons, Inc, Chichester (1998)

    Google Scholar 

  21. Tsuneto, R., Nau, D., Hendler, J.: Plan-refinement strategies and search-space size. In: Steel, S. (ed.) ECP 1997. LNCS, vol. 1348, Springer, Heidelberg (1997)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Actenum Corporation,  

    Morten Irgens & William S. Havens

  2. Simon Fraser University,  

    William S. Havens

Authors
  1. Morten Irgens
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. William S. Havens
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Windsor, 401 Sunset Avenue, N9B 3P4, Windsor, Ontario, Canada

    Ahmed Y. Tawfik

  2. School of Computer Science, University of Windsor, Windsor, Ontario,  

    Scott D. Goodwin

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Irgens, M., Havens, W.S. (2004). On Selection Strategies for the DPLL Algorithm. In: Tawfik, A.Y., Goodwin, S.D. (eds) Advances in Artificial Intelligence. Canadian AI 2004. Lecture Notes in Computer Science(), vol 3060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24840-8_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24840-8_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22004-6

  • Online ISBN: 978-3-540-24840-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation