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 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr 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 C00BEBC69 for ; Tue, 2 Oct 2007 19:02:23 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.21,220,1188770400"; d="scan'208";a="17201357" Received: from mga02.intel.com ([134.134.136.20]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Oct 2007 19:02:23 +0200 Received: from orsmga001.jf.intel.com ([10.7.209.18]) by orsmga101.jf.intel.com with ESMTP; 02 Oct 2007 10:02:20 -0700 X-ExtLoop1: 1 X-IronPort-AV: E=Sophos;i="4.21,220,1188802800"; d="scan'208";a="237873578" Received: from azsmsx333.ch.intel.com (HELO azsmsx333.amr.corp.intel.com) ([10.2.121.77]) by orsmga001.jf.intel.com with ESMTP; 02 Oct 2007 10:02:19 -0700 Received: from azsmsx343.amr.corp.intel.com ([143.182.253.5]) by azsmsx333.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.1830); Tue, 2 Oct 2007 10:02:21 -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:02:20 -0700 Message-ID: <4702799B.9050600@intel.com> Date: Tue, 02 Oct 2007 10:02:19 -0700 From: Jim Grundy User-Agent: Mail/News 1.5.0.2 (X11/20060508) MIME-Version: 1.0 To: skaller 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> In-Reply-To: <1191343440.6020.5.camel@rosella.wigram> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-OriginalArrivalTime: 02 Oct 2007 17:02:20.0346 (UTC) FILETIME=[FE9181A0:01C80515] X-Spam: no; 0.00; backtracking:01 solvers:01 variants:01 solver:01 solver:01 ocaml:01 smt:01 chaff:98 atoms:98 equality:01 wrote:01 wrote:01 caml-list:01 functions:01 functions:01 DPLL = The Davis-Putnam-Logemann-Loveland backtracking algorithm for 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