[SMT-COMP] Scoring rules in the draft SMT-COMP 2015 rules

[David R. Cok]

SMT organizers and competitors:

I note a (minor) change from previous practice in the draft rules for 
SMTCOMP 2015. In previous competitions the accumulated time used for 
comparison among solvers was the total of the times for all benchmarks 
solved correctly. In the 2015 rules, the measured time includes the time 
taken to produce 'unknown' answers (and wrong answers, though that 
aspect is likely immaterial).

I favor this change. Indeed, from a user's point of view, if a tool is 
eventually going to report unknown it is better to do so sooner rather 
than later (though unknown results with a candidate model are still 
useful). In the competition ranking, the change is only significant if 
there is a tie in the numbers of benchmarks in the erroneous result, 
correct result, and unknown result categories, and not all the 
benchmarks are solved - which is not a likely scenario. Despite that, 
including the time to produce an unknown result gives, IMHO, a better 
measure of a solver's performance.

If the organizers intended this change, I think it ought to be 
explicitly mentioned as a difference in 2015 (in section 3, perhaps). If 
they did not, then the discussion of scoring needs a slight modification.

- David

On 5/11/2015 9:54 AM, Tjark Weber wrote:
> The revised (draft) rules for SMT-COMP 2015 are now available on the
> competition website: http://smtcomp.sourceforge.net/2015/rules15.pdf
>
> These rules are open for comment through Sunday, May 17.
>
> The overall shape of the competition remains unchanged from last year.
> However, we have simplified and slightly altered the rules with regard
> to several important points, including
>
> - parallel performance,
> - competition-wide ranking,
> - floating-point divisions, and
> - benchmark selection.
>
> We received several new benchmarks, including new floating-point
> benchmarks. Thanks to all contributors! More details on the size and
> content of the benchmark set will be provided once the new benchmarks
> have been curated and entered into SMT-LIB.
>
> Current deadlines are
>
>     June 1 for first versions of solvers
>     June 14 for final versions of solvers
>
> Earlier (non-binding) indications of intention to enter a solver in the
> competition are appreciated by the organizers.
>
> Tjark Weber
> for the organizers
>
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp