Performance data for 19 SAT solvers on 2433 SAT instances.
satsolvers is a list in the format returned by
expected by the other functions of LLAMA. The list has the following components.
The original input data merged. That is, the data frames processed
input in a single data frame with the following additional
The algorithm(s) with the best performance for each row.
For each algorithm whether it was successful on the respective row.
The names of the columns that contain feature values.
The names of the columns that contain performance data.
The names of the columns indicating whether an algorithm was successful.
Whether the performance is to be minimized.
The names of the columns that contain the feature group computation cost for each instance.
A list the maps the names of the feature groups to the list of feature names that are contained in it.
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.
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.
Add the following code to your website.
For more information on customizing the embed code, read Embedding Snippets.