SMT-COMP Parallel and Cloud Tracks

[Antti Hyvärinen]

* SMT-COMP Cloud and Parallel Tracks *

This year we are planning new, experimental, cloud and parallel tracks
for SMT-COMP. Similar tracks were organised in the SAT competition 2020
and to our understanding the competition had a positive impact on the
development of parallel SAT solvers (see
https://satcompetition.github.io/2020/).

The goal in both the cloud and the parallel tracks will be to measure
the success of a solver in solving a single, hard instance. This will be
done by giving solvers instances one at a time, similar to the SMT-COMP
single-query track. The participating solvers will be scored based on
the number of instances that a solver solves within the per-instance
wall-clock time limit and the total run time, similar to the
single-query track’s parallel score.

For these tracks we need to choose in total 400 benchmarks from the
single-query track logics, and we are specifically reaching out to you,
the community and especially the competitors, for suggesting suitable
instances to be included in the tracks. In addition we will try to
identify instances that are considered interesting.

The solver submission rules follow those of the rest of the tracks.
However, on this track we do accept portfolio solvers, as defined in the
rules, as competitors. We encourage submission of non-portfolio solvers
and reserve the right to give special mentions to non-portfolio solvers
in reporting the results.

While the standard competition will be run in StarExec, the parallel and
cloud tracks will be run on Amazon Web Services. AWS has kindly agreed
to sponsor the participants in the testing phase.

* Cloud Track *

The Cloud Track evaluates the effectiveness of parallel SMT solvers to
run in a distributed manner. The solvers participating in this track
will be executed with a wall-clock time limit of 20 minutes running on
100 m4.4xlarge machines in parallel. Each m4.4xlarge machine has 16
virtual CPUs and 64 GB memory. Communication between the machines
is possible using MPI and SSH.

Participants of this track are required to submit their solver via a
GitHub repository (which can be private). The repository should contain
a docker file that compiles the solver. As an example, scripts for
account configuration and instructions to run HordeSAT in the default
configuration are available at
https://github.com/aws-samples/aws-batch-comp-infrastructure-sample.

* Parallel Track *

The solvers participating in this track will be executed with a
wall-clock time limit of 20 minutes, thus similar to the Single Query
Track. Each solver will be run on a single AWS machine of the type
m4.16xlarge, which has 64 virtual cores and 256GB of memory. More
details about m4.16xlarge nodes can be found in
https://aws.amazon.com/about-aws/whats-new/2016/09/introducing-new-m4-instance-size-m4-16xlarge-and-new-region-availability-of-m4-instances/.

Similar to the Cloud Track, participants of this track are required to
submit their solver via a GitHub repository (which can be private). The
repository should contain a docker file that compiles the solver.

* Solver Submission to Parallel and Cloud Tracks *

In order to participate in the Cloud or Parallel Track please send an
email to smt-co...@amazon.com containing the following:

1. name of the solver and a list of the authors
2. your AWS account number
3. the URL of the GitHub repository including the branch
4. the full, 40-character SHA-1 hash of the commit

Sincerely,

The organizing team

Haniel Barbosa
Jochen Hoenicke (chair)
Antti Hyvarinen

[Antti Hyvärinen]

Dear all,

Because of some technical issues we have decided to change the email
alias to a domain outside of amazon. From now on, please contact us
at

aws-smt-...@googlegroups.com

Best regards,

The organizing team

Haniel Barbosa
Jochen Hoenicke (chair)

Antti Hyvärinen