Results

This page presents the results of the five tracks of the SAT Challenge 2012. In each track each solver had to tackle 600 SAT instances. Below, you can find the awarded solvers and the complete final rankings for each track.

Awarded Solvers

Main Track: Application SAT+UNSAT

Best Single-Engine Solver in the Application Track:
glucose
by Gilles Audemard and Laurent Simon
Best Interacting Multi-Engine Approach in the Application Track:
Industrial Satisfiability Solver (ISS)
by Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, and Meinolf Sellmann
Best Portfolio Approach in the Application Track:
SATzilla 2012 APP
by Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown

Main Track: Hard Combinatorial SAT+UNSAT

Best Single-Engine Solver in the Hard Combinatorial Track:
clasp-crafted
by Benjamin Kaufmann, Torsten Schaub, and Marius Schneider
Best Interacting Multi-Engine Approach in the Hard Combinatorial Track:
interactSAT_c
by Jingchao Chen
Best Portfolio Approach in the Hard Combinatorial Track:
SATzilla 2012 COMB
by Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown

Main Track: Random SAT

Best Solver in the Sequential Random SAT Track:
CCASat
by Shaowei Cai, Chuan Luo, and Kaile Su

Parallel Track: Application SAT+UNSAT

Best Solver in the Parallel Track:
pfolioUZK
by Andreas Wotzlaw, Alexander van der Grinten, Ewald Speckenmeyer, and Stefan Porschen

Sequential Portfolio Track

Best Solver in the Sequential Portfolio Track:
SATzilla 2012 ALL
by Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown

The color coding in the tables is as follows:

Green for Single-Engine Solvers
Blue for Interacting Multi-Engine Solvers
Orange for Parallel Solvers
Pink for Portfolio Solvers
Grey for the Virtual Best Solver (VBS)

