File generated on 6-09-2001
| 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 |
|