SAT Competition 2020

Results

Main Track

Solver	Configuration	Score	Solved	Score SAT	Solved SAT	Score UNSAT	Solved UNSAT	Score Planning	Solved Planning
Kissat-sc2020-sat	default	3926	264	3127	146	4724	118	6773	73
Kissat-sc2020-default	default	4083	260	3830	134	4335	126	6774	73
Relaxed_LCMDCBDL_newTech	default	4179	253	2997	150	5361	103	7512	59
cryptominisat-ccnr-lsids	default	4266	248	3262	144	5270	104	6466	79
cryptominisat-ccnr	default	4278	250	3317	145	5238	105	6471	79
cadical-alluip-trail	default	4428	250	3908	135	4947	115	6406	80
cadical-alluip	default	4429	250	3909	135	4949	115	6409	80
Relaxed_LCMDCBDL	default	4436	245	3355	143	5517	102	7366	64
cryptominisat-walksat	default	4501	243	3721	139	5281	104	6472	79
cadical-trail	default	4554	243	4265	126	4842	117	6650	79
Kissat-sc2020-unsat	default	4560	238	4804	114	4315	124	6622	74
CaDiCaL-sc2020	default	4607	246	4368	130	4846	116	7339	61
MapleLCMDistChronoBT-DL-f2trc	default	5159	220	5264	110	5054	110	7213	66
Undominated-LC-MapleLCMDiscChronoBT-DL	default	5170	215	5173	110	5167	105	7312	62
Painless-ExMapleLCMDistChronoBT	PADC_DL	5177	214	5244	107	5110	107	7269	64
MapleLCMDistChronoBT-f2trc	default	5197	215	5344	106	5051	109	7269	64
MapleLCMDistChronoBT-f2trc-s	default	5210	214	5430	104	4991	110	7610	54
DurianSat	default	5257	210	5372	104	5142	106	7176	66
MapleLCMDistChronoBT-DL-v3	default	5258	211	5388	104	5128	107	7240	65
Painless-ExMapleLCMDistChronoBT	PADC_DL_OVAU_Lin	5277	211	5369	105	5185	106	7280	63
Maple_simp	default	5305	208	5484	101	5126	107	6754	73
Painless-ExMapleLCMDistChronoBT	PSIDS_DL	5327	210	5467	104	5188	106	7213	66
SLIME	default	5331	211	5502	104	5160	107	7560	58
Maple_mix	default	5360	208	5651	99	5069	109	6712	75
Painless-ExMapleLCMDistChronoBT	PADC_DL_OVAU_Exp	5403	203	5564	98	5242	105	7198	66
MLCMDChronoBT-DL-Scavel	default	5404	210	5408	107	5400	103	7467	60
MapleLCMDistChronoBT-DL-Scavel01	default	5489	208	5651	103	5326	105	7440	61
MapleCOMSPS_LRB_VSIDS_2	default_drup	5498	199	5679	96	5317	103	6772	73
MapleCOMSPS_LRB_VSIDS_2	LRB_VSIDS_2_init	5525	200	5779	96	5270	104	6746	75
exp_V_MLD_CBT_DL	default	5531	202	5713	98	5349	104	7319	65
Maple_CM+dist+sattime2s+-	default	5562	203	5386	105	5738	98	7472	59
MapleLCMDistChronoBT-DL-Scavel02	default	5572	203	5766	99	5377	104	7513	59
Maple-LCM-Dist-alluip-trail	default	5588	201	5872	95	5305	106	7699	54
exp_V_LGB_MLD_CBT_DL	default	5685	194	5854	94	5516	100	7376	64
exp_V_L_MLD_CBT_DL	default	5767	193	6124	89	5410	104	7334	65
Maple_CMused+dist	default	5770	193	6135	89	5404	104	7604	57
exp_L_MLD_CBT_DL	default	5777	192	6169	87	5384	105	7357	64
Maple_CM+dist	default	5845	188	6172	88	5517	100	7510	59
Maple_CM+dist+simp2--	default	5890	187	6121	90	5660	97	7527	58
upGlucose-3.0_PADC	default	6630	155	7234	64	6027	91	7025	68
glucose3.0	proofs	6662	154	7145	67	6179	87	7044	66
ParaFROST_CBT	default	6933	144	7547	59	6320	85	7973	44
Top36-Undominated-LC-MapleLCMDiscChronoBT-DL	default	7022	138	7302	62	6742	76	7601	57
Top24-Undominated-LC-MapleLCMDiscChronoBT-DL	default	7023	138	7302	62	6744	76	7577	58
Top16-Undominated-LC-MapleLCMDiscChronoBT-DL	default	7023	138	7303	62	6742	76	7575	58
ParaFROST	default	7073	137	7526	59	6621	78	8001	43
PauSat_noproof	default	9467	24	9355	15	9580	9	9142	19
PauSat	default	9469	24	9357	15	9580	9	9179	18

Incremental Track

	abcdsat-i20		cadicalsc2020		cryptominisat5		Riss-7.1.2
bones	513 (46)	2	631 (43)	3	390 (46)	1	903 (40)	4
essentials	1333 (35)	4	1210 (37)	2	1200 (36)	1	1241 (36)	3
lsp	2495 (21)	4	1959 (26)	3	1789 (29)	1	1881 (27)	2
max	1987 (27)	1	2021 (25)	2	2024 (25)	3	2021 (25)	2
ijtihad	3238 (10)	4	3002 (13)	1	3079 (12)	2	3145 (11)	3
pasar	471 (45)	2	506 (45)	3	969 (38)	4	386 (46)	1
final	1		1		3		1

Parallel Track

Solver	Score	Solved	Score SAT	Solved SAT	Score UNSAT	Solved UNSAT
P-MCOMSPS-STR-32	3316	283	2853	153	3779	130
P-MCOMSPS-STR-64	3714	271	3196	148	4232	123
Plingeling	3743	269	3805	133	3680	136
abcd-para-scavel (disqualified)	3872	267	3405	143	4338	124
maplepainlessdc (disqualified)	3888	260	3319	144	4457	116
ManyGlucose-32	3985	260	4076	130	3894	130
painlessmaplevone	4022	262	2913	154	5131	108
ManyGlucose-64	4036	258	4048	130	4024	128
painlessmaplevtwo	4103	260	3082	151	5123	109
syrupscavel	4433	243	4675	119	4191	124
mergesat (disqualified)	4852	224	5043	109	4660	115
mergesatnothp (disqualified)	4865	223	5068	108	4661	115
treengeling	4903	225	4907	114	4899	111
abcdsatptwenty	5240	214	6337	86	4142	128

Cloud Track

Solver	Score	Solved
mallob-mono	583	299
TopoSAT2	706	278
Slime	1057	214
Paracooba	1440	133
CTSat	1499	111
Paracooba-March	1708	63

NoLimits Track

Solver	Configuration	Score	Solved
Kissat-sc2020-sat	default	4073	192
Kissat-sc2020-default	default	4394	185
Relaxed_LCMDCBDL_newTech	default	4410	182
cryptominisat-ccnr-lsids	default	4498	179
cryptominisat-ccnr	default	4530	180
Relaxed_LCMDCBDL	default	4629	177
cryptominisat-ccnr-nolimits	default	4675	175
cryptominisat-ccnr-lsids-nolimits	default	4705	174
cryptominisat-walksat	default	4741	175
cadical-alluip-trail	default	4751	178
cadical-alluip	default	4752	178
cryptominisat-walksat-nolimits	default	4760	176
Kissat-sc2020-unsat	default	4854	169
CaDiCaL-sc2020	default	4924	176
cadical-trail	default	5012	168
Undominated-LC-MapleLCMDiscChronoBT-DL	default	5505	152
MapleLCMDistChronoBT-DL-f2trc	default	5513	156
Painless-ExMapleLCMDistChronoBT	PADC_DL	5558	150
abcdsat_n20	default	5570	151
MapleLCMDistChronoBT-f2trc	default	5632	149
MapleLCMDistChronoBT-f2trc-s	default	5643	148
MapleLCMDistChronoBT-DL-v3	default	5647	147
DurianSat	default	5668	146
SLIME	default	5703	148
Painless-ExMapleLCMDistChronoBT	PADC_DL_OVAU_Lin	5708	146
optsat_m20	default	5713	149
Maple_mix	default	5728	146
Maple_simp	default	5738	143
Painless-ExMapleLCMDistChronoBT	PSIDS_DL	5755	145
MLCMDChronoBT-DL-Scavel	default	5759	148
Painless-ExMapleLCMDistChronoBT	PADC_DL_OVAU_Exp	5784	141
MapleLCMDistChronoBT-DL-Scavel01	default	5901	145
exp_V_MLD_CBT_DL	default	5956	139
MapleCOMSPS_LRB_VSIDS_2	LRB_VSIDS_2_init	5974	137
MapleLCMDistChronoBT-DL-Scavel02	default	5986	141
SLIME	default-no-drup	6012	135
Maple_CM+dist+sattime2s+-	default	6043	138
MapleCOMSPS_LRB_VSIDS_2	default_drup	6049	133
Maple-LCM-Dist-alluip-trail	default	6157	134
exp_V_LGB_MLD_CBT_DL	default	6227	130
exp_V_L_MLD_CBT_DL	default	6229	132
exp_L_MLD_CBT_DL	default	6259	130
Maple_CMused+dist	default	6309	129
Maple_CM+dist+simp2--	default	6340	129
Maple_CM+dist	default	6370	126
Riss-nolimit	NOLIMIT	7043	103
Riss	default_proof	7085	103
upGlucose-3.0_PADC	default	7110	101
glucose3.0	proofs	7163	100
ParaFROST_CBT	default	7283	98
Top16-Undominated-LC-MapleLCMDiscChronoBT-DL	default	7418	91
Top24-Undominated-LC-MapleLCMDiscChronoBT-DL	default	7418	91
Top36-Undominated-LC-MapleLCMDiscChronoBT-DL	default	7419	91
ParaFROST	default	7478	90
Riss	NOUNSAT_proof-fixed	7504	92
GlucoseEsbpSel	default	7644	84
glucose-3.0-inprocess	default	7769	80
PauSat_noproof	default	9483	18
PauSat	default	9484	18