CMU Artificial Intelligence Repository
DP: Solving Propositional Satisfiability Problems
areas/kr/systems/kl_one/dp/
This directory contains DP, an implementation of the well known
Davis Putnam procedure for solving propositional satisfiability
problems.
Version: 02.1 (1-JUL-93)
Requires: ANSI C
Copying: Copyright (C) 1993 by Peter Barth
GNU GPL v2
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Author(s): Peter Barth
Max-Planck-Institut f. Informatik
Im Stadtwald
6600 Saarbr"ucken, Germany
Fax: +49 681 302 5401
Keywords:
Authors!Barth, C!Code, DP, Davis Putnam, GNU GPL, KL-ONE,
Knowledge Representation, Satisfiability Problems
References:
R.E. Jeroslow and J. Wang, "Solving propositional satisfiability
problems", Annals of Mathematics and AI 1:167-187, 1990.
M. Buro and H. Kleine B"uning, "Report on a sat competition", FB 17
Mathematik/Informatik Universit"at Paderborn, Bericht Nr. 110, Reihe
Informatik, November 1992.
Last Web update on Mon Feb 13 10:24:02 1995
AI.Repository@cs.cmu.edu