The next competition will be organized in conjunction with SAT 2009.
Carsten Sinz organize a new SAT Race in conjunction with the SAT 2008 Conference.
| SAT 2007 competition | |
| Organizing committee | Daniel Le Berre,Olivier Roussel and Laurent Simon |
| Judges | Ewald Speckenmeyer, Geoff Sutcliffe and Lintao Zhang |
| Benchmarks | random (tar.bz2 44MB), crafted (.tar, bz2 compressed files inside 175MB), industrial (.tar, bz2 compressed files inside, 556 MB)+ velev 's VLIW-SAT 4.0 and VLIW-UNSAT 2.0 + IBM benchmarks |
| Systems | All/Winners precompiled for linux (tgz, 25/10 MB). Source code (competition division only, tgz, -updated 11/7/07- 6MB). |
| Industrial | handmade | Random | Gold | Silver | Bronze | Gold | Silver | Bronze | Gold | Silver | Bronze |
|---|---|---|---|---|---|---|---|---|---|
| SAT+UNSAT | Rsat | Picosat | Minisat | SATzilla CRAFTED | Minisat | MXC | SATzilla RANDOM | March KS | KCNFS 2004 |
| SAT | Picosat | Rsat | Minisat | March KS | SATzilla CRAFTED | Minisat | gnovelty+ | adaptg2wsat0 | adaptg2wsat+ |
| UNSAT | Rsat | Minisat | TiniSatELite | SATzilla CRAFTED | TTS | Minisat | March KS | KCNFS 2004 | SATzilla RANDOM |
In 2006, Carsten Sinz organized the SAT Race.
| SAT 2005 competition | |
| Organizing committee | Daniel Le Berre and Laurent Simon |
| Judges | Armin Biere, Oliver Kullmann and Allen Van Gelder |
| Reference | Daniel Le Berre and Laurent Simon Editors, Journal on Satisfiability, Boolean Modeling and Computation, Volume 2, Special Volume on the SAT 2005 competitions and evaluations, March 2006. |
| Benchmarks | Random (.tar.bz2, 25MB), Crafted (.tar.bz2, 360MB), Industrial (.tar.bz2, 205MB) See also IBM and Velev web sites. |
| Industrial | handmade | Random | Gold | Silver | Bronze | Gold | Silver | Bronze | Gold | Silver | Bronze |
|---|---|---|---|---|---|---|---|---|---|---|
| SAT+UNSAT | SatELiteGTI | MiniSAT 1.13 | zChaff_rand and HaifaSAT | Vallst | SatELiteGTI | March_dl | kcnf-2004 | March_dl | Dew_Satz1a | |
| SAT | SatELiteGTI | MiniSAT 1.13 | Jerusat 1.31 B and HaifaSAT | Vallst | March_dl | Hsat1 | ranov | g2wsat | VW | |
| UNSAT | SatELiteGTI | Zchaff_rand | HaifaSat | SatELiteGTI | MiniSAT 1.13 | Vallst and March-dl | kcnf-2004 | March_dl | Dew_Satz1a | |
| Special tracks | ||||||||||
| CERTIFIED UNSAT | zChaff | TTSP-3.0 | ||||||||
| NON CLAUSAL | No solver submitted | |||||||||
| PSEUDO BOOLEAN | Go to official web site | |||||||||
| SAT 2004 competition | |
| Organizing committee | Daniel Le Berre and Laurent Simon |
| Judges | Fahiem Bacchus, Hans Kleine Buning and Joao Marques Silva |
| Reference | 55 Solvers in Vancouver: The SAT 2004 competition. Daniel Le Berre and Laurent Simon. Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, Springer, Lecture Notes in Computer Science, n° 3542, pp 321-344, 2005. Revised Selected Papers. |
| Benchmarks | Random (.tar.bz2, 11MB), Crafted (.tar.bz2, 36MB), Industrial (.tar.bz2, 2GB) |
| Industrial | handmade | Random | |
|---|---|---|---|
| ALL (SAT+UNSAT) | Zchaff 2004 | March-eq | AdaptNovelty |
| SAT | Jerusat | Satzoo | AdaptNovelty |
| UNSAT | Zchaff 2004 | March-eq | Kcnfs |
| SAT 2003 competition | |
| Organizing committee | Daniel Le Berre and Laurent Simon |
| Judges | John Franco, Hans van Maaren and Toby Walsh |
| Reference | The essentials of the SAT 2003 competition. Daniel Le Berre and Laurent Simon. Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003). Lecture Notes in Computer Science 2919, pp 452-467, 2003. |
| Benchmarks | available from SATLIB (.tar.bz2, 345MB) |
| Industrial | handmade | Random | |
|---|---|---|---|
| Complete on all | Forklift | Satzoo | Kcnfs |
| ALL on SAT | Forklift | Satzoo | Unitwalk |
| SAT 2002 competition | |
| Organizing committee | Edward A. Hirsch, Daniel Le Berre and Laurent Simon |
| Judges | N/A |
| Reference | The SAT2002 competition
report. Laurent Simon, Daniel Le Berre and Edward
A. Hirsch. Annals of Mathematics and Artificial Intelligence, Volume 43, Issue 1-4, pp. 307-342, January 2005 See also A Parsimony Tree for the SAT2002 Competition. Paul W. Purdom, Daniel Le Berre, Laurent Simon Annals of Mathematics and Artificial Intelligence, Volume 43, Issue 1-4, pp. 343-365, January 2005 |
| Benchmarks | available from SATLIB (tgz, 147MB) |
| Industrial | handmade | Random | |
|---|---|---|---|
| Complete on all | zChaff | zChaff | OKSolver |
| ALL on SAT | Limmat | Berkmin | OKSolver |
The purpose of the competition is to identify new challenging benchmarks and to promote new solvers for the propositional satisfiability problem (SAT) as well as to compare them with state-of-the-art solvers. We strongly encourage people thinking about SAT-based techniques in their area (planning, hardware or software verification, etc.) to submit benchmarks to be used for the competition. The result of the competition will be a good indicator of the current feasibility of such approach. The competition will be completely automated using the SAT-Ex system.
Credits go to Hans van Maaren and John Franco who contributed significantly to the first SAT competition in order to make it into a success.
SATcompetition@satlive.org