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.770 8337.099 0.000
baseline singleBest 0.577 15330.171 716.756
baseline singleBestByPar 0.577 15330.171 716.756
baseline singleBestBySuccesses 0.577 15330.171 716.756
classif rpart 0.717 10293.055 227.008
classif randomForest 0.730 9829.105 165.690
classif ksvm 0.704 10742.787 250.424
cluster XMeans 0.660 12343.237 429.822
regr lm 0.714 10388.712 227.928
regr rpart 0.714 10405.537 244.754
regr randomForest 0.744 9300.812 111.082

The following default feature steps were used for model building:

all_feats

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 5 to 5, resulting in a PAR10 score of 9203.960 for the reduced model. Analogously, the model that was generated based on 4 of the originally 46 features resulted in a PAR10 score of 9051.064. Below, you can find the list of the selected features and solvers:

Selected Features:
W_OCCS_FORALL_NO_PER_VAR, OCCP_OCCN, NEG_HORN_CLAUSE, WOCCEP_WOCC

Selected Solvers:
X2clsQ, QuBE, quantor, sKizzo, sSolve