[SMT-COMP] SMT-COMP 2020 pre-announcement

[Antti Hyvärinen]

Hi Gereon,

We discussed your point, and agree that there are cases like yours where
limiting to one solver per team would be harsh.  We also agree that
defining "substantially different" seems too hard to be worth it.  In
previous years the rules have established the following:

  if the number of solver submissions is too large for the computational
  resources available to the competition, the organizers reserve the right
  not to accept multiple versions of solvers from the same solver team

so the organizers already had the discretion of not allowing multiple
versions. A good compromise might be to keep this rule but to add a
strong recommendation to it, stating that teams:

- only submit more than one entry if they are substantially different,
  as justified by an explanation to be considered by the organizers
- try to keep the number of solvers per team per category up to 2

This way it would be clear that not well motivated alternative versions
might be denied.

Cheers,
Antti, on behalf of the organising committee

On Fri, Jan 3, 2020 at 7:37 PM Gereon Kremer
<gereon.kremer at cs.rwth-aachen.de> wrote:
>
> Hi all,
>
> representing one of the solvers being impacted by change 2: while I
> understand the motivation and would support some limit, a single solver
> seems very harsh. I'd argue that it is reasonable to submit more than
> one solver, if the different solvers implement *substantially different*
> solving techniques, even if they are implemented in the same code base
> by the same team. Of course we then need to define what qualifies as
> "substantially different"...
>
> Best (and thanks for your work!), Gereon
>
> On 03.01.20 15:47, Antti Hyvärinen wrote:
> > Dear SMT-COMP participants, dear SMT-LIB community,
> >
> > We were happy to be contacted by the SMT steering committee to
> > organise the international SMT competition 2020.  The steering
> > committee specifically tasked us with finding ways of making the 2020
> > competition lighter to run in comparison to the previous editions and
> > in particular that of 2019.
> >
> > To achieve the goal while keeping the quality of the competition high,
> > we are suggesting the following changes:
> >
> > 1. Reducing the number of benchmarks to run in each division.  This
> > was already done in 2019 with a formula that resulted in 50% of
> > benchmarks being run in bigger divisions.  We plan to further decrease
> > this percentage to 40% in 2020.
> >
> > 2. Reducing the number of submissions per team per track: We plan to
> > allow a single solver per track for each solver development team.
> >
> > 3. Reducing the timeout.  In 2020 the timeout was set to 40 minutes in
> > the single-query track.  We plan to decrease this to 20 minutes in all
> > tracks.
> >
> > 4. Moving the solver submission deadline further away from the
> > workshop by two weeks.  This would put the deadline for the first
> > versions of the solvers roughly to the beginning of May 2020.
> >
> > 5. Changing the rules so that text printed to standard error will not
> > be ignored but will be combined together with standard output.
> >
> > The motivation for these changes is as follows.  Based on the data
> > from 2019, with the changes 1 and 2 in place, the number of jobs run
> > for the competition would have dropped roughly by 40% (from 781'659 to
> > 496'715).  In case that SMT-LIB grows significantly in 2020, we might
> > consider a lower percentage (while, as in 2019, favouring the new
> > benchmarks). Reducing the timeout and moving the solver submission
> > deadline makes re-running divisions in case of problems less stressful
> > for the organisers.  The reason for joining the standard input and
> > standard error is related to StarExec, and removes a possible source
> > of error where the change would have to be done manually by the
> > organisers.
> >
> > We hope that these changes will have a two-fold positive effect on the
> > competition: keep the quality of the competition high; and allow
> > further development of the competition concept by giving more time to
> > the current and future organisers for planning for improvements.
> >
> > We would be happy to receive community's feedback on the suggestions!
> >
> > Best regards,
> >
> > Haniel Barbosa, Jochen Hoenicke, and Antti Hyvärinen (chair)
> > _______________________________________________
> > SMT-COMP mailing list
> > SMT-COMP at cs.nyu.edu
> > https://cs.nyu.edu/mailman/listinfo/smt-comp
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp