Quick help: All I had gathered about this family and some statistical results of all solvers over the benchmarks of this family. |
|
|
List of included benchmarks | : | f7hh.14, f7hh.15, f8h_10, f8h_11, facts7h.10, facts7h, facts7hh.12, facts7hh.13-simp, facts7hh.13-simp.simple, facts7hh.13, facts7hh.13.simple, facts7hha.12, facts7hha.13, facts8.13, facts8h.12 |
Specific By-Hand Informations |
The family information for facts is not yet available. I'm sorry. If you want, you can mail me your request, just to hurry me... I'll be happy. (really).
Sorting according the total cpu-time needed |
Rank | Solver | Total Time | Total Time (s) | Slow factor | #Tested/#Total | #Failed |
1 | sato | 12 s | 12.78 | 1.00 | 15/15 | 0 |
2 | zchaff | 13 s | 13.45 | 1.05 | 15/15 | 0 |
3 | satz-215 | 1 m 8 s | 68.75 | 5.38 | 15/15 | 0 |
4 | relsat-200 | 1 m 15 s | 75.46 | 5.90 | 15/15 | 0 |
5 | relsat | 2 m 4 s | 124.85 | 9.77 | 15/15 | 0 |
6 | sato-3.2.1 | 3 m 49 s | 229.38 | 17.95 | 15/15 | 0 |
7 | sat-grasp | 8 m 4 s | 484.98 | 37.95 | 15/15 | 0 |
8 | csat | 14 m 29 s | 869.10 | 68.00 | 15/15 | 0 |
9 | modoc-2.0 | 3 h 25 m 14 s | 12314.37 | 963.57 | 15/15 | 1 |
10 | modoc | 3 h 44 m 1 s | 13441.53 | >1000 | 15/15 | 1 |
11 | satz-213 | 5 h 39 m 39 s | 20379.24 | >1000 | 15/15 | 2 |
12 | satz | 11 h 7 m 1 s | 40021.93 | >1000 | 15/15 | 4 |
13 | posit | 23 h 34 m 26 s | 84866.78 | >1000 | 15/15 | 6 |
14 | nsat | 23 h 59 m 14 s | 86354.47 | >1000 | 15/15 | 8 |
15 | heerhugo | 1 d 1 h 21 m 5 s | 91265.70 | >1000 | 15/15 | 9 |
16 | ntab_back2 | 1 d 3 h 50 m 4 s | 100204.11 | >1000 | 15/15 | 10 |
17 | ntab_back | 1 d 4 h 13 m 20 s | 101600.57 | >1000 | 15/15 | 10 |
18 | eqsatz | 1 d 12 h 7 m 35 s | 130055.52 | >1000 | 15/15 | 13 |
19 | asat | 1 d 13 h 7 m 55 s | 133675.05 | >1000 | 15/15 | 13 |
20 | ntab | 1 d 14 h 17 m 49 s | 137869.55 | >1000 | 15/15 | 13 |
21 | dr | 1 d 17 h 40 m 0 s | 150000.00 | >1000 | 15/15 | 15 |
22 | zres | 1 d 17 h 40 m 0 s | 150000.00 | >1000 | 15/15 | 15 |
23 | calcres | 1 d 17 h 40 m 0 s | 150000.00 | >1000 | 15/15 | 15 |
Sorting according the median cpu-time needed |
Rank | Solver | Median Time (s) | Slow factor | #Tested/#Total | #Failed |
1 | sato | 0.47 | 1.00 | 15/15 | 0 |
2 | zchaff | 0.77 | 1.64 | 15/15 | 0 |
3 | satz-215 | 2.27 | 4.83 | 15/15 | 0 |
4 | modoc-2.0 | 2.32 | 4.94 | 15/15 | 1 |
5 | sato-3.2.1 | 2.52 | 5.36 | 15/15 | 0 |
6 | modoc | 2.61 | 5.55 | 15/15 | 1 |
7 | satz | 2.64 | 5.62 | 15/15 | 4 |
8 | satz-213 | 2.82 | 6.00 | 15/15 | 2 |
9 | relsat-200 | 3.96 | 8.43 | 15/15 | 0 |
10 | relsat | 4.93 | 10.49 | 15/15 | 0 |
11 | csat | 11.62 | 24.72 | 15/15 | 0 |
12 | sat-grasp | 20.04 | 42.64 | 15/15 | 0 |
13 | posit | 9339.29 | >1000 | 15/15 | 6 |
14 | dr | 10000.00 | >1000 | 15/15 | 15 |
15 | ntab_back2 | 10000.00 | >1000 | 15/15 | 10 |
16 | ntab_back | 10000.00 | >1000 | 15/15 | 10 |
17 | ntab | 10000.00 | >1000 | 15/15 | 13 |
18 | heerhugo | 10000.00 | >1000 | 15/15 | 9 |
19 | zres | 10000.00 | >1000 | 15/15 | 15 |
20 | calcres | 10000.00 | >1000 | 15/15 | 15 |
21 | eqsatz | 10000.00 | >1000 | 15/15 | 13 |
22 | nsat | 10000.00 | >1000 | 15/15 | 8 |
23 | asat | 10000.00 | >1000 | 15/15 | 13 |
Sorting according the mean cpu-time needed |
Rank | Solver | Mean (Std) Time (s) | Slow factor | #Tested/#Total | #Failed |
1 | sato | 0.85 (0.90) | 1.00 | 15/15 | 0 |
2 | zchaff | 0.90 (0.60) | 1.06 | 15/15 | 0 |
3 | satz-215 | 4.58 (7.34) | 5.39 | 15/15 | 0 |
4 | relsat-200 | 5.03 (3.49) | 5.92 | 15/15 | 0 |
5 | relsat | 8.32 (7.84) | 9.79 | 15/15 | 0 |
6 | sato-3.2.1 | 15.29 (26.86) | 17.99 | 15/15 | 0 |
7 | sat-grasp | 32.33 (39.09) | 38.04 | 15/15 | 0 |
8 | csat | 57.94 (114.97) | 68.16 | 15/15 | 0 |
9 | modoc-2.0 | 820.96 (2560.65) | 965.84 | 15/15 | 1 |
10 | modoc | 896.10 (2588.11) | >1000 | 15/15 | 1 |
11 | satz-213 | 1358.62 (3509.51) | >1000 | 15/15 | 2 |
12 | satz | 2668.13 (4576.46) | >1000 | 15/15 | 4 |
13 | posit | 5657.79 (4782.27) | >1000 | 15/15 | 6 |
14 | nsat | 5756.96 (4950.19) | >1000 | 15/15 | 8 |
15 | heerhugo | 6084.38 (4967.89) | >1000 | 15/15 | 9 |
16 | ntab_back2 | 6680.27 (4859.76) | >1000 | 15/15 | 10 |
17 | ntab_back | 6773.37 (4737.08) | >1000 | 15/15 | 10 |
18 | eqsatz | 8670.37 (3508.90) | >1000 | 15/15 | 13 |
19 | asat | 8911.67 (2939.80) | >1000 | 15/15 | 13 |
20 | ntab | 9191.30 (2227.53) | >1000 | 15/15 | 13 |
21 | dr | 10000.00 (0.00) | >1000 | 15/15 | 15 |
22 | zres | 10000.00 (0.00) | >1000 | 15/15 | 15 |
23 | calcres | 10000.00 (0.00) | >1000 | 15/15 | 15 |
Crossing rank comparison |
Solver | Rank in Sum |
Rank in Median |
Rank in Mean |
Number of Solvers |
asat | 19 | 19 | 23 | 23 |
calcres | 23 | 23 | 20 | 23 |
csat | 8 | 8 | 11 | 23 |
dr | 21 | 21 | 14 | 23 |
eqsatz | 18 | 18 | 21 | 23 |
heerhugo | 15 | 15 | 18 | 23 |
modoc | 10 | 10 | 6 | 23 |
modoc-2.0 | 9 | 9 | 4 | 23 |
nsat | 14 | 14 | 22 | 23 |
ntab | 20 | 20 | 17 | 23 |
ntab_back | 17 | 17 | 16 | 23 |
ntab_back2 | 16 | 16 | 15 | 23 |
posit | 13 | 13 | 13 | 23 |
relsat | 5 | 5 | 10 | 23 |
relsat-200 | 4 | 4 | 9 | 23 |
sat-grasp | 7 | 7 | 12 | 23 |
sato | 1 | 1 | 1 | 23 |
sato-3.2.1 | 6 | 6 | 5 | 23 |
satz | 12 | 12 | 7 | 23 |
satz-213 | 11 | 11 | 8 | 23 |
satz-215 | 3 | 3 | 3 | 23 |
zchaff | 2 | 2 | 2 | 23 |
zres | 22 | 22 | 19 | 23 |
© 2000-2001 Laurent Simon | Scripts last modified on 01-07-2001 File generated on 6-09-2001 |
![]() ![]() |