CMU Artificial Intelligence Repository
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
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
[Note: Email address probably obsolete. --mk]
Authors!Pehoushek, Lisp!Math, Math, Quine Tree Algorithm,
Last Web update on Mon Feb 13 10:30:26 1995