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.810 9841.233 0.000
baseline singleBest 0.586 21132.115 1220.060
baseline singleBestByPar 0.586 21132.115 1220.060
baseline singleBestBySuccesses 0.586 21132.115 1220.060
classif rpart 0.671 16854.266 766.573
classif randomForest 0.697 15524.588 584.204
classif ksvm 0.683 16230.220 652.442
cluster XMeans 0.612 19914.273 1149.527
regr lm 0.694 15674.298 606.436
regr rpart 0.657 17486.690 761.604
regr randomForest 0.700 15356.449 543.544

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 50 / 50 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, BINARY., TRINARY.,
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 37 to 11, resulting in a PAR10 score of 13757.915 for the reduced model. Analogously, the model that was generated based on 4 of the originally 48 features resulted in a PAR10 score of 13711.867. Below, you can find the list of the selected features and solvers:

Selected Features:
POSNEG.RATIO.CLAUSE.coeff.variation, BINARY., horn.clauses.fraction, VG.max

Selected Solvers:
CaDiCaL, Candy, YalSAT, Maple_CM_ordUIP., Maple_CM_ordUIP,
Maple_CM, MapleLCMDistChronoBT, Lingeling, gluHack, Glucose_Hack_Kiel_fastBVE,
Sparrow2Riss.2018.fixfix