Re: [Caml-list] compiler bug?

[Jacques Carette <carette@mcmaster.ca>]

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