Abstract
Propositional theorem provers have become a core technology in a range of areas, such as in hardware and software verification, AI planning , and mathematical discovery. The theorem provers rely on fast Boolean satisfiabilty (SAT) solving procedures, whose roots can be traced back to the work by Martin Davis and colleagues in the late 1950s. We review the history of this work with recent advances and applications.
This paper is dedicated to Martin Davis, in recognition of his foundational contributions to the area of automated reasoning.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
The Dunham, Fridshal, and Sward project might have begun in 1957.
- 3.
Almost all of the papers cited in the introduction can be found in [46].
- 4.
This project was also executed at IBM.
- 5.
\(\overline{c}\) denotes \(not \ c\) here.
- 6.
A complementary literal has the same variable name but opposite negation status.
- 7.
An AE formula is a formula with all quantifiers leftmost with no existential quantifier to the left of a universal quantifier.
- 8.
A tautological clause contains \(p \vee \lnot p\) for some variable p.
- 9.
U.S. News and World Report: Best Grad Schools 2014.
References
Audemard, G., & Simon, L. (2009, July). Predicting learnt clauses quality in modern SAT solvers. In 21st IJCAI (pp. 399–404), Pasadena, CA.
Beame, P., Kautz, H., & Sabharwal, A. (2004). Understanding and harnessing the potential of clause learning. JAIR, 22, 319–351.
Biere, A. (2012). Plingeling: Solver description. In SAT Challenge 2012.
Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.) (2009). Handbook of satisfiability. IOS Press.
Bloom, B., Grove, D., Herta, B., Sabharwal, A., Samulowitz, H., & Saraswat, V. A. (2012). SatX10: A scalable plug&play parallel sat framework—(tool presentation). In 15th SAT (pp. 463–468).
Böhm, M., & Speckenmeyer, E. (1996). A fast parallel SAT-solver—efficient workload balancing. Annals of Mathematics and Artificial Intelligence, 17(3–4), 381–400.
Cook, S. A. (1971, May). The complexity of theorem proving procedures. In Conference Record of 3rd STOC (pp. 151–158), Shaker Heights, OH.
Davis, M. (1983). A computer program for Presburger’s algorithm. In J. Siekmann and G. Wrightson (Eds.) Automated reasoning: Classical papers on computational logic (pp. 41–48). Springer.
Davis, M. (2014). Private communication.
Davis, M. (2015). My life as a logician. In this volume. Springer.
Davis, M., Logemann, G., & Loveland, D. (1962) A machine program for theorem-proving. Communication of ACM, 5, 394–397. ISSN: 0001-0782.
Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7, 201–215. ISSN: 0004-5411.
Dunham, B., Fridshal, R., & Sward, G. (1959). A non-heuristic program for proving elementary logical theorems. In IFIP Congress (pp. 282–284).
Dunham, B., Fridshal, R., & Sward, G. (1959). A non-heuristic program for proving elementary logical theorems (abstract). CACM, 2, 19–20.
Eén, N., & Sörensson, N. (2005, June). MiniSat: A SAT solver with conflict-clause minimization. In 8th SAT, St. Andrews, U.K.
Frost, D., Rish, I., & Vila, L. (1997). Summarizing CSP hardness with continuous probability distributions. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97) (pp. 327–334). New Providence, RI: AAAI Press.
Gelernter, H. (1960). Realization of a geometry theorem proving machine. In Information processing (pp. 273–282). UNESCO, Paris: R. Oldenbourg, Munich: Butterworths, London.
Gelernter, H., Hansen, J. R., & Loveland, D. W. (1960). Empirical explorations of the geometry theorem machine. In Papers presented at the May 3–5, 1960, Western Joint IRE-AIEE-ACM computer conference (pp. 143–149). ACM.
Gelfond, M. (2008). Answer sets. In F. van Harmelen, V. Lifschitz and B. Porter (Eds.), Handbook of knowledge representation. Foundations of artificial intelligence, Chapter 7 (Vol. 3, pp. 285–316). Elsevier.
Gilmore, P. (1958). Private communication.
Gilmore, P. C. (1959). A program for the production of proofs of theorems derivable within the first order predicate calculus. In CACM (Vol. 2, pp. 19–19). ACM.
Gilmore, P. C. (1960). A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4, 28–35. ISSN: 0018-8646.
Goldberg, E., & Novikov, Y. (2007). BerkMin: A fast and robust SAT-solver. Discrete Applied Mathematics, 155(12), 1549–1561.
Gomes, C., Kautz, H., Sabharwal, A., & Selman, B. (2008). Satisfiability solvers. In F. Van Harmelen, V. Lifschitz and B. Porter (Eds.), Handbook of knowledge representation (pp. 89–134). Elsevier.
Gomes, C., Selman, B., & Crato, N. (1997). Heavy-tailed distributions in combinatorial search. In 3rd CP (pp. 121–135).
Gomes, C. P., Selman, B., & Kautz, H. (1998, July). Boosting combinatorial search through randomization. In 15th AAAI (pp. 431–437), Madison, WI.
Hamadi, Y., Jabbour, S., & Sais, L. (2009). Manysat: A parallel SAT solver. Journal on Satisfiability, 6(4), 245–262.
Hamadi, Y., & Wintersteiger, C. M. (2012). Seven challenges in parallel SAT solving. In 26th AAAI.
Hogg, T., & Williams, C. (1994). Expected gains from parallelizing constraint solving for hard problems. In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI-94) (pp. 1310–1315). Seattle, WA: AAAI Press.
Jeroslow, R. G., & Wang, J. (1990). Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1(1-4), 167–187.
Katsirelos, G., Sabharwal, A., Samulowitz, H., & Simon, L. (2013). Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers. In 27th AAAI.
Kautz, H., & Selman, B. (1996). Pushing the envelope: Planning, propositional logic, and stochastic search. In Proceedings of AAAI-96, Portland, OR.
Levin, L. A. (1973). Universal sequential search problems. Problems of Information Transmission, 9(3), 265–266. Originally in Russian.
Marques-Silva, J. P. (1999, September). The impact of branching heuristics in propositional satisfiability algorithms. In 9th Portuguese Conference on AI. LNCS (Vol. 1695, pp. 62–74).
Marques-Silva, J. P., & Sakallah, K. A. (1996, November). GRASP—a new search algorithm for satisfiability. In ICCAD (pp. 220–227), San Jose, CA.
Mitchell, D., & Levesque, H. (1996). Some pitfalls for experimenters with random SAT. Artificial Intelligence, 81(1–2), 111–125.
Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001, June). Chaff: Engineering an efficient SAT solver. In 38th DAC (pp. 530–535), Las Vegas, NV.
Nadel, A. (2002). Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master’s thesis, Hebrew University of Jerusalem.
Newell, A., Shaw, J. C., & Simon, H. (1957). Empirical explorations with the logic theory machine: A case study in heuristics. Western Joint Comp. Conf., 1, 49–73.
Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of Association for Computing Machinery, 53(6), 937–977.
Palù, A. D., Dovier, A., Formisano, A., & Pontelli, E. (2015). CUD@SAT: SAT solving on GPUs. Journal of Experimental and Theoretical Artificial Intelligence, 27(3), 293–316.
Pipatsrisawat, K., & Darwiche, A. (2006). RSat 1.03: SAT solver description. Technical Report D-152, Automated Reasoning Group, Computer Science Department, UCLA.
Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. AI Journal, 175(2), 512–525.
Selman, B., Kautz, H., & Cohen, B. (1996). Local search strategies for satisfiability testing. In D. S. Johnson and M. A. Trick (Eds.), Cliques, coloring, and satisfiability: The second DIMACS implementation challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (Vol. 26, pp. 521–532). American Mathematical Society.
Selman, B., Levesque, H. J., & Mitchell, D. G. (1992, July). A new method for solving hard satisfiability problems. In 10th AAAI (pp. 440–446), San Jose, CA.
Siekmann, J., & Wrightson, G. (Eds.) (1983). Automation of Reasoning1: Classical Papers on Computational Logic 1957–1966. Springer Publishing Company Incorporated.
Stallman, R. M., & Sussman, G. J. (1977). Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. AI Journal, 9, 135–196.
Szeider, S. (2005). Backdoor sets for DLL subsolvers. Journal of Automated Reasoning, 35(1–3).
Wang, H. (1960, April). Proving theorems by pattern recognition—I. Communications of the ACM, 3(4), 220–234. ISSN: 0001-0782.
Wang, H. (1960). Toward mechanical mathematics. IBM Journal of Research and Development, 4, 2–22. ISSN: 0018-8646.
Wang, H. (1961). Proving theorems by pattern recognition—II. Bell System Technical Journal, 40(1), 1–41. ISSN: 1538-7305.
Williams, R., Gomes, C., & Selman, B. (2003). Backdoors to typical case complexity. In 18th IJCAI.
Zhang, H. (1997, July). SATO: An efficient propositional prover. In 14th CADE. LNCS (Vol. 1249, pp. 272–275), Townsville, Australia.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Loveland, D., Sabharwal, A., Selman, B. (2016). DPLL: The Core of Modern Satisfiability Solvers. In: Omodeo, E., Policriti, A. (eds) Martin Davis on Computability, Computational Logic, and Mathematical Foundations. Outstanding Contributions to Logic, vol 10. Springer, Cham. https://doi.org/10.1007/978-3-319-41842-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-41842-1_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41841-4
Online ISBN: 978-3-319-41842-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)