Competition Tracks

Main Track

Main track is the track for sequential SAT solvers. This track as well as its subtracks will be run on the StarExec cluster. Consider the general submission guidelines and the StarExec submission instructions. We will use 300-600 benchmark problems, the time limit will be 5000 seconds. Solvers in all tracks will be ranked based on the PAR-2 score, which is the sum of the runtime plus twice the timeout for unsolved instances. The solvers will be allowed to use up to 128GB of RAM. All solvers participating in the Main track are required to provide certificates in both SAT and UNSAT cases. Like last year, we will offer to choose from different proof checkers. For more information about the UNSAT certificates see this page.

CaDiCaL 1.9.4 Hacks

We encourage CaDiCaL Hack authors to participate in the Main track. A prize will be awarded to the best CaDiCaL hack.

Hack tracks have been part of many SAT Competition since 2009. The motivation of hack tracks is two-fold. On the one hand, we want to lower the threshold for Master and PhD students to enter the SAT Competition with new and innovative ideas. On the other hand, the aim is to see how far the performance of CaDiCaL can be improved by making only minor changes to its source code. Competing with minor hacks helps the community to isolate the actual causes of improvements. Thus, we strongly encourage all participants of the Main track (including non-students) to participate with a "hacked" CaDiCaL solver.

Participants in the CaDiCaL Hack track should use the source of the release version of CaDiCaL 1.9.4. In order to qualify as a CaDiCaL Hack, the diff between the patched and modified sources of CaDiCaL 1.9.4 has to be less than 1000 non-space characters. You can use our edit distance tool on all modified files to count the number of modifications.

No-limits Track

If your solver does not generate result certificates or if the source code of your solver can not be public, you can submit your solver to the No-limits track. Submissions to the No-limits track will only be evaluated on the new benchmark instances submitted to this SAT competition and must outperform the top three solvers of the Main track on those instances to receive an award.

Parallel Track

The Parallel track will be run on Amazon Web Services (AWS). Consider the general submission guidelines and the AWS submission instructions. All solvers participating in the Parallel track are required to provide a model in the SAT case. The solvers participating in this track will be executed with a wall-clock time limit of 5000 seconds. Each solver will be run an a single AWS machine of the type m6i.16xlarge, which has 64 virtual cores and 256GB of memory. More details about m6i.16xlarge nodes can be found here.

Cloud Track

The Cloud track will evaluate the effectiveness of parallel SAT solvers to run in a distributed manner. This track will be run on Amazon Web Services(AWS). Consider the general submission guidelines and the AWS submission instructions. All solvers participating in the Cloud track are required to provide a model in the SAT case. The solvers participating in this track will be executed with a wall-clock time limit of 1000 seconds running on 100 m6i.4xlarge machines in parallel. Each m6i.4xlarge machine has 16 virtual CPUs and 64 GB memory. Communication between the machines is possible using MPI and SSH.