[SMT-LIB] Fwd: An alternative to SMT-COMP?

[geoff at cs.miami.edu]

Hi Cesare, all,

This sounds very similar to the TSTP and the associated statistics, problem
ratings, and system ratings. I find the data that emerges from such an
evaluation useful for recommending systems to users, and finding unique
capabilities of the various systems.

Cheers,

Geoff

> As a follow up to my previous message about the future of SMT-COMP, there
> have been a few suggestions recently to have a different kind of event
> altogether: a comparative evaluation, let's call it SMT-EVAL, instead of a
> competition.
> 
> This would be a non-live effort aimed at comparing solvers more thoroughly
> by running them on a much larger set of benchmarks and exploring several
> features and options for each solver, with the goal of getting a broader
> and more accurate picture of the state of the art.
> SMT-EVAL would perhaps not require official solver submissions and focus
> instead on publicly available solvers.
> 
> The evaluation would clearly be a major endeavor and require a lot of work
> and a committed team of people. On the positive side, it would span a
> longer period of time, not have the sort of pressure and stress associated
> with a live competition, and for being more research oriented, could more
> easily lead to publications. Last but not least, the team in charge of it
> would benefit from the use of the StarExec execution service to run the
> experiments (see http://www.starexec.org/starexec/public/about.jsp).
> StarExec is going live soon and will be initially available only to a
> couple of logic solver communities, with SMT being one of them.
> 
> The evaluation could be timed to end before SMT'13, which is expected to be
> in conjunction with SAT next year, so that its results could be presented
> there in lieu of the competition results.
> 
> David Cok would be willing to be part of the evaluation team if SMT-EVAL
> replaced SMT-COMP next year. Aaron Stump has expressed a strong interest in
> being in the team too, both for its research aspects and because it would
> be a great stress test for StarExec. They both think that at least another
> person would be needed.
> I would add that it might be good if all the members of the team were not
> solver developers, to avoid any possible conflicts of interest.
> 
> What do you think of the idea of SMT-EVAL as a replacement for SMT-COMP in
> 2013?
> 
> Cheers,
> 
> 
> Cesare
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264
----- "My cat" is not a float. Every string should learn to swim. ------