Skip to main content
SpringerLink
Log in
Book cover

International ERCIM Workshop on Constraint Solving and Constraint Logic Programming

CologNet 2002: Recent Advances in Constraints pp 144–158Cite as

The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms

  • Conference paper
  • First Online:

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

Abstract

Propositional Satisfiability (SAT) solvers have been the subject of remarkable improvements in the last few years. Currently, the most successful SAT solvers share a number of similarities, being based on backtrack search, applying unit propagation, and incorporating a number of additional search pruning techniques. Most, if not all, of the search reduction techniques used by state-of-the-art SAT solvers have been imported from the Constraint Satisfaction Problem (CSP) domain and, most significantly, include forms of backjumping and of nogood recording. This paper proposes to investigate the actual usefulness of these CSP techniques in SAT solvers, with the objective of evaluating the actual role played by each individual technique.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. Apt. Some remarks on boolean constraint propagation. In New Trends in Constraints, number 1865 in Lecture Notes in Artificial Intelligence, pages 91–107. Springer, 2000.

    Google Scholar 

  2. R. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve exceptionally hard SAT instances. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 46–60, August 1996.

    Google Scholar 

  3. R. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the National Conference on Artificial Intelligence, pages 203–208, July 1997.

    Google Scholar 

  4. C. Bessière and J. C. Régin. MAC and combined heuristics: two reasons to forsake FC (and CBJ?) on hard problems. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 61–75, August 1996.

    Google Scholar 

  5. X. Chen and P. van Beek. Conflict-directed backjumping revisited. Journal of Artificial Intelligence Research, 14:53–81, 2001.

    MATH  MathSciNet  Google Scholar 

  6. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the Association for Computing Machinery, 5:394–397, July 1962.

    MATH  MathSciNet  Google Scholar 

  7. M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201–215, July 1960.

    MATH  MathSciNet  Google Scholar 

  8. R. Dechter. Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artificial Intelligence, 41(3):273–312, January 1990.

    Article  Google Scholar 

  9. J. Gaschnig. Performance Measurement and Analysis of Certain Search Algorithms. PhD thesis, Carnegie-Mellon University, Pittsburgh, PA, May 1979.

    Google Scholar 

  10. I. Gent. Arc consistency in SAT. In Proceedings of the European Conference on Artificial Intelligence, pages 121–125, July 2002.

    Google Scholar 

  11. E. Goldberg and Y. Novikov. BerkMin: a fast and robust sat-solver. In Proceedings of the Design and Test in Europe Conference, pages 142–149, March 2002.

    Google Scholar 

  12. C. M. Li and Anbulagan. Look-ahead versus look-back for satisfiability problems. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 341–355, October 1997.

    Google Scholar 

  13. I. Lynce and J. P. Marques-Silva. The effect of nogood recording in MAC-CBJ SAT algorithms. Technical Report RT/04/2002, INESC, April 2002.

    Google Scholar 

  14. I. Lynce and J. P. Marques-Silva. An overview of backtrack search satisfiability algorithms. Annals of Mathematics and Artificial Intelligence, 37(3):307–326, March 2003.

    Article  MATH  MathSciNet  Google Scholar 

  15. A. K. Mackworth. Consistency in networks of relations. Artificial Intelligence, 8(1):99–118, 1977.

    Article  MATH  MathSciNet  Google Scholar 

  16. J. P. Marques-Silva and K. A. Sakallah. GRASP: A new search algorithm for satisfiability. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design, pages 220–227, November 1996.

    Google Scholar 

  17. M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, pages 530–535, June 2001.

    Google Scholar 

  18. P. Prosser. Domain filtering can degrade intelligent backjumping search. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 262–267, August 1993.

    Google Scholar 

  19. P. Prosser. Hybrid algorithms for the constraint satisfaction problems. Computational Intelligence, 9(3):268–299, August 1993.

    Article  Google Scholar 

  20. P. Prosser. MAC-CBJ: maintaining arc consistency with conflict-directed backjumping. Technical Report 177, University of Strathclyde, Glasgow, Scotland, May 1995.

    Google Scholar 

  21. D. Sabin and E. Freuder. Contradicting conventional wisdom in constraint satisfaction. In Proceedings of the European Conference on Artificial Intelligence, pages 125–129, August 1994.

    Google Scholar 

  22. B. Selman and H. Kautz. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 290–295, August 1993.

    Google Scholar 

  23. R. M. Stallman and G. J. Sussman. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence, 9:135–196, October 1977.

    Google Scholar 

  24. T. Walsh. SAT v CSP. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 441–456, September 2000.

    Google Scholar 

  25. R. Zabih and D. A. McAllester. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence, pages 155–160, July 1988.

    Google Scholar 

  26. H. Zhang. SATO: An efficient propositional prover. In Proceedings of the International Conference on Automated Deduction, pages 272–275, July 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Lisbon, IST/INESC/CEL, Lisbon, Portugal

    Inês Lynce & João Marques-Silva

Authors
  1. Inês Lynce
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. João Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University College Cork, Ireland

    Barry O’Sullivan

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lynce, I., Marques-Silva, J. (2003). The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms. In: O’Sullivan, B. (eds) Recent Advances in Constraints. CologNet 2002. Lecture Notes in Computer Science, vol 2627. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36607-5_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-36607-5_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00986-3

  • Online ISBN: 978-3-540-36607-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation