SMT-Comp 2024 - AWS credits

9 views

Skip to first unread message

Martin Bromberger

unread,

May 23, 2024, 9:45:15 AM5/23/24

to smt-...@cs.nyu.edu, smt...@googlegroups.com, smt-an...@googlegroups.com, aws-smtc...@googlegroups.com

If you plan to participate in SMT-Comp 2024 parallel or cloud tracks, this email is for you. Again this year, the parallel and cloud tracks will be run on AWS. Ben Jones, Karo Antonyan, and I are handling the AWS side.

I’m pleased to let you know that AWS has again agreed to provide AWS credit for use as you prepare your solvers. The credits must be requested, and are applied on a per-account basis. So far, we’ve received only one request for SMT-Comp.

This year, the internal AWS approval loop has been longer; you should plan on at least a week between request and credit appearing in your account. We want you to have time to use the credits, so we encourage you to apply now. All you need to do is reply to this email (only to me) with the following:

Name
e-mail (needs to be affiliated with an academic institution to be eligible for AWS credit)
University
Sponsoring faculty/staff member and their email
AWS account number where the credit will be used

An important note: After discussion with some of the participants, we are changing the timeout back to 1200s for the parallel and cloud tracks. The starter kit for parallel and cloud tracks is here; the interface is the same as last year.

As a reminder, these are the deadlines:

May 27 - Deadline for first versions of participating solvers (for all tracks), including preliminary system descriptions
June 8 - Deadline for final versions of participating solvers, including final system descriptions

If the final date is a hardship, please contact us ASAP. If we receive multiple requests, we will consider pushing the date back. This would only apply for the parallel and cloud tracks.

Make sure we (Robert Jones, Ben Jones, and Karo Antonyan) can access the github repository containing the solver. If you make it public at submission time then it is easy. If not, then please add us: (rbtjones-aws, benjaminfjones, kantonya-aws) as readers of the repository.
Provide a branch / commit hash from the repository that we should use for building your solver.
Provide instructions on how to build your solver into one Docker container (for parallel) or two Docker containers (for cloud). A single command build script, if possible, is greatly appreciated!
It is expected that the competition solver will not require command line arguments other than the file to execute. Please configure your solver appropriately for the competition.

We will contact you about our progress with your solver at two stages:

When we have built your solver
When we have run initial tests

If we have trouble at either of these two points, we will attempt to work with you to resolve any issues.

Please reach out with any questions. We look forward to seeing your solvers in action!