Re: [Caml-list] Announcing The Decision Procedure Toolkit Version 1.1

[Jim Grundy <jim.d.grundy@intel.com>]

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 <jim.d.grundy@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