satsolvers {llama}

Example data for Leveraging Learning to Automatically Manage Algorithms

Description

Performance data for 19 SAT solvers on 2433 SAT instances.

Usage

data(satsolvers)

Format

satsolvers is a list in the format returned by input and expected by the other functions of LLAMA. The list has the following components.

data:

The original input data merged. That is, the data frames processed by input in a single data frame with the following additional columns.

best:

The algorithm(s) with the best performance for each row.

*_success:

For each algorithm whether it was successful on the respective row.

features:

The names of the columns that contain feature values.

performance:

The names of the columns that contain performance data.

success:

The names of the columns indicating whether an algorithm was successful.

minimize:

Whether the performance is to be minimized.

cost:

The names of the columns that contain the feature group computation cost for each instance.

costGroups:

A list the maps the names of the feature groups to the list of feature names that are contained in it.

Details

Performance data for 19 SAT solvers on 2433 SAT instances. For each instance, 36 features were measured. In addition to the performance (time) on each instance, data on whether a solver timed out on an instance is included. The cost to compute all features is included as well.

Source

Hurley, B., Kotthoff, L., Malitsky, Y., O'Sullivan, B. (2014) Proteus: A Hierarchical Portfolio of Solvers and Transformations. Eleventh International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming.

See Also

input

Examples

data(satsolvers)