[SMT-COMP] Results

[Tjark Weber]

On Sun, 2019-07-07 at 14:43 -0700, Aina Niemetz wrote:
> the results of SMT-COMP 2019 are available at
> https://smt-comp.github.io/2019/results.html

With the 2019 competition results available, now might be a good time
to think about portfolio solvers (aka wrapper tools). These have been
allowed in the competition for a long time but no portfolio solvers
were actually submitted in recent years.

This year, I submitted a simple portfolio solver (Par4) that performed
rather well in many of the divisions into which it was entered. I
probably spent far less time on this solver than the developers of the
wrapped tools spent on their solvers. Credit to them! If people start
developing portfolio solvers in earnest, it might become difficult in
the future to win any division with anything but a portfolio approach.

There are different options for how portfolio solvers could be treated
in future competitions: run them like any other solver; rank them
separately from ordinary solvers; run them hors concours; or do not
allow them at all. Perhaps we should have a discussion to identify
which of these options would be most beneficial to the competition and
to progress in SMT solving in general.

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