Information on Family 'facts'

Quick help: All I had gathered about this family and some statistical results of all solvers over the benchmarks of this family.
General Informations
Name :facts
Origin :formal-verification
Parent :facts
Brothers :None

Total Time spent :TODO
Best Total time :TODO (program)
Best Worst Time :TODO
Contains Challenges :TODO
Satistics on formulae
#Benchs :15
Clauses :
Mean (Std): 59197 (32954.87)
Median: 48920
[min-max]: [22539-140258]
Variables :
Mean (Std): 3429 (930.32)
Median: 3303
[min-max]: [2218-5315]

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
Powered by mySQLPowered by PHP3