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

[Gereon Kremer]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 659 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20200103/00916911/attachment.asc>