CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

QUINE: Quine Tree algorithm for satisfiability

A satisfiability program implemented in Common Lisp. It is supposed to work on any boolean expression, but was mainly designed for 3sat. If you use a propositional inference engine in your work, this program is probably faster in a majority of cases. On Mitchell, Selman, Levesque hard spot problems, the program takes from 1 minute to 15 minutes on 150 variable instances, including unsatisfiable instances, averaging under 10 minutes. The program appears to run in time N*2^(N/22) on MSL hard spot instances.

   comp.lang.lisp 1-DEC-92 post by Dan Pehoushek

Version: 1-DEC-92 Copying: Use, copying, modification, and distribution permitted. If you do anything with the program, Dan would be interested in receiving a quick summary. Also, if you let him know that you are using it, he may be able to send you patches, upgrades, etc. CD-ROM: Prime Time Freeware for AI, Issue 1-1 Author(s): Dan Pehoushek Computer Science Department Stanford University [Note: Email address probably obsolete. --mk] Keywords: Authors!Pehoushek, Lisp!Math, Math, Quine Tree Algorithm, Satisfiability, Stanford References: ?
Last Web update on Mon Feb 13 10:30:26 1995