This experimental tool allows interactive visualization and exploration of
solver performance data. It is intended, in particular, as an aid to
understanding large-scale evaluations on collections of benchmark instances in
the satisfiability domain. It was developed primarily by Bryan Silverthorn as part of the borg project at The
University of Texas at Austin. A modern browser is required, and Google Chrome is strongly recommended.
Overview of functionality
This tool visualizes the computational cost, and the success or failure, of
runs made by different solvers on collections of instances of some decision
problem. The available collections are listed under "Data Set" on the left side
of this page. It provides two views into these data: the raw data can be
explored in the "Tabular View", and a similarity-based projection of all
instances can be analyzed in the "Projection View". A probabilistic model---the
same model that underlies the borg portfolio solver---is used to quantify
instances' similarity, defined as the KL divergence between their solver
runtime distributions as predicted by the model.
Details of the table view
The table view provides a compact representation of the raw data. Each row
corresponds to a problem instance, each column to a solver, and each cell to a
run. The color of a cell conveys the length of the run required to solve that
instance, where black cells denote runs that failed. The "best" run on a given
instance is marked by an asterisk. The names of satisfiable and unsatisfiable
instances are colored accordingly, and the cluster number for each instance
(the number of the model's most relevant mixture component) provides high-level
Details of the cluster view
The cluster view projects the set of problem instances into two dimensions.
Each point represents a problem instance, and the distance between two points
corresponds roughly to their similarity. Points are numbered by their dominant
cluster. Satisfiable instances are represented by a circle, unsatisfiable
instances by a diamond, and unknown instances by a square. Regions of this
projection can be selected; the properties of instances in each region are
included in the bar chart, which presents either the probability of each
solver's success on a random instance in the regions, or the runtime distribution
of a particular solver on instances in the regions.