Skip to main content
SpringerLink
Log in

The Quest for Efficient Boolean Satisfiability Solvers

  • Conference paper
  • First Online:
Automated Deduction—CADE-18 (CADE 2002)

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

Included in the following conference series:

Abstract

The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.

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. S. A. Cook, “The complexity of theorem-proving procedures,” presented at Third Annual ACM Symposium on Theory of Computing, 1971.

    Google Scholar 

  2. H. Kautz and B. Selman, “Planning as Satisfiability,” presented at European Conference on Artificial Intelligence(ECAI-92), 1992.

    Google Scholar 

  3. P. Stephan, R. Brayton, and A. Sangiovanni-Vencentelli, “Combinational Test Generation Using Satisfiability,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, pp. 1167–1176, 1996.

    Article  Google Scholar 

  4. D. Jackson and M. Vaziri, “Finding Bugs with a Constraint Solver,” presented at International Symposium on Software Testing and Analysis, Portland, OR, 2000.

    Google Scholar 

  5. M. Davis and H. Putnam, “A computing procedure for quantification theory,” Journal of ACM, vol. 7, pp. 201–215, 1960.

    Article  MATH  MathSciNet  Google Scholar 

  6. M. Davis, G. Logemann, and D. Loveland, “A machine program for theorem proving,” Communications of the ACM, vol. 5, pp. 394–397, 1962.

    Article  MATH  MathSciNet  Google Scholar 

  7. B. Selman, H. Kautz, and B. Cohen, “Local Search Strategies for Satisfiability Testing,” in Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, D. S. Johnson and M. A. Trick, Eds.: American Methematical Society, 1996.

    Google Scholar 

  8. R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, vol. C-35, pp. 677–691, 1986.

    Article  Google Scholar 

  9. G. Stålmarck, “A system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula.” US Patent N 5 27689, 1995.

    Google Scholar 

  10. J. Gu, P. W. Purdom, J. Franco, and B. W. Wah, “Algorithms for the Satisfiability (SAT) Problem: A Survey,” in DIMACS Series in Discrete Mathematics and Theoretical Computer Science: American Mathematical Society, 1997.

    Google Scholar 

  11. G.-J. Nam, K. A. Sakallah, and R. A. Rutenbar, “Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT,” presented at ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA’99), Monterey, California, 1999.

    Google Scholar 

  12. A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs,” presented at Tools and Algorithms for the Analysis and Construction of Systems (TACAS’99), 1999.

    Google Scholar 

  13. J. Crawford and L. Auton, “Experimental results on the cross-over point in satisfiability problems,” presented at National Conference on Artificial Intelligence (AAAI), 1993.

    Google Scholar 

  14. J. W. Freeman, “Improvements to Propositional Satisfiability Search Algorithms,” in Ph.D. Thesis, Department of Computer and Information Science: University of Pennsylvania, 1995.

    Google Scholar 

  15. A. V. Gelder and Y. K. Tsuji, “Satisfiability Testing with more Reasoning and Less guessing,” in Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, M. Trick, Ed.: American Mathematical Society, 1995.

    Google Scholar 

  16. O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier, “SAT v.s. UNSAT,” in Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, D. S. Johnson and M. Trick, Eds., 1993.

    Google Scholar 

  17. J. P. Marques-Silva and K. A. Sakallah, “Conflict Analysis in Search Algorithms for Propositional Satisfiability,” presented at IEEE International Conference on Tools with Artificial Intelligence, 1996.

    Google Scholar 

  18. R. Bayardo and R. Schrag, “Using CSP look-back techniques to solve real-world SAT instances,” presented at National Conference on Artificial Intelligence (AAAI), 1997.

    Google Scholar 

  19. H. Zhang, “SATO: An efficient propositional prover,” presented at International Conference on Automated Deduction (CADE), 1997.

    Google Scholar 

  20. M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” presented at 39th Design Automation Conference, 2001.

    Google Scholar 

  21. E. Goldberg and Y. Novikov, “BerkMin: a Fast and Robust SAT-Solver,” presented at Design Automation & Test in Europe (DATE 2002), 2002.

    Google Scholar 

  22. C. M. Li and Anbulagan, “Heuristics based on unit propagation for satisfiability problems,” presented at the fifteenth International Joint Conference on Artificial Intelligence (IJCAI’97), Nagayo, Japan, 1997.

    Google Scholar 

  23. O. Dubois and G. Dequen, “A backbone-search heuristic for efficient solving of hard 3-SAT formulae,” presented at International Joint Conference on Artificial Intelligence (IJCAI), 2001.

    Google Scholar 

  24. D. A. Plaisted and S. Greenbaum, “A Stucture-preserving Clause Form Translation,” Journal of Symbolic Computation, vol. 2, pp. 293–304, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  25. J. P. Marques-Silva and K. A. Sakallah, “GRASP — A New Search Algorithm for Satisfiability,” presented at IEEE International Conference on Tools with Artificial Intelligence, 1996.

    Google Scholar 

  26. J. P. Marques-Silva, “The Impact of Branching Heuristics in Propositional Satisfiability Algorithms,” presented at the 9th Portuguese Conference on Artificial Intelligence (EPIA), 1999.

    Google Scholar 

  27. J. N. Hooker and V. Vinay, “Branching rules for satisfiability,” Journal of Automated Reasoning, vol. 15, pp. 359–383, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  28. M. Buro and H. Kleine-Buning, “Report on a SAT competition,” Technical Report, University of Paderborn 1992.

    Google Scholar 

  29. R. G. Jeroslow and J. Wang, “Solving propositional satisfiability problems,” Annals of Mathematics and Artificial Intelligence, vol. 1, pp. 167–187, 1990.

    Article  MATH  Google Scholar 

  30. H. Zhang and M. Stickel, “An efficient algorithm for unit-propagation,” presented at International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, Florida, 1996.

    Google Scholar 

  31. I. Lynce and J. P. Marques-Silva, “Efficient data structures for backtrack search SAT solvers,” presented at Fifth International Symposium on the Theory and Applications of Satisfiability Testing, 2002.

    Google Scholar 

  32. C. M. Li, “Integrating equivalency reasoning into Davis-Putnam Procedure,” presented at National Conference on Artificial Intelligence (AAAI), 2000.

    Google Scholar 

  33. I. Lynce and J. P. Marques-Silva, “Integrating Simplification Techniques in SAT Algorithms,” presented at Logic in Computer Science Short Paper Session (LICS-SP), 2001.

    Google Scholar 

  34. A. V. Gelder and Y. K. Tsuji, “Satisfiability Testing with more Reasoning and Less guessing,” in Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, D. S. Johnson and M. Trick, Eds.: American Mathematical Society, 1993.

    Google Scholar 

  35. S. T. Chakradhar and V. D. Agrawal, “A Transitive Closure Based Algorithm for Test Generation,” presented at Design Automation Conference (DAC), 1991.

    Google Scholar 

  36. W. Kunz and D. K. Pradhan, “Recursive Learning: A New Implication Technique for Efficient Solutions to CAD-problems: Test, Verification and Optimization,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, pp. 1143–1158, 1994.

    Article  Google Scholar 

  37. J. P. Marques-Silva, “Improving Satisfiability Algorithms by Using Recursive Learning,” presented at International Workshop on Boolean Problems (IWBP), 1998.

    Google Scholar 

  38. P. Prosser, “Hybrid algorithms for the constraint satisfaction problem,” Computational Intelligence, vol. 9, pp. 268–299, 1993.

    Article  Google Scholar 

  39. L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, “Efficient Conflict Driven Learning in a Boolean Satisfiability Solver,” presented at International Conference on Computer Aided Design (ICCAD), San Jose, CA, 2001.

    Google Scholar 

  40. G. Hachtel and F. Somenzi, Logic Sysntheiss and Verification Algorithms: Kluwer Academic Publishers, 1996.

    Google Scholar 

  41. H. Zhang and M. Stickel, “Implementing Davis-Putnam’s method,” Technical Report, University of Iowa 1994.

    Google Scholar 

  42. P. Chatalic and L. Simon, “Multi-Resolution on Compressed Sets of Clauses,” presented at International Conference on Tools with Artificial Intelligence, 2000.

    Google Scholar 

  43. F. Aloul, M. Mneimneh, and K. Sakallah, “Backtrack Search Using ZBDDs,” presented at International Workshop on Logic Synthesis (IWLS), 2001.

    Google Scholar 

  44. S. I. Minato, “Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems,” presented at 30th Design Automation Conference (DAC), 1993.

    Google Scholar 

  45. I. Lynce and J. P. Marques-Silva, “The Puzzling Role of Simplification in Propositional Satisfiability,” presented at EPIA’01 Workshop on Constraint Satisfaction and Operational Research Techniques for Problem Solving (EPIA-CSOR), 2001.

    Google Scholar 

  46. C. P. Gomes, B. Selman, and H. Kautz, “Boosting Combinatorial Search Through Randomization,” presented at National Conference on Artificial Intelligence (AAAI), Madison, WI, 1998.

    Google Scholar 

  47. B. A. Huberman, R. M. Lukose, and T. Hogg, “An Economics approach to hard computational problems,” Science, vol. 275, pp. 51–54, 1997.

    Article  Google Scholar 

  48. I. Lynce and J. P. Marques-Silva, “Complete unrestricted backtracking algorithms for Satisfiability,” presented at Fifth International Symposium on the Theory and Applications of Satisfiability Testing, 2002.

    Google Scholar 

  49. C. P. Gomes, B. Selman, N. Crator, and H. Kautz, “Heavy-tailed phenomena in satisfiability and constraint satisfaction problems,” Journal of Automated Reasoning, vol. 24(1/2), pp. 67–100, 1999.

    Article  Google Scholar 

  50. “Prover Proof Engine,” Prover Technology.

    Google Scholar 

  51. J. F. Groote and J. P. Warners, “The propositional formula checker HeerHugo,” Journal of Automated Reasoning, vol. 24, 2000.

    Google Scholar 

  52. Y. Shang and B. W. Wah, “A Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems,” Journal of Global Optimization, vol. 12, pp. 61–99, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  53. I. Gent and T. Walsh, “The SAT Phase Transition,” presented at European Conference on Artificial Intelligence (ECAI-94), 1994.

    Google Scholar 

  54. M. Prasad, P. Chong, and K. Keutzer, “Why is ATPG easy?,” presented at Design Automation Conference (DAC99), 1999.

    Google Scholar 

  55. F. Brglez, X. Li, and M. Stallmann, “The role of a skeptic agent in testing and benchmarking of SAT algorithms,” presented at Fifth International Symposium on theTheory and Applications of Satisfiability Testing, 2002.

    Google Scholar 

  56. O. Strichman, “Pruning techniques for the SAT-based Bounded Model Checking Problem,” presented at 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARM’01), 2001.

    Google Scholar 

  57. M. Ganai, L. Zhang, P. Ashar, A. Gupta, and S. Malik, “Combining Strengths of Circuit-based and CNF-based Algorithms for a High-Performance SAT Solver,” presented at Design Automation Conference (DAC’02), 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical Engineering, Princeton University, Princeton, NJ, 08544

    Lintao Zhang & Sharad Malik

Authors
  1. Lintao Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sharad Malik
    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 of Manchester, Oxford Rd, Manchester, M13 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, L., Malik, S. (2002). The Quest for Efficient Boolean Satisfiability Solvers. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-45620-1_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43931-8

  • Online ISBN: 978-3-540-45620-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation