SAT solvers from the first competitions to Knuth's programs, each as a Docker image with a binary ready to run, the most thorough traceability we can offer (original sources, dated build environment, recipe and verification), and reproducible in a few clicks on your own machine.

A collective site, still being completed: please check, correct and contribute. Everything on these pages is generated from the data of the sat-heritage/docker-images repository as it stands today: which solvers build, which answer correctly, who wrote them, under which licence, with which awards. Much of it was assembled recently, year by year, partly with the help of an AI assistant, and is still being verified. Treat every claim as provisional and check it against the original competition material before relying on it. We strongly encourage pull requests and verification reports: a corrected author line, a licence, a working recipe, a missing solver, or the outcome of running an image on your own machine are all welcome as pull requests or issues. The goal is a site maintained by the SAT community as a whole. Images not on Docker Hub yet can be built locally with satex build <solver>:<year> (pip install satex).

Leaderboards

Solvers and authors ranked by competition medals: 3 points per gold, 2 per silver, 1 per bronze, every track and category counted, as recorded in data/awards.json. Only solvers with an image here are counted, so this is a view of the archive, not the official history; podiums and credits are still being clarified, corrections welcome by pull request. Click a column to sort.
#SolverYearAuthorsGoldSilverBronzePointsTracksStatus
1ppfolio other2011Olivier ROUSSEL533245Verified
2sateliteGTI other2005Niklas Eén, Niklas Sörensson410142Not run yet
3kissat-sc2024 Kissat2024Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt30091Verified
4March_KS other2007Marijn Heule and Hans van Maaren21082Verified
5Rsat other2007Knot Pipatsrisawat and Adnan Darwiche21081Verified
6SATzilla other2007Lin Xu, Frank Hutter, Holger H. Hoos and Kevin Leyton-Brown21081Verified
7clasp other2009Benjamin Kaufmann21081Verified
8painless-mcomsps other2018Ludovic Le Frioux, Hakan Metin, Souheib Baarir, Maximilien Colange, Julien Sopena, Fabrice Kordon21081Source unavailable
9SBVA other2023Andrew Haberlandt, Harrison Green21081Verified
10kissat-sc2022-bulky Kissat2022Armin Biere, Mathias Fleury12182Verified
11march-dl other2005Marijn Heule, Mark Dufour, Joris van Zwieten, Hans van Maaren03282Not run yet
12minisat MiniSat2007Niklas Sorensson and Niklas Een02482Verified
13vallst other2005Daniel Vallstrom20171Verified
14precosat other2009Armin Biere12071Verified
15glueminisat MiniSat2011Hidetomo NABESHIMA12072Verified
16Plingeling Lingeling2014Armin Biere12071Verified
17plingeling-sc18-starexec Lingeling2018Armin Biere12071Source unavailable
18ppfolio other2011Olivier ROUSSEL02374Verified
19oksolver other2002Oliver Kullmann20061Verified (packaged binary)
20zchaff other2002Lintao Zhang, Sharad Malik20062Verified (packaged binary)
21Forklift other2003Eugene Goldberg, Yakov Novikov20061Verified (packaged binary)
22Satzoo1 other2003Niklas Eén20061Verified (packaged binary)
23adaptnovelty other2004Holger Hoos, Dave Tompkins20061Verified (packaged binary)
24march-eq-100 other2004Marijn Heule, Hans van Maaren20061Verified (packaged binary)
25zchaff-rand other2004Zhaohui Fu, Yogesh Mahajan20061Verified (packaged binary)
26kcnfs-2004 other2005Gilles Dequen, Olivier Dubois20061Verified (packaged binary)
27march_rw other2011Marijn Heule20062Verified
28sparrow2011 other2011Adrian Balint & Andreas Froehlich and Dave Tompkins & Holger Hoos20062Verified
29Lingeling Lingeling2013Armin Biere20061Verified
30MapleCOMSPS_DRUP Maple2016Jia Hui Liang, Chanseok Oh, Vijay Ganesh, Krzysztof Czarnecki, Pascal Poupart20061Verified
31MapleLCMDistChronoBT Glucose2018Vadim Ryvchin, Alexander Nadel20061Verified
32MapleLCMDiscChronoBT-DL-v3 Maple2019Stepan Kochemazov, Oleg Zaikin, Victor Kondratiev, Alexander Semenov20061Verified
33kissat-MAB Kissat2021Mohamed Sami Cherif, Djamal Habet, Cyril Terrioux20061Verified
34hKis Kissat2022Rodrigue Konan Tchinda, Clémentin Tayou Djamegni20062Verified
35AE_kissat2025_MAB Kissat2025Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, Xinyun Wu20061Verified
36satsuma-iter-kissat Kissat2026Markus Anders, Cayden Codel20061Verified
37glucose Glucose2011Gilles Audemard and Laurent Simon11162Verified
38Plingeling Lingeling2011Armin Biere11161Verified
39minisat-static MiniSat2005Niklas Sörensson, Niklas Eén03062Verified (packaged binary)
40kissat_inc Kissat2022Zhihan Chen, Xindi Zhang, Shaowei Cai, Pinyan Lu03062Verified
41picosat other2007Armin Biere11051Verified
42glucose Glucose2009Gilles Audemard and Laurent Simon11051Verified
43march_hi other2009Marijn Heule11051Verified
44SATzilla2009_C other2009Lin Xu, Frank Hutter, Holger H. Hoos and Kevin Leyton-Brown11051Verified
45SATzilla2009_R other2009Lin Xu, Frank Hutter, Holger H. Hoos and Kevin Leyton-Brown11051Verified
46clasp other2011Benjamin Kaufmann11052Verified
47claspmt other2011Benjamin Kaufmann11051Source available, build fails
48CryptoMiniSat MiniSat2011Mate Soos11051Verified
49minisat-hack-cir_minisat MiniSat2011Tomohiro Sonobe11052Verified
50glucose Glucose2013Gilles Audemard and Laurent Simon11052Verified
51Plingeling Lingeling2013Armin Biere11051Verified
52Treengeling other2013Armin Biere11051Not run yet
53Lingeling Lingeling2014Armin Biere11052Runs, checks failed
54Lingeling (druplig) Lingeling2014Armin Biere11052Verified
55minisat_blbd MiniSat2014Jingchao Chen11052Verified
56Riss6 other2016Norbert Manthey, Aaron Stephan, Elias Werner11052Verified
57CaDiCaL CaDiCaL2019Armin Biere11051Verified
58Kissat-sc2020-sat Kissat2020Armin Biere, Katalin Fazekas, Mathias Fleury, Max Heisinger11051Verified
59Relaxed_LCMDCBDL_newTech other2020Xindi Zhang, Shaowei Cai11051Verified
60Kissat_MAB_ESA Kissat2022Shuolin Li, Jordi Coll, Chu-Min Li, Mao Luo, Djamal Habet, Felip Manyà11051Verified
61kissat_pre Kissat2022Zhihan Chen, Xindi Zhang, Shaowei Cai, Pinyan Lu11052Runs, checks failed
62Kissat_MAB-HyWalk Kissat2022Jiongzhi Zheng, Kun He, Zhuo Chen, Jianrong Zhou, Chu-Min Li10252Verified
63SATzilla other2007Lin Xu, Frank Hutter, Holger H. Hoos and Kevin Leyton-Brown10141Verified
64minisat-hack-contrasat MiniSat2011Allen Van Gelder10142Verified
65BreakIDGlucose Glucose2013Jo Devriendt, Bart Bogaerts10141Verified
66glucose Glucose2013Gilles Audemard and Laurent Simon10141Verified
67Riss3g other2013Norbert Manthey10142Verified
68SparrowToRiss other2014Adrian Balint, Norbert Manthey10141Verified
69Treengeling other2014Armin Biere10141Verified
70Kissat-sc2020-unsat Kissat2020Armin Biere, Katalin Fazekas, Mathias Fleury, Max Heisinger10142Verified
71CaDiCaL_vivinst CaDiCaL2023Armin Biere, Mathias Fleury, Florian Pollitt10142Verified
72gluebit_clasp other2013Jingchao Chen02041Verified
73Maple_LCM_Scavel Maple2018Yang Xu, Guanfeng Wu, Qingshan Chen, Shuwei Chen02041Verified
74kissat-public Kissat2025Armin Biere, Tobias Faller, Mathias Fleury, Nils Froleyks, Florian Pollitt02041Verified
75kissat-mab-hypre Kissat2026Jiongzhi Zheng and co-authors (provisional: 2026 proceedings not yet published)02041Verified
76Maple_CM Glucose2018Mao Luo, Fan Xiao, Chu-Min Li, Felip Manyà, Zhipeng Lü, Yu Li01242Verified
77cryptominisat-ccnr-lsids MiniSat2020Mate Soos, Shaowei Cai, Jo Devriendt, Stephan Gocht, Arijit Shaw, Kuldeep S. Meel01242Verified
78berkmin other2002Eugene Goldberg, Yakov Novikov10031Verified (packaged binary)
79limmat other2002Armin Biere10031Verified (packaged binary)
80kcnfs other2003Gilles Dequen, Olivier Dubois10031Verified (packaged binary)
81UnitWalk other2003Edward Hirsch, Arist Kojevnikov10031Verified (packaged binary)
82Jerusat1.3 other2004Alexander Nadel10031Verified (packaged binary)
83ranov other2005Duc Nghia Pham, Anbulagan10031Verified (packaged binary)
84gnovelty+ other2007Duc Nghia Pham and Charles Gretton10031Verified
85gNovelty+-T other2009Duc-Nghia Pham, Charles Gretton10031Runs, checks failed
86ManySAT-1.1 other2009Youssef Hamadi, Saïd Jabbour, Lakhdar Saïs10031Verified
87MiniSAT_09z MiniSat2009Markus Iser10031Verified
88SATzilla2009_I other2009Lin Xu, Frank Hutter, Holger H. Hoos and Kevin Leyton-Brown10031Verified
89TNM other2009Wanxia Wei and Chu Min Li10031Verified
90CSHCrandMC other2013Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf Sellmann.10031Not run yet
91probSAT other2013Adrian Balint, Uwe Schöning10031Not run yet
92SINNminisat MiniSat2013Takeru Yasumoto10031Verified
93dimetheus other2014Oliver Gableske10031Verified
94glueSplit_clasp other2014Jingchao Chen10031Verified
95MiniSat_HACK_999ED MiniSat2014Chanseok Oh10031Verified
96pprobSAT other2014Adrian Balint, Uwe Schöning10031Not run yet
97dimetheus other2016Oliver Gableske10031Not run yet
98glucose_hack_kiel_newScript Glucose2016Thorsten Ehlers, Dirk Nowotka10031Verified
99tc_glucose Glucose2016authors not recorded10031Verified
100treengeling-bbc-sc2016 other2016Armin Biere10031Verified
101Maple_LCM_Dist Glucose2017Fan Xiao, Mao Luo, Chu-Min Li, Felip Manyà, Zhipeng Lü10031Verified
102syrup Glucose2017Gilles Audemard, Laurent Simon10031Verified
103yalsat-03s other2017Armin Biere10031Verified
104CaDiCaL CaDiCaL2018Armin Biere10031Source unavailable
105GHackCOMSPS_drup other2018Chanseok Oh10031Verified
106Sparrow2Riss-2018 other2018Adrian Balint, Norbert Manthey10031Not run yet
107cadical-alluip-trail CaDiCaL2020Randy Hickey, Nick Feng, Fahiem Bacchus10031Verified
108cadical-PriPro CaDiCaL2021Benjamin Kaiser, Robert Clausecker10031Verified
109cadical-rp CaDiCaL2021Xindi Zhang, Shaowei Cai, Zhihan Chen10031Verified
110hKiS Kissat2021Rodrigue Konan Tchinda, Clémentin Tayou Djamegni10031Verified
111SLIME SLIME2021Oscar Riveros10031Verified
112hKis Kissat2022Rodrigue Konan Tchinda, Clémentin Tayou Djamegni10031Verified
113SeqFROST-ERE-All SeqFROST2022Muhammad Osama, Anton Wijs10031Verified
114SeqFROST-NoExtend SeqFROST2022Muhammad Osama, Anton Wijs10031Verified
115Kissat_MAB_prop Kissat2023Yu Gao10031Verified
116cadical-sc2025 CaDiCaL2025Armin Biere, Tobias Faller, Mathias Fleury, Nils Froleyks, Florian Pollitt10031Verified
117lymphosat other2026Harrison Green10031Verified
118satsuma-iter-ae-kissat-mab Kissat2026Markus Anders, Cayden Codel10031Verified
119zchaff-rand other2005Yogesh Mahajan, Sharad Malik, Lintao Zhang, Zhaohui Fu01131Verified (packaged binary)
120KCNFS other2007Gilles Dequen and Olivier Dubois01131Verified
121MPhaseSAT_M other2011Jingchao chen01132Verified
122sattime2011 other2011Chumin Li, Yu Li01132Verified
123ZENN other2013Takeru Yasumoto01131Verified
124glucose (certified unsat) Glucose2014Gilles Audemard and Laurent Simon01132Runs, checks failed
125kissat-sc2021 Kissat2021Armin Biere, Mathias Fleury, Maximilian Heisinger01131Verified
126Kissat_MAB_UCB Kissat2022Mohamed Sami Cherif, Djamal Habet, Cyril Terrioux01132Verified
127Kissat_MAB-DC Kissat2024Jinjin Liu, Jianmin Zhang, Yan Sun01131Verified
128vsa Kissat2025Shuolin Li, Jialu Zhang01131Verified
129HaifaSat other2005Roman Gershman00331Verified (packaged binary)
130g2wsat other2005Chu Min Li, Wen Qi Huang01021Verified (packaged binary)
131adaptg2wsat0 other2007Chu-Min Li, Wanxia Wei and Harry Zhang01021Verified
132TTS other2007Ivor Spence01021Verified
133gnovelty+2 other2009Duc-Nghia Pham and Charles Gretton01021Verified
134SApperloT-base other2009Stephan Kottler01021Not run yet
135csls other2011Alejandro Arbelaez and Youssef Hamadi01021Verified
136glueminisat-cert-unsat MiniSat2013Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue01021Verified
137Lingeling Lingeling2013Armin Biere01021Verified
138minisat_bit MiniSat2013Jingchao Chen01021Verified
139sattime2013 other2013Chu Min LI and Yu LI01021Not run yet
140BalancedZ other2014Chong HUANG, Chumin LI, Ruchu XU01021Runs, checks failed
141CCAnr+glucose Glucose2014Shaowei Cai, Chuan Luo, Kaile Su01021Runs, checks failed
142PeneLoPe other2014Audemard-Hoessen-Jabbour-Lagniez-Piette01021Verified
143CSCCSat other2016Chuan Luo, Shaowei Cai, Wei Wu, Kaile Su01021Verified
144plingeling-bbc-sc2016 Lingeling2016Armin Biere01021Verified
145tb_glucose Glucose2016authors not recorded01021Verified
146glu_vc other2017Jingchao Chen01021Verified
147MapleCOMSPS_LRB_VSIDS_2_drup Maple2017Jia Hui Liang, Chanseok Oh, Vijay Ganesh, Krzysztof Czarnecki, Pascal Poupart01021Verified
148plingeling-bbe-sc2017 Lingeling2017Armin Biere01021Verified
149tch_glucose3 Glucose2017Seongsoo Moon, Mary Inaba01021Verified
150gluHack other2018Aolong Zha01021Verified
151inIDGlucose Glucose2018Jo Devriendt01021Verified
152Maple_LCM_M1 Glucose2018Zhen Li, Kun He01021Verified
153expMaple_CM_GCBumpOnlyLRB Glucose2019Md Solimul Chowdhury, Martin Müller, Jia-Huai You01021Verified
154MapleLCMDistChronoBT-DL-v2.1 Maple2019Stepan Kochemazov, Oleg Zaikin, Victor Kondratiev, Alexander Semenov01021Verified
155cadical-trail other2020Randy Hickey, Nick Feng, Fahiem Bacchus01021Not run yet
156kissat_bonus Kissat2021Xindi Zhang, Shaowei Cai, Zhihan Chen01021Verified
157lstech_maple Glucose2021Xindi Zhang, Shaowei Cai, Zhihan Chen01021Verified
158Relaxed_LCMDCBDL_SCAVEL01 Glucose2021Zhihui Li, Guanfeng Wu, Yang Xu, Huimin Fu01021Verified
159Cadical_rel_1.5.3.Scavel CaDiCaL2023Zhihui Li, Guanfeng Wu, Yang Xu, Keming Wang, Zhiguo Long, Zhibin Yu01021Verified
160Kissat_MAB_prop_pr Kissat2023Yu Gao01021Verified
161BreakID-Kissat Kissat2024Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande01021Verified
162hCaD other2024Rodrigue Konan Tchinda, Clémentin Tayou Djamegni01021Verified
163kissat-mab-hypre-v2 Kissat2026Jiongzhi Zheng and co-authors (provisional: 2026 proceedings not yet published)01021Verified
164Dew-Satz-1a other2005Anbulagan00221Verified (packaged binary)
165IUT_BMB_SAT other2009Abdorrahim Bahrami, Seyed Rasoul Mousavi, Kiarash Bazargan00221Not run yet
166mxc-sat09 other2009David Bregman00222Verified
167CSCCSat2014 other2014Chuan Luo, Shaowei Cai, Wei Wu, Kaile Su00222Verified
168abcd_para18 other2018Jingchao Chen00221Source unavailable
169kissat_gb Kissat2021Md Solimul Chowdhury, Martin Müller, Jia-Huai You00221Verified
170ekissat-mab-gb-db Kissat2022Md Solimul Chowdhury00221Verified
171hKis other2024Rodrigue Konan Tchinda, Clémentin Tayou Djamegni00221Verified
172hsat.1 other2005Domagoj Babic00111Verified (packaged binary)
173Jerusat1.31-B other2005Alexander Nadel00111Verified (packaged binary)
174vw other2005Steven Prestwich00111Packaged binary, checks failed
175adaptg2wsat+ other2007Wanxia Wei, Chu-Min Li and Harry Zhang00111Verified
176MXC other2007David R. Bregman and David G. Mitchell00111Not run yet
177TiniSatELite other2007Jinbo Huang00111Verified
178adaptg2wsat2009++ other2009chuMin Li, Wanxia Wei00111Verified
179hybridGM3 other2009Adrian Balint00111Verified
180EagleUP other2011Oliver Gableske00111Verified
181Lingeling Lingeling2011Armin Biere00111Verified
182MPhaseSAT64 other2011Jingchao chen00111Verified
183QuteRSat other2011Chi-An Wu00111Source available, build fails
184forl other2013Mate Soos00111Not run yet
185march_vflip other2013Jingchao Chen00111Verified
186MiniGolf other2013Norbert Manthey00111Verified
187Ncca+ other2013Djamal Habet and Donia Toumi and André Abramé00111Verified
188PeneLoPe other2013Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette00111Not run yet
189pmcSAT other2013Ricardo Marques, Luís Guerra e Silva, Paulo Flores and Luís Miguel Silveira00111Verified
190satUZK other2013Alexander van der Grinten, Andreas Wotzlaw, Ewald Speckemeyer00111Not run yet
191pmcSAT other2014Ricardo Marques, Luís Guerra e Silva, Paulo Flores and Luís Miguel Silveira00111Verified
192SGSeq other2014Chu Min Li,Hua Jiang,Ru Chu Xu00111Verified
193CHBR_glucose Glucose2016Seongsoo Moon, Mary Inaba00111Verified
194cmsat5_run_parallel MiniSat2016Mate Soos00111Not run yet
195DCCAlm other2016Chuan Luo, Shaowei Cai, Kaile Su00111Verified
196Lingelingbbcmain Lingeling2016Armin Biere00111Verified
197COMiniSatPS_Pulsar_drup MiniSat2017Chanseok Oh00111Verified
198glucose-4.1 Glucose2017Gilles Audemard, Laurent Simon00111Verified
199painless Maple2017Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon00111Verified
200Score2SAT other2017Shaowei Cai, Chuan Luo00111Not run yet
201cms55-main-all4fixed MiniSat2018Mate Soos00111Verified
202cmsat55_run_parallel MiniSat2018Mate Soos00111Source unavailable
203glu_mix other2018Jingchao Chen00111Verified
204glucose-3.0_PADC_10 Glucose2018Rodrigue Konan Tchinda, Clémentin Tayou Djamegni00111Verified
205MapleLCMdistCBTcoreFirst Maple2019Jingchao Chen00111Verified
206PSIDS_MapleLCMDistChronoBT Glucose2019Rodrigue Konan Tchinda, Clémentin Tayou Djamegni00111Verified
207smallsat other2019Jingchao Chen00111Not run yet
208MapleLCMDistChronoBT-f2trc-s Maple2020Stepan Kochemazov00111Verified
209Relaxed_LCFTP_V2 Glucose2021Shunyang Bi, Zhang Qu, Meihua Liu, Pengfei Li, Yang Zhang, Hailong You00111Verified
210ekissat-mab-db-v1 Kissat2022Md Solimul Chowdhury00111Verified
211MapleCaDiCaL_PPD CaDiCaL2023Jonathan Chung, Sam Buss, Vijay Ganesh00111Verified
212PReLearn-kissat Kissat2023Joseph E. Reeves, Randal E. Bryant00111Verified
213AE_kissat2025_bump Kissat2025Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, Xinyun Wu00111Verified
214Kissat-CURE Kissat2025Yalun Cai, Mengxia Tao, Kezhi Li, Jiaying Zhu, Zhengyuan Shi, Qiang Xu00111Verified
215kissat-ae-hucb Kissat2026Jianmin Zhang and co-authors (provisional: 2026 proceedings not yet published)00111Verified
216kissat-eda-2 Kissat2026Yalun Cai, Qiang Xu00111Verified
217kissat-eda-3 Kissat2026Yalun Cai, Qiang Xu00111Verified