The international SAT Competitions web page
Current competition
| Gold | Silver | Bronze | Gold | Silver | Bronze | Gold | Silver | Bronze |
| Agile Track | Main Track | Random Track |
| Riss |
TB_Glucose |
CHBR_Glucose |
MapleCOMSPS |
Riss |
Lingeling |
Dimetheus |
CSCCSat |
DCCAlm |
| Parallel Track | No-Limit Track | Incremental Library Track |
| Treengeling |
Plingeling |
CryptoMiniSat |
BreakIDCOMiniSatPS |
Lingeling |
abcdSAT |
CryptoMiniSat |
Glucose |
Riss |
| Best Application Benchmark Solver in the Main Track | Best Crafted Benchmark Solver in the Main Track | Best Glucose Hack in the Main Track |
| MapleCOMSPS |
|
TC Glucose |
|
Kiel |
|
Past competitions
In 2015, we had a SAT-Race 2015!
| Application | Hard combinatorial | Random |
| Gold | Silver | Bronze | Gold | Silver | Bronze | Gold | Silver | Bronze |
| Core solvers |
| Lingeling |
SWDiA5BY |
Riss BlackBox |
glueSplit_clasp |
Lingeling |
SparrowToRiss |
|
| minisat_blbd |
Riss BlackBox |
SWDiA5BY |
SparrowToRiss |
CCAnr+glucose |
SGSeq |
Dimetheus |
BalancedZ |
CSCCSat2014 |
| Lingeling (druplig) |
glucose |
SWDiA5BY |
Riss BlackBox |
Lingeling (druplig) |
glucose |
|
| Core solvers, Parallel |
| Plingeling |
PeneLoPe |
Treengeling |
Treengeling |
Plingeling |
pmcSAT 2.0 |
|
| |
pprobSAT |
Plingeling |
CSCCSat2014 |
| Minisat hack |
| MiniSat_HACK_999ED |
minisat_blbd |
ROKKminisat |
|
| Application | Hard combinatorial | Random |
| Gold | Silver | Bronze | Gold | Silver | Bronze | Gold | Silver | Bronze |
| Core solvers |
| Lingeling aqw |
Lingeling 587f |
ZENN 0.1.0 |
BreakIDGlucose 1 |
gluebit_clasp 1.0 |
glucose 2.3 |
CSHCrandMC |
MIPSat random sat_unsat |
march_vflip 1.0 |
| Lingeling aqw |
ZENN 0.1.0 |
satUZK 48 |
glucose 2.3 |
gluebit_clasp 1.0 |
BreakIDGlucose 1 |
probSAT SC13 |
sattime2013 2013 |
Ncca+ V 1.0 |
| glucose 2.3 (certified unsat) |
glueminisat-cert-unsat 2.2.7j |
Riss3g cert |
Riss3g cert |
glucose 2.3 (certified unsat) |
forl drup-nocachestamp |
|
| Core solvers, Parallel |
| Plingeling aqw |
Treengeling aqw |
PeneLoPe 2013 |
Treengeling aqw |
Plingeling aqw |
pmcSAT 1.0 |
|
| Minisat hack |
| SINNminisat 1.0.0 |
minisat_bit 1.0 |
MiniGolf prefetch |
|
| Open track (multiple solver sources, mixed benchmarks) |
| CSHCpar8 |
MIPSat |
GlucoRed+March r531 |
In 2012, we had a SAT Challenge!
In 2010, we have a new SAT Race!.
Carsten Sinz organized a new SAT Race in conjunction with the SAT 2008 Conference.
| Daniel Le Berre,Olivier Roussel and Laurent Simon |
| Ewald Speckenmeyer, Geoff Sutcliffe and Lintao Zhang |
| 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 |
| All/Winners precompiled for linux (tgz, 25/10 MB). Source code (competition division only, tgz, -updated 11/7/07- 6MB). |
In 2006, Carsten Sinz organized the SAT Race.
| Daniel Le Berre and Laurent Simon |
| Armin Biere, Oliver Kullmann and Allen Van Gelder |
| 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. |
| Random (.tar.bz2, 25MB), Crafted (.tar.bz2, 360MB), Industrial (.tar.bz2, 205MB) See also IBM and Velev web sites. |
| Daniel Le Berre and Laurent Simon |
| Fahiem Bacchus, Hans Kleine Buning
and Joao Marques Silva |
| 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. |
| Random (.tar.bz2, 11MB), Crafted (.tar.bz2, 36MB), Industrial (.tar.bz2, 2GB) |
| Daniel Le Berre and Laurent Simon |
| John Franco, Hans van Maaren and Toby Walsh |
| 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. |
| available from SATLIB (.tar.bz2, 345MB) |
| Edward
A. Hirsch, Daniel Le Berre and Laurent Simon |
| N/A |
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 |
| available from SATLIB (tgz, 147MB) |
Purpose
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
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
[SAT-Ex]
[SATLIB]
[SAT Live!]