The International SAT Competition Web Page

Current Competition

SAT 2024 Competition
Organizers	Marijn Heule, Markus Iser Matti Järvisalo, Martin Suda

Past Competitions, Races and Evaluations

SAT 2023 Competition
Organizers	Marijn Heule, Matti Järvisalo, Martin Suda, Markus Iser, Tomáš Balyo

SAT 2022 Competition
Organizers	Marijn Heule, Matti Järvisalo, Martin Suda, Markus Iser, Tomáš Balyo

SAT 2021 Competition
Organizers	Marijn Heule, Matti Järvisalo, Martin Suda, Markus Iser, Tomáš Balyo Nils Froleyks

SAT 2020 Competition
Organizers	Marijn Heule, Matti Järvisalo, Martin Suda, Markus Iser, Tomáš Balyo Nils Froleyks

SAT 2019 Race
Organizers	Marijn Heule, Matti Järvisalo, Martin Suda

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

SAT 2016 Competition
Organizers	Marijn Heule, Matti Järvisalo Tomáš Balyo
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	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 2015 Race
Organizing committee	Tomas Balyo, Carsten Sinz, Markus Iser, Armin Biere

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

SAT 2012 Challenge
Organizers	Adrian Balint, Anton Belov, Matti Järvisalo, Carsten Sinz

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

SAT 2010 Race
Organizer	Carsten Sinz

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)

	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 2008 Race
Organizer	Carsten Sinz

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 2006 Race
Organizer	Carsten Sinz

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 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.

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

Imprint Privacy