obs | nas | min | qu_1st | med | mean | qu_3rd | max | sd | coeff_var | |
---|---|---|---|---|---|---|---|---|---|---|
EXIST_VARS | 825 | 12 | 3 | 5.9e+02 | 1.8e+03 | 1.5e+04 | 8.4e+03 | 5.7e+05 | 5.2e+04 | 3.5 |
FORALL_VARS | 825 | 12 | 0 | 12 | 44 | 5.6e+02 | 2.1e+02 | 3e+04 | 2e+03 | 3.6 |
TOTAL_VARS | 825 | 12 | 4 | 6.2e+02 | 1.9e+03 | 1.6e+04 | 9.1e+03 | 5.7e+05 | 5.3e+04 | 3.4 |
CLAUSES | 825 | 12 | 5 | 1.9e+03 | 6.5e+03 | 5.8e+04 | 3.3e+04 | 2.1e+06 | 1.8e+05 | 3 |
LITERALS | 825 | 12 | 9 | 5.1e+03 | 2e+04 | 1.8e+05 | 9.4e+04 | 7.8e+06 | 6.6e+05 | 3.6 |
EXIST_SET | 825 | 12 | 1 | 2 | 2 | 8.9 | 9 | 5.3e+02 | 30 | 3.3 |
FORALL_SET | 825 | 12 | 0 | 1 | 1 | 8.1 | 8 | 5.3e+02 | 30 | 3.7 |
TOTAL_SET | 825 | 12 | 1 | 3 | 3 | 17 | 17 | 1.1e+03 | 59 | 3.5 |
UNARY_CLAUSES | 825 | 12 | 0 | 1 | 1 | 7.1e+02 | 18 | 1e+05 | 6.8e+03 | 9.6 |
BINARY_CLAUSES | 825 | 12 | 0 | 9e+02 | 3.2e+03 | 3.4e+04 | 1.7e+04 | 2e+06 | 1.3e+05 | 3.9 |
TERNARY_MORE_CLAUSES | 825 | 12 | 1 | 5.4e+02 | 2.1e+03 | 2.3e+04 | 9.9e+03 | 8.1e+05 | 8.2e+04 | 3.6 |
POS_HORN | 825 | 12 | 3 | 1.3e+03 | 4.1e+03 | 4e+04 | 1.9e+04 | 2.1e+06 | 1.4e+05 | 3.6 |
NEG_HORN | 825 | 12 | 4 | 1e+03 | 3.3e+03 | 2.4e+04 | 1.8e+04 | 8.6e+05 | 7.4e+04 | 3.1 |
EXIST_LIT_PER_CLAUSE | 825 | 12 | 1 | 2 | 2.2 | 2.5 | 2.4 | 36 | 2 | 0.82 |
FORALL_LIT_PER_CLAUSE | 825 | 12 | 0 | 0.12 | 0.31 | 0.61 | 0.72 | 12 | 1.2 | 2 |
EXIST_VARS_PER_SET | 825 | 12 | 1 | 60 | 5.3e+02 | 6.7e+03 | 3e+03 | 3.4e+05 | 2.7e+04 | 4 |
FORALL_POS_LITS_PER_CLAUSE | 825 | 12 | 0 | 0.058 | 0.16 | 0.31 | 0.38 | 6 | 0.63 | 2 |
FORALL_NEG_LITS_PER_CLAUSE | 825 | 12 | 0 | 0.056 | 0.15 | 0.3 | 0.33 | 6 | 0.6 | 2 |
OCCS_POS_NO_PER_VAR | 825 | 12 | 0.027 | 2.9 | 3.4 | 9.2 | 4.4 | 1.3e+03 | 52 | 5.6 |
OCCS_FORALL_NO_PER_VAR | 825 | 12 | 0 | 8.5 | 16 | 3.7e+03 | 52 | 5.7e+05 | 3.9e+04 | 11 |
OCCS_FORALL_POS_NO_PER_VAR | 825 | 12 | 0 | 4.3 | 8.1 | 1.9e+03 | 30 | 2.9e+05 | 2e+04 | 11 |
W_OCCS_POS_NO_PER_VAR | 825 | 12 | 0.027 | 7.2 | 12 | 56 | 58 | 2.4e+03 | 1.5e+02 | 2.8 |
W_OCCS_FORALL_NO_PER_VAR | 825 | 12 | 0 | 22 | 68 | 8.6e+03 | 4e+02 | 1.1e+06 | 8.4e+04 | 9.9 |
W_OCCS_FORALL_POS_NO_PER_VAR | 825 | 12 | 0 | 11 | 36 | 4.3e+03 | 2e+02 | 5.7e+05 | 4.2e+04 | 9.8 |
W_PRODUCTS | 825 | 12 | 0.0081 | 30 | 92 | 2.3e+03 | 3.6e+02 | 6.7e+05 | 2.5e+04 | 11 |
LITN_LIT | 825 | 12 | 0.36 | 0.49 | 0.52 | 0.55 | 0.57 | 0.99 | 0.11 | 0.19 |
LITEP_LIT | 825 | 12 | 0.013 | 0.31 | 0.39 | 0.37 | 0.45 | 0.62 | 0.12 | 0.33 |
LITEN_LITE | 825 | 12 | 0.35 | 0.49 | 0.53 | 0.56 | 0.58 | 0.99 | 0.11 | 0.2 |
LITEN_LITN | 825 | 12 | 0.1 | 0.76 | 0.89 | 0.84 | 0.97 | 1 | 0.17 | 0.2 |
LITFN_LIT | 825 | 12 | 0 | 0.018 | 0.055 | 0.082 | 0.13 | 0.45 | 0.085 | 1 |
LITFP_LITFN | 825 | 12 | 0 | 1 | 1 | 1 | 1 | 3 | 0.23 | 0.22 |
OCCP_OCCN | 825 | 12 | 0.013 | 0.75 | 0.93 | 0.88 | 1 | 1.8 | 0.28 | 0.32 |
OCCE_OCC | 825 | 12 | 0.12 | 0.86 | 0.93 | 0.89 | 0.99 | 1.3 | 0.15 | 0.17 |
OCCEN_OCC | 825 | 12 | 0.066 | 0.41 | 0.48 | 0.5 | 0.55 | 1.1 | 0.15 | 0.3 |
OCCFP_OCCF | 825 | 12 | 0 | 0.5 | 0.5 | 0.51 | 0.5 | 0.75 | 0.051 | 0.1 |
OCCEN_OCCE | 825 | 12 | 0.35 | 0.49 | 0.53 | 0.56 | 0.58 | 0.99 | 0.11 | 0.2 |
OCCEN_OCCN | 825 | 12 | 0.13 | 0.87 | 0.94 | 0.9 | 1 | 1.4 | 0.15 | 0.17 |
OCCFP_OCCFN | 825 | 12 | 0 | 1 | 1 | 1 | 1 | 3 | 0.23 | 0.22 |
TERMORE_CLAUSE | 825 | 12 | 0.0019 | 0.23 | 0.3 | 0.41 | 0.55 | 1 | 0.28 | 0.69 |
NEG_HORN_CLAUSE | 825 | 12 | 0.00075 | 0.48 | 0.64 | 0.57 | 0.74 | 1 | 0.22 | 0.38 |
WOCCN_WOCC | 825 | 12 | 0.37 | 0.49 | 0.52 | 0.55 | 0.57 | 0.99 | 0.1 | 0.19 |
WOCCEP_WOCC | 825 | 12 | 0.013 | 0.39 | 0.42 | 0.41 | 0.48 | 0.74 | 0.12 | 0.29 |
WOCCFN_WOCC | 825 | 12 | 0 | 0.48 | 0.91 | 39 | 1.9 | 4.8e+03 | 3.2e+02 | 8.2 |
WOCCEP_WOCCE | 825 | 12 | 0.013 | 0.42 | 0.48 | 0.45 | 0.52 | 0.64 | 0.11 | 0.25 |
WOCCEP_WOCCP | 825 | 12 | 0.059 | 0.86 | 0.96 | 0.9 | 1 | 1.3 | 0.15 | 0.17 |
WOCCFN_WOCCN | 825 | 12 | 0 | 0.78 | 1.8 | 79 | 3.5 | 9.7e+03 | 6.5e+02 | 8.3 |
size | ok | timeout | memout | presolved | crash | other | unknown | cost_min | cost_mean | cost_max | cost_na | |
---|---|---|---|---|---|---|---|---|---|---|---|---|
base | 1 | 99 | 0 | 1.5 | 0 | 0 | 0 | 0 | 0.2 | 1.3 | 21 | 0.015 |
block | numbers | instances |
---|---|---|
1 | 2 | b20_PR_7_20 +++++++ b20_PR_7_90 |
2 | 2 | biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004 +++++++ biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004 |
3 | 12 | c1_BMC_p2_k1024 +++++++ c1_BMC_p2_k512 +++++++ c1_Debug_s3_f1_e1_v1 +++++++ c2_BMC_p1_k2048 +++++++ c3_Debug_s3_f2_e2_v2 +++++++ ... |
4 | 2 | C880.blif_0.10_0.20_0_0_out_exact +++++++ C880.blif_0.10_0.20_0_1_out_exact |
5 | 2 | cnt02e +++++++ counter_e_2 |
6 | 2 | connect_5x4_3_D +++++++ connect_5x4_3_R |
7 | 2 | k_dum_p-2 +++++++ k_dum_p-3 |
8 | 2 | lights3_021_0_009 +++++++ lights3_021_0_027 |
9 | 3 | lights3_035_0_002 +++++++ lights3_035_0_027 +++++++ lights3_035_0_051 |
10 | 2 | s05378_PR_1_75 +++++++ s05378_PR_9_2 |
11 | 2 | s09234_PR_8_2 +++++++ s09234_PR_8_5 |