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.853 3127.236 0.000
baseline singleBest 0.769 4893.141 190.904
baseline singleBestByPar 0.769 4893.141 190.904
baseline singleBestBySuccesses 0.769 4893.141 190.904
classif rpart 0.821 3795.520 64.070
classif randomForest 0.823 3743.180 54.879
classif ksvm 0.818 3836.658 62.058
cluster XMeans 0.820 3833.897 80.871
regr lm 0.822 3777.872 68.000
regr rpart 0.822 3789.716 79.841
regr randomForest 0.844 3321.285 21.339

The following default feature steps were used for model building:

group_basics

Number of presolved instances: 0

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

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

numVars, numClauses, perc_soft, soft_mean, soft_std,
soft_min, soft_max, var_clauses_ratio, vcg_var_mean, vcg_var_std,
vcg_var_min, vcg_var_max, vcg_var_spread, vcg_cls_mean, vcg_cls_std,
vcg_cls_min, vcg_cls_max, vcg_cls_spread, pnr_var_mean, pnr_var_std,
pnr_var_min, pnr_var_max, pnr_var_spread, pnr_cls_mean, pnr_cls_std,
pnr_cls_min, pnr_cls_max, pnr_cls_spread, unary, binary,
trinary, horn_mean, horn_std, horn_min, horn_max,
horn_spread, horn

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 6 to 3, resulting in a PAR10 score of 3322.795 for the reduced model. Analogously, the model that was generated based on 7 of the originally 30 features resulted in a PAR10 score of 3270.075. Below, you can find the list of the selected features and solvers:

Selected Features:
vcg_var_mean, vcg_var_min, vcg_cls_max, pnr_var_spread, pnr_cls_std,
unary, horn_max

Selected Solvers:
DSWPM1_924, akmaxsat, qmaxsat0.21g2comp