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

[Tjark Weber]

Mathias,

On Thu, 2019-01-31 at 14:00 -0800, Mathias Preiner wrote:
> On 1/31/19 1:29 PM, Tjark Weber wrote:
> > Note that this argument applies also to benchmarks that are "too hard."
> > Running a hard benchmark only to find that every solver timed out is,
> > in a sense, not very useful either. (In fact, it is worse: it probably
> > takes as long as running hundreds of trivial benchmarks.)
>
> I disagree. The SMT-COMP organizers plan to filter out easy benchmarks
> based on the results of the previous competition. However, they can't
> foresee if solvers will be able to solve hard benchmarks in the next
> competition. As solver developer you focus on benchmarks that have not
> been solved in the past.

Of course, I agree that it may be difficult in practice to identify
benchmarks that are "too hard" (without running them), and that the
fact that last year's solvers couldn't solve a benchmark is not
sufficient to conclude that the benchmark is still "too hard" this
year. So, perhaps, there is no good solution.

But the fact remains that running a benchmark on which every solver
times out has no effect on the (relative) ranking of solvers.

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