| fpga10_11 |
220 |
1122 |
561 |
73.93 |
- |
561 |
28.51 |
561 |
18.26 |
561 |
13.06 |
| fpga10_12 |
240 |
1344 |
663 |
104.28 |
- |
672 |
71.27 |
561 |
30.11 |
561 |
16.9 |
| fpga10_13 |
260 |
1586 |
561 |
74.61 |
- |
793 |
166.99 |
561 |
51.67 |
561 |
25.95 |
| fpga10_15 |
300 |
2130 |
561 |
80.61 |
- |
1065 |
570.3 |
561 |
128.05 |
561 |
44.18 |
| fpga11_12 |
264 |
1476 |
738 |
928.40 |
- |
738 |
112.53 |
738 |
66.8 |
738 |
65.49 |
| fpga11_13 |
286 |
1742 |
870 |
1971.77 |
- |
871 |
504.97 |
738 |
180.66 |
738 |
56.71 |
| fpga11_14 |
308 |
2030 |
856 |
1200.37 |
- |
1015 |
1565.6 |
738 |
415.32 |
738 |
69.55 |
| fpga11_15 |
330 |
2340 |
738 |
1008.08 |
- |
time out |
738 |
568.79 |
738 |
52.14 |
| aim-100-1_6-no-1 |
100 |
160 |
47 |
0.10 |
47 |
47 |
0.12 |
47 |
0.31 |
47 |
0.38 |
| aim-100-1_6-no-2 |
100 |
160 |
54 |
0.07 |
54 |
54 |
0.05 |
53 |
0.27 |
53 |
0.38 |
| aim-100-1_6-no-3 |
100 |
160 |
57 |
0.10 |
57 |
57 |
0.09 |
57 |
0.29 |
57 |
0.40 |
| aim-100-1_6-no-4 |
100 |
160 |
48 |
0.10 |
48 |
48 |
0.09 |
48 |
0.27 |
48 |
0.29 |
| aim-100-2_0-no-1 |
100 |
200 |
19 |
0.05 |
19 |
19 |
0.09 |
19 |
0.22 |
19 |
0.19 |
| aim-100-2_0-no-2 |
100 |
200 |
39 |
0.11 |
39 |
39 |
0.09 |
39 |
0.42 |
39 |
0.77 |
| aim-100-2_0-no-3 |
100 |
200 |
27 |
0.09 |
27 |
27 |
0.12 |
27 |
0.30 |
27 |
0.42 |
| aim-100-2_0-no-4 |
100 |
200 |
32 |
0.10 |
32 |
31 |
0.09 |
31 |
0.33 |
31 |
0.59 |
| aim-200-1_6-no-1 |
200 |
320 |
55 |
0.11 |
55 |
55 |
0.09 |
55 |
0.48 |
55 |
0.63 |
| aim-200-1_6-no-2 |
200 |
320 |
82 |
0.11 |
82 |
81 |
0.14 |
81 |
0.43 |
81 |
0.51 |
| aim-200-1_6-no-3 |
200 |
320 |
83 |
0.06 |
86 |
83 |
0.07 |
83 |
0.37 |
83 |
0.44 |
| aim-200-1_6-no-4 |
200 |
320 |
46 |
0.11 |
46 |
46 |
0.10 |
46 |
0.35 |
46 |
0.39 |
| aim-200-2_0-no-1 |
200 |
400 |
53 |
0.13 |
54 |
54 |
0.14 |
53 |
0.67 |
53 |
1.13 |
| aim-200-2_0-no-2 |
200 |
400 |
50 |
0.12 |
50 |
50 |
0.12 |
50 |
0.65 |
50 |
1.07 |
| aim-200-2_0-no-3 |
200 |
400 |
37 |
0.08 |
37 |
37 |
0.23 |
37 |
0.37 |
37 |
0.49 |
| aim-200-2_0-no-4 |
200 |
400 |
42 |
0.12 |
42 |
42 |
0.13 |
43 |
0.59 |
42 |
0.84 |
| aim-50-1_6-no-1 |
50 |
80 |
22 |
0.10 |
22 |
22 |
0.09 |
22 |
0.15 |
22 |
0.16 |
| aim-50-1_6-no-2 |
50 |
80 |
32 |
0.09 |
32 |
32 |
0.09 |
32 |
0.22 |
32 |
0.19 |
| aim-50-1_6-no-3 |
50 |
80 |
31 |
0.10 |
31 |
31 |
0.09 |
31 |
0.19 |
31 |
0.20 |
| aim-50-1_6-no-4 |
50 |
80 |
20 |
0.06 |
20 |
20 |
0.04 |
20 |
0.16 |
20 |
0.16 |
| aim-50-2_0-no-1 |
50 |
100 |
22 |
0.09 |
22 |
22 |
0.09 |
22 |
0.25 |
22 |
0.34 |
| aim-50-2_0-no-2 |
50 |
100 |
30 |
0.10 |
31 |
30 |
0.12 |
31 |
0.36 |
31 |
0.64 |
| aim-50-2_0-no-3 |
50 |
100 |
29 |
0.10 |
28 |
28 |
0.09 |
28 |
0.30 |
28 |
0.49 |
| aim-50-2_0-no-4 |
50 |
100 |
21 |
0.07 |
21 |
21 |
0.14 |
21 |
0.21 |
21 |
0.22 |
| 2bitadd_10 |
590 |
1422 |
929 |
148.27 |
- |
815 |
343.48 |
1212 |
42.75 |
806 |
189.47 |
| barrel2 |
50 |
159 |
79 |
0.22 |
- |
77 |
0.04 |
100 |
0.35 |
77 |
0.36 |
| jnh10 |
100 |
850 |
119 |
0.09 |
161 |
68 |
0.88 |
128 |
9.35 |
79 |
42.25 |
| jnh11 |
100 |
850 |
188 |
0.85 |
129 |
121 |
0.18 |
117 |
42.16 |
111 |
117.73 |
| jnh13 |
100 |
850 |
80 |
0.83 |
106 |
57 |
0.76 |
64 |
40.71 |
75 |
118.22 |
| jnh14 |
100 |
850 |
105 |
0.22 |
124 |
91 |
0.14 |
76 |
49.92 |
72 |
130.15 |
| jnh15 |
100 |
850 |
154 |
0.23 |
140 |
119 |
0.23 |
108 |
56.31 |
119 |
108.74 |
| jnh16 |
100 |
850 |
404 |
0.31 |
321 |
298 |
0.95 |
314 |
29.68 |
283 |
64.78 |
| jnh18 |
100 |
850 |
243 |
0.52 |
168 |
138 |
0.58 |
147 |
46.01 |
138 |
122.98 |
| jnh19 |
100 |
850 |
173 |
0.21 |
122 |
109 |
0.18 |
115 |
54.83 |
114 |
129.98 |
| jnh202 |
100 |
800 |
63 |
0.55 |
- |
55 |
0.53 |
58 |
21.63 |
70 |
65.14 |
| jnh203 |
100 |
800 |
182 |
0.24 |
- |
129 |
0.27 |
127 |
33.32 |
125 |
94.70 |
| jnh206 |
100 |
800 |
238 |
0.28 |
- |
174 |
0.33 |
209 |
20.28 |
189 |
68.51 |
| jnh208 |
100 |
800 |
166 |
0.21 |
- |
124 |
0.22 |
123 |
30.25 |
115 |
85.45 |
| jnh20 |
100 |
850 |
141 |
0.11 |
120 |
102 |
0.23 |
104 |
21.68 |
87 |
48.93 |
| jnh211 |
100 |
800 |
99 |
0.21 |
- |
86 |
0.14 |
85 |
37.70 |
73 |
109.27 |
| jnh2 |
100 |
850 |
64 |
0.46 |
60 |
45 |
0.49 |
50 |
28.64 |
51 |
87.80 |
| jnh302 |
100 |
900 |
23 |
0.21 |
- |
23 |
0.10 |
23 |
56.18 |
23 |
113.86 |
| jnh303 |
100 |
900 |
188 |
0.23 |
- |
118 |
0.31 |
156 |
62.09 |
98 |
148.85 |
| jnh304 |
100 |
900 |
32 |
0.21 |
- |
37 |
0.14 |
32 |
54.87 |
32 |
131.52 |
| jnh305 |
100 |
900 |
104 |
0.24 |
- |
89 |
0.17 |
78 |
74.34 |
73 |
176.64 |
| jnh306 |
100 |
900 |
289 |
0.25 |
- |
215 |
0.46 |
254 |
32.67 |
274 |
92.75 |
| jnh307 |
100 |
900 |
41 |
0.21 |
- |
33 |
0.14 |
42 |
53.22 |
38 |
159.06 |
| jnh308 |
100 |
900 |
112 |
0.23 |
- |
96 |
0.18 |
80 |
54.01 |
79 |
147.89 |
| jnh309 |
100 |
900 |
89 |
0.22 |
- |
51 |
0.14 |
54 |
40.58 |
51 |
114.11 |
| jnh310 |
100 |
900 |
21 |
0.20 |
- |
13 |
0.10 |
13 |
112.51 |
13 |
187.60 |
| jnh3 |
100 |
850 |
210 |
0.24 |
173 |
145 |
0.36 |
157 |
43.83 |
147 |
118.08 |
| jnh4 |
100 |
850 |
120 |
0.23 |
140 |
110 |
0.18 |
110 |
39.03 |
98 |
112.17 |
| jnh5 |
100 |
850 |
151 |
0.09 |
125 |
86 |
0.39 |
140 |
12.65 |
88 |
46.2 |
| jnh6 |
100 |
850 |
172 |
0.21 |
159 |
132 |
0.23 |
126 |
38.02 |
120 |
107.78 |
| jnh8 |
100 |
850 |
156 |
0.09 |
91 |
90 |
0.22 |
162 |
28.96 |
69 |
90.53 |
| jnh9 |
100 |
850 |
98 |
0.22 |
118 |
93 |
0.17 |
74 |
49.14 |
71 |
138.63 |
| homer06 |
180 |
830 |
415 |
34.96 |
- |
415 |
15.96 |
415 |
10.97 |
415 |
9.04 |
| homer07 |
198 |
1012 |
506 |
37.66 |
- |
506 |
21.6 |
415 |
12.59 |
415 |
10.67 |
| homer08 |
216 |
1212 |
506 |
52.42 |
- |
606 |
44.46 |
554 |
23.43 |
415 |
19.79 |
| homer09 |
270 |
1920 |
832 |
217.15 |
- |
960 |
141.48 |
415 |
93.19 |
504 |
60.9 |
| homer10 |
360 |
3460 |
1096 |
195.87 |
- |
940 |
624.11 |
1614 |
148.27 |
503 |
466.94 |
| homer11 |
220 |
1122 |
561 |
324.13 |
- |
561 |
23.44 |
561 |
41.68 |
561 |
15.6 |
| homer12 |
240 |
1344 |
672 |
575.54 |
- |
672 |
76.19 |
708 |
25.92 |
564 |
41.03 |
| homer13 |
260 |
1586 |
793 |
930.83 |
- |
793 |
152.13 |
579 |
67.38 |
561 |
76.66 |
| homer14 |
300 |
2130 |
793 |
999.18 |
- |
1065 |
714.03 |
561 |
347.19 |
561 |
28.03 |
| homer15 |
400 |
3840 |
1546 |
3426.76 |
- |
time out |
677 |
247.84 |
561 |
1048.28 |
| homer16 |
264 |
1476 |
time out |
- |
738 |
115.49 |
738 |
78.44 |
738 |
61.31 |
| homer17 |
286 |
1742 |
time out |
- |
871 |
369.11 |
870 |
127.43 |
738 |
68.28 |
| homer18 |
308 |
2030 |
time out |
- |
time out |
1015 |
746.09 |
870 |
406.79 |
| homer19 |
330 |
2340 |
time out |
- |
1170 |
3304.12 |
738 |
344.89 |
738 |
419.18 |
| homer20 |
440 |
4220 |
time out |
- |
time out |
time out |
time out |
| linvrinv2 |
24 |
61 |
51 |
0.07 |
- |
51 |
0.05 |
57 |
0.17 |
53 |
0.11 |
| linvrinv3 |
90 |
262 |
253 |
0.09 |
- |
250 |
0.15 |
250 |
0.41 |
244 |
0.32 |
| linvrinv4 |
224 |
689 |
689 |
4.15 |
- |
689 |
22.19 |
689 |
21.35 |
657 |
19.11 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| [1] Y. Oh, M.N. Mneimneh, Z.S. Andraus, K.A. Sakallah, and I.L. Markov, “AMUSE : A Minimally-Unsatisfiable Subformula Extractor” Proceedings of the Design Automation Conference (DAC'04), 518-523 (2004) |
| [2] Renato Bruni, “Approximating minimal unsatisfiable subformulae by means of adaptive core search” Discrete Applied Mathematics 130(2), 85-100 (2003) |
| [3] L. Zhang and S. Malik, “Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula” Conference on Theory and Applications of Satisfiability Testing (SAT'03), (2003) |
| [4] Bertrand Mazure, Lakdhar Saïs, Eric Grégoire, “Boosting complete techniques thanks to local search methods” Annals of Mathematics and Artificial Intelligence 22, 319-331 (2003) |
| [5] Eric Grégoire, Bertrand Mazure, Cédric Piette, “Extracting MUSes” , Proceedings of the 17th European Conference on Artificial Intelligence (ECAI'06), (2006) |