The columns denote, from left to right, the rank in the track (Rank), the rank in the track with respect to the type of solver (RiG, Rank-in-Group), the solver name (Solver), the number of solved instances (#solved), the percentage of solved instances (%solved), the cumulative run-time on all solved instances (cum. run-time) and the median run-time (counting time-outs as 900 seconds).

The given run-times are in seconds and denote wall-clock time for the Parallel Track and CPU time for all other tracks.

Detailed results (runtimes for each solver on each instance, statistical evaluation) are available within the EDACC system.

Main Track: Application SAT+UNSAT

Rank	RiG	Solver	#solved	%solved	cum. run-time	median run-time
–	–	Virtual Best Solver (VBS)	568	94.7	56528	30.3
1	1	SATzilla2012 APP	531	88.5	85194	114.0
2	2	SATzilla2012 ALL	515	85.8	86638	122.2
3	1	Industrial SAT Solver	499	83.2	93705	160.2
–	–	lingeling (SAT Competition 2011 Bronze)	488	81.3	84715	135.3
4	2	interactSAT	480	80.0	87676	152.5
5	1	glucose	475	79.2	71501	114.4
6	2	SINN	472	78.7	86302	146.4
7	3	ZENN	468	78.0	74019	124.7
8	4	Lingeling	467	77.8	91973	185.5
9	5	linge_dyphase	458	76.3	90192	204.4
10	6	simpsat	453	75.5	95737	222.0
11	7	glue_dyphase	452	75.3	67412	126.4
–	–	glueminisat (SAT Competition 2011 Silver)	452	75.3	68818	145.7
12	3	CCCneq	452	75.3	94956	224.7
–	–	glucose (SAT Competition 2011 Gold)	451	75.2	66076	120.6
13	8	TENN	451	75.2	82154	173.1
14	4	CCCeq	446	74.3	91896	230.9
–	–	CryptoMiniSat (REFERENCE)	442	73.7	95035	240.6
15	3	ppfolio2012	423	70.5	97819	293.0
16	4	pfolioUZK	404	67.3	98418	348.6
–	–	minisat (REFERENCE)	399	66.5	65633	189.5
17	9	relback	393	65.5	75842	285.6
18	10	Glucose++	389	64.8	75377	300.4
19	11	satUZKs	387	64.5	70910	263.7
20	12	caglue	387	64.5	78154	323.6
21	13	contrasat12	383	63.8	63645	243.6
22	14	satUZK	379	63.2	68621	282.3
23	15	relback_m	358	59.7	65364	397.3
24	16	riss	351	58.5	67549	434.3
25	5	Clingeling	278	46.3	76576	900.0
26	17	Sat4j	249	41.5	61334	900.0
27	6	Flegel	231	38.5	40190	900.0
28	18	march	37	6.2	9689	900.0

Main Track: Hard Combinatorial SAT+UNSAT

Rank	RiG	Solver	#solved	%solved	cum. run-time	median run-time
–	–	Virtual Best Solver (VBS)	529	88.2	24848	1.3
1	1	SATzilla2012 COMB	476	79.3	38108	45.4
2	2	SATzilla2012 ALL	473	78.8	41765	45.2
3	3	ppfolio2012	422	70.3	35784	50.5
4	1	interactSAT_c	417	69.5	40313	56.6
5	4	pfolioUZK	401	66.8	34187	77.7
6	5	aspeed-crafted	370	61.7	49239	269.3
7	1	clasp-crafted	367	61.2	49317	277.0
–	–	MPhaseSAT (SAT Competititon 2011) (REFERENCE)	361	60.2	35006	172.6
8	6	claspfolio-crafted	352	58.7	42522	296.7
–	–	clasp (SAT Competition 2011 #1 Non-portfolio) (REFERENCE)	347	57.8	41038	322.2
9	2	Lingeling	333	55.5	27313	291.0
10	2	CCCneq	329	54.8	36311	454.6
11	3	CCCeq	329	54.8	36943	494.3
12	4	Flegel	326	54.3	42999	596.2
13	5	Clingeling	326	54.3	47136	599.8
–	–	glucose (SAT Competition 2011 #3 Non-portfolio) (REFERENCE)	322	53.7	34546	515.4
14	3	ZENN	314	52.3	27878	490.8
15	4	simpsat	314	52.3	30999	582.3
16	5	relback	314	52.3	32182	642.5
17	6	SINN	313	52.2	33730	647.6
18	7	caglue	311	51.8	30109	647.1
–	–	CryptoMiniSat (REFERENCE)	307	51.2	32414	682.9
19	8	satUZKs	306	51.0	40401	801.5
20	9	contrasat12	306	51.0	40540	778.0
21	10	lingeling	305	50.8	29095	801.4
22	11	relback_m	304	50.7	36940	806.0
–	–	minisat (REFERENCE)	304	50.7	39055	843.9
23	12	satUZK	300	50.0	35028	869.6
24	13	TENN	287	47.8	26183	900.0
25	14	linge_dyphase	279	46.5	29183	900.0
26	15	riss	273	45.5	31599	900.0
27	16	Sat4j	271	45.2	26382	900.0
28	17	sattime2012	243	40.5	30541	900.0
29	18	sattime2011	238	39.7	28198	900.0
30	19	gNovelty+PCL	231	38.5	12791	900.0
31	20	Sparrow2011	217	36.2	19972	900.0
32	21	march	217	36.2	21817	900.0
33	22	BossLS	190	31.7	15034	900.0
34	23	CCASat	184	30.7	9052	900.0
35	24	sparrow2011-PCL	150	25.0	15330	900.0
–	–	EagleUP (SAT Competition 2011) (REFERENCE)	34	5.7	997	900.0

Main Track: Random SAT

Rank	RiG	Solver	#solved	%solved	cum. run-time	median run-time
–	–	Virtual Best Solver (VBS)	558	93.0	72841	39.2
1	1	CCASat	423	70.5	76206	218.8
2	1	SATzilla2012 RAND	321	53.5	80796	714.4
3	2	SATzilla2012 ALL	306	51.0	83273	845.6
–	–	Sparrow2011 (SAT Competition 2011 Gold) (REFERENCE)	303	50.5	76396	876.1
–	–	EagleUP (SAT Competition 2011 Bronze) (REFERENCE)	283	47.2	83787	900.0
4	2	sattime2012	269	44.8	80345	900.0
5	3	ppfolio2012	253	42.2	70903	900.0
–	–	sattime2011 (SAT Competition 2011 Silver) (REFERENCE)	236	39.3	67237	900.0
6	4	pfolioUZK	230	38.3	55584	900.0
7	3	ssa	150	25.0	35316	900.0
8	4	gNovelty+PCL	123	20.5	40240	900.0
9	5	BossLS	103	17.2	18934	900.0
10	6	sparrow2011-PCL	81	13.5	22788	900.0

Parallel Track: Application SAT+UNSAT

Rank	Solver	#solved	%solved	cum. run-time	median run-time
–	Virtual Best Solver (VBS)	576	96.0	39670	19.6
1	pfolioUZK	531	88.5	72390	69.1
2	PeneLoPe	530	88.3	62967	54.4
3	ppfolio2012	525	87.5	78833	91.4
4	Cellulose	521	86.8	53705	42.0
5	ppfolio	509	84.8	75400	91.3
6	Sucrose	503	83.8	76120	80.7
7	ParaCIRMiniSAT	496	82.7	63497	86.7
8	clasp	490	81.7	62424	77.8
9	Glycogen	489	81.5	76241	97.1
10	ZENNfork	485	80.8	73808	89.1
11	CryptoMiniSat	482	80.3	90543	166.4
12	Plingeling	467	77.8	87632	169.2
13	CCCneq	467	77.8	87970	159.5
14	CCCeq	466	77.7	92724	167.1
15	SATX10	464	77.3	73527	124.3
16	Treengeling	457	76.2	82929	180.2
17	Minifork	428	71.3	55864	106.5
18	claspmt (REFERENCE)	362	60.3	56435	352.3
19	splitter	273	45.5	35325	900.0

Sequential Portfolio Track

Rank	Solver	#solved	%solved	cum. run-time	median run-time
–	Virtual Best Solver (VBS)	484	80.7	64805	65.5
1	SATzilla2012 ALL	433	72.2	68033	139.9
2	ppfolio2012	370	61.7	65598	376.0
3	pfolioUZK	362	60.3	69485	391.6