[SMT-COMP] SMT-COMP 2019: Call for Comments, Benchmarks, Solvers

[Tjark Weber]

On Thu, 2019-01-31 at 13:36 +0000, Giles Reger wrote:
> As a further point to the scoring comments, which I agree with, it’s
> really best to avoid making the score reliant on the performance of
> other solvers [...]

I concur. Independence of a solver's score from the performance of
other solvers has been an important criterion for past scoring schemes;
both for simplicity and to avoid susceptibility to manipulation (by
submitting solvers with certain behavior).

> One question here is whether we need an overall ranking at all. As you
> point out Tjark, not all divisions are `equal' but the relative
> importance of divisions is not always clear. As organisers we had
> discussed trying to merge divisions into larger entities such that we
> could reward fewer awards but we could not find any sensible larger
> grouping of divisions that could be properly justified from a pragmatic
> perspective. Given that the competition aims to encourage new
> developments, the awards should be associated with things we think that
> solver developers should be concentrating on. What’s unclear to me is
> whether we should be encouraging ‘general’ solvers able to handle all
> logics (or larger groups of logics) rather than ‘specialist’ solvers
> focussed on one or two logics - the notion of a global winner
> encourages general solvers.

The competition-wide ranking was introduced for the 2014 FLoC Olympic
Games (mainly as a criterion to award some of the Kurt Gödel medals).
Based on various conversations with competitors and users I got the
impression that the ranking was popular. People seemed to have a strong
preference for an (apparently) simple, one-dimensional ranking scheme,
and so it was retained.

But it was always clear (to me at least) that the competition-wide
ranking was of limited informative value, and that anyone looking for
performance in a specific logic should look at the respective division
ranking instead. In that sense, the competition-wide ranking was never
meant to devalue the achievements of "specialist" solvers in individual
divisions.

Best,
Tjark









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy