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

[Tjark Weber]

======================================================================

    12th International Satisfiability Modulo Theories Competition
                            (SMT-COMP'17)

                            July 23, 2017
                         Heidelberg, Germany

                          CALL FOR COMMENTS
                         CALL FOR BENCHMARKS
                     PRELIMINARY CALL FOR SOLVERS

======================================================================

SMT-COMP is the annual competition among Satisfiability Modulo Theories
(SMT) solvers. The goals of SMT-COMP are to spur solver advances,
collect benchmarks, and encourage adoption of the SMT-LIB standard,
through friendly competition.

SMT-COMP'17 will end in time to be described and the results announced
at the SMT Workshop (July 22-23), which is affiliated with the
International Conference on Computer-Aided Verification (CAV 2017).

SMT-COMP'17 is organized under the direction of the SMT Steering
committee. The organizing team for SMT-COMP'17 is

    . Matthias Heizmann - University of Freiburg, Germany
    . Giles Reger       - University of Manchester, UK
    . Tjark Weber       - Uppsala University, Sweden

This is a call for three things:


CALL FOR COMMENTS: 

The organizing team is preparing the schedule and rules for 2017.
Any comments you may have to improve the competition over past years
or to redirect its focus are welcome and will be considered by the
team. We particularly appreciate comments received until

    *** March 31, 2017. ***

For SMT-COMP'17, we are especially interested in comments regarding:

- Benchmarks with unknown status: Previous SMT-COMPs have only used
  benchmarks whose status (sat/unsat) was known. One might argue that
  this favors imitation of existing solvers over innovation. Should
  benchmarks with unknown status be used in the competition? If so,
  how should answers for such benchmarks be scored? Can scoring for
  one solver remain independent of the answers given by other solvers,
  or should disagreements between solvers lead to negative scores for
  a solver?

- Benchmark weighting: To avoid over-representation of certain (large)
  benchmark families, a weighting scheme for benchmarks was introduced
  in 2016. This causes division scores to be real numbers rather than
  simply an integer indicating the number of benchmarks solved, and
  the winning solver in a division is (intentionally) no longer
  necessarily the solver that solved the largest number of benchmarks.
  Do the methodological benefits of this weighting scheme justify the
  increased complexity in interpreting division scores?

- Scope: The new (draft) version 2.6 of the SMT-LIB standard includes
  support for algebraic datatypes. Are corresponding benchmarks and
  sufficiently stable solver implementations available for SMT-COMP to
  feature an (experimental) datatype division in 2017? Should the
  scope or emphasis of the competition be adapted in other ways?


CALL FOR BENCHMARKS:

The competition is enhanced by new sets of benchmarks to add to those
already in use (and used in past competitions). A selection of
benchmarks in various categories is used for the competition (according
to rules that are currently being revised).

If you have benchmarks that you think would be useful to SMT-LIB and
SMT-COMP (and may be made public), please let us know as soon as
possible, even if the material is not quite ready. We will work in
close cooperation with the SMT-LIB maintainers to integrate such
benchmarks into the SMT-LIB in time to be taken into account for the
competition. The deadline for benchmarks to be used in the 2017
competition will be announced when the schedule and rules are
finalized.


PRELIMINARY CALL FOR SOLVERS:

A submission deadline for solvers will be announced along with the
rules. However, it is useful to the organizing team to know in advance
which and how many solvers may be entering. Thus we request that you
let us know at your earliest convenience if you think you may be
submitting one or more solvers to SMT-COMP'17; particularly if you
have not submitted a solver before, or if you think there may be
unusual circumstances.


COMMUNICATION:

The competition web-site will be at www.smtcomp.org.

Public email regarding the competition may be sent to
smt-comp at cs.nyu.edu.

Announcements will be sent on both smt-comp at cs.nyu.edu and
smt-lib at cs.nyu.edu.

Non-confidential email to the organizers may be sent to
smtcomp-discussion at lists.sourceforge.net.

Sincerely,
The organizing team