Description of Tracks

The following tracks will be featured in 2020 SAT Competition.

• Main Track is the track of sequential SAT solvers. 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.
  • We encourage CaDiCaL Hack authors to participate in the Main track. A prize will be awarded to the best CaDiCaL hack.
  • This time, the Application Track will be a Crypto Track.
  • If your solver can not produce UNSAT certificates you can still participate in the No Limits Track.
• Incremental Library Track is for incremental SAT solvers.
• We will also have the Parallel Track again.
• The Cloud Track is for massively parallel SAT solvers using up to 1024 cores.

Printing a model in case of a satisfiable instance is required for all tracks. UNSAT certificates (proofs) are required only in the main tracks.

Execution Environment

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 24GB 128GB of RAM.

The Incremental Library Track will be run on computers with 2 x Intel Xeon E5430 2.66 GHz (4-Core) processors and 24GB of RAM.