LDPP' - List-Based Davis-Putnam Prover

Overview

LDPP' is an efficient Common Lisp implementation of the Davis-Putnam-Loveland-Logemann procedure for testing satisfiability and finding models of sets of propositional clauses. The pigeonhole problem with 10 holes and 11 objects can be decided by LDPP' with a search space of 10! = 3,628,800 branches in 3.0 minutes using Allegro Common Lisp on a Sun Ultra 1/170E Creator (167 MHz UltraSPARC).

• LDPP' and its predecessors have been used to solve open problems of the existence of quasigroups [Slaney et al., 1995].
• LDPP' is used in SRI's DISSECT (Database Inference System Security Tool), a prototype tool for controlling specific types of inference in a multilevel database.
• LDPP' has been used by Ian Gent and Toby Walsh in their study of hard satisfiability problems.

Selected Publications

• Zhang, H. and M.E. Stickel. Implementing the Davis-Putnam method. Journal of Automated Resoning 24, 1-2 (February 2000), 277-296.
• Slaney, J., M. Fujita, and M. Stickel. Automated reasoning and exhaustive search: quasigroup existence problems. Computers and Mathematics with Applications 29 (1995), 115-132.
• Uribe, T.E. and M.E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. Proceedings of the First International Conference on Constraints in Computational Logics, Munich, Germany, September 1994, 34-49.

Some Related Systems

• FINDER, by John Slaney (jksarp.anu.edu.au)
• MACE, by William McCune (mccunemcs.anl.gov)
• POSIT, by Jon Freeman (freemangradient.cis.upenn.edu)
• SATO, by Hantao Zhang (hzhangcs.uiowa.edu)
• SATLIB Satisfiability Library lists satisfiability problems and solvers
• CSPLib: a problem library for constraints lists constraint problems and solvers
• Automated Reasoning Systems Database lists additional automated reasoning systems

Downloads

• LDPP' is included in SNARK - SRI's New Automated Reasoning Kit
• Quasigroup example generator

Mark E. Stickel (stickelai.sri.com)