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
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 |
|
|
|
|
Next: Difficulties and future competitions
Up: Other views of the
Previous: Graphical analysis of SOTA
LE BERRE Daniel
2002-09-16