DPLL = The Davis-Putnam-Logemann-Loveland backtracking algorithm for 
deciding the satisfiability of propositional logic formulae.  Modern SAT 
solvers (mini-SAT, chaff, etc) use cunning variants of DPLL - as does DPT.

DPLL(T) is an algorithm that combines a DPLL solver with a solver for 
some theory to yield a combined solver.  In the case of DPT, we have 
included a EUF solver.  EUF is the theory of equality of uninterpreted 
functions.    You can pose DPT problems propositional problems with the 
atoms are propositional variables or equations between variables and 
(uninterpreted) function applications.

DPT is completely implemented in OCaml - even the DPLL solver, and yet 
we get good (read seemingly competitive) from the tool.

All the best

Jim Grundy

skaller wrote:
> On Tue, 2007-10-02 at 09:21 -0700, Jim Grundy wrote:
>> We are pleased to announce the open source availability of the
>> Decision Procedure Toolkit (DPT).  DPT is a modern SMT solver.  This
>> release provides a MiniSAT-like DPLL solver, a DPLL(T) style theory
>> combination mechanism, and a solver for the theory of Uninterpreted
>> Functions (EUF).  The next release will add a linear arithmetic solver
>> and a cooperation mechanism for more than one theory.
> 
> Ouch .. can someone briefly explain what all that means?

-- 
Jim Grundy, Research Scientist. Intel Corporation, Strategic CAD Labs
Mail Stop RA2-451, 2501 NW 229th Ave, Hillsboro, OR 97124-5503, USA
Phone: +1 971 214-1709   Fax: +1 971 214-1771
http://www.intel.com/technology/techresearch/people/bios/grundy_j.htm
Key Fingerprint: 5F8B 8EEC 9355 839C D777  4D42 404A 492A AEF6 15E2