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.933 1209.329 0.000
baseline singleBest 0.798 3666.706 258.104
baseline singleBestByPar 0.798 3666.706 258.104
baseline singleBestBySuccesses 0.798 3666.706 258.104
classif rpart 0.815 3351.037 216.570
classif randomForest 0.875 2259.968 107.202
classif ksvm 0.857 2587.177 139.883
cluster XMeans 0.808 3469.874 237.239
regr lm 0.863 2480.926 131.808
regr rpart 0.812 3395.125 221.384
regr randomForest 0.899 1828.310 68.243

The following default feature steps were used for model building:

base

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

EXIST_VARS, FORALL_VARS, TOTAL_VARS, CLAUSES, LITERALS,
EXIST_SET, FORALL_SET, TOTAL_SET, UNARY_CLAUSES, BINARY_CLAUSES,
TERNARY_MORE_CLAUSES, POS_HORN, NEG_HORN, EXIST_LIT_PER_CLAUSE, FORALL_LIT_PER_CLAUSE,
EXIST_VARS_PER_SET, FORALL_POS_LITS_PER_CLAUSE, FORALL_NEG_LITS_PER_CLAUSE, OCCS_POS_NO_PER_VAR, OCCS_FORALL_NO_PER_VAR,
OCCS_FORALL_POS_NO_PER_VAR, W_OCCS_POS_NO_PER_VAR, W_OCCS_FORALL_NO_PER_VAR, W_OCCS_FORALL_POS_NO_PER_VAR, W_PRODUCTS,
LITN_LIT, LITEP_LIT, LITEN_LITE, LITEN_LITN, LITFN_LIT,
LITFP_LITFN, OCCP_OCCN, OCCE_OCC, OCCEN_OCC, OCCFP_OCCF,
OCCEN_OCCE, OCCEN_OCCN, OCCFP_OCCFN, TERMORE_CLAUSE, NEG_HORN_CLAUSE,
WOCCN_WOCC, WOCCEP_WOCC, WOCCFN_WOCC, WOCCEP_WOCCE, WOCCEP_WOCCP,
WOCCFN_WOCCN

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

Selected Features:
FORALL_VARS, W_OCCS_POS_NO_PER_VAR, W_PRODUCTS, LITEN_LITE, TERMORE_CLAUSE


Selected Solvers:
AIGSolve, depqbf.v2, qsts, rareqs, xb.bid.qsts