Introduction

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 grouping information.

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.