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=1.0 required=5.0 tests=AWL,SPF_NEUTRAL 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 2BEE8BC69 for ; Tue, 2 Oct 2007 19:06:07 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJMXAkdC+VLli2dsb2JhbACONQEBAQgEBg0TBQ X-IronPort-AV: E=Sophos;i="4.21,220,1188770400"; d="scan'208";a="17201500" Received: from wx-out-0506.google.com ([66.249.82.229]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Oct 2007 19:06:06 +0200 Received: by wx-out-0506.google.com with SMTP id h27so3335865wxd for ; Tue, 02 Oct 2007 10:06:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; bh=rCBrThgmAS/ZCzICUOVUGD6KXpIB/lalmkPzVqZ5npk=; b=MztvbMXBDuWRQJbsrNswy/p64R6UWmw7F5TA7kcX74nZh3tVuuC4OFmOz8Pi5HzPwNw8NUnHib6gcHbCUt7sBuDIeB+iIlwD0qk3DoHAEWi3apAY6dZVmIT5xoSORsBN8KtcZkdco/iSz7rb0CC0jJFTawToCEPtNLpI49nh8ro= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=LHHx2BnRrqPKDQgcsO8g1AeUDDRqz4m4XVqtUNsg2je0zdwsT9lD6lCruGlbtkV2wqK+mlPlTJS8BbhF9udJZt1Dltf0IYyAhSijm+q4SwXnzZheJbdTxeq+r2YZ7lWF6HGLIQ9e3ljD3HcAlG/kemBAl1kjIT9BculehHic/Rk= Received: by 10.90.105.19 with SMTP id d19mr381723agc.1191344763601; Tue, 02 Oct 2007 10:06:03 -0700 (PDT) Received: by 10.90.101.16 with HTTP; Tue, 2 Oct 2007 10:06:03 -0700 (PDT) Message-ID: <6dbd4d000710021006n4ae35995t1acf167b569cf6c@mail.gmail.com> Date: Tue, 2 Oct 2007 13:06:03 -0400 From: "Denis Bueno" To: "Jim Grundy" Subject: Re: [Caml-list] Announcing The Decision Procedure Toolkit Version 1.1 Cc: caml-list@yquem.inria.fr In-Reply-To: <4702799B.9050600@intel.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <47027001.3070506@intel.com> <1191343440.6020.5.camel@rosella.wigram> <4702799B.9050600@intel.com> X-Spam: no; 0.00; ocaml:01 solver:01 ocaml:01 solver:01 wrote:01 caml-list:01 implemented:02 aiming:03 framework:11 opposed:12 procedure:12 yet:12 version:13 toolkit:13 paper:14 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? -- Denis