From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 87881BC69 for ; Tue, 2 Oct 2007 19:13:48 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.21,220,1188770400"; d="scan'208";a="17201739" Received: from mga11.intel.com ([192.55.52.93]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Oct 2007 19:13:47 +0200 Received: from fmsmga001.fm.intel.com ([10.253.24.23]) by fmsmga102.fm.intel.com with ESMTP; 02 Oct 2007 10:13:45 -0700 X-ExtLoop1: 1 X-IronPort-AV: E=Sophos;i="4.21,220,1188802800"; d="scan'208";a="332791237" Received: from azsmsx334.amr.corp.intel.com ([10.2.121.57]) by fmsmga001.fm.intel.com with ESMTP; 02 Oct 2007 10:13:46 -0700 Received: from azsmsx343.amr.corp.intel.com ([143.182.253.5]) by azsmsx334.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.1830); Tue, 2 Oct 2007 10:13:46 -0700 Received: from [10.10.35.173] ([10.10.35.173]) by azsmsx343.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.1830); Tue, 2 Oct 2007 10:13:45 -0700 Message-ID: <47027C49.80708@intel.com> Date: Tue, 02 Oct 2007 10:13:45 -0700 From: Jim Grundy User-Agent: Mail/News 1.5.0.2 (X11/20060508) MIME-Version: 1.0 To: Denis Bueno Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Announcing The Decision Procedure Toolkit Version 1.1 References: <47027001.3070506@intel.com> <1191343440.6020.5.camel@rosella.wigram> <4702799B.9050600@intel.com> <6dbd4d000710021006n4ae35995t1acf167b569cf6c@mail.gmail.com> In-Reply-To: <6dbd4d000710021006n4ae35995t1acf167b569cf6c@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-OriginalArrivalTime: 02 Oct 2007 17:13:45.0559 (UTC) FILETIME=[96FCB670:01C80517] X-Spam: no; 0.00; translated:01 solver:01 ocaml:01 solver:01 ocaml:01 garbage:01 assertions:01 imho:01 wrote:01 wrote:01 caml-list:01 cleanly:01 implemented:02 commented:02 api:02 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 http://www.intel.com/technology/techresearch/people/bios/grundy_j.htm Key Fingerprint: 5F8B 8EEC 9355 839C D777 4D42 404A 492A AEF6 15E2