Plans regarding the method for comparing two solvers according to [Mladen Nikolic, 2010].
More...
Plans regarding the method for comparing two solvers according to [Mladen Nikolic, 2010].
[Mladen Nikolic, 2010, Statistical Methodology for Comparison of SAT Solvers] is to appear in SAT 2010 proceedings.
 Todo:
 The wider framework
 Todo:
 Specifications for ProbabilityOfSuperiority.R

All functions need to be specified.

gwtest

gehanw

rcor

jackknifevariance

bootstrapvariance

probsup_solvcmp

probsup_solvcmp_files

read_probsup_solvcmp
 Todo:
 Write docus

How is the main function to be used? Examples?

Input specification:

DONE (yes, this is the case) It appears that the input is just a dataframe file, which per row contains the times for the two solvers A, B to be compared.

DONE (yes, needed) Is the knowledge of the cutofftime needed for the evaluation?

DONE (one row per instance As discussed in the paper, there are actually dependencies between the rows, in that a block of rows belongs to a single instances and its shuffled variations  however it seems for the computations performed this is irrelevant?

Output specification:

Besides the precise specification in computational terms, also the "meaning" needs to be specified.

Best if a precise probabilistic semantics can be given.

In any case, we need also a good discussion of the "intuitive
meaning".

What shall be achieved by the comparison? Is the underlying (precise) model, that one solver is better than the other iff the expected runtime over the space of sample inputs is lower?
Definition in file ProbabilityOfSuperiority.hpp.