A Radial Layout

My first approach at generating a radial layout of the graph data logged by the theorem prover. Posted by Thomas Sutton on December 15, 2004

All of my work to date [as is now reflected by back posts below] has been on two tasks:

  1. generating runtime data dumps; and

  2. experimenting with radial layout techniques.

Generating data has been relatively easy. The automated reasoning system (one based on SCOTT I believe) already had the capability to output most of the data I need (like some statistics and the generated clauses that are kept) so I simply added the capability to output clauses that are discarded. After the data has been generated, I have a whole heap of scripts in a number of languages to translate it into a variety of formats, from CSV-like formats suitable for generating graphs of various statistics (using GNUplot) to a simple XML dialect which is then transformed into a number of others (for a couple of graph rendering packages) to dot (the language Graphviz uses to describe graphs).

On the radial layout front, I have been looking at papers describing a number of visualisation toolkits and radial layout algorithms for graphs and trees. I’ve modified a layout component from one of these toolkits (prefuse) to display my data in a radial layout, where radial distance is proportional to time. Unfortunately, this leads to very messy graphs like this one:

A naïve radial plot of the GRP024 problem

I’m going to try and simplify the dataset and see if that will help resolve the problem. If not, I think we’ll have to find another visualisation for the data.

This post was published on December 15, 2004 and last modified on June 4, 2020. It is tagged with: srp, logic, graph, visualisation.