|
Best-Sol |
VBS |
Exact_mse_result |
Loandra_mse_result |
NuWLS_c_IBR_mse_result |
SPB_MaxSAT_c_Band_mse_result |
SPB_MaxSAT_c_FPS_mse_result |
SPB_MaxSAT_c_mse_result |
noSAT_MaxSAT_c_mse_result |
noSAT_MaxSAT_mse_result |
tt_open_wbo_inc_glucose_mse_result |
tt_open_wbo_inc_intelsat_mse_result |
| Instance |
|
|
|
|
|
|
|
|
|
|
|
|
| optimizing-BDDs-hypothyroid-un-wcnf_incomplete_improved_1_2019_2.wcnf.xz |
70 |
70 |
119 |
70 |
70 |
277 |
70 |
277 |
118 |
118 |
70 |
70 |
| protein_ins-6ebx_.1era_.g.wcnf.t.wcnf.xz |
30 |
30 |
30 |
30 |
30 |
30 |
30 |
30 |
30 |
30 |
30 |
30 |
| hs-timetabling-GreeceWesternGreeceUniversityInstance4.xml.wcnf.xz |
21 |
53 |
202 |
53 |
132 |
127 |
110 |
121 |
75 |
82 |
132 |
122 |
| des-cnf.16.p.6.wcnf.xz |
16 |
16 |
18 |
16 |
16 |
16 |
16 |
16 |
25 |
<NA> |
16 |
16 |
| minimize-5gons-u5-cube-maxcdcl-60-tmp-15-2655746.wcnf.xz |
77 |
77 |
147 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| minimize-5gons-u5-cube-maxcdcl-19-tmp-15-2655746.wcnf.xz |
77 |
77 |
140 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| inconsistency-measurement-im-contension-A-2-grd_1948_5_1.tgf.pl.wcnf.xz |
325 |
325 |
557 |
325 |
340 |
334 |
341 |
336 |
343 |
342 |
340 |
341 |
| ramsey-ram_k4_n20.ra0.wcnf.xz |
24 |
24 |
56 |
24 |
24 |
24 |
24 |
24 |
24 |
24 |
24 |
24 |
| treewidth-computation-TWComp_1en2_N69.wcnf.xz |
16 |
16 |
16 |
16 |
16 |
16 |
17 |
16 |
16 |
16 |
16 |
16 |
| ramsey-ram_k3_n12.ra0.wcnf.xz |
10 |
10 |
11 |
10 |
10 |
10 |
10 |
10 |
10 |
10 |
10 |
10 |
| protein_ins-1bpi_.5pti_.g.wcnf.t.wcnf.xz |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
| minimize-5gons-u5-cube-maxcdcl-8-tmp-15-2655746.wcnf.xz |
77 |
77 |
118 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| close_solutions-SAT07__industrial__vliw_sat_4.0__9vliw_m_9stages_iq3_C1_bug6.cnf.wcnf.4.wcnf.xz |
24 |
24 |
24 |
24 |
24 |
24 |
24 |
24 |
24 |
<NA> |
24 |
24 |
| protein_ins-3ebx_.1era_.g.wcnf.t.wcnf.xz |
34 |
34 |
34 |
54 |
34 |
34 |
34 |
34 |
34 |
34 |
34 |
34 |
| inconsistency-measurement-im-contension-A-2-grd_1697_5_7.tgf.pl.wcnf.xz |
272 |
273 |
307 |
273 |
286 |
281 |
280 |
281 |
287 |
287 |
286 |
284 |
| optic-gen_mult_4_6_9999.wcnf.xz |
348 |
348 |
2203 |
408 |
348 |
353 |
349 |
353 |
357 |
360 |
348 |
350 |
| logic-synthesis-normalized-test4.pi.opb.msat.wcnf.xz |
95 |
95 |
417 |
125 |
98 |
95 |
95 |
95 |
98 |
98 |
98 |
98 |
| optimizing-BDDs-splice-1-un-wcnf_incomplete_improved_1_2019_5.wcnf.xz |
371 |
371 |
1507 |
1716 |
574 |
371 |
946 |
573 |
1535 |
1312 |
574 |
1315 |
| scheduling-cnf_small.wcnf.xz |
28 |
28 |
31 |
28 |
28 |
31 |
31 |
28 |
46 |
47 |
28 |
28 |
| protein_ins-1bpi_.2knt_.g.wcnf.t.wcnf.xz |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
| decision-tree-australian-credit-un-formula_0.8_2021_atleast_127_max-6_reduced_incomplete_tree.wcnf.xz |
54 |
62 |
460 |
210 |
66 |
66 |
62 |
67 |
73 |
130 |
66 |
72 |
| judgment-aggregation-ja-maxham-preflib-00049-00000106.wcnf.xz |
43 |
43 |
44 |
43 |
43 |
43 |
43 |
43 |
44 |
44 |
43 |
43 |
| fault-diagnosis-s38584_nan_explicit_27_0.wcnf.xz |
203 |
203 |
231 |
203 |
206 |
203 |
206 |
204 |
279 |
287 |
206 |
203 |
| min-fill-MinFill_R3_david.wcnf.xz |
61 |
61 |
122 |
61 |
62 |
61 |
61 |
61 |
64 |
67 |
62 |
61 |
| SeanSafarpour-rsdecoder-problem.dimacs_37.filtered.wcnf.xz |
1 |
3 |
<NA> |
563 |
568 |
779 |
2713 |
1351 |
3 |
3 |
568 |
947 |
| ramsey-ram_k3_n18.ra0.wcnf.xz |
60 |
60 |
91 |
62 |
60 |
60 |
60 |
60 |
60 |
60 |
60 |
60 |
| protein_ins-2knt_.5pti_.g.wcnf.t.wcnf.xz |
32 |
32 |
32 |
32 |
32 |
32 |
32 |
32 |
32 |
32 |
32 |
32 |
| treewidth-computation-TWComp_mulsol.i.5-pp_N119.wcnf.xz |
31 |
31 |
31 |
31 |
31 |
31 |
31 |
31 |
31 |
31 |
31 |
31 |
| planning-bnn-navigation_4x4_5.wcnf.xz |
5 |
5 |
<NA> |
5 |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| xai-mindset2-ecoli.wcnf.xz |
510 |
520 |
1023 |
520 |
597 |
628 |
633 |
632 |
662 |
636 |
594 |
566 |
| inconsistency-measurement-im-hit-C-2-stb_304_352.tgf.pl.wcnf.xz |
42 |
42 |
56 |
44 |
42 |
42 |
42 |
42 |
42 |
42 |
42 |
42 |
| gen-hyper-tw-GenHyperTW_par8-2-c.wcnf.xz |
7 |
7 |
19 |
12 |
10 |
8 |
8 |
8 |
7 |
7 |
10 |
11 |
| SeanSafarpour-b15-bug-fourvec-gate-0.dimacs.seq.filtered.wcnf.xz |
4 |
4 |
221384 |
1384 |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
37 |
| inconsistency-measurement-im-forgetting-B-3-stb_339_393.tgf.pl.wcnf.xz |
56 |
56 |
585 |
57 |
56 |
57 |
58 |
58 |
68 |
66 |
56 |
56 |
| decision-tree-vote-un-formula_0.8_2021_atleast_15_max-3_reduced_incomplete_tree.wcnf.xz |
6 |
6 |
7 |
6 |
7 |
7 |
7 |
6 |
11 |
11 |
7 |
7 |
| optimizing-BDDs-lymph-un-wcnf_incomplete_improved_1_2019_6.wcnf.xz |
7 |
7 |
21 |
7 |
7 |
7 |
7 |
10 |
13 |
15 |
7 |
7 |
| railway-transport-d4.wcnf.xz |
1598 |
1892 |
21707 |
17734 |
2027 |
1984 |
2789 |
1985 |
2372 |
2501 |
2027 |
1892 |
| optimizing-BDDs-anneal-un-wcnf_incomplete_improved_1_2019_5.wcnf.xz |
121 |
121 |
146 |
121 |
137 |
139 |
133 |
125 |
140 |
127 |
137 |
138 |
| privilege-escalation-cloud_access_control_repair_task-134.wcnf.xz |
6 |
6 |
<NA> |
<NA> |
6 |
6 |
82 |
6 |
36 |
<NA> |
6 |
<NA> |
| privilege-escalation-cloud_access_control_repair_task-141.wcnf.xz |
27 |
78 |
4294 |
277 |
134 |
125 |
216 |
123 |
78 |
<NA> |
122 |
1269 |
| frb-frb40-19-4.partial.wcnf.xz |
720 |
720 |
727 |
720 |
720 |
721 |
721 |
721 |
721 |
720 |
720 |
720 |
| des-cnf.19.p.10.wcnf.xz |
19 |
19 |
<NA> |
19 |
30 |
30 |
30 |
30 |
32 |
<NA> |
30 |
21 |
| des-cnf.17.p.10.wcnf.xz |
17 |
17 |
24 |
18 |
20 |
20 |
20 |
20 |
27 |
<NA> |
20 |
17 |
| minimize-5gons-u5-cube-maxcdcl-9-tmp-15-2655746.wcnf.xz |
77 |
77 |
196 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| MaxSATQueriesinInterpretableClassifiers-toms_train_8_DNF_2_1.wcnf.xz |
567 |
567 |
3179 |
616 |
576 |
574 |
607 |
591 |
587 |
597 |
576 |
567 |
| optimizing-BDDs-anneal-un-wcnf_incomplete_improved_1_2019_7.wcnf.xz |
109 |
121 |
160 |
122 |
125 |
128 |
123 |
125 |
128 |
129 |
125 |
121 |
| privilege-escalation-cloud_access_control_repair_task-15.wcnf.xz |
67 |
1709 |
4785 |
5254 |
2432 |
1932 |
1709 |
1842 |
5255 |
<NA> |
2099 |
<NA> |
| inconsistency-measurement-im-sum-B-3-stb_390_450.tgf.pl.wcnf.xz |
46 |
46 |
1878 |
46 |
48 |
49 |
49 |
52 |
58 |
56 |
48 |
52 |
| setcover-sts-data.135.wcnf.xz |
103 |
103 |
105 |
104 |
103 |
103 |
103 |
103 |
103 |
103 |
103 |
104 |
| optic-gen_mult_4_6_991.wcnf.xz |
134 |
134 |
1126 |
163 |
137 |
134 |
134 |
135 |
138 |
138 |
137 |
136 |
| ramsey-ram_k3_n16.ra0.wcnf.xz |
39 |
39 |
108 |
39 |
39 |
39 |
39 |
39 |
39 |
39 |
39 |
39 |
| judgment-aggregation-ja-maxham-preflib-00049-00000291.wcnf.xz |
55 |
55 |
57 |
55 |
55 |
55 |
55 |
55 |
56 |
56 |
55 |
55 |
| gen-hyper-tw-GenHyperTW_grid3d_5.wcnf.xz |
10 |
11 |
15 |
14 |
13 |
12 |
12 |
12 |
11 |
11 |
13 |
12 |
| planning-bnn-cellda_x_10.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| close_solutions-SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug4_q0.used-as.sat04-723.cnf.wcnf.8.wcnf.xz |
86 |
86 |
86 |
86 |
86 |
86 |
86 |
86 |
1044 |
<NA> |
86 |
86 |
| gen-hyper-tw-GenHyperTW_grid4d_3.wcnf.xz |
6 |
7 |
8 |
8 |
8 |
7 |
7 |
7 |
7 |
7 |
8 |
7 |
| privilege-escalation-cloud_access_control_repair_task-34.wcnf.xz |
25 |
25 |
25 |
25 |
25 |
25 |
279 |
25 |
25 |
<NA> |
184 |
69 |
| SeanSafarpour-wb_4m8s4.dimacs.filtered.wcnf.xz |
213 |
213 |
42253 |
503 |
215 |
213 |
213 |
215 |
232 |
245 |
215 |
327 |
| optimizing-BDDs-soybean-un-wcnf_incomplete_improved_1_2019_7.wcnf.xz |
18 |
27 |
75 |
30 |
42 |
41 |
43 |
59 |
85 |
60 |
27 |
50 |
| optimizing-BDDs-tic-tac-toe-un-wcnf_incomplete_improved_1_2019_7.wcnf.xz |
56 |
142 |
289 |
142 |
182 |
228 |
182 |
180 |
271 |
248 |
182 |
188 |
| optic-gen_mult_4_5_991.wcnf.xz |
115 |
115 |
424 |
134 |
117 |
116 |
115 |
116 |
117 |
117 |
117 |
117 |
| minimize-5gons-u5-cube-maxcdcl-11-tmp-15-2655746.wcnf.xz |
77 |
77 |
164 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| minimize-5gons-u5-cube-maxcdcl-12-tmp-15-2655746.wcnf.xz |
77 |
77 |
161 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| decision-tree-splice-1-un-formula_0.8_2021_atleast_31_max-4_reduced_incomplete_tree.wcnf.xz |
343 |
1158 |
2039 |
1158 |
1343 |
1343 |
1337 |
1343 |
1195 |
<NA> |
1305 |
1226 |
| gen-hyper-tw-GenHyperTW_b06.wcnf.xz |
4 |
4 |
5 |
4 |
4 |
4 |
4 |
4 |
5 |
5 |
4 |
4 |
| minimize-5gons-u5-cube-maxcdcl-24-tmp-15-2655746.wcnf.xz |
77 |
77 |
98 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| planning-bnn-navigation_4x4_7.wcnf.xz |
5 |
7 |
<NA> |
7 |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| railway-transport-we.wcnf.xz |
294 |
1521 |
7193 |
5691 |
4543 |
4543 |
4543 |
4543 |
7966 |
<NA> |
4543 |
1521 |
| minimize-5gons-u5-cube-maxcdcl-59-tmp-15-2655746.wcnf.xz |
77 |
77 |
87 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| CircuitDebuggingProblems-spi-debug.dimacs.wcnf.xz |
1 |
1 |
1 |
687 |
2 |
2 |
2 |
2 |
2 |
1 |
2 |
1 |
| minimize-5gons-u5-cube-maxcdcl-36-tmp-15-2655746.wcnf.xz |
77 |
77 |
130 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| privilege-escalation-cloud_access_control_repair_task-146.wcnf.xz |
8 |
8 |
<NA> |
<NA> |
8 |
8 |
8 |
8 |
8254 |
<NA> |
8 |
<NA> |
| min-fill-MinFill_R0_myciel6.wcnf.xz |
753 |
773 |
2542 |
773 |
790 |
789 |
794 |
802 |
806 |
811 |
794 |
803 |
| judgment-aggregation-ja-maxham-preflib-00049-00000516.wcnf.xz |
53 |
54 |
56 |
54 |
54 |
54 |
54 |
54 |
56 |
55 |
54 |
54 |
| causal-discovery-causal_n6_i1_N500_uai13_harddeps_int.wcnf.xz |
19 |
19 |
45 |
19 |
19 |
19 |
19 |
19 |
38 |
38 |
19 |
19 |
| treewidth-computation-TWComp_queen5_5_N25.wcnf.xz |
18 |
18 |
18 |
18 |
18 |
18 |
18 |
18 |
18 |
18 |
18 |
18 |
| gen-hyper-tw-GenHyperTW_dubois29.wcnf.xz |
5 |
5 |
8 |
38 |
6 |
6 |
6 |
6 |
5 |
6 |
6 |
7 |
| SeanSafarpour-rsdecoder-problem.dimacs_39.filtered.wcnf.xz |
1 |
1 |
1 |
499 |
213 |
377 |
401 |
215 |
1 |
1 |
131 |
1 |
| program-disambiguation-Q27_YESNO_1.wcnf.xz |
2 |
2 |
2 |
2 |
2 |
2 |
2 |
2 |
4 |
<NA> |
2 |
2 |
| pseudoBoolean-normalized-par32-1.opb.msat.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| close_solutions-SAT11__application__fuhs__AProVE11__AProVE11-16.cnf.wcnf.1.wcnf.xz |
263 |
263 |
5783 |
263 |
263 |
263 |
263 |
263 |
11920 |
<NA> |
263 |
263 |
| privilege-escalation-cloud_access_control_repair_task-61.wcnf.xz |
16 |
16 |
<NA> |
<NA> |
123 |
153 |
1068 |
95 |
16 |
<NA> |
128 |
<NA> |
| ramsey-ram_k3_n19.ra0.wcnf.xz |
75 |
75 |
125 |
76 |
75 |
75 |
75 |
75 |
75 |
75 |
75 |
75 |
| minimize-5gons-u5-cube-maxcdcl-7-tmp-15-2655746.wcnf.xz |
77 |
77 |
122 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| gen-hyper-tw-GenHyperTW_b01.wcnf.xz |
5 |
5 |
5 |
5 |
5 |
5 |
5 |
5 |
5 |
5 |
5 |
5 |
| minimize-5gons-u5-cube-maxcdcl-61-tmp-15-2655746.wcnf.xz |
77 |
77 |
171 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| min-fill-MinFill_R0_myciel5.wcnf.xz |
196 |
196 |
473 |
196 |
197 |
196 |
197 |
197 |
197 |
196 |
197 |
205 |
| ramsey-ram_k3_n10.ra0.wcnf.xz |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
4 |
| optimizing-BDDs-primary-tumor-un-wcnf_incomplete_improved_1_2019_4.wcnf.xz |
49 |
49 |
53 |
49 |
49 |
49 |
49 |
49 |
54 |
56 |
49 |
49 |
| MaxSATQueriesinInterpretableClassifiers-twitter_train_3_CNF_2_1.wcnf.xz |
1637 |
1684 |
16125 |
2003 |
1776 |
1684 |
1795 |
1710 |
1770 |
1713 |
1769 |
1697 |
| treewidth-computation-TWComp_1dj7_N73.wcnf.xz |
26 |
26 |
26 |
26 |
26 |
26 |
26 |
26 |
27 |
28 |
26 |
26 |
| fault-diagnosis-s38584_nan_explicit_15_0.wcnf.xz |
208 |
208 |
240 |
208 |
211 |
210 |
211 |
210 |
282 |
283 |
210 |
211 |
| decision-tree-soybean-un-formula_0.8_2021_atleast_15_max-3_reduced_incomplete_tree.wcnf.xz |
22 |
22 |
23 |
22 |
22 |
22 |
22 |
22 |
44 |
64 |
22 |
22 |
| fault-diagnosis-s38584_nan_explicit_18_0.wcnf.xz |
186 |
187 |
225 |
187 |
187 |
187 |
187 |
187 |
284 |
285 |
187 |
187 |
| minimize-5gons-u5-cube-maxcdcl-46-tmp-15-2655746.wcnf.xz |
77 |
77 |
218 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| MaxSATQueriesinInterpretableClassifiers-compas_train_5_DNF_5_1.wcnf.xz |
2108 |
2110 |
2907 |
2128 |
2167 |
2110 |
2130 |
2144 |
2170 |
2153 |
2180 |
2189 |
| frb-frb40-19-2.partial.wcnf.xz |
720 |
720 |
730 |
720 |
720 |
721 |
721 |
721 |
720 |
721 |
720 |
721 |
| MaxSATQueriesinInterpretableClassifiers-toms_test_5_DNF_5_1.wcnf.xz |
60 |
60 |
148 |
239 |
61 |
60 |
66 |
63 |
63 |
62 |
61 |
61 |
| optic-gen_add_4_carry_991.wcnf.xz |
56 |
56 |
64 |
57 |
56 |
56 |
56 |
56 |
56 |
56 |
56 |
56 |
| optimizing-BDDs-splice-1-un-wcnf_incomplete_improved_1_2019_6.wcnf.xz |
573 |
573 |
1586 |
1717 |
1404 |
574 |
1404 |
911 |
1535 |
<NA> |
1365 |
573 |
| pseudoBoolean-normalized-par32-4.opb.msat.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| judgment-aggregation-ja-maxham-preflib-00049-00000338.wcnf.xz |
53 |
53 |
54 |
53 |
54 |
53 |
53 |
54 |
53 |
54 |
54 |
54 |
| gen-hyper-tw-GenHyperTW_aim-50-1_6-yes1-3.wcnf.xz |
10 |
10 |
13 |
14 |
12 |
12 |
12 |
11 |
10 |
11 |
12 |
11 |
| optimizing-BDDs-primary-tumor-un-wcnf_incomplete_improved_1_2019_8.wcnf.xz |
30 |
35 |
51 |
36 |
35 |
36 |
41 |
38 |
48 |
48 |
35 |
42 |
| inconsistency-measurement-im-hit-A-2-WS_300_16_90_30.tgf.pl.wcnf.xz |
34 |
34 |
38 |
36 |
35 |
34 |
34 |
35 |
34 |
34 |
35 |
35 |
| optimizing-BDDs-breast-cancer-un-wcnf_incomplete_improved_1_2019_8.wcnf.xz |
17 |
24 |
170 |
27 |
26 |
31 |
24 |
32 |
55 |
54 |
34 |
30 |
| judgment-aggregation-ja-maxham-preflib-00049-00000512.wcnf.xz |
54 |
54 |
56 |
56 |
56 |
56 |
55 |
54 |
57 |
56 |
56 |
56 |
| judgment-aggregation-ja-maxham-preflib-00049-00000304.wcnf.xz |
56 |
56 |
57 |
84 |
56 |
56 |
57 |
57 |
57 |
57 |
56 |
56 |
| inconsistency-measurement-im-sum-A-2-stb_547_485.tgf.pl.wcnf.xz |
66 |
68 |
2338 |
69 |
74 |
74 |
68 |
70 |
81 |
78 |
74 |
84 |
| xai-mindset2-lymphography.wcnf.xz |
52 |
52 |
56 |
53 |
53 |
52 |
52 |
52 |
59 |
63 |
53 |
53 |
| minimize-5gons-u5-cube-maxcdcl-20-tmp-15-2655746.wcnf.xz |
77 |
77 |
142 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| minimize-5gons-u5-cube-maxcdcl-18-tmp-15-2655746.wcnf.xz |
77 |
77 |
131 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| judgment-aggregation-ja-slater-preflib-00043-00000180.wcnf.xz |
306 |
306 |
2777 |
310 |
306 |
306 |
306 |
306 |
306 |
306 |
306 |
306 |
| minimize-5gons-u5-cube-maxcdcl-48-tmp-15-2655746.wcnf.xz |
77 |
77 |
153 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| judgment-aggregation-ja-maxham-preflib-00049-00000092.wcnf.xz |
46 |
46 |
48 |
47 |
47 |
46 |
47 |
46 |
48 |
48 |
47 |
47 |
| inconsistency-measurement-im-contension-A-2-grd_3018_3_7.tgf.pl.wcnf.xz |
529 |
529 |
2155 |
529 |
555 |
551 |
550 |
549 |
556 |
556 |
553 |
552 |
| SeanSafarpour-rsdecoder5.dimacs.filtered.wcnf.xz |
2 |
2 |
9945 |
254 |
2 |
2 |
2 |
2 |
7 |
14 |
2 |
2 |
| setcover-sts-data.729.wcnf.xz |
617 |
617 |
652 |
648 |
633 |
633 |
637 |
633 |
617 |
633 |
633 |
617 |
| fault-diagnosis-s38584_nan_explicit_33_0.wcnf.xz |
189 |
189 |
202 |
189 |
191 |
190 |
191 |
192 |
268 |
250 |
191 |
190 |
| xai-mindset2-australian.wcnf.xz |
471 |
489 |
1148 |
1548 |
536 |
536 |
510 |
502 |
1153 |
663 |
540 |
489 |
| program-disambiguation-Q36_YESNO_1.wcnf.xz |
0 |
0 |
<NA> |
0 |
0 |
0 |
0 |
0 |
<NA> |
<NA> |
0 |
8 |
| privilege-escalation-cloud_access_control_repair_task-178.wcnf.xz |
20 |
152 |
3353 |
187 |
667 |
985 |
838 |
912 |
4184 |
<NA> |
1072 |
152 |
| close_solutions-SAT04__industrial__velev__pipe-sat-1-1__12pipe_bug6_q0.used-as.sat04-725.cnf.wcnf.3.wcnf.xz |
148 |
148 |
148 |
148 |
148 |
148 |
148 |
148 |
148 |
<NA> |
148 |
148 |
| gen-hyper-tw-GenHyperTW_flat30-1.wcnf.xz |
20 |
20 |
<NA> |
64 |
26 |
23 |
20 |
23 |
22 |
23 |
26 |
22 |
| scheduling-cnf_10_center.wcnf.xz |
159 |
159 |
262 |
159 |
168 |
160 |
160 |
174 |
209 |
202 |
168 |
167 |
| minimize-5gons-u5-cube-maxcdcl-23-tmp-15-2655746.wcnf.xz |
77 |
77 |
126 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| optimizing-BDDs-tic-tac-toe-un-wcnf_incomplete_improved_1_2019_5.wcnf.xz |
160 |
203 |
314 |
203 |
256 |
229 |
254 |
233 |
258 |
268 |
256 |
217 |
| planning-bnn-sysadmin_4_4.wcnf.xz |
4 |
4 |
<NA> |
4 |
6 |
7 |
6 |
7 |
<NA> |
<NA> |
6 |
<NA> |
| min-fill-MinFill_R0_queen9_9.wcnf.xz |
1639 |
1639 |
1949 |
1639 |
1692 |
1690 |
1690 |
1666 |
1690 |
1687 |
1692 |
1686 |
| min-fill-MinFill_R0_myciel7.wcnf.xz |
3229 |
3393 |
10790 |
3393 |
3978 |
3659 |
3876 |
3742 |
3606 |
3468 |
3978 |
3679 |
| close_solutions-SAT_RACE06__velev-pipe-sat-1.0-b9.cnf.wcnf.8.wcnf.xz |
50 |
50 |
1181 |
50 |
50 |
50 |
50 |
50 |
<NA> |
<NA> |
559 |
50 |
| decision-tree-kr-vs-kp-un-formula_0.8_2021_atleast_127_max-6_reduced_incomplete_tree.wcnf.xz |
284 |
386 |
2452 |
1155 |
535 |
1090 |
386 |
1090 |
1329 |
<NA> |
1072 |
871 |
| planning-bnn-sysadmin_5_4.wcnf.xz |
6 |
10 |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
10 |
| privilege-escalation-cloud_access_control_repair_task-73.wcnf.xz |
31 |
31 |
31 |
106 |
91 |
79 |
136 |
79 |
5584 |
<NA> |
91 |
<NA> |
| inconsistency-measurement-im-forgetting-T-2-stb_265_466.tgf.pl.wcnf.xz |
36 |
36 |
1830 |
36 |
36 |
36 |
36 |
38 |
42 |
43 |
36 |
37 |
| scheduling-cnf_12.wcnf.xz |
61 |
61 |
238 |
67 |
61 |
62 |
62 |
62 |
111 |
114 |
61 |
61 |
| decision-tree-mushroom-un-formula_0.8_2021_atleast_127_max-6_reduced_incomplete_tree.wcnf.xz |
0 |
0 |
6498 |
2904 |
1272 |
1143 |
465 |
634 |
3341 |
<NA> |
344 |
0 |
| minimize-5gons-u5-cube-maxcdcl-44-tmp-15-2655746.wcnf.xz |
77 |
77 |
158 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| CircuitDebuggingProblems-rsdecoder-debug.dimacs.wcnf.xz |
1 |
1 |
<NA> |
1 |
1 |
1 |
1 |
1 |
1 |
1 |
1 |
264 |
| min-fill-MinFill_R0_mulsol.i.3.wcnf.xz |
241 |
241 |
10428 |
247 |
242 |
241 |
275 |
265 |
311 |
274 |
242 |
243 |
| xai-mindset2-postoperative-patient-data.wcnf.xz |
62 |
62 |
77 |
63 |
62 |
63 |
62 |
62 |
79 |
79 |
62 |
62 |
| decision-tree-vote-un-formula_0.8_2021_atleast_63_max-5_reduced_incomplete_tree.wcnf.xz |
0 |
0 |
4 |
1 |
1 |
2 |
1 |
1 |
11 |
11 |
1 |
0 |
| gen-hyper-tw-GenHyperTW_flat30-99.wcnf.xz |
22 |
22 |
<NA> |
58 |
23 |
24 |
22 |
22 |
22 |
23 |
23 |
24 |
| decision-tree-car-un-formula_0.8_2021_atleast_15_max-3_reduced_incomplete_tree.wcnf.xz |
143 |
143 |
152 |
143 |
143 |
143 |
143 |
143 |
193 |
153 |
143 |
151 |
| xai-mindset2-colic.wcnf.xz |
152 |
152 |
500 |
152 |
184 |
185 |
193 |
174 |
231 |
224 |
194 |
190 |
| inconsistency-measurement-im-sum-B-3-stb_428_430.tgf.pl.wcnf.xz |
53 |
54 |
1436 |
54 |
54 |
56 |
57 |
56 |
62 |
62 |
54 |
58 |
| judgment-aggregation-ja-maxham-preflib-00049-00000272.wcnf.xz |
56 |
56 |
58 |
57 |
58 |
57 |
57 |
56 |
58 |
58 |
58 |
57 |
| setcover-sts-data.243.wcnf.xz |
198 |
198 |
204 |
198 |
198 |
198 |
198 |
198 |
198 |
198 |
198 |
198 |
| minimize-5gons-u5-cube-maxcdcl-32-tmp-15-2655746.wcnf.xz |
77 |
77 |
168 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| protein_ins-p1.wcnf.t.wcnf.xz |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
| optic-gen_mult_5_5_991.wcnf.xz |
230 |
230 |
1846 |
268 |
230 |
232 |
231 |
231 |
232 |
232 |
230 |
231 |
| judgment-aggregation-ja-maxham-preflib-00049-00000511.wcnf.xz |
46 |
46 |
49 |
47 |
48 |
46 |
48 |
47 |
48 |
48 |
48 |
47 |
| judgment-aggregation-ja-slater-preflib-00049-00000451.wcnf.xz |
505 |
505 |
2162 |
513 |
505 |
505 |
505 |
505 |
505 |
505 |
505 |
505 |
| SeanSafarpour-wb_4m8s1.dimacs.filtered.wcnf.xz |
33 |
34 |
41801 |
261 |
66 |
80 |
73 |
66 |
34 |
34 |
66 |
66 |
| planning-bnn-cellda_y_8.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| judgment-aggregation-ja-slater-preflib-00043-00000196.wcnf.xz |
321 |
321 |
2677 |
324 |
321 |
321 |
321 |
321 |
321 |
321 |
321 |
321 |
| minimize-5gons-u5-cube-maxcdcl-41-tmp-15-2655746.wcnf.xz |
77 |
77 |
183 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| program-disambiguation-Q35_OPTIONS_1.wcnf.xz |
0 |
3 |
<NA> |
4 |
14 |
14 |
12 |
14 |
12 |
<NA> |
14 |
3 |
| minimize-5gons-u5-cube-maxcdcl-49-tmp-15-2655746.wcnf.xz |
77 |
77 |
213 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| judgment-aggregation-ja-maxham-preflib-00049-00000562.wcnf.xz |
42 |
42 |
43 |
43 |
42 |
42 |
42 |
42 |
42 |
43 |
42 |
43 |
| fault-diagnosis-s38584_nan_explicit_16_0.wcnf.xz |
188 |
188 |
237 |
188 |
190 |
190 |
189 |
190 |
275 |
289 |
189 |
188 |
| decision-tree-soybean-un-formula_0.8_2021_atleast_31_max-4_reduced_incomplete_tree.wcnf.xz |
9 |
10 |
25 |
11 |
11 |
11 |
14 |
10 |
65 |
73 |
11 |
12 |
| privilege-escalation-cloud_access_control_repair_task-47.wcnf.xz |
24 |
53 |
<NA> |
<NA> |
54 |
58 |
61 |
58 |
9166 |
<NA> |
53 |
<NA> |
| gen-hyper-tw-GenHyperTW_2bitcomp_5.wcnf.xz |
16 |
16 |
<NA> |
67 |
19 |
16 |
19 |
20 |
16 |
19 |
19 |
22 |
| planning-bnn-sysadmin_5_3.wcnf.xz |
4 |
6 |
8 |
6 |
9 |
9 |
9 |
9 |
<NA> |
<NA> |
7 |
6 |
| optimizing-BDDs-anneal-un-wcnf_incomplete_improved_1_2019_2.wcnf.xz |
139 |
139 |
139 |
139 |
139 |
139 |
139 |
139 |
151 |
151 |
139 |
139 |
| min-fill-MinFill_R0_queen11_11.wcnf.xz |
4207 |
4208 |
5118 |
4300 |
4349 |
4208 |
4373 |
4308 |
4485 |
4507 |
4355 |
4353 |
| inconsistency-measurement-im-contension-C-1-grd_3018_3_7.tgf.pl.wcnf.xz |
497 |
497 |
2267 |
497 |
520 |
520 |
521 |
513 |
526 |
524 |
520 |
519 |
| privilege-escalation-cloud_access_control_repair_task-130.wcnf.xz |
36 |
137 |
<NA> |
<NA> |
252 |
229 |
385 |
137 |
5532 |
<NA> |
307 |
<NA> |
| minimize-5gons-u5-cube-maxcdcl-38-tmp-15-2655746.wcnf.xz |
77 |
77 |
145 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| minimize-5gons-u5-cube-maxcdcl-58-tmp-15-2655746.wcnf.xz |
77 |
77 |
142 |
78 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| minimize-5gons-u5-cube-maxcdcl-29-tmp-15-2655746.wcnf.xz |
77 |
77 |
110 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| inconsistency-measurement-im-forgetting-B-3-stb_696_412.tgf.pl.wcnf.xz |
80 |
82 |
1004 |
89 |
82 |
84 |
82 |
86 |
97 |
98 |
82 |
96 |
| decision-tree-kr-vs-kp-un-formula_0.8_2021_atleast_31_max-4_reduced_incomplete_tree.wcnf.xz |
145 |
254 |
535 |
592 |
1074 |
449 |
504 |
449 |
1329 |
<NA> |
254 |
811 |
| gen-hyper-tw-GenHyperTW_uf20-099.wcnf.xz |
6 |
6 |
6 |
6 |
6 |
6 |
6 |
6 |
6 |
6 |
6 |
6 |
| decision-tree-australian-credit-un-formula_0.8_2021_atleast_63_max-5_reduced_incomplete_tree.wcnf.xz |
56 |
60 |
169 |
69 |
69 |
60 |
69 |
68 |
180 |
130 |
69 |
72 |
| xai-mindset2-house-votes-84.wcnf.xz |
74 |
74 |
75 |
74 |
74 |
74 |
74 |
74 |
102 |
<NA> |
74 |
74 |
| planning-bnn-cellda_x_12.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| planning-bnn-cellda_y_9.wcnf.xz |
6 |
8 |
<NA> |
<NA> |
8 |
8 |
8 |
8 |
<NA> |
<NA> |
8 |
8 |
| min-fill-MinFill_R1_games120.wcnf.xz |
1627 |
1627 |
4068 |
2647 |
1776 |
1627 |
1747 |
1811 |
2013 |
1927 |
1776 |
2026 |
| privilege-escalation-cloud_access_control_repair_task-117.wcnf.xz |
12 |
12 |
12 |
12 |
12 |
12 |
12 |
12 |
50 |
<NA> |
12 |
12 |
| decision-tree-soybean-un-formula_0.8_2021_atleast_127_max-6_reduced_incomplete_tree.wcnf.xz |
4 |
5 |
306 |
23 |
9 |
10 |
5 |
5 |
73 |
69 |
9 |
21 |
| protein_ins-1knt_.5pti_.g.wcnf.t.wcnf.xz |
29 |
29 |
37 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
29 |
| inconsistency-measurement-im-contension-A-2-grd_5178_1_1.tgf.pl.wcnf.xz |
837 |
837 |
4223 |
837 |
878 |
871 |
874 |
862 |
881 |
885 |
878 |
871 |
| decision-tree-splice-1-un-formula_0.8_2021_atleast_127_max-6_reduced_incomplete_tree.wcnf.xz |
1016 |
1180 |
<NA> |
1361 |
1360 |
1360 |
1360 |
1360 |
1195 |
<NA> |
1360 |
1180 |
| inconsistency-measurement-im-sum-T-1-grd_2130_2_7.tgf.pl.wcnf.xz |
406 |
406 |
46784 |
406 |
458 |
453 |
447 |
455 |
439 |
433 |
458 |
456 |
| SeanSafarpour-mem_ctrl-problem.dimacs_27.filtered.wcnf.xz |
1 |
1 |
<NA> |
<NA> |
35 |
38 |
38 |
35 |
18 |
16 |
35 |
1 |
| pseudoBoolean-normalized-par32-5.opb.msat.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| judgment-aggregation-ja-maxham-preflib-00049-00000003.wcnf.xz |
41 |
41 |
42 |
42 |
41 |
41 |
41 |
41 |
41 |
41 |
41 |
41 |
| SeanSafarpour-rsdecoder4.dimacs.filtered.wcnf.xz |
4 |
4 |
10160 |
203 |
4 |
24 |
4 |
24 |
16 |
133 |
19 |
32 |
| min-fill-MinFill_R0_queen7_7.wcnf.xz |
495 |
495 |
536 |
499 |
495 |
506 |
503 |
500 |
515 |
518 |
495 |
502 |
| decision-tree-hypothyroid-un-formula_0.8_2021_atleast_127_max-6_reduced_incomplete_tree.wcnf.xz |
39 |
40 |
2515 |
1822 |
68 |
46 |
64 |
40 |
102 |
103 |
43 |
58 |
| minimize-5gons-u5-cube-maxcdcl-53-tmp-15-2655746.wcnf.xz |
77 |
77 |
147 |
81 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| optic-gen_add_6_carry_991.wcnf.xz |
104 |
104 |
146 |
118 |
104 |
104 |
104 |
104 |
106 |
106 |
104 |
105 |
| min-fill-MinFill_R3_miles750.wcnf.xz |
473 |
690 |
4576 |
912 |
818 |
1030 |
1260 |
690 |
1927 |
1713 |
969 |
705 |
| HaplotypeAssembly-splitedReads_0.matrix.wcnf.xz |
1510 |
1510 |
3848 |
1535 |
1550 |
1510 |
1534 |
1528 |
1515 |
1521 |
1550 |
1548 |
| xai-mindset2-cleveland-nominal.wcnf.xz |
228 |
228 |
330 |
231 |
228 |
228 |
228 |
228 |
402 |
<NA> |
228 |
229 |
| protein_ins-1knt_.1bpi_.g.wcnf.t.wcnf.xz |
35 |
35 |
35 |
55 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
35 |
| MaxSATQueriesinInterpretableClassifiers-credit_train_3_DNF_3_1.wcnf.xz |
4814 |
4815 |
14636 |
5295 |
4840 |
4815 |
4839 |
4837 |
4831 |
4822 |
4840 |
4822 |
| decision-tree-soybean-un-formula_0.8_2021_atleast_63_max-5_reduced_incomplete_tree.wcnf.xz |
6 |
6 |
37 |
9 |
9 |
6 |
12 |
10 |
55 |
73 |
9 |
10 |
| min-fill-MinFill_R0_mulsol.i.1.wcnf.xz |
142 |
142 |
2955 |
142 |
142 |
142 |
154 |
142 |
179 |
208 |
142 |
142 |
| protein_ins-sandiaprotein.g.wcnf.t.wcnf.xz |
28 |
28 |
28 |
28 |
28 |
28 |
28 |
28 |
28 |
28 |
28 |
28 |
| inconsistency-measurement-im-forgetting-A-2-WS_300_16_90_30.tgf.pl.wcnf.xz |
34 |
34 |
724 |
36 |
37 |
36 |
36 |
34 |
46 |
44 |
37 |
36 |
| railway-transport-pesp_5min.wcnf.xz |
68 |
69 |
1384 |
71 |
69 |
73 |
73 |
79 |
70 |
74 |
69 |
78 |
| judgment-aggregation-ja-slater-preflib-00049-00000107.wcnf.xz |
300 |
300 |
706 |
300 |
300 |
300 |
300 |
300 |
300 |
300 |
300 |
300 |
| planning-bnn-sysadmin_4_3.wcnf.xz |
2 |
3 |
4 |
6 |
3 |
3 |
3 |
3 |
6 |
<NA> |
3 |
4 |
| railway-transport-pesp_18Min.wcnf.xz |
280 |
302 |
3051 |
313 |
302 |
363 |
812 |
392 |
335 |
319 |
302 |
324 |
| gen-hyper-tw-GenHyperTW_hole8.wcnf.xz |
9 |
9 |
<NA> |
52 |
9 |
9 |
11 |
10 |
9 |
9 |
9 |
10 |
| minimize-5gons-u5-cube-maxcdcl-13-tmp-15-2655746.wcnf.xz |
77 |
77 |
184 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
77 |
| planning-bnn-navigation_5x5_9.wcnf.xz |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
<NA> |
| gen-hyper-tw-GenHyperTW_atv_partial_system.wcnf.xz |
3 |
4 |
14 |
28 |
7 |
6 |
7 |
6 |
12 |
10 |
7 |
4 |
| scheduling-cnf_10.wcnf.xz |
50 |
52 |
368 |
99 |
54 |
55 |
55 |
52 |
116 |
119 |
54 |
52 |
| setcover-sts-data.405.wcnf.xz |
336 |
336 |
349 |
343 |
336 |
336 |
336 |
336 |
336 |
336 |
336 |
336 |
| scheduling-cnf_12_center.wcnf.xz |
237 |
237 |
362 |
237 |
237 |
237 |
237 |
237 |
264 |
263 |
237 |
251 |
| optic-gen_mult_5_5_9999.wcnf.xz |
500 |
500 |
2860 |
569 |
500 |
505 |
501 |
504 |
501 |
501 |
500 |
501 |
| privilege-escalation-cloud_access_control_repair_task-163.wcnf.xz |
9 |
9 |
3701 |
3768 |
9 |
9 |
9 |
9 |
35 |
<NA> |
9 |
<NA> |