Overview of performance values

The following statistics were calculated from the performance values of each algorithm:
obs nas min qu_1st med mean qu_3rd max sd coeff_var
CryptoMiniSat_Strange.Night2.st_fixed_ 300 0 0.003998 41.443 467.154 1903.67 5000 5000 2201.45 1.15642
EBGlucose_1.0 300 0 0.006998 28.7346 644.982 2158.13 5000 5000 2276.53 1.05486
Lingeling_587f_fixed_ 300 0 0.008997 41.5027 483.255 1926.3 5000 5000 2217.77 1.15131
MPhaseSAT64_2011.05.14_fixed_ 300 0 0.005999 38.6452 569.907 2072.55 5000 5000 2253.88 1.08749
QuteRSat_2011.05.12_fixed_ 300 0 0.011997 36.6687 473.351 1947.07 5000 5000 2215.61 1.13792
RestartSAT_B95 300 0 0.002998 29.9875 546.307 1994.81 5000 5000 2238.9 1.12236
SAT09referencesolverglucose_1.0 300 0 0.005998 38.4601 907.731 2144.64 5000 5000 2250.33 1.04928
SAT09referencesolverprecosat_236 300 0 0.001999 38.2717 412.651 1973.68 5000 5000 2207.81 1.11863
glucose_2 300 0 0.004998 21.6994 423.372 1855.9 5000 5000 2162.08 1.16497
glueminisat_2.2.5 300 0 0.002999 27.2674 461.454 1956.46 5000 5000 2218.78 1.13408
minisathackEBMiniSAT_2011.03.02 300 0 0.000999 22.7178 600.56 2092.24 5000 5000 2268.92 1.08444
minisathackLR_GL_SHR_2011.03.02 300 0 0.001999 23.7789 807.479 2189.08 5000 5000 2288.18 1.04527
minisathackMiniSAT_2.2.0.agile.26 300 0 0.002998 20.9251 638.556 2154.95 5000 5000 2305.9 1.07005
minisathackcir_minisat_2011.05.13_simp_ 300 0 0.002998 21.0651 588.639 2060.42 5000 5000 2251.64 1.09281
minisathackcontrasat_2011.03.02 300 0 0.001999 34.6415 638.396 2125.75 5000 5000 2265.98 1.06596
minisathackminisat_psm_2011.04.01 300 0 0.007998 21.2758 612.067 2102.61 5000 5000 2271.68 1.08041
minisathackreferenceminisat_2.2.0 300 0 0.002998 21.1846 651.88 2105 5000 5000 2273.5 1.08005
rcl_2011.04.01 300 0 0.008998 32.743 908.356 2260.77 5000 5000 2317.51 1.0251

Summary of the runstatus per algorithm

The following table summarizes the runstatus of each algorithm over all instances (in %).

ok timeout memout not_applicable crash other
CryptoMiniSat_Strange.Night2.st_fixed_ 69.000 31.000 0.000 0.000 0.000 0.000
EBGlucose_1.0 66.333 33.667 0.000 0.000 0.000 0.000
glucose_2 71.667 28.333 0.000 0.000 0.000 0.000
glueminisat_2.2.5 70.333 29.667 0.000 0.000 0.000 0.000
Lingeling_587f_fixed_ 69.333 30.667 0.000 0.000 0.000 0.000
minisathackcir_minisat_2011.05.13_simp_ 67.333 32.667 0.000 0.000 0.000 0.000
minisathackcontrasat_2011.03.02 66.333 33.667 0.000 0.000 0.000 0.000
minisathackEBMiniSAT_2011.03.02 65.333 34.667 0.000 0.000 0.000 0.000
minisathackLR_GL_SHR_2011.03.02 63.667 36.333 0.000 0.000 0.000 0.000
minisathackMiniSAT_2.2.0.agile.26 63.000 37.000 0.000 0.000 0.000 0.000
minisathackminisat_psm_2011.04.01 65.667 34.333 0.000 0.000 0.000 0.000
minisathackreferenceminisat_2.2.0 64.667 35.333 0.000 0.000 0.000 0.000
MPhaseSAT64_2011.05.14_fixed_ 67.000 33.000 0.000 0.000 0.000 0.000
QuteRSat_2011.05.12_fixed_ 68.667 31.333 0.000 0.000 0.000 0.000
rcl_2011.04.01 61.333 38.667 0.000 0.000 0.000 0.000
RestartSAT_B95 67.000 33.000 0.000 0.000 0.000 0.000
SAT09referencesolverglucose_1.0 65.667 34.333 0.000 0.000 0.000 0.000
SAT09referencesolverprecosat_236 68.667 31.333 0.000 0.000 0.000 0.000

Dominated Algorithms

Here, you'll find an overview of dominating/dominated algorithms:
None of the algorithms was superior to any of the other.

An algorithm (A) is considered to be superior to an other algorithm (B), if it has at least an equal performance on all instances (compared to B) and if it is better on at least one of them. A missing value is automatically a worse performance. However, instances which could not be solved by either one of the algorithms, were not considered for the dominance relation.


Visualisations

Important note w.r.t. some of the following plots:
If appropriate, we imputed performance values for failed or censored runs. We used max + 0.3 * (max - min), in case of minimization problems, or min - 0.3 * (max - min), in case of maximization problems.
In addition, a small noise is added to the imputed values (except for the cluster matrix, based on correlations, which is shown at the end of this page).

Boxplots of performance values


Imputing the performance values of failed or censored runs (as described in the red note at the beginning of this section):
plot of chunk unnamed-chunk-4

Discarding the performance values of failed or censored runs:
## Warning: Removed 1797 rows containing non-finite values (stat_boxplot).
plot of chunk unnamed-chunk-5

Estimated densitities of performance values


Imputing the performance values of failed or censored runs (as described in the red note at the beginning of this section):
plot of chunk unnamed-chunk-6

Discarding the performance values of failed or censored runs:
plot of chunk unnamed-chunk-7

Estimated cumulative distribution functions of performance values


Imputing the performance values of failed runs (as described in the red note at the beginning of this section):
plot of chunk unnamed-chunk-8

Discarding the performance values of failed or censored runs:
plot of chunk unnamed-chunk-9

Scatterplot matrix of the performance values

The figure underneath shows pairwise scatterplots of the performance values.

Imputing the performance values of failed and censored runs (as described in the red note at the beginning of this section):
plot of chunk unnamed-chunk-10

Clustering algorithms based on their correlations

The following figure shows the correlations of the ranks of the performance values. Per default it will show the correlation coefficient of spearman. Missing values were imputed prior to computing the correlation coefficients. The algorithms are ordered in a way that similar (highly correlated) algorithms are close to each other. Per default the clustering is based on hierarchical clustering, using Ward's method.

plot of chunk unnamed-chunk-11