Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 LDPP' - List-Based Davis-Putnam Prover
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.