next up previous
Next: Some SAT Benchmarks Visualised Up: Translating SAT Instances to Previous: Some Simple Lossy Translations

Generating The Images

The presentation, i.e. the actual drawing, of a graph is important to the way one will interpret its contents. To generate the images of the graphs we used the `dot' tool available from http://www.research.att.com/sw/tools/graphviz/. This software attempts to draw a graph which attempts to expose hierarchical structure and keep the present the graph as simple as possible. For details of the algorithm see [1].

Using colour to enhance visualising the graph allows more information to be embedded into the translated instance. For the experiments presented below the edges of a graph were coloured according to the size of the clause used to define them. Binary clauses produced pure red, clauses of size nine or greater produced pure blue. All sizes in between were linearly blended between red and blue. The bound of nine was nominally chosen small enough to avoid a Sorites paradox. It also turns out that the normalised RGB values have amusing values due to the properties of the sequences in the reciprocals of some primes (for the 6 colour blends the two 3 digit values for red and blue channels gives a numerically decreasing sequence of digit cycles of 142857). The colours range approximately as follows: size 2, size 3, size 4, size 5, size 6, size 7, size 8, size 9.


next up previous
Next: Some SAT Benchmarks Visualised Up: Translating SAT Instances to Previous: Some Simple Lossy Translations
Last modified: 2004-03-17
Andrew Slater