[SMT-COMP] SMT-COMP 2016: Benchmarks in 2.0 and 2.5 Formats

[Clark Barrett]

I can take some blame for not making a greater effort to determine unknown
statuses.  We made a huge effort after the 2014 competition and it was
quite a lot of work to get that reflected in starexec.  Unfortunately, I
did not have time to do that this year.

I think that getting the community to help more in the future is a great
idea.  For existing benchmarks, let me suggest two kinds of evidence I
would accept from the community for changing benchmark statuses:
1. Two established SMT solvers agree on the new status (perhaps after a run
with a very long timeout).
2. There is some independently-checkable evidence for the new status (i.e.
a model for a sat benchmark or a verifiable proof certificate for an unsat
benchmark).

For new benchmarks, I agree it would be good to release them sooner.
Sometimes the benchmarks are only submitted at the last moment, so this is
not always possible.

-Clark

On Thu, May 26, 2016 at 12:03 PM, Tjark Weber <tjark.weber at it.uu.se> wrote:

> Dejan,
>
> On Thu, 2016-05-26 at 17:47 +0000, Dejan Jovanović wrote:
> > Can you please give the final word on this. Will only the "known"
> > benchmarks be used in the competition?
>
> Yes. The competition rules are quite clear that benchmarks with unknown
> status will not be used. This has been established practice of SMT-COMP
> for a long time, and as mentioned earlier, I do not believe it would be
> appropriate to change this on short notice. The implications of such a
> change for the size of the competition, for the competition tools and
> its scoring rules are non-trivial and deserve careful consideration.
>
> Of course, the performance of solvers on benchmarks with unknown status
> is still of interest. If there is sufficient time after we've run the
> competition jobs, we may make an attempt to determine it and report our
> findings at the SMT Workshop in addition to the competition results.
>
> If I am involved in organizing SMT-COMP again in 2017, I would aim to
> incorporate benchmarks with unknown status in a more systematic manner
> then.
>
> Best,
> Tjark
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>