LLAMA results

All results were produced by using the cross-validation splits in the repository with 10 folds and 1 repetitions.
The best values within a type (i.e., baseline (except for vbs), classif, regr and cluster) and performance measure (i.e., Percentage solved, PAR10, MCP) are colored green. Furthermore, the three best values over all groups within a performance measure are colored pink, the absolute best one is red.

The performance is measured in three different ways.

algo model succ par10 mcp
baseline vbs 0.808 1758.139 0.000
baseline singleBest 0.626 3401.815 170.949
baseline singleBestByPar 0.626 3401.815 170.949
baseline singleBestBySuccesses 0.626 3401.815 170.949
classif rpart 0.696 2762.263 99.818
classif randomForest 0.717 2572.056 77.554
classif ksvm 0.702 2710.964 93.734
cluster XMeans 0.638 3290.490 156.514
regr lm 0.690 2824.379 110.260
regr rpart 0.721 2548.488 86.283
regr randomForest 0.776 2046.680 30.168

The following default feature steps were used for model building:

default

Number of presolved instances: 0

The cost for using the feature steps (adapted for presolving) is: 0 or on average: NA

The feature steps correspond to the following 46 / 46 instance features:

EXIST_VARS, FORALL_VARS, TOTAL_VARS, CLAUSES, LITERALS,
EXIST_SET, FORALL_SET, TOTAL_SET, UNARY_CLAUSES, BINARY_CLAUSES,
TERNARY_MORE_CLAUSES, POS_HORN, NEG_HORN, EXIST_LIT_PER_CLAUSE, FORALL_LIT_PER_CLAUSE,
EXIST_VARS_PER_SET, FORALL_POS_LITS_PER_CLAUSE, FORALL_NEG_LITS_PER_CLAUSE, OCCS_POS_NO_PER_VAR, OCCS_FORALL_NO_PER_VAR,
OCCS_FORALL_POS_NO_PER_VAR, W_OCCS_POS_NO_PER_VAR, W_OCCS_FORALL_NO_PER_VAR, W_OCCS_FORALL_POS_NO_PER_VAR, W_PRODUCTS,
LITN_LIT, LITEP_LIT, LITEN_LITE, LITEN_LITN, LITFN_LIT,
LITFP_LITFN, OCCP_OCCN, OCCE_OCC, OCCEN_OCC, OCCFP_OCCF,
OCCEN_OCCE, OCCEN_OCCN, OCCFP_OCCFN, TERMORE_CLAUSE, NEG_HORN_CLAUSE,
WOCCN_WOCC, WOCCEP_WOCC, WOCCFN_WOCC, WOCCEP_WOCCE, WOCCEP_WOCCP,
WOCCFN_WOCCN

Algorithm and Feature Subset Selection

In order to get a better insight of the scenarios, forward selections have been applied to the solvers and features to determine whether small subsets achieve comparable performances. Following this approach, we reduced the number of solvers from 14 to 10, resulting in a PAR10 score of 2051.841 for the reduced model. Analogously, the model that was generated based on 6 of the originally 46 features resulted in a PAR10 score of 2003.861. Below, you can find the list of the selected features and solvers:

Selected Features:
TOTAL_SET, UNARY_CLAUSES, W_OCCS_FORALL_POS_NO_PER_VAR, OCCEN_OCCE, TERMORE_CLAUSE,
WOCCEP_WOCCP

Selected Solvers:
bcghostq, brareqs, depqbf, dual_ooq13, ghostq,
hiqqer3, ooq13, pre_dual_ooq13, rareqs, sqube