Cumulative CPU analysis of results

There is a lot of different ways to study the data collected during the first stage. Here, we give a ranking similar to the one of SAT-Ex. Each solver is given a maximal amount of time to solve an instance (recall that the launching heuristic also applies here). If it cannot solve the instance, then we only penalize it with the maximal cpu time. The ranking is given by the sum of all cpu time. However, this kind of ranking implies to penalize solvers that cannot solve a given instance, instead of just counting successes, we also have to count failures. So, a problem occurs with incomplete solvers on Unknown instances (whose can be Unsat). Thus, we reconsider how to compare solvers, and we rather partition solvers in Complete/Uncomplete solvers rather than by solver/benchmarks (e.g. Complete on ALL, All on SAT).

Results are given on Tables 15 (Industrial), 16 (Handmade) and 17 (Random). For randomized solvers, the median cpu time needed for a given benchmark is taken into account. As already noted using the SOTA system, berkmin is in head on industrial benchmarks, the whole picture tends to reinforce our awards, in all categories.

Table 15: Cumulative cpu time on Industrial benchmarks. Beware, we partition here complete vs incomplete solvers.

Complete			Incomplete
solver	cpu (Hours)	#solved (245)	solver	cpu (Hours)	#solved (137)
berkmin	54	175	unitwalk	54	57
zchaff	66	163	dlmsat1	57	53
2clseq	70	146	dlmsat2	57	54
limmat	79	144	saturn	60	49
simo	97	105	dlmsat3	63	51
rb2cl	114	81	usat05	64	44
OKsolver	115	78	usat10	64	46
modoc	117	79	ga	79	20
marchIIse	118	72
jquest	122	71
marchII	128	59
blindsat	146	25

Table 16: Cumulative cpu time on Handmade benchmarks. Beware, we partition here complete vs incomplete solvers.

Complete			Incomplete
solver	cpu (Hours)	#solved (276)	solver	cpu (Hours)	#solved (156)
berkmin	83	160	dlmsat1	71	56
zchaff	88	160	dlmsat3	71	54
limmat	99	139	dlmsat2	76	52
simo	105	134	saturn	80	44
2clseq	107	125	unitwalk	84	45
OKsolver	109	122	usat05	84	33
rb2cl	120	102	usat10	85	31
jquest	126	98	ga	96	15
marchII	129	91
marchIIse	129	98
modoc	130	89
blindsat	172	18

Table 17: Cumulative cpu time on Random benchmarks. Beware, we partition here complete vs incomplete solvers.

Complete			Incomplete
solver	cpu (Hours)	#solved (1502)	solver	cpu (Hours)	#solved (1502)
OKsolver	248	834	dlmsat1	325	541
marchII	253	829	unitwalk	332	513
marchIIse	254	829	dlmsat2	332	517
2clseq	310	655	dlmsat3	335	519
rb2cl	316	616	usat10	339	492
zchaff	326	573	usat05	340	491
berkmin	333	541	saturn	345	493
simo	337	569	ga	462	116
limmat	361	461
modoc	370	448
jquest	422	252
blindsat	464	115