[SMT-COMP] SMT-COMP'20 preliminary call for solvers

[Antti Hyvärinen]

PRELIMINARY CALL FOR SOLVERS:

A submission deadline for solvers will be announced along with the
rules.  However, it is useful for the organizing team to know in advance
which and how many solvers may be entering.  If you have not submitted a
solver before, or if you think there may be unusual circumstances, we
request that you let us know at your earliest convenience if you think
you may be submitting a solver to SMT-COMP'20.  We require a system
description for all submitted solvers as part of the submission of the
final solver versions.

We have two central changes to the call for solvers with respect to
previous years: the ban for portfolio solvers, and a limit on the number
of solvers that a team may submit.  Both are elaborated below.

FORBIDDING PORTFOLIO SOLVERS

This year we explicitly forbid the submission of so-called portfolio
solvers as competition entries.  We acknowledge that judging what
constitutes a portfolio SMT solver is difficult.  However, we are not
the first in history to face a similar challenge, and plan to apply an
equally historical approach where we write down a “law”, act as its
“judges”, and have a few “precedents”.

Here we define a portfolio solver as “a solver using a combination of
two or more sub-solvers, developed by different groups of authors, on
the same component or abstraction of the input problem.” For example, a
solver using one subsolver to solve the ground abstraction of a
quantified problem is allowed, while a solver using two or more
subsolvers from different groups of authors is not.

As to the precedents, we would have judged the 2019 competition entry
Par4 (https://smt-comp.github.io/2019/system-descriptions/Par4.pdf) as a
portfolio solver, and Vampire
(https://smt-comp.github.io/2019/system-descriptions/vampire.pdf) as not
a portfolio solver.

If you think a solver you plan to submit would be judged as a portfolio
solver, please contact us beforehand to avoid unnecessary complications.

LIMIT ON THE NUMBER OF SOLVERS

This year solver development teams may only submit more than one entry
if they are substantially different.  A justification must be provided
for the difference.  We strongly encourage the teams to keep the number
of solvers per team per category at at most two.  The idea in allowing
up to two submissions is to encourage the development of new,
experimental techniques by allowing an “alternative solver” to be
submitted while keeping the competition manageable.

We’re looking forward to an interesting competition this year, and
welcome any comments to this call for solvers.

Sincerely,

The organizing team

Haniel Barbosa, Universidade Federal de Minas Gerais, Brazil
Jochen Hoenicke, Albert-Ludwigs-Universität Freiburg, Germany
Antti Hyvärinen (chair), Università della Svizzera italiana, Switzerland