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

[Tinelli, Cesare]

Dear all,

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