SAT Competitions (original) (raw)

The International SAT Competition Web Page

Current Competition

Past Competitions, Races and Evaluations

SAT 2018 Competition
Organizers Marijn Heule,Matti Järvisalo,Martin Suda
Slides Slides used at SAT 2018
Proceedings Descriptions of the solvers and benchmarks
Benchmarks Available here
Solvers Available here
Gold Silver Bronze
Main Track
SAT+UNSAT Maple_LCM_Dist_ChronoBT Maple_LCM_Scavel Maple_CM
SAT Maple_LCM_Dist_ChronoBT Maple_LCM_Scavel CryptoMiniSat 5.5
UNSAT CaDiCaL Maple_LCM_M1 Maple_CM
Parallel Track
SAT+UNSAT Painless Plingeling abcdSAT
SAT Plingeling Painless CryptoMiniSat 5.5
UNSAT Painless Plingeling abcdSAT
No-Limits Track
ReasonLS Maple_CM CryptoMiniSat 5.5 V20
Glucose Hack Track
GHackCOMSPS inIDGlucose glu_mix
Random Track
Sparrow2Riss gluHack glucose-3.0_PADC_10
SAT 2017 Competition
Organizers Marijn Heule,Matti Järvisalo,Tomáš Balyo
Slides Slides used at SAT 2017
Proceedings Descriptions of the solvers and benchmarks
Benchmarks Available here
Solvers Available here
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
Agile Track Main Track Random Track
SAT+UNSAT CaDiCaL Agile, CaDiCaL NoProof Glu_VC Glucose 4.1 Maple LCM Dist, Maple LCM, MapleLRB LCMOccRestart, MapleLRB LCM MapleCOMSPS LRB VSIDS 2, MapleCOMSPS LRB VSIDS COMiniSATPS Pulsar YalSAT tch glucose3 Score2SAT
Parallel Track No-Limit Track Incremental Library Track
SAT+UNSAT Syrup24, Syrup48 Plingeling Painless MapleCOMSPS COMiniSATPS Pulsar MapleCOMPSPS LRB VSIDS 2, MapleCOMPSPS LRB VSIDS CaDiCaL NoProof AbcdSAT Glucose Riss
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
Agile Track Main Track Random Track
SAT+UNSAT Riss TB_Glucose CHBR_Glucose MapleCOMSPS Riss Lingeling Dimetheus CSCCSat DCCAlm
Parallel Track No-Limit Track Incremental Library Track
SAT+UNSAT 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
SAT+UNSAT MapleCOMSPS TC Glucose Kiel
SAT 2014 Competition
Organizing committee Anton Belov,Daniel Diepold,Marijn Heule,Matti Järvisalo
Judges Pete Manolios, Lakhdar Sais and Peter Stuckey
Proceedings Descriptions of the solvers and benchmarks
Benchmarks Application, Hard combinatorial, Random
Solvers Source code available in EDACC
Application Hard combinatorial Random
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
Core solvers
SAT+UNSAT Lingeling SWDiA5BY Riss BlackBox glueSplit_clasp Lingeling SparrowToRiss
SAT minisat_blbd Riss BlackBox SWDiA5BY SparrowToRiss CCAnr+glucose SGSeq Dimetheus BalancedZ CSCCSat2014
Certified UNSAT Lingeling (druplig) glucose SWDiA5BY Riss BlackBox Lingeling (druplig) glucose
Core solvers, Parallel
SAT+UNSAT Plingeling PeneLoPe Treengeling Treengeling Plingeling pmcSAT 2.0
SAT pprobSAT Plingeling CSCCSat2014
Minisat hack
SAT+UNSAT MiniSat_HACK_999ED minisat_blbd ROKKminisat
SAT 2013 Competition
Organizing committee Adrian Balint,Anton Belov,Marijn Heule,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
Application Hard combinatorial Random
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
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
CPU Time
Application Crafted Random
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
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
Application Crafted Random
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
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 Hack CirMinisat hack
Application Crafted Random
Gold Silver Bronze Gold Silver Bronze Gold Silver Bronze
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 application ManySAT
Parallel solver random gNovelty2+
Best Minisat Hack Minisat 09z
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
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

Purpose

The purpose of the competition is to identify new challengingbenchmarks and to promote new solversfor 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-Exsystem.

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.

[SAT-Ex] [SATLIB] [SAT Live!]

Imprint Privacy