LDPP' - List-Based Davis-Putnam Prover
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
- LDPP' has been used by Ian Gent and Toby Walsh in their study
of hard satisfiability problems.
- 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
Mark E. Stickel (stickelai.sri.com)