From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 7C4BEBB84 for ; Thu, 18 May 2006 21:30:43 +0200 (CEST) Received: from cgpsrv2.cis.mcmaster.ca (univmail.CIS.McMaster.CA [130.113.64.46]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k4IJUgT6024339 for ; Thu, 18 May 2006 21:30:43 +0200 Received: from [130.113.68.27] (account carette@univmail.cis.mcmaster.ca [130.113.68.27] verified) by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro SMTP 4.1.8) with ESMTP id 126589385; Thu, 18 May 2006 15:30:41 -0400 Message-ID: <446CCB8E.8080601@mcmaster.ca> Date: Thu, 18 May 2006 15:31:26 -0400 From: Jacques Carette Organization: McMaster University User-Agent: Mozilla Thunderbird 1.0.6 (Windows/20050716) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Xavier Leroy Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] compiler bug? References: <20060517231426.30289.qmail@web32203.mail.mud.yahoo.com> <446CABCA.8000906@inria.fr> <446CB021.6000009@mcmaster.ca> <446CB2EE.1080102@inria.fr> In-Reply-To: <446CB2EE.1080102@inria.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 446CCB62.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; compiler:01 bug:01 compilers:01 compilation:01 compiler:01 solver:01 solvers:01 algebra:01 worst-case:01 worst-case:01 solvers:01 smt:01 otc:98 wrote:01 caml-list:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Xavier Leroy wrote: >Clearly, you're not the guy who would have to support both compilers :-) > > Clearly :-). [Although I've done my time maintaining ancient software used by ~2 million users, so you only get so much sympathy from me ;-) ] >Actually, George and Appel found that compilation times with their >approach were almost reasonable (e.g. a few minutes instead of a few >seconds for a standard compiler), but they had to use a commercial ILP >solver. If only there were *really good* ILP and SAT solvers under free >licenses... > > In Computer Algebra, people use Groebner bases all the time. They have doubly-exponential worst-case complexity -- but seem to work rather well in practice. So I have stopped paying attention to worst-case; average case, when available, does matter a lot more. For ILP, I have found http://www-unix.mcs.anl.gov/otc/Guide/faq/linear-programming-faq.html#Q2 to be quite informative about current sources of "free" ILP solvers. Of particular interest are: GLPK: http://www.gnu.org/software/glpk/glpk.html lp_solve: http://groups.yahoo.com/group/lp_solve/ For SAT, things are weirder. Of course there is http://www.satlib.org/ as well as SVC http://chicory.stanford.edu/SVC/ and CVC Lite http://www.cs.nyu.edu/acsys/cvcl/ (these last 2 for SMT rather than pure SAT) which are under compatible licenses. But at http://www.qbflib.org/ and http://www.satlive.org/ there are a number of additional candidates. Of course, getting an agreement with SRI to use Yices (http://fm.csl.sri.com/yices/) would go a long way towards satisfying the "really good" requirement... Jacques