The international SAT Competitions web page

Current competition

SAT 2014 competition
Organizing committee Anton Belov, Daniel Diepold, Marijn Heule, Matti Järvisalo

Past competitions

SAT 2013 competition
Organizing committee Adrian Balint, Anton Belov, Marijn Heule and Matti Järvisalo
Judges Roberto Sebastiani, Karem A. Sakallah and Youssef Hamadi
Proceedings Descriptions of the solvers and benchmarks
Benchmarks Application, Hard combinatorial, Random
Solvers
ApplicationHard combinatorialRandom
GoldSilverBronzeGoldSilverBronzeGoldSilverBronze
Core solvers
SAT+UNSAT 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
SAT 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
Certified UNSAT 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
SAT+UNSAT Plingeling aqw Treengeling aqw PeneLoPe 2013 Treengeling aqw Plingeling aqw pmcSAT 1.0  
Minisat hack
SAT+UNSAT 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!

SAT 2011 competition
Organizing committee Matti Järvisalo, Daniel Le Berre and Olivier Roussel
Judges Uwe Egly,Alexander Nadel, Ashish Sabharwal and Moshe Vardi
Benchmarks whole selection (tar of bz2 files, 1.7 GiB)
Solvers static binaries / dynamic libraries / source code
CPU Time
ApplicationCraftedRandom
GoldSilverBronzeGoldSilverBronzeGoldSilverBronze
SAT+UNSAT glucose glueminisat lingeling 3S ppfolio // ppfolio seq 3S ppfolio // ppfolio seq
SAT contrasat hack cirminisat hack mphasesat64 ppfolio // ppfolio seq 3S sparrow2011 sattime2011 eagleup
UNSAT glueminisat glucose qutersat clasp 3S glucose march_rw mphasesat_m ppfolio //
WC Time
ApplicationCraftedRandom
GoldSilverBronzeGoldSilverBronzeGoldSilverBronze
SAT+UNSAT plingeling cryptominisat // ppfolio // ppfolio // claspmt // 3S ppfolio // 3S ppfolio seq
SAT ppfolio // plingeling // contrasat ppfolio // ppfolio seq 3S sparrow2011 csls // sattime2011
UNSAT cryptominisat // glueminisat plingeling // claspmt // clasp ppfolio // march_rw ppfolio // mphasesat_m
Special prizes
Best Minisat HackCirMinisat hack

In 2010, we have a new SAT Race!.

SAT 2009 competition
Organizing committee Daniel Le Berre,Olivier Roussel and Laurent Simon
Judges Andreas Goerdt, Ines Lynce and Aaron Stump
Benchmarks random (7z 46MiB), crafted (.7z 171MiB), industrial (7z 385 MiB)
Solvers binaries (7z, 33MiB)/sources (7z, 25MiB)/booklet with the description of the solvers (and benchmarks)
ApplicationCraftedRandom
GoldSilverBronzeGoldSilverBronzeGoldSilverBronze
SAT+UNSAT precosat glucose lysat clasp SATzilla2009_C IUT_BMB_SAT SATzilla2009_R March hi NA
SAT SATzilla I precosat MXC clasp SApperloT MXC TNM gNovelty2+ hybridGM3 / adapt2wsat2009++
UNSAT glucose precosat lysat SATzilla2009_C clasp IUT_BMB_SAT March hi SATzilla2009_R NA
Special prizes
Parallel solver applicationManySAT
Parallel solver randomgNovelty2+
Best Minisat HackMinisat 09z

Carsten Sinz organized 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).
IndustrialhandmadeRandom
GoldSilverBronzeGoldSilverBronzeGoldSilverBronze
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.
IndustrialhandmadeRandom
GoldSilverBronzeGoldSilverBronzeGoldSilverBronze
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 UNSATzChaffTTSP-3.0
NON CLAUSALNo solver submitted
PSEUDO BOOLEANGo 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)
IndustrialhandmadeRandom
ALL (SAT+UNSAT)Zchaff 2004March-eqAdaptNovelty
SATJerusatSatzooAdaptNovelty
UNSATZchaff 2004March-eqKcnfs

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)
IndustrialhandmadeRandom
Complete on allForkliftSatzooKcnfs
ALL on SATForkliftSatzooUnitwalk

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)
IndustrialhandmadeRandom
Complete on allzChaffzChaffOKSolver
ALL on SATLimmatBerkminOKSolver

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!]