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.821 2221.497 0.000
baseline singleBest 0.736 3266.048 128.355
baseline singleBestByPar 0.736 3266.048 128.355
baseline singleBestBySuccesses 0.736 3266.048 128.355
classif rpart 0.722 3449.570 121.238
classif randomForest 0.772 2848.671 46.430
classif ksvm 0.766 2924.275 58.629
cluster XMeans 0.724 3433.010 118.633
regr lm 0.759 3015.787 75.810
regr rpart 0.738 3272.584 105.620
regr randomForest 0.774 2832.076 49.036

The following default feature steps were used for model building:

Pre, Basic, KLB, CG

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 50 / 115 instance features:

nvarsOrig, nclausesOrig, nvars, nclauses, reducedVars,
reducedClauses, vars_clauses_ratio, POSNEG_RATIO_CLAUSE_mean, POSNEG_RATIO_CLAUSE_coeff_variation, POSNEG_RATIO_CLAUSE_min,
POSNEG_RATIO_CLAUSE_max, POSNEG_RATIO_CLAUSE_entropy, VCG_CLAUSE_mean, VCG_CLAUSE_coeff_variation, VCG_CLAUSE_min,
VCG_CLAUSE_max, VCG_CLAUSE_entropy, UNARY, BINARYp, TRINARYp,
VCG_VAR_mean, VCG_VAR_coeff_variation, VCG_VAR_min, VCG_VAR_max, VCG_VAR_entropy,
POSNEG_RATIO_VAR_mean, POSNEG_RATIO_VAR_stdev, POSNEG_RATIO_VAR_min, POSNEG_RATIO_VAR_max, POSNEG_RATIO_VAR_entropy,
HORNY_VAR_mean, HORNY_VAR_coeff_variation, HORNY_VAR_min, HORNY_VAR_max, HORNY_VAR_entropy,
horn_clauses_fraction, VG_mean, VG_coeff_variation, VG_min, VG_max,
CG_mean, CG_coeff_variation, CG_min, CG_max, CG_entropy,
cluster_coeff_mean, cluster_coeff_coeff_variation, cluster_coeff_min, cluster_coeff_max, cluster_coeff_entropy

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

Selected Features:
POSNEG_RATIO_CLAUSE_coeff_variation, TRINARYp, cl_num_q10, SP_bias_mean, SP_bias_coeff_variation


Selected Solvers:
clasp2, cryptominisat2011, glucose2, lingeling, lrglshr,
mphaseSAT64, mphaseSATm