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
regr lm 0.575 21692.200 1270.230
regr rpart 0.513 24772.092 1545.589
regr randomForest 0.714 14630.844 455.333

The following default feature steps were used for model building:

instance, software

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

The feature steps correspond to the following 75 / 75 algorithm features:

Lines..Average., Lines..Total., Size..Average., Size..Total., Number.of.files,
Cyclomatic..Average., Cyclomatic..Total., Max.Indent..Average., Max.Indent..Total., nb_nodes,
nb_edges, degree_min, degree_max, degree_mean, degree_variance,
degree_entropy, transitivity, clustering_min, clustering_max, clustering_mean,
clustering_variance, path_min, paths_max, path_mean, path_variance,
path_entropy, Stmt, Type, Decl, Attribute,
Operator, Literal, edge_ss, edge_st, edge_sd,
edge_sa, edge_so, edge_sl, edge_ts, edge_tt,
edge_td, edge_ta, edge_to, edge_tl, edge_ds,
edge_dt, edge_dd, edge_da, edge_do, edge_dl,
edge_as, edge_at, edge_ad, edge_aa, edge_ao,
edge_al, edge_os, edge_ot, edge_od, edge_oa,
edge_oo, edge_ol, edge_ls, edge_lt, edge_ld,
edge_la, edge_lo, edge_ll, op_short, op_int,
op_long, op_long_long, op_float, op_double, op_bit

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

Selected Features:
VCG.CLAUSE.coeff.variation, VCG.CLAUSE.min, Literal, edge_td

Selected Solvers:
CaDiCaL, cms55.main.all4fixed, COMiniSatPS_Pulsar_drup, YalSAT, smallsat,
Maple_CM_ordUIP., Maple_CM_Dist, MapleLCMDistChronoBT, inIDGlucose, gluHack,
glucose.3.0_PADC_3, Riss7.1.fix, Sparrow2Riss.2018.fixfix