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. For more information about the UNSAT certificates see this page.Opportunity to choose from several different proof checkers
For the first time in the history of SAT Competitions, we will offer to choose from different proof checkers. At the time of writing, we received two proposals for verified proof checkers. Note that, among those DPR / LPR is the only checker using a system which is different from the traditional DRAT.CaDiCaL 1.5.3 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.5.3. In order to qualify as a CaDiCaL Hack, the diff between the patched and modified sources of CaDiCaL 1.5.3 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 SAT or UNSAT certificates or if you do not want to publish your source code, you can still submit your solver to the No-Limits track.Each solver submitted to the Main track will automatically participate in the No-Limits track.
The No-Limits track will only be evaluated with respect to the new benchmarks instances which are submitted to this SAT Competition.