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

[Bruno Dutertre]

On 05/26/2016 12:03 PM, Tjark Weber 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.
>

That's indeed been the practice, but, in earlier years, the organizers
typically tried to find the status of benchmarks (especially new ones)
before the competition. Maybe that's not so easy now, but the community
could help if the benchmarks were released earlier.

Also, in the past, we didn't have star-exec and the competition was
run on a randomly selected (and smallish) subset. Now that it is
possible to run on a large set of benchmarks within reasonable time,
I don't see why it would be so hard to run on all.  I understand that
there are rules and constraints, but if the competitors agree
and there's enough time, why not?

Bruno

> 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
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4049 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-comp/attachments/20160526/7dde86a2/attachment-0001.p7s>