Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Announcing The Decision Procedure Toolkit Version 1.1
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-10-02 (17:13)
From: Jim Grundy <jim.d.grundy@i...>
Subject: Re: [Caml-list] Announcing The Decision Procedure Toolkit Version 1.1
We have benchmarked against MiniSAT - at little.
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 <> 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
Key Fingerprint: 5F8B 8EEC 9355 839C D777  4D42 404A 492A AEF6 15E2