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.943 2287.571 0.000
baseline singleBest 0.870 5189.358 525.787
baseline singleBestByPar 0.870 5189.358 525.787
baseline singleBestBySuccesses 0.870 5189.358 525.787
classif rpart 0.880 4706.229 366.658
classif randomForest 0.887 4455.380 331.809
classif ksvm 0.883 4567.651 336.080
cluster XMeans 0.860 5483.982 496.412
regr lm 0.873 4930.556 374.985
regr rpart 0.870 5119.231 455.661
regr randomForest 0.910 3649.287 281.717

The following default feature steps were used for model building:

ALL

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

nvarsOrig, nclausesOrig, nvars, nclauses, reducedVars,
reducedClauses, Pre.featuretime, 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, BINARY.,
TRINARY., Basic.featuretime, 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, KLB.featuretime, 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, CG.featuretime

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

Selected Features:
TRINARY., POSNEG.RATIO.VAR.entropy, HORNY.VAR.entropy

Selected Solvers:
ADS.cryptominisat.autotune, Glucose_nbSat, GlueMiniSat_2.2.10, GlueMiniSat_2.2.10.5, Lingeling_sr15bal,
Lingeling_sr15baq, abcdSAT, minisat_BCD, or.tools, riss_505_1