Abstract
Davis-Putnam (DP) [3] was the first practical complete algorithm for solving propositional satisfiability (SAT) problems. DP uses resolution to determine whether a SAT problem instance is satisfiable. However, resolution is generally impractical, as it can use exponential space and time. The most important refinement to DP was DLL [2], which replaced the resolution in DP with backtracking search. Backtracking search still uses exponential time in the worst case, but only needs linear space. As time is more readily available than space, the change to search was a big improvement.
Chapter PDF
Similar content being viewed by others
References
Byungki Cha and Kazuo Iwama. Adding new clauses for faster local search. In Proceedings of AAAI-96, pages 332–337, 1996.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394–397, 1962.
Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201–215, 1960.
Jun Gu, Paul W. Purdon, John Franco, and Benjamin W. Wah. Algorithms for the satisfiability (SAT) problem: A survey. In Satisfiability Problem: Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 19–152. American Mathematical Society, 1997.
Irina Rish and Rina Dechter. Resolution versus search: Two strategies for SAT. In Ian Gent, Hans van Maaren, and Toby Walsh, editors, SAT2000: Highlights of Satisfiability Research in the Year 2000, volume 63 of Frontiers in Artificial Intelligence and Applications, pages 215–259. IOS Press, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drake, L. (2001). Automatic Generation of Implied Clauses for SAT. In: Walsh, T. (eds) Principles and Practice of Constraint Programming — CP 2001. CP 2001. Lecture Notes in Computer Science, vol 2239. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45578-7_62
Download citation
DOI: https://doi.org/10.1007/3-540-45578-7_62
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42863-3
Online ISBN: 978-3-540-45578-3
eBook Packages: Springer Book Archive