[Caml-list] Announcing The Decision Procedure Toolkit Version 1.1
Jim Grundy
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.
DPT is an open source project licensed under the Apache 2.0 license.
You can download DPT from sourceforge:
http://sourceforge.net/projects/dpt
DPT is intended to serve as a platform for experiments in SMT solvers
and their applications. Subsequent releases will include features
like model generation, proof production and interpolants. We also
expect to support parametric theories and the HOL logic.
The DPT design philosophy emphasizes flexible interfaces and
transparent implementation over raw speed. DPT is implemented in
OCaml. These decisions not withstanding, speed is good, and so we
have made a reasonable effort to ensure DPT is fast.
Further announcements about DPT will be made on the dpt-announce mailing
list. You can subscribe to the list via the project web site.
Kind regards,
Amit Goel, Jim Grundy and Sava Krstic
--
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
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
skaller
> 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?
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
Jim Grundy
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
_______________________________________________
Denis Bueno
> DPT is completely implemented in OCaml - even the DPLL solver, and yet
> we get good (read seemingly competitive) from the tool.
Have you benchmarked against Minisat? Is DPT a re-implementation of
the Minisat paper using OCaml, or is simply a solver in the DPLL
framework as opposed to a solver aiming to mimic Minisat?
--
Denis
Jim Grundy
Naturally MiniSAT is faster. For problems that combine SAT reasoning
with theory reasoning then the extra SAT performance doesn't all get
translated into extra combined theory solving performance - hence our
overall performance is not too shabby.
Our SAT solver is very much MiniSAT like, but with some extra features
and a more open API to better facilitate it's use in a collaborative
solving tool. The code is very cleanly written (IMHO), commented, and
heavy with assertions. It may serve as a good starting place for someone
wishing to learn about how MiniSAT like algorithms work.
Our SAT performance - on a few selected benchmarks we have tried - is
about 1/2 - 1/3 of MiniSAT. If you start playing with the garbage
collection tuning, which we have yet to experiment much with, you seem
to be able to get better than 1/3.
Denis Bueno wrote:
> On 10/2/07, Jim Grundy <jim.d....@intel.com> wrote:
>> DPT is completely implemented in OCaml - even the DPLL solver, and yet
>> we get good (read seemingly competitive) from the tool.
>
> Have you benchmarked against Minisat? Is DPT a re-implementation of
> the Minisat paper using OCaml, or is simply a solver in the DPLL
> framework as opposed to a solver aiming to mimic Minisat?
>
--
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
_______________________________________________