Competition Tracks
The Main track as well as its subtracks will be run on the StarExec cluster. The time limit for solving an instance will be 5000 seconds (in each track). The solvers will be allowed to use up to 128GB of RAM.
Printing a model in case of a satisfiable instance is required for all tracks. UNSAT certificates (proofs) are required only in the main tracks.
Anniversary Track
International competitions for SAT solvers have a long tradition. The first sporadic events took place in the 1990s (Paderborn 1992, DIMACS 1993, and Beijing 1996). In 2002, Edward A. Hirsch, Daniel Le Berre, and Laurent Simon initiated a series of regularly scheduled competitions: the SAT Competition as we know it. Today, we can look back on 20 years of exciting public evaluations and award ceremonies; 20 years of SAT competitions that testify to the tremendous scientific progress made in SAT solving.
We celebrate the 20th anniversary of this event series in the form of a special Anniversary track. The benchmarks for this track will be comprised of all benchmark instances which have been used in Application, Crafted, and Main Tracks of previous SAT competitions.
There will be three categories of this track, one each for Main track, Parallel track and Cloud track solvers. Participants can submit a maximum of two solvers to the Main category of this track, and one solver for each of the Parallel and Cloud categories. We particularly welcome you to also submit solvers or configurations which are tailored to specific instance types.
All submissions to the Anniversary track have to be open source. Solvers which contain code which could be perceived as instance-specific branching or a result-lookup table will be disqualified. If you are unsure whether your solver meets these requirements, please feel free to contact us.
Main Track
Main track is the track for sequential SAT solvers. This track 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. 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.CaDiCaL 1.4.1 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 newly released CaDiCaL 1.4.1. These sources include a comfortable script for preparing the submission for StarExec. In order to qualify as a CaDiCaL Hack, the diff between the patched and modified sources of CaDiCaL 1.4.1 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 UNSAT proofs 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.