is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the and stands in the tradition of the yearly SAT Competitions and SAT-Races / Challenges.
- [21.04.2022] Parallel and Cloud track solvers sources are now archived and available in the downloads section (unfortunatly not all submissions repositories were still online)
- [27.08.2021] The Proceedings of SAT Competition 2021 are now available
- [12.07.2021] Reuploaded results CSV
- Replaced all magic numbers >10000 by strings carrying their semantics: "memout", "timeout"
- Removed data for disqualified solvers
- Fixed scores of VBSs
- [12.07.2021] The Cloud track results presented were incorrectly evaluated with respect to a 5000 seconds timeout (instead of 1000 seconds as announced). This has now been corrected in the results section and a corrected set of slides is available in the downloads section. Unfortunately, this has led to a change in the third-placed cloud solver.
- [10.07.2021] The benchmarks and sequential solvers are now available in the downloads section
- [10.07.2021] The detailed results per track are now available in the results section
The area of SAT Solving has seen tremendous progress over the last years. Many problems (e.g. in hardware and software verification) that seemed to be completely out of reach a decade ago can now be handled routinely. Besides new algorithms and better heuristics, refined implementation techniques turned out to be vital for this success.
To keep up the driving force in improving SAT solvers, we want to motivate implementors to present their work to a broader audience and to compare it with that of others.
will consist of the following tracks*:
- Main Track (with No-Limits and CaDiCaL-Hack sub-tracks)
- Application Track: Cryptography
- Incremental Library Track
- Parallel Track
- Cloud Track
* Tracks with less than 3 participants will be canceled.
|Registration Opens:||March 1|
|Benchmark Submission Deadline|
|Solver Submission Deadline:|
|Announcement of Results:||At the|
Researchers from both academia and industry are invited to submit their solvers and benchmarks to .