Next: Difficulties and future competitions
Up: Other views of the
Previous: Graphical analysis of SOTA
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
SATEx. 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 




Next: Difficulties and future competitions
Up: Other views of the
Previous: Graphical analysis of SOTA
LE BERRE Daniel
20020916