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

[Andres Noetzli]

> 
>>  they just make the gap between solvers (in terms of % of problems
>>  solved) smaller e.g. if 90% of benchmarks are ‘uninteresting’ 
>> then the
>>  gap between solvers is about an order of magnitude smaller than it
>>  would be if those benchmarks were removed. Solving an extra 50
>>  problems
>>  out of a set of 500 is a more clear success than out of a set of
>>  50000.
> 
> True, but it is not immediately clear to me that this gives a more
> accurate picture. Of course, absolute numbers mean little without
> context, but I feel vaguely reminded of
> https://en.wikipedia.org/wiki/Misleading_graph#Truncated_graph

One way to sidestep this problem (or at least to think about it 
differently)
is to focus on timeouts instead of solved instances. One could imagine
to (negatively) score the number of timeouts instead of counting
the number of solved instances. In that case, it doesn't matter how 
many of
the commonly solved instances you remove.

-Andres