Competition Tracks

Main Track

Main track is the track for sequential SAT solvers. All sequential tracks will be run on the HoreKa Blue Instance of NHR@KIT in Karlsruhe using compute nodes with 76 cores Intel Xeon Platinum 8368 CPU running 8 benchmarks in parallel. Consider the general submission guidelines and the submission instructions. We will use 300-600 benchmark problems. 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 executed with a time limit of 5000 seconds and memory limit of 32GB. All solvers participating in the Main track are required to provide certificates in both SAT and UNSAT cases. We offer to choose from different proof checkers. For more information about the UNSAT certificates see this page.

Experimental Track

If your solver uses techniques that are not yet supported by certificate generation, you can submit it to the Experimental Track. Submissions to the Experimental Track must outperform any of the top three solvers of the Main track to receive an award.

Sub-Tracks for AI-Generated and AI-Tuned Solvers

There are separate subcategories for AI-generated and AI-tuned solvers in each of the Main, Experimental, Parallel, and Cloud tracks. The same rules and limitations that apply to each track also apply to solvers flagged as AI-generated and/or AI-tuned. However, these solvers are not eligible for regular track prizes. An award will be given to the best AI-tuned and AI-generated solver in each track.

Parallel and Cloud Tracks

(Updated) The Parallel and Cloud tracks will be run on Amazon Web Services (AWS). Consider the general submission guidelines and the AWS submission instructions. All solvers participating in the Parallel and Cloud tracks are required to provide a model in the SAT case. Parallel solvers will be executed with a wall-clock time limit of 1000 seconds. Each parallel solver will be run an a single AWS machine of the type m6i.16xlarge, which has 64 virtual cores (32 physical cores) and 256GB of memory. More details about m6i.16xlarge nodes can be found here. Cloud solvers will evaluate the effectiveness of parallel SAT solvers run in a distributed manner. Cloud track solvers will be executed with a wall-clock time limit of 200 seconds running on 100 m6i.4xlarge machines in parallel. Each m6i.4xlarge machine has 16 virtual CPUs (8 physical CPUs) and 64 GB memory. Communication between the machines is possible using MPI and SSH